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

Constructor & Destructor Documentation

§ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 6906 of file z3py.py.

6906  def __init__(self, ctx=None):
6907  self.ctx = _get_ctx(ctx)
6908  self.optimize = Z3_mk_optimize(self.ctx.ref())
6909  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
6910 
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 6914 of file z3py.py.

6914  def __del__(self):
6915  if self.optimize is not None and self.ctx.ref() is not None:
6916  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
6917 
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 6911 of file z3py.py.

6911  def __deepcopy__(self, memo={}):
6912  return Optimize(self.optimize, self.ctx)
6913 

§ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6946 of file z3py.py.

6946  def __iadd__(self, fml):
6947  self.add(fml)
6948  return self
6949 

§ __repr__()

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

Definition at line 7042 of file z3py.py.

7042  def __repr__(self):
7043  """Return a formatted string with all added rules and constraints."""
7044  return self.sexpr()
7045 

§ add()

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

Definition at line 6942 of file z3py.py.

Referenced by Optimize.__iadd__().

6942  def add(self, *args):
6943  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
6944  self.assert_exprs(*args)
6945 

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

6950  def add_soft(self, arg, weight = "1", id = None):
6951  """Add soft constraint with optional weight and optional identifier.
6952  If no weight is supplied, then the penalty for violating the soft constraint
6953  is 1.
6954  Soft constraints are grouped by identifiers. Soft constraints that are
6955  added without identifiers are grouped by default.
6956  """
6957  if _is_int(weight):
6958  weight = "%d" % weight
6959  elif isinstance(weight, float):
6960  weight = "%f" % weight
6961  if not isinstance(weight, str):
6962  raise Z3Exception("weight should be a string or an integer")
6963  if id is None:
6964  id = ""
6965  id = to_symbol(id, self.ctx)
6966  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
6967  return OptimizeObjective(self, v, False)
6968 
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 6932 of file z3py.py.

Referenced by Optimize.add().

6932  def assert_exprs(self, *args):
6933  """Assert constraints as background axioms for the optimize solver."""
6934  args = _get_args(args)
6935  for arg in args:
6936  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6937  for f in arg:
6938  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
6939  else:
6940  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
6941 
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 7034 of file z3py.py.

7034  def assertions(self):
7035  """Return an AST vector containing all added constraints."""
7036  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
7037 
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 6985 of file z3py.py.

6985  def check(self):
6986  """Check satisfiability while optimizing objective functions."""
6987  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))
6988 
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 7020 of file z3py.py.

7020  def from_file(self, filename):
7021  """Parse assertions and objectives from a file"""
7022  try:
7023  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
7024  except Z3Exception as e:
7025  _handle_parse_error(e, self.ctx)
7026 
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 7027 of file z3py.py.

7027  def from_string(self, s):
7028  """Parse assertions and objectives from a string"""
7029  try:
7030  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
7031  except Z3Exception as e:
7032  _handle_parse_error(e, self.ctx)
7033 
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 6924 of file z3py.py.

6924  def help(self):
6925  """Display a string describing all available options."""
6926  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
6927 
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 7000 of file z3py.py.

7000  def lower(self, obj):
7001  if not isinstance(obj, OptimizeObjective):
7002  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7003  return obj.lower()
7004 

§ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 7010 of file z3py.py.

7010  def lower_values(self, obj):
7011  if not isinstance(obj, OptimizeObjective):
7012  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7013  return obj.lower_values()
7014 

§ maximize()

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

Definition at line 6969 of file z3py.py.

6969  def maximize(self, arg):
6970  """Add objective function to maximize."""
6971  return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
6972 
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 6973 of file z3py.py.

6973  def minimize(self, arg):
6974  """Add objective function to minimize."""
6975  return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
6976 
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 6993 of file z3py.py.

6993  def model(self):
6994  """Return a model for the last check()."""
6995  try:
6996  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
6997  except Z3Exception:
6998  raise Z3Exception("model is not available")
6999 
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 7038 of file z3py.py.

7038  def objectives(self):
7039  """returns set of objective functions"""
7040  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
7041 
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 6928 of file z3py.py.

6928  def param_descrs(self):
6929  """Return the parameter description set."""
6930  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
6931 
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 6981 of file z3py.py.

6981  def pop(self):
6982  """restore to previously created backtracking point"""
6983  Z3_optimize_pop(self.ctx.ref(), self.optimize)
6984 
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 6977 of file z3py.py.

6977  def push(self):
6978  """create a backtracking point for added rules, facts and assertions"""
6979  Z3_optimize_push(self.ctx.ref(), self.optimize)
6980 
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 6989 of file z3py.py.

6989  def reason_unknown(self):
6990  """Return a string that describes why the last `check()` returned `unknown`."""
6991  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
6992 
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 6918 of file z3py.py.

6918  def set(self, *args, **keys):
6919  """Set a configuration option. The method `help()` return a string containing all available options.
6920  """
6921  p = args2params(args, keys, self.ctx)
6922  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
6923 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:4744
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 7046 of file z3py.py.

Referenced by Optimize.__repr__().

7046  def sexpr(self):
7047  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
7048  """
7049  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
7050 
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 7051 of file z3py.py.

7051  def statistics(self):
7052  """Return statistics for the last check`.
7053  """
7054  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
7055 
7056 
7057 
7058 
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 7005 of file z3py.py.

7005  def upper(self, obj):
7006  if not isinstance(obj, OptimizeObjective):
7007  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7008  return obj.upper()
7009 

§ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 7015 of file z3py.py.

7015  def upper_values(self, obj):
7016  if not isinstance(obj, OptimizeObjective):
7017  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7018  return obj.upper_values()
7019 

Field Documentation

§ ctx

ctx

§ optimize

optimize