Z3
 
Loading...
Searching...
No Matches
solver Class Reference

#include <z3++.h>

+ 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
 
solveroperator= (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.
 
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
 
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)
 
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
 
contextctx () 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
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

◆ solver() [1/7]

solver ( context & c)
inline

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

2771:object(c) { init(Z3_mk_solver(c)); check_error(); }
Z3_error_code check_error() const
Definition z3++.h:475
object(context &c)
Definition z3++.h:472
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 ...

Referenced by Solver::__del__(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::check(), Solver::model(), Solver::num_scopes(), Solver::pop(), Solver::push(), Solver::reset(), and Solver::set().

◆ solver() [2/7]

solver ( context & c,
simple  )
inline

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

2772:object(c) { init(Z3_mk_simple_solver(c)); check_error(); }
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.

Referenced by Solver::__del__(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::check(), Solver::model(), Solver::num_scopes(), Solver::pop(), Solver::push(), Solver::reset(), and Solver::set().

◆ solver() [3/7]

◆ solver() [4/7]

solver ( context & c,
char const * logic )
inline

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

2774:object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); check_error(); }
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...

Referenced by Solver::__del__(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::check(), Solver::model(), Solver::num_scopes(), Solver::pop(), Solver::push(), Solver::reset(), and Solver::set().

◆ solver() [5/7]

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

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

2775: object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); }
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.

Referenced by Solver::__del__(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::check(), Solver::model(), Solver::num_scopes(), Solver::pop(), Solver::push(), Solver::reset(), and Solver::set().

◆ solver() [6/7]

◆ solver() [7/7]

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

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

3194:object(s) { init(Z3_solver_add_simplifier(s.ctx(), s, simp)); }
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.

Referenced by Solver::__del__(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::check(), Solver::model(), Solver::num_scopes(), Solver::pop(), Solver::push(), Solver::reset(), and Solver::set().

◆ ~solver()

~solver ( )
inlineoverride

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

2778{ Z3_solver_dec_ref(ctx(), m_solver); }
context & ctx() const
Definition z3++.h:474
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.

Member Function Documentation

◆ add() [1/4]

void add ( expr const & e)
inline

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

2806{ assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.

Referenced by Solver::__iadd__(), solver::add(), and solver::add().

◆ add() [2/4]

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

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

2812 {
2813 add(e, ctx().bool_const(p));
2814 }
void add(expr const &e)
Definition z3++.h:2806

Referenced by Solver::__iadd__().

◆ add() [3/4]

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

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

2807 {
2808 assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
2809 Z3_solver_assert_and_track(ctx(), m_solver, e, p);
2810 check_error();
2811 }
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.

Referenced by Solver::__iadd__().

◆ add() [4/4]

void add ( expr_vector const & v)
inline

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

2815 {
2816 check_context(*this, v);
2817 for (unsigned i = 0; i < v.size(); ++i)
2818 add(v[i]);
2819 }
friend void check_context(object const &a, object const &b)
Definition z3++.h:478

Referenced by Solver::__iadd__().

◆ assertions()

expr_vector assertions ( ) const
inline

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

2854{ Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
ast_vector_tpl< expr > expr_vector
Definition z3++.h:76

Referenced by solver::to_smt2().

◆ check() [1/3]

check_result check ( )
inline

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

2823{ Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
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_lbool
Lifted Boolean type: false, undefined, true.
Definition z3_api.h:61
check_result to_check_result(Z3_lbool l)
Definition z3++.h:147

◆ check() [2/3]

check_result check ( expr_vector const & assumptions)
inline

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

2834 {
2835 unsigned n = assumptions.size();
2836 array<Z3_ast> _assumptions(n);
2837 for (unsigned i = 0; i < n; i++) {
2838 check_context(*this, assumptions[i]);
2839 _assumptions[i] = assumptions[i];
2840 }
2841 Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2842 check_error();
2843 return to_check_result(r);
2844 }
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not.

◆ check() [3/3]

check_result check ( unsigned n,
expr *const assumptions )
inline

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

2824 {
2825 array<Z3_ast> _assumptions(n);
2826 for (unsigned i = 0; i < n; i++) {
2827 check_context(*this, assumptions[i]);
2828 _assumptions[i] = assumptions[i];
2829 }
2830 Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2831 check_error();
2832 return to_check_result(r);
2833 }

◆ consequences()

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

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

2846 {
2847 Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
2848 check_error();
2849 return to_check_result(r);
2850 }
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.

◆ cube()

expr_vector cube ( expr_vector & vars,
unsigned cutoff )
inline

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

2907 {
2908 Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
2909 check_error();
2910 return expr_vector(ctx(), r);
2911 }
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)
extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...

◆ cubes() [1/2]

cube_generator cubes ( )
inline

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

2994{ return cube_generator(*this); }

◆ cubes() [2/2]

cube_generator cubes ( expr_vector & vars)
inline

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

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

◆ dimacs()

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

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

2902{ return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }
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.

◆ from_file()

void from_file ( char const * file)
inline

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

2820{ Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
void check_parser_error() const
Definition z3++.h:199
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.

◆ from_string()

void from_string ( char const * s)
inline

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

2821{ Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string str)
load solver assertions from a string.

◆ get_model()

model get_model ( ) const
inline

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

2845{ Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
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.

◆ get_param_descrs()

param_descrs get_param_descrs ( )
inline

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

2904{ return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }
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.

◆ non_units()

expr_vector non_units ( ) const
inline

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

2855{ Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
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.

◆ operator Z3_solver()

operator Z3_solver ( ) const
inline

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

2779{ return m_solver; }

◆ operator=()

solver & operator= ( solver const & s)
inline

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

2780 {
2781 Z3_solver_inc_ref(s.ctx(), s.m_solver);
2782 Z3_solver_dec_ref(ctx(), m_solver);
2783 object::operator=(s);
2784 m_solver = s.m_solver;
2785 return *this;
2786 }
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.

◆ pop()

void pop ( unsigned n = 1)
inline

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

2804{ Z3_solver_pop(ctx(), m_solver, n); check_error(); }
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.

Referenced by Solver::__exit__().

◆ proof()

expr proof ( ) const
inline

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

2879{ Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
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.

◆ push()

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

2803{ Z3_solver_push(ctx(), m_solver); check_error(); }
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.

Referenced by Solver::__enter__().

◆ reason_unknown()

std::string reason_unknown ( ) const
inline

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

2851{ Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition z3_api.h:53
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...

◆ reset()

void reset ( )
inline

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

2805{ Z3_solver_reset(ctx(), m_solver); check_error(); }
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.

◆ set() [1/6]

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

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

2788{ params p(ctx()); p.set(k, v); set(p); }
void set(params const &p)
Definition z3++.h:2787

Referenced by solver::set().

◆ set() [2/6]

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

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

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

Referenced by solver::set().

◆ set() [3/6]

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

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

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

Referenced by solver::set().

◆ set() [4/6]

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

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

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

Referenced by solver::set().

◆ set() [5/6]

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

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

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

Referenced by solver::set().

◆ set() [6/6]

void set ( params const & p)
inline

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

2787{ Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.

◆ set_initial_value() [1/3]

void set_initial_value ( expr const & var,
bool b )
inline

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

2875 {
2876 set_initial_value(var, ctx().bool_val(b));
2877 }
void set_initial_value(expr const &var, expr const &value)
Definition z3++.h:2868

◆ set_initial_value() [2/3]

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

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

2868 {
2869 Z3_solver_set_initial_value(ctx(), m_solver, var, value);
2870 check_error();
2871 }
void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast v, Z3_ast val)
provide an initialization hint to the solver. The initialization hint is used to calibrate an initial...

Referenced by solver::set_initial_value(), and solver::set_initial_value().

◆ set_initial_value() [3/3]

void set_initial_value ( expr const & var,
int i )
inline

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

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

◆ statistics()

stats statistics ( ) const
inline

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

2852{ Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.

◆ to_smt2()

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

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

2882 {
2883 array<Z3_ast> es(assertions());
2884 Z3_ast const* fmls = es.ptr();
2885 Z3_ast fml = 0;
2886 unsigned sz = es.size();
2887 if (sz > 0) {
2888 --sz;
2889 fml = fmls[sz];
2890 }
2891 else {
2892 fml = ctx().bool_val(true);
2893 }
2894 return std::string(Z3_benchmark_to_smtlib_string(
2895 ctx(),
2896 "", "", status, "",
2897 sz,
2898 fmls,
2899 fml));
2900 }
expr bool_val(bool b)
Definition z3++.h:3791
expr_vector assertions() const
Definition z3++.h:2854
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.

◆ trail() [1/2]

expr_vector trail ( ) const
inline

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

2857{ Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
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...

◆ trail() [2/2]

expr_vector trail ( array< unsigned > & levels) const
inline

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

2858 {
2859 Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver);
2860 check_error();
2861 expr_vector result(ctx(), r);
2862 unsigned sz = result.size();
2863 levels.resize(sz);
2864 Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.ptr());
2865 check_error();
2866 return result;
2867 }
void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[])
retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat c...

◆ units()

expr_vector units ( ) const
inline

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

2856{ Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.

◆ unsat_core()

expr_vector unsat_core ( ) const
inline

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

2853{ Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...

Friends And Related Symbol Documentation

◆ operator<<

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

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

2998{ out << Z3_solver_to_string(s.ctx(), s); return out; }
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.