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 |
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 |
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 |
Definition at line 2771 of file z3++.h.
Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
Definition at line 2772 of file z3++.h.
Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
Definition at line 2773 of file z3++.h.
Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
Definition at line 2774 of file z3++.h.
Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
Definition at line 2775 of file z3++.h.
Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
Definition at line 2776 of file z3++.h.
Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
|
inline |
Definition at line 3194 of file z3++.h.
Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
|
inlineoverride |
|
inline |
Definition at line 2806 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), Optimize::__iadd__(), and solver::add().
|
inline |
Definition at line 2812 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().
Definition at line 2807 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().
|
inline |
Definition at line 2815 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().
|
inline |
Definition at line 2854 of file z3++.h.
Referenced by solver::to_smt2(), and Solver::to_smt2().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 2855 of file z3++.h.
|
inline |
|
inline |
Definition at line 2804 of file z3++.h.
Referenced by Solver::__exit__().
|
inline |
|
inline |
Create a backtracking point.
The solver contains a stack of assertions.
def_API('Z3_solver_push', VOID, (_in(CONTEXT), _in(SOLVER)))
Definition at line 2803 of file z3++.h.
Referenced by Solver::__enter__().
|
inline |
Definition at line 2851 of file z3++.h.
|
inline |
|
inline |
|
inline |
Definition at line 2792 of file z3++.h.
Referenced by solver::set().
|
inline |
Definition at line 2790 of file z3++.h.
Referenced by solver::set().
|
inline |
Definition at line 2791 of file z3++.h.
Referenced by solver::set().
|
inline |
Definition at line 2789 of file z3++.h.
Referenced by solver::set().
|
inline |
|
inline |
Definition at line 2875 of file z3++.h.
Definition at line 2868 of file z3++.h.
Referenced by solver::set_initial_value().
|
inline |
|
inline |
Definition at line 2852 of file z3++.h.
|
inline |
Definition at line 2882 of file z3++.h.
|
inline |
Definition at line 2857 of file z3++.h.
Referenced by Solver::trail_levels().
|
inline |
Definition at line 2858 of file z3++.h.
Referenced by Solver::trail_levels().
|
inline |
Definition at line 2856 of file z3++.h.
|
inline |
Definition at line 2853 of file z3++.h.