RetroSearch Browse

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

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

Z3: Optimize Class Reference

def __init__ (self, optimize=None, ctx=None) def __deepcopy__ (self, memo={}) def __del__ (self) def set (self, *args, **keys) def help (self) def param_descrs (self) def assert_exprs (self, *args) def add (self, *args) def __iadd__ (self, fml) def assert_and_track (self, a, p) def add_soft (self, arg, weight="1", id=None) def set_initial_value (self, var, value) def maximize (self, arg) def minimize (self, arg) def push (self) def pop (self) def check (self, *assumptions) def reason_unknown (self) def model (self) def unsat_core (self) def lower (self, obj) def upper (self, obj) def lower_values (self, obj) def upper_values (self, obj) def from_file (self, filename) def from_string (self, s) def assertions (self) def objectives (self) def __repr__ (self) def sexpr (self) def statistics (self) def set_on_model (self, on_model) def use_pp (self)

Optimize API provides methods for solving using objective functions and weighted soft constraints

Definition at line 7933 of file z3py.py.

◆ __init__() def __init__ ( self, optimize = None, ctx = None )

Definition at line 7936 of file z3py.py.

7936 def

__init__(self, optimize=None, ctx=None):

7937

self.ctx = _get_ctx(ctx)

7938 if

optimize

is None

7941

self.optimize = optimize

7942

self._on_models_id =

None

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.

◆ __del__()

Definition at line 7948 of file z3py.py.

7949 if

self.optimize

is not None and

self.ctx.ref()

is not None and

Z3_optimize_dec_ref

is not None

7951 if

self._on_models_id

is not None

7952

del _on_models[self._on_models_id]

void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)

Decrement the reference counter of the given optimize context.

◆ __deepcopy__() def __deepcopy__ ( self, memo = {} )

Definition at line 7945 of file z3py.py.

7945 def

__deepcopy__(self, memo={}):

7946 return

Optimize(self.optimize, self.ctx)

◆ __iadd__() def __iadd__ ( self, fml )

Definition at line 7985 of file z3py.py.

7985 def

__iadd__(self, fml):

◆ __repr__()

Return a formatted string with all added rules and constraints.

Definition at line 8132 of file z3py.py.

8133 """Return a formatted string with all added rules and constraints.""" ◆ add()

Assert constraints as background axioms for the optimize solver. Alias for assert_expr.

Definition at line 7981 of file z3py.py.

7981 def

add(self, *args):

7982 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr.""" 7983

self.assert_exprs(*args)

Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().

◆ add_soft() def add_soft ( self, arg, weight = "1", id = None )

Add soft constraint with optional weight and optional identifier.
   If no weight is supplied, then the penalty for violating the soft constraint
   is 1.
   Soft constraints are grouped by identifiers. Soft constraints that are
   added without identifiers are grouped by default.

Definition at line 8018 of file z3py.py.

8018 def

add_soft(self, arg, weight="1", id=None):

8019 """Add soft constraint with optional weight and optional identifier. 8020 If no weight is supplied, then the penalty for violating the soft constraint 8022 Soft constraints are grouped by identifiers. Soft constraints that are 8023 added without identifiers are grouped by default. 8026

weight =

"%d"

% weight

8027 elif

isinstance(weight, float):

8028

weight =

"%f"

% weight

8029 if not

isinstance(weight, str):

8030 raise

Z3Exception(

"weight should be a string or an integer"

)

8037 return

OptimizeObjective(self, v,

False

)

8038 if

sys.version_info.major >= 3

and

isinstance(arg, Iterable):

8039 return

[asoft(a)

for

in

arg]

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.

def to_symbol(s, ctx=None)

◆ assert_and_track() def assert_and_track ( self, a, p )

Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.

If `p` is a string, it will be automatically converted into a Boolean constant.

>>> x = Int('x')
>>> p3 = Bool('p3')
>>> s = Optimize()
>>> s.assert_and_track(x > 0,  'p1')
>>> s.assert_and_track(x != 1, 'p2')
>>> s.assert_and_track(x < 0,  p3)
>>> print(s.check())
unsat
>>> c = s.unsat_core()
>>> len(c)
2
>>> Bool('p1') in c
True
>>> Bool('p2') in c
False
>>> p3 in c
True

Definition at line 7989 of file z3py.py.

7989 def

assert_and_track(self, a, p):

7990 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`. 7992 If `p` is a string, it will be automatically converted into a Boolean constant. 7997 >>> s.assert_and_track(x > 0, 'p1') 7998 >>> s.assert_and_track(x != 1, 'p2') 7999 >>> s.assert_and_track(x < 0, p3) 8000 >>> print(s.check()) 8002 >>> c = s.unsat_core() 8012 if

isinstance(p, str):

8013

p =

Bool

(p, self.ctx)

8014

_z3_assert(isinstance(a, BoolRef),

"Boolean expression expected"

)

8015

_z3_assert(isinstance(p, BoolRef)

and is_const

(p),

"Boolean expression expected"

)

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.

◆ assert_exprs() def assert_exprs ( self, * args )

Assert constraints as background axioms for the optimize solver.

Definition at line 7969 of file z3py.py.

7969 def

assert_exprs(self, *args):

7970 """Assert constraints as background axioms for the optimize solver.""" 7971

args = _get_args(args)

7974 if

isinstance(arg, Goal)

or

isinstance(arg, AstVector):

void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)

Assert hard constraint to the optimization context.

Referenced by Goal.add(), Solver.add(), Fixedpoint.add(), Optimize.add(), Goal.append(), Solver.append(), Fixedpoint.append(), Goal.insert(), Solver.insert(), and Fixedpoint.insert().

◆ assertions()

Return an AST vector containing all added constraints.

Definition at line 8124 of file z3py.py.

8124 def

assertions(self):

8125 """Return an AST vector containing all added constraints."""

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.

Referenced by Solver.to_smt2().

◆ check() def check ( self, * assumptions )

Check consistency and produce optimal values.

Definition at line 8073 of file z3py.py.

8073 def

check(self, *assumptions):

8074 """Check consistency and produce optimal values.""" 8075

assumptions = _get_args(assumptions)

8076

num = len(assumptions)

8077

_assumptions = (Ast * num)()

8078 for

in range

(num):

8079

_assumptions[i] = assumptions[i].as_ast()

8080 return

CheckSatResult(

Z3_optimize_check

(self.ctx.ref(), self.optimize, num, _assumptions))

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.

expr range(expr const &lo, expr const &hi)

◆ from_file() def from_file ( self, filename )

Parse assertions and objectives from a file

Definition at line 8116 of file z3py.py.

8116 def

from_file(self, filename):

8117 """Parse assertions and objectives from a file"""

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() def from_string ( self, s )

Parse assertions and objectives from a string

Definition at line 8120 of file z3py.py.

8120 def

from_string(self, s):

8121 """Parse assertions and objectives from a string"""

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

◆ help()

Display a string describing all available options.

Definition at line 7961 of file z3py.py.

7962 """Display a string describing all available options."""

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 8096 of file z3py.py.

8096 def

lower(self, obj):

8097 if not

isinstance(obj, OptimizeObjective):

8098 raise

Z3Exception(

"Expecting objective handle returned by maximize/minimize"

)

Referenced by OptimizeObjective.value().

◆ lower_values() def lower_values ( self, obj )

Definition at line 8106 of file z3py.py.

8106 def

lower_values(self, obj):

8107 if not

isinstance(obj, OptimizeObjective):

8108 raise

Z3Exception(

"Expecting objective handle returned by maximize/minimize"

)

8109 return

obj.lower_values()

◆ maximize() def maximize ( self, arg )

Add objective function to maximize.

Definition at line 8049 of file z3py.py.

8049 def

maximize(self, arg):

8050 """Add objective function to maximize.""" 8051 return

OptimizeObjective(

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

Add a maximization constraint.

◆ minimize() def minimize ( self, arg )

Add objective function to minimize.

Definition at line 8057 of file z3py.py.

8057 def

minimize(self, arg):

8058 """Add objective function to minimize.""" 8059 return

OptimizeObjective(

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

Add a minimization constraint.

◆ model()

Return a model for the last check().

Definition at line 8086 of file z3py.py.

8087 """Return a model for the last check().""" 8091 raise

Z3Exception(

"model is not available"

)

Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)

Retrieve the model for the last Z3_optimize_check.

Referenced by ModelRef.__del__(), ModelRef.__getitem__(), ModelRef.__len__(), ModelRef.decls(), ModelRef.eval(), ModelRef.get_interp(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), ModelRef.sexpr(), FuncInterp.translate(), ModelRef.translate(), and ModelRef.update_value().

◆ objectives()

returns set of objective functions

Definition at line 8128 of file z3py.py.

8128 def

objectives(self):

8129 """returns set of objective functions"""

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

◆ param_descrs() def param_descrs ( self )

Return the parameter description set.

Definition at line 7965 of file z3py.py.

7965 def

param_descrs(self):

7966 """Return the parameter description set."""

Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o)

Return the parameter description set for the given optimize object.

◆ pop()

restore to previously created backtracking point

Definition at line 8069 of file z3py.py.

8070 """restore to previously created backtracking point"""

void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)

Backtrack one level.

Referenced by Solver.__exit__().

◆ push()

create a backtracking point for added rules, facts and assertions

Definition at line 8065 of file z3py.py.

8066 """create a backtracking point for added rules, facts and assertions"""

void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)

Create a backtracking point.

Referenced by Solver.__enter__().

◆ reason_unknown() def reason_unknown ( self )

Return a string that describes why the last `check()` returned `unknown`.

Definition at line 8082 of file z3py.py.

8082 def

reason_unknown(self):

8083 """Return a string that describes why the last `check()` returned `unknown`."""

Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d)

Retrieve a string that describes the last status returned by Z3_optimize_check.

◆ set() def set ( self, * args, ** keys )

Set a configuration option.
The method `help()` return a string containing all available options.

Definition at line 7954 of file z3py.py.

7954 def

set(self, *args, **keys):

7955 """Set a configuration option. 7956 The method `help()` return a string containing all available options.

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

Set parameters on optimization context.

def args2params(arguments, keywords, ctx=None)

◆ set_initial_value() def set_initial_value ( self, var, value )

initialize the solver's state by setting the initial value of var to value

Definition at line 8042 of file z3py.py.

8042 def

set_initial_value(self, var, value):

8043 """initialize the solver's state by setting the initial value of var to value 8046

value = s.cast(value)

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

◆ set_on_model() def set_on_model ( self, on_model )

Register a callback that is invoked with every incremental improvement to
objective values. The callback takes a model as argument.
The life-time of the model is limited to the callback so the
model has to be (deep) copied if it is to be used after the callback

Definition at line 8147 of file z3py.py.

8147 def

set_on_model(self, on_model):

8148 """Register a callback that is invoked with every incremental improvement to 8149 objective values. The callback takes a model as argument. 8150 The life-time of the model is limited to the callback so the 8151 model has to be (deep) copied if it is to be used after the callback 8153

id = len(_on_models) + 41

8154

mdl =

Model

(self.ctx)

8155

_on_models[id] = (on_model, mdl)

8156

self._on_models_id = id

8158

self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,

void Z3_API Z3_optimize_register_model_eh(Z3_context c, Z3_optimize o, Z3_model m, void *ctx, Z3_model_eh model_eh)

◆ sexpr()

Return a formatted string (in Lisp-like format) with all added constraints.
We say the string is in s-expression format.

Definition at line 8136 of file z3py.py.

8137 """Return a formatted string (in Lisp-like format) with all added constraints. 8138 We say the string is in s-expression format.

Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)

Print the current context as a string.

Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().

◆ statistics()

Return statistics for the last check`.

Definition at line 8142 of file z3py.py.

8142 def

statistics(self):

8143 """Return statistics for the last check`.

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 8093 of file z3py.py.

8093 def

unsat_core(self):

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 8101 of file z3py.py.

8101 def

upper(self, obj):

8102 if not

isinstance(obj, OptimizeObjective):

8103 raise

Z3Exception(

"Expecting objective handle returned by maximize/minimize"

)

Referenced by OptimizeObjective.value().

◆ upper_values() def upper_values ( self, obj )

Definition at line 8111 of file z3py.py.

8111 def

upper_values(self, obj):

8112 if not

isinstance(obj, OptimizeObjective):

8113 raise

Z3Exception(

"Expecting objective handle returned by maximize/minimize"

)

8114 return

obj.upper_values()

◆ ctx

Definition at line 7937 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), FPRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), Probe.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Simplifier.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Context.__del__(), AstRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), ParamsRef.__del__(), ParamDescrsRef.__del__(), Goal.__del__(), AstVector.__del__(), AstMap.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Statistics.__del__(), Solver.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Simplifier.__del__(), Tactic.__del__(), Probe.__del__(), ParserContext.__del__(), ArithRef.__div__(), BitVecRef.__div__(), FPRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), FPRef.__ge__(), SeqRef.__ge__(), AstVector.__getitem__(), SeqRef.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ApplyResult.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), FPRef.__gt__(), SeqRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), FPRef.__le__(), SeqRef.__le__(), CharRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ApplyResult.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), FPRef.__lt__(), SeqRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BoolRef.__mul__(), ArithRef.__mul__(), BitVecRef.__mul__(), FPRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), FPRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), FPRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), FPRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), FPRef.__rsub__(), BitVecRef.__rxor__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), FPRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), Simplifier.add(), Fixedpoint.add_cover(), ParserContext.add_decl(), Fixedpoint.add_rule(), Optimize.add_soft(), ParserContext.add_sort(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), ApplyResult.as_expr(), FPNumRef.as_string(), Solver.assert_and_track(), Optimize.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), SeqRef.at(), SeqSortRef.basis(), ReSortRef.basis(), QuantifierRef.body(), BoolSortRef.cast(), Solver.check(), Optimize.check(), UserPropagateBase.conflict(), Solver.consequences(), DatatypeSortRef.constructor(), Goal.convert_model(), AstRef.ctx_ref(), UserPropagateBase.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), Solver.dimacs(), ArraySortRef.domain(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), FPNumRef.exponent(), FPNumRef.exponent_as_bv(), FPNumRef.exponent_as_long(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), Optimize.from_string(), ParserContext.from_string(), Goal.get(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), ParamDescrsRef.get_documentation(), Fixedpoint.get_ground_sat_answer(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), ModelRef.get_sort(), ModelRef.get_universe(), Solver.help(), Fixedpoint.help(), Optimize.help(), Simplifier.help(), Tactic.help(), Solver.import_model_converter(), Goal.inconsistent(), Solver.interrupt(), CharRef.is_digit(), FPNumRef.isInf(), FPNumRef.isNaN(), FPNumRef.isNegative(), FPNumRef.isNormal(), FPNumRef.isPositive(), FPNumRef.isSubnormal(), FPNumRef.isZero(), AstMap.keys(), Statistics.keys(), SortRef.kind(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), Solver.next(), QuantifierRef.no_pattern(), Solver.non_units(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), RatNumRef.numerator(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Simplifier.param_descrs(), Tactic.param_descrs(), FuncDeclRef.params(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Optimize.pop(), Solver.pop(), Goal.prec(), Solver.proof(), Solver.push(), Optimize.push(), AstVector.push(), QuantifierRef.qid(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), FuncDeclRef.range(), ArraySortRef.range(), Solver.reason_unknown(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), DatatypeSortRef.recognizer(), Context.ref(), Fixedpoint.register_relation(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.root(), Solver.set(), Fixedpoint.set(), Optimize.set(), ParamsRef.set(), Solver.set_initial_value(), Optimize.set_initial_value(), Optimize.set_on_model(), Fixedpoint.set_predicate_representation(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), Solver.sexpr(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), FPNumRef.sign(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), FPNumRef.significand_as_long(), ParamDescrsRef.size(), Goal.size(), QuantifierRef.skolem_id(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), FiniteDomainRef.sort(), FPRef.sort(), SeqRef.sort(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), CharRef.to_bv(), CharRef.to_int(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), AstVector.translate(), FuncInterp.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), Fixedpoint.update_rule(), Simplifier.using_params(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ optimize

Definition at line 7939 of file z3py.py.

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

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