Z3
Public Member Functions | Data Fields
Optimize Class Reference
+ Inheritance diagram for Optimize:

Public Member Functions

def __init__ (self, ctx=None)
 
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 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 6687 of file z3py.py.

Constructor & Destructor Documentation

§ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 6690 of file z3py.py.

6690  def __init__(self, ctx=None):
6691  self.ctx = _get_ctx(ctx)
6692  self.optimize = Z3_mk_optimize(self.ctx.ref())
6693  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
6694 

§ __del__()

def __del__ (   self)

Definition at line 6695 of file z3py.py.

6695  def __del__(self):
6696  if self.optimize is not None and self.ctx.ref() is not None:
6697  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
6698 

Member Function Documentation

§ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6727 of file z3py.py.

6727  def __iadd__(self, fml):
6728  self.add(fml)
6729  return self
6730 

§ __repr__()

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

Definition at line 6807 of file z3py.py.

6807  def __repr__(self):
6808  """Return a formatted string with all added rules and constraints."""
6809  return self.sexpr()
6810 

§ add()

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

Definition at line 6723 of file z3py.py.

Referenced by Optimize.__iadd__().

6723  def add(self, *args):
6724  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
6725  self.assert_exprs(*args)
6726 

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

6731  def add_soft(self, arg, weight = "1", id = None):
6732  """Add soft constraint with optional weight and optional identifier.
6733  If no weight is supplied, then the penalty for violating the soft constraint
6734  is 1.
6735  Soft constraints are grouped by identifiers. Soft constraints that are
6736  added without identifiers are grouped by default.
6737  """
6738  if _is_int(weight):
6739  weight = "%d" % weight
6740  elif isinstance(weight, float):
6741  weight = "%f" % weight
6742  if not isinstance(weight, str):
6743  raise Z3Exception("weight should be a string or an integer")
6744  if id is None:
6745  id = ""
6746  id = to_symbol(id, self.ctx)
6747  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
6748  return OptimizeObjective(self, v, False)
6749 
def to_symbol(s, ctx=None)
Definition: z3py.py:100

§ assert_exprs()

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

Definition at line 6713 of file z3py.py.

Referenced by Optimize.add().

6713  def assert_exprs(self, *args):
6714  """Assert constraints as background axioms for the optimize solver."""
6715  args = _get_args(args)
6716  for arg in args:
6717  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6718  for f in arg:
6719  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
6720  else:
6721  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
6722 

§ assertions()

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

Definition at line 6799 of file z3py.py.

6799  def assertions(self):
6800  """Return an AST vector containing all added constraints."""
6801  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
6802 

§ check()

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

Definition at line 6766 of file z3py.py.

6766  def check(self):
6767  """Check satisfiability while optimizing objective functions."""
6768  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))
6769 

§ from_file()

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

Definition at line 6791 of file z3py.py.

6791  def from_file(self, filename):
6792  """Parse assertions and objectives from a file"""
6793  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
6794 

§ from_string()

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

Definition at line 6795 of file z3py.py.

6795  def from_string(self, s):
6796  """Parse assertions and objectives from a string"""
6797  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
6798 

§ help()

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

Definition at line 6705 of file z3py.py.

6705  def help(self):
6706  """Display a string describing all available options."""
6707  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
6708 

§ lower()

def lower (   self,
  obj 
)

Definition at line 6781 of file z3py.py.

6781  def lower(self, obj):
6782  if not isinstance(obj, OptimizeObjective):
6783  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
6784  return obj.lower()
6785 

§ maximize()

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

Definition at line 6750 of file z3py.py.

6750  def maximize(self, arg):
6751  """Add objective function to maximize."""
6752  return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
6753 

§ minimize()

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

Definition at line 6754 of file z3py.py.

6754  def minimize(self, arg):
6755  """Add objective function to minimize."""
6756  return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
6757 

§ model()

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

Definition at line 6774 of file z3py.py.

6774  def model(self):
6775  """Return a model for the last check()."""
6776  try:
6777  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
6778  except Z3Exception:
6779  raise Z3Exception("model is not available")
6780 

§ objectives()

def objectives (   self)
returns set of objective functions

Definition at line 6803 of file z3py.py.

6803  def objectives(self):
6804  """returns set of objective functions"""
6805  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
6806 

§ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 6709 of file z3py.py.

6709  def param_descrs(self):
6710  """Return the parameter description set."""
6711  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
6712 

§ pop()

def pop (   self)
restore to previously created backtracking point

Definition at line 6762 of file z3py.py.

6762  def pop(self):
6763  """restore to previously created backtracking point"""
6764  Z3_optimize_pop(self.ctx.ref(), self.optimize)
6765 

§ push()

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

Definition at line 6758 of file z3py.py.

6758  def push(self):
6759  """create a backtracking point for added rules, facts and assertions"""
6760  Z3_optimize_push(self.ctx.ref(), self.optimize)
6761 

§ reason_unknown()

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

Definition at line 6770 of file z3py.py.

6770  def reason_unknown(self):
6771  """Return a string that describes why the last `check()` returned `unknown`."""
6772  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
6773 

§ set()

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

Definition at line 6699 of file z3py.py.

6699  def set(self, *args, **keys):
6700  """Set a configuration option. The method `help()` return a string containing all available options.
6701  """
6702  p = args2params(args, keys, self.ctx)
6703  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
6704 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:4644

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

Referenced by Optimize.__repr__().

6811  def sexpr(self):
6812  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6813  """
6814  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
6815 

§ statistics()

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

Definition at line 6816 of file z3py.py.

6816  def statistics(self):
6817  """Return statistics for the last check`.
6818  """
6819  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
6820 
6821 
6822 
6823 

§ upper()

def upper (   self,
  obj 
)

Definition at line 6786 of file z3py.py.

6786  def upper(self, obj):
6787  if not isinstance(obj, OptimizeObjective):
6788  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
6789  return obj.upper()
6790 

Field Documentation

§ ctx

ctx

§ optimize

optimize