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

Constructor & Destructor Documentation

def __init__ (   self,
  ctx = None 
)

Definition at line 6423 of file z3py.py.

6423  def __init__(self, ctx=None):
6424  self.ctx = _get_ctx(ctx)
6425  self.optimize = Z3_mk_optimize(self.ctx.ref())
6426  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
6427 
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
def __init__(self, ctx=None)
Definition: z3py.py:6423
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
def __del__ (   self)

Definition at line 6428 of file z3py.py.

6428  def __del__(self):
6429  if self.optimize != None:
6430  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
6431 
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
def __del__(self)
Definition: z3py.py:6428

Member Function Documentation

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

Definition at line 6518 of file z3py.py.

6518  def __repr__(self):
6519  """Return a formatted string with all added rules and constraints."""
6520  return self.sexpr()
6521 
def __repr__(self)
Definition: z3py.py:6518
def sexpr(self)
Definition: z3py.py:6522
def add (   self,
  args 
)
Assert constraints as background axioms for the optimize solver. Alias for assert_expr.

Definition at line 6456 of file z3py.py.

6456  def add(self, *args):
6457  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
6458  self.assert_exprs(*args)
6459 
def add(self, args)
Definition: z3py.py:6456
def assert_exprs(self, args)
Definition: z3py.py:6446
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 6460 of file z3py.py.

6460  def add_soft(self, arg, weight = "1", id = None):
6461  """Add soft constraint with optional weight and optional identifier.
6462  If no weight is supplied, then the penalty for violating the soft constraint
6463  is 1.
6464  Soft constraints are grouped by identifiers. Soft constraints that are
6465  added without identifiers are grouped by default.
6466  """
6467  if _is_int(weight):
6468  weight = "%d" % weight
6469  if not isinstance(weight, str):
6470  raise Z3Exception("weight should be a string or an integer")
6471  if id == None:
6472  id = ""
6473  id = to_symbol(id, self.ctx)
6474  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
6475  return OptimizeObjective(self, v, False)
6476 
def to_symbol(s, ctx=None)
Definition: z3py.py:94
def add_soft(self, arg, weight="1", id=None)
Definition: z3py.py:6460
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.
def assert_exprs (   self,
  args 
)
Assert constraints as background axioms for the optimize solver.

Definition at line 6446 of file z3py.py.

Referenced by Optimize.add().

6446  def assert_exprs(self, *args):
6447  """Assert constraints as background axioms for the optimize solver."""
6448  args = _get_args(args)
6449  for arg in args:
6450  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6451  for f in arg:
6452  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
6453  else:
6454  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
6455 
def assert_exprs(self, args)
Definition: z3py.py:6446
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
def check (   self)
Check satisfiability while optimizing objective functions.

Definition at line 6493 of file z3py.py.

6493  def check(self):
6494  """Check satisfiability while optimizing objective functions."""
6495  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))
6496 
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o)
Check consistency and produce optimal values.
def check(self)
Definition: z3py.py:6493
def help (   self)
Display a string describing all available options.

Definition at line 6438 of file z3py.py.

6438  def help(self):
6439  """Display a string describing all available options."""
6440  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
6441 
def help(self)
Definition: z3py.py:6438
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.
def lower (   self,
  obj 
)

Definition at line 6508 of file z3py.py.

6508  def lower(self, obj):
6509  if not isinstance(obj, OptimizeObjective):
6510  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
6511  return obj.lower()
6512 
def lower(self, obj)
Definition: z3py.py:6508
def maximize (   self,
  arg 
)
Add objective function to maximize.

Definition at line 6477 of file z3py.py.

6477  def maximize(self, arg):
6478  """Add objective function to maximize."""
6479  return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
6480 
def maximize(self, arg)
Definition: z3py.py:6477
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
def minimize (   self,
  arg 
)
Add objective function to minimize.

Definition at line 6481 of file z3py.py.

6481  def minimize(self, arg):
6482  """Add objective function to minimize."""
6483  return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
6484 
def minimize(self, arg)
Definition: z3py.py:6481
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
def model (   self)
Return a model for the last check().

Definition at line 6501 of file z3py.py.

6501  def model(self):
6502  """Return a model for the last check()."""
6503  try:
6504  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
6505  except Z3Exception:
6506  raise Z3Exception("model is not available")
6507 
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
def model(self)
Definition: z3py.py:6501
def param_descrs (   self)
Return the parameter description set.

Definition at line 6442 of file z3py.py.

6442  def param_descrs(self):
6443  """Return the parameter description set."""
6444  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
6445 
def param_descrs(self)
Definition: z3py.py:6442
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.
def pop (   self)
restore to previously created backtracking point

Definition at line 6489 of file z3py.py.

6489  def pop(self):
6490  """restore to previously created backtracking point"""
6491  Z3_optimize_pop(self.ctx.ref(), self.optimize)
6492 
def pop(self)
Definition: z3py.py:6489
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
def push (   self)
create a backtracking point for added rules, facts and assertions

Definition at line 6485 of file z3py.py.

6485  def push(self):
6486  """create a backtracking point for added rules, facts and assertions"""
6487  Z3_optimize_push(self.ctx.ref(), self.optimize)
6488 
def push(self)
Definition: z3py.py:6485
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
def reason_unknown (   self)
Return a string that describes why the last `check()` returned `unknown`.

Definition at line 6497 of file z3py.py.

6497  def reason_unknown(self):
6498  """Return a string that describes why the last `check()` returned `unknown`."""
6499  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
6500 
def reason_unknown(self)
Definition: z3py.py:6497
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.
def set (   self,
  args,
  keys 
)
Set a configuration option. The method `help()` return a string containing all available options.        

Definition at line 6432 of file z3py.py.

6432  def set(self, *args, **keys):
6433  """Set a configuration option. The method `help()` return a string containing all available options.
6434  """
6435  p = args2params(args, keys, self.ctx)
6436  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
6437 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:4527
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
def set(self, args, keys)
Definition: z3py.py:6432
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 6522 of file z3py.py.

Referenced by Optimize.__repr__().

6522  def sexpr(self):
6523  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6524  """
6525  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
6526 
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
def sexpr(self)
Definition: z3py.py:6522
def statistics (   self)
Return statistics for the last `query()`.

Definition at line 6527 of file z3py.py.

6527  def statistics(self):
6528  """Return statistics for the last `query()`.
6529  """
6530  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
6531 
6532 
6533 
6534 
Statistics.
Definition: z3py.py:5604
def statistics(self)
Definition: z3py.py:6527
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.
def upper (   self,
  obj 
)

Definition at line 6513 of file z3py.py.

6513  def upper(self, obj):
6514  if not isinstance(obj, OptimizeObjective):
6515  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
6516  return obj.upper()
6517 
def upper(self, obj)
Definition: z3py.py:6513

Field Documentation

ctx
optimize