Public Member Functions | |
def | __init__ (self, fixedpoint=None, ctx=None) |
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 | 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 | push (self) |
def | pop (self) |
def | update_rule (self, head, body, name) |
def | get_answer (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) |
Data Fields | |
ctx | |
fixedpoint | |
vars | |
Fixedpoint API provides methods for solving with recursive predicates
def __init__ | ( | self, | |
fixedpoint = None , |
|||
ctx = None |
|||
) |
def __del__ | ( | self | ) |
def __repr__ | ( | self | ) |
def abstract | ( | self, | |
fml, | |||
is_forall = True |
|||
) |
Definition at line 6363 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), Fixedpoint.query(), and Fixedpoint.update_rule().
def add | ( | self, | |
args | |||
) |
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 6291 of file z3py.py.
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 6207 of file z3py.py.
Referenced by Fixedpoint.fact(), and Fixedpoint.rule().
def append | ( | self, | |
args | |||
) |
def assert_exprs | ( | self, | |
args | |||
) |
Assert constraints as background axioms for the fixedpoint solver.
Definition at line 6181 of file z3py.py.
Referenced by Fixedpoint.add(), Optimize.add(), Fixedpoint.append(), and Fixedpoint.insert().
def declare_var | ( | self, | |
vars | |||
) |
def fact | ( | self, | |
head, | |||
name = None |
|||
) |
def get_answer | ( | self | ) |
def get_assertions | ( | self | ) |
retrieve assertions that have been added to fixedpoint context
Definition at line 6323 of file z3py.py.
def get_cover_delta | ( | self, | |
level, | |||
predicate | |||
) |
Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)
def get_num_levels | ( | self, | |
predicate | |||
) |
def get_rules | ( | self | ) |
retrieve rules that have been added to fixedpoint context
Definition at line 6319 of file z3py.py.
def help | ( | self | ) |
def insert | ( | self, | |
args | |||
) |
def param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 6177 of file z3py.py.
def parse_file | ( | self, | |
f | |||
) |
Parse rules and queries from a file
Definition at line 6315 of file z3py.py.
def parse_string | ( | self, | |
s | |||
) |
Parse rules and queries from a string
Definition at line 6311 of file z3py.py.
def pop | ( | self | ) |
def push | ( | self | ) |
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 6238 of file z3py.py.
def reason_unknown | ( | self | ) |
def register_relation | ( | self, | |
relations | |||
) |
def rule | ( | self, | |
head, | |||
body = None , |
|||
name = None |
|||
) |
def set | ( | self, | |
args, | |||
keys | |||
) |
Set a configuration option. The method `help()` return a string containing all available options.
def set_predicate_representation | ( | self, | |
f, | |||
representations | |||
) |
Control how relation is represented
Definition at line 6301 of file z3py.py.
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 6331 of file z3py.py.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
def statistics | ( | self | ) |
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 6336 of file z3py.py.
def update_rule | ( | self, | |
head, | |||
body, | |||
name | |||
) |
ctx |
Definition at line 6154 of file z3py.py.
Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), ApplyResult.convert_model(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), Optimize.model(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), and Fixedpoint.update_rule().
fixedpoint |
Definition at line 6155 of file z3py.py.
Referenced by Fixedpoint.__del__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_num_levels(), Fixedpoint.get_rules(), Fixedpoint.help(), Fixedpoint.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.pop(), Fixedpoint.push(), Fixedpoint.query(), Fixedpoint.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Fixedpoint.statistics(), Fixedpoint.to_string(), and Fixedpoint.update_rule().
vars |
Definition at line 6161 of file z3py.py.
Referenced by Fixedpoint.abstract(), and Fixedpoint.declare_var().