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

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 7976 of file z3py.py.

7976 def __init__(self, optimize=None, ctx=None):
7977 self.ctx = _get_ctx(ctx)
7978 if optimize is None:
7979 self.optimize = Z3_mk_optimize(self.ctx.ref())
7980 else:
7981 self.optimize = optimize
7982 self._on_models_id = None
7983 Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7984
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 7988 of file z3py.py.

7988 def __del__(self):
7989 if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
7990 Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7991 if self._on_models_id is not None:
7992 del _on_models[self._on_models_id]
7993
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 7985 of file z3py.py.

7985 def __deepcopy__(self, memo={}):
7986 return Optimize(self.optimize, self.ctx)
7987

◆ __enter__()

__enter__ ( self)

Definition at line 7994 of file z3py.py.

7994 def __enter__(self):
7995 self.push()
7996 return self
7997

◆ __exit__()

__exit__ ( self,
* exc_info )

Definition at line 7998 of file z3py.py.

7998 def __exit__(self, *exc_info):
7999 self.pop()
8000

◆ __iadd__()

__iadd__ ( self,
fml )

Definition at line 8032 of file z3py.py.

8032 def __iadd__(self, fml):
8033 self.add(fml)
8034 return self
8035

◆ __repr__()

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

Definition at line 8179 of file z3py.py.

8179 def __repr__(self):
8180 """Return a formatted string with all added rules and constraints."""
8181 return self.sexpr()
8182

◆ add()

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

Definition at line 8028 of file z3py.py.

8028 def add(self, *args):
8029 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
8030 self.assert_exprs(*args)
8031

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

8065 def add_soft(self, arg, weight="1", id=None):
8066 """Add soft constraint with optional weight and optional identifier.
8067 If no weight is supplied, then the penalty for violating the soft constraint
8068 is 1.
8069 Soft constraints are grouped by identifiers. Soft constraints that are
8070 added without identifiers are grouped by default.
8071 """
8072 if _is_int(weight):
8073 weight = "%d" % weight
8074 elif isinstance(weight, float):
8075 weight = "%f" % weight
8076 if not isinstance(weight, str):
8077 raise Z3Exception("weight should be a string or an integer")
8078 if id is None:
8079 id = ""
8080 id = to_symbol(id, self.ctx)
8081
8082 def asoft(a):
8083 v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
8084 return OptimizeObjective(self, v, False)
8085 if sys.version_info.major >= 3 and isinstance(arg, Iterable):
8086 return [asoft(a) for a in arg]
8087 return asoft(arg)
8088
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 8036 of file z3py.py.

8036 def assert_and_track(self, a, p):
8037 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
8038
8039 If `p` is a string, it will be automatically converted into a Boolean constant.
8040
8041 >>> x = Int('x')
8042 >>> p3 = Bool('p3')
8043 >>> s = Optimize()
8044 >>> s.assert_and_track(x > 0, 'p1')
8045 >>> s.assert_and_track(x != 1, 'p2')
8046 >>> s.assert_and_track(x < 0, p3)
8047 >>> print(s.check())
8048 unsat
8049 >>> c = s.unsat_core()
8050 >>> len(c)
8051 2
8052 >>> Bool('p1') in c
8053 True
8054 >>> Bool('p2') in c
8055 False
8056 >>> p3 in c
8057 True
8058 """
8059 if isinstance(p, str):
8060 p = Bool(p, self.ctx)
8061 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
8062 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
8063 Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
8064
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 8016 of file z3py.py.

8016 def assert_exprs(self, *args):
8017 """Assert constraints as background axioms for the optimize solver."""
8018 args = _get_args(args)
8019 s = BoolSort(self.ctx)
8020 for arg in args:
8021 if isinstance(arg, Goal) or isinstance(arg, AstVector):
8022 for f in arg:
8023 Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
8024 else:
8025 arg = s.cast(arg)
8026 Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
8027
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 8171 of file z3py.py.

8171 def assertions(self):
8172 """Return an AST vector containing all added constraints."""
8173 return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
8174
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 8120 of file z3py.py.

8120 def check(self, *assumptions):
8121 """Check consistency and produce optimal values."""
8122 assumptions = _get_args(assumptions)
8123 num = len(assumptions)
8124 _assumptions = (Ast * num)()
8125 for i in range(num):
8126 _assumptions[i] = assumptions[i].as_ast()
8127 return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
8128
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 8163 of file z3py.py.

8163 def from_file(self, filename):
8164 """Parse assertions and objectives from a file"""
8165 Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
8166
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 8167 of file z3py.py.

8167 def from_string(self, s):
8168 """Parse assertions and objectives from a string"""
8169 Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
8170
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 8008 of file z3py.py.

8008 def help(self):
8009 """Display a string describing all available options."""
8010 print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
8011
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 8143 of file z3py.py.

8143 def lower(self, obj):
8144 if not isinstance(obj, OptimizeObjective):
8145 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8146 return obj.lower()
8147

◆ lower_values()

lower_values ( self,
obj )

Definition at line 8153 of file z3py.py.

8153 def lower_values(self, obj):
8154 if not isinstance(obj, OptimizeObjective):
8155 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8156 return obj.lower_values()
8157

◆ maximize()

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

Definition at line 8096 of file z3py.py.

8096 def maximize(self, arg):
8097 """Add objective function to maximize."""
8098 return OptimizeObjective(
8099 self,
8100 Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
8101 is_max=True,
8102 )
8103
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 8104 of file z3py.py.

8104 def minimize(self, arg):
8105 """Add objective function to minimize."""
8106 return OptimizeObjective(
8107 self,
8108 Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
8109 is_max=False,
8110 )
8111
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 8133 of file z3py.py.

8133 def model(self):
8134 """Return a model for the last check()."""
8135 try:
8136 return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
8137 except Z3Exception:
8138 raise Z3Exception("model is not available")
8139
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 8175 of file z3py.py.

8175 def objectives(self):
8176 """returns set of objective functions"""
8177 return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
8178
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 8012 of file z3py.py.

8012 def param_descrs(self):
8013 """Return the parameter description set."""
8014 return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
8015
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 8116 of file z3py.py.

8116 def pop(self):
8117 """restore to previously created backtracking point"""
8118 Z3_optimize_pop(self.ctx.ref(), self.optimize)
8119
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 8112 of file z3py.py.

8112 def push(self):
8113 """create a backtracking point for added rules, facts and assertions"""
8114 Z3_optimize_push(self.ctx.ref(), self.optimize)
8115
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 8129 of file z3py.py.

8129 def reason_unknown(self):
8130 """Return a string that describes why the last `check()` returned `unknown`."""
8131 return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
8132
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 8001 of file z3py.py.

8001 def set(self, *args, **keys):
8002 """Set a configuration option.
8003 The method `help()` return a string containing all available options.
8004 """
8005 p = args2params(args, keys, self.ctx)
8006 Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
8007
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 8089 of file z3py.py.

8089 def set_initial_value(self, var, value):
8090 """initialize the solver's state by setting the initial value of var to value
8091 """
8092 s = var.sort()
8093 value = s.cast(value)
8094 Z3_optimize_set_initial_value(self.ctx.ref(), self.optimize, var.ast, value.ast)
8095
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 8194 of file z3py.py.

8194 def set_on_model(self, on_model):
8195 """Register a callback that is invoked with every incremental improvement to
8196 objective values. The callback takes a model as argument.
8197 The life-time of the model is limited to the callback so the
8198 model has to be (deep) copied if it is to be used after the callback
8199 """
8200 id = len(_on_models) + 41
8201 mdl = Model(self.ctx)
8202 _on_models[id] = (on_model, mdl)
8203 self._on_models_id = id
8205 self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
8206 )
8207
8208
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 8183 of file z3py.py.

8183 def sexpr(self):
8184 """Return a formatted string (in Lisp-like format) with all added constraints.
8185 We say the string is in s-expression format.
8186 """
8187 return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
8188
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 8189 of file z3py.py.

8189 def statistics(self):
8190 """Return statistics for the last check`.
8191 """
8192 return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
8193
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 8140 of file z3py.py.

8140 def unsat_core(self):
8141 return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
8142
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 8148 of file z3py.py.

8148 def upper(self, obj):
8149 if not isinstance(obj, OptimizeObjective):
8150 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8151 return obj.upper()
8152

◆ upper_values()

upper_values ( self,
obj )

Definition at line 8158 of file z3py.py.

8158 def upper_values(self, obj):
8159 if not isinstance(obj, OptimizeObjective):
8160 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8161 return obj.upper_values()
8162

Field Documentation

◆ _on_models_id

_on_models_id = None
protected

Definition at line 7982 of file z3py.py.

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 7977 of file z3py.py.

◆ optimize

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

Definition at line 7979 of file z3py.py.