Z3
Public Member Functions | Data Fields
Optimize Class Reference
+ Inheritance diagram for Optimize:

Public Member Functions

def __init__
 
def __deepcopy__
 
def __del__ (self)
 
def set (self, args, keys)
 
def help (self)
 
def param_descrs (self)
 
def assert_exprs (self, args)
 
def add (self, args)
 
def __iadd__ (self, fml)
 
def assert_and_track (self, a, p)
 
def add_soft
 
def maximize (self, arg)
 
def minimize (self, arg)
 
def push (self)
 
def pop (self)
 
def check (self, assumptions)
 
def reason_unknown (self)
 
def model (self)
 
def unsat_core (self)
 
def lower (self, obj)
 
def upper (self, obj)
 
def lower_values (self, obj)
 
def upper_values (self, obj)
 
def from_file (self, filename)
 
def from_string (self, s)
 
def assertions (self)
 
def objectives (self)
 
def __repr__ (self)
 
def sexpr (self)
 
def statistics (self)
 
def set_on_model (self, on_model)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Data Fields

 ctx
 
 optimize
 

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

def __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 
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
def __init__
Definition: z3py.py:7929
def __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.
def __del__(self)
Definition: z3py.py:7938

Member Function Documentation

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7935 of file z3py.py.

7935  def __deepcopy__(self, memo={}):
7936  return Optimize(self.optimize, self.ctx)
7937 
def __deepcopy__
Definition: z3py.py:7935
def __iadd__ (   self,
  fml 
)

Definition at line 7975 of file z3py.py.

7975  def __iadd__(self, fml):
7976  self.add(fml)
7977  return self
7978 
def add(self, args)
Definition: z3py.py:7971
def __iadd__(self, fml)
Definition: z3py.py:7975
def __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 
def __repr__(self)
Definition: z3py.py:8115
def sexpr(self)
Definition: z3py.py:8119
def add (   self,
  args 
)
Assert constraints as background axioms for the optimize solver. Alias for assert_expr.

Definition at line 7971 of file z3py.py.

Referenced by Optimize.__iadd__().

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 
def add(self, args)
Definition: z3py.py:7971
def assert_exprs(self, args)
Definition: z3py.py:7959
def 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.
def to_symbol
Definition: z3py.py:124
def add_soft
Definition: z3py.py:8008
def 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 
def is_const(a)
Definition: z3py.py:1309
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.
def assert_and_track(self, a, p)
Definition: z3py.py:7979
def Bool
Definition: z3py.py:1768
def assert_exprs (   self,
  args 
)
Assert constraints as background axioms for the optimize solver.

Definition at line 7959 of file z3py.py.

Referenced by Optimize.add().

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 
def BoolSort
Definition: z3py.py:1731
def assert_exprs(self, args)
Definition: z3py.py:7959
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
def 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 
def assertions(self)
Definition: z3py.py:8107
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.
def 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 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
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.
def check(self, assumptions)
Definition: z3py.py:8056
def 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 
def from_file(self, filename)
Definition: z3py.py:8099
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. Add the parsed constraints and objectives to the optimization context.
def 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 
def from_string(self, s)
Definition: z3py.py:8103
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. Add the parsed constraints and objectives to the optimization context.
def 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 
def help(self)
Definition: z3py.py:7951
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.
def 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 
def lower(self, obj)
Definition: z3py.py:8079
def 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 
def lower_values(self, obj)
Definition: z3py.py:8089
def 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 
def maximize(self, arg)
Definition: z3py.py:8032
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
def 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 
def minimize(self, arg)
Definition: z3py.py:8040
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
def model (   self)
Return a model for the last check().

Definition at line 8069 of file z3py.py.

Referenced by FuncInterp.translate().

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.
def model(self)
Definition: z3py.py:8069
def 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...
def objectives(self)
Definition: z3py.py:8111
def 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 
def param_descrs(self)
Definition: z3py.py:7955
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.
def 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 
def pop(self)
Definition: z3py.py:8052
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
def 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 
def push(self)
Definition: z3py.py:8048
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
def 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 
def reason_unknown(self)
Definition: z3py.py:8065
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.
def 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 
def args2params
Definition: z3py.py:5512
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
def set(self, args, keys)
Definition: z3py.py:7944
def 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.
def Model
Definition: z3py.py:6735
def set_on_model(self, on_model)
Definition: z3py.py:8130
def 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.

Referenced by Optimize.__repr__().

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.
def sexpr(self)
Definition: z3py.py:8119
def 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 
Statistics.
Definition: z3py.py:6758
def statistics(self)
Definition: z3py.py:8125
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.
def 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 
def unsat_core(self)
Definition: z3py.py:8076
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 ...
def 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 
def upper(self, obj)
Definition: z3py.py:8084
def 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 
def upper_values(self, obj)
Definition: z3py.py:8094

Field Documentation

ctx
optimize