Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/api/api_datalog.cpp

@@ -449,6 +449,23 @@ extern "C" {
         RETURN_Z3(of_ast_vector(v));
         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) {

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

@@ -6145,7 +6145,11 @@ class Fixedpoint(Z3PPObject):
     def get_rules(self):
 	"""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_cmds.cpp

@@ -315,7 +315,7 @@ private:
         if (m_params.get_bool(":print-certificate", false)) {
             datalog::context& dlctx = m_dl_ctx->dlctx();
             if (!dlctx.display_certificate(ctx.regular_stream())) {
-                throw cmd_exception("certificates are not supported for selected DL_ENGINE");
+                throw cmd_exception("certificates are not supported for the selected engine");
             }
             ctx.regular_stream() << "\n";
         }

src/muz_qe/dl_context.cpp

@@ -238,6 +238,7 @@ namespace datalog {
         m_pinned(m),
         m_vars(m),
         m_rule_set(*this),
+        m_rule_fmls(m),
         m_background(m),
         m_closed(false),
         m_saturation_was_run(false),
@@ -521,10 +522,19 @@ namespace datalog {
     }
 
     void context::add_rule(expr* rl, symbol const& name) {
+        m_rule_fmls.push_back(rl);
+        m_rule_names.push_back(name);
+    }
+
+    void context::flush_add_rules() {
         datalog::rule_manager& rm = get_rule_manager();
         datalog::rule_ref_vector rules(rm);
-        rm.mk_rule(rl, rules, name);
+        for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
+            rm.mk_rule(m_rule_fmls[i].get(), rules, m_rule_names[i]);
+        }
         add_rules(rules);
+        m_rule_fmls.reset();
+        m_rule_names.reset();
     }
 
     //
@@ -1223,6 +1233,7 @@ namespace datalog {
     }
 
     void context::new_query() {
+        flush_add_rules();
         if (m_last_result_relation) {
             m_last_result_relation->deallocate();
             m_last_result_relation = 0;
@@ -1512,7 +1523,7 @@ namespace datalog {
         switch(get_engine()) {
         case DATALOG_ENGINE:            
             return false;
-        case PDR_ENGINE: 
+        case QPDR_ENGINE: 
             ensure_pdr();
             m_pdr->display_certificate(out);
             return true;
@@ -1618,6 +1629,10 @@ namespace datalog {
                 names.push_back((*it)->name());
             }
         }
+        for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
+            rules.push_back(m_rule_fmls[i].get());
+            names.push_back(m_rule_names[i]);
+        }
 
         smt2_pp_environment_dbg env(m);
         pp_params params;
@@ -1674,8 +1689,11 @@ namespace datalog {
             declare_vars(rules, fresh_names, out);
         }
 
+        if (num_axioms > 0 && !use_fixedpoint_extensions) {
+            throw default_exception("Background axioms cannot be used with SMT-LIB2 HORN format");
+        }
+
         for (unsigned i = 0; i < num_axioms; ++i) {
-            SASSERT(use_fixedpoint_extensions);
             out << "(assert ";
             ast_smt2_pp(out, axioms[i], env, params);
             out << ")\n";

src/muz_qe/dl_context.h

@@ -96,6 +96,8 @@ namespace datalog {
         pred2syms          m_argument_var_names;
         decl_set           m_output_preds;
         rule_set           m_rule_set;
+        expr_ref_vector    m_rule_fmls;
+        svector<symbol>    m_rule_names;
         expr_ref_vector    m_background;
 
         scoped_ptr<pdr::dl_interface>   m_pdr;
@@ -259,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.
@@ -454,6 +458,8 @@ namespace datalog {
 
     private:
 
+        void flush_add_rules();
+
         void ensure_pdr();
 
         void ensure_bmc();

src/muz_qe/dl_mk_rule_inliner.cpp

@@ -194,6 +194,7 @@ namespace datalog {
         }
     }
 
+    // TBD: replace by r.has_quantifiers() and test
     bool mk_rule_inliner::has_quantifier(rule const& r) const {
         unsigned utsz = r.get_uninterpreted_tail_size();
         for (unsigned i = utsz; i < r.get_tail_size(); ++i) {

src/muz_qe/dl_mk_slice.cpp

@@ -818,6 +818,11 @@ namespace datalog {
     }
 
     rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc, proof_converter_ref& pc) {        
+        for (unsigned i = 0; i < src.get_num_rules(); ++i) {
+            if (src.get_rule(i)->has_quantifiers()) {
+                return 0;
+            }
+        }
         ref<slice_proof_converter> spc;
         ref<slice_model_converter> smc;
         if (pc) {