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, assumptions)
 
def reason_unknown (self)
 
def model (self)
 
def unsat_core (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 7278 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 7281 of file z3py.py.

7281  def __init__(self, ctx=None):
7282  self.ctx = _get_ctx(ctx)
7283  self.optimize = Z3_mk_optimize(self.ctx.ref())
7284  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7285 
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 7289 of file z3py.py.

7289  def __del__(self):
7290  if self.optimize is not None and self.ctx.ref() is not None:
7291  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7292 
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 7286 of file z3py.py.

7286  def __deepcopy__(self, memo={}):
7287  return Optimize(self.optimize, self.ctx)
7288 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7323 of file z3py.py.

7323  def __iadd__(self, fml):
7324  self.add(fml)
7325  return self
7326 

◆ __repr__()

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

Definition at line 7427 of file z3py.py.

7427  def __repr__(self):
7428  """Return a formatted string with all added rules and constraints."""
7429  return self.sexpr()
7430 

◆ add()

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

Definition at line 7319 of file z3py.py.

Referenced by Optimize.__iadd__().

7319  def add(self, *args):
7320  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7321  self.assert_exprs(*args)
7322 

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

7327  def add_soft(self, arg, weight = "1", id = None):
7328  """Add soft constraint with optional weight and optional identifier.
7329  If no weight is supplied, then the penalty for violating the soft constraint
7330  is 1.
7331  Soft constraints are grouped by identifiers. Soft constraints that are
7332  added without identifiers are grouped by default.
7333  """
7334  if _is_int(weight):
7335  weight = "%d" % weight
7336  elif isinstance(weight, float):
7337  weight = "%f" % weight
7338  if not isinstance(weight, str):
7339  raise Z3Exception("weight should be a string or an integer")
7340  if id is None:
7341  id = ""
7342  id = to_symbol(id, self.ctx)
7343  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
7344  return OptimizeObjective(self, v, False)
7345 
def to_symbol(s, ctx=None)
Definition: z3py.py:105
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 7307 of file z3py.py.

Referenced by Optimize.add().

7307  def assert_exprs(self, *args):
7308  """Assert constraints as background axioms for the optimize solver."""
7309  args = _get_args(args)
7310  s = BoolSort(self.ctx)
7311  for arg in args:
7312  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7313  for f in arg:
7314  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7315  else:
7316  arg = s.cast(arg)
7317  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7318 
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
def BoolSort(ctx=None)
Definition: z3py.py:1512

◆ assertions()

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

Definition at line 7419 of file z3py.py.

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

Definition at line 7362 of file z3py.py.

7362  def check(self, *assumptions):
7363  """Check satisfiability while optimizing objective functions."""
7364  assumptions = _get_args(assumptions)
7365  num = len(assumptions)
7366  _assumptions = (Ast * num)()
7367  for i in range(num):
7368  _assumptions[i] = assumptions[i].as_ast()
7369  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7370 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3244
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])
Check consistency and produce optimal values.

◆ from_file()

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

Definition at line 7405 of file z3py.py.

7405  def from_file(self, filename):
7406  """Parse assertions and objectives from a file"""
7407  try:
7408  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
7409  except Z3Exception as e:
7410  _handle_parse_error(e, self.ctx)
7411 
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 7412 of file z3py.py.

7412  def from_string(self, s):
7413  """Parse assertions and objectives from a string"""
7414  try:
7415  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
7416  except Z3Exception as e:
7417  _handle_parse_error(e, self.ctx)
7418 
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 7299 of file z3py.py.

7299  def help(self):
7300  """Display a string describing all available options."""
7301  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7302 
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 7385 of file z3py.py.

7385  def lower(self, obj):
7386  if not isinstance(obj, OptimizeObjective):
7387  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7388  return obj.lower()
7389 

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 7395 of file z3py.py.

7395  def lower_values(self, obj):
7396  if not isinstance(obj, OptimizeObjective):
7397  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7398  return obj.lower_values()
7399 

◆ maximize()

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

Definition at line 7346 of file z3py.py.

7346  def maximize(self, arg):
7347  """Add objective function to maximize."""
7348  return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
7349 
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 7350 of file z3py.py.

7350  def minimize(self, arg):
7351  """Add objective function to minimize."""
7352  return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
7353 
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 7375 of file z3py.py.

7375  def model(self):
7376  """Return a model for the last check()."""
7377  try:
7378  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7379  except Z3Exception:
7380  raise Z3Exception("model is not available")
7381 
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 7423 of file z3py.py.

7423  def objectives(self):
7424  """returns set of objective functions"""
7425  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
7426 
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 7303 of file z3py.py.

7303  def param_descrs(self):
7304  """Return the parameter description set."""
7305  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7306 
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 7358 of file z3py.py.

7358  def pop(self):
7359  """restore to previously created backtracking point"""
7360  Z3_optimize_pop(self.ctx.ref(), self.optimize)
7361 
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 7354 of file z3py.py.

7354  def push(self):
7355  """create a backtracking point for added rules, facts and assertions"""
7356  Z3_optimize_push(self.ctx.ref(), self.optimize)
7357 
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 7371 of file z3py.py.

7371  def reason_unknown(self):
7372  """Return a string that describes why the last `check()` returned `unknown`."""
7373  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
7374 
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 7293 of file z3py.py.

7293  def set(self, *args, **keys):
7294  """Set a configuration option. The method `help()` return a string containing all available options.
7295  """
7296  p = args2params(args, keys, self.ctx)
7297  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7298 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5001
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 7431 of file z3py.py.

Referenced by Optimize.__repr__().

7431  def sexpr(self):
7432  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
7433  """
7434  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
7435 
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 7436 of file z3py.py.

7436  def statistics(self):
7437  """Return statistics for the last check`.
7438  """
7439  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
7440 
7441 
7442 
7443 
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.

◆ unsat_core()

def unsat_core (   self)

Definition at line 7382 of file z3py.py.

7382  def unsat_core(self):
7383  return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
7384 
Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o)
Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions ...

◆ upper()

def upper (   self,
  obj 
)

Definition at line 7390 of file z3py.py.

7390  def upper(self, obj):
7391  if not isinstance(obj, OptimizeObjective):
7392  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7393  return obj.upper()
7394 

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 7400 of file z3py.py.

7400  def upper_values(self, obj):
7401  if not isinstance(obj, OptimizeObjective):
7402  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7403  return obj.upper_values()
7404 

Field Documentation

◆ ctx

ctx

◆ optimize

optimize