#include <z3++.h>
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 () | |
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. | |
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) |
![]() | |
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 | |
![]() | |
context * | m_ctx |
Definition at line 2742 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::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
Definition at line 2743 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::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
Definition at line 2744 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::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
Definition at line 2745 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::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
Definition at line 2746 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::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
Definition at line 2747 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::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
|
inline |
Definition at line 3154 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::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().
|
inline |
|
inline |
Definition at line 2777 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), Optimize::__iadd__(), solver::add(), and solver::add().
|
inline |
Definition at line 2783 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().
Definition at line 2778 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().
|
inline |
Definition at line 2786 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().
|
inline |
Definition at line 2825 of file z3++.h.
Referenced by solver::to_smt2(), and Solver::to_smt2().
|
inline |
|
inline |
Definition at line 2805 of file z3++.h.
|
inline |
Definition at line 2795 of file z3++.h.
|
inline |
Definition at line 2817 of file z3++.h.
|
inline |
Definition at line 2867 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 2826 of file z3++.h.
|
inline |
Definition at line 2751 of file z3++.h.
|
inline |
Definition at line 2775 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 2774 of file z3++.h.
Referenced by Solver::__enter__().
|
inline |
Definition at line 2822 of file z3++.h.
|
inline |
|
inline |
|
inline |
Definition at line 2763 of file z3++.h.
Referenced by solver::set().
|
inline |
Definition at line 2761 of file z3++.h.
Referenced by solver::set().
|
inline |
Definition at line 2762 of file z3++.h.
Referenced by solver::set().
|
inline |
Definition at line 2760 of file z3++.h.
Referenced by solver::set().
|
inline |
|
inline |
Definition at line 2823 of file z3++.h.
|
inline |
Definition at line 2842 of file z3++.h.
|
inline |
Definition at line 2828 of file z3++.h.
Referenced by Solver::trail_levels().
|
inline |
Definition at line 2829 of file z3++.h.
Referenced by Solver::trail_levels().
|
inline |
Definition at line 2827 of file z3++.h.
|
inline |
Definition at line 2824 of file z3++.h.