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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 7743 of file z3py.py.

7743  def __init__(self, ctx=None):
7744  self.ctx = _get_ctx(ctx)
7745  self.optimize = Z3_mk_optimize(self.ctx.ref())
7746  self._on_models_id = None
7747  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7748 
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 7752 of file z3py.py.

7752  def __del__(self):
7753  if self.optimize is not None and self.ctx.ref() is not None:
7754  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7755  if self._on_models_id is not None:
7756  del _on_models[self._on_models_id]
7757 
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 7749 of file z3py.py.

7749  def __deepcopy__(self, memo={}):
7750  return Optimize(self.optimize, self.ctx)
7751 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7789 of file z3py.py.

7789  def __iadd__(self, fml):
7790  self.add(fml)
7791  return self
7792 

◆ __repr__()

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

Definition at line 7929 of file z3py.py.

7929  def __repr__(self):
7930  """Return a formatted string with all added rules and constraints."""
7931  return self.sexpr()
7932 

◆ add()

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

Definition at line 7785 of file z3py.py.

7785  def add(self, *args):
7786  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7787  self.assert_exprs(*args)
7788 

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

7822  def add_soft(self, arg, weight="1", id=None):
7823  """Add soft constraint with optional weight and optional identifier.
7824  If no weight is supplied, then the penalty for violating the soft constraint
7825  is 1.
7826  Soft constraints are grouped by identifiers. Soft constraints that are
7827  added without identifiers are grouped by default.
7828  """
7829  if _is_int(weight):
7830  weight = "%d" % weight
7831  elif isinstance(weight, float):
7832  weight = "%f" % weight
7833  if not isinstance(weight, str):
7834  raise Z3Exception("weight should be a string or an integer")
7835  if id is None:
7836  id = ""
7837  id = to_symbol(id, self.ctx)
7838 
7839  def asoft(a):
7840  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
7841  return OptimizeObjective(self, v, False)
7842  if sys.version_info.major >= 3 and isinstance(arg, Iterable):
7843  return [asoft(a) for a in arg]
7844  return asoft(arg)
7845 
def to_symbol(s, ctx=None)
Definition: z3py.py:129
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_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 7793 of file z3py.py.

7793  def assert_and_track(self, a, p):
7794  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7795 
7796  If `p` is a string, it will be automatically converted into a Boolean constant.
7797 
7798  >>> x = Int('x')
7799  >>> p3 = Bool('p3')
7800  >>> s = Optimize()
7801  >>> s.assert_and_track(x > 0, 'p1')
7802  >>> s.assert_and_track(x != 1, 'p2')
7803  >>> s.assert_and_track(x < 0, p3)
7804  >>> print(s.check())
7805  unsat
7806  >>> c = s.unsat_core()
7807  >>> len(c)
7808  2
7809  >>> Bool('p1') in c
7810  True
7811  >>> Bool('p2') in c
7812  False
7813  >>> p3 in c
7814  True
7815  """
7816  if isinstance(p, str):
7817  p = Bool(p, self.ctx)
7818  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7819  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7820  Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
7821 
def is_const(a)
Definition: z3py.py:1259
def Bool(name, ctx=None)
Definition: z3py.py:1692
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.

◆ assert_exprs()

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

Definition at line 7773 of file z3py.py.

7773  def assert_exprs(self, *args):
7774  """Assert constraints as background axioms for the optimize solver."""
7775  args = _get_args(args)
7776  s = BoolSort(self.ctx)
7777  for arg in args:
7778  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7779  for f in arg:
7780  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7781  else:
7782  arg = s.cast(arg)
7783  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7784 
def BoolSort(ctx=None)
Definition: z3py.py:1655
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.

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

7921  def assertions(self):
7922  """Return an AST vector containing all added constraints."""
7923  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
7924 
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 7870 of file z3py.py.

7870  def check(self, *assumptions):
7871  """Check satisfiability while optimizing objective functions."""
7872  assumptions = _get_args(assumptions)
7873  num = len(assumptions)
7874  _assumptions = (Ast * num)()
7875  for i in range(num):
7876  _assumptions[i] = assumptions[i].as_ast()
7877  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7878 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
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 7913 of file z3py.py.

7913  def from_file(self, filename):
7914  """Parse assertions and objectives from a file"""
7915  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
7916 
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 7917 of file z3py.py.

7917  def from_string(self, s):
7918  """Parse assertions and objectives from a string"""
7919  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
7920 
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 7765 of file z3py.py.

7765  def help(self):
7766  """Display a string describing all available options."""
7767  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7768 
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 7893 of file z3py.py.

7893  def lower(self, obj):
7894  if not isinstance(obj, OptimizeObjective):
7895  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7896  return obj.lower()
7897 

Referenced by OptimizeObjective.value().

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 7903 of file z3py.py.

7903  def lower_values(self, obj):
7904  if not isinstance(obj, OptimizeObjective):
7905  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7906  return obj.lower_values()
7907 

◆ maximize()

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

Definition at line 7846 of file z3py.py.

7846  def maximize(self, arg):
7847  """Add objective function to maximize."""
7848  return OptimizeObjective(
7849  self,
7850  Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
7851  is_max=True,
7852  )
7853 
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 7854 of file z3py.py.

7854  def minimize(self, arg):
7855  """Add objective function to minimize."""
7856  return OptimizeObjective(
7857  self,
7858  Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
7859  is_max=False,
7860  )
7861 
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 7883 of file z3py.py.

7883  def model(self):
7884  """Return a model for the last check()."""
7885  try:
7886  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7887  except Z3Exception:
7888  raise Z3Exception("model is not available")
7889 
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(), and ModelRef.translate().

◆ objectives()

def objectives (   self)
returns set of objective functions

Definition at line 7925 of file z3py.py.

7925  def objectives(self):
7926  """returns set of objective functions"""
7927  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
7928 
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 7769 of file z3py.py.

7769  def param_descrs(self):
7770  """Return the parameter description set."""
7771  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7772 
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 7866 of file z3py.py.

7866  def pop(self):
7867  """restore to previously created backtracking point"""
7868  Z3_optimize_pop(self.ctx.ref(), self.optimize)
7869 
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 7862 of file z3py.py.

7862  def push(self):
7863  """create a backtracking point for added rules, facts and assertions"""
7864  Z3_optimize_push(self.ctx.ref(), self.optimize)
7865 
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 7879 of file z3py.py.

7879  def reason_unknown(self):
7880  """Return a string that describes why the last `check()` returned `unknown`."""
7881  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
7882 
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 7758 of file z3py.py.

7758  def set(self, *args, **keys):
7759  """Set a configuration option.
7760  The method `help()` return a string containing all available options.
7761  """
7762  p = args2params(args, keys, self.ctx)
7763  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7764 
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5396
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.

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

7944  def set_on_model(self, on_model):
7945  """Register a callback that is invoked with every incremental improvement to
7946  objective values. The callback takes a model as argument.
7947  The life-time of the model is limited to the callback so the
7948  model has to be (deep) copied if it is to be used after the callback
7949  """
7950  id = len(_on_models) + 41
7951  mdl = Model(self.ctx)
7952  _on_models[id] = (on_model, mdl)
7953  self._on_models_id = id
7955  self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
7956  )
7957 
7958 
def Model(ctx=None)
Definition: z3py.py:6579
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.

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

7933  def sexpr(self):
7934  """Return a formatted string (in Lisp-like format) with all added constraints.
7935  We say the string is in s-expression format.
7936  """
7937  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
7938 
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 7939 of file z3py.py.

7939  def statistics(self):
7940  """Return statistics for the last check`.
7941  """
7942  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
7943 
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 7890 of file z3py.py.

7890  def unsat_core(self):
7891  return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
7892 
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 7898 of file z3py.py.

7898  def upper(self, obj):
7899  if not isinstance(obj, OptimizeObjective):
7900  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7901  return obj.upper()
7902 

Referenced by OptimizeObjective.value().

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 7908 of file z3py.py.

7908  def upper_values(self, obj):
7909  if not isinstance(obj, OptimizeObjective):
7910  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7911  return obj.upper_values()
7912 

Field Documentation

◆ ctx

ctx

Definition at line 7744 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__(), QuantifierRef.__getitem__(), ArrayRef.__getitem__(), 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__(), 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(), 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(), 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(), 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