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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 7287 of file z3py.py.

7287  def __init__(self, ctx=None):
7288  self.ctx = _get_ctx(ctx)
7289  self.optimize = Z3_mk_optimize(self.ctx.ref())
7290  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7291 
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 7295 of file z3py.py.

7295  def __del__(self):
7296  if self.optimize is not None and self.ctx.ref() is not None:
7297  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7298 
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 7292 of file z3py.py.

7292  def __deepcopy__(self, memo={}):
7293  return Optimize(self.optimize, self.ctx)
7294 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7329 of file z3py.py.

7329  def __iadd__(self, fml):
7330  self.add(fml)
7331  return self
7332 

◆ __repr__()

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

Definition at line 7433 of file z3py.py.

7433  def __repr__(self):
7434  """Return a formatted string with all added rules and constraints."""
7435  return self.sexpr()
7436 

◆ add()

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

Definition at line 7325 of file z3py.py.

Referenced by Optimize.__iadd__().

7325  def add(self, *args):
7326  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7327  self.assert_exprs(*args)
7328 

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

7333  def add_soft(self, arg, weight = "1", id = None):
7334  """Add soft constraint with optional weight and optional identifier.
7335  If no weight is supplied, then the penalty for violating the soft constraint
7336  is 1.
7337  Soft constraints are grouped by identifiers. Soft constraints that are
7338  added without identifiers are grouped by default.
7339  """
7340  if _is_int(weight):
7341  weight = "%d" % weight
7342  elif isinstance(weight, float):
7343  weight = "%f" % weight
7344  if not isinstance(weight, str):
7345  raise Z3Exception("weight should be a string or an integer")
7346  if id is None:
7347  id = ""
7348  id = to_symbol(id, self.ctx)
7349  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
7350  return OptimizeObjective(self, v, False)
7351 
def to_symbol(s, ctx=None)
Definition: z3py.py:105
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_exprs()

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

Definition at line 7313 of file z3py.py.

Referenced by Optimize.add().

7313  def assert_exprs(self, *args):
7314  """Assert constraints as background axioms for the optimize solver."""
7315  args = _get_args(args)
7316  s = BoolSort(self.ctx)
7317  for arg in args:
7318  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7319  for f in arg:
7320  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7321  else:
7322  arg = s.cast(arg)
7323  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7324 
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:1512

◆ assertions()

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

Definition at line 7425 of file z3py.py.

7425  def assertions(self):
7426  """Return an AST vector containing all added constraints."""
7427  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
7428 
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 7368 of file z3py.py.

7368  def check(self, *assumptions):
7369  """Check satisfiability while optimizing objective functions."""
7370  assumptions = _get_args(assumptions)
7371  num = len(assumptions)
7372  _assumptions = (Ast * num)()
7373  for i in range(num):
7374  _assumptions[i] = assumptions[i].as_ast()
7375  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7376 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
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 7411 of file z3py.py.

7411  def from_file(self, filename):
7412  """Parse assertions and objectives from a file"""
7413  try:
7414  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
7415  except Z3Exception as e:
7416  _handle_parse_error(e, self.ctx)
7417 
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 7418 of file z3py.py.

7418  def from_string(self, s):
7419  """Parse assertions and objectives from a string"""
7420  try:
7421  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
7422  except Z3Exception as e:
7423  _handle_parse_error(e, self.ctx)
7424 
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 7305 of file z3py.py.

7305  def help(self):
7306  """Display a string describing all available options."""
7307  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7308 
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 7391 of file z3py.py.

7391  def lower(self, obj):
7392  if not isinstance(obj, OptimizeObjective):
7393  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7394  return obj.lower()
7395 

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 7401 of file z3py.py.

7401  def lower_values(self, obj):
7402  if not isinstance(obj, OptimizeObjective):
7403  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7404  return obj.lower_values()
7405 

◆ maximize()

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

Definition at line 7352 of file z3py.py.

7352  def maximize(self, arg):
7353  """Add objective function to maximize."""
7354  return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
7355 
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 7356 of file z3py.py.

7356  def minimize(self, arg):
7357  """Add objective function to minimize."""
7358  return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
7359 
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 7381 of file z3py.py.

7381  def model(self):
7382  """Return a model for the last check()."""
7383  try:
7384  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7385  except Z3Exception:
7386  raise Z3Exception("model is not available")
7387 
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 7429 of file z3py.py.

7429  def objectives(self):
7430  """returns set of objective functions"""
7431  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
7432 
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 7309 of file z3py.py.

7309  def param_descrs(self):
7310  """Return the parameter description set."""
7311  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7312 
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 7364 of file z3py.py.

7364  def pop(self):
7365  """restore to previously created backtracking point"""
7366  Z3_optimize_pop(self.ctx.ref(), self.optimize)
7367 
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 7360 of file z3py.py.

7360  def push(self):
7361  """create a backtracking point for added rules, facts and assertions"""
7362  Z3_optimize_push(self.ctx.ref(), self.optimize)
7363 
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 7377 of file z3py.py.

7377  def reason_unknown(self):
7378  """Return a string that describes why the last `check()` returned `unknown`."""
7379  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
7380 
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 7299 of file z3py.py.

7299  def set(self, *args, **keys):
7300  """Set a configuration option. The method `help()` return a string containing all available options.
7301  """
7302  p = args2params(args, keys, self.ctx)
7303  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7304 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5007
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 7437 of file z3py.py.

Referenced by Optimize.__repr__().

7437  def sexpr(self):
7438  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
7439  """
7440  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
7441 
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 7442 of file z3py.py.

7442  def statistics(self):
7443  """Return statistics for the last check`.
7444  """
7445  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
7446 
7447 
7448 
7449 
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 7388 of file z3py.py.

7388  def unsat_core(self):
7389  return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
7390 
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 7396 of file z3py.py.

7396  def upper(self, obj):
7397  if not isinstance(obj, OptimizeObjective):
7398  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7399  return obj.upper()
7400 

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 7406 of file z3py.py.

7406  def upper_values(self, obj):
7407  if not isinstance(obj, OptimizeObjective):
7408  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7409  return obj.upper_values()
7410 

Field Documentation

◆ ctx

ctx

◆ optimize

optimize