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) | |
![]() | |
use_pp (self) | |
Data Fields | |
ctx = _get_ctx(ctx) | |
fixedpoint = None | |
list | vars = [] |
Additional Inherited Members | |
![]() | |
_repr_html_ (self) | |
Fixedpoint API provides methods for solving with recursive predicates
__init__ | ( | self, | |
fixedpoint = None, | |||
ctx = None ) |
Definition at line 7594 of file z3py.py.
__del__ | ( | self | ) |
Definition at line 7608 of file z3py.py.
__deepcopy__ | ( | self, | |
memo = {} ) |
__iadd__ | ( | self, | |
fml ) |
__repr__ | ( | self | ) |
abstract | ( | self, | |
fml, | |||
is_forall = True ) |
add | ( | self, | |
* | args ) |
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.
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.
append | ( | self, | |
* | args ) |
assert_exprs | ( | self, | |
* | args ) |
Assert constraints as background axioms for the fixedpoint solver.
Definition at line 7626 of file z3py.py.
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.
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.
get_answer | ( | self | ) |
Retrieve answer from last query call.
Definition at line 7734 of file z3py.py.
get_assertions | ( | self | ) |
retrieve assertions that have been added to fixedpoint context
Definition at line 7801 of file z3py.py.
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.
get_ground_sat_answer | ( | self | ) |
get_num_levels | ( | self, | |
predicate ) |
Retrieve number of levels used for predicate in PDR engine
Definition at line 7756 of file z3py.py.
get_rule_names_along_trace | ( | self | ) |
retrieve rule names along the counterexample trace
Definition at line 7748 of file z3py.py.
get_rules | ( | self | ) |
retrieve rules that have been added to fixedpoint context
Definition at line 7797 of file z3py.py.
get_rules_along_trace | ( | self | ) |
help | ( | self | ) |
Display a string describing all available options.
Definition at line 7618 of file z3py.py.
insert | ( | self, | |
* | args ) |
param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 7622 of file z3py.py.
parse_file | ( | self, | |
f ) |
Parse rules and queries from a file
Definition at line 7793 of file z3py.py.
parse_string | ( | self, | |
s ) |
Parse rules and queries from a string
Definition at line 7789 of file z3py.py.
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.
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.
reason_unknown | ( | self | ) |
Return a string describing why the last `query()` returned `unknown`.
Definition at line 7828 of file z3py.py.
register_relation | ( | self, | |
* | relations ) |
Register relation as recursive
Definition at line 7773 of file z3py.py.
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.
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.
set_predicate_representation | ( | self, | |
f, | |||
* | representations ) |
Control how relation is represented
Definition at line 7779 of file z3py.py.
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.
statistics | ( | self | ) |
Return statistics for the last `query()`.
Definition at line 7823 of file z3py.py.
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.
update_rule | ( | self, | |
head, | |||
body, | |||
name ) |
update rule
Definition at line 7725 of file z3py.py.