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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 8022 of file z3py.py.

8022 def __init__(self, optimize=None, ctx=None):
8023 self.ctx = _get_ctx(ctx)
8024 if optimize is None:
8025 self.optimize = Z3_mk_optimize(self.ctx.ref())
8026 else:
8027 self.optimize = optimize
8028 self._on_models_id = None
8029 Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
8030
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 8034 of file z3py.py.

8034 def __del__(self):
8035 if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
8036 Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
8037 if self._on_models_id is not None:
8038 del _on_models[self._on_models_id]
8039
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 8031 of file z3py.py.

8031 def __deepcopy__(self, memo={}):
8032 return Optimize(self.optimize, self.ctx)
8033

◆ __enter__()

__enter__ ( self)

Definition at line 8040 of file z3py.py.

8040 def __enter__(self):
8041 self.push()
8042 return self
8043

◆ __exit__()

__exit__ ( self,
* exc_info )

Definition at line 8044 of file z3py.py.

8044 def __exit__(self, *exc_info):
8045 self.pop()
8046

◆ __iadd__()

__iadd__ ( self,
fml )

Definition at line 8078 of file z3py.py.

8078 def __iadd__(self, fml):
8079 self.add(fml)
8080 return self
8081

◆ __repr__()

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

Definition at line 8225 of file z3py.py.

8225 def __repr__(self):
8226 """Return a formatted string with all added rules and constraints."""
8227 return self.sexpr()
8228

◆ add()

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

Definition at line 8074 of file z3py.py.

8074 def add(self, *args):
8075 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
8076 self.assert_exprs(*args)
8077

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

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

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

8062 def assert_exprs(self, *args):
8063 """Assert constraints as background axioms for the optimize solver."""
8064 args = _get_args(args)
8065 s = BoolSort(self.ctx)
8066 for arg in args:
8067 if isinstance(arg, Goal) or isinstance(arg, AstVector):
8068 for f in arg:
8069 Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
8070 else:
8071 arg = s.cast(arg)
8072 Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
8073
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 8217 of file z3py.py.

8217 def assertions(self):
8218 """Return an AST vector containing all added constraints."""
8219 return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
8220
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 8166 of file z3py.py.

8166 def check(self, *assumptions):
8167 """Check consistency and produce optimal values."""
8168 assumptions = _get_args(assumptions)
8169 num = len(assumptions)
8170 _assumptions = (Ast * num)()
8171 for i in range(num):
8172 _assumptions[i] = assumptions[i].as_ast()
8173 return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
8174
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 8209 of file z3py.py.

8209 def from_file(self, filename):
8210 """Parse assertions and objectives from a file"""
8211 Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
8212
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 8213 of file z3py.py.

8213 def from_string(self, s):
8214 """Parse assertions and objectives from a string"""
8215 Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
8216
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 8054 of file z3py.py.

8054 def help(self):
8055 """Display a string describing all available options."""
8056 print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
8057
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 8189 of file z3py.py.

8189 def lower(self, obj):
8190 if not isinstance(obj, OptimizeObjective):
8191 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8192 return obj.lower()
8193

◆ lower_values()

lower_values ( self,
obj )

Definition at line 8199 of file z3py.py.

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

◆ maximize()

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

Definition at line 8142 of file z3py.py.

8142 def maximize(self, arg):
8143 """Add objective function to maximize."""
8144 return OptimizeObjective(
8145 self,
8146 Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
8147 is_max=True,
8148 )
8149
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 8150 of file z3py.py.

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

8179 def model(self):
8180 """Return a model for the last check()."""
8181 try:
8182 return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
8183 except Z3Exception:
8184 raise Z3Exception("model is not available")
8185
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 8221 of file z3py.py.

8221 def objectives(self):
8222 """returns set of objective functions"""
8223 return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
8224
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 8058 of file z3py.py.

8058 def param_descrs(self):
8059 """Return the parameter description set."""
8060 return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
8061
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 8162 of file z3py.py.

8162 def pop(self):
8163 """restore to previously created backtracking point"""
8164 Z3_optimize_pop(self.ctx.ref(), self.optimize)
8165
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 8158 of file z3py.py.

8158 def push(self):
8159 """create a backtracking point for added rules, facts and assertions"""
8160 Z3_optimize_push(self.ctx.ref(), self.optimize)
8161
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 8175 of file z3py.py.

8175 def reason_unknown(self):
8176 """Return a string that describes why the last `check()` returned `unknown`."""
8177 return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
8178
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 8047 of file z3py.py.

8047 def set(self, *args, **keys):
8048 """Set a configuration option.
8049 The method `help()` return a string containing all available options.
8050 """
8051 p = args2params(args, keys, self.ctx)
8052 Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
8053
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 8135 of file z3py.py.

8135 def set_initial_value(self, var, value):
8136 """initialize the solver's state by setting the initial value of var to value
8137 """
8138 s = var.sort()
8139 value = s.cast(value)
8140 Z3_optimize_set_initial_value(self.ctx.ref(), self.optimize, var.ast, value.ast)
8141
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 8240 of file z3py.py.

8240 def set_on_model(self, on_model):
8241 """Register a callback that is invoked with every incremental improvement to
8242 objective values. The callback takes a model as argument.
8243 The life-time of the model is limited to the callback so the
8244 model has to be (deep) copied if it is to be used after the callback
8245 """
8246 id = len(_on_models) + 41
8247 mdl = Model(self.ctx)
8248 _on_models[id] = (on_model, mdl)
8249 self._on_models_id = id
8251 self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
8252 )
8253
8254
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 8229 of file z3py.py.

8229 def sexpr(self):
8230 """Return a formatted string (in Lisp-like format) with all added constraints.
8231 We say the string is in s-expression format.
8232 """
8233 return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
8234
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 8235 of file z3py.py.

8235 def statistics(self):
8236 """Return statistics for the last check`.
8237 """
8238 return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
8239
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 8186 of file z3py.py.

8186 def unsat_core(self):
8187 return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
8188
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 8194 of file z3py.py.

8194 def upper(self, obj):
8195 if not isinstance(obj, OptimizeObjective):
8196 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8197 return obj.upper()
8198

◆ upper_values()

upper_values ( self,
obj )

Definition at line 8204 of file z3py.py.

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

Field Documentation

◆ _on_models_id

_on_models_id = None
protected

Definition at line 8028 of file z3py.py.

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 8023 of file z3py.py.

◆ optimize

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

Definition at line 8025 of file z3py.py.