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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 8026 of file z3py.py.

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

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

8035 def __deepcopy__(self, memo={}):
8036 return Optimize(self.optimize, self.ctx)
8037

◆ __enter__()

__enter__ ( self)

Definition at line 8044 of file z3py.py.

8044 def __enter__(self):
8045 self.push()
8046 return self
8047

◆ __exit__()

__exit__ ( self,
* exc_info )

Definition at line 8048 of file z3py.py.

8048 def __exit__(self, *exc_info):
8049 self.pop()
8050

◆ __iadd__()

__iadd__ ( self,
fml )

Definition at line 8082 of file z3py.py.

8082 def __iadd__(self, fml):
8083 self.add(fml)
8084 return self
8085

◆ __repr__()

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

Definition at line 8229 of file z3py.py.

8229 def __repr__(self):
8230 """Return a formatted string with all added rules and constraints."""
8231 return self.sexpr()
8232

◆ add()

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

Definition at line 8078 of file z3py.py.

8078 def add(self, *args):
8079 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
8080 self.assert_exprs(*args)
8081

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

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

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

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

8221 def assertions(self):
8222 """Return an AST vector containing all added constraints."""
8223 return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
8224
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 8170 of file z3py.py.

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

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

8217 def from_string(self, s):
8218 """Parse assertions and objectives from a string"""
8219 Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
8220
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 8058 of file z3py.py.

8058 def help(self):
8059 """Display a string describing all available options."""
8060 print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
8061
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 8193 of file z3py.py.

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

◆ lower_values()

lower_values ( self,
obj )

Definition at line 8203 of file z3py.py.

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

◆ maximize()

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

Definition at line 8146 of file z3py.py.

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

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

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

8225 def objectives(self):
8226 """returns set of objective functions"""
8227 return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
8228
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 8062 of file z3py.py.

8062 def param_descrs(self):
8063 """Return the parameter description set."""
8064 return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
8065
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 8166 of file z3py.py.

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

8162 def push(self):
8163 """create a backtracking point for added rules, facts and assertions"""
8164 Z3_optimize_push(self.ctx.ref(), self.optimize)
8165
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 8179 of file z3py.py.

8179 def reason_unknown(self):
8180 """Return a string that describes why the last `check()` returned `unknown`."""
8181 return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
8182
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 8051 of file z3py.py.

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

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

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

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

8239 def statistics(self):
8240 """Return statistics for the last check`.
8241 """
8242 return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
8243
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 8190 of file z3py.py.

8190 def unsat_core(self):
8191 return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
8192
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 8198 of file z3py.py.

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

◆ upper_values()

upper_values ( self,
obj )

Definition at line 8208 of file z3py.py.

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

Field Documentation

◆ _on_models_id

_on_models_id = None
protected

Definition at line 8032 of file z3py.py.

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 8027 of file z3py.py.

◆ optimize

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

Definition at line 8029 of file z3py.py.