mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

python spacer-specific API

Browse source
This commit is contained in:
Arie Gurfinkel 2017-07-31 15:52:31 -04:00
parent d080c146a2
commit 86db446afa
1 changed files with 33 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/api/python/z3/z3.py
View file

@ -6536,6 +6536,22 @@ class Fixedpoint(Z3PPObject):
r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast()) r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
return CheckSatResult(r) return CheckSatResult(r)
def query_from_lvl (self, lvl, *query):
"""Query the fixedpoint engine whether formula is derivable starting at the given query level.
"""
query = _get_args(query)
sz = len(query)
if sz >= 1 and isinstance(query[0], FuncDecl):
_z3_assert (False, "unsupported")
else:
if sz == 1:
query = query[0]
else:
query = And(query)
query = self.abstract(query, False)
r = Z3_fixedpoint_query_from_lvl (self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
return CheckSatResult(r)
def push(self): def push(self):
"""create a backtracking point for added rules, facts and assertions""" """create a backtracking point for added rules, facts and assertions"""
Z3_fixedpoint_push(self.ctx.ref(), self.fixedpoint) Z3_fixedpoint_push(self.ctx.ref(), self.fixedpoint)
@ -6558,6 +6574,23 @@ class Fixedpoint(Z3PPObject):
r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint) r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
return _to_expr_ref(r, self.ctx) return _to_expr_ref(r, self.ctx)
def get_ground_sat_answer(self):
"""Retrieve a ground cex from last query call."""
r = Z3_fixedpoint_get_ground_sat_answer(self.ctx.ref(), self.fixedpoint)
return _to_expr_ref(r, self.ctx)
def get_rules_along_trace(self):
"""retrieve rules along the counterexample trace"""
return AstVector(Z3_fixedpoint_get_rules_along_trace(self.ctx.ref(), self.fixedpoint), self.ctx)
def get_rule_names_along_trace(self):
"""retrieve rule names along the counterexample trace"""
# this is a hack as I don't know how to return a list of symbols from C++;
# obtain names as a single string separated by semicolons
names = _symbol2py (self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))
# split into individual names
return names.split (';')
def get_num_levels(self, predicate): def get_num_levels(self, predicate):
"""Retrieve number of levels used for predicate in PDR engine""" """Retrieve number of levels used for predicate in PDR engine"""
return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast) return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)