RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/classz3_1_1optimize.html below:

Z3: optimize Class Reference

Definition at line 3287 of file z3++.h.

◆ optimize() [1/3]

Definition at line 3297 of file z3++.h.

void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)

Increment the reference counter of the given optimize context.

Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)

Create a new optimize context.

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().

◆ optimize() [2/3]

Definition at line 3298 of file z3++.h.

3298

object

(o), m_opt(o.m_opt) {

◆ optimize() [3/3]

Definition at line 3301 of file z3++.h.

3306 for

(expr_vector::iterator it = v.begin(); it != v.end(); ++it)

minimize

(*it);

handle minimize(expr const &e)

ast_vector_tpl< expr > expr_vector

◆ ~optimize()

Definition at line 3315 of file z3++.h.

void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)

Decrement the reference counter of the given optimize context.

◆ add() [1/5] void add ( expr const & e ) inline ◆ add() [2/5] void add ( expr const & e, char const * p ) inline ◆ add() [3/5] void add ( expr const & e, expr const & t ) inline ◆ add() [4/5] ◆ add() [5/5] ◆ add_soft() [1/2] handle add_soft ( expr const & e, char const * weight ) inline

Definition at line 3337 of file z3++.h.

3338

assert(e.is_bool());

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.

◆ add_soft() [2/2] handle add_soft ( expr const & e, unsigned weight ) inline

Definition at line 3332 of file z3++.h.

3333

assert(e.is_bool());

3334 auto

str = std::to_string(weight);

Referenced by optimize::add().

◆ assertions()

Definition at line 3392 of file z3++.h.

Z3_error_code check_error() const

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.

System.IntPtr Z3_ast_vector

Referenced by optimize::optimize(), and Solver::to_smt2().

◆ check() [1/2]

Definition at line 3367 of file z3++.h.

Z3_lbool

Lifted Boolean type: false, undefined, true.

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.

check_result to_check_result(Z3_lbool l)

◆ check() [2/2]

Definition at line 3368 of file z3++.h.

3369 unsigned

n = asms.size();

3370

array<Z3_ast> _asms(n);

3371 for

(

unsigned

i = 0; i < n; i++) {

friend void check_context(object const &a, object const &b)

◆ from_file() void from_file ( char const * filename ) inline

Definition at line 3396 of file z3++.h.

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....

◆ from_string() void from_string ( char const * constraints ) inline

Definition at line 3397 of file z3++.h.

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....

◆ get_model() model get_model ( ) const inline

Definition at line 3379 of file z3++.h.

Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)

Retrieve the model for the last Z3_optimize_check.

◆ help() std::string help ( ) const inline

Definition at line 3398 of file z3++.h.

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.

◆ lower()

Definition at line 3382 of file z3++.h.

3385 return

expr(

ctx

(), r);

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.

Referenced by OptimizeObjective::value().

◆ maximize()

Definition at line 3355 of file z3++.h.

unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)

Add a maximization constraint.

◆ minimize()

Definition at line 3358 of file z3++.h.

unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)

Add a minimization constraint.

Referenced by optimize::optimize().

◆ objectives()

Definition at line 3393 of file z3++.h.

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...

Referenced by optimize::optimize().

◆ operator Z3_optimize() operator Z3_optimize ( ) const inline ◆ operator=()

Definition at line 3308 of file z3++.h.

3312

object::operator=(o);

◆ pop()

Definition at line 3364 of file z3++.h.

void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)

Backtrack one level.

Referenced by Solver::__exit__().

◆ push()

Definition at line 3361 of file z3++.h.

void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)

Create a backtracking point.

Referenced by Solver::__enter__().

◆ set()

Definition at line 3381 of file z3++.h.

void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)

Set parameters on optimization context.

◆ set_initial_value() [1/3] void set_initial_value ( expr const & var, bool b ) inline

Definition at line 3351 of file z3++.h.

void set_initial_value(expr const &var, expr const &value)

◆ set_initial_value() [2/3] void set_initial_value ( expr const & var, expr const & value ) inline

Definition at line 3344 of file z3++.h.

void Z3_API Z3_optimize_set_initial_value(Z3_context c, Z3_optimize o, Z3_ast v, Z3_ast val)

provide an initialization hint to the solver. The initialization hint is used to calibrate an initial...

Referenced by optimize::set_initial_value().

◆ set_initial_value() [3/3] void set_initial_value ( expr const & var, int i ) inline ◆ statistics() stats statistics ( ) const inline

Definition at line 3394 of file z3++.h.

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.

◆ unsat_core()

Definition at line 3380 of file z3++.h.

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 ...

◆ upper()

Definition at line 3387 of file z3++.h.

3390 return

expr(

ctx

(), r);

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.

Referenced by OptimizeObjective::value().

◆ operator<< std::ostream& operator<< ( std::ostream & out, optimize const & s ) friend

Definition at line 3400 of file z3++.h.

Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)

Print the current context as a string.

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4