Public Member Functions | |
def | __init__ |
def | __deepcopy__ |
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 |
def | rule |
def | fact |
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 |
![]() | |
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 | ) |
Definition at line 7515 of file z3py.py.
def __repr__ | ( | self | ) |
def abstract | ( | self, | |
fml, | |||
is_forall = True |
|||
) |
Definition at line 7749 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), and Fixedpoint.update_rule().
def add | ( | self, | |
args | |||
) |
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
Definition at line 7547 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)
Definition at line 7674 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 7563 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 7533 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 7708 of file z3py.py.
def get_cover_delta | ( | self, | |
level, | |||
predicate | |||
) |
def get_ground_sat_answer | ( | self | ) |
def get_num_levels | ( | self, | |
predicate | |||
) |
def get_rule_names_along_trace | ( | self | ) |
retrieve rule names along the counterexample trace
Definition at line 7655 of file z3py.py.
def get_rules | ( | self | ) |
retrieve rules that have been added to fixedpoint context
Definition at line 7704 of file z3py.py.
def get_rules_along_trace | ( | self | ) |
retrieve rules along the counterexample trace
Definition at line 7651 of file z3py.py.
def help | ( | self | ) |
def insert | ( | self, | |
args | |||
) |
def param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 7529 of file z3py.py.
def parse_file | ( | self, | |
f | |||
) |
Parse rules and queries from a file
Definition at line 7700 of file z3py.py.
def parse_string | ( | self, | |
s | |||
) |
Parse rules and queries from a string
Definition at line 7696 of file z3py.py.
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 7594 of file z3py.py.
def query_from_lvl | ( | self, | |
lvl, | |||
query | |||
) |
Query the fixedpoint engine whether formula is derivable starting at the given query level.
Definition at line 7616 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 7686 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 7716 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 7722 of file z3py.py.
def update_rule | ( | self, | |
head, | |||
body, | |||
name | |||
) |
ctx |
Definition at line 7503 of file z3py.py.
Referenced by Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Simplifier.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Simplifier.add(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Optimize.assert_and_track(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), ParserContext.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Simplifier.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Optimize.set_on_model(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Optimize.unsat_core(), Fixedpoint.update_rule(), and Simplifier.using_params().
fixedpoint |
Definition at line 7504 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 |
Definition at line 7510 of file z3py.py.
Referenced by Fixedpoint.abstract(), and Fixedpoint.declare_var().