working on quantifiers

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

src/muz_qe/dl_mk_array_blast.cpp

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Remove array variables from rules.
+    Remove array stores from rules.
 
 Author:
 
@@ -53,6 +53,11 @@ namespace datalog {
         unsigned utsz = r.get_uninterpreted_tail_size();
         unsigned tsz = r.get_tail_size();
         expr_ref_vector conjs(m), new_conjs(m);
+        expr_ref tmp(m);
+        expr_substitution sub(m);
+        uint_set lhs_vars, rhs_vars;
+        bool change = false;
+
         for (unsigned i = 0; i < utsz; ++i) {
             new_conjs.push_back(r.get_tail(i));
         }
@@ -60,11 +65,10 @@ namespace datalog {
             conjs.push_back(r.get_tail(i));
         }
         flatten_and(conjs);
-        expr_substitution sub(m);
-        uint_set lhs_vars, rhs_vars;
         for (unsigned i = 0; i < conjs.size(); ++i) {
-            expr* x, *y;
+            expr* x, *y, *e = conjs[i].get();
-            if (is_store_def(conjs[i].get(), x, y)) {
+            
+            if (is_store_def(e, x, y)) {
                 // enforce topological order consistency:
                 uint_set lhs;
                 collect_vars(m, x, lhs_vars);
@@ -72,17 +76,20 @@ namespace datalog {
                 lhs = lhs_vars;
                 lhs &= rhs_vars;
                 if (!lhs.empty()) {
-                    new_conjs.push_back(conjs[i].get());
+                    TRACE("dl", tout << "unusable equality " << mk_pp(e, m) << "\n";);
+                    new_conjs.push_back(e);
                 }
                 else {
                     sub.insert(x, y);
                 }
             }
             else {
-                new_conjs.push_back(conjs[i].get());
+                m_rewriter(e, tmp);
+                change = change || (tmp != e);
+                new_conjs.push_back(tmp);
             }
         }
-        if (sub.empty()) {
+        if (sub.empty() && !change) {
             rules.add_rule(&r);
             return false;
         }
@@ -102,6 +109,8 @@ namespace datalog {
         rm.mk_rule(fml2, new_rules, r.name());
         SASSERT(new_rules.size() == 1);
 
+        TRACE("dl", tout << "new body " << mk_pp(fml2, m) << "\n";);
+        
         rules.add_rule(new_rules[0].get());
         if (m_pc) {
             new_rules[0]->to_formula(fml2);
@@ -131,7 +140,6 @@ namespace datalog {
             pc = concat(pc.get(), epc.get());
         }
         return rules;        
-
     }
 
 };

src/muz_qe/dl_mk_extract_quantifiers.cpp

@@ -121,10 +121,11 @@ namespace datalog {
         }
         else {
             rule_ref new_rule(rm);
-            std::cout << mk_pp(r.get_head(), m) << " :- \n";
+            TRACE("dl", 
-            for (unsigned i = 0; i < tail.size(); ++i) {
+                  tout << mk_pp(r.get_head(), m) << " :- \n";
-                std::cout << "  " << mk_pp(tail[i].get(), m) << "\n";
+                  for (unsigned i = 0; i < tail.size(); ++i) {
-            }
+                      tout << "  " << mk_pp(tail[i].get(), m) << "\n";
+                  });
             new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), 0, r.name(), false);
             quantifier_ref_vector* qs = alloc(quantifier_ref_vector, quantifiers);
             m_refs.push_back(qs);

src/muz_qe/dl_mk_extract_quantifiers.h

@@ -39,8 +39,6 @@ namespace datalog {
 
         app_ref ensure_app(expr* e);
 
-        void ensure_predicate(expr* e, unsigned& max_var, app_ref_vector& tail);
-
     public:
         /**
            \brief Create rule transformer that extracts universal quantifiers (over recursive predicates).
@@ -55,6 +53,8 @@ namespace datalog {
 
         bool has_quantifiers() const { return !m_quantifiers.empty(); }
 
+        void ensure_predicate(expr* e, unsigned& max_var, app_ref_vector& tail);
+
     };
 
 };

src/muz_qe/pdr_context.cpp

@@ -442,6 +442,7 @@ namespace pdr {
         tmp = pm.mk_and(conj);
         prop_solver::scoped_level _sl(m_solver, level);
         m_solver.set_core(core);
+        m_solver.set_model(0);
         lbool r = m_solver.check_conjunction_as_assumptions(tmp);
         if (r == l_false) {
             assumes_level = m_solver.assumes_level();
@@ -706,7 +707,6 @@ namespace pdr {
         SASSERT(m_head == other.m_head);
         obj_map<expr, unsigned>::iterator it  = other.m_prop2level.begin();
         obj_map<expr, unsigned>::iterator end = other.m_prop2level.end();        
-        
         for (; it != end; ++it) {
             add_property(it->m_key, it->m_value);
         }

src/muz_qe/pdr_prop_solver.h

@@ -94,7 +94,7 @@ namespace pdr {
             scoped_level(prop_solver& ps, unsigned lvl):m_lev(ps.m_in_level) { 
                 SASSERT(!m_lev); m_lev = true; ps.m_current_level = lvl; 
             }
-                ~scoped_level() { m_lev = false; }
+            ~scoped_level() { m_lev = false; }
         };
         
         void add_formula(expr * form);

src/muz_qe/pdr_quantifiers.cpp

@@ -26,6 +26,7 @@ Revision History:
 #include "model_smt2_pp.h"
 #include "ast_smt_pp.h"
 #include "expr_abstract.h"
+#include "dl_mk_extract_quantifiers.h"
 
 
 namespace pdr {
@@ -129,7 +130,10 @@ namespace pdr {
         inv_var_shifter invsh(m);
         vs(q->get_expr(), binding.size(), binding.c_ptr(), e);
         invsh(e, q->get_num_decls(), e);
-        expr_abstract(m, 0, var_inst.size(), (expr*const*)var_inst.c_ptr(), e, e);
+        expr_ref_vector inst(m);
+        inst.append(var_inst.size(), (expr*const*)var_inst.c_ptr());
+        inst.reverse();
+        expr_abstract(m, 0, inst.size(), inst.c_ptr(), e, e);
         TRACE("pdr", tout << mk_pp(e, m) << "\n";);
         m_instantiated_rules.push_back(m_current_rule);
         m_instantiations.push_back(to_app(e));
@@ -403,16 +407,18 @@ namespace pdr {
     }
 
     void quantifier_model_checker::refine() {
-        IF_VERBOSE(1, verbose_stream() << "instantiating quantifiers\n";);
+        datalog::mk_extract_quantifiers eq(m_ctx.get_context());
-        datalog::rule_manager& rule_m = m_rules.get_rule_manager();
+        datalog::rule_manager& rm = m_rules.get_rule_manager();
         datalog::rule_set new_rules(m_rules.get_context());
         datalog::rule_set::iterator it = m_rules.begin(), end = m_rules.end();
         for (; it != end; ++it) {
             datalog::rule* r = *it;
-            expr_ref_vector body(m);
+            datalog::var_counter vc(true);
+            unsigned max_var = vc.get_max_var(*r);
+            app_ref_vector body(m);
             for (unsigned i = 0; i < m_instantiations.size(); ++i) {
                 if (r == m_instantiated_rules[i]) {
-                    body.push_back(m_instantiations[i].get());
+                    eq.ensure_predicate(m_instantiations[i].get(), max_var, body);
                 }
             }
             if (body.empty()) {
@@ -425,14 +431,15 @@ namespace pdr {
                 quantifier_ref_vector* qs = 0;
                 m_quantifiers.find(r, qs);
                 m_quantifiers.remove(r);                
-                datalog::rule_ref_vector rules(rule_m);
+                datalog::rule_ref new_rule(rm);
-                expr_ref rule(m.mk_implies(m.mk_and(body.size(), body.c_ptr()), r->get_head()), m);
+                new_rule = rm.mk(r->get_head(), body.size(), body.c_ptr(), 0, r->name(), false);
-                std::cout << mk_pp(rule, m) << "\n";
+                new_rules.add_rule(new_rule);
-                rule_m.mk_rule(rule, rules, r->name());
+                m_quantifiers.insert(new_rule, qs);
-                for (unsigned i = 0; i < rules.size(); ++i) {
+                IF_VERBOSE(1, 
-                    new_rules.add_rule(rules[i].get());
+                           verbose_stream() << "instantiating quantifiers\n";                           
-                    m_quantifiers.insert(rules[i].get(), qs);
+                           r->display(m_ctx.get_context(), verbose_stream());
-                }
+                           verbose_stream() << "replaced by\n";
+                           new_rule->display(m_ctx.get_context(), verbose_stream()););
             }
         }
         new_rules.close();