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

Public Member Functions

def __init__ (self, ctx=None)
 
def __deepcopy__ (self, memo={})
 
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 (self, arg, weight="1", id=None)
 
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)
 
- 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 7380 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 7383 of file z3py.py.

7383  def __init__(self, ctx=None):
7384  self.ctx = _get_ctx(ctx)
7385  self.optimize = Z3_mk_optimize(self.ctx.ref())
7386  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7387 

◆ __del__()

def __del__ (   self)

Definition at line 7391 of file z3py.py.

7391  def __del__(self):
7392  if self.optimize is not None and self.ctx.ref() is not None:
7393  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7394 

Member Function Documentation

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7388 of file z3py.py.

7388  def __deepcopy__(self, memo={}):
7389  return Optimize(self.optimize, self.ctx)
7390 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7425 of file z3py.py.

7425  def __iadd__(self, fml):
7426  self.add(fml)
7427  return self
7428 

◆ __repr__()

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

Definition at line 7552 of file z3py.py.

7552  def __repr__(self):
7553  """Return a formatted string with all added rules and constraints."""
7554  return self.sexpr()
7555 

◆ add()

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

Definition at line 7421 of file z3py.py.

7421  def add(self, *args):
7422  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7423  self.assert_exprs(*args)
7424 

Referenced by Optimize.__iadd__().

◆ add_soft()

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

7458  def add_soft(self, arg, weight = "1", id = None):
7459  """Add soft constraint with optional weight and optional identifier.
7460  If no weight is supplied, then the penalty for violating the soft constraint
7461  is 1.
7462  Soft constraints are grouped by identifiers. Soft constraints that are
7463  added without identifiers are grouped by default.
7464  """
7465  if _is_int(weight):
7466  weight = "%d" % weight
7467  elif isinstance(weight, float):
7468  weight = "%f" % weight
7469  if not isinstance(weight, str):
7470  raise Z3Exception("weight should be a string or an integer")
7471  if id is None:
7472  id = ""
7473  id = to_symbol(id, self.ctx)
7474  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
7475  return OptimizeObjective(self, v, False)
7476 

◆ assert_and_track()

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

7429  def assert_and_track(self, a, p):
7430  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7431 
7432  If `p` is a string, it will be automatically converted into a Boolean constant.
7433 
7434  >>> x = Int('x')
7435  >>> p3 = Bool('p3')
7436  >>> s = Optimize()
7437  >>> s.assert_and_track(x > 0, 'p1')
7438  >>> s.assert_and_track(x != 1, 'p2')
7439  >>> s.assert_and_track(x < 0, p3)
7440  >>> print(s.check())
7441  unsat
7442  >>> c = s.unsat_core()
7443  >>> len(c)
7444  2
7445  >>> Bool('p1') in c
7446  True
7447  >>> Bool('p2') in c
7448  False
7449  >>> p3 in c
7450  True
7451  """
7452  if isinstance(p, str):
7453  p = Bool(p, self.ctx)
7454  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7455  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7456  Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
7457 

◆ assert_exprs()

def assert_exprs (   self,
args 
)
Assert constraints as background axioms for the optimize solver.

Definition at line 7409 of file z3py.py.

7409  def assert_exprs(self, *args):
7410  """Assert constraints as background axioms for the optimize solver."""
7411  args = _get_args(args)
7412  s = BoolSort(self.ctx)
7413  for arg in args:
7414  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7415  for f in arg:
7416  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7417  else:
7418  arg = s.cast(arg)
7419  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7420 

Referenced by Optimize.add().

◆ assertions()

def assertions (   self)
Return an AST vector containing all added constraints.

Definition at line 7544 of file z3py.py.

7544  def assertions(self):
7545  """Return an AST vector containing all added constraints."""
7546  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
7547 

◆ check()

def check (   self,
assumptions 
)
Check satisfiability while optimizing objective functions.

Definition at line 7493 of file z3py.py.

7493  def check(self, *assumptions):
7494  """Check satisfiability while optimizing objective functions."""
7495  assumptions = _get_args(assumptions)
7496  num = len(assumptions)
7497  _assumptions = (Ast * num)()
7498  for i in range(num):
7499  _assumptions[i] = assumptions[i].as_ast()
7500  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7501 

◆ from_file()

def from_file (   self,
  filename 
)
Parse assertions and objectives from a file

Definition at line 7536 of file z3py.py.

7536  def from_file(self, filename):
7537  """Parse assertions and objectives from a file"""
7538  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
7539 

◆ from_string()

def from_string (   self,
  s 
)
Parse assertions and objectives from a string

Definition at line 7540 of file z3py.py.

7540  def from_string(self, s):
7541  """Parse assertions and objectives from a string"""
7542  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
7543 

◆ help()

def help (   self)
Display a string describing all available options.

Definition at line 7401 of file z3py.py.

7401  def help(self):
7402  """Display a string describing all available options."""
7403  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7404 

◆ lower()

def lower (   self,
  obj 
)

Definition at line 7516 of file z3py.py.

7516  def lower(self, obj):
7517  if not isinstance(obj, OptimizeObjective):
7518  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7519  return obj.lower()
7520 

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 7526 of file z3py.py.

7526  def lower_values(self, obj):
7527  if not isinstance(obj, OptimizeObjective):
7528  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7529  return obj.lower_values()
7530 

◆ maximize()

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

Definition at line 7477 of file z3py.py.

7477  def maximize(self, arg):
7478  """Add objective function to maximize."""
7479  return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
7480 

◆ minimize()

def minimize (   self,
  arg 
)
Add objective function to minimize.

Definition at line 7481 of file z3py.py.

7481  def minimize(self, arg):
7482  """Add objective function to minimize."""
7483  return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
7484 

◆ model()

def model (   self)
Return a model for the last check().

Definition at line 7506 of file z3py.py.

7506  def model(self):
7507  """Return a model for the last check()."""
7508  try:
7509  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7510  except Z3Exception:
7511  raise Z3Exception("model is not available")
7512 

Referenced by FuncInterp.translate().

◆ objectives()

def objectives (   self)
returns set of objective functions

Definition at line 7548 of file z3py.py.

7548  def objectives(self):
7549  """returns set of objective functions"""
7550  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
7551 

◆ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 7405 of file z3py.py.

7405  def param_descrs(self):
7406  """Return the parameter description set."""
7407  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7408 

◆ pop()

def pop (   self)
restore to previously created backtracking point

Definition at line 7489 of file z3py.py.

7489  def pop(self):
7490  """restore to previously created backtracking point"""
7491  Z3_optimize_pop(self.ctx.ref(), self.optimize)
7492 

◆ push()

def push (   self)
create a backtracking point for added rules, facts and assertions

Definition at line 7485 of file z3py.py.

7485  def push(self):
7486  """create a backtracking point for added rules, facts and assertions"""
7487  Z3_optimize_push(self.ctx.ref(), self.optimize)
7488 

◆ reason_unknown()

def reason_unknown (   self)
Return a string that describes why the last `check()` returned `unknown`.

Definition at line 7502 of file z3py.py.

7502  def reason_unknown(self):
7503  """Return a string that describes why the last `check()` returned `unknown`."""
7504  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
7505 

◆ set()

def set (   self,
args,
**  keys 
)
Set a configuration option. The method `help()` return a string containing all available options.

Definition at line 7395 of file z3py.py.

7395  def set(self, *args, **keys):
7396  """Set a configuration option. The method `help()` return a string containing all available options.
7397  """
7398  p = args2params(args, keys, self.ctx)
7399  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7400 

◆ sexpr()

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

7556  def sexpr(self):
7557  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
7558  """
7559  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
7560 

Referenced by Optimize.__repr__().

◆ statistics()

def statistics (   self)
Return statistics for the last check`.

Definition at line 7561 of file z3py.py.

7561  def statistics(self):
7562  """Return statistics for the last check`.
7563  """
7564  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
7565 
7566 
7567 
7568 

◆ unsat_core()

def unsat_core (   self)

Definition at line 7513 of file z3py.py.

7513  def unsat_core(self):
7514  return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
7515 

◆ upper()

def upper (   self,
  obj 
)

Definition at line 7521 of file z3py.py.

7521  def upper(self, obj):
7522  if not isinstance(obj, OptimizeObjective):
7523  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7524  return obj.upper()
7525 

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 7531 of file z3py.py.

7531  def upper_values(self, obj):
7532  if not isinstance(obj, OptimizeObjective):
7533  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7534  return obj.upper_values()
7535 

Field Documentation

◆ ctx

ctx

◆ optimize

optimize
Z3_optimize_pop
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
Z3_optimize_assert_and_track
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.
Z3_optimize_dec_ref
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
Z3_optimize_get_reason_unknown
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.
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3488
Z3_optimize_from_string
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....
Z3_optimize_get_objectives
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...
Z3_optimize_get_statistics
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.
Z3_optimize_get_assertions
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.
Z3_optimize_get_param_descrs
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.
z3py.to_symbol
def to_symbol(s, ctx=None)
Definition: z3py.py:109
Z3_optimize_assert_soft
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.
Z3_optimize_maximize
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
Z3_optimize_to_string
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
z3py.is_const
def is_const(a)
Definition: z3py.py:1182
Z3_optimize_check
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.
Z3_optimize_assert
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
Z3_optimize_from_file
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....
Z3_optimize_set_params
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
Z3_mk_optimize
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
z3py.Bool
def Bool(name, ctx=None)
Definition: z3py.py:1588
Z3_optimize_push
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
Z3_optimize_get_unsat_core
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 ...
Z3_optimize_get_model
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
z3py.args2params
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5093
z3py.BoolSort
def BoolSort(ctx=None)
Definition: z3py.py:1553
Z3_optimize_get_help
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.
Z3_optimize_minimize
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
Z3_optimize_inc_ref
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.