Definition at line 2827 of file z3++.h.
◆ optimize() [1/3]
◆ optimize() [2/3]
◆ optimize() [3/3]
Definition at line 2842 of file z3++.h.
2847 for (expr_vector::iterator it = v.begin(); it != v.end(); ++it)
minimize(*it);
◆ ~optimize()
◆ add() [1/5]
void add |
( |
expr const & |
e | ) |
|
|
inline |
◆ add() [2/5]
void add |
( |
expr const & |
e, |
|
|
char const * |
p |
|
) |
| |
|
inline |
Definition at line 2869 of file z3++.h.
2870 assert(e.is_bool());
2871 add(e,
ctx().bool_const(p));
◆ add() [3/5]
void add |
( |
expr const & |
e, |
|
|
expr const & |
t |
|
) |
| |
|
inline |
Definition at line 2865 of file z3++.h.
2866 assert(e.is_bool());
◆ add() [4/5]
◆ add() [5/5]
Definition at line 2862 of file z3++.h.
2863 for (expr_vector::iterator it = es.begin(); it != es.end(); ++it)
add(*it);
◆ add_soft() [1/2]
handle add_soft |
( |
expr const & |
e, |
|
|
char const * |
weight |
|
) |
| |
|
inline |
Definition at line 2878 of file z3++.h.
2879 assert(e.is_bool());
◆ add_soft() [2/2]
handle add_soft |
( |
expr const & |
e, |
|
|
unsigned |
weight |
|
) |
| |
|
inline |
Definition at line 2873 of file z3++.h.
2874 assert(e.is_bool());
2875 auto str = std::to_string(weight);
Referenced by optimize::add().
◆ assertions()
◆ check() [1/2]
◆ check() [2/2]
Definition at line 2898 of file z3++.h.
2899 unsigned n = asms.size();
2900 array<Z3_ast> _asms(n);
2901 for (
unsigned i = 0; i < n; i++) {
◆ from_file()
void from_file |
( |
char const * |
filename | ) |
|
|
inline |
◆ from_string()
void from_string |
( |
char const * |
constraints | ) |
|
|
inline |
◆ get_model()
model get_model |
( |
| ) |
const |
|
inline |
◆ help()
std::string help |
( |
| ) |
const |
|
inline |
◆ lower()
Definition at line 2912 of file z3++.h.
2915 return expr(
ctx(), r);
◆ maximize()
◆ minimize()
◆ objectives()
◆ operator Z3_optimize()
operator Z3_optimize |
( |
| ) |
const |
|
inline |
◆ operator=()
◆ pop()
◆ push()
◆ set()
◆ statistics()
stats statistics |
( |
| ) |
const |
|
inline |
◆ unsat_core()
◆ upper()
Definition at line 2917 of file z3++.h.
2920 return expr(
ctx(), r);
◆ operator<<
std::ostream& operator<< |
( |
std::ostream & |
out, |
|
|
optimize const & |
s |
|
) |
| |
|
friend |
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t)
Assert tracked hard constraint to the optimization context.
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives....
Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o)
Return objectives on the optimization context. If the objective function is a max-sat objective it is...
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d)
Retrieve statistics information from the last call to Z3_optimize_check.
Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o)
Return the set of asserted formulas on the optimization context.
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
Assert soft constraint to the optimization context.
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective.
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])
Check consistency and produce optimal values.
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives....
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
ast_vector_tpl< expr > expr_vector
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
friend void check_context(object const &a, object const &b)
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
check_result to_check_result(Z3_lbool l)
handle minimize(expr const &e)
Z3_error_code check_error() const
Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o)
Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions ...
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
handle add_soft(expr const &e, unsigned weight)
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)
Return a string containing a description of parameters accepted by optimize.
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.