Data Structures | |
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 () | |
operator Z3_solver () const | |
solver & | operator= (solver const &s) |
void | set (params const &p) |
void | push () |
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) |
check_result | check () |
check_result | check (unsigned n, expr *const assumptions) |
check_result | check (expr_vector 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 | proof () const |
std::string | to_smt2 (char const *status="unknown") |
param_descrs | get_param_descrs () |
![]() | |
object (context &c) | |
object (object const &s) | |
context & | ctx () const |
void | check_error () const |
Friends | |
std::ostream & | operator<< (std::ostream &out, solver const &s) |
Additional Inherited Members | |
![]() | |
context * | m_ctx |
|
inline |
|
inline |
Definition at line 1714 of file z3++.h.
Referenced by Fixedpoint::__iadd__(), and Optimize::__iadd__().
Definition at line 1715 of file z3++.h.
Referenced by Fixedpoint::__iadd__(), and Optimize::__iadd__().
|
inline |
Definition at line 1720 of file z3++.h.
Referenced by Fixedpoint::__iadd__(), and Optimize::__iadd__().
|
inline |
Definition at line 1754 of file z3++.h.
Referenced by Solver::to_smt2().
|
inline |
|
inline |
Definition at line 1724 of file z3++.h.
|
inline |
Definition at line 1734 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 1751 of file z3++.h.
|
inline |
|
inline |
|
inline |
Definition at line 1752 of file z3++.h.
|
inline |
Definition at line 1758 of file z3++.h.
|
inline |
Definition at line 1753 of file z3++.h.