Z3
 
Loading...
Searching...
No Matches
Public Member Functions | Data Fields | Protected Attributes
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
 

Protected Attributes

 _on_models_id
 

Additional Inherited Members

- Protected Member Functions inherited from Z3PPObject
def _repr_html_ (self)
 

Detailed Description

Optimize API provides methods for solving using objective functions and weighted soft constraints

Definition at line 7858 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 7861 of file z3py.py.

7861 def __init__(self, ctx=None):
7862 self.ctx = _get_ctx(ctx)
7863 self.optimize = Z3_mk_optimize(self.ctx.ref())
7864 self._on_models_id = None
7865 Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7866
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 7870 of file z3py.py.

7870 def __del__(self):
7871 if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
7872 Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7873 if self._on_models_id is not None:
7874 del _on_models[self._on_models_id]
7875
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 7867 of file z3py.py.

7867 def __deepcopy__(self, memo={}):
7868 return Optimize(self.optimize, self.ctx)
7869

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7907 of file z3py.py.

7907 def __iadd__(self, fml):
7908 self.add(fml)
7909 return self
7910

◆ __repr__()

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

Definition at line 8047 of file z3py.py.

8047 def __repr__(self):
8048 """Return a formatted string with all added rules and constraints."""
8049 return self.sexpr()
8050

◆ add()

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

Definition at line 7903 of file z3py.py.

7903 def add(self, *args):
7904 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7905 self.assert_exprs(*args)
7906

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

7940 def add_soft(self, arg, weight="1", id=None):
7941 """Add soft constraint with optional weight and optional identifier.
7942 If no weight is supplied, then the penalty for violating the soft constraint
7943 is 1.
7944 Soft constraints are grouped by identifiers. Soft constraints that are
7945 added without identifiers are grouped by default.
7946 """
7947 if _is_int(weight):
7948 weight = "%d" % weight
7949 elif isinstance(weight, float):
7950 weight = "%f" % weight
7951 if not isinstance(weight, str):
7952 raise Z3Exception("weight should be a string or an integer")
7953 if id is None:
7954 id = ""
7955 id = to_symbol(id, self.ctx)
7956
7957 def asoft(a):
7958 v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
7959 return OptimizeObjective(self, v, False)
7960 if sys.version_info.major >= 3 and isinstance(arg, Iterable):
7961 return [asoft(a) for a in arg]
7962 return asoft(arg)
7963
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 7911 of file z3py.py.

7911 def assert_and_track(self, a, p):
7912 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7913
7914 If `p` is a string, it will be automatically converted into a Boolean constant.
7915
7916 >>> x = Int('x')
7917 >>> p3 = Bool('p3')
7918 >>> s = Optimize()
7919 >>> s.assert_and_track(x > 0, 'p1')
7920 >>> s.assert_and_track(x != 1, 'p2')
7921 >>> s.assert_and_track(x < 0, p3)
7922 >>> print(s.check())
7923 unsat
7924 >>> c = s.unsat_core()
7925 >>> len(c)
7926 2
7927 >>> Bool('p1') in c
7928 True
7929 >>> Bool('p2') in c
7930 False
7931 >>> p3 in c
7932 True
7933 """
7934 if isinstance(p, str):
7935 p = Bool(p, self.ctx)
7936 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7937 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7938 Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
7939
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 7891 of file z3py.py.

7891 def assert_exprs(self, *args):
7892 """Assert constraints as background axioms for the optimize solver."""
7893 args = _get_args(args)
7894 s = BoolSort(self.ctx)
7895 for arg in args:
7896 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7897 for f in arg:
7898 Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7899 else:
7900 arg = s.cast(arg)
7901 Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7902
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 8039 of file z3py.py.

8039 def assertions(self):
8040 """Return an AST vector containing all added constraints."""
8041 return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
8042
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 7988 of file z3py.py.

7988 def check(self, *assumptions):
7989 """Check satisfiability while optimizing objective functions."""
7990 assumptions = _get_args(assumptions)
7991 num = len(assumptions)
7992 _assumptions = (Ast * num)()
7993 for i in range(num):
7994 _assumptions[i] = assumptions[i].as_ast()
7995 return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7996
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 8031 of file z3py.py.

8031 def from_file(self, filename):
8032 """Parse assertions and objectives from a file"""
8033 Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
8034
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 8035 of file z3py.py.

8035 def from_string(self, s):
8036 """Parse assertions and objectives from a string"""
8037 Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
8038
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 7883 of file z3py.py.

7883 def help(self):
7884 """Display a string describing all available options."""
7885 print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7886
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 8011 of file z3py.py.

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

Referenced by OptimizeObjective.value().

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 8021 of file z3py.py.

8021 def lower_values(self, obj):
8022 if not isinstance(obj, OptimizeObjective):
8023 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8024 return obj.lower_values()
8025

◆ maximize()

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

Definition at line 7964 of file z3py.py.

7964 def maximize(self, arg):
7965 """Add objective function to maximize."""
7966 return OptimizeObjective(
7967 self,
7968 Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
7969 is_max=True,
7970 )
7971
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 7972 of file z3py.py.

7972 def minimize(self, arg):
7973 """Add objective function to minimize."""
7974 return OptimizeObjective(
7975 self,
7976 Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
7977 is_max=False,
7978 )
7979
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 8001 of file z3py.py.

8001 def model(self):
8002 """Return a model for the last check()."""
8003 try:
8004 return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
8005 except Z3Exception:
8006 raise Z3Exception("model is not available")
8007
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 8043 of file z3py.py.

8043 def objectives(self):
8044 """returns set of objective functions"""
8045 return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
8046
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 7887 of file z3py.py.

7887 def param_descrs(self):
7888 """Return the parameter description set."""
7889 return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7890
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 7984 of file z3py.py.

7984 def pop(self):
7985 """restore to previously created backtracking point"""
7986 Z3_optimize_pop(self.ctx.ref(), self.optimize)
7987
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 7980 of file z3py.py.

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

7997 def reason_unknown(self):
7998 """Return a string that describes why the last `check()` returned `unknown`."""
7999 return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
8000
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 7876 of file z3py.py.

7876 def set(self, *args, **keys):
7877 """Set a configuration option.
7878 The method `help()` return a string containing all available options.
7879 """
7880 p = args2params(args, keys, self.ctx)
7881 Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7882
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 8062 of file z3py.py.

8062 def set_on_model(self, on_model):
8063 """Register a callback that is invoked with every incremental improvement to
8064 objective values. The callback takes a model as argument.
8065 The life-time of the model is limited to the callback so the
8066 model has to be (deep) copied if it is to be used after the callback
8067 """
8068 id = len(_on_models) + 41
8069 mdl = Model(self.ctx)
8070 _on_models[id] = (on_model, mdl)
8071 self._on_models_id = id
8073 self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
8074 )
8075
8076
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 8051 of file z3py.py.

8051 def sexpr(self):
8052 """Return a formatted string (in Lisp-like format) with all added constraints.
8053 We say the string is in s-expression format.
8054 """
8055 return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
8056
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 8057 of file z3py.py.

8057 def statistics(self):
8058 """Return statistics for the last check`.
8059 """
8060 return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
8061
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 8008 of file z3py.py.

8008 def unsat_core(self):
8009 return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
8010
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 8016 of file z3py.py.

8016 def upper(self, obj):
8017 if not isinstance(obj, OptimizeObjective):
8018 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8019 return obj.upper()
8020

Referenced by OptimizeObjective.value().

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 8026 of file z3py.py.

8026 def upper_values(self, obj):
8027 if not isinstance(obj, OptimizeObjective):
8028 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
8029 return obj.upper_values()
8030

Field Documentation

◆ _on_models_id

_on_models_id
protected

Definition at line 7864 of file z3py.py.

Referenced by Optimize.__del__(), and Optimize.set_on_model().

◆ ctx

ctx

Definition at line 7862 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__(), Simplifier.__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__(), Simplifier.__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__(), BoolRef.__mul__(), 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(), Simplifier.add(), 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(), Simplifier.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(), Solver.next(), 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(), Simplifier.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.root(), 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(), Simplifier.using_params(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ optimize

optimize