Z3
 
Loading...
Searching...
No Matches
Fixedpoint Class Reference

Fixedpoint. More...

+ Inheritance diagram for Fixedpoint:

Public Member Functions

 __init__ (self, fixedpoint=None, ctx=None)
 
 __deepcopy__ (self, memo={})
 
 __del__ (self)
 
 set (self, *args, **keys)
 
 help (self)
 
 param_descrs (self)
 
 assert_exprs (self, *args)
 
 add (self, *args)
 
 __iadd__ (self, fml)
 
 append (self, *args)
 
 insert (self, *args)
 
 add_rule (self, head, body=None, name=None)
 
 rule (self, head, body=None, name=None)
 
 fact (self, head, name=None)
 
 query (self, *query)
 
 query_from_lvl (self, lvl, *query)
 
 update_rule (self, head, body, name)
 
 get_answer (self)
 
 get_ground_sat_answer (self)
 
 get_rules_along_trace (self)
 
 get_rule_names_along_trace (self)
 
 get_num_levels (self, predicate)
 
 get_cover_delta (self, level, predicate)
 
 add_cover (self, level, predicate, property)
 
 register_relation (self, *relations)
 
 set_predicate_representation (self, f, *representations)
 
 parse_string (self, s)
 
 parse_file (self, f)
 
 get_rules (self)
 
 get_assertions (self)
 
 __repr__ (self)
 
 sexpr (self)
 
 to_string (self, queries)
 
 statistics (self)
 
 reason_unknown (self)
 
 declare_var (self, *vars)
 
 abstract (self, fml, is_forall=True)
 
- Public Member Functions inherited from Z3PPObject
 use_pp (self)
 

Data Fields

 ctx = _get_ctx(ctx)
 
 fixedpoint = None
 
list vars = []
 

Additional Inherited Members

- Protected Member Functions inherited from Z3PPObject
 _repr_html_ (self)
 

Detailed Description

Fixedpoint.

Fixedpoint API provides methods for solving with recursive predicates

Definition at line 7591 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

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

Definition at line 7594 of file z3py.py.

7594 def __init__(self, fixedpoint=None, ctx=None):
7595 assert fixedpoint is None or ctx is not None
7596 self.ctx = _get_ctx(ctx)
7597 self.fixedpoint = None
7598 if fixedpoint is None:
7599 self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
7600 else:
7601 self.fixedpoint = fixedpoint
7602 Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
7603 self.vars = []
7604
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__()

__del__ ( self)

Definition at line 7608 of file z3py.py.

7608 def __del__(self):
7609 if self.fixedpoint is not None and self.ctx.ref() is not None and Z3_fixedpoint_dec_ref is not None:
7610 Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
7611
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.

Member Function Documentation

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 7605 of file z3py.py.

7605 def __deepcopy__(self, memo={}):
7606 return FixedPoint(self.fixedpoint, self.ctx)
7607

◆ __iadd__()

__iadd__ ( self,
fml )

Definition at line 7644 of file z3py.py.

7644 def __iadd__(self, fml):
7645 self.add(fml)
7646 return self
7647

◆ __repr__()

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

Definition at line 7805 of file z3py.py.

7805 def __repr__(self):
7806 """Return a formatted string with all added rules and constraints."""
7807 return self.sexpr()
7808

◆ abstract()

abstract ( self,
fml,
is_forall = True )

Definition at line 7842 of file z3py.py.

7842 def abstract(self, fml, is_forall=True):
7843 if self.vars == []:
7844 return fml
7845 if is_forall:
7846 return ForAll(self.vars, fml)
7847 else:
7848 return Exists(self.vars, fml)
7849
7850

◆ add()

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

Definition at line 7640 of file z3py.py.

7640 def add(self, *args):
7641 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7642 self.assert_exprs(*args)
7643

◆ add_cover()

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

Definition at line 7767 of file z3py.py.

7767 def add_cover(self, level, predicate, property):
7768 """Add property to predicate for the level'th unfolding.
7769 -1 is treated as infinity (infinity)
7770 """
7771 Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
7772
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()

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

7656 def add_rule(self, head, body=None, name=None):
7657 """Assert rules defining recursive predicates to the fixedpoint solver.
7658 >>> a = Bool('a')
7659 >>> b = Bool('b')
7660 >>> s = Fixedpoint()
7661 >>> s.register_relation(a.decl())
7662 >>> s.register_relation(b.decl())
7663 >>> s.fact(a)
7664 >>> s.rule(b, a)
7665 >>> s.query(b)
7666 sat
7667 """
7668 if name is None:
7669 name = ""
7670 name = to_symbol(name, self.ctx)
7671 if body is None:
7672 head = self.abstract(head)
7673 Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
7674 else:
7675 body = _get_args(body)
7676 f = self.abstract(Implies(And(body, self.ctx), head))
7677 Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
7678
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:

◆ append()

append ( self,
* args )
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 7648 of file z3py.py.

7648 def append(self, *args):
7649 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7650 self.assert_exprs(*args)
7651

◆ assert_exprs()

assert_exprs ( self,
* args )
Assert constraints as background axioms for the fixedpoint solver.

Definition at line 7626 of file z3py.py.

7626 def assert_exprs(self, *args):
7627 """Assert constraints as background axioms for the fixedpoint solver."""
7628 args = _get_args(args)
7629 s = BoolSort(self.ctx)
7630 for arg in args:
7631 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7632 for f in arg:
7633 f = self.abstract(f)
7634 Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
7635 else:
7636 arg = s.cast(arg)
7637 arg = self.abstract(arg)
7638 Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
7639
void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom)
Assert a constraint to the fixedpoint context.

◆ declare_var()

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

7833 def declare_var(self, *vars):
7834 """Add variable or several variables.
7835 The added variable or variables will be bound in the rules
7836 and queries
7837 """
7838 vars = _get_args(vars)
7839 for v in vars:
7840 self.vars += [v]
7841

◆ fact()

fact ( self,
head,
name = None )
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 7683 of file z3py.py.

7683 def fact(self, head, name=None):
7684 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7685 self.add_rule(head, None, name)
7686

◆ get_answer()

get_answer ( self)
Retrieve answer from last query call.

Definition at line 7734 of file z3py.py.

7734 def get_answer(self):
7735 """Retrieve answer from last query call."""
7736 r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
7737 return _to_expr_ref(r, self.ctx)
7738
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()

get_assertions ( self)
retrieve assertions that have been added to fixedpoint context

Definition at line 7801 of file z3py.py.

7801 def get_assertions(self):
7802 """retrieve assertions that have been added to fixedpoint context"""
7803 return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
7804
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()

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

7760 def get_cover_delta(self, level, predicate):
7761 """Retrieve properties known about predicate for the level'th unfolding.
7762 -1 is treated as the limit (infinity)
7763 """
7764 r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
7765 return _to_expr_ref(r, self.ctx)
7766
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()

get_ground_sat_answer ( self)
Retrieve a ground cex from last query call.

Definition at line 7739 of file z3py.py.

7739 def get_ground_sat_answer(self):
7740 """Retrieve a ground cex from last query call."""
7741 r = Z3_fixedpoint_get_ground_sat_answer(self.ctx.ref(), self.fixedpoint)
7742 return _to_expr_ref(r, self.ctx)
7743

◆ get_num_levels()

get_num_levels ( self,
predicate )
Retrieve number of levels used for predicate in PDR engine

Definition at line 7756 of file z3py.py.

7756 def get_num_levels(self, predicate):
7757 """Retrieve number of levels used for predicate in PDR engine"""
7758 return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
7759
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()

get_rule_names_along_trace ( self)
retrieve rule names along the counterexample trace

Definition at line 7748 of file z3py.py.

7748 def get_rule_names_along_trace(self):
7749 """retrieve rule names along the counterexample trace"""
7750 # this is a hack as I don't know how to return a list of symbols from C++;
7751 # obtain names as a single string separated by semicolons
7752 names = _symbol2py(self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))
7753 # split into individual names
7754 return names.split(";")
7755

◆ get_rules()

get_rules ( self)
retrieve rules that have been added to fixedpoint context

Definition at line 7797 of file z3py.py.

7797 def get_rules(self):
7798 """retrieve rules that have been added to fixedpoint context"""
7799 return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
7800
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()

get_rules_along_trace ( self)
retrieve rules along the counterexample trace

Definition at line 7744 of file z3py.py.

7744 def get_rules_along_trace(self):
7745 """retrieve rules along the counterexample trace"""
7746 return AstVector(Z3_fixedpoint_get_rules_along_trace(self.ctx.ref(), self.fixedpoint), self.ctx)
7747

◆ help()

help ( self)
Display a string describing all available options.

Definition at line 7618 of file z3py.py.

7618 def help(self):
7619 """Display a string describing all available options."""
7620 print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint))
7621
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.

◆ insert()

insert ( self,
* args )
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 7652 of file z3py.py.

7652 def insert(self, *args):
7653 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7654 self.assert_exprs(*args)
7655

◆ param_descrs()

param_descrs ( self)
Return the parameter description set.

Definition at line 7622 of file z3py.py.

7622 def param_descrs(self):
7623 """Return the parameter description set."""
7624 return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
7625
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()

parse_file ( self,
f )
Parse rules and queries from a file

Definition at line 7793 of file z3py.py.

7793 def parse_file(self, f):
7794 """Parse rules and queries from a file"""
7795 return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
7796
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()

parse_string ( self,
s )
Parse rules and queries from a string

Definition at line 7789 of file z3py.py.

7789 def parse_string(self, s):
7790 """Parse rules and queries from a string"""
7791 return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
7792
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()

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

7687 def query(self, *query):
7688 """Query the fixedpoint engine whether formula is derivable.
7689 You can also pass an tuple or list of recursive predicates.
7690 """
7691 query = _get_args(query)
7692 sz = len(query)
7693 if sz >= 1 and isinstance(query[0], FuncDeclRef):
7694 _decls = (FuncDecl * sz)()
7695 i = 0
7696 for q in query:
7697 _decls[i] = q.ast
7698 i = i + 1
7699 r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
7700 else:
7701 if sz == 1:
7702 query = query[0]
7703 else:
7704 query = And(query, self.ctx)
7705 query = self.abstract(query, False)
7706 r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
7707 return CheckSatResult(r)
7708
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()

query_from_lvl ( self,
lvl,
* query )
Query the fixedpoint engine whether formula is derivable starting at the given query level.

Definition at line 7709 of file z3py.py.

7709 def query_from_lvl(self, lvl, *query):
7710 """Query the fixedpoint engine whether formula is derivable starting at the given query level.
7711 """
7712 query = _get_args(query)
7713 sz = len(query)
7714 if sz >= 1 and isinstance(query[0], FuncDecl):
7715 _z3_assert(False, "unsupported")
7716 else:
7717 if sz == 1:
7718 query = query[0]
7719 else:
7720 query = And(query)
7721 query = self.abstract(query, False)
7722 r = Z3_fixedpoint_query_from_lvl(self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
7723 return CheckSatResult(r)
7724

◆ reason_unknown()

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

Definition at line 7828 of file z3py.py.

7828 def reason_unknown(self):
7829 """Return a string describing why the last `query()` returned `unknown`.
7830 """
7831 return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
7832
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()

register_relation ( self,
* relations )
Register relation as recursive

Definition at line 7773 of file z3py.py.

7773 def register_relation(self, *relations):
7774 """Register relation as recursive"""
7775 relations = _get_args(relations)
7776 for f in relations:
7777 Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
7778
void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...

◆ rule()

rule ( self,
head,
body = None,
name = None )
Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 7679 of file z3py.py.

7679 def rule(self, head, body=None, name=None):
7680 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7681 self.add_rule(head, body, name)
7682

◆ set()

set ( self,
* args,
** keys )
Set a configuration option. The method `help()` return a string containing all available options.

Definition at line 7612 of file z3py.py.

7612 def set(self, *args, **keys):
7613 """Set a configuration option. The method `help()` return a string containing all available options.
7614 """
7615 p = args2params(args, keys, self.ctx)
7616 Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
7617
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.

◆ set_predicate_representation()

set_predicate_representation ( self,
f,
* representations )
Control how relation is represented

Definition at line 7779 of file z3py.py.

7779 def set_predicate_representation(self, f, *representations):
7780 """Control how relation is represented"""
7781 representations = _get_args(representations)
7782 representations = [to_symbol(s) for s in representations]
7783 sz = len(representations)
7784 args = (Symbol * sz)()
7785 for i in range(sz):
7786 args[i] = representations[i]
7787 Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
7788
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.

◆ sexpr()

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

7809 def sexpr(self):
7810 """Return a formatted string (in Lisp-like format) with all added constraints.
7811 We say the string is in s-expression format.
7812 """
7813 return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
7814
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.

◆ statistics()

statistics ( self)
Return statistics for the last `query()`.

Definition at line 7823 of file z3py.py.

7823 def statistics(self):
7824 """Return statistics for the last `query()`.
7825 """
7826 return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
7827
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()

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

7815 def to_string(self, queries):
7816 """Return a formatted string (in Lisp-like format) with all added constraints.
7817 We say the string is in s-expression format.
7818 Include also queries.
7819 """
7820 args, len = _to_ast_array(queries)
7821 return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
7822

◆ update_rule()

update_rule ( self,
head,
body,
name )
update rule

Definition at line 7725 of file z3py.py.

7725 def update_rule(self, head, body, name):
7726 """update rule"""
7727 if name is None:
7728 name = ""
7729 name = to_symbol(name, self.ctx)
7730 body = _get_args(body)
7731 f = self.abstract(Implies(And(body, self.ctx), head))
7732 Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
7733
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.

Field Documentation

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 7596 of file z3py.py.

◆ fixedpoint

fixedpoint = None

Definition at line 7597 of file z3py.py.

◆ vars

vars = []

Definition at line 7603 of file z3py.py.