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 (solver const &s, simplifier const &simp)

	~solver () override

	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 ()
	Create a backtracking point. More...

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	congruence_root (expr const &t) const

expr	congruence_next (expr const &t) const

expr	congruence_explain (expr const &a, expr const &b) const

void	set_initial_value (expr const &var, expr const &value)

void	set_initial_value (expr const &var, int i)

void	set_initial_value (expr const &var, bool b)

void	solve_for (expr_vector const &vars, expr_vector &terms, expr_vector &guards)

void	import_model_converter (solver const &src)

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)

virtual	~object ()=default

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 2892 of file z3++.h.

Constructor & Destructor Documentation

solver ( context & c )

inline

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

2902 :object(c) { init(Z3_mk_solver(c)); check_error(); }

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::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::object

object(context &c)

Definition: z3++.h:538

solver	(	context &	c,
		simple
	)

inline

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

2903 :object(c) { init(Z3_mk_simple_solver(c)); check_error(); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::object

object(context &c)

Definition: z3++.h:538

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 2904 of file z3++.h.

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

z3::object::object

object(context &c)

Definition: z3++.h:538

solver	(	context &	c,
		char const *	logic
	)

inline

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

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

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::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::object

object(context &c)

Definition: z3++.h:538

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

inline

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

2906 : object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); }

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

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:538

solver ( solver const & s )

inline

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

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

z3::object::object

object(context &c)

Definition: z3++.h:538

solver	(	solver const &	s,
		simplifier const &	simp
	)

inline

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

3364 :object(s) { init(Z3_solver_add_simplifier(s.ctx(), s, simp)); }

z3::object::object

object(context &c)

Definition: z3++.h:538

Z3_solver_add_simplifier

Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier)

Attach simplifier to a solver. The solver will use the simplifier for incremental pre-processing...

~solver ( )

inlineoverride

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

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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 2937 of file z3++.h.

Referenced by solver::add().

2937 { 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:541

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:540

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

inline

Definition at line 2938 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 2943 of file z3++.h.

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

void add ( expr_vector const & v )

inline

Definition at line 2946 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 2985 of file z3++.h.

Referenced by solver::to_smt2().

2985 { 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:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

z3::expr_vector

ast_vector_tpl< expr > expr_vector

Definition: z3++.h:77

check_result check ( )

inline

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

2954 { 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:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

Z3_lbool

Lifted Boolean type: false, undefined, true.

Definition: z3_api.h:57

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:178

check_result check	(	unsigned	n,
		expr *const	assumptions
	)

inline

Definition at line 2955 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 2965 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);
         }

expr congruence_explain	(	expr const &	a,
		expr const &	b
	)		const

inline

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

                                                                     {
             check_context(*this, a);
             check_context(*this, b);
             Z3_ast r = Z3_solver_congruence_explain(ctx(), m_solver, a, b);
             check_error();
             return expr(ctx(), r);
         }

expr congruence_next ( expr const & t ) const

inline

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

                                                   {
             check_context(*this, t);
             Z3_ast r = Z3_solver_congruence_next(ctx(), m_solver, t);
             check_error();
             return expr(ctx(), r);
         }

expr congruence_root ( expr const & t ) const

inline

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

                                                   {
             check_context(*this, t);
             Z3_ast r = Z3_solver_congruence_root(ctx(), m_solver, t);
             check_error();
             return expr(ctx(), r);
         }

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

inline

Definition at line 2977 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 3077 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 3164 of file z3++.h.

3164 { return cube_generator(*this); }

cube_generator cubes ( expr_vector & vars )

inline

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

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

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

inline

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

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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 2951 of file z3++.h.

2951 { 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:248

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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 2952 of file z3++.h.

2952 { 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:248

Z3_solver_from_string

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

load solver assertions from a string.

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

model get_model ( ) const

inline

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

2976 { 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:541

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:540

param_descrs get_param_descrs ( )

inline

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

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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.

void import_model_converter ( solver const & src )

inline

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

                                                        {
             check_context(*this, src);
             Z3_solver_import_model_converter(ctx(), src.m_solver, m_solver);
             check_error();
         }

expr_vector non_units ( ) const

inline

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

2986 { 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:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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:77

operator Z3_solver ( ) const

inline

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

2910 { return m_solver; }

solver& operator= ( solver const & s )

inline

Definition at line 2911 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 2935 of file z3++.h.

2935 { 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:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

expr proof ( ) const

inline

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

3049 { 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:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

void push ( )

inline

Create a backtracking point.

The solver contains a stack of assertions.

See also: Z3_solver_get_num_scopes; Z3_solver_pop

def_API('Z3_solver_push', VOID, (_in(CONTEXT), _in(SOLVER)))

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

2934 { 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:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

std::string reason_unknown ( ) const

inline

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

2982 { 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:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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:50

void reset ( )

inline

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

2936 { 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:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

void set ( params const & p )

inline

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

2918 { 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:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

void set	(	char const *	k,
		bool	v
	)

inline

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

Referenced by solver::set().

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

z3::solver::set

void set(params const &p)

Definition: z3++.h:2918

void set	(	char const *	k,
		unsigned	v
	)

inline

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

Referenced by solver::set().

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

z3::solver::set

void set(params const &p)

Definition: z3++.h:2918

void set	(	char const *	k,
		double	v
	)

inline

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

Referenced by solver::set().

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

z3::solver::set

void set(params const &p)

Definition: z3++.h:2918

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

inline

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

Referenced by solver::set().

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

z3::solver::set

void set(params const &p)

Definition: z3++.h:2918

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

inline

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

Referenced by solver::set().

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

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

z3::solver::set

void set(params const &p)

Definition: z3++.h:2918

void set_initial_value	(	expr const &	var,
		expr const &	value
	)

inline

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

Referenced by solver::set_initial_value().

                                                                    {
             Z3_solver_set_initial_value(ctx(), m_solver, var, value);
             check_error();
         }

void set_initial_value	(	expr const &	var,
		int	i
	)

inline

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

                                                        {
             set_initial_value(var, ctx().num_val(i, var.get_sort()));
         }

void set_initial_value	(	expr const &	var,
		bool	b
	)

inline

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

                                                         {
             set_initial_value(var, ctx().bool_val(b));            
         }

void solve_for	(	expr_vector const &	vars,
		expr_vector &	terms,
		expr_vector &	guards
	)

inline

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

                                                                                          {
             // Create a copy of vars since the C API modifies the variables vector
             expr_vector variables(ctx());
             for (unsigned i = 0; i < vars.size(); ++i) {
                 check_context(*this, vars[i]);
                 variables.push_back(vars[i]);
             }
             // Clear output vectors before calling C API
             terms = expr_vector(ctx());
             guards = expr_vector(ctx());
             Z3_solver_solve_for(ctx(), m_solver, variables, terms, guards);
             check_error();
         }

stats statistics ( ) const

inline

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

2983 { 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:541

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:540

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

inline

Definition at line 3052 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 2988 of file z3++.h.

2988 { 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:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

z3::expr_vector

ast_vector_tpl< expr > expr_vector

Definition: z3++.h:77

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 2989 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; 
         }