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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 7362 of file z3py.py.

7362  def __init__(self, ctx=None):
7363  self.ctx = _get_ctx(ctx)
7364  self.optimize = Z3_mk_optimize(self.ctx.ref())
7365  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7366 
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.

◆ __del__()

def __del__ (   self)

Definition at line 7370 of file z3py.py.

7370  def __del__(self):
7371  if self.optimize is not None and self.ctx.ref() is not None:
7372  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7373 
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

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7367 of file z3py.py.

7367  def __deepcopy__(self, memo={}):
7368  return Optimize(self.optimize, self.ctx)
7369 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7404 of file z3py.py.

7404  def __iadd__(self, fml):
7405  self.add(fml)
7406  return self
7407 

◆ __repr__()

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

Definition at line 7531 of file z3py.py.

7531  def __repr__(self):
7532  """Return a formatted string with all added rules and constraints."""
7533  return self.sexpr()
7534 

◆ add()

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

Definition at line 7400 of file z3py.py.

7400  def add(self, *args):
7401  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7402  self.assert_exprs(*args)
7403 

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

7437  def add_soft(self, arg, weight = "1", id = None):
7438  """Add soft constraint with optional weight and optional identifier.
7439  If no weight is supplied, then the penalty for violating the soft constraint
7440  is 1.
7441  Soft constraints are grouped by identifiers. Soft constraints that are
7442  added without identifiers are grouped by default.
7443  """
7444  if _is_int(weight):
7445  weight = "%d" % weight
7446  elif isinstance(weight, float):
7447  weight = "%f" % weight
7448  if not isinstance(weight, str):
7449  raise Z3Exception("weight should be a string or an integer")
7450  if id is None:
7451  id = ""
7452  id = to_symbol(id, self.ctx)
7453  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
7454  return OptimizeObjective(self, v, False)
7455 
def to_symbol(s, ctx=None)
Definition: z3py.py:111
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.

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

7408  def assert_and_track(self, a, p):
7409  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7410 
7411  If `p` is a string, it will be automatically converted into a Boolean constant.
7412 
7413  >>> x = Int('x')
7414  >>> p3 = Bool('p3')
7415  >>> s = Optimize()
7416  >>> s.assert_and_track(x > 0, 'p1')
7417  >>> s.assert_and_track(x != 1, 'p2')
7418  >>> s.assert_and_track(x < 0, p3)
7419  >>> print(s.check())
7420  unsat
7421  >>> c = s.unsat_core()
7422  >>> len(c)
7423  2
7424  >>> Bool('p1') in c
7425  True
7426  >>> Bool('p2') in c
7427  False
7428  >>> p3 in c
7429  True
7430  """
7431  if isinstance(p, str):
7432  p = Bool(p, self.ctx)
7433  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7434  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7435  Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
7436 
def is_const(a)
Definition: z3py.py:1164
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 Bool(name, ctx=None)
Definition: z3py.py:1570

◆ assert_exprs()

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

Definition at line 7388 of file z3py.py.

7388  def assert_exprs(self, *args):
7389  """Assert constraints as background axioms for the optimize solver."""
7390  args = _get_args(args)
7391  s = BoolSort(self.ctx)
7392  for arg in args:
7393  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7394  for f in arg:
7395  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7396  else:
7397  arg = s.cast(arg)
7398  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7399 
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
def BoolSort(ctx=None)
Definition: z3py.py:1535

Referenced by Optimize.add().

◆ assertions()

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

Definition at line 7523 of file z3py.py.

7523  def assertions(self):
7524  """Return an AST vector containing all added constraints."""
7525  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
7526 
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.

◆ check()

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

Definition at line 7472 of file z3py.py.

7472  def check(self, *assumptions):
7473  """Check satisfiability while optimizing objective functions."""
7474  assumptions = _get_args(assumptions)
7475  num = len(assumptions)
7476  _assumptions = (Ast * num)()
7477  for i in range(num):
7478  _assumptions[i] = assumptions[i].as_ast()
7479  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7480 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3370
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.

◆ from_file()

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

Definition at line 7515 of file z3py.py.

7515  def from_file(self, filename):
7516  """Parse assertions and objectives from a file"""
7517  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
7518 
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....

◆ from_string()

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

Definition at line 7519 of file z3py.py.

7519  def from_string(self, s):
7520  """Parse assertions and objectives from a string"""
7521  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
7522 
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....

◆ help()

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

Definition at line 7380 of file z3py.py.

7380  def help(self):
7381  """Display a string describing all available options."""
7382  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7383 
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.

◆ lower()

def lower (   self,
  obj 
)

Definition at line 7495 of file z3py.py.

7495  def lower(self, obj):
7496  if not isinstance(obj, OptimizeObjective):
7497  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7498  return obj.lower()
7499 

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 7505 of file z3py.py.

7505  def lower_values(self, obj):
7506  if not isinstance(obj, OptimizeObjective):
7507  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7508  return obj.lower_values()
7509 

◆ maximize()

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

Definition at line 7456 of file z3py.py.

7456  def maximize(self, arg):
7457  """Add objective function to maximize."""
7458  return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
7459 
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.

◆ minimize()

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

Definition at line 7460 of file z3py.py.

7460  def minimize(self, arg):
7461  """Add objective function to minimize."""
7462  return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
7463 
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.

◆ model()

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

Definition at line 7485 of file z3py.py.

7485  def model(self):
7486  """Return a model for the last check()."""
7487  try:
7488  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7489  except Z3Exception:
7490  raise Z3Exception("model is not available")
7491 
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.

Referenced by FuncInterp.translate().

◆ objectives()

def objectives (   self)
returns set of objective functions

Definition at line 7527 of file z3py.py.

7527  def objectives(self):
7528  """returns set of objective functions"""
7529  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
7530 
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...

◆ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 7384 of file z3py.py.

7384  def param_descrs(self):
7385  """Return the parameter description set."""
7386  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7387 
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.

◆ pop()

def pop (   self)
restore to previously created backtracking point

Definition at line 7468 of file z3py.py.

7468  def pop(self):
7469  """restore to previously created backtracking point"""
7470  Z3_optimize_pop(self.ctx.ref(), self.optimize)
7471 
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.

◆ push()

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

Definition at line 7464 of file z3py.py.

7464  def push(self):
7465  """create a backtracking point for added rules, facts and assertions"""
7466  Z3_optimize_push(self.ctx.ref(), self.optimize)
7467 
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.

◆ reason_unknown()

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

Definition at line 7481 of file z3py.py.

7481  def reason_unknown(self):
7482  """Return a string that describes why the last `check()` returned `unknown`."""
7483  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
7484 
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.

◆ set()

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

Definition at line 7374 of file z3py.py.

7374  def set(self, *args, **keys):
7375  """Set a configuration option. The method `help()` return a string containing all available options.
7376  """
7377  p = args2params(args, keys, self.ctx)
7378  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7379 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5074
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.

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

7535  def sexpr(self):
7536  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
7537  """
7538  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
7539 
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.

Referenced by Optimize.__repr__().

◆ statistics()

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

Definition at line 7540 of file z3py.py.

7540  def statistics(self):
7541  """Return statistics for the last check`.
7542  """
7543  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
7544 
7545 
7546 
7547 
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.

◆ unsat_core()

def unsat_core (   self)

Definition at line 7492 of file z3py.py.

7492  def unsat_core(self):
7493  return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
7494 
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 ...

◆ upper()

def upper (   self,
  obj 
)

Definition at line 7500 of file z3py.py.

7500  def upper(self, obj):
7501  if not isinstance(obj, OptimizeObjective):
7502  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7503  return obj.upper()
7504 

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 7510 of file z3py.py.

7510  def upper_values(self, obj):
7511  if not isinstance(obj, OptimizeObjective):
7512  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7513  return obj.upper_values()
7514 

Field Documentation

◆ ctx

ctx

◆ optimize

optimize