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)
 __enter__ (self)
 __exit__ (self, *exc_info)
 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 8028 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 8031 of file z3py.py.

8031 def __init__(self, optimize=None, ctx=None):
8032 self.ctx = _get_ctx(ctx)
8033 if optimize is None:
8034 self.optimize = Z3_mk_optimize(self.ctx.ref())
8035 else:
8036 self.optimize = optimize
8037 self._on_models_id = None
8038 Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
8039
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 8043 of file z3py.py.

8043 def __del__(self):
8044 if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
8045 Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
8046 if self._on_models_id is not None:
8047 del _on_models[self._on_models_id]
8048
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 8040 of file z3py.py.

8040 def __deepcopy__(self, memo={}):
8041 return Optimize(self.optimize, self.ctx)
8042

◆ __enter__()

__enter__ ( self)

Definition at line 8049 of file z3py.py.

8049 def __enter__(self):
8050 self.push()
8051 return self
8052

◆ __exit__()

__exit__ ( self,
* exc_info )

Definition at line 8053 of file z3py.py.

8053 def __exit__(self, *exc_info):
8054 self.pop()
8055

◆ __iadd__()

__iadd__ ( self,
fml )

Definition at line 8087 of file z3py.py.

8087 def __iadd__(self, fml):
8088 self.add(fml)
8089 return self
8090

◆ __repr__()

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

Definition at line 8234 of file z3py.py.

8234 def __repr__(self):
8235 """Return a formatted string with all added rules and constraints."""
8236 return self.sexpr()
8237

◆ add()

add ( self,
* args )
Assert constraints as background axioms for the optimize solver. Alias for assert_expr.

Definition at line 8083 of file z3py.py.

8083 def add(self, *args):
8084 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
8085 self.assert_exprs(*args)
8086

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

8120 def add_soft(self, arg, weight="1", id=None):
8121 """Add soft constraint with optional weight and optional identifier.
8122 If no weight is supplied, then the penalty for violating the soft constraint
8123 is 1.
8124 Soft constraints are grouped by identifiers. Soft constraints that are
8125 added without identifiers are grouped by default.
8126 """
8127 if _is_int(weight):
8128 weight = "%d" % weight
8129 elif isinstance(weight, float):
8130 weight = "%f" % weight
8131 if not isinstance(weight, str):
8132 raise Z3Exception("weight should be a string or an integer")
8133 if id is None:
8134 id = ""
8135 id = to_symbol(id, self.ctx)
8136
8137 def asoft(a):
8138 v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
8139 return OptimizeObjective(self, v, False)
8140 if sys.version_info.major >= 3 and isinstance(arg, Iterable):
8141 return [asoft(a) for a in arg]
8142 return asoft(arg)
8143
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 8091 of file z3py.py.

8091 def assert_and_track(self, a, p):
8092 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
8093
8094 If `p` is a string, it will be automatically converted into a Boolean constant.
8095
8096 >>> x = Int('x')
8097 >>> p3 = Bool('p3')
8098 >>> s = Optimize()
8099 >>> s.assert_and_track(x > 0, 'p1')
8100 >>> s.assert_and_track(x != 1, 'p2')
8101 >>> s.assert_and_track(x < 0, p3)
8102 >>> print(s.check())
8103 unsat
8104 >>> c = s.unsat_core()
8105 >>> len(c)
8106 2
8107 >>> Bool('p1') in c
8108 True
8109 >>> Bool('p2') in c
8110 False
8111 >>> p3 in c
8112 True
8113 """
8114 if isinstance(p, str):
8115 p = Bool(p, self.ctx)
8116 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
8117 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
8118 Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
8119
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 8071 of file z3py.py.

8071 def assert_exprs(self, *args):
8072 """Assert constraints as background axioms for the optimize solver."""
8073 args = _get_args(args)
8074 s = BoolSort(self.ctx)
8075 for arg in args:
8076 if isinstance(arg, Goal) or isinstance(arg, AstVector):
8077 for f in arg:
8078 Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
8079 else:
8080 arg = s.cast(arg)
8081 Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
8082
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.

◆ assertions()

assertions ( self)
Return an AST vector containing all added constraints.

Definition at line 8226 of file z3py.py.

8226 def assertions(self):
8227 """Return an AST vector containing all added constraints."""
8228 return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
8229
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 8175 of file z3py.py.

8175 def check(self, *assumptions):
8176 """Check consistency and produce optimal values."""
8177 assumptions = _get_args(assumptions)
8178 num = len(assumptions)
8179 _assumptions = (Ast * num)()
8180 for i in range(num):
8181 _assumptions[i] = assumptions[i].as_ast()
8182 return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
8183
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 8218 of file z3py.py.

8218 def from_file(self, filename):
8219 """Parse assertions and objectives from a file"""
8220 Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
8221
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 8222 of file z3py.py.

8222 def from_string(self, s):
8223 """Parse assertions and objectives from a string"""
8224 Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
8225
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 8063 of file z3py.py.

8063 def help(self):
8064 """Display a string describing all available options."""
8065 print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
8066
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 8198 of file z3py.py.

8198 def lower(self, obj):
8199 if not isinstance(obj, OptimizeObjective):
8200 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8201 return obj.lower()
8202

◆ lower_values()

lower_values ( self,
obj )

Definition at line 8208 of file z3py.py.

8208 def lower_values(self, obj):
8209 if not isinstance(obj, OptimizeObjective):
8210 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8211 return obj.lower_values()
8212

◆ maximize()

maximize ( self,
arg )
Add objective function to maximize.

Definition at line 8151 of file z3py.py.

8151 def maximize(self, arg):
8152 """Add objective function to maximize."""
8153 return OptimizeObjective(
8154 self,
8155 Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
8156 is_max=True,
8157 )
8158
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 8159 of file z3py.py.

8159 def minimize(self, arg):
8160 """Add objective function to minimize."""
8161 return OptimizeObjective(
8162 self,
8163 Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
8164 is_max=False,
8165 )
8166
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 8188 of file z3py.py.

8188 def model(self):
8189 """Return a model for the last check()."""
8190 try:
8191 return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
8192 except Z3Exception:
8193 raise Z3Exception("model is not available")
8194
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.

◆ objectives()

objectives ( self)
returns set of objective functions

Definition at line 8230 of file z3py.py.

8230 def objectives(self):
8231 """returns set of objective functions"""
8232 return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
8233
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 8067 of file z3py.py.

8067 def param_descrs(self):
8068 """Return the parameter description set."""
8069 return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
8070
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 8171 of file z3py.py.

8171 def pop(self):
8172 """restore to previously created backtracking point"""
8173 Z3_optimize_pop(self.ctx.ref(), self.optimize)
8174
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.

◆ push()

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

Definition at line 8167 of file z3py.py.

8167 def push(self):
8168 """create a backtracking point for added rules, facts and assertions"""
8169 Z3_optimize_push(self.ctx.ref(), self.optimize)
8170
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.

◆ reason_unknown()

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

Definition at line 8184 of file z3py.py.

8184 def reason_unknown(self):
8185 """Return a string that describes why the last `check()` returned `unknown`."""
8186 return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
8187
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 8056 of file z3py.py.

8056 def set(self, *args, **keys):
8057 """Set a configuration option.
8058 The method `help()` return a string containing all available options.
8059 """
8060 p = args2params(args, keys, self.ctx)
8061 Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
8062
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 8144 of file z3py.py.

8144 def set_initial_value(self, var, value):
8145 """initialize the solver's state by setting the initial value of var to value
8146 """
8147 s = var.sort()
8148 value = s.cast(value)
8149 Z3_optimize_set_initial_value(self.ctx.ref(), self.optimize, var.ast, value.ast)
8150
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 8249 of file z3py.py.

8249 def set_on_model(self, on_model):
8250 """Register a callback that is invoked with every incremental improvement to
8251 objective values. The callback takes a model as argument.
8252 The life-time of the model is limited to the callback so the
8253 model has to be (deep) copied if it is to be used after the callback
8254 """
8255 id = len(_on_models) + 41
8256 mdl = Model(self.ctx)
8257 _on_models[id] = (on_model, mdl)
8258 self._on_models_id = id
8260 self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
8261 )
8262
8263
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 8238 of file z3py.py.

8238 def sexpr(self):
8239 """Return a formatted string (in Lisp-like format) with all added constraints.
8240 We say the string is in s-expression format.
8241 """
8242 return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
8243
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 8244 of file z3py.py.

8244 def statistics(self):
8245 """Return statistics for the last check`.
8246 """
8247 return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
8248
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 8195 of file z3py.py.

8195 def unsat_core(self):
8196 return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
8197
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 8203 of file z3py.py.

8203 def upper(self, obj):
8204 if not isinstance(obj, OptimizeObjective):
8205 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8206 return obj.upper()
8207

◆ upper_values()

upper_values ( self,
obj )

Definition at line 8213 of file z3py.py.

8213 def upper_values(self, obj):
8214 if not isinstance(obj, OptimizeObjective):
8215 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8216 return obj.upper_values()
8217

Field Documentation

◆ _on_models_id

_on_models_id = None
protected

Definition at line 8037 of file z3py.py.

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 8032 of file z3py.py.

◆ optimize

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

Definition at line 8034 of file z3py.py.