Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/classz3py_1_1_solver.html below:

Z3: Solver Class Reference

Solver API provides methods for implementing the main SMT 2.0 commands:
push, pop, check, get-model, etc.

Definition at line 6943 of file z3py.py.

Definition at line 6949 of file z3py.py.

__init__(self, solver=None, ctx=None, logFile=None):

solver

ctx

self.ctx = _get_ctx(ctx)

self.backtrack_level = 4000000000

self.solver = solver

logFile

:

self.set(

, logFile)

Z3_solver Z3_API Z3_mk_solver(Z3_context c)

Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...

void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)

Increment the reference counter of the given solver.

Definition at line 6962 of file z3py.py.

self.solver

self.ctx.ref()

Z3_solver_dec_ref

:

void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)

Decrement the reference counter of the given solver.

Definition at line 7424 of file z3py.py.

self.translate(self.ctx)

Definition at line 7427 of file z3py.py.

__deepcopy__(self, memo={}):

self.translate(self.ctx)

Definition at line 6966 of file z3py.py.

__enter__(self):

Definition at line 6970 of file z3py.py.

__exit__(self, *exc_info):

Definition at line 7092 of file z3py.py.

__iadd__(self, fml):

Return a formatted string with all added constraints.

Definition at line 7407 of file z3py.py.

obj_to_string(self)

Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 7081 of file z3py.py.

add(self, *args):

self.assert_exprs(*args)

Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().

Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.append(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 7096 of file z3py.py.

append(self, *args):

self.assert_exprs(*args)

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 = Solver()
>>> s.set(unsat_core=True)
>>> 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 7118 of file z3py.py.

assert_and_track(self, a, p):

isinstance(p, str):

p =

(p, self.ctx)

_z3_assert(isinstance(a, BoolRef),

)

_z3_assert(isinstance(p, BoolRef)

(p),

)

void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)

Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.

Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.assert_exprs(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 7062 of file z3py.py.

assert_exprs(self, *args):

args = _get_args(args)

isinstance(arg, Goal)

isinstance(arg, AstVector):

void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)

Assert a constraint into the solver.

Referenced by Goal.add(), Solver.add(), Fixedpoint.add(), Optimize.add(), Goal.append(), Solver.append(), Fixedpoint.append(), Goal.insert(), Solver.insert(), and Fixedpoint.insert().

Return an AST vector containing all added constraints.

>>> s = Solver()
>>> s.assertions()
[]
>>> a = Int('a')
>>> s.add(a > 0)
>>> s.add(a < 10)
>>> s.assertions()
[a > 0, a < 10]

Definition at line 7324 of file z3py.py.

assertions(self):

Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)

Return the set of asserted formulas on the solver.

Referenced by Solver.to_smt2().

Check whether the assertions in the given solver plus the optional assumptions are consistent or not.

>>> x = Int('x')
>>> s = Solver()
>>> s.check()
sat
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> s.model().eval(x)
1
>>> s.add(x < 1)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(2**x == 4)
>>> s.check()
unknown

Definition at line 7148 of file z3py.py.

check(self, *assumptions):

assumptions = _get_args(assumptions)

num = len(assumptions)

_assumptions = (Ast * num)()

i

(num):

_assumptions[i] = s.cast(assumptions[i]).as_ast()

CheckSatResult(r)

Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])

Check whether the assertions in the given solver and optional assumptions are consistent or not.

expr range(expr const &lo, expr const &hi)

Determine fixed values for the variables based on the solver state and assumptions.
>>> s = Solver()
>>> a, b, c, d = Bools('a b c d')
>>> s.add(Implies(a,b), Implies(b, c))
>>> s.consequences([a],[b,c,d])
(sat, [Implies(a, b), Implies(a, c)])
>>> s.consequences([Not(c),d],[a,b,c,d])
(sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])

Definition at line 7239 of file z3py.py.

consequences(self, assumptions, variables):

isinstance(assumptions, list):

_asms = AstVector(

, self.ctx)

a

assumptions:

isinstance(variables, list):

_vars = AstVector(

, self.ctx)

_z3_assert(isinstance(assumptions, AstVector),

)

_z3_assert(isinstance(variables, AstVector),

)

consequences = AstVector(

, self.ctx)

variables.vector, consequences.vector)

sz = len(consequences)

consequences = [consequences[i]

i

(sz)]

CheckSatResult(r), consequences

Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)

retrieve consequences from solver that determine values of the supplied function symbols.

Get set of cubes
The method takes an optional set of variables that restrict which
variables may be used as a starting point for cubing.
If vars is not None, then the first case split is based on a variable in
this set.

Definition at line 7276 of file z3py.py.

cube(self, vars=None):

self.cube_vs = AstVector(

, self.ctx)

vars

:

self.cube_vs.push(v)

lvl = self.backtrack_level

self.backtrack_level = 4000000000

r = AstVector(

(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)

(len(r) == 1

(r[0])):

Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)

extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...

Access the set of variables that were touched by the most recently generated cube.
This set of variables can be used as a starting point for additional cubes.
The idea is that variables that appear in clauses that are reduced by the most recent
cube are likely more useful to cube on.

Definition at line 7297 of file z3py.py.

cube_vars(self):

Return a textual representation of the solver in DIMACS format.

Definition at line 7442 of file z3py.py.

dimacs(self, include_names=True):

Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names)

Convert a solver into a DIMACS formatted string.

Parse assertions from a file

Definition at line 7268 of file z3py.py.

from_file(self, filename):

void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)

load solver assertions from a file.

Parse assertions from a string

Definition at line 7272 of file z3py.py.

from_string(self, s):

void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string str)

load solver assertions from a string.

Display a string describing all available options.

Definition at line 7399 of file z3py.py.

Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)

Return a string describing all solver available parameters.

Import model converter from other into the current solver

Definition at line 7196 of file z3py.py.

import_model_converter(self, other):

void Z3_API Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst)

Ad-hoc method for importing model conversion from solver.

Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.insert(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 7107 of file z3py.py.

insert(self, *args):

self.assert_exprs(*args)

Interrupt the execution of the solver object.
Remarks: This ensures that the interrupt applies only
to the given solver object and it applies only if it is running.

Definition at line 7200 of file z3py.py.

interrupt(self):

void Z3_API Z3_solver_interrupt(Z3_context c, Z3_solver s)

Solver local interrupt. Normally you should use Z3_interrupt to cancel solvers because only one solve...

Return a model for the last `check()`.

This function raises an exception if
a model is not available (e.g., last `check()` returned unsat).

>>> s = Solver()
>>> a = Int('a')
>>> s.add(a + 2 == 0)
>>> s.check()
sat
>>> s.model()
[a = -2]

Definition at line 7177 of file z3py.py.

Z3Exception(

)

Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)

Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.

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().

Definition at line 7312 of file z3py.py.

t = _py2expr(t, self.ctx)

Z3_ast Z3_API Z3_solver_congruence_next(Z3_context c, Z3_solver s, Z3_ast a)

retrieve the next expression in the congruence class. The set of congruent siblings form a cyclic lis...

Return an AST vector containing all atomic formulas in solver state that are not units.

Definition at line 7343 of file z3py.py.

non_units(self):

Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)

Return the set of non units in the solver state.

Return the current number of backtracking points.

>>> s = Solver()
>>> s.num_scopes()
0
>>> s.push()
>>> s.num_scopes()
1
>>> s.push()
>>> s.num_scopes()
2
>>> s.pop()
>>> s.num_scopes()
1

Definition at line 7030 of file z3py.py.

num_scopes(self):

unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)

Return the number of backtracking points.

Return the parameter description set.

Definition at line 7403 of file z3py.py.

param_descrs(self):

Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)

Return the parameter description set for the given solver object.

Backtrack \\c num backtracking points.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]

Definition at line 7008 of file z3py.py.

pop(self, num=1):

void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)

Backtrack n backtracking points.

Referenced by Solver.__exit__().

Return a proof for the last `check()`. Proof construction must be enabled.

Definition at line 7320 of file z3py.py.

Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)

Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.

Create a backtracking point.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]

Definition at line 6986 of file z3py.py.

void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)

Create a backtracking point.

Referenced by Solver.__enter__().

Return a string describing why the last `check()` returned `unknown`.

>>> x = Int('x')
>>> s = SimpleSolver()
>>> s.add(2**x == 4)
>>> s.check()
unknown
>>> s.reason_unknown()
'(incomplete (theory arithmetic))'

Definition at line 7386 of file z3py.py.

reason_unknown(self):

Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)

Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...

Remove all asserted constraints and backtracking points created using `push()`.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.reset()
>>> s
[]

Definition at line 7048 of file z3py.py.

void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)

Remove all assertions from the solver.

Definition at line 7304 of file z3py.py.

t = _py2expr(t, self.ctx)

Z3_ast Z3_API Z3_solver_congruence_root(Z3_context c, Z3_solver s, Z3_ast a)

retrieve the congruence closure root of an expression. The root is retrieved relative to the state wh...

Set a configuration option.
The method `help()` return a string containing all available options.

>>> s = Solver()
>>> # The option MBQI can be set using three different approaches.
>>> s.set(mbqi=True)
>>> s.set('MBQI', True)
>>> s.set(':mbqi', True)

Definition at line 6973 of file z3py.py.

set(self, *args, **keys):

void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)

Set the given solver using the given parameters.

def args2params(arguments, keywords, ctx=None)

initialize the solver's state by setting the initial value of var to value

Definition at line 7356 of file z3py.py.

set_initial_value(self, var, value):

value = s.cast(value)

void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast v, Z3_ast val)

provide an initialization hint to the solver. The initialization hint is used to calibrate an initial...

Return a formatted string (in Lisp-like format) with all added constraints.
We say the string is in s-expression format.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> r = s.sexpr()

Definition at line 7430 of file z3py.py.

Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)

Convert a solver into a string.

Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().

Return statistics for the last `check()`.

>>> s = SimpleSolver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> st.get_key_value('final checks')
1
>>> len(st) > 0
True
>>> st[0] != 0
True

Definition at line 7368 of file z3py.py.

statistics(self):

Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)

Return statistics for the given solver.

return SMTLIB2 formatted benchmark for solver's assertions

Definition at line 7446 of file z3py.py.

es = self.assertions()

i

(sz1):

v[i] = es[i].as_ast()

e = es[sz1].as_ast()

e =

(

, self.ctx).as_ast()

self.ctx.ref(),

,

,

,

, sz1, v, e,

Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)

Convert the given benchmark into SMT-LIB formatted string.

def BoolVal(val, ctx=None)

Return trail of the solver state after a check() call.

Definition at line 7363 of file z3py.py.

Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s)

Return the trail modulo model conversion, in order of decision level The decision level can be retrie...

Referenced by Solver.trail_levels().

Return trail and decision levels of the solver state after a check() call.

Definition at line 7348 of file z3py.py.

trail_levels(self):

trail = self.trail()

levels = (ctypes.c_uint * len(trail))()

trail, levels

void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[])

retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat c...

Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.

>>> c1 = Context()
>>> c2 = Context()
>>> s1 = Solver(ctx=c1)
>>> s2 = s1.translate(c2)

Definition at line 7411 of file z3py.py.

translate(self, target):

_z3_assert(isinstance(target, Context),

)

Solver(solver, target)

Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)

Copy a solver s from the context source to the context target.

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().

Return an AST vector containing all currently inferred units.

Definition at line 7338 of file z3py.py.

Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)

Return the set of units modulo model conversion.

Return a subset (as an AST vector) of the assumptions provided to the last check().

These are the assumptions Z3 used in the unsatisfiability proof.
Assumptions are available in Z3. They are used to extract unsatisfiable cores.
They may be also used to "retract" assumptions. Note that, assumptions are not really
"soft constraints", but they can be used to implement them.

>>> p1, p2, p3 = Bools('p1 p2 p3')
>>> x, y       = Ints('x y')
>>> s          = Solver()
>>> s.add(Implies(p1, x > 0))
>>> s.add(Implies(p2, y > x))
>>> s.add(Implies(p2, y < 1))
>>> s.add(Implies(p3, y > -3))
>>> s.check(p1, p2, p3)
unsat
>>> core = s.unsat_core()
>>> len(core)
2
>>> p1 in core
True
>>> p2 in core
True
>>> p3 in core
False
>>> # "Retracting" p2
>>> s.check(p1, p3)
sat

Definition at line 7207 of file z3py.py.

unsat_core(self):

Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)

Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...

Definition at line 6951 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(), Solver.interrupt(), 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(), QuantifierRef.qid(), 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(), Solver.set_initial_value(), Optimize.set_initial_value(), 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(), QuantifierRef.skolem_id(), 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().

Definition at line 6953 of file z3py.py.

Referenced by Solver.__del__(), UserPropagateBase.add(), UserPropagateBase.add_created(), UserPropagateBase.add_decide(), UserPropagateBase.add_diseq(), UserPropagateBase.add_eq(), UserPropagateBase.add_final(), UserPropagateBase.add_fixed(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.assertions(), Solver.check(), Solver.consequences(), UserPropagateBase.ctx(), Solver.dimacs(), Solver.from_file(), Solver.from_string(), Solver.help(), Solver.import_model_converter(), Solver.interrupt(), Solver.model(), Solver.next(), Solver.non_units(), Solver.num_scopes(), Solver.param_descrs(), Solver.pop(), Solver.proof(), Solver.push(), Solver.reason_unknown(), Solver.reset(), Solver.root(), Solver.set(), Solver.set_initial_value(), Solver.sexpr(), Solver.statistics(), Solver.trail(), Solver.trail_levels(), Solver.translate(), Solver.units(), and Solver.unsat_core().

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4