Data Structures | |
class | handle |
Public Member Functions | |
optimize (context &c) | |
optimize (optimize const &o) | |
optimize (context &c, optimize &src) | |
optimize & | operator= (optimize const &o) |
~optimize () override | |
operator Z3_optimize () const | |
void | add (expr const &e) |
void | add (expr_vector const &es) |
void | add (expr const &e, expr const &t) |
void | add (expr const &e, char const *p) |
handle | add_soft (expr const &e, unsigned weight) |
handle | add_soft (expr const &e, char const *weight) |
handle | add (expr const &e, unsigned weight) |
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) |
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 |
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, optimize const &s) |
Additional Inherited Members | |
Protected Attributes inherited from object | |
context * | m_ctx |
Definition at line 3297 of file z3++.h.
Referenced by Optimize::__deepcopy__(), Optimize::__del__(), Optimize::add_soft(), Optimize::assert_and_track(), Optimize::assert_exprs(), Optimize::assertions(), Optimize::check(), Optimize::from_file(), Optimize::from_string(), Optimize::help(), Optimize::maximize(), Optimize::minimize(), Optimize::model(), Optimize::objectives(), Optimize::param_descrs(), Optimize::pop(), Optimize::push(), Optimize::reason_unknown(), Optimize::set(), Optimize::set_initial_value(), Optimize::set_on_model(), Optimize::sexpr(), Optimize::statistics(), and Optimize::unsat_core().
Definition at line 3298 of file z3++.h.
Referenced by Optimize::__deepcopy__(), Optimize::__del__(), Optimize::add_soft(), Optimize::assert_and_track(), Optimize::assert_exprs(), Optimize::assertions(), Optimize::check(), Optimize::from_file(), Optimize::from_string(), Optimize::help(), Optimize::maximize(), Optimize::minimize(), Optimize::model(), Optimize::objectives(), Optimize::param_descrs(), Optimize::pop(), Optimize::push(), Optimize::reason_unknown(), Optimize::set(), Optimize::set_initial_value(), Optimize::set_on_model(), Optimize::sexpr(), Optimize::statistics(), and Optimize::unsat_core().
Definition at line 3301 of file z3++.h.
Referenced by Optimize::__deepcopy__(), Optimize::__del__(), Optimize::add_soft(), Optimize::assert_and_track(), Optimize::assert_exprs(), Optimize::assertions(), Optimize::check(), Optimize::from_file(), Optimize::from_string(), Optimize::help(), Optimize::maximize(), Optimize::minimize(), Optimize::model(), Optimize::objectives(), Optimize::param_descrs(), Optimize::pop(), Optimize::push(), Optimize::reason_unknown(), Optimize::set(), Optimize::set_initial_value(), Optimize::set_on_model(), Optimize::sexpr(), Optimize::statistics(), and Optimize::unsat_core().
|
inlineoverride |
|
inline |
Definition at line 3317 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), Optimize::__iadd__(), optimize::add(), and optimize::optimize().
|
inline |
Definition at line 3328 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().
Definition at line 3324 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().
Definition at line 3341 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().
|
inline |
Definition at line 3321 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().
|
inline |
Definition at line 3392 of file z3++.h.
Referenced by optimize::optimize(), and Solver::to_smt2().
|
inline |
Definition at line 3367 of file z3++.h.
|
inline |
Definition at line 3368 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 3382 of file z3++.h.
Referenced by OptimizeObjective::value().
Definition at line 3358 of file z3++.h.
Referenced by optimize::optimize().
|
inline |
Definition at line 3393 of file z3++.h.
Referenced by optimize::optimize().
|
inline |
|
inline |
|
inline |
Definition at line 3361 of file z3++.h.
Referenced by Solver::__enter__().
|
inline |
|
inline |
Definition at line 3351 of file z3++.h.
Definition at line 3344 of file z3++.h.
Referenced by optimize::set_initial_value().
|
inline |
|
inline |
Definition at line 3394 of file z3++.h.
|
inline |
Definition at line 3380 of file z3++.h.
Definition at line 3387 of file z3++.h.
Referenced by OptimizeObjective::value().