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

Public Member Functions

 __init__ (self, 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)
 
 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 7926 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
ctx = None )

Definition at line 7929 of file z3py.py.

7929 def __init__(self, ctx=None):
7930 self.ctx = _get_ctx(ctx)
7931 self.optimize = Z3_mk_optimize(self.ctx.ref())
7932 self._on_models_id = None
7933 Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7934
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 7938 of file z3py.py.

7938 def __del__(self):
7939 if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
7940 Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7941 if self._on_models_id is not None:
7942 del _on_models[self._on_models_id]
7943
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 7935 of file z3py.py.

7935 def __deepcopy__(self, memo={}):
7936 return Optimize(self.optimize, self.ctx)
7937

◆ __iadd__()

__iadd__ ( self,
fml )

Definition at line 7975 of file z3py.py.

7975 def __iadd__(self, fml):
7976 self.add(fml)
7977 return self
7978

◆ __repr__()

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

Definition at line 8115 of file z3py.py.

8115 def __repr__(self):
8116 """Return a formatted string with all added rules and constraints."""
8117 return self.sexpr()
8118

◆ add()

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

Definition at line 7971 of file z3py.py.

7971 def add(self, *args):
7972 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7973 self.assert_exprs(*args)
7974

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

8008 def add_soft(self, arg, weight="1", id=None):
8009 """Add soft constraint with optional weight and optional identifier.
8010 If no weight is supplied, then the penalty for violating the soft constraint
8011 is 1.
8012 Soft constraints are grouped by identifiers. Soft constraints that are
8013 added without identifiers are grouped by default.
8014 """
8015 if _is_int(weight):
8016 weight = "%d" % weight
8017 elif isinstance(weight, float):
8018 weight = "%f" % weight
8019 if not isinstance(weight, str):
8020 raise Z3Exception("weight should be a string or an integer")
8021 if id is None:
8022 id = ""
8023 id = to_symbol(id, self.ctx)
8024
8025 def asoft(a):
8026 v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
8027 return OptimizeObjective(self, v, False)
8028 if sys.version_info.major >= 3 and isinstance(arg, Iterable):
8029 return [asoft(a) for a in arg]
8030 return asoft(arg)
8031
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 7979 of file z3py.py.

7979 def assert_and_track(self, a, p):
7980 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7981
7982 If `p` is a string, it will be automatically converted into a Boolean constant.
7983
7984 >>> x = Int('x')
7985 >>> p3 = Bool('p3')
7986 >>> s = Optimize()
7987 >>> s.assert_and_track(x > 0, 'p1')
7988 >>> s.assert_and_track(x != 1, 'p2')
7989 >>> s.assert_and_track(x < 0, p3)
7990 >>> print(s.check())
7991 unsat
7992 >>> c = s.unsat_core()
7993 >>> len(c)
7994 2
7995 >>> Bool('p1') in c
7996 True
7997 >>> Bool('p2') in c
7998 False
7999 >>> p3 in c
8000 True
8001 """
8002 if isinstance(p, str):
8003 p = Bool(p, self.ctx)
8004 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
8005 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
8006 Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
8007
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 7959 of file z3py.py.

7959 def assert_exprs(self, *args):
7960 """Assert constraints as background axioms for the optimize solver."""
7961 args = _get_args(args)
7962 s = BoolSort(self.ctx)
7963 for arg in args:
7964 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7965 for f in arg:
7966 Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7967 else:
7968 arg = s.cast(arg)
7969 Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7970
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 8107 of file z3py.py.

8107 def assertions(self):
8108 """Return an AST vector containing all added constraints."""
8109 return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
8110
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 8056 of file z3py.py.

8056 def check(self, *assumptions):
8057 """Check consistency and produce optimal values."""
8058 assumptions = _get_args(assumptions)
8059 num = len(assumptions)
8060 _assumptions = (Ast * num)()
8061 for i in range(num):
8062 _assumptions[i] = assumptions[i].as_ast()
8063 return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
8064
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 8099 of file z3py.py.

8099 def from_file(self, filename):
8100 """Parse assertions and objectives from a file"""
8101 Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
8102
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 8103 of file z3py.py.

8103 def from_string(self, s):
8104 """Parse assertions and objectives from a string"""
8105 Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
8106
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 7951 of file z3py.py.

7951 def help(self):
7952 """Display a string describing all available options."""
7953 print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7954
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 8079 of file z3py.py.

8079 def lower(self, obj):
8080 if not isinstance(obj, OptimizeObjective):
8081 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8082 return obj.lower()
8083

◆ lower_values()

lower_values ( self,
obj )

Definition at line 8089 of file z3py.py.

8089 def lower_values(self, obj):
8090 if not isinstance(obj, OptimizeObjective):
8091 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8092 return obj.lower_values()
8093

◆ maximize()

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

Definition at line 8032 of file z3py.py.

8032 def maximize(self, arg):
8033 """Add objective function to maximize."""
8034 return OptimizeObjective(
8035 self,
8036 Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
8037 is_max=True,
8038 )
8039
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 8040 of file z3py.py.

8040 def minimize(self, arg):
8041 """Add objective function to minimize."""
8042 return OptimizeObjective(
8043 self,
8044 Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
8045 is_max=False,
8046 )
8047
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 8069 of file z3py.py.

8069 def model(self):
8070 """Return a model for the last check()."""
8071 try:
8072 return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
8073 except Z3Exception:
8074 raise Z3Exception("model is not available")
8075
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 8111 of file z3py.py.

8111 def objectives(self):
8112 """returns set of objective functions"""
8113 return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
8114
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 7955 of file z3py.py.

7955 def param_descrs(self):
7956 """Return the parameter description set."""
7957 return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7958
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 8052 of file z3py.py.

8052 def pop(self):
8053 """restore to previously created backtracking point"""
8054 Z3_optimize_pop(self.ctx.ref(), self.optimize)
8055
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 8048 of file z3py.py.

8048 def push(self):
8049 """create a backtracking point for added rules, facts and assertions"""
8050 Z3_optimize_push(self.ctx.ref(), self.optimize)
8051
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 8065 of file z3py.py.

8065 def reason_unknown(self):
8066 """Return a string that describes why the last `check()` returned `unknown`."""
8067 return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
8068
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 7944 of file z3py.py.

7944 def set(self, *args, **keys):
7945 """Set a configuration option.
7946 The method `help()` return a string containing all available options.
7947 """
7948 p = args2params(args, keys, self.ctx)
7949 Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7950
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.

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

8130 def set_on_model(self, on_model):
8131 """Register a callback that is invoked with every incremental improvement to
8132 objective values. The callback takes a model as argument.
8133 The life-time of the model is limited to the callback so the
8134 model has to be (deep) copied if it is to be used after the callback
8135 """
8136 id = len(_on_models) + 41
8137 mdl = Model(self.ctx)
8138 _on_models[id] = (on_model, mdl)
8139 self._on_models_id = id
8141 self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
8142 )
8143
8144
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 8119 of file z3py.py.

8119 def sexpr(self):
8120 """Return a formatted string (in Lisp-like format) with all added constraints.
8121 We say the string is in s-expression format.
8122 """
8123 return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
8124
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 8125 of file z3py.py.

8125 def statistics(self):
8126 """Return statistics for the last check`.
8127 """
8128 return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
8129
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 8076 of file z3py.py.

8076 def unsat_core(self):
8077 return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
8078
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 8084 of file z3py.py.

8084 def upper(self, obj):
8085 if not isinstance(obj, OptimizeObjective):
8086 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8087 return obj.upper()
8088

◆ upper_values()

upper_values ( self,
obj )

Definition at line 8094 of file z3py.py.

8094 def upper_values(self, obj):
8095 if not isinstance(obj, OptimizeObjective):
8096 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8097 return obj.upper_values()
8098

Field Documentation

◆ _on_models_id

_on_models_id = None
protected

Definition at line 7932 of file z3py.py.

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 7930 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 7931 of file z3py.py.