#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 () 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. | |
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) |
![]() | |
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 | |
![]() | |
context * | m_ctx |
Definition at line 2771 of file z3++.h.
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().
Definition at line 2772 of file z3++.h.
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().
Definition at line 2773 of file z3++.h.
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().
Definition at line 2774 of file z3++.h.
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().
Definition at line 2775 of file z3++.h.
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().
Definition at line 2776 of file z3++.h.
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().
|
inline |
Definition at line 3194 of file z3++.h.
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().
|
inlineoverride |
|
inline |
Definition at line 2806 of file z3++.h.
Referenced by Solver::__iadd__(), solver::add(), and solver::add().
|
inline |
Definition at line 2807 of file z3++.h.
Referenced by Solver::__iadd__().
|
inline |
Definition at line 2815 of file z3++.h.
Referenced by Solver::__iadd__().
|
inline |
Definition at line 2854 of file z3++.h.
Referenced by solver::to_smt2().
|
inline |
|
inline |
Definition at line 2834 of file z3++.h.
|
inline |
Definition at line 2824 of file z3++.h.
|
inline |
Definition at line 2846 of file z3++.h.
|
inline |
Definition at line 2907 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 2855 of file z3++.h.
|
inline |
Definition at line 2780 of file z3++.h.
|
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 2868 of file z3++.h.
Referenced by solver::set_initial_value(), and 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.
|
inline |
Definition at line 2858 of file z3++.h.
|
inline |
Definition at line 2856 of file z3++.h.
|
inline |
Definition at line 2853 of file z3++.h.