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 | __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 | 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 __del__ | ( | self | ) |
def __iadd__ | ( | self, | |
fml | |||
) |
def __repr__ | ( | self | ) |
def abstract | ( | self, | |
fml, | |||
is_forall = True |
|||
) |
Definition at line 6537 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), Fixedpoint.query(), and Fixedpoint.update_rule().
def add | ( | self, | |
args | |||
) |
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
Definition at line 6365 of file z3py.py.
Referenced by Fixedpoint.__iadd__(), and Optimize.__iadd__().
def add_cover | ( | self, | |
level, | |||
predicate, | |||
property | |||
) |
Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)
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 6381 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 6351 of file z3py.py.
Referenced by Fixedpoint.add(), Optimize.add(), Fixedpoint.append(), and Fixedpoint.insert().
def declare_var | ( | self, | |
vars | |||
) |
Add variable or several variables. The added variable or variables will be bound in the rules and queries
def fact | ( | self, | |
head, | |||
name = None |
|||
) |
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.
def get_answer | ( | self | ) |
def get_assertions | ( | self | ) |
retrieve assertions that have been added to fixedpoint context
def get_cover_delta | ( | self, | |
level, | |||
predicate | |||
) |
def get_num_levels | ( | self, | |
predicate | |||
) |
Retrieve number of levels used for predicate in PDR engine
def get_rules | ( | self | ) |
def help | ( | self | ) |
def insert | ( | self, | |
args | |||
) |
def param_descrs | ( | self | ) |
def parse_file | ( | self, | |
f | |||
) |
def parse_string | ( | self, | |
s | |||
) |
def pop | ( | self | ) |
def push | ( | self | ) |
def query | ( | self, | |
query | |||
) |
def reason_unknown | ( | self | ) |
Return a string describing why the last `query()` returned `unknown`.
def register_relation | ( | self, | |
relations | |||
) |
Register relation as recursive
def rule | ( | self, | |
head, | |||
body = None , |
|||
name = None |
|||
) |
Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.
def set | ( | self, | |
args, | |||
keys | |||
) |
def set_predicate_representation | ( | self, | |
f, | |||
representations | |||
) |
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 6505 of file z3py.py.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
def statistics | ( | self | ) |
def to_string | ( | self, | |
queries | |||
) |
ctx |
Definition at line 6324 of file z3py.py.
Referenced by Probe.__call__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), ApplyResult.convert_model(), Optimize.from_file(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_num_levels(), Fixedpoint.get_rules(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.pop(), Optimize.pop(), Fixedpoint.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Fixedpoint.to_string(), and Fixedpoint.update_rule().
fixedpoint |
Definition at line 6325 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 6331 of file z3py.py.
Referenced by Fixedpoint.abstract(), and Fixedpoint.declare_var().