postpone rule flushing dependent on engine

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

src/api/python/z3.py

@@ -585,6 +585,9 @@ class FuncDeclRef(AstRef):
     def as_ast(self):
         return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
 
+    def as_func_decl(self):
+	return self.ast
+
     def name(self):
         """Return the name of the function declaration `self`.
         

src/muz_qe/dl_context.cpp

@@ -234,6 +234,7 @@ namespace datalog {
         m_vars(m),
         m_rule_set(*this),
         m_transformed_rule_set(*this),
+        m_rule_fmls_head(0),
         m_rule_fmls(m),
         m_background(m),
         m_mc(0),
@@ -243,8 +244,6 @@ namespace datalog {
         m_last_answer(m),
         m_engine(LAST_ENGINE),
         m_cancel(false) {
-        
-        //register plugins for builtin tables
     }
 
     context::~context() {
@@ -254,6 +253,9 @@ namespace datalog {
     void context::reset() {
         m_trail.reset();
         m_rule_set.reset();
+        m_rule_fmls_head = 0;
+        m_rule_fmls.reset();
+        m_rule_names.reset();
         m_argument_var_names.reset();
         m_preds.reset();
         m_preds_by_name.reset();
@@ -457,13 +459,18 @@ namespace datalog {
     void context::flush_add_rules() {
         datalog::rule_manager& rm = get_rule_manager();
         scoped_proof_mode _scp(m, generate_proof_trace()?PGM_FINE:PGM_DISABLED);
-        for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
+        while (m_rule_fmls_head < m_rule_fmls.size()) {
-            expr* fml = m_rule_fmls[i].get();
+            expr* fml = m_rule_fmls[m_rule_fmls_head].get();
             proof* p = generate_proof_trace()?m.mk_asserted(fml):0;
-            rm.mk_rule(fml, p, m_rule_set, m_rule_names[i]);
+            rm.mk_rule(fml, p, m_rule_set, m_rule_names[m_rule_fmls_head]);
+            ++m_rule_fmls_head;
+        }
+        rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
+        rule_ref r(m_rule_manager);
+        for (; it != end; ++it) {
+            r = *it;
+            check_rule(r);
         }
-        m_rule_fmls.reset();
-        m_rule_names.reset();
     }
 
     //
@@ -958,18 +965,21 @@ namespace datalog {
         engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine(DATALOG_ENGINE) {}
 
         DL_ENGINE get_engine() const { return m_engine; }
+
         void operator()(expr* e) {
             if (is_quantifier(e)) {
                 m_engine = QPDR_ENGINE;
             }
-            else if (a.is_int_real(e) && m_engine != QPDR_ENGINE) {
+            else if (m_engine != QPDR_ENGINE) {
-                m_engine = PDR_ENGINE;
+                if (a.is_int_real(e)) {
-            }
+                    m_engine = PDR_ENGINE;
-            else if (is_var(e) && m.is_bool(e)) {
+                }
-                m_engine = PDR_ENGINE;
+                else if (is_var(e) && m.is_bool(e)) {
-            }
+                    m_engine = PDR_ENGINE;
-            else if (dt.is_datatype(m.get_sort(e))) {
+                }
-                m_engine = PDR_ENGINE;
+                else if (dt.is_datatype(m.get_sort(e))) {
+                    m_engine = PDR_ENGINE;
+                }
             }
         }
     };
@@ -1002,7 +1012,7 @@ namespace datalog {
         if (m_engine == LAST_ENGINE) {
             expr_fast_mark1 mark;
             engine_type_proc proc(m);
-            m_engine = DATALOG_ENGINE;
+            m_engine = DATALOG_ENGINE;            
             for (unsigned i = 0; m_engine == DATALOG_ENGINE && i < m_rule_set.get_num_rules(); ++i) {
                 rule * r = m_rule_set.get_rule(i);
                 quick_for_each_expr(proc, mark, r->get_head());
@@ -1011,29 +1021,38 @@ namespace datalog {
                 }
                 m_engine = proc.get_engine();
             }
+            for (unsigned i = m_rule_fmls_head; m_engine == DATALOG_ENGINE && i < m_rule_fmls.size(); ++i) {
+                expr* fml = m_rule_fmls[i].get();
+                while (is_quantifier(fml)) {
+                    fml = to_quantifier(fml)->get_expr();
+                }
+                quick_for_each_expr(proc, mark, fml);
+                m_engine = proc.get_engine();
+            }
         }
     }
 
     lbool context::query(expr* query) {
-        new_query();
+        m_mc = mk_skip_model_converter();
-        rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
+        m_last_status = OK;
-        rule_ref r(m_rule_manager);
+        m_last_answer = 0;
-        for (; it != end; ++it) {
+        switch (get_engine()) {
-            r = *it;
-            check_rule(r);
-        }        
-        switch(get_engine()) {
         case DATALOG_ENGINE:
+            flush_add_rules();
             return rel_query(query);
         case PDR_ENGINE:
         case QPDR_ENGINE:
+            flush_add_rules();
             return pdr_query(query);
         case BMC_ENGINE:
         case QBMC_ENGINE:
+            flush_add_rules();
             return bmc_query(query);
         case TAB_ENGINE:
+            flush_add_rules();
             return tab_query(query);
         case CLP_ENGINE:
+            flush_add_rules();
             return clp_query(query);
         default:
             UNREACHABLE();
@@ -1041,14 +1060,6 @@ namespace datalog {
         }
     }
 
-    void context::new_query() {
-        m_mc = mk_skip_model_converter();
-
-        flush_add_rules();
-        m_last_status = OK;
-        m_last_answer = 0;
-    }
-
     model_ref context::get_model() {
         switch(get_engine()) {
         case PDR_ENGINE:
@@ -1277,7 +1288,7 @@ namespace datalog {
         datalog::rule_manager& rm = get_rule_manager();
         
         // ensure that rules are all using bound variables.
-        for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
+        for (unsigned i = m_rule_fmls_head; i < m_rule_fmls.size(); ++i) {
             ptr_vector<sort> sorts;
             get_free_vars(m_rule_fmls[i].get(), sorts);
             if (!sorts.empty()) {
@@ -1295,7 +1306,7 @@ namespace datalog {
             rules.push_back(fml);
             names.push_back((*it)->name());
         }
-        for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
+        for (unsigned i = m_rule_fmls_head; i < m_rule_fmls.size(); ++i) {
             rules.push_back(m_rule_fmls[i].get());
             names.push_back(m_rule_names[i]);            
         }

src/muz_qe/dl_context.h

@@ -114,6 +114,7 @@ namespace datalog {
         pred2syms          m_argument_var_names;
         rule_set           m_rule_set;
         rule_set           m_transformed_rule_set;
+        unsigned           m_rule_fmls_head;
         expr_ref_vector    m_rule_fmls;
         svector<symbol>    m_rule_names;
         expr_ref_vector    m_background;
@@ -482,8 +483,6 @@ namespace datalog {
 
         void ensure_rel();
 
-        void new_query();
-
         lbool rel_query(expr* query);
 
         lbool pdr_query(expr* query);

src/muz_qe/dl_mk_slice.cpp

@@ -120,12 +120,11 @@ namespace datalog {
             obj_map<rule, rule*>::iterator end = m_rule2slice.end();
             expr_ref fml(m);
             for (; it != end; ++it) {
-                TRACE("dl", 
-                      it->m_key->display(m_ctx, tout << "orig:\n");
-                      it->m_value->display(m_ctx, tout << "new:\n"););
-                
                 it->m_value->to_formula(fml);
                 m_pinned_exprs.push_back(fml);
+                TRACE("dl", 
+                      tout << "orig: " << mk_pp(fml, m) << "\n";
+                      it->m_value->display(m_ctx, tout << "new:\n"););                
                 m_sliceform2rule.insert(fml, it->m_key);                
             }
         }
@@ -202,9 +201,10 @@ namespace datalog {
             proof* p0_new = m_new_proof.find(p0);            
             expr* fact0   = m.get_fact(p0);
             TRACE("dl", tout << "fact0: " << mk_pp(fact0, m) << "\n";);
-            rule* orig0    = m_sliceform2rule.find(fact0);
+            rule* orig0;
-            /* rule* slice0   = */ m_rule2slice.find(orig0);
+            if (!m_sliceform2rule.find(fact0, orig0)) {
-            /* unsigned_vector const& renaming0 = m_renaming.find(orig0); */
+                return false;
+            }
             premises.push_back(p0_new);
             rule_ref r1(rm), r2(rm), r3(rm);
             r1 = orig0;
@@ -214,9 +214,10 @@ namespace datalog {
                 proof* p1_new = m_new_proof.find(p1);
                 expr* fact1   = m.get_fact(p1);
                 TRACE("dl", tout << "fact1: " << mk_pp(fact1, m) << "\n";);
-                rule* orig1     = m_sliceform2rule.find(fact1);
+                rule* orig1 = 0;
-                /* rule* slice1    = */ m_rule2slice.find(orig1);
+                if (!m_sliceform2rule.find(fact1, orig1)) {
-                /* unsigned_vector const& renaming1 =  m_renaming.find(orig1); TBD */
+                    return false;
+                }
                 premises.push_back(p1_new);
 
                 // TODO: work with substitutions.
@@ -241,6 +242,9 @@ namespace datalog {
             proof* new_p = m.mk_hyper_resolve(premises.size(), premises.c_ptr(), concl, positions, substs);
             m_pinned_exprs.push_back(new_p);
             m_pinned_rules.push_back(r1.get());
+            TRACE("dl", 
+                  tout << "orig: " << mk_pp(slice_concl, m) << "\n";
+                  r1->display(m_ctx, tout << "new:"););
             m_sliceform2rule.insert(slice_concl, r1.get());
             m_rule2slice.insert(r1.get(), 0);
             m_renaming.insert(r1.get(), unsigned_vector());

src/muz_qe/pdr_dl_interface.cpp

@@ -32,6 +32,7 @@ Revision History:
 #include "dl_mk_slice.h"
 #include "dl_mk_unfold.h"
 #include "dl_mk_coalesce.h"
+#include "model_smt2_pp.h"
 
 using namespace pdr;
 
@@ -134,10 +135,10 @@ lbool dl_interface::query(expr * query) {
     }
     query_pred = m_ctx.get_rules().get_output_predicate();
 
-
     IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););
     m_pdr_rules.replace_rules(m_ctx.get_rules());
     m_pdr_rules.close();
+    m_ctx.record_transformed_rules();
     m_ctx.reopen();
     m_ctx.replace_rules(old_rules);
     
@@ -151,6 +152,7 @@ lbool dl_interface::query(expr * query) {
     
     if (m_pdr_rules.get_rules().empty()) {
         m_context->set_unsat();
+        IF_VERBOSE(1, model_smt2_pp(verbose_stream(), m, *m_context->get_model(),0););
         return l_false;
     }