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 assert_and_track (self, a, p)
 
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)
 
def set_on_model (self, on_model)
 
- 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 7813 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 7816 of file z3py.py.

7816  def __init__(self, ctx=None):
7817  self.ctx = _get_ctx(ctx)
7818  self.optimize = Z3_mk_optimize(self.ctx.ref())
7819  self._on_models_id = None
7820  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7821 
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.

◆ __del__()

def __del__ (   self)

Definition at line 7825 of file z3py.py.

7825  def __del__(self):
7826  if self.optimize is not None and self.ctx.ref() is not None:
7827  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7828  if self._on_models_id is not None:
7829  del _on_models[self._on_models_id]
7830 
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 7822 of file z3py.py.

7822  def __deepcopy__(self, memo={}):
7823  return Optimize(self.optimize, self.ctx)
7824 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7862 of file z3py.py.

7862  def __iadd__(self, fml):
7863  self.add(fml)
7864  return self
7865 

◆ __repr__()

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

Definition at line 8002 of file z3py.py.

8002  def __repr__(self):
8003  """Return a formatted string with all added rules and constraints."""
8004  return self.sexpr()
8005 

◆ add()

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

Definition at line 7858 of file z3py.py.

7858  def add(self, *args):
7859  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7860  self.assert_exprs(*args)
7861 

Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().

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

7895  def add_soft(self, arg, weight="1", id=None):
7896  """Add soft constraint with optional weight and optional identifier.
7897  If no weight is supplied, then the penalty for violating the soft constraint
7898  is 1.
7899  Soft constraints are grouped by identifiers. Soft constraints that are
7900  added without identifiers are grouped by default.
7901  """
7902  if _is_int(weight):
7903  weight = "%d" % weight
7904  elif isinstance(weight, float):
7905  weight = "%f" % weight
7906  if not isinstance(weight, str):
7907  raise Z3Exception("weight should be a string or an integer")
7908  if id is None:
7909  id = ""
7910  id = to_symbol(id, self.ctx)
7911 
7912  def asoft(a):
7913  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
7914  return OptimizeObjective(self, v, False)
7915  if sys.version_info.major >= 3 and isinstance(arg, Iterable):
7916  return [asoft(a) for a in arg]
7917  return asoft(arg)
7918 
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 to_symbol(s, ctx=None)
Definition: z3py.py:124

◆ assert_and_track()

def assert_and_track (   self,
  a,
  p 
)
Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.

If `p` is a string, it will be automatically converted into a Boolean constant.

>>> x = Int('x')
>>> p3 = Bool('p3')
>>> s = Optimize()
>>> s.assert_and_track(x > 0,  'p1')
>>> s.assert_and_track(x != 1, 'p2')
>>> s.assert_and_track(x < 0,  p3)
>>> print(s.check())
unsat
>>> c = s.unsat_core()
>>> len(c)
2
>>> Bool('p1') in c
True
>>> Bool('p2') in c
False
>>> p3 in c
True

Definition at line 7866 of file z3py.py.

7866  def assert_and_track(self, a, p):
7867  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7868 
7869  If `p` is a string, it will be automatically converted into a Boolean constant.
7870 
7871  >>> x = Int('x')
7872  >>> p3 = Bool('p3')
7873  >>> s = Optimize()
7874  >>> s.assert_and_track(x > 0, 'p1')
7875  >>> s.assert_and_track(x != 1, 'p2')
7876  >>> s.assert_and_track(x < 0, p3)
7877  >>> print(s.check())
7878  unsat
7879  >>> c = s.unsat_core()
7880  >>> len(c)
7881  2
7882  >>> Bool('p1') in c
7883  True
7884  >>> Bool('p2') in c
7885  False
7886  >>> p3 in c
7887  True
7888  """
7889  if isinstance(p, str):
7890  p = Bool(p, self.ctx)
7891  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7892  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7893  Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
7894 
void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t)
Assert tracked hard constraint to the optimization context.
def is_const(a)
Definition: z3py.py:1280
def Bool(name, ctx=None)
Definition: z3py.py:1713

◆ assert_exprs()

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

Definition at line 7846 of file z3py.py.

7846  def assert_exprs(self, *args):
7847  """Assert constraints as background axioms for the optimize solver."""
7848  args = _get_args(args)
7849  s = BoolSort(self.ctx)
7850  for arg in args:
7851  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7852  for f in arg:
7853  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7854  else:
7855  arg = s.cast(arg)
7856  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7857 
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:1676

Referenced by Goal.add(), Solver.add(), Fixedpoint.add(), Optimize.add(), Goal.append(), Solver.append(), Fixedpoint.append(), Goal.insert(), Solver.insert(), and Fixedpoint.insert().

◆ assertions()

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

Definition at line 7994 of file z3py.py.

7994  def assertions(self):
7995  """Return an AST vector containing all added constraints."""
7996  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
7997 
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.

Referenced by Solver.to_smt2().

◆ check()

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

Definition at line 7943 of file z3py.py.

7943  def check(self, *assumptions):
7944  """Check satisfiability while optimizing objective functions."""
7945  assumptions = _get_args(assumptions)
7946  num = len(assumptions)
7947  _assumptions = (Ast * num)()
7948  for i in range(num):
7949  _assumptions[i] = assumptions[i].as_ast()
7950  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7951 
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.
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3824

◆ from_file()

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

Definition at line 7986 of file z3py.py.

7986  def from_file(self, filename):
7987  """Parse assertions and objectives from a file"""
7988  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
7989 
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....

◆ from_string()

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

Definition at line 7990 of file z3py.py.

7990  def from_string(self, s):
7991  """Parse assertions and objectives from a string"""
7992  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
7993 
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....

◆ help()

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

Definition at line 7838 of file z3py.py.

7838  def help(self):
7839  """Display a string describing all available options."""
7840  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7841 
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 7966 of file z3py.py.

7966  def lower(self, obj):
7967  if not isinstance(obj, OptimizeObjective):
7968  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7969  return obj.lower()
7970 

Referenced by OptimizeObjective.value().

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 7976 of file z3py.py.

7976  def lower_values(self, obj):
7977  if not isinstance(obj, OptimizeObjective):
7978  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7979  return obj.lower_values()
7980 

◆ maximize()

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

Definition at line 7919 of file z3py.py.

7919  def maximize(self, arg):
7920  """Add objective function to maximize."""
7921  return OptimizeObjective(
7922  self,
7923  Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
7924  is_max=True,
7925  )
7926 
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 7927 of file z3py.py.

7927  def minimize(self, arg):
7928  """Add objective function to minimize."""
7929  return OptimizeObjective(
7930  self,
7931  Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
7932  is_max=False,
7933  )
7934 
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 7956 of file z3py.py.

7956  def model(self):
7957  """Return a model for the last check()."""
7958  try:
7959  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7960  except Z3Exception:
7961  raise Z3Exception("model is not available")
7962 
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.

Referenced by ModelRef.__del__(), ModelRef.__getitem__(), ModelRef.__len__(), ModelRef.decls(), ModelRef.eval(), ModelRef.get_interp(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), ModelRef.sexpr(), FuncInterp.translate(), ModelRef.translate(), and ModelRef.update_value().

◆ objectives()

def objectives (   self)
returns set of objective functions

Definition at line 7998 of file z3py.py.

7998  def objectives(self):
7999  """returns set of objective functions"""
8000  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
8001 
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 7842 of file z3py.py.

7842  def param_descrs(self):
7843  """Return the parameter description set."""
7844  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7845 
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 7939 of file z3py.py.

7939  def pop(self):
7940  """restore to previously created backtracking point"""
7941  Z3_optimize_pop(self.ctx.ref(), self.optimize)
7942 
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 7935 of file z3py.py.

7935  def push(self):
7936  """create a backtracking point for added rules, facts and assertions"""
7937  Z3_optimize_push(self.ctx.ref(), self.optimize)
7938 
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 7952 of file z3py.py.

7952  def reason_unknown(self):
7953  """Return a string that describes why the last `check()` returned `unknown`."""
7954  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
7955 
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 7831 of file z3py.py.

7831  def set(self, *args, **keys):
7832  """Set a configuration option.
7833  The method `help()` return a string containing all available options.
7834  """
7835  p = args2params(args, keys, self.ctx)
7836  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7837 
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5447

◆ set_on_model()

def set_on_model (   self,
  on_model 
)
Register a callback that is invoked with every incremental improvement to
objective values. The callback takes a model as argument.
The life-time of the model is limited to the callback so the
model has to be (deep) copied if it is to be used after the callback

Definition at line 8017 of file z3py.py.

8017  def set_on_model(self, on_model):
8018  """Register a callback that is invoked with every incremental improvement to
8019  objective values. The callback takes a model as argument.
8020  The life-time of the model is limited to the callback so the
8021  model has to be (deep) copied if it is to be used after the callback
8022  """
8023  id = len(_on_models) + 41
8024  mdl = Model(self.ctx)
8025  _on_models[id] = (on_model, mdl)
8026  self._on_models_id = id
8028  self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
8029  )
8030 
8031 
void Z3_API Z3_optimize_register_model_eh(Z3_context c, Z3_optimize o, Z3_model m, void *ctx, Z3_model_eh model_eh)
register a model event handler for new models.
def Model(ctx=None)
Definition: z3py.py:6652

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

8006  def sexpr(self):
8007  """Return a formatted string (in Lisp-like format) with all added constraints.
8008  We say the string is in s-expression format.
8009  """
8010  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
8011 
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.

Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().

◆ statistics()

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

Definition at line 8012 of file z3py.py.

8012  def statistics(self):
8013  """Return statistics for the last check`.
8014  """
8015  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
8016 
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 7963 of file z3py.py.

7963  def unsat_core(self):
7964  return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
7965 
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 7971 of file z3py.py.

7971  def upper(self, obj):
7972  if not isinstance(obj, OptimizeObjective):
7973  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7974  return obj.upper()
7975 

Referenced by OptimizeObjective.value().

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 7981 of file z3py.py.

7981  def upper_values(self, obj):
7982  if not isinstance(obj, OptimizeObjective):
7983  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7984  return obj.upper_values()
7985 

Field Documentation

◆ ctx

ctx

Definition at line 7817 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), FPRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), Probe.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Context.__del__(), AstRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), ParamsRef.__del__(), ParamDescrsRef.__del__(), Goal.__del__(), AstVector.__del__(), AstMap.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Statistics.__del__(), Solver.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), ArithRef.__div__(), BitVecRef.__div__(), FPRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), FPRef.__ge__(), SeqRef.__ge__(), AstVector.__getitem__(), SeqRef.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ApplyResult.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), FPRef.__gt__(), SeqRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), FPRef.__le__(), SeqRef.__le__(), CharRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ApplyResult.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), FPRef.__lt__(), SeqRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), FPRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), FPRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), FPRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), FPRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), FPRef.__rsub__(), BitVecRef.__rxor__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), FPRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), ApplyResult.as_expr(), FPNumRef.as_string(), Solver.assert_and_track(), Optimize.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), SeqRef.at(), SeqSortRef.basis(), ReSortRef.basis(), QuantifierRef.body(), BoolSortRef.cast(), Solver.check(), Optimize.check(), UserPropagateBase.conflict(), Solver.consequences(), DatatypeSortRef.constructor(), Goal.convert_model(), AstRef.ctx_ref(), UserPropagateBase.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), Solver.dimacs(), ArraySortRef.domain(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), FPNumRef.exponent(), FPNumRef.exponent_as_bv(), FPNumRef.exponent_as_long(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), Optimize.from_string(), Goal.get(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), ParamDescrsRef.get_documentation(), Fixedpoint.get_ground_sat_answer(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), ModelRef.get_sort(), ModelRef.get_universe(), Solver.help(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Solver.import_model_converter(), Goal.inconsistent(), CharRef.is_digit(), FPNumRef.isInf(), FPNumRef.isNaN(), FPNumRef.isNegative(), FPNumRef.isNormal(), FPNumRef.isPositive(), FPNumRef.isSubnormal(), FPNumRef.isZero(), AstMap.keys(), Statistics.keys(), SortRef.kind(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), Solver.non_units(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), RatNumRef.numerator(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), FuncDeclRef.params(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Optimize.pop(), Solver.pop(), Goal.prec(), Solver.proof(), Solver.push(), Optimize.push(), AstVector.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), FuncDeclRef.range(), ArraySortRef.range(), Solver.reason_unknown(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), DatatypeSortRef.recognizer(), Context.ref(), Fixedpoint.register_relation(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.set(), Fixedpoint.set(), Optimize.set(), ParamsRef.set(), Optimize.set_on_model(), Fixedpoint.set_predicate_representation(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), Solver.sexpr(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), FPNumRef.sign(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), FPNumRef.significand_as_long(), ParamDescrsRef.size(), Goal.size(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), FiniteDomainRef.sort(), FPRef.sort(), SeqRef.sort(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), CharRef.to_bv(), CharRef.to_int(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), AstVector.translate(), FuncInterp.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), Fixedpoint.update_rule(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ optimize

optimize