Data Structures | |
class | handle |
Public Member Functions | |
optimize (context &c) | |
optimize (optimize &o) | |
optimize & | operator= (optimize const &o) |
~optimize () | |
operator Z3_optimize () const | |
void | add (expr const &e) |
handle | add (expr const &e, unsigned weight) |
void | add (expr const &e, expr const &t) |
handle | add (expr const &e, char const *weight) |
handle | maximize (expr const &e) |
handle | minimize (expr const &e) |
void | push () |
void | pop () |
check_result | check () |
check_result | check (expr_vector const &asms) |
model | get_model () const |
expr_vector | unsat_core () const |
void | set (params const &p) |
expr | lower (handle const &h) |
expr | upper (handle const &h) |
expr_vector | assertions () const |
expr_vector | objectives () const |
stats | statistics () const |
void | from_file (char const *filename) |
void | from_string (char const *constraints) |
std::string | help () const |
![]() | |
object (context &c) | |
object (object const &s) | |
context & | ctx () const |
Z3_error_code | check_error () const |
Friends | |
std::ostream & | operator<< (std::ostream &out, optimize const &s) |
Additional Inherited Members | |
![]() | |
context * | m_ctx |
|
inline |
|
inline |
|
inline |
Definition at line 2774 of file z3++.h.
|
inline |
Definition at line 2749 of file z3++.h.
|
inline |
Definition at line 2750 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 2775 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 2776 of file z3++.h.
|
inline |
Definition at line 2762 of file z3++.h.