Z3
 
Loading...
Searching...
No Matches
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 7841 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 7844 of file z3py.py.

7844 def __init__(self, ctx=None):
7845 self.ctx = _get_ctx(ctx)
7846 self.optimize = Z3_mk_optimize(self.ctx.ref())
7847 self._on_models_id = None
7848 Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7849
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 7853 of file z3py.py.

7853 def __del__(self):
7854 if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
7855 Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7856 if self._on_models_id is not None:
7857 del _on_models[self._on_models_id]
7858
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 7850 of file z3py.py.

7850 def __deepcopy__(self, memo={}):
7851 return Optimize(self.optimize, self.ctx)
7852

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7890 of file z3py.py.

7890 def __iadd__(self, fml):
7891 self.add(fml)
7892 return self
7893

◆ __repr__()

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

Definition at line 8030 of file z3py.py.

8030 def __repr__(self):
8031 """Return a formatted string with all added rules and constraints."""
8032 return self.sexpr()
8033

◆ add()

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

Definition at line 7886 of file z3py.py.

7886 def add(self, *args):
7887 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7888 self.assert_exprs(*args)
7889

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

7923 def add_soft(self, arg, weight="1", id=None):
7924 """Add soft constraint with optional weight and optional identifier.
7925 If no weight is supplied, then the penalty for violating the soft constraint
7926 is 1.
7927 Soft constraints are grouped by identifiers. Soft constraints that are
7928 added without identifiers are grouped by default.
7929 """
7930 if _is_int(weight):
7931 weight = "%d" % weight
7932 elif isinstance(weight, float):
7933 weight = "%f" % weight
7934 if not isinstance(weight, str):
7935 raise Z3Exception("weight should be a string or an integer")
7936 if id is None:
7937 id = ""
7938 id = to_symbol(id, self.ctx)
7939
7940 def asoft(a):
7941 v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
7942 return OptimizeObjective(self, v, False)
7943 if sys.version_info.major >= 3 and isinstance(arg, Iterable):
7944 return [asoft(a) for a in arg]
7945 return asoft(arg)
7946
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 7894 of file z3py.py.

7894 def assert_and_track(self, a, p):
7895 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7896
7897 If `p` is a string, it will be automatically converted into a Boolean constant.
7898
7899 >>> x = Int('x')
7900 >>> p3 = Bool('p3')
7901 >>> s = Optimize()
7902 >>> s.assert_and_track(x > 0, 'p1')
7903 >>> s.assert_and_track(x != 1, 'p2')
7904 >>> s.assert_and_track(x < 0, p3)
7905 >>> print(s.check())
7906 unsat
7907 >>> c = s.unsat_core()
7908 >>> len(c)
7909 2
7910 >>> Bool('p1') in c
7911 True
7912 >>> Bool('p2') in c
7913 False
7914 >>> p3 in c
7915 True
7916 """
7917 if isinstance(p, str):
7918 p = Bool(p, self.ctx)
7919 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7920 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7921 Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
7922
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 7874 of file z3py.py.

7874 def assert_exprs(self, *args):
7875 """Assert constraints as background axioms for the optimize solver."""
7876 args = _get_args(args)
7877 s = BoolSort(self.ctx)
7878 for arg in args:
7879 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7880 for f in arg:
7881 Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7882 else:
7883 arg = s.cast(arg)
7884 Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7885
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 8022 of file z3py.py.

8022 def assertions(self):
8023 """Return an AST vector containing all added constraints."""
8024 return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
8025
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 7971 of file z3py.py.

7971 def check(self, *assumptions):
7972 """Check satisfiability while optimizing objective functions."""
7973 assumptions = _get_args(assumptions)
7974 num = len(assumptions)
7975 _assumptions = (Ast * num)()
7976 for i in range(num):
7977 _assumptions[i] = assumptions[i].as_ast()
7978 return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7979
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 8014 of file z3py.py.

8014 def from_file(self, filename):
8015 """Parse assertions and objectives from a file"""
8016 Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
8017
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 8018 of file z3py.py.

8018 def from_string(self, s):
8019 """Parse assertions and objectives from a string"""
8020 Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
8021
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 7866 of file z3py.py.

7866 def help(self):
7867 """Display a string describing all available options."""
7868 print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7869
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.

Referenced by Optimize.set().

◆ lower()

def lower (   self,
  obj 
)

Definition at line 7994 of file z3py.py.

7994 def lower(self, obj):
7995 if not isinstance(obj, OptimizeObjective):
7996 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7997 return obj.lower()
7998

Referenced by OptimizeObjective.value().

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 8004 of file z3py.py.

8004 def lower_values(self, obj):
8005 if not isinstance(obj, OptimizeObjective):
8006 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8007 return obj.lower_values()
8008

◆ maximize()

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

Definition at line 7947 of file z3py.py.

7947 def maximize(self, arg):
7948 """Add objective function to maximize."""
7949 return OptimizeObjective(
7950 self,
7951 Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
7952 is_max=True,
7953 )
7954
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 7955 of file z3py.py.

7955 def minimize(self, arg):
7956 """Add objective function to minimize."""
7957 return OptimizeObjective(
7958 self,
7959 Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
7960 is_max=False,
7961 )
7962
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 7984 of file z3py.py.

7984 def model(self):
7985 """Return a model for the last check()."""
7986 try:
7987 return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7988 except Z3Exception:
7989 raise Z3Exception("model is not available")
7990
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 8026 of file z3py.py.

8026 def objectives(self):
8027 """returns set of objective functions"""
8028 return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
8029
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 7870 of file z3py.py.

7870 def param_descrs(self):
7871 """Return the parameter description set."""
7872 return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7873
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 7967 of file z3py.py.

7967 def pop(self):
7968 """restore to previously created backtracking point"""
7969 Z3_optimize_pop(self.ctx.ref(), self.optimize)
7970
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 7963 of file z3py.py.

7963 def push(self):
7964 """create a backtracking point for added rules, facts and assertions"""
7965 Z3_optimize_push(self.ctx.ref(), self.optimize)
7966
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 7980 of file z3py.py.

7980 def reason_unknown(self):
7981 """Return a string that describes why the last `check()` returned `unknown`."""
7982 return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
7983
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 7859 of file z3py.py.

7859 def set(self, *args, **keys):
7860 """Set a configuration option.
7861 The method `help()` return a string containing all available options.
7862 """
7863 p = args2params(args, keys, self.ctx)
7864 Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7865
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 8045 of file z3py.py.

8045 def set_on_model(self, on_model):
8046 """Register a callback that is invoked with every incremental improvement to
8047 objective values. The callback takes a model as argument.
8048 The life-time of the model is limited to the callback so the
8049 model has to be (deep) copied if it is to be used after the callback
8050 """
8051 id = len(_on_models) + 41
8052 mdl = Model(self.ctx)
8053 _on_models[id] = (on_model, mdl)
8054 self._on_models_id = id
8056 self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
8057 )
8058
8059
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 8034 of file z3py.py.

8034 def sexpr(self):
8035 """Return a formatted string (in Lisp-like format) with all added constraints.
8036 We say the string is in s-expression format.
8037 """
8038 return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
8039
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 8040 of file z3py.py.

8040 def statistics(self):
8041 """Return statistics for the last check`.
8042 """
8043 return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
8044
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 7991 of file z3py.py.

7991 def unsat_core(self):
7992 return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
7993
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 7999 of file z3py.py.

7999 def upper(self, obj):
8000 if not isinstance(obj, OptimizeObjective):
8001 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8002 return obj.upper()
8003

Referenced by OptimizeObjective.value().

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 8009 of file z3py.py.

8009 def upper_values(self, obj):
8010 if not isinstance(obj, OptimizeObjective):
8011 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8012 return obj.upper_values()
8013

Field Documentation

◆ ctx

ctx

Definition at line 7845 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__(), ParserContext.__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(), ParserContext.add_decl(), Fixedpoint.add_rule(), Optimize.add_soft(), ParserContext.add_sort(), 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(), ParserContext.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