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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 7778 of file z3py.py.

7778  def __init__(self, ctx=None):
7779  self.ctx = _get_ctx(ctx)
7780  self.optimize = Z3_mk_optimize(self.ctx.ref())
7781  self._on_models_id = None
7782  Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7783 
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 7787 of file z3py.py.

7787  def __del__(self):
7788  if self.optimize is not None and self.ctx.ref() is not None:
7789  Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7790  if self._on_models_id is not None:
7791  del _on_models[self._on_models_id]
7792 
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 7784 of file z3py.py.

7784  def __deepcopy__(self, memo={}):
7785  return Optimize(self.optimize, self.ctx)
7786 

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7824 of file z3py.py.

7824  def __iadd__(self, fml):
7825  self.add(fml)
7826  return self
7827 

◆ __repr__()

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

Definition at line 7964 of file z3py.py.

7964  def __repr__(self):
7965  """Return a formatted string with all added rules and constraints."""
7966  return self.sexpr()
7967 

◆ add()

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

Definition at line 7820 of file z3py.py.

7820  def add(self, *args):
7821  """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7822  self.assert_exprs(*args)
7823 

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

7857  def add_soft(self, arg, weight="1", id=None):
7858  """Add soft constraint with optional weight and optional identifier.
7859  If no weight is supplied, then the penalty for violating the soft constraint
7860  is 1.
7861  Soft constraints are grouped by identifiers. Soft constraints that are
7862  added without identifiers are grouped by default.
7863  """
7864  if _is_int(weight):
7865  weight = "%d" % weight
7866  elif isinstance(weight, float):
7867  weight = "%f" % weight
7868  if not isinstance(weight, str):
7869  raise Z3Exception("weight should be a string or an integer")
7870  if id is None:
7871  id = ""
7872  id = to_symbol(id, self.ctx)
7873 
7874  def asoft(a):
7875  v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
7876  return OptimizeObjective(self, v, False)
7877  if sys.version_info.major >= 3 and isinstance(arg, Iterable):
7878  return [asoft(a) for a in arg]
7879  return asoft(arg)
7880 
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 7828 of file z3py.py.

7828  def assert_and_track(self, a, p):
7829  """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7830 
7831  If `p` is a string, it will be automatically converted into a Boolean constant.
7832 
7833  >>> x = Int('x')
7834  >>> p3 = Bool('p3')
7835  >>> s = Optimize()
7836  >>> s.assert_and_track(x > 0, 'p1')
7837  >>> s.assert_and_track(x != 1, 'p2')
7838  >>> s.assert_and_track(x < 0, p3)
7839  >>> print(s.check())
7840  unsat
7841  >>> c = s.unsat_core()
7842  >>> len(c)
7843  2
7844  >>> Bool('p1') in c
7845  True
7846  >>> Bool('p2') in c
7847  False
7848  >>> p3 in c
7849  True
7850  """
7851  if isinstance(p, str):
7852  p = Bool(p, self.ctx)
7853  _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7854  _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7855  Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
7856 
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:1258
def Bool(name, ctx=None)
Definition: z3py.py:1691

◆ assert_exprs()

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

Definition at line 7808 of file z3py.py.

7808  def assert_exprs(self, *args):
7809  """Assert constraints as background axioms for the optimize solver."""
7810  args = _get_args(args)
7811  s = BoolSort(self.ctx)
7812  for arg in args:
7813  if isinstance(arg, Goal) or isinstance(arg, AstVector):
7814  for f in arg:
7815  Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7816  else:
7817  arg = s.cast(arg)
7818  Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7819 
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:1654

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

7956  def assertions(self):
7957  """Return an AST vector containing all added constraints."""
7958  return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
7959 
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 7905 of file z3py.py.

7905  def check(self, *assumptions):
7906  """Check satisfiability while optimizing objective functions."""
7907  assumptions = _get_args(assumptions)
7908  num = len(assumptions)
7909  _assumptions = (Ast * num)()
7910  for i in range(num):
7911  _assumptions[i] = assumptions[i].as_ast()
7912  return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7913 
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:3823

◆ from_file()

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

Definition at line 7948 of file z3py.py.

7948  def from_file(self, filename):
7949  """Parse assertions and objectives from a file"""
7950  Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
7951 
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 7952 of file z3py.py.

7952  def from_string(self, s):
7953  """Parse assertions and objectives from a string"""
7954  Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
7955 
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 7800 of file z3py.py.

7800  def help(self):
7801  """Display a string describing all available options."""
7802  print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7803 
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 7928 of file z3py.py.

7928  def lower(self, obj):
7929  if not isinstance(obj, OptimizeObjective):
7930  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7931  return obj.lower()
7932 

Referenced by OptimizeObjective.value().

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 7938 of file z3py.py.

7938  def lower_values(self, obj):
7939  if not isinstance(obj, OptimizeObjective):
7940  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7941  return obj.lower_values()
7942 

◆ maximize()

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

Definition at line 7881 of file z3py.py.

7881  def maximize(self, arg):
7882  """Add objective function to maximize."""
7883  return OptimizeObjective(
7884  self,
7885  Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
7886  is_max=True,
7887  )
7888 
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 7889 of file z3py.py.

7889  def minimize(self, arg):
7890  """Add objective function to minimize."""
7891  return OptimizeObjective(
7892  self,
7893  Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
7894  is_max=False,
7895  )
7896 
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 7918 of file z3py.py.

7918  def model(self):
7919  """Return a model for the last check()."""
7920  try:
7921  return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7922  except Z3Exception:
7923  raise Z3Exception("model is not available")
7924 
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 7960 of file z3py.py.

7960  def objectives(self):
7961  """returns set of objective functions"""
7962  return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
7963 
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 7804 of file z3py.py.

7804  def param_descrs(self):
7805  """Return the parameter description set."""
7806  return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7807 
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 7901 of file z3py.py.

7901  def pop(self):
7902  """restore to previously created backtracking point"""
7903  Z3_optimize_pop(self.ctx.ref(), self.optimize)
7904 
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 7897 of file z3py.py.

7897  def push(self):
7898  """create a backtracking point for added rules, facts and assertions"""
7899  Z3_optimize_push(self.ctx.ref(), self.optimize)
7900 
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 7914 of file z3py.py.

7914  def reason_unknown(self):
7915  """Return a string that describes why the last `check()` returned `unknown`."""
7916  return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
7917 
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 7793 of file z3py.py.

7793  def set(self, *args, **keys):
7794  """Set a configuration option.
7795  The method `help()` return a string containing all available options.
7796  """
7797  p = args2params(args, keys, self.ctx)
7798  Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7799 
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:5422

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

7979  def set_on_model(self, on_model):
7980  """Register a callback that is invoked with every incremental improvement to
7981  objective values. The callback takes a model as argument.
7982  The life-time of the model is limited to the callback so the
7983  model has to be (deep) copied if it is to be used after the callback
7984  """
7985  id = len(_on_models) + 41
7986  mdl = Model(self.ctx)
7987  _on_models[id] = (on_model, mdl)
7988  self._on_models_id = id
7990  self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
7991  )
7992 
7993 
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:6614

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

7968  def sexpr(self):
7969  """Return a formatted string (in Lisp-like format) with all added constraints.
7970  We say the string is in s-expression format.
7971  """
7972  return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
7973 
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 7974 of file z3py.py.

7974  def statistics(self):
7975  """Return statistics for the last check`.
7976  """
7977  return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
7978 
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 7925 of file z3py.py.

7925  def unsat_core(self):
7926  return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
7927 
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 7933 of file z3py.py.

7933  def upper(self, obj):
7934  if not isinstance(obj, OptimizeObjective):
7935  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7936  return obj.upper()
7937 

Referenced by OptimizeObjective.value().

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 7943 of file z3py.py.

7943  def upper_values(self, obj):
7944  if not isinstance(obj, OptimizeObjective):
7945  raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7946  return obj.upper_values()
7947 

Field Documentation

◆ ctx

ctx

Definition at line 7779 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