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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ctx = None 
)

Definition at line 7360 of file z3py.py.

7360 def __init__(self, ctx=None):
7361 self.ctx = _get_ctx(ctx)
7362 self.optimize = Z3_mk_optimize(self.ctx.ref())
7363 Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
7364
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 7368 of file z3py.py.

7368 def __del__(self):
7369 if self.optimize is not None and self.ctx.ref() is not None:
7370 Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
7371
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 7365 of file z3py.py.

7365 def __deepcopy__(self, memo={}):
7366 return Optimize(self.optimize, self.ctx)
7367

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 7402 of file z3py.py.

7402 def __iadd__(self, fml):
7403 self.add(fml)
7404 return self
7405

◆ __repr__()

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

Definition at line 7529 of file z3py.py.

7529 def __repr__(self):
7530 """Return a formatted string with all added rules and constraints."""
7531 return self.sexpr()
7532

◆ add()

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

Definition at line 7398 of file z3py.py.

7398 def add(self, *args):
7399 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7400 self.assert_exprs(*args)
7401

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

7435 def add_soft(self, arg, weight = "1", id = None):
7436 """Add soft constraint with optional weight and optional identifier.
7437 If no weight is supplied, then the penalty for violating the soft constraint
7438 is 1.
7439 Soft constraints are grouped by identifiers. Soft constraints that are
7440 added without identifiers are grouped by default.
7441 """
7442 if _is_int(weight):
7443 weight = "%d" % weight
7444 elif isinstance(weight, float):
7445 weight = "%f" % weight
7446 if not isinstance(weight, str):
7447 raise Z3Exception("weight should be a string or an integer")
7448 if id is None:
7449 id = ""
7450 id = to_symbol(id, self.ctx)
7451 v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
7452 return OptimizeObjective(self, v, False)
7453
def to_symbol(s, ctx=None)
Definition: z3py.py:109
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 7406 of file z3py.py.

7406 def assert_and_track(self, a, p):
7407 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7408
7409 If `p` is a string, it will be automatically converted into a Boolean constant.
7410
7411 >>> x = Int('x')
7412 >>> p3 = Bool('p3')
7413 >>> s = Optimize()
7414 >>> s.assert_and_track(x > 0, 'p1')
7415 >>> s.assert_and_track(x != 1, 'p2')
7416 >>> s.assert_and_track(x < 0, p3)
7417 >>> print(s.check())
7418 unsat
7419 >>> c = s.unsat_core()
7420 >>> len(c)
7421 2
7422 >>> Bool('p1') in c
7423 True
7424 >>> Bool('p2') in c
7425 False
7426 >>> p3 in c
7427 True
7428 """
7429 if isinstance(p, str):
7430 p = Bool(p, self.ctx)
7431 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
7432 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
7433 Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
7434
def is_const(a)
Definition: z3py.py:1162
def Int(name, ctx=None)
Definition: z3py.py:3010
def Bool(name, ctx=None)
Definition: z3py.py:1568
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 7386 of file z3py.py.

7386 def assert_exprs(self, *args):
7387 """Assert constraints as background axioms for the optimize solver."""
7388 args = _get_args(args)
7389 s = BoolSort(self.ctx)
7390 for arg in args:
7391 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7392 for f in arg:
7393 Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
7394 else:
7395 arg = s.cast(arg)
7396 Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
7397
def BoolSort(ctx=None)
Definition: z3py.py:1533
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 7521 of file z3py.py.

7521 def assertions(self):
7522 """Return an AST vector containing all added constraints."""
7523 return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
7524
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 7470 of file z3py.py.

7470 def check(self, *assumptions):
7471 """Check satisfiability while optimizing objective functions."""
7472 assumptions = _get_args(assumptions)
7473 num = len(assumptions)
7474 _assumptions = (Ast * num)()
7475 for i in range(num):
7476 _assumptions[i] = assumptions[i].as_ast()
7477 return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
7478
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
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 7513 of file z3py.py.

7513 def from_file(self, filename):
7514 """Parse assertions and objectives from a file"""
7515 Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
7516
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 7517 of file z3py.py.

7517 def from_string(self, s):
7518 """Parse assertions and objectives from a string"""
7519 Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
7520
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 7378 of file z3py.py.

7378 def help(self):
7379 """Display a string describing all available options."""
7380 print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
7381
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 7493 of file z3py.py.

7493 def lower(self, obj):
7494 if not isinstance(obj, OptimizeObjective):
7495 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7496 return obj.lower()
7497

Referenced by OptimizeObjective.value().

◆ lower_values()

def lower_values (   self,
  obj 
)

Definition at line 7503 of file z3py.py.

7503 def lower_values(self, obj):
7504 if not isinstance(obj, OptimizeObjective):
7505 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7506 return obj.lower_values()
7507

◆ maximize()

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

Definition at line 7454 of file z3py.py.

7454 def maximize(self, arg):
7455 """Add objective function to maximize."""
7456 return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
7457
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 7458 of file z3py.py.

7458 def minimize(self, arg):
7459 """Add objective function to minimize."""
7460 return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
7461
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 7483 of file z3py.py.

7483 def model(self):
7484 """Return a model for the last check()."""
7485 try:
7486 return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
7487 except Z3Exception:
7488 raise Z3Exception("model is not available")
7489
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 7525 of file z3py.py.

7525 def objectives(self):
7526 """returns set of objective functions"""
7527 return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
7528
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 7382 of file z3py.py.

7382 def param_descrs(self):
7383 """Return the parameter description set."""
7384 return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
7385
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 7466 of file z3py.py.

7466 def pop(self):
7467 """restore to previously created backtracking point"""
7468 Z3_optimize_pop(self.ctx.ref(), self.optimize)
7469
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 7462 of file z3py.py.

7462 def push(self):
7463 """create a backtracking point for added rules, facts and assertions"""
7464 Z3_optimize_push(self.ctx.ref(), self.optimize)
7465
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 7479 of file z3py.py.

7479 def reason_unknown(self):
7480 """Return a string that describes why the last `check()` returned `unknown`."""
7481 return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
7482
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 7372 of file z3py.py.

7372 def set(self, *args, **keys):
7373 """Set a configuration option. The method `help()` return a string containing all available options.
7374 """
7375 p = args2params(args, keys, self.ctx)
7376 Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
7377
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5070
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.

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

7533 def sexpr(self):
7534 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
7535 """
7536 return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
7537
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 7538 of file z3py.py.

7538 def statistics(self):
7539 """Return statistics for the last check`.
7540 """
7541 return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
7542
7543
7544
7545
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 7490 of file z3py.py.

7490 def unsat_core(self):
7491 return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
7492
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 7498 of file z3py.py.

7498 def upper(self, obj):
7499 if not isinstance(obj, OptimizeObjective):
7500 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7501 return obj.upper()
7502

Referenced by OptimizeObjective.value().

◆ upper_values()

def upper_values (   self,
  obj 
)

Definition at line 7508 of file z3py.py.

7508 def upper_values(self, obj):
7509 if not isinstance(obj, OptimizeObjective):
7510 raise Z3Exception("Expecting objective handle returned by maximize/minimize")
7511 return obj.upper_values()
7512

Field Documentation

◆ ctx

ctx

Definition at line 7361 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(), Solver.consequences(), DatatypeSortRef.constructor(), Goal.convert_model(), AstRef.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(), 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(), 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