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 7006 of file z3py.py.
◆ __init__()
def __init__ |
( |
|
self, |
|
|
|
fixedpoint = None , |
|
|
|
ctx = None |
|
) |
| |
Definition at line 7009 of file z3py.py.
7009 def __init__(self, fixedpoint=None, ctx=None):
7010 assert fixedpoint
is None or ctx
is not None
7011 self.ctx = _get_ctx(ctx)
7012 self.fixedpoint =
None
7013 if fixedpoint
is None:
7016 self.fixedpoint = fixedpoint
◆ __del__()
Definition at line 7023 of file z3py.py.
7024 if self.fixedpoint
is not None and self.ctx.ref()
is not None:
◆ __deepcopy__()
def __deepcopy__ |
( |
|
self, |
|
|
|
memo = {} |
|
) |
| |
Definition at line 7020 of file z3py.py.
7020 def __deepcopy__(self, memo={}):
7021 return FixedPoint(self.fixedpoint, self.ctx)
◆ __iadd__()
def __iadd__ |
( |
|
self, |
|
|
|
fml |
|
) |
| |
Definition at line 7059 of file z3py.py.
7059 def __iadd__(self, fml):
◆ __repr__()
Return a formatted string with all added rules and constraints.
Definition at line 7216 of file z3py.py.
7217 """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 7055 of file z3py.py.
7055 def add(self, *args):
7056 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7057 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 7180 of file z3py.py.
7180 def add_cover(self, level, predicate, property):
7181 """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 7071 of file z3py.py.
7071 def add_rule(self, head, body = None, name = None):
7072 """Assert rules defining recursive predicates to the fixedpoint solver.
7075 >>> s = Fixedpoint()
7076 >>> s.register_relation(a.decl())
7077 >>> s.register_relation(b.decl())
7087 head = self.abstract(head)
7090 body = _get_args(body)
7091 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 7063 of file z3py.py.
7063 def append(self, *args):
7064 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7065 self.assert_exprs(*args)
◆ assert_exprs()
def assert_exprs |
( |
|
self, |
|
|
* |
args |
|
) |
| |
Assert constraints as background axioms for the fixedpoint solver.
Definition at line 7041 of file z3py.py.
7041 def assert_exprs(self, *args):
7042 """Assert constraints as background axioms for the fixedpoint solver."""
7043 args = _get_args(args)
7046 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
7048 f = self.abstract(f)
7052 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 7243 of file z3py.py.
7243 def declare_var(self, *vars):
7244 """Add variable or several variables.
7245 The added variable or variables will be bound in the rules
7248 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 7098 of file z3py.py.
7098 def fact(self, head, name = None):
7099 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7100 self.add_rule(head,
None, name)
◆ get_answer()
Retrieve answer from last query call.
Definition at line 7149 of file z3py.py.
7149 def get_answer(self):
7150 """Retrieve answer from last query call."""
7152 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 7212 of file z3py.py.
7212 def get_assertions(self):
7213 """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 7175 of file z3py.py.
7175 def get_cover_delta(self, level, predicate):
7176 """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
7178 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 7154 of file z3py.py.
7154 def get_ground_sat_answer(self):
7155 """Retrieve a ground cex from last query call."""
7156 r = Z3_fixedpoint_get_ground_sat_answer(self.ctx.ref(), self.fixedpoint)
7157 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 7171 of file z3py.py.
7171 def get_num_levels(self, predicate):
7172 """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 7163 of file z3py.py.
7163 def get_rule_names_along_trace(self):
7164 """retrieve rule names along the counterexample trace"""
7167 names = _symbol2py (self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))
7169 return names.split (
';')
◆ get_rules()
retrieve rules that have been added to fixedpoint context
Definition at line 7208 of file z3py.py.
7208 def get_rules(self):
7209 """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 7159 of file z3py.py.
7159 def get_rules_along_trace(self):
7160 """retrieve rules along the counterexample trace"""
7161 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 7033 of file z3py.py.
7034 """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 7067 of file z3py.py.
7067 def insert(self, *args):
7068 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7069 self.assert_exprs(*args)
◆ param_descrs()
Return the parameter description set.
Definition at line 7037 of file z3py.py.
7037 def param_descrs(self):
7038 """Return the parameter description set."""
◆ parse_file()
def parse_file |
( |
|
self, |
|
|
|
f |
|
) |
| |
Parse rules and queries from a file
Definition at line 7204 of file z3py.py.
7204 def parse_file(self, f):
7205 """Parse rules and queries from a file"""
◆ parse_string()
def parse_string |
( |
|
self, |
|
|
|
s |
|
) |
| |
Parse rules and queries from a string
Definition at line 7200 of file z3py.py.
7200 def parse_string(self, s):
7201 """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 7102 of file z3py.py.
7102 def query(self, *query):
7103 """Query the fixedpoint engine whether formula is derivable.
7104 You can also pass an tuple or list of recursive predicates.
7106 query = _get_args(query)
7108 if sz >= 1
and isinstance(query[0], FuncDeclRef):
7109 _decls = (FuncDecl * sz)()
7119 query =
And(query, self.ctx)
7120 query = self.abstract(query,
False)
7122 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 7124 of file z3py.py.
7124 def query_from_lvl (self, lvl, *query):
7125 """Query the fixedpoint engine whether formula is derivable starting at the given query level.
7127 query = _get_args(query)
7129 if sz >= 1
and isinstance(query[0], FuncDecl):
7130 _z3_assert (
False,
"unsupported")
7136 query = self.abstract(query,
False)
7137 r = Z3_fixedpoint_query_from_lvl (self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
7138 return CheckSatResult(r)
◆ reason_unknown()
def reason_unknown |
( |
|
self | ) |
|
Return a string describing why the last `query()` returned `unknown`.
Definition at line 7238 of file z3py.py.
7238 def reason_unknown(self):
7239 """Return a string describing why the last `query()` returned `unknown`.
◆ register_relation()
def register_relation |
( |
|
self, |
|
|
* |
relations |
|
) |
| |
Register relation as recursive
Definition at line 7184 of file z3py.py.
7184 def register_relation(self, *relations):
7185 """Register relation as recursive"""
7186 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 7094 of file z3py.py.
7094 def rule(self, head, body = None, name = None):
7095 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7096 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 7027 of file z3py.py.
7027 def set(self, *args, **keys):
7028 """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 7190 of file z3py.py.
7190 def set_predicate_representation(self, f, *representations):
7191 """Control how relation is represented"""
7192 representations = _get_args(representations)
7193 representations = [
to_symbol(s)
for s
in representations]
7194 sz = len(representations)
7195 args = (Symbol * sz)()
7197 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 7220 of file z3py.py.
7221 """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 7233 of file z3py.py.
7233 def statistics(self):
7234 """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 7225 of file z3py.py.
7225 def to_string(self, queries):
7226 """Return a formatted string (in Lisp-like format) with all added constraints.
7227 We say the string is in s-expression format.
7228 Include also queries.
7230 args, len = _to_ast_array(queries)
◆ update_rule()
def update_rule |
( |
|
self, |
|
|
|
head, |
|
|
|
body, |
|
|
|
name |
|
) |
| |
update rule
Definition at line 7140 of file z3py.py.
7140 def update_rule(self, head, body, name):
7145 body = _get_args(body)
7146 f = self.abstract(
Implies(
And(body, self.ctx),head))
◆ ctx
Definition at line 7011 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(), UserPropagateBase.conflict(), UserPropagateBase.ctx_ref(), 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 7012 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
def __init__(self, s, ctx=None)
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: