Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions | Data Fields
Optimize Class Reference
+ Inheritance diagram for Optimize:

Public Member Functions

def __init__
 
def __deepcopy__
 
def __del__
 
def set
 
def help
 
def param_descrs
 
def assert_exprs
 
def add
 
def __iadd__
 
def assert_and_track
 
def add_soft
 
def maximize
 
def minimize
 
def push
 
def pop
 
def check
 
def reason_unknown
 
def model
 
def unsat_core
 
def lower
 
def upper
 
def lower_values
 
def upper_values
 
def from_file
 
def from_string
 
def assertions
 
def objectives
 
def __repr__
 
def sexpr
 
def statistics
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

Data Fields

 ctx
 
 optimize
 

Detailed Description

Optimize API provides methods for solving using objective functions and weighted soft constraints

Definition at line 7324 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  ctx = None 
)

Definition at line 7327 of file z3py.py.

7328  def __init__(self, ctx=None):
7329  self.ctx = _get_ctx(ctx)
7330  self.optimize = Z3_mk_optimize(self.ctx.ref())
7331  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
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:7327
def __del__ (   self)

Definition at line 7335 of file z3py.py.

7336  def __del__(self):
7337  if self.optimize is not None and self.ctx.ref() is not None:
7338  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
def __del__
Definition: z3py.py:7335
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

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7332 of file z3py.py.

7333  def __deepcopy__(self, memo={}):
7334  return Optimize(self.optimize, self.ctx)
def __deepcopy__
Definition: z3py.py:7332
def __iadd__ (   self,
  fml 
)

Definition at line 7369 of file z3py.py.

7370  def __iadd__(self, fml):
7371  self.add(fml)
7372  return self
def __iadd__
Definition: z3py.py:7369
def __repr__ (   self)
Return a formatted string with all added rules and constraints.

Definition at line 7496 of file z3py.py.

7497  def __repr__(self):
7498  """Return a formatted string with all added rules and constraints."""
7499  return self.sexpr()
def sexpr
Definition: z3py.py:7500
def __repr__
Definition: z3py.py:7496
def add (   self,
  args 
)
Assert constraints as background axioms for the optimize solver. Alias for assert_expr.

Definition at line 7365 of file z3py.py.

Referenced by Optimize.__iadd__().

7366  def add(self, *args):
7367  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7368  self.assert_exprs(*args)
def assert_exprs
Definition: z3py.py:7353
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 7402 of file z3py.py.

7403  def add_soft(self, arg, weight = "1", id = None):
7404  """Add soft constraint with optional weight and optional identifier.
7405  If no weight is supplied, then the penalty for violating the soft constraint
7406  is 1.
7407  Soft constraints are grouped by identifiers. Soft constraints that are
7408  added without identifiers are grouped by default.
7409  """
7410  if _is_int(weight):
7411  weight = "%d" % weight
7412  elif isinstance(weight, float):
7413  weight = "%f" % weight
7414  if not isinstance(weight, str):
7415  raise Z3Exception("weight should be a string or an integer")
7416  if id is None:
7417  id = ""
7418  id = to_symbol(id, self.ctx)
7419  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
7420  return OptimizeObjective(self, v, False)
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:111
def add_soft
Definition: z3py.py:7402
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 7373 of file z3py.py.

7374  def assert_and_track(self, a, p):
7375  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7376 
7377  If `p` is a string, it will be automatically converted into a Boolean constant.
7378 
7379  >>> x = Int('x')
7380  >>> p3 = Bool('p3')
7381  >>> s = Optimize()
7382  >>> s.assert_and_track(x > 0, 'p1')
7383  >>> s.assert_and_track(x != 1, 'p2')
7384  >>> s.assert_and_track(x < 0, p3)
7385  >>> print(s.check())
7386  unsat
7387  >>> c = s.unsat_core()
7388  >>> len(c)
7389  2
7390  >>> Bool('p1') in c
7391  True
7392  >>> Bool('p2') in c
7393  False
7394  >>> p3 in c
7395  True
7396  """
7397  if isinstance(p, str):
7398  p = Bool(p, self.ctx)
7399  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7400  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7401  Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
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 is_const
Definition: z3py.py:1152
def Bool
Definition: z3py.py:1558
def assert_and_track
Definition: z3py.py:7373
def assert_exprs (   self,
  args 
)
Assert constraints as background axioms for the optimize solver.

Definition at line 7353 of file z3py.py.

Referenced by Optimize.add().

7354  def assert_exprs(self, *args):
7355  """Assert constraints as background axioms for the optimize solver."""
7356  args = _get_args(args)
7357  s = BoolSort(self.ctx)
7358  for arg in args:
7359  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7360  for f in arg:
7361  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7362  else:
7363  arg = s.cast(arg)
7364  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
def BoolSort
Definition: z3py.py:1523
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
def assert_exprs
Definition: z3py.py:7353
def assertions (   self)
Return an AST vector containing all added constraints.

Definition at line 7488 of file z3py.py.

7489  def assertions(self):
7490  """Return an AST vector containing all added constraints."""
7491  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
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 assertions
Definition: z3py.py:7488
def check (   self,
  assumptions 
)
Check satisfiability while optimizing objective functions.

Definition at line 7437 of file z3py.py.

7438  def check(self, *assumptions):
7439  """Check satisfiability while optimizing objective functions."""
7440  assumptions = _get_args(assumptions)
7441  num = len(assumptions)
7442  _assumptions = (Ast * num)()
7443  for i in range(num):
7444  _assumptions[i] = assumptions[i].as_ast()
7445  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
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
Definition: z3py.py:7437
def from_file (   self,
  filename 
)
Parse assertions and objectives from a file

Definition at line 7480 of file z3py.py.

7481  def from_file(self, filename):
7482  """Parse assertions and objectives from a file"""
7483  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
def from_file
Definition: z3py.py:7480
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 7484 of file z3py.py.

7485  def from_string(self, s):
7486  """Parse assertions and objectives from a string"""
7487  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
def from_string
Definition: z3py.py:7484
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 7345 of file z3py.py.

7346  def help(self):
7347  """Display a string describing all available options."""
7348  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
def help
Definition: z3py.py:7345
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 7460 of file z3py.py.

7461  def lower(self, obj):
7462  if not isinstance(obj, OptimizeObjective):
7463  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7464  return obj.lower()
def lower
Definition: z3py.py:7460
def lower_values (   self,
  obj 
)

Definition at line 7470 of file z3py.py.

7471  def lower_values(self, obj):
7472  if not isinstance(obj, OptimizeObjective):
7473  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7474  return obj.lower_values()
def lower_values
Definition: z3py.py:7470
def maximize (   self,
  arg 
)
Add objective function to maximize.

Definition at line 7421 of file z3py.py.

7422  def maximize(self, arg):
7423  """Add objective function to maximize."""
7424  return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
def maximize
Definition: z3py.py:7421
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 7425 of file z3py.py.

7426  def minimize(self, arg):
7427  """Add objective function to minimize."""
7428  return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
def minimize
Definition: z3py.py:7425
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 7450 of file z3py.py.

Referenced by FuncInterp.translate().

7451  def model(self):
7452  """Return a model for the last check()."""
7453  try:
7454  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7455  except Z3Exception:
7456  raise Z3Exception("model is not available")
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
Definition: z3py.py:7450
def objectives (   self)
returns set of objective functions

Definition at line 7492 of file z3py.py.

7493  def objectives(self):
7494  """returns set of objective functions"""
7495  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
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
Definition: z3py.py:7492
def param_descrs (   self)
Return the parameter description set.

Definition at line 7349 of file z3py.py.

7350  def param_descrs(self):
7351  """Return the parameter description set."""
7352  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
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 param_descrs
Definition: z3py.py:7349
def pop (   self)
restore to previously created backtracking point

Definition at line 7433 of file z3py.py.

7434  def pop(self):
7435  """restore to previously created backtracking point"""
7436  Z3_optimize_pop(self.ctx.ref(), self.optimize)
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 7429 of file z3py.py.

7430  def push(self):
7431  """create a backtracking point for added rules, facts and assertions"""
7432  Z3_optimize_push(self.ctx.ref(), self.optimize)
def push
Definition: z3py.py:7429
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 7446 of file z3py.py.

7447  def reason_unknown(self):
7448  """Return a string that describes why the last `check()` returned `unknown`."""
7449  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
def reason_unknown
Definition: z3py.py:7446
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 7339 of file z3py.py.

7340  def set(self, *args, **keys):
7341  """Set a configuration option. The method `help()` return a string containing all available options.
7342  """
7343  p = args2params(args, keys, self.ctx)
7344  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
def args2params
Definition: z3py.py:5050
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
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 7500 of file z3py.py.

Referenced by Optimize.__repr__().

7501  def sexpr(self):
7502  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
7503  """
7504  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
def sexpr
Definition: z3py.py:7500
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
def statistics (   self)
Return statistics for the last check`.

Definition at line 7505 of file z3py.py.

7506  def statistics(self):
7507  """Return statistics for the last check`.
7508  """
7509  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
7510 
7511 
7512 
Statistics.
Definition: z3py.py:6235
def statistics
Definition: z3py.py:7505
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 7457 of file z3py.py.

7458  def unsat_core(self):
7459  return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
def unsat_core
Definition: z3py.py:7457
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 7465 of file z3py.py.

7466  def upper(self, obj):
7467  if not isinstance(obj, OptimizeObjective):
7468  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7469  return obj.upper()
def upper
Definition: z3py.py:7465
def upper_values (   self,
  obj 
)

Definition at line 7475 of file z3py.py.

7476  def upper_values(self, obj):
7477  if not isinstance(obj, OptimizeObjective):
7478  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7479  return obj.upper_values()
def upper_values
Definition: z3py.py:7475

Field Documentation

ctx

Definition at line 7328 of file z3py.py.

Referenced by Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Optimize.assert_and_track(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.model(), Optimize.objectives(), Optimize.param_descrs(), Tactic.param_descrs(), Optimize.set(), Tactic.solver(), Optimize.statistics(), and Optimize.unsat_core().

optimize

Definition at line 7329 of file z3py.py.

Referenced by Optimize.__deepcopy__(), Optimize.__del__(), Optimize.add_soft(), Optimize.assert_and_track(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), Optimize.from_file(), Optimize.from_string(), Optimize.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Optimize.param_descrs(), Optimize.pop(), Optimize.push(), Optimize.reason_unknown(), Optimize.set(), Optimize.sexpr(), Optimize.statistics(), and Optimize.unsat_core().