From 86db446afa1514ed63682cf9b5dcfe7222a4cb4d Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 31 Jul 2017 15:52:31 -0400
Subject: [PATCH] python spacer-specific API

---
 src/api/python/z3/z3.py | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index a16c1b92b..1452a037e 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6536,6 +6536,22 @@ class Fixedpoint(Z3PPObject):
             r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
         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):
         """create a backtracking point for added rules, facts and assertions"""
         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)
         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):
         """Retrieve number of levels used for predicate in PDR engine"""
         return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)