RetroSearch Browse

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

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

Z3: Fixedpoint Class Reference

def __init__ (self, fixedpoint=None, 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 append (self, *args) def insert (self, *args) def add_rule (self, head, body=None, name=None) def rule (self, head, body=None, name=None) def fact (self, head, name=None) def query (self, *query) def query_from_lvl (self, lvl, *query) def update_rule (self, head, body, name) def get_answer (self) def get_ground_sat_answer (self) def get_rules_along_trace (self) def get_rule_names_along_trace (self) def get_num_levels (self, predicate) def get_cover_delta (self, level, predicate) def add_cover (self, level, predicate, property) def register_relation (self, *relations) def set_predicate_representation (self, f, *representations) def parse_string (self, s) def parse_file (self, f) def get_rules (self) def get_assertions (self) def __repr__ (self) def sexpr (self) def to_string (self, queries) def statistics (self) def reason_unknown (self) def declare_var (self, *vars) def abstract (self, fml, is_forall=True) def use_pp (self)

Fixedpoint.

Fixedpoint API provides methods for solving with recursive predicates

Definition at line 7505 of file z3py.py.

◆ __init__() def __init__ ( self, fixedpoint = None, ctx = None )

Definition at line 7508 of file z3py.py.

7508 def

__init__(self, fixedpoint=None, ctx=None):

7509 assert

fixedpoint

is None or

ctx

is not None 7510

self.ctx = _get_ctx(ctx)

7511

self.fixedpoint =

None 7512 if

fixedpoint

is None

7515

self.fixedpoint = fixedpoint

void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)

Increment the reference counter of the given fixedpoint context.

Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)

Create a new fixedpoint context.

◆ __del__()

Definition at line 7522 of file z3py.py.

7523 if

self.fixedpoint

is not None and

self.ctx.ref()

is not None and

Z3_fixedpoint_dec_ref

is not None

void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)

Decrement the reference counter of the given fixedpoint context.

◆ __deepcopy__() def __deepcopy__ ( self, memo = {} )

Definition at line 7519 of file z3py.py.

7519 def

__deepcopy__(self, memo={}):

7520 return

FixedPoint(self.fixedpoint, self.ctx)

◆ __iadd__() def __iadd__ ( self, fml )

Definition at line 7558 of file z3py.py.

7558 def

__iadd__(self, fml):

◆ __repr__()

Return a formatted string with all added rules and constraints.

Definition at line 7719 of file z3py.py.

7720 """Return a formatted string with all added rules and constraints.""" ◆ abstract() def abstract ( self, fml, is_forall = True )

Definition at line 7756 of file z3py.py.

7756 def

abstract(self, fml, is_forall=True):

7760 return ForAll

(self.vars, fml)

7762 return Exists

(self.vars, fml)

def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])

def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])

Referenced by Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), and Fixedpoint.update_rule().

◆ add()

Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 7554 of file z3py.py.

7554 def

add(self, *args):

7555 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 7556

self.assert_exprs(*args)

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

◆ add_cover() def add_cover ( self, level, predicate, property )

Add property to predicate for the level'th unfolding.
-1 is treated as infinity (infinity)

Definition at line 7681 of file z3py.py.

7681 def

add_cover(self, level, predicate, property):

7682 """Add property to predicate for the level'th unfolding. 7683 -1 is treated as infinity (infinity)

void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)

Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...

◆ add_rule() def add_rule ( self, head, body = None, name = None )

Assert rules defining recursive predicates to the fixedpoint solver.
>>> a = Bool('a')
>>> b = Bool('b')
>>> s = Fixedpoint()
>>> s.register_relation(a.decl())
>>> s.register_relation(b.decl())
>>> s.fact(a)
>>> s.rule(b, a)
>>> s.query(b)
sat

Definition at line 7570 of file z3py.py.

7570 def

add_rule(self, head, body=None, name=None):

7571 """Assert rules defining recursive predicates to the fixedpoint solver. 7574 >>> s = Fixedpoint() 7575 >>> s.register_relation(a.decl()) 7576 >>> s.register_relation(b.decl()) 7586

head = self.abstract(head)

7589

body = _get_args(body)

7590

f = self.abstract(

Implies

(

And

(body, self.ctx), head))

void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)

Add a universal Horn clause as a named rule. The horn_rule should be of the form:

def Implies(a, b, ctx=None)

def to_symbol(s, ctx=None)

Referenced by Fixedpoint.fact(), and Fixedpoint.rule().

◆ append() def append ( self, * args )

Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 7562 of file z3py.py.

7562 def

append(self, *args):

7563 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 7564

self.assert_exprs(*args)

◆ assert_exprs() def assert_exprs ( self, * args )

Assert constraints as background axioms for the fixedpoint solver.

Definition at line 7540 of file z3py.py.

7540 def

assert_exprs(self, *args):

7541 """Assert constraints as background axioms for the fixedpoint solver.""" 7542

args = _get_args(args)

7545 if

isinstance(arg, Goal)

or

isinstance(arg, AstVector):

7547

f = self.abstract(f)

7551

arg = self.abstract(arg)

void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom)

Assert a constraint to the fixedpoint context.

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

◆ declare_var() def declare_var ( self, * vars )

Add variable or several variables.
The added variable or variables will be bound in the rules
and queries

Definition at line 7747 of file z3py.py.

7747 def

declare_var(self, *vars):

7748 """Add variable or several variables. 7749 The added variable or variables will be bound in the rules 7752

vars = _get_args(vars)

◆ fact() def fact ( self, head, name = None )

Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 7597 of file z3py.py.

7597 def

fact(self, head, name=None):

7598 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 7599

self.add_rule(head,

None

, name)

◆ get_answer()

Retrieve answer from last query call.

Definition at line 7648 of file z3py.py.

7648 def

get_answer(self):

7649 """Retrieve answer from last query call.""" 7651 return

_to_expr_ref(r, self.ctx)

Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)

Retrieve a formula that encodes satisfying answers to the query.

◆ get_assertions() def get_assertions ( self )

retrieve assertions that have been added to fixedpoint context

Definition at line 7715 of file z3py.py.

7715 def

get_assertions(self):

7716 """retrieve assertions that have been added to fixedpoint context"""

Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)

Retrieve set of background assertions from fixedpoint context.

◆ get_cover_delta() def get_cover_delta ( self, level, predicate )

Retrieve properties known about predicate for the level'th unfolding.
-1 is treated as the limit (infinity)

Definition at line 7674 of file z3py.py.

7674 def

get_cover_delta(self, level, predicate):

7675 """Retrieve properties known about predicate for the level'th unfolding. 7676 -1 is treated as the limit (infinity) 7679 return

_to_expr_ref(r, self.ctx)

Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)

◆ get_ground_sat_answer() def get_ground_sat_answer ( self )

Retrieve a ground cex from last query call.

Definition at line 7653 of file z3py.py.

7653 def

get_ground_sat_answer(self):

7654 """Retrieve a ground cex from last query call.""" 7655

r = Z3_fixedpoint_get_ground_sat_answer(self.ctx.ref(), self.fixedpoint)

7656 return

_to_expr_ref(r, self.ctx)

◆ get_num_levels() def get_num_levels ( self, predicate )

Retrieve number of levels used for predicate in PDR engine

Definition at line 7670 of file z3py.py.

7670 def

get_num_levels(self, predicate):

7671 """Retrieve number of levels used for predicate in PDR engine"""

unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)

Query the PDR engine for the maximal levels properties are known about predicate.

◆ get_rule_names_along_trace() def get_rule_names_along_trace ( self )

retrieve rule names along the counterexample trace

Definition at line 7662 of file z3py.py.

7662 def

get_rule_names_along_trace(self):

7663 """retrieve rule names along the counterexample trace""" 7666

names = _symbol2py(self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))

7668 return

names.split(

";"

)

◆ get_rules()

retrieve rules that have been added to fixedpoint context

Definition at line 7711 of file z3py.py.

7711 def

get_rules(self):

7712 """retrieve rules that have been added to fixedpoint context"""

Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)

Retrieve set of rules from fixedpoint context.

◆ get_rules_along_trace() def get_rules_along_trace ( self )

retrieve rules along the counterexample trace

Definition at line 7658 of file z3py.py.

7658 def

get_rules_along_trace(self):

7659 """retrieve rules along the counterexample trace""" 7660 return

AstVector(Z3_fixedpoint_get_rules_along_trace(self.ctx.ref(), self.fixedpoint), self.ctx)

◆ help()

Display a string describing all available options.

Definition at line 7532 of file z3py.py.

7533 """Display a string describing all available options."""

Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)

Return a string describing all fixedpoint available parameters.

◆ insert() def insert ( self, * args )

Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 7566 of file z3py.py.

7566 def

insert(self, *args):

7567 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 7568

self.assert_exprs(*args)

◆ param_descrs() def param_descrs ( self )

Return the parameter description set.

Definition at line 7536 of file z3py.py.

7536 def

param_descrs(self):

7537 """Return the parameter description set."""

Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f)

Return the parameter description set for the given fixedpoint object.

◆ parse_file() def parse_file ( self, f )

Parse rules and queries from a file

Definition at line 7707 of file z3py.py.

7707 def

parse_file(self, f):

7708 """Parse rules and queries from a file"""

Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, Z3_string s)

Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context....

◆ parse_string() def parse_string ( self, s )

Parse rules and queries from a string

Definition at line 7703 of file z3py.py.

7703 def

parse_string(self, s):

7704 """Parse rules and queries from a string"""

Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s)

Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context....

◆ query() def query ( self, * query )

Query the fixedpoint engine whether formula is derivable.
   You can also pass an tuple or list of recursive predicates.

Definition at line 7601 of file z3py.py.

7601 def

query(self, *query):

7602 """Query the fixedpoint engine whether formula is derivable. 7603 You can also pass an tuple or list of recursive predicates. 7605

query = _get_args(query)

7607 if

sz >= 1

and

isinstance(query[0], FuncDeclRef):

7608

_decls = (FuncDecl * sz)()

7618

query =

And

(query, self.ctx)

7619

query = self.abstract(query,

False

)

7621 return

CheckSatResult(r)

Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)

Pose a query against the asserted rules.

Z3_lbool Z3_API Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, unsigned num_relations, Z3_func_decl const relations[])

Pose multiple queries against the asserted rules.

◆ query_from_lvl() def query_from_lvl ( self, lvl, * query )

Query the fixedpoint engine whether formula is derivable starting at the given query level.

Definition at line 7623 of file z3py.py.

7623 def

query_from_lvl(self, lvl, *query):

7624 """Query the fixedpoint engine whether formula is derivable starting at the given query level. 7626

query = _get_args(query)

7628 if

sz >= 1

and

isinstance(query[0], FuncDecl):

7629

_z3_assert(

False

"unsupported"

)

7635

query = self.abstract(query,

False

)

7636

r = Z3_fixedpoint_query_from_lvl(self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)

7637 return

CheckSatResult(r)

◆ reason_unknown() def reason_unknown ( self )

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

Definition at line 7742 of file z3py.py.

7742 def

reason_unknown(self):

7743 """Return a string describing why the last `query()` returned `unknown`.

Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d)

Retrieve a string that describes the last status returned by Z3_fixedpoint_query.

◆ register_relation() def register_relation ( self, * relations )

Register relation as recursive

Definition at line 7687 of file z3py.py.

7687 def

register_relation(self, *relations):

7688 """Register relation as recursive""" 7689

relations = _get_args(relations)

void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f)

◆ rule() def rule ( self, head, body = None, name = None )

Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 7593 of file z3py.py.

7593 def

rule(self, head, body=None, name=None):

7594 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" 7595

self.add_rule(head, body, name)

◆ set() def set ( self, * args, ** keys )

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

Definition at line 7526 of file z3py.py.

7526 def

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

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

void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)

Set parameters on fixedpoint context.

def args2params(arguments, keywords, ctx=None)

◆ set_predicate_representation() def set_predicate_representation ( self, f, * representations )

Control how relation is represented

Definition at line 7693 of file z3py.py.

7693 def

set_predicate_representation(self, f, *representations):

7694 """Control how relation is represented""" 7695

representations = _get_args(representations)

7696

representations = [

to_symbol

(s)

for

in

representations]

7697

sz = len(representations)

7698

args = (Symbol * sz)()

7699 for

in range

(sz):

7700

args[i] = representations[i]

void Z3_API Z3_fixedpoint_set_predicate_representation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f, unsigned num_relations, Z3_symbol const relation_kinds[])

Configure the predicate representation.

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

◆ sexpr()

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

Definition at line 7723 of file z3py.py.

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

Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])

Print the current rules and background axioms as a string.

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

◆ statistics()

Return statistics for the last `query()`.

Definition at line 7737 of file z3py.py.

7737 def

statistics(self):

7738 """Return statistics for the last `query()`.

Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d)

Retrieve statistics information from the last call to Z3_fixedpoint_query.

◆ to_string() def to_string ( self, queries )

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

Definition at line 7729 of file z3py.py.

7729 def

to_string(self, queries):

7730 """Return a formatted string (in Lisp-like format) with all added constraints. 7731 We say the string is in s-expression format. 7732 Include also queries. 7734

args, len = _to_ast_array(queries)

◆ update_rule() def update_rule ( self, head, body, name )

update rule

Definition at line 7639 of file z3py.py.

7639 def

update_rule(self, head, body, name):

7644

body = _get_args(body)

7645

f = self.abstract(

Implies

(

And

(body, self.ctx), head))

void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name)

Update a named rule. A rule with the same name must have been previously created.

◆ ctx

Definition at line 7510 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().

◆ fixedpoint

Definition at line 7511 of file z3py.py.

Referenced by Fixedpoint.__deepcopy__(), Fixedpoint.__del__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Fixedpoint.help(), Fixedpoint.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Fixedpoint.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Fixedpoint.statistics(), Fixedpoint.to_string(), and Fixedpoint.update_rule().

◆ vars

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