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

Constructor & Destructor Documentation

def __init__ (   self,
  ctx = None 
)

Definition at line 7861 of file z3py.py.

7861  def __init__(self, ctx=None):
7862  self.ctx = _get_ctx(ctx)
7863  self.optimize = Z3_mk_optimize(self.ctx.ref())
7864  self._on_models_id = None
7865  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7866 
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:7861
def __del__ (   self)

Definition at line 7870 of file z3py.py.

7870  def __del__(self):
7871  if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
7872  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7873  if self._on_models_id is not None:
7874  del _on_models[self._on_models_id]
7875 
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:7870

Member Function Documentation

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7867 of file z3py.py.

7867  def __deepcopy__(self, memo={}):
7868  return Optimize(self.optimize, self.ctx)
7869 
def __deepcopy__
Definition: z3py.py:7867
def __iadd__ (   self,
  fml 
)

Definition at line 7907 of file z3py.py.

7907  def __iadd__(self, fml):
7908  self.add(fml)
7909  return self
7910 
def add(self, args)
Definition: z3py.py:7903
def __iadd__(self, fml)
Definition: z3py.py:7907
def __repr__ (   self)
Return a formatted string with all added rules and constraints.

Definition at line 8047 of file z3py.py.

8047  def __repr__(self):
8048  """Return a formatted string with all added rules and constraints."""
8049  return self.sexpr()
8050 
def __repr__(self)
Definition: z3py.py:8047
def sexpr(self)
Definition: z3py.py:8051
def add (   self,
  args 
)
Assert constraints as background axioms for the optimize solver. Alias for assert_expr.

Definition at line 7903 of file z3py.py.

Referenced by Optimize.__iadd__().

7903  def add(self, *args):
7904  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7905  self.assert_exprs(*args)
7906 
def add(self, args)
Definition: z3py.py:7903
def assert_exprs(self, args)
Definition: z3py.py:7891
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 7940 of file z3py.py.

7940  def add_soft(self, arg, weight="1", id=None):
7941  """Add soft constraint with optional weight and optional identifier.
7942  If no weight is supplied, then the penalty for violating the soft constraint
7943  is 1.
7944  Soft constraints are grouped by identifiers. Soft constraints that are
7945  added without identifiers are grouped by default.
7946  """
7947  if _is_int(weight):
7948  weight = "%d" % weight
7949  elif isinstance(weight, float):
7950  weight = "%f" % weight
7951  if not isinstance(weight, str):
7952  raise Z3Exception("weight should be a string or an integer")
7953  if id is None:
7954  id = ""
7955  id = to_symbol(id, self.ctx)
7956 
7957  def asoft(a):
7958  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
7959  return OptimizeObjective(self, v, False)
7960  if sys.version_info.major >= 3 and isinstance(arg, Iterable):
7961  return [asoft(a) for a in arg]
7962  return asoft(arg)
7963 
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:7940
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 7911 of file z3py.py.

7911  def assert_and_track(self, a, p):
7912  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7913 
7914  If `p` is a string, it will be automatically converted into a Boolean constant.
7915 
7916  >>> x = Int('x')
7917  >>> p3 = Bool('p3')
7918  >>> s = Optimize()
7919  >>> s.assert_and_track(x > 0, 'p1')
7920  >>> s.assert_and_track(x != 1, 'p2')
7921  >>> s.assert_and_track(x < 0, p3)
7922  >>> print(s.check())
7923  unsat
7924  >>> c = s.unsat_core()
7925  >>> len(c)
7926  2
7927  >>> Bool('p1') in c
7928  True
7929  >>> Bool('p2') in c
7930  False
7931  >>> p3 in c
7932  True
7933  """
7934  if isinstance(p, str):
7935  p = Bool(p, self.ctx)
7936  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7937  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7938  Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
7939 
def is_const(a)
Definition: z3py.py:1287
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:7911
def Bool
Definition: z3py.py:1724
def assert_exprs (   self,
  args 
)
Assert constraints as background axioms for the optimize solver.

Definition at line 7891 of file z3py.py.

Referenced by Optimize.add().

7891  def assert_exprs(self, *args):
7892  """Assert constraints as background axioms for the optimize solver."""
7893  args = _get_args(args)
7894  s = BoolSort(self.ctx)
7895  for arg in args:
7896  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7897  for f in arg:
7898  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7899  else:
7900  arg = s.cast(arg)
7901  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7902 
def BoolSort
Definition: z3py.py:1687
def assert_exprs(self, args)
Definition: z3py.py:7891
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 8039 of file z3py.py.

8039  def assertions(self):
8040  """Return an AST vector containing all added constraints."""
8041  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
8042 
def assertions(self)
Definition: z3py.py:8039
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 satisfiability while optimizing objective functions.

Definition at line 7988 of file z3py.py.

7988  def check(self, *assumptions):
7989  """Check satisfiability while optimizing objective functions."""
7990  assumptions = _get_args(assumptions)
7991  num = len(assumptions)
7992  _assumptions = (Ast * num)()
7993  for i in range(num):
7994  _assumptions[i] = assumptions[i].as_ast()
7995  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7996 
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:7988
def from_file (   self,
  filename 
)
Parse assertions and objectives from a file

Definition at line 8031 of file z3py.py.

8031  def from_file(self, filename):
8032  """Parse assertions and objectives from a file"""
8033  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
8034 
def from_file(self, filename)
Definition: z3py.py:8031
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 8035 of file z3py.py.

8035  def from_string(self, s):
8036  """Parse assertions and objectives from a string"""
8037  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
8038 
def from_string(self, s)
Definition: z3py.py:8035
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 7883 of file z3py.py.

7883  def help(self):
7884  """Display a string describing all available options."""
7885  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7886 
def help(self)
Definition: z3py.py:7883
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 8011 of file z3py.py.

8011  def lower(self, obj):
8012  if not isinstance(obj, OptimizeObjective):
8013  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8014  return obj.lower()
8015 
def lower(self, obj)
Definition: z3py.py:8011
def lower_values (   self,
  obj 
)

Definition at line 8021 of file z3py.py.

8021  def lower_values(self, obj):
8022  if not isinstance(obj, OptimizeObjective):
8023  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8024  return obj.lower_values()
8025 
def lower_values(self, obj)
Definition: z3py.py:8021
def maximize (   self,
  arg 
)
Add objective function to maximize.

Definition at line 7964 of file z3py.py.

7964  def maximize(self, arg):
7965  """Add objective function to maximize."""
7966  return OptimizeObjective(
7967  self,
7968  Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
7969  is_max=True,
7970  )
7971 
def maximize(self, arg)
Definition: z3py.py:7964
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 7972 of file z3py.py.

7972  def minimize(self, arg):
7973  """Add objective function to minimize."""
7974  return OptimizeObjective(
7975  self,
7976  Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
7977  is_max=False,
7978  )
7979 
def minimize(self, arg)
Definition: z3py.py:7972
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 8001 of file z3py.py.

Referenced by FuncInterp.translate().

8001  def model(self):
8002  """Return a model for the last check()."""
8003  try:
8004  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
8005  except Z3Exception:
8006  raise Z3Exception("model is not available")
8007 
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:8001
def objectives (   self)
returns set of objective functions

Definition at line 8043 of file z3py.py.

8043  def objectives(self):
8044  """returns set of objective functions"""
8045  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
8046 
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:8043
def param_descrs (   self)
Return the parameter description set.

Definition at line 7887 of file z3py.py.

7887  def param_descrs(self):
7888  """Return the parameter description set."""
7889  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7890 
def param_descrs(self)
Definition: z3py.py:7887
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 7984 of file z3py.py.

7984  def pop(self):
7985  """restore to previously created backtracking point"""
7986  Z3_optimize_pop(self.ctx.ref(), self.optimize)
7987 
def pop(self)
Definition: z3py.py:7984
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 7980 of file z3py.py.

7980  def push(self):
7981  """create a backtracking point for added rules, facts and assertions"""
7982  Z3_optimize_push(self.ctx.ref(), self.optimize)
7983 
def push(self)
Definition: z3py.py:7980
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 7997 of file z3py.py.

7997  def reason_unknown(self):
7998  """Return a string that describes why the last `check()` returned `unknown`."""
7999  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
8000 
def reason_unknown(self)
Definition: z3py.py:7997
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 7876 of file z3py.py.

7876  def set(self, *args, **keys):
7877  """Set a configuration option.
7878  The method `help()` return a string containing all available options.
7879  """
7880  p = args2params(args, keys, self.ctx)
7881  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7882 
def args2params
Definition: z3py.py:5458
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:7876
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 8062 of file z3py.py.

8062  def set_on_model(self, on_model):
8063  """Register a callback that is invoked with every incremental improvement to
8064  objective values. The callback takes a model as argument.
8065  The life-time of the model is limited to the callback so the
8066  model has to be (deep) copied if it is to be used after the callback
8067  """
8068  id = len(_on_models) + 41
8069  mdl = Model(self.ctx)
8070  _on_models[id] = (on_model, mdl)
8071  self._on_models_id = id
8073  self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
8074  )
8075 
8076 
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:6681
def set_on_model(self, on_model)
Definition: z3py.py:8062
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 8051 of file z3py.py.

Referenced by Optimize.__repr__().

8051  def sexpr(self):
8052  """Return a formatted string (in Lisp-like format) with all added constraints.
8053  We say the string is in s-expression format.
8054  """
8055  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
8056 
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:8051
def statistics (   self)
Return statistics for the last check`.

Definition at line 8057 of file z3py.py.

8057  def statistics(self):
8058  """Return statistics for the last check`.
8059  """
8060  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
8061 
Statistics.
Definition: z3py.py:6704
def statistics(self)
Definition: z3py.py:8057
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 8008 of file z3py.py.

8008  def unsat_core(self):
8009  return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
8010 
def unsat_core(self)
Definition: z3py.py:8008
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 8016 of file z3py.py.

8016  def upper(self, obj):
8017  if not isinstance(obj, OptimizeObjective):
8018  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8019  return obj.upper()
8020 
def upper(self, obj)
Definition: z3py.py:8016
def upper_values (   self,
  obj 
)

Definition at line 8026 of file z3py.py.

8026  def upper_values(self, obj):
8027  if not isinstance(obj, OptimizeObjective):
8028  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8029  return obj.upper_values()
8030 
def upper_values(self, obj)
Definition: z3py.py:8026

Field Documentation

ctx
optimize