expose assertions that are pushed to the context

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_datalog.cpp

@@ -450,6 +450,23 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(
+        Z3_context c,
+        Z3_fixedpoint d)
+    {
+        Z3_TRY;
+        LOG_Z3_fixedpoint_get_assertions(c, d);
+        ast_manager& m = mk_c(c)->m();
+        Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
+        mk_c(c)->save_object(v);
+        unsigned num_asserts = to_fixedpoint_ref(d)->ctx().get_num_assertions();
+        for (unsigned i = 0; i < num_asserts; ++i) {
+            v->m_ast_vector.push_back(to_fixedpoint_ref(d)->ctx().get_assertion(i));
+        }
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(0);
+    }
+    
     void Z3_API Z3_fixedpoint_set_reduce_assign_callback(
         Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr f) {
         Z3_TRY;

src/api/dotnet/Fixedpoint.cs

@@ -278,6 +278,23 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Retrieve set of assertions added to fixedpoint context.
+        /// </summary>                
+        public BoolExpr[] Assertions {
+            get
+            {
+                Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
+
+                ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
+                uint n = v.Size;
+                BoolExpr[] res = new BoolExpr[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = new BoolExpr(Context, v[i].NativeObject);
+                return res;
+            }
+        }
+
 
         #region Internal
         internal Fixedpoint(Context ctx, IntPtr obj)

src/api/python/z3.py

@@ -6146,6 +6146,10 @@ class Fixedpoint(Z3PPObject):
 	"""retrieve rules that have been added to fixedpoint context"""
 	return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
 
+    def get_assertions(self):
+	"""retrieve assertions that have been added to fixedpoint context"""
+	return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
+
     def __repr__(self):
         """Return a formatted string with all added rules and constraints."""
 	return self.sexpr()

src/api/z3_api.h

@@ -5696,6 +5696,15 @@ END_MLAPI_EXCLUDE
         __in Z3_context c,
         __in Z3_fixedpoint f);
 
+    /**
+       \brief Retrieve set of background assertions from fixedpoint context.
+
+       def_API('Z3_fixedpoint_get_assertions', AST_VECTOR, (_in(CONTEXT),_in(FIXEDPOINT)))
+     */
+    Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(
+        __in Z3_context c,
+        __in Z3_fixedpoint f);
+
     /**
        \brief Set parameters on fixedpoint context.       
 

src/muz_qe/dl_context.h

@@ -261,6 +261,8 @@ namespace datalog {
         
         void assert_expr(expr* e);
         expr_ref get_background_assertion();
+        unsigned get_num_assertions() { return m_background.size(); }
+        expr*    get_assertion(unsigned i) const { return m_background[i]; }
 
         /**
            Method exposed from API for adding rules.