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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 7402 of file z3py.py.

7402  def __init__(self, ctx=None):
7403  self.ctx = _get_ctx(ctx)
7404  self.optimize = Z3_mk_optimize(self.ctx.ref())
7405  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7406 

◆ __del__()

def __del__ (   self)

Definition at line 7410 of file z3py.py.

7410  def __del__(self):
7411  if self.optimize is not None and self.ctx.ref() is not None:
7412  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7413 

Member Function Documentation

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7407 of file z3py.py.

7407  def __deepcopy__(self, memo={}):
7408  return Optimize(self.optimize, self.ctx)
7409 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7444 of file z3py.py.

7444  def __iadd__(self, fml):
7445  self.add(fml)
7446  return self
7447 

◆ __repr__()

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

Definition at line 7571 of file z3py.py.

7571  def __repr__(self):
7572  """Return a formatted string with all added rules and constraints."""
7573  return self.sexpr()
7574 

◆ add()

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

Definition at line 7440 of file z3py.py.

7440  def add(self, *args):
7441  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7442  self.assert_exprs(*args)
7443 

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

7477  def add_soft(self, arg, weight = "1", id = None):
7478  """Add soft constraint with optional weight and optional identifier.
7479  If no weight is supplied, then the penalty for violating the soft constraint
7480  is 1.
7481  Soft constraints are grouped by identifiers. Soft constraints that are
7482  added without identifiers are grouped by default.
7483  """
7484  if _is_int(weight):
7485  weight = "%d" % weight
7486  elif isinstance(weight, float):
7487  weight = "%f" % weight
7488  if not isinstance(weight, str):
7489  raise Z3Exception("weight should be a string or an integer")
7490  if id is None:
7491  id = ""
7492  id = to_symbol(id, self.ctx)
7493  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
7494  return OptimizeObjective(self, v, False)
7495 

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

7448  def assert_and_track(self, a, p):
7449  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7450 
7451  If `p` is a string, it will be automatically converted into a Boolean constant.
7452 
7453  >>> x = Int('x')
7454  >>> p3 = Bool('p3')
7455  >>> s = Optimize()
7456  >>> s.assert_and_track(x > 0, 'p1')
7457  >>> s.assert_and_track(x != 1, 'p2')
7458  >>> s.assert_and_track(x < 0, p3)
7459  >>> print(s.check())
7460  unsat
7461  >>> c = s.unsat_core()
7462  >>> len(c)
7463  2
7464  >>> Bool('p1') in c
7465  True
7466  >>> Bool('p2') in c
7467  False
7468  >>> p3 in c
7469  True
7470  """
7471  if isinstance(p, str):
7472  p = Bool(p, self.ctx)
7473  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7474  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7475  Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
7476 

◆ assert_exprs()

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

Definition at line 7428 of file z3py.py.

7428  def assert_exprs(self, *args):
7429  """Assert constraints as background axioms for the optimize solver."""
7430  args = _get_args(args)
7431  s = BoolSort(self.ctx)
7432  for arg in args:
7433  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7434  for f in arg:
7435  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7436  else:
7437  arg = s.cast(arg)
7438  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7439 

Referenced by Optimize.add().

◆ assertions()

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

Definition at line 7563 of file z3py.py.

7563  def assertions(self):
7564  """Return an AST vector containing all added constraints."""
7565  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
7566 

◆ check()

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

Definition at line 7512 of file z3py.py.

7512  def check(self, *assumptions):
7513  """Check satisfiability while optimizing objective functions."""
7514  assumptions = _get_args(assumptions)
7515  num = len(assumptions)
7516  _assumptions = (Ast * num)()
7517  for i in range(num):
7518  _assumptions[i] = assumptions[i].as_ast()
7519  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7520 

◆ from_file()

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

Definition at line 7555 of file z3py.py.

7555  def from_file(self, filename):
7556  """Parse assertions and objectives from a file"""
7557  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
7558 

◆ from_string()

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

Definition at line 7559 of file z3py.py.

7559  def from_string(self, s):
7560  """Parse assertions and objectives from a string"""
7561  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
7562 

◆ help()

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

Definition at line 7420 of file z3py.py.

7420  def help(self):
7421  """Display a string describing all available options."""
7422  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7423 

◆ lower()

def lower (   self,
  obj 
)

Definition at line 7535 of file z3py.py.

7535  def lower(self, obj):
7536  if not isinstance(obj, OptimizeObjective):
7537  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7538  return obj.lower()
7539 

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 7545 of file z3py.py.

7545  def lower_values(self, obj):
7546  if not isinstance(obj, OptimizeObjective):
7547  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7548  return obj.lower_values()
7549 

◆ maximize()

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

Definition at line 7496 of file z3py.py.

7496  def maximize(self, arg):
7497  """Add objective function to maximize."""
7498  return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
7499 

◆ minimize()

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

Definition at line 7500 of file z3py.py.

7500  def minimize(self, arg):
7501  """Add objective function to minimize."""
7502  return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
7503 

◆ model()

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

Definition at line 7525 of file z3py.py.

7525  def model(self):
7526  """Return a model for the last check()."""
7527  try:
7528  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7529  except Z3Exception:
7530  raise Z3Exception("model is not available")
7531 

Referenced by FuncInterp.translate().

◆ objectives()

def objectives (   self)
returns set of objective functions

Definition at line 7567 of file z3py.py.

7567  def objectives(self):
7568  """returns set of objective functions"""
7569  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
7570 

◆ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 7424 of file z3py.py.

7424  def param_descrs(self):
7425  """Return the parameter description set."""
7426  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7427 

◆ pop()

def pop (   self)
restore to previously created backtracking point

Definition at line 7508 of file z3py.py.

7508  def pop(self):
7509  """restore to previously created backtracking point"""
7510  Z3_optimize_pop(self.ctx.ref(), self.optimize)
7511 

◆ push()

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

Definition at line 7504 of file z3py.py.

7504  def push(self):
7505  """create a backtracking point for added rules, facts and assertions"""
7506  Z3_optimize_push(self.ctx.ref(), self.optimize)
7507 

◆ reason_unknown()

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

Definition at line 7521 of file z3py.py.

7521  def reason_unknown(self):
7522  """Return a string that describes why the last `check()` returned `unknown`."""
7523  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
7524 

◆ set()

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

Definition at line 7414 of file z3py.py.

7414  def set(self, *args, **keys):
7415  """Set a configuration option. The method `help()` return a string containing all available options.
7416  """
7417  p = args2params(args, keys, self.ctx)
7418  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7419 

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

7575  def sexpr(self):
7576  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
7577  """
7578  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
7579 

Referenced by Optimize.__repr__().

◆ statistics()

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

Definition at line 7580 of file z3py.py.

7580  def statistics(self):
7581  """Return statistics for the last check`.
7582  """
7583  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
7584 
7585 
7586 
7587 

◆ unsat_core()

def unsat_core (   self)

Definition at line 7532 of file z3py.py.

7532  def unsat_core(self):
7533  return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
7534 

◆ upper()

def upper (   self,
  obj 
)

Definition at line 7540 of file z3py.py.

7540  def upper(self, obj):
7541  if not isinstance(obj, OptimizeObjective):
7542  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7543  return obj.upper()
7544 

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 7550 of file z3py.py.

7550  def upper_values(self, obj):
7551  if not isinstance(obj, OptimizeObjective):
7552  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7553  return obj.upper_values()
7554 

Field Documentation

◆ ctx

ctx

◆ optimize

optimize
Z3_optimize_pop
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
z3py.UserPropagateBase.__init__
def __init__(self, s, ctx=None)
Definition: z3py.py:10582
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:3515
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.UserPropagateBase.pop
def pop(self, num_scopes)
Definition: z3py.py:10647
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.UserPropagateBase.push
def push(self)
Definition: z3py.py:10644
z3py.UserPropagateBase.__del__
def __del__(self)
Definition: z3py.py:10607
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.UserPropagateBase.add
def add(self, e)
Definition: z3py.py:10653
z3py.args2params
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5111
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.