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 6991 of file z3py.py.
◆ __init__()
def __init__ |
( |
|
self, |
|
|
|
fixedpoint = None , |
|
|
|
ctx = None |
|
) |
| |
Definition at line 6994 of file z3py.py.
6994 def __init__(self, fixedpoint=None, ctx=None):
6995 assert fixedpoint
is None or ctx
is not None
6996 self.ctx = _get_ctx(ctx)
6997 self.fixedpoint =
None
6998 if fixedpoint
is None:
7001 self.fixedpoint = fixedpoint
◆ __del__()
Definition at line 7008 of file z3py.py.
7009 if self.fixedpoint
is not None and self.ctx.ref()
is not None:
◆ __deepcopy__()
def __deepcopy__ |
( |
|
self, |
|
|
|
memo = {} |
|
) |
| |
Definition at line 7005 of file z3py.py.
7005 def __deepcopy__(self, memo={}):
7006 return FixedPoint(self.fixedpoint, self.ctx)
◆ __iadd__()
def __iadd__ |
( |
|
self, |
|
|
|
fml |
|
) |
| |
Definition at line 7044 of file z3py.py.
7044 def __iadd__(self, fml):
◆ __repr__()
Return a formatted string with all added rules and constraints.
Definition at line 7201 of file z3py.py.
7202 """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 7040 of file z3py.py.
7040 def add(self, *args):
7041 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7042 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 7165 of file z3py.py.
7165 def add_cover(self, level, predicate, property):
7166 """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 7056 of file z3py.py.
7056 def add_rule(self, head, body = None, name = None):
7057 """Assert rules defining recursive predicates to the fixedpoint solver.
7060 >>> s = Fixedpoint()
7061 >>> s.register_relation(a.decl())
7062 >>> s.register_relation(b.decl())
7072 head = self.abstract(head)
7075 body = _get_args(body)
7076 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 7048 of file z3py.py.
7048 def append(self, *args):
7049 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7050 self.assert_exprs(*args)
◆ assert_exprs()
def assert_exprs |
( |
|
self, |
|
|
* |
args |
|
) |
| |
Assert constraints as background axioms for the fixedpoint solver.
Definition at line 7026 of file z3py.py.
7026 def assert_exprs(self, *args):
7027 """Assert constraints as background axioms for the fixedpoint solver."""
7028 args = _get_args(args)
7031 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
7033 f = self.abstract(f)
7037 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 7228 of file z3py.py.
7228 def declare_var(self, *vars):
7229 """Add variable or several variables.
7230 The added variable or variables will be bound in the rules
7233 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 7083 of file z3py.py.
7083 def fact(self, head, name = None):
7084 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7085 self.add_rule(head,
None, name)
◆ get_answer()
Retrieve answer from last query call.
Definition at line 7134 of file z3py.py.
7134 def get_answer(self):
7135 """Retrieve answer from last query call."""
7137 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 7197 of file z3py.py.
7197 def get_assertions(self):
7198 """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 7160 of file z3py.py.
7160 def get_cover_delta(self, level, predicate):
7161 """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
7163 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 7139 of file z3py.py.
7139 def get_ground_sat_answer(self):
7140 """Retrieve a ground cex from last query call."""
7141 r = Z3_fixedpoint_get_ground_sat_answer(self.ctx.ref(), self.fixedpoint)
7142 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 7156 of file z3py.py.
7156 def get_num_levels(self, predicate):
7157 """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 7148 of file z3py.py.
7148 def get_rule_names_along_trace(self):
7149 """retrieve rule names along the counterexample trace"""
7152 names = _symbol2py (self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))
7154 return names.split (
';')
◆ get_rules()
retrieve rules that have been added to fixedpoint context
Definition at line 7193 of file z3py.py.
7193 def get_rules(self):
7194 """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 7144 of file z3py.py.
7144 def get_rules_along_trace(self):
7145 """retrieve rules along the counterexample trace"""
7146 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 7018 of file z3py.py.
7019 """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 7052 of file z3py.py.
7052 def insert(self, *args):
7053 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7054 self.assert_exprs(*args)
◆ param_descrs()
Return the parameter description set.
Definition at line 7022 of file z3py.py.
7022 def param_descrs(self):
7023 """Return the parameter description set."""
◆ parse_file()
def parse_file |
( |
|
self, |
|
|
|
f |
|
) |
| |
Parse rules and queries from a file
Definition at line 7189 of file z3py.py.
7189 def parse_file(self, f):
7190 """Parse rules and queries from a file"""
◆ parse_string()
def parse_string |
( |
|
self, |
|
|
|
s |
|
) |
| |
Parse rules and queries from a string
Definition at line 7185 of file z3py.py.
7185 def parse_string(self, s):
7186 """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 7087 of file z3py.py.
7087 def query(self, *query):
7088 """Query the fixedpoint engine whether formula is derivable.
7089 You can also pass an tuple or list of recursive predicates.
7091 query = _get_args(query)
7093 if sz >= 1
and isinstance(query[0], FuncDeclRef):
7094 _decls = (FuncDecl * sz)()
7104 query =
And(query, self.ctx)
7105 query = self.abstract(query,
False)
7107 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 7109 of file z3py.py.
7109 def query_from_lvl (self, lvl, *query):
7110 """Query the fixedpoint engine whether formula is derivable starting at the given query level.
7112 query = _get_args(query)
7114 if sz >= 1
and isinstance(query[0], FuncDecl):
7115 _z3_assert (
False,
"unsupported")
7121 query = self.abstract(query,
False)
7122 r = Z3_fixedpoint_query_from_lvl (self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
7123 return CheckSatResult(r)
◆ reason_unknown()
def reason_unknown |
( |
|
self | ) |
|
Return a string describing why the last `query()` returned `unknown`.
Definition at line 7223 of file z3py.py.
7223 def reason_unknown(self):
7224 """Return a string describing why the last `query()` returned `unknown`.
◆ register_relation()
def register_relation |
( |
|
self, |
|
|
* |
relations |
|
) |
| |
Register relation as recursive
Definition at line 7169 of file z3py.py.
7169 def register_relation(self, *relations):
7170 """Register relation as recursive"""
7171 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 7079 of file z3py.py.
7079 def rule(self, head, body = None, name = None):
7080 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7081 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 7012 of file z3py.py.
7012 def set(self, *args, **keys):
7013 """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 7175 of file z3py.py.
7175 def set_predicate_representation(self, f, *representations):
7176 """Control how relation is represented"""
7177 representations = _get_args(representations)
7178 representations = [
to_symbol(s)
for s
in representations]
7179 sz = len(representations)
7180 args = (Symbol * sz)()
7182 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 7205 of file z3py.py.
7206 """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 7218 of file z3py.py.
7218 def statistics(self):
7219 """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 7210 of file z3py.py.
7210 def to_string(self, queries):
7211 """Return a formatted string (in Lisp-like format) with all added constraints.
7212 We say the string is in s-expression format.
7213 Include also queries.
7215 args, len = _to_ast_array(queries)
◆ update_rule()
def update_rule |
( |
|
self, |
|
|
|
head, |
|
|
|
body, |
|
|
|
name |
|
) |
| |
update rule
Definition at line 7125 of file z3py.py.
7125 def update_rule(self, head, body, name):
7130 body = _get_args(body)
7131 f = self.abstract(
Implies(
And(body, self.ctx),head))
◆ ctx
Definition at line 6996 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 6997 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: