Z3
 
Loading...
Searching...
No Matches
Optimize Class Reference
+ Inheritance diagram for Optimize:

Public Member Functions

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

Data Fields

 ctx = _get_ctx(ctx)
 
 optimize = Z3_mk_optimize(self.ctx.ref())
 

Protected Attributes

 _on_models_id = None
 

Additional Inherited Members

- Protected Member Functions inherited from Z3PPObject
 _repr_html_ (self)
 

Detailed Description

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

Definition at line 7933 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

__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:
7939 self.optimize = Z3_mk_optimize(self.ctx.ref())
7940 else:
7941 self.optimize = optimize
7942 self._on_models_id = None
7943 Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7944
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__()

__del__ ( self)

Definition at line 7948 of file z3py.py.

7948 def __del__(self):
7949 if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
7950 Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7951 if self._on_models_id is not None:
7952 del _on_models[self._on_models_id]
7953
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.

Member Function Documentation

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 7945 of file z3py.py.

7945 def __deepcopy__(self, memo={}):
7946 return Optimize(self.optimize, self.ctx)
7947

◆ __iadd__()

__iadd__ ( self,
fml )

Definition at line 7985 of file z3py.py.

7985 def __iadd__(self, fml):
7986 self.add(fml)
7987 return self
7988

◆ __repr__()

__repr__ ( self)
Return a formatted string with all added rules and constraints.

Definition at line 8132 of file z3py.py.

8132 def __repr__(self):
8133 """Return a formatted string with all added rules and constraints."""
8134 return self.sexpr()
8135

◆ add()

add ( self,
* args )
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)
7984

Referenced by Solver.__iadd__().

◆ add_soft()

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
8021 is 1.
8022 Soft constraints are grouped by identifiers. Soft constraints that are
8023 added without identifiers are grouped by default.
8024 """
8025 if _is_int(weight):
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")
8031 if id is None:
8032 id = ""
8033 id = to_symbol(id, self.ctx)
8034
8035 def asoft(a):
8036 v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
8037 return OptimizeObjective(self, v, False)
8038 if sys.version_info.major >= 3 and isinstance(arg, Iterable):
8039 return [asoft(a) for a in arg]
8040 return asoft(arg)
8041
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.

◆ assert_and_track()

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`.
7991
7992 If `p` is a string, it will be automatically converted into a Boolean constant.
7993
7994 >>> x = Int('x')
7995 >>> p3 = Bool('p3')
7996 >>> s = Optimize()
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())
8001 unsat
8002 >>> c = s.unsat_core()
8003 >>> len(c)
8004 2
8005 >>> Bool('p1') in c
8006 True
8007 >>> Bool('p2') in c
8008 False
8009 >>> p3 in c
8010 True
8011 """
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")
8016 Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
8017
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()

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)
7972 s = BoolSort(self.ctx)
7973 for arg in args:
7974 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7975 for f in arg:
7976 Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7977 else:
7978 arg = s.cast(arg)
7979 Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7980
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(), Goal.append(), Solver.append(), Goal.insert(), and Solver.insert().

◆ assertions()

assertions ( self)
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."""
8126 return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
8127
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.

◆ check()

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 i in range(num):
8079 _assumptions[i] = assumptions[i].as_ast()
8080 return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
8081
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.

◆ from_file()

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"""
8118 Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
8119
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()

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"""
8122 Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
8123
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()

help ( self)
Display a string describing all available options.

Definition at line 7961 of file z3py.py.

7961 def help(self):
7962 """Display a string describing all available options."""
7963 print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7964
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()

lower ( self,
obj )

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")
8099 return obj.lower()
8100

◆ lower_values()

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

◆ maximize()

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(
8052 self,
8053 Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
8054 is_max=True,
8055 )
8056
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.

◆ minimize()

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(
8060 self,
8061 Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
8062 is_max=False,
8063 )
8064
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.

◆ model()

model ( self)
Return a model for the last check().

Definition at line 8086 of file z3py.py.

8086 def model(self):
8087 """Return a model for the last check()."""
8088 try:
8089 return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
8090 except Z3Exception:
8091 raise Z3Exception("model is not available")
8092
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(), ModelRef.translate(), and ModelRef.update_value().

◆ objectives()

objectives ( self)
returns set of objective functions

Definition at line 8128 of file z3py.py.

8128 def objectives(self):
8129 """returns set of objective functions"""
8130 return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
8131
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()

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."""
7967 return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7968
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()

pop ( self)
restore to previously created backtracking point

Definition at line 8069 of file z3py.py.

8069 def pop(self):
8070 """restore to previously created backtracking point"""
8071 Z3_optimize_pop(self.ctx.ref(), self.optimize)
8072
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.

Referenced by Solver.__exit__().

◆ push()

push ( self)
create a backtracking point for added rules, facts and assertions

Definition at line 8065 of file z3py.py.

8065 def push(self):
8066 """create a backtracking point for added rules, facts and assertions"""
8067 Z3_optimize_push(self.ctx.ref(), self.optimize)
8068
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.

Referenced by Solver.__enter__().

◆ reason_unknown()

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`."""
8084 return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
8085
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()

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.
7957 """
7958 p = args2params(args, keys, self.ctx)
7959 Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7960
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.

◆ set_initial_value()

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
8044 """
8045 s = var.sort()
8046 value = s.cast(value)
8047 Z3_optimize_set_initial_value(self.ctx.ref(), self.optimize, var.ast, value.ast)
8048
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()

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
8152 """
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,
8159 )
8160
8161
void Z3_API Z3_optimize_register_model_eh(Z3_context c, Z3_optimize o, Z3_model m, void *ctx, Z3_model_eh model_eh)
register a model event handler for new models.

◆ sexpr()

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

8136 def sexpr(self):
8137 """Return a formatted string (in Lisp-like format) with all added constraints.
8138 We say the string is in s-expression format.
8139 """
8140 return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
8141
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.

◆ statistics()

statistics ( self)
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`.
8144 """
8145 return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
8146
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()

unsat_core ( self)

Definition at line 8093 of file z3py.py.

8093 def unsat_core(self):
8094 return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
8095
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()

upper ( self,
obj )

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")
8104 return obj.upper()
8105

◆ upper_values()

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

Field Documentation

◆ _on_models_id

_on_models_id = None
protected

Definition at line 7942 of file z3py.py.

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 7937 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), Goal.__copy__(), ModelRef.__copy__(), AstMap.__deepcopy__(), AstRef.__deepcopy__(), AstVector.__deepcopy__(), Datatype.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), Goal.__deepcopy__(), ModelRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), ParamsRef.__deepcopy__(), Statistics.__deepcopy__(), AstMap.__del__(), AstRef.__del__(), AstVector.__del__(), Context.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), Goal.__del__(), ModelRef.__del__(), ParamDescrsRef.__del__(), ParamsRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), Solver.__del__(), Statistics.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstMap.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstMap.__len__(), AstVector.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), BoolRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), AstMap.__repr__(), ParamDescrsRef.__repr__(), ParamsRef.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstMap.__setitem__(), AstVector.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), AstVector.push(), Solver.push(), QuantifierRef.qid(), ArraySortRef.range(), FuncDeclRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), ParamsRef.set(), Solver.set(), AstVector.sexpr(), Goal.sexpr(), ModelRef.sexpr(), Goal.size(), ParamDescrsRef.size(), QuantifierRef.skolem_id(), AstRef.translate(), AstVector.translate(), Goal.translate(), ModelRef.translate(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ optimize

optimize = Z3_mk_optimize(self.ctx.ref())

Definition at line 7939 of file z3py.py.