Fixedpoint.
More...
|
def | __init__ (self, fixedpoint=None, ctx=None) |
|
def | __deepcopy__ (self, memo={}) |
|
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 | 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 (self, fml, is_forall=True) |
|
def | use_pp (self) |
|
Fixedpoint.
Fixedpoint API provides methods for solving with recursive predicates
Definition at line 6972 of file z3py.py.
◆ __init__()
def __init__ |
( |
|
self, |
|
|
|
fixedpoint = None , |
|
|
|
ctx = None |
|
) |
| |
Definition at line 6975 of file z3py.py.
6975 def __init__(self, fixedpoint=None, ctx=None):
6976 assert fixedpoint
is None or ctx
is not None
6977 self.ctx = _get_ctx(ctx)
6978 self.fixedpoint =
None
6979 if fixedpoint
is None:
6982 self.fixedpoint = fixedpoint
◆ __del__()
Definition at line 6989 of file z3py.py.
6990 if self.fixedpoint
is not None and self.ctx.ref()
is not None:
◆ __deepcopy__()
def __deepcopy__ |
( |
|
self, |
|
|
|
memo = {} |
|
) |
| |
Definition at line 6986 of file z3py.py.
6986 def __deepcopy__(self, memo={}):
6987 return FixedPoint(self.fixedpoint, self.ctx)
◆ __iadd__()
def __iadd__ |
( |
|
self, |
|
|
|
fml |
|
) |
| |
Definition at line 7025 of file z3py.py.
7025 def __iadd__(self, fml):
◆ __repr__()
Return a formatted string with all added rules and constraints.
Definition at line 7182 of file z3py.py.
7183 """Return a formatted string with all added rules and constraints."""
◆ abstract()
def abstract |
( |
|
self, |
|
|
|
fml, |
|
|
|
is_forall = True |
|
) |
| |
◆ add()
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
Definition at line 7021 of file z3py.py.
7021 def add(self, *args):
7022 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7023 self.assert_exprs(*args)
Referenced by Fixedpoint.__iadd__(), and Optimize.__iadd__().
◆ add_cover()
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 7146 of file z3py.py.
7146 def add_cover(self, level, predicate, property):
7147 """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
◆ add_rule()
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 7037 of file z3py.py.
7037 def add_rule(self, head, body = None, name = None):
7038 """Assert rules defining recursive predicates to the fixedpoint solver.
7041 >>> s = Fixedpoint()
7042 >>> s.register_relation(a.decl())
7043 >>> s.register_relation(b.decl())
7053 head = self.abstract(head)
7056 body = _get_args(body)
7057 f = self.abstract(
Implies(
And(body, self.ctx),head))
Referenced by Fixedpoint.fact(), and Fixedpoint.rule().
◆ append()
def append |
( |
|
self, |
|
|
* |
args |
|
) |
| |
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
Definition at line 7029 of file z3py.py.
7029 def append(self, *args):
7030 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7031 self.assert_exprs(*args)
◆ assert_exprs()
def assert_exprs |
( |
|
self, |
|
|
* |
args |
|
) |
| |
Assert constraints as background axioms for the fixedpoint solver.
Definition at line 7007 of file z3py.py.
7007 def assert_exprs(self, *args):
7008 """Assert constraints as background axioms for the fixedpoint solver."""
7009 args = _get_args(args)
7012 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
7014 f = self.abstract(f)
7018 arg = self.abstract(arg)
Referenced by Fixedpoint.add(), Optimize.add(), Fixedpoint.append(), and Fixedpoint.insert().
◆ declare_var()
def 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 7209 of file z3py.py.
7209 def declare_var(self, *vars):
7210 """Add variable or several variables.
7211 The added variable or variables will be bound in the rules
7214 vars = _get_args(vars)
◆ fact()
def fact |
( |
|
self, |
|
|
|
head, |
|
|
|
name = None |
|
) |
| |
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.
Definition at line 7064 of file z3py.py.
7064 def fact(self, head, name = None):
7065 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7066 self.add_rule(head,
None, name)
◆ get_answer()
Retrieve answer from last query call.
Definition at line 7115 of file z3py.py.
7115 def get_answer(self):
7116 """Retrieve answer from last query call."""
7118 return _to_expr_ref(r, self.ctx)
◆ get_assertions()
def get_assertions |
( |
|
self | ) |
|
retrieve assertions that have been added to fixedpoint context
Definition at line 7178 of file z3py.py.
7178 def get_assertions(self):
7179 """retrieve assertions that have been added to fixedpoint context"""
◆ get_cover_delta()
def 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 7141 of file z3py.py.
7141 def get_cover_delta(self, level, predicate):
7142 """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
7144 return _to_expr_ref(r, self.ctx)
◆ get_ground_sat_answer()
def get_ground_sat_answer |
( |
|
self | ) |
|
Retrieve a ground cex from last query call.
Definition at line 7120 of file z3py.py.
7120 def get_ground_sat_answer(self):
7121 """Retrieve a ground cex from last query call."""
7122 r = Z3_fixedpoint_get_ground_sat_answer(self.ctx.ref(), self.fixedpoint)
7123 return _to_expr_ref(r, self.ctx)
◆ get_num_levels()
def get_num_levels |
( |
|
self, |
|
|
|
predicate |
|
) |
| |
Retrieve number of levels used for predicate in PDR engine
Definition at line 7137 of file z3py.py.
7137 def get_num_levels(self, predicate):
7138 """Retrieve number of levels used for predicate in PDR engine"""
◆ get_rule_names_along_trace()
def get_rule_names_along_trace |
( |
|
self | ) |
|
retrieve rule names along the counterexample trace
Definition at line 7129 of file z3py.py.
7129 def get_rule_names_along_trace(self):
7130 """retrieve rule names along the counterexample trace"""
7133 names = _symbol2py (self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))
7135 return names.split (
';')
◆ get_rules()
retrieve rules that have been added to fixedpoint context
Definition at line 7174 of file z3py.py.
7174 def get_rules(self):
7175 """retrieve rules that have been added to fixedpoint context"""
◆ get_rules_along_trace()
def get_rules_along_trace |
( |
|
self | ) |
|
retrieve rules along the counterexample trace
Definition at line 7125 of file z3py.py.
7125 def get_rules_along_trace(self):
7126 """retrieve rules along the counterexample trace"""
7127 return AstVector(Z3_fixedpoint_get_rules_along_trace(self.ctx.ref(), self.fixedpoint), self.ctx)
◆ help()
Display a string describing all available options.
Definition at line 6999 of file z3py.py.
7000 """Display a string describing all available options."""
◆ insert()
def insert |
( |
|
self, |
|
|
* |
args |
|
) |
| |
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
Definition at line 7033 of file z3py.py.
7033 def insert(self, *args):
7034 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7035 self.assert_exprs(*args)
◆ param_descrs()
Return the parameter description set.
Definition at line 7003 of file z3py.py.
7003 def param_descrs(self):
7004 """Return the parameter description set."""
◆ parse_file()
def parse_file |
( |
|
self, |
|
|
|
f |
|
) |
| |
Parse rules and queries from a file
Definition at line 7170 of file z3py.py.
7170 def parse_file(self, f):
7171 """Parse rules and queries from a file"""
◆ parse_string()
def parse_string |
( |
|
self, |
|
|
|
s |
|
) |
| |
Parse rules and queries from a string
Definition at line 7166 of file z3py.py.
7166 def parse_string(self, s):
7167 """Parse rules and queries from a string"""
◆ query()
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 7068 of file z3py.py.
7068 def query(self, *query):
7069 """Query the fixedpoint engine whether formula is derivable.
7070 You can also pass an tuple or list of recursive predicates.
7072 query = _get_args(query)
7074 if sz >= 1
and isinstance(query[0], FuncDeclRef):
7075 _decls = (FuncDecl * sz)()
7085 query =
And(query, self.ctx)
7086 query = self.abstract(query,
False)
7088 return CheckSatResult(r)
◆ query_from_lvl()
def query_from_lvl |
( |
|
self, |
|
|
|
lvl, |
|
|
* |
query |
|
) |
| |
Query the fixedpoint engine whether formula is derivable starting at the given query level.
Definition at line 7090 of file z3py.py.
7090 def query_from_lvl (self, lvl, *query):
7091 """Query the fixedpoint engine whether formula is derivable starting at the given query level.
7093 query = _get_args(query)
7095 if sz >= 1
and isinstance(query[0], FuncDecl):
7096 _z3_assert (
False,
"unsupported")
7102 query = self.abstract(query,
False)
7103 r = Z3_fixedpoint_query_from_lvl (self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
7104 return CheckSatResult(r)
◆ reason_unknown()
def reason_unknown |
( |
|
self | ) |
|
Return a string describing why the last `query()` returned `unknown`.
Definition at line 7204 of file z3py.py.
7204 def reason_unknown(self):
7205 """Return a string describing why the last `query()` returned `unknown`.
◆ register_relation()
def register_relation |
( |
|
self, |
|
|
* |
relations |
|
) |
| |
Register relation as recursive
Definition at line 7150 of file z3py.py.
7150 def register_relation(self, *relations):
7151 """Register relation as recursive"""
7152 relations = _get_args(relations)
◆ rule()
def rule |
( |
|
self, |
|
|
|
head, |
|
|
|
body = None , |
|
|
|
name = None |
|
) |
| |
Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.
Definition at line 7060 of file z3py.py.
7060 def rule(self, head, body = None, name = None):
7061 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7062 self.add_rule(head, body, name)
◆ set()
def set |
( |
|
self, |
|
|
* |
args, |
|
|
** |
keys |
|
) |
| |
Set a configuration option. The method `help()` return a string containing all available options.
Definition at line 6993 of file z3py.py.
6993 def set(self, *args, **keys):
6994 """Set a configuration option. The method `help()` return a string containing all available options.
◆ set_predicate_representation()
def set_predicate_representation |
( |
|
self, |
|
|
|
f, |
|
|
* |
representations |
|
) |
| |
Control how relation is represented
Definition at line 7156 of file z3py.py.
7156 def set_predicate_representation(self, f, *representations):
7157 """Control how relation is represented"""
7158 representations = _get_args(representations)
7159 representations = [
to_symbol(s)
for s
in representations]
7160 sz = len(representations)
7161 args = (Symbol * sz)()
7163 args[i] = representations[i]
◆ sexpr()
Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
Definition at line 7186 of file z3py.py.
7187 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
◆ statistics()
Return statistics for the last `query()`.
Definition at line 7199 of file z3py.py.
7199 def statistics(self):
7200 """Return statistics for the last `query()`.
◆ to_string()
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 7191 of file z3py.py.
7191 def to_string(self, queries):
7192 """Return a formatted string (in Lisp-like format) with all added constraints.
7193 We say the string is in s-expression format.
7194 Include also queries.
7196 args, len = _to_ast_array(queries)
◆ update_rule()
def update_rule |
( |
|
self, |
|
|
|
head, |
|
|
|
body, |
|
|
|
name |
|
) |
| |
update rule
Definition at line 7106 of file z3py.py.
7106 def update_rule(self, head, body, name):
7111 body = _get_args(body)
7112 f = self.abstract(
Implies(
And(body, self.ctx),head))
◆ ctx
Definition at line 6977 of file z3py.py.
Referenced by Probe.__call__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), 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(), Optimize.assert_and_track(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), Optimize.from_file(), Optimize.from_string(), 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(), 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(), Optimize.pop(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), 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(), Optimize.unsat_core(), and Fixedpoint.update_rule().
◆ fixedpoint
Definition at line 6978 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
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
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.
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....
expr range(expr const &lo, expr const &hi)
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
def to_symbol(s, ctx=None)
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.
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....
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
def Implies(a, b, ctx=None)
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.
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...
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom)
Assert a constraint to the fixedpoint context.
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.
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
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.
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.
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.
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.
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...
def args2params(arguments, keywords, ctx=None)
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
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: