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)
 
def reason_unknown (self)
 
def model (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 6971 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 6974 of file z3py.py.

6974  def __init__(self, ctx=None):
6975  self.ctx = _get_ctx(ctx)
6976  self.optimize = Z3_mk_optimize(self.ctx.ref())
6977  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
6978 
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 6982 of file z3py.py.

6982  def __del__(self):
6983  if self.optimize is not None and self.ctx.ref() is not None:
6984  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
6985 
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 6979 of file z3py.py.

6979  def __deepcopy__(self, memo={}):
6980  return Optimize(self.optimize, self.ctx)
6981 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7014 of file z3py.py.

7014  def __iadd__(self, fml):
7015  self.add(fml)
7016  return self
7017 

◆ __repr__()

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

Definition at line 7110 of file z3py.py.

7110  def __repr__(self):
7111  """Return a formatted string with all added rules and constraints."""
7112  return self.sexpr()
7113 

◆ add()

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

Definition at line 7010 of file z3py.py.

Referenced by Optimize.__iadd__().

7010  def add(self, *args):
7011  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7012  self.assert_exprs(*args)
7013 

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

7018  def add_soft(self, arg, weight = "1", id = None):
7019  """Add soft constraint with optional weight and optional identifier.
7020  If no weight is supplied, then the penalty for violating the soft constraint
7021  is 1.
7022  Soft constraints are grouped by identifiers. Soft constraints that are
7023  added without identifiers are grouped by default.
7024  """
7025  if _is_int(weight):
7026  weight = "%d" % weight
7027  elif isinstance(weight, float):
7028  weight = "%f" % weight
7029  if not isinstance(weight, str):
7030  raise Z3Exception("weight should be a string or an integer")
7031  if id is None:
7032  id = ""
7033  id = to_symbol(id, self.ctx)
7034  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
7035  return OptimizeObjective(self, v, False)
7036 
def to_symbol(s, ctx=None)
Definition: z3py.py:101
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 7000 of file z3py.py.

Referenced by Optimize.add().

7000  def assert_exprs(self, *args):
7001  """Assert constraints as background axioms for the optimize solver."""
7002  args = _get_args(args)
7003  for arg in args:
7004  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7005  for f in arg:
7006  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7007  else:
7008  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7009 
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.

◆ assertions()

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

Definition at line 7102 of file z3py.py.

7102  def assertions(self):
7103  """Return an AST vector containing all added constraints."""
7104  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
7105 
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)
Check satisfiability while optimizing objective functions.

Definition at line 7053 of file z3py.py.

7053  def check(self):
7054  """Check satisfiability while optimizing objective functions."""
7055  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))
7056 
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o)
Check consistency and produce optimal values.

◆ from_file()

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

Definition at line 7088 of file z3py.py.

7088  def from_file(self, filename):
7089  """Parse assertions and objectives from a file"""
7090  try:
7091  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
7092  except Z3Exception as e:
7093  _handle_parse_error(e, self.ctx)
7094 
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 7095 of file z3py.py.

7095  def from_string(self, s):
7096  """Parse assertions and objectives from a string"""
7097  try:
7098  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
7099  except Z3Exception as e:
7100  _handle_parse_error(e, self.ctx)
7101 
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 6992 of file z3py.py.

6992  def help(self):
6993  """Display a string describing all available options."""
6994  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
6995 
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 7068 of file z3py.py.

7068  def lower(self, obj):
7069  if not isinstance(obj, OptimizeObjective):
7070  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7071  return obj.lower()
7072 

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 7078 of file z3py.py.

7078  def lower_values(self, obj):
7079  if not isinstance(obj, OptimizeObjective):
7080  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7081  return obj.lower_values()
7082 

◆ maximize()

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

Definition at line 7037 of file z3py.py.

7037  def maximize(self, arg):
7038  """Add objective function to maximize."""
7039  return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
7040 
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 7041 of file z3py.py.

7041  def minimize(self, arg):
7042  """Add objective function to minimize."""
7043  return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
7044 
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 7061 of file z3py.py.

7061  def model(self):
7062  """Return a model for the last check()."""
7063  try:
7064  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7065  except Z3Exception:
7066  raise Z3Exception("model is not available")
7067 
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 7106 of file z3py.py.

7106  def objectives(self):
7107  """returns set of objective functions"""
7108  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
7109 
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 6996 of file z3py.py.

6996  def param_descrs(self):
6997  """Return the parameter description set."""
6998  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
6999 
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 7049 of file z3py.py.

7049  def pop(self):
7050  """restore to previously created backtracking point"""
7051  Z3_optimize_pop(self.ctx.ref(), self.optimize)
7052 
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 7045 of file z3py.py.

7045  def push(self):
7046  """create a backtracking point for added rules, facts and assertions"""
7047  Z3_optimize_push(self.ctx.ref(), self.optimize)
7048 
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 7057 of file z3py.py.

7057  def reason_unknown(self):
7058  """Return a string that describes why the last `check()` returned `unknown`."""
7059  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
7060 
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 6986 of file z3py.py.

6986  def set(self, *args, **keys):
6987  """Set a configuration option. The method `help()` return a string containing all available options.
6988  """
6989  p = args2params(args, keys, self.ctx)
6990  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
6991 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:4766
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 7114 of file z3py.py.

Referenced by Optimize.__repr__().

7114  def sexpr(self):
7115  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
7116  """
7117  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
7118 
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 7119 of file z3py.py.

7119  def statistics(self):
7120  """Return statistics for the last check`.
7121  """
7122  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
7123 
7124 
7125 
7126 
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.

◆ upper()

def upper (   self,
  obj 
)

Definition at line 7073 of file z3py.py.

7073  def upper(self, obj):
7074  if not isinstance(obj, OptimizeObjective):
7075  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7076  return obj.upper()
7077 

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 7083 of file z3py.py.

7083  def upper_values(self, obj):
7084  if not isinstance(obj, OptimizeObjective):
7085  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7086  return obj.upper_values()
7087 

Field Documentation

◆ ctx

ctx

◆ optimize

optimize