Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions | Data Fields
Optimize Class Reference
+ Inheritance diagram for Optimize:

Public Member Functions

def __init__
 
def __del__
 
def set
 
def help
 
def param_descrs
 
def assert_exprs
 
def add
 
def add_soft
 
def maximize
 
def minimize
 
def push
 
def pop
 
def check
 
def reason_unknown
 
def model
 
def lower
 
def upper
 
def __repr__
 
def sexpr
 
def statistics
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

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

Definition at line 6428 of file z3py.py.

6428 
6429  def __del__(self):
6430  if self.optimize != None:
6431  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
z3py.Optimize.__del__
def __del__
Definition: z3py.py:6428
Z3_optimize_dec_ref
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

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

Definition at line 6518 of file z3py.py.

6518 
6519  def __repr__(self):
6520  """Return a formatted string with all added rules and constraints."""
6521  return self.sexpr()
z3py.Optimize.sexpr
def sexpr
Definition: z3py.py:6522
z3py.Optimize.__repr__
def __repr__
Definition: z3py.py:6518
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 
6457  def add(self, *args):
6458  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
6459  self.assert_exprs(*args)
z3py.Optimize.assert_exprs
def assert_exprs
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 
6461  def add_soft(self, arg, weight = "1", id = None):
6462  """Add soft constraint with optional weight and optional identifier.
6463  If no weight is supplied, then the penalty for violating the soft constraint
6464  is 1.
6465  Soft constraints are grouped by identifiers. Soft constraints that are
6466  added without identifiers are grouped by default.
6467  """
6468  if _is_int(weight):
6469  weight = "%d" % weight
6470  if not isinstance(weight, str):
6471  raise Z3Exception("weight should be a string or an integer")
6472  if id == None:
6473  id = ""
6474  id = to_symbol(id, self.ctx)
6475  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
6476  return OptimizeObjective(self, v, False)
Z3_optimize_assert_soft
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.
z3py.to_symbol
def to_symbol
Definition: z3py.py:94
z3py.Optimize.add_soft
def add_soft
Definition: z3py.py:6460
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 
6447  def assert_exprs(self, *args):
6448  """Assert constraints as background axioms for the optimize solver."""
6449  args = _get_args(args)
6450  for arg in args:
6451  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6452  for f in arg:
6453  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
6454  else:
6455  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
Z3_optimize_assert
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
z3py.Optimize.assert_exprs
def assert_exprs
Definition: z3py.py:6446
def check (   self) 
Check satisfiability while optimizing objective functions.

Definition at line 6493 of file z3py.py.

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

Definition at line 6438 of file z3py.py.

6438 
6439  def help(self):
6440  """Display a string describing all available options."""
6441  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
z3py.Optimize.help
def help
Definition: z3py.py:6438
Z3_optimize_get_help
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 
6509  def lower(self, obj):
6510  if not isinstance(obj, OptimizeObjective):
6511  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
6512  return obj.lower()
z3py.Optimize.lower
def lower
Definition: z3py.py:6508
def maximize (   self,
  arg 
) 
Add objective function to maximize.

Definition at line 6477 of file z3py.py.

6477 
6478  def maximize(self, arg):
6479  """Add objective function to maximize."""
6480  return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
z3py.Optimize.maximize
def maximize
Definition: z3py.py:6477
Z3_optimize_maximize
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 
6482  def minimize(self, arg):
6483  """Add objective function to minimize."""
6484  return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
z3py.Optimize.minimize
def minimize
Definition: z3py.py:6481
Z3_optimize_minimize
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 
6502  def model(self):
6503  """Return a model for the last check()."""
6504  try:
6505  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
6506  except Z3Exception:
6507  raise Z3Exception("model is not available")
Z3_optimize_get_model
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
z3py.Optimize.model
def model
Definition: z3py.py:6501
def param_descrs (   self) 
Return the parameter description set.

Definition at line 6442 of file z3py.py.

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

Definition at line 6489 of file z3py.py.

6489 
6490  def pop(self):
6491  """restore to previously created backtracking point"""
6492  Z3_optimize_pop(self.ctx.ref(), self.optimize)
Z3_optimize_pop
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 
6486  def push(self):
6487  """create a backtracking point for added rules, facts and assertions"""
6488  Z3_optimize_push(self.ctx.ref(), self.optimize)
z3py.Optimize.push
def push
Definition: z3py.py:6485
Z3_optimize_push
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 
6498  def reason_unknown(self):
6499  """Return a string that describes why the last `check()` returned `unknown`."""
6500  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
z3py.Optimize.reason_unknown
def reason_unknown
Definition: z3py.py:6497
Z3_optimize_get_reason_unknown
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 
6433  def set(self, *args, **keys):
6434  """Set a configuration option. The method `help()` return a string containing all available options.
6435  """
6436  p = args2params(args, keys, self.ctx)
6437  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
z3py.args2params
def args2params
Definition: z3py.py:4527
Z3_optimize_set_params
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
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 
6523  def sexpr(self):
6524  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6525  """
6526  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
z3py.Optimize.sexpr
def sexpr
Definition: z3py.py:6522
Z3_optimize_to_string
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
def statistics (   self) 
Return statistics for the last `query()`.

Definition at line 6527 of file z3py.py.

6527 
6528  def statistics(self):
6529  """Return statistics for the last `query()`.
6530  """
6531  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
6532 
6533 
6534 
z3py.Statistics
Statistics.
Definition: z3py.py:5604
z3py.Optimize.statistics
def statistics
Definition: z3py.py:6527
Z3_optimize_get_statistics
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 
6514  def upper(self, obj):
6515  if not isinstance(obj, OptimizeObjective):
6516  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
6517  return obj.upper()
z3py.Optimize.upper
def upper
Definition: z3py.py:6513

Field Documentation

ctx

Definition at line 6424 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), ApplyResult.convert_model(), Optimize.model(), Optimize.param_descrs(), Tactic.param_descrs(), Optimize.set(), Tactic.solver(), and Optimize.statistics().

optimize

Definition at line 6425 of file z3py.py.

Referenced by Optimize.__del__(), Optimize.add_soft(), Optimize.assert_exprs(), Optimize.check(), Optimize.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.param_descrs(), Optimize.pop(), Optimize.push(), Optimize.reason_unknown(), Optimize.set(), Optimize.sexpr(), and Optimize.statistics().

Generated on Fri Apr 12 2019 11:38:55 for Z3 by   doxygen 1.8.5