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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 7327 of file z3py.py.

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

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

7332  def __deepcopy__(self, memo={}):
7333  return Optimize(self.optimize, self.ctx)
7334 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7369 of file z3py.py.

7369  def __iadd__(self, fml):
7370  self.add(fml)
7371  return self
7372 

◆ __repr__()

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

Definition at line 7496 of file z3py.py.

7496  def __repr__(self):
7497  """Return a formatted string with all added rules and constraints."""
7498  return self.sexpr()
7499 

◆ add()

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__().

7365  def add(self, *args):
7366  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7367  self.assert_exprs(*args)
7368 

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

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

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

◆ assert_exprs()

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().

7353  def assert_exprs(self, *args):
7354  """Assert constraints as background axioms for the optimize solver."""
7355  args = _get_args(args)
7356  s = BoolSort(self.ctx)
7357  for arg in args:
7358  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7359  for f in arg:
7360  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7361  else:
7362  arg = s.cast(arg)
7363  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7364 
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:1523

◆ assertions()

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

Definition at line 7488 of file z3py.py.

7488  def assertions(self):
7489  """Return an AST vector containing all added constraints."""
7490  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
7491 
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 7437 of file z3py.py.

7437  def check(self, *assumptions):
7438  """Check satisfiability while optimizing objective functions."""
7439  assumptions = _get_args(assumptions)
7440  num = len(assumptions)
7441  _assumptions = (Ast * num)()
7442  for i in range(num):
7443  _assumptions[i] = assumptions[i].as_ast()
7444  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7445 
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.

◆ from_file()

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

Definition at line 7480 of file z3py.py.

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

◆ from_string()

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

Definition at line 7484 of file z3py.py.

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

◆ help()

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

Definition at line 7345 of file z3py.py.

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

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

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 7470 of file z3py.py.

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

◆ maximize()

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

Definition at line 7421 of file z3py.py.

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

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

7450  def model(self):
7451  """Return a model for the last check()."""
7452  try:
7453  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7454  except Z3Exception:
7455  raise Z3Exception("model is not available")
7456 
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.

◆ objectives()

def objectives (   self)
returns set of objective functions

Definition at line 7492 of file z3py.py.

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

7349  def param_descrs(self):
7350  """Return the parameter description set."""
7351  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7352 
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 7433 of file z3py.py.

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

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

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

7339  def set(self, *args, **keys):
7340  """Set a configuration option. The method `help()` return a string containing all available options.
7341  """
7342  p = args2params(args, keys, self.ctx)
7343  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7344 
def args2params(arguments, keywords, ctx=None)
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.

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

Referenced by Optimize.__repr__().

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

◆ statistics()

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

Definition at line 7505 of file z3py.py.

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

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

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

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 7475 of file z3py.py.

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

Field Documentation

◆ ctx

ctx

◆ optimize

optimize