Inheritance diagram for solver:

Data Structures
class	cube_generator

class	cube_iterator

struct	simple

struct	translate

Public Member Functions
	solver (context &c)

	solver (context &c, simple)

	solver (context &c, Z3_solver s)

	solver (context &c, char const *logic)

	solver (context &c, solver const &src, translate)

	solver (solver const &s)

	~solver ()

	operator Z3_solver () const

solver &	operator= (solver const &s)

void	set (params const &p)

void	set (char const *k, bool v)

void	set (char const *k, unsigned v)

void	set (char const *k, double v)

void	set (char const *k, symbol const &v)

void	set (char const k, char const v)

void	push ()

void	pop (unsigned n=1)

void	reset ()

void	add (expr const &e)

void	add (expr const &e, expr const &p)

void	add (expr const &e, char const *p)

void	add (expr_vector const &v)

void	from_file (char const *file)

void	from_string (char const *s)

check_result	check ()

check_result	check (unsigned n, expr *const assumptions)

check_result	check (expr_vector const &assumptions)

model	get_model () const

check_result	consequences (expr_vector &assumptions, expr_vector &vars, expr_vector &conseq)

std::string	reason_unknown () const

stats	statistics () const

expr_vector	unsat_core () const

expr_vector	assertions () const

expr_vector	non_units () const

expr_vector	units () const

expr_vector	trail () const

expr_vector	trail (array< unsigned > &levels) const

expr	proof () const

std::string	to_smt2 (char const *status="unknown")

std::string	dimacs (bool include_names=true) const

param_descrs	get_param_descrs ()

expr_vector	cube (expr_vector &vars, unsigned cutoff)

cube_generator	cubes ()

cube_generator	cubes (expr_vector &vars)

Public Member Functions inherited from object
	object (context &c)

context &	ctx () const

Z3_error_code	check_error () const

Friends
std::ostream &	operator<< (std::ostream &out, solver const &s)

Additional Inherited Members
Protected Attributes inherited from object
context *	m_ctx

Detailed Description

Definition at line 2619 of file z3++.h.

Constructor & Destructor Documentation

solver ( context & c )

inline

Definition at line 2628 of file z3++.h.

2628 :object(c) { init(Z3_mk_solver(c)); }

Z3_mk_solver

Z3_solver Z3_API Z3_mk_solver(Z3_context c)

Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...

z3::object::object

object(context &c)

Definition: z3++.h:427

solver	(	context &	c,
		simple
	)

inline

Definition at line 2629 of file z3++.h.

2629 :object(c) { init(Z3_mk_simple_solver(c)); }

z3::object::object

object(context &c)

Definition: z3++.h:427

Z3_mk_simple_solver

Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)

Create a new incremental solver.

solver	(	context &	c,
		Z3_solver	s
	)

inline

Definition at line 2630 of file z3++.h.

2630 :object(c) { init(s); }

z3::object::object

object(context &c)

Definition: z3++.h:427

solver	(	context &	c,
		char const *	logic
	)

inline

Definition at line 2631 of file z3++.h.

2631 :object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }

Z3_mk_solver_for_logic

Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)

Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...

z3::object::object

object(context &c)

Definition: z3++.h:427

solver	(	context &	c,
		solver const &	src,
		translate
	)

inline

Definition at line 2632 of file z3++.h.

2632 : object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }

Z3_solver_translate

Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)

Copy a solver s from the context source to the context target.

z3::object::object

object(context &c)

Definition: z3++.h:427

solver ( solver const & s )

inline

Definition at line 2633 of file z3++.h.

2633 :object(s) { init(s.m_solver); }

z3::object::object

object(context &c)

Definition: z3++.h:427

~solver ( )

inline

Definition at line 2634 of file z3++.h.

2634 { Z3_solver_dec_ref(ctx(), m_solver); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

Z3_solver_dec_ref

void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)

Decrement the reference counter of the given solver.

Member Function Documentation

void add ( expr const & e )

inline

Definition at line 2652 of file z3++.h.

Referenced by solver::add().

2652 { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

Z3_solver_assert

void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)

Assert a constraint into the solver.

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

void add	(	expr const &	e,
		expr const &	p
	)

inline

Definition at line 2653 of file z3++.h.

                                                  {
             assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
             Z3_solver_assert_and_track(ctx(), m_solver, e, p);
             check_error();
         }

void add	(	expr const &	e,
		char const *	p
	)

inline

Definition at line 2658 of file z3++.h.

                                                  {
             add(e, ctx().bool_const(p));
         }        

void add ( expr_vector const & v )

inline

Definition at line 2661 of file z3++.h.

                                        { 
             check_context(*this, v); 
             for (unsigned i = 0; i < v.size(); ++i) 
                 add(v[i]); 
         }

expr_vector assertions ( ) const

inline

Definition at line 2700 of file z3++.h.

Referenced by solver::to_smt2().

2700 { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

Z3_solver_get_assertions

Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)

Return the set of asserted formulas on the solver.

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

z3::expr_vector

ast_vector_tpl< expr > expr_vector

Definition: z3++.h:73

check_result check ( )

inline

Definition at line 2669 of file z3++.h.

2669 { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

Z3_lbool

Lifted Boolean type: false, undefined, true.

Definition: z3_api.h:101

Z3_solver_check

Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s)

Check whether the assertions in a given solver are consistent or not.

z3::to_check_result

check_result to_check_result(Z3_lbool l)

Definition: z3++.h:144

check_result check	(	unsigned	n,
		expr *const	assumptions
	)

inline

Definition at line 2670 of file z3++.h.

                                                                  {
             array<Z3_ast> _assumptions(n);
             for (unsigned i = 0; i < n; i++) {
                 check_context(*this, assumptions[i]);
                 _assumptions[i] = assumptions[i];
             }
             Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
             check_error();
             return to_check_result(r);
         }

check_result check ( expr_vector const & assumptions )

inline

Definition at line 2680 of file z3++.h.

                                                            {
             unsigned n = assumptions.size();
             array<Z3_ast> _assumptions(n);
             for (unsigned i = 0; i < n; i++) {
                 check_context(*this, assumptions[i]);
                 _assumptions[i] = assumptions[i];
             }
             Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
             check_error();
             return to_check_result(r);
         }

check_result consequences	(	expr_vector &	assumptions,
		expr_vector &	vars,
		expr_vector &	conseq
	)

inline

Definition at line 2692 of file z3++.h.

                                                                                                     {
             Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
             check_error();
             return to_check_result(r);
         }

expr_vector cube	(	expr_vector &	vars,
		unsigned	cutoff
	)

inline

Definition at line 2742 of file z3++.h.

                                                              {
             Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
             check_error();
             return expr_vector(ctx(), r);
         }

cube_generator cubes ( )

inline

Definition at line 2829 of file z3++.h.

2829 { return cube_generator(*this); }

cube_generator cubes ( expr_vector & vars )

inline

Definition at line 2830 of file z3++.h.

2830 { return cube_generator(*this, vars); }

std::string dimacs ( bool include_names = true ) const

inline

Definition at line 2737 of file z3++.h.

2737 { return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

Z3_solver_to_dimacs_string

Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names)

Convert a solver into a DIMACS formatted string.

void from_file ( char const * file )

inline

Definition at line 2666 of file z3++.h.

2666 { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }

z3::context::check_parser_error

void check_parser_error() const

Definition: z3++.h:195

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

Z3_solver_from_file

void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)

load solver assertions from a file.

void from_string ( char const * s )

inline

Definition at line 2667 of file z3++.h.

2667 { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }

z3::context::check_parser_error

void check_parser_error() const

Definition: z3++.h:195

Z3_solver_from_string

void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)

load solver assertions from a string.

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

model get_model ( ) const

inline

Definition at line 2691 of file z3++.h.

2691 { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

Z3_solver_get_model

Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)

Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

param_descrs get_param_descrs ( )

inline

Definition at line 2739 of file z3++.h.

2739 { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

Z3_solver_get_param_descrs

Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)

Return the parameter description set for the given solver object.

expr_vector non_units ( ) const

inline

Definition at line 2701 of file z3++.h.

2701 { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

Z3_solver_get_non_units

Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)

Return the set of non units in the solver state.

z3::expr_vector

ast_vector_tpl< expr > expr_vector

Definition: z3++.h:73

operator Z3_solver ( ) const

inline

Definition at line 2635 of file z3++.h.

2635 { return m_solver; }

solver& operator= ( solver const & s )

inline

Definition at line 2636 of file z3++.h.

                                              {
             Z3_solver_inc_ref(s.ctx(), s.m_solver);
             Z3_solver_dec_ref(ctx(), m_solver);
             object::operator=(s);
             m_solver = s.m_solver;
             return *this;
         }

void pop ( unsigned n = 1 )

inline

Definition at line 2650 of file z3++.h.

2650 { Z3_solver_pop(ctx(), m_solver, n); check_error(); }

Z3_solver_pop

void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)

Backtrack n backtracking points.

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

expr proof ( ) const

inline

Definition at line 2714 of file z3++.h.

2714 { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }

Z3_solver_get_proof

Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)

Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

void push ( )

inline

Definition at line 2649 of file z3++.h.

2649 { Z3_solver_push(ctx(), m_solver); check_error(); }

Z3_solver_push

void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)

Create a backtracking point.

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

std::string reason_unknown ( ) const

inline

Definition at line 2697 of file z3++.h.

2697 { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

Z3_solver_get_reason_unknown

Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)

Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...

Z3_string

const char * Z3_string

Z3 string type. It is just an alias for const char *.

Definition: z3_api.h:84

void reset ( )

inline

Definition at line 2651 of file z3++.h.

2651 { Z3_solver_reset(ctx(), m_solver); check_error(); }

Z3_solver_reset

void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)

Remove all assertions from the solver.

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

void set ( params const & p )

inline

Definition at line 2643 of file z3++.h.

2643 { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }

Z3_solver_set_params

void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)

Set the given solver using the given parameters.

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

void set	(	char const *	k,
		bool	v
	)

inline

Definition at line 2644 of file z3++.h.

Referenced by solver::set().

2644 { params p(ctx()); p.set(k, v); set(p); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

z3::solver::set

void set(params const &p)

Definition: z3++.h:2643

void set	(	char const *	k,
		unsigned	v
	)

inline

Definition at line 2645 of file z3++.h.

Referenced by solver::set().

2645 { params p(ctx()); p.set(k, v); set(p); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

z3::solver::set

void set(params const &p)

Definition: z3++.h:2643

void set	(	char const *	k,
		double	v
	)

inline

Definition at line 2646 of file z3++.h.

Referenced by solver::set().

2646 { params p(ctx()); p.set(k, v); set(p); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

z3::solver::set

void set(params const &p)

Definition: z3++.h:2643

void set	(	char const *	k,
		symbol const &	v
	)

inline

Definition at line 2647 of file z3++.h.

Referenced by solver::set().

2647 { params p(ctx()); p.set(k, v); set(p); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

z3::solver::set

void set(params const &p)

Definition: z3++.h:2643

void set	(	char const *	k,
		char const *	v
	)

inline

Definition at line 2648 of file z3++.h.

Referenced by solver::set().

2648 { params p(ctx()); p.set(k, v); set(p); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

z3::solver::set

void set(params const &p)

Definition: z3++.h:2643

stats statistics ( ) const

inline

Definition at line 2698 of file z3++.h.

2698 { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

Z3_solver_get_statistics

Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)

Return statistics for the given solver.

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

std::string to_smt2 ( char const * status = "unknown" )

inline

Definition at line 2717 of file z3++.h.

                                                           {
             array<Z3_ast> es(assertions());
             Z3_ast const* fmls = es.ptr();
             Z3_ast fml = 0;
             unsigned sz = es.size();
             if (sz > 0) {
                 --sz;
                 fml = fmls[sz];
             }
             else {
                 fml = ctx().bool_val(true);
             }
             return std::string(Z3_benchmark_to_smtlib_string(
                                    ctx(),
                                    "", "", status, "",
                                    sz,
                                    fmls,
                                    fml));
         }

expr_vector trail ( ) const

inline

Definition at line 2703 of file z3++.h.

2703 { Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:429

z3::object::ctx

context & ctx() const

Definition: z3++.h:428

z3::expr_vector

ast_vector_tpl< expr > expr_vector

Definition: z3++.h:73

Z3_solver_get_trail

Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s)

Return the trail modulo model conversion, in order of decision level The decision level can be retrie...

expr_vector trail ( array< unsigned > & levels ) const

inline

Definition at line 2704 of file z3++.h.

                                                          { 
             Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); 
             check_error(); 
             expr_vector result(ctx(), r);
             unsigned sz = result.size();
             levels.resize(sz);
             Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.ptr());
             check_error(); 
             return result; 
         }