rewrite quantifier module

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

src/muz_qe/pdr_context.cpp

@@ -65,10 +65,6 @@ namespace pdr {
         m_reachable(pm, pm.get_params()) {}
 
     pred_transformer::~pred_transformer() {
-        qinst_map::iterator it = m_rule2qinst.begin(), end = m_rule2qinst.end();
-        for (; it != end; ++it) {
-            dealloc(it->m_value);
-        }
         rule2inst::iterator it2 = m_rule2inst.begin(), end2 = m_rule2inst.end();
         for (; it2 != end2; ++it2) {
             dealloc(it2->m_value);
@@ -556,7 +552,6 @@ namespace pdr {
         // positions the variables occur are made equivalent with these.
         expr_ref_vector conj(m);
         app_ref_vector& var_reprs = *(alloc(app_ref_vector, m));
-        qinst* qi = 0;
         ptr_vector<app> aux_vars;
                 
         unsigned ut_size = rule.get_uninterpreted_tail_size();
@@ -581,19 +576,6 @@ namespace pdr {
         for (unsigned i = 0; i < tail.size(); ++i) {
             expr_ref tmp(m);
             var_subst(m, false)(tail[i].get(), var_reprs.size(), (expr*const*)var_reprs.c_ptr(), tmp);
-            quantifier* q;
-            if (datalog::rule_manager::is_forall(m, tmp, q)) {
-
-                if (!qi) {
-                    qi = alloc(qinst, m);                                      
-                }
-                //
-                // The contract is to instantiate q with 
-                // sufficient witnesses to validate body.
-                //
-                qi->quantifiers.push_back(q);
-                tmp = m.mk_true();
-            }
             conj.push_back(tmp);
             TRACE("pdr", tout << mk_pp(tail[i].get(), m) << "\n" << mk_pp(tmp, m) << "\n";);
             SASSERT(is_ground(tmp));
@@ -607,12 +589,10 @@ namespace pdr {
         TRACE("pdr", tout << mk_pp(fml, m) << "\n";);
         SASSERT(is_ground(fml));
         if (m.is_false(fml)) {
-            dealloc(qi);
-            qi = 0;
             // no-op.
         }
         else {
-            if (ut_size == 0 && !qi) {
+            if (ut_size == 0) {
                 init = m.mk_or(init, fml);
             }
             transitions.push_back(fml);            
@@ -620,9 +600,6 @@ namespace pdr {
             m_rule2transition.insert(&rule, fml.get());
             rules.push_back(&rule);
         }
-        if (qi) {
-            m_rule2qinst.insert(&rule, qi);            
-        }
         m_rule2inst.insert(&rule,&var_reprs);
         m_rule2vars.insert(&rule, aux_vars);
     }
@@ -1119,7 +1096,6 @@ namespace pdr {
           m_params(params),
           m(m),
           m_context(0),
-          m_quantifier_inst(*this, m),
           m_pm(m_fparams, m_params, m),
           m_query_pred(m),
           m_query(0),
@@ -1491,7 +1467,6 @@ namespace pdr {
             UNREACHABLE();
         }
         catch (model_exception) {        
-            check_quantifiers();
             IF_VERBOSE(1, verbose_stream() << "\n"; m_search.display(verbose_stream()););  
             m_last_result = l_true;
             validate();
@@ -1605,24 +1580,6 @@ namespace pdr {
         }
     }
 
-    //
-    // Check that quantifiers are satisfied in the produced model.
-    // 
-    void context::check_quantifiers() {
-        if (has_quantifiers()) {
-            m_quantifier_inst.model_check(m_search.get_root());
-        }
-    }
-
-    bool context::has_quantifiers() const {
-        decl2rel const& dr = get_pred_transformers();
-        decl2rel::iterator it = dr.begin(), end = dr.end();
-        for (; it != end; ++it) {
-            pred_transformer* pt = it->m_value;
-            if (pt->has_quantifiers()) return true;
-        }
-        return false;
-    }
 
     //
     // Pick a potential counter example state.
@@ -1832,8 +1789,7 @@ namespace pdr {
         for (unsigned i = 0; i < sig_size; ++i) {
             vars.push_back(m.mk_const(m_pm.o2n(pt.sig(i), 0)));
         }
-        ptr_vector<app> aux_vars;
+        ptr_vector<app>& aux_vars = pt.get_aux_vars(r);
-        pt.get_aux_vars(r, aux_vars);
         vars.append(aux_vars.size(), aux_vars.c_ptr());
 
         scoped_ptr<expr_replacer> rep;

src/muz_qe/pdr_context.h

@@ -29,7 +29,6 @@ Revision History:
 #include "dl_base.h"
 #include "pdr_prop_solver.h"
 #include "pdr_reachable_cache.h"
-#include "pdr_quantifiers.h"
 
 namespace datalog {
     class rule_set;
@@ -42,7 +41,6 @@ namespace pdr {
     class model_node;
     class context;
 
-    typedef obj_map<datalog::rule const, qinst*> qinst_map;
     typedef obj_map<datalog::rule const, app_ref_vector*> rule2inst;
     typedef obj_map<func_decl, pred_transformer*> decl2rel;
 
@@ -78,7 +76,6 @@ namespace pdr {
         obj_map<expr, unsigned>      m_prop2level;      // map property to level where it occurs.
         obj_map<expr, datalog::rule const*> m_tag2rule; // map tag predicate to rule. 
         rule2expr                    m_rule2tag;        // map rule to predicate tag.
-        qinst_map                    m_rule2qinst;      // map tag to quantifier instantiation.
         rule2inst                    m_rule2inst;       // map rules to instantiations of indices
         rule2expr                    m_rule2transition; // map rules to transition 
         rule2apps                    m_rule2vars;       // map rule to auxiliary variables
@@ -99,7 +96,6 @@ namespace pdr {
         void init_rule(decl2rel const& pts, datalog::rule const& rule, expr_ref& init,                                      
                        ptr_vector<datalog::rule const>& rules, expr_ref_vector& transition);
         void init_atom(decl2rel const& pts, app * atom, app_ref_vector& var_reprs, expr_ref_vector& conj, unsigned tail_idx);
-        void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars);
 
         void simplify_formulas(tactic& tac, expr_ref_vector& fmls);
 
@@ -122,8 +118,6 @@ namespace pdr {
         func_decl* const* sig() { init_sig(); return m_sig.c_ptr(); }
         expr*  transition() const { return m_transition; }
         expr*  initial_state() const { return m_initial_state; }
-        bool   has_quantifiers() const { return !m_rule2qinst.empty(); }
-        qinst* get_quantifiers(datalog::rule const* r) const { qinst* q = 0; m_rule2qinst.find(r, q); return q; }
         expr*  rule2tag(datalog::rule const* r) { return m_rule2tag.find(r); }
         unsigned get_num_levels() { return m_levels.size(); }
         expr_ref get_cover_delta(func_decl* p_orig, int level);
@@ -140,7 +134,7 @@ namespace pdr {
         void find_predecessors(model_core const& model, ptr_vector<func_decl>& preds) const;
         datalog::rule const& find_rule(model_core const& model) const;
         expr* get_transition(datalog::rule const& r) { return m_rule2transition.find(&r); }
-        void  get_aux_vars(datalog::rule const& r, ptr_vector<app>& vs) { m_rule2vars.find(&r, vs); }
+        ptr_vector<app>& get_aux_vars(datalog::rule const& r) { return m_rule2vars.find(&r); }
 
         bool propagate_to_next_level(unsigned level);
         void add_property(expr * lemma, unsigned lvl);  // add property 'p' to state at level.
@@ -166,6 +160,8 @@ namespace pdr {
 
         void inherit_properties(pred_transformer& other);
 
+        void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars);
+
     };
 
 
@@ -292,7 +288,6 @@ namespace pdr {
         params_ref const&    m_params;
         ast_manager&         m;
         datalog::context*    m_context;
-        quantifier_model_checker m_quantifier_inst;
         manager              m_pm;  
         decl2rel             m_rels;         // Map from relation predicate to fp-operator.       
         func_decl_ref        m_query_pred;
@@ -309,8 +304,6 @@ namespace pdr {
         // Functions used by search.
         void solve_impl();
         bool check_reachability(unsigned level);        
-        void check_quantifiers();
-        bool has_quantifiers() const;
         void propagate(unsigned max_prop_lvl);
         void close_node(model_node& n);
         void check_pre_closed(model_node& n);
@@ -396,8 +389,6 @@ namespace pdr {
 
         void set_axioms(expr* axioms) { m_pm.set_background(axioms); }
 
-        void refine(qi& q, datalog::rule_set& rules) { m_quantifier_inst.refine(q, rules); }
-
         unsigned get_num_levels(func_decl* p);
 
         expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p);
@@ -408,6 +399,8 @@ namespace pdr {
 
         proof_ref get_proof() const;
 
+        model_node& get_root() const { return m_search.get_root(); }
+
     };
 
 };

src/muz_qe/pdr_dl_interface.cpp

@@ -25,6 +25,7 @@ Revision History:
 #include "dl_mk_rule_inliner.h"
 #include "dl_rule.h"
 #include "dl_rule_transformer.h"
+#include "dl_mk_extract_quantifiers.h"
 #include "smt2parser.h"
 #include "pdr_context.h"
 #include "pdr_dl_interface.h"
@@ -32,6 +33,7 @@ Revision History:
 #include "dl_mk_slice.h"
 #include "dl_mk_unfold.h"
 #include "dl_mk_coalesce.h"
+#include "pdr_quantifiers.h"
 
 using namespace pdr;
 
@@ -145,12 +147,20 @@ lbool dl_interface::query(expr * query) {
         }
     }
 
+    // remove universal quantifiers from body.
+    datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx);
+    datalog::rule_transformer extract_q_tr(m_ctx);
+    extract_q_tr.register_plugin(extract_quantifiers);
+    m_ctx.transform_rules(extract_q_tr, mc, pc);
+    
+
     IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););
     m_pdr_rules.add_rules(m_ctx.get_rules());
     m_pdr_rules.close();
     m_ctx.reopen();
     m_ctx.replace_rules(old_rules);
 
+    quantifier_model_checker quantifier_mc(*m_context, m, extract_quantifiers->quantifiers(), m_pdr_rules);
 
     m_context->set_proof_converter(pc);
     m_context->set_model_converter(mc);
@@ -163,12 +173,17 @@ lbool dl_interface::query(expr * query) {
         return l_false;
     }
         
+    lbool result;
     while (true) {
-        try {
+        result = m_context->solve();
-            return m_context->solve();
+        if (result == l_true && extract_quantifiers->has_quantifiers()) {
+            if (quantifier_mc.check()) {
+                return l_true;
+            }
+            // else continue
         }
-        catch (pdr::qi& q) {
+        else {
-            m_context->refine(q, m_pdr_rules);
+            return result;
         }
     }
 }

src/muz_qe/pdr_quantifiers.cpp

@@ -115,166 +115,21 @@ namespace pdr {
         var_subst vs(m, false);
         vs(q->get_expr(), binding.size(), binding.c_ptr(), e);
         (*rep)(e);        
-        m_rules.push_back(m_current_rule);
+        m_instantiated_rules.push_back(m_current_rule);
-        m_apps.push_back(to_app(e));
+        m_instantiations.push_back(to_app(e));
         TRACE("pdr", tout << mk_pp(e, m) << "\n";);
     }
 
-    void quantifier_model_checker::model_check(model_node& root) {
-        m_apps.reset();
-        m_rules.reset();
-        ptr_vector<model_node> nodes;
-        get_nodes(root, nodes);
-        for (unsigned i = nodes.size(); i > 0; ) {
-            --i;
-            model_check_node(*nodes[i]);
-        }
-        if (m_apps.empty()) {
-            return;
-        }
-        qi q(m);
-        for (unsigned i = 0; i < m_apps.size(); ++i) {
-            q.add(m_rules[i], m_apps[i].get());
-        }
-        throw q;
-    }
 
     // As & not Body_i is satisfiable 
     // then instantiate with model for parameters to Body_i
 
-    bool quantifier_model_checker::find_instantiations(qinst& qi, unsigned level) {
+    bool quantifier_model_checker::find_instantiations(quantifier_ref_vector const& qs, unsigned level) {
         return 
-            find_instantiations_proof_based(qi, level); // ||
+            find_instantiations_proof_based(qs, level); // ||
-            // find_instantiations_qe_based(qi, level);
+            // find_instantiations_qe_based(qs, level);
     }
 
-    bool quantifier_model_checker::find_instantiations_model_based(qinst& qi, unsigned level) {
-        bool found_instance = false;
-        expr_ref C(m);
-        front_end_params fparams;
-        smt::kernel solver(m, fparams);
-        solver.assert_expr(m_A);
-        for (unsigned i = 0; i < m_Bs.size(); ++i) {
-            expr_ref_vector fresh_vars(m);
-            quantifier* q = qi.quantifiers[i].get();
-            for (unsigned j = 0; j < q->get_num_decls(); ++j) {
-                fresh_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j)));
-            }
-            var_subst varsubst(m, false);
-            varsubst(m_Bs[i].get(), fresh_vars.size(), fresh_vars.c_ptr(), C);
-            TRACE("pdr", tout << "updated propagation formula: " << mk_pp(C,m) << "\n";);
-            
-            solver.push();
-            // TBD: what to do with the different tags when unfolding the same predicate twice?
-            solver.assert_expr(m.mk_not(C));
-            lbool result = solver.check();
-            if (result == l_true) {
-                found_instance = true;
-                model_ref mr;
-                solver.get_model(mr);                
-                TRACE("pdr", model_smt2_pp(tout, m, *mr, 0););
-                
-                expr_ref_vector insts(m);
-                for (unsigned j = 0; j < fresh_vars.size(); ++j) {
-                    expr* interp = mr->get_const_interp(to_app(fresh_vars[j].get())->get_decl());
-                    if (interp) {
-                        insts.push_back(interp);
-                    }
-                    else {
-                        insts.push_back(fresh_vars[j].get());
-                    }
-                    TRACE("pdr", tout << mk_pp(insts.back(), m) << "\n";);
-                }
-                add_binding(q, insts);
-            }
-            solver.pop(1);
-        }
-        return found_instance;
-    }
-
-    //
-    // Build:
-    //
-    //    A & forall x . B1 & forall y . B2 & ...
-    // =  
-    //    not exists x y . (!A or !B1 or !B2 or ...)
-    // 
-    // Find an instance that satisfies formula.
-    // (or find all instances?)
-    //
-    bool quantifier_model_checker::find_instantiations_qe_based(qinst& qi, unsigned level) {
-        expr_ref_vector fmls(m), conjs(m), fresh_vars(m);
-        app_ref_vector all_vars(m);
-        expr_ref C(m);
-        qe::def_vector defs(m);
-        front_end_params fparams;
-        qe::expr_quant_elim qe(m, fparams);
-        for (unsigned i = 0; i < m_Bs.size(); ++i) {
-            quantifier* q = qi.quantifiers[i].get();
-            unsigned num_decls = q->get_num_decls();
-            unsigned offset = all_vars.size();
-            for (unsigned j = 0; j < num_decls; ++j) {
-                all_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j)));
-            }
-            var_subst varsubst(m, false);
-            varsubst(m_Bs[i].get(), num_decls, (expr**)(all_vars.c_ptr() + offset), C);
-            fmls.push_back(C);
-        }
-        conjs.push_back(m_A);
-        conjs.push_back(m.mk_not(m.mk_and(fmls.size(), fmls.c_ptr())));
-        // add previous instances.
-        expr* r = m.mk_and(m_Bs.size(), m_Bs.c_ptr());
-        m_trail.push_back(r);
-        expr* inst;
-        if (!m_bound.find(m_current_rule, r, inst)) {
-            TRACE("pdr", tout << "did not find: " << mk_pp(r, m) << "\n";);
-            m_trail.push_back(r);
-            inst = m.mk_true();
-            m_bound.insert(m_current_rule, r, inst);
-        }
-        else {
-            TRACE("pdr", tout << "blocking: " << mk_pp(inst, m) << "\n";);
-            conjs.push_back(inst);
-        }
-        C = m.mk_and(conjs.size(), conjs.c_ptr());
-        lbool result = qe.first_elim(all_vars.size(), all_vars.c_ptr(), C, defs);
-        TRACE("pdr", tout << mk_pp(C.get(), m) << "\n" << result << "\n";);
-        if (result != l_true) {
-            return false;
-        }
-        inst = m.mk_and(inst, m.mk_not(C));
-        m_trail.push_back(inst);
-        m_bound.insert(m_current_rule, r, inst);
-        TRACE("pdr",
-              tout << "Instantiating\n";
-              for (unsigned i = 0; i < defs.size(); ++i) {
-                  tout << defs.var(i)->get_name() << " " << mk_pp(defs.def(i), m) << "\n";
-              }
-              );
-        expr_substitution sub(m);  
-        for (unsigned i = 0; i < defs.size(); ++i) {
-            sub.insert(m.mk_const(defs.var(i)), defs.def(i));
-        }
-        scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
-        rep->set_substitution(&sub);
-        for (unsigned i = 0; i < all_vars.size(); ++i) {
-            expr_ref tmp(all_vars[i].get(), m);
-            (*rep)(tmp);
-            all_vars[i] = to_app(tmp);
-            }
-        unsigned offset = 0;
-        for (unsigned i = 0; i < m_Bs.size(); ++i) {
-            quantifier* q = qi.quantifiers[i].get();
-            unsigned num_decls = q->get_num_decls();                
-            expr_ref_vector new_binding(m);
-            for (unsigned j = 0; j < num_decls; ++j) {
-                new_binding.push_back(all_vars[offset+j].get());
-            }
-            offset += num_decls;
-            add_binding(q, new_binding);
-        }
-        return true;
-    }
 
     class collect_insts {
         ast_manager&     m;
@@ -322,7 +177,7 @@ namespace pdr {
         
     };
 
-    bool quantifier_model_checker::find_instantiations_proof_based(qinst& qi, unsigned level) {
+    bool quantifier_model_checker::find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level) {
         bool found_instance = false;
         TRACE("pdr", tout << mk_pp(m_A,m) << "\n";);
  
@@ -336,7 +191,7 @@ namespace pdr {
         expr_ref C(m);
         fmls.push_back(tr(m_A.get()));
         for (unsigned i = 0; i < m_Bs.size(); ++i) {
-            C = m.update_quantifier(qi.quantifiers[i].get(), m_Bs[i].get());
+            C = m.update_quantifier(qs[i], m_Bs[i].get());
             fmls.push_back(tr(C.get()));
         }        
         TRACE("pdr",
@@ -355,8 +210,8 @@ namespace pdr {
         }
         map<symbol, quantifier*, symbol_hash_proc, symbol_eq_proc> qid_map;
         quantifier* q;
-        for (unsigned i = 0; i < qi.quantifiers.size(); ++i) {
+        for (unsigned i = 0; i < qs.size();  ++i) {
-            q = qi.quantifiers[i].get();
+            q = qs[i];
             qid_map.insert(q->get_qid(), q);
         }
 
@@ -391,7 +246,7 @@ namespace pdr {
         if (collector.size() == 0) {
             // Try to create dummy instances.
             for (unsigned i = 0; i < m_Bs.size(); ++i) {
-                q = qi.quantifiers[i].get();
+                q = qs[i];
                 expr_ref_vector binding(m);
                 for (unsigned j = 0; j < q->get_num_decls(); ++j) {
                     binding.push_back(m.mk_fresh_const("B", q->get_decl_sort(j)));
@@ -403,7 +258,6 @@ namespace pdr {
         return found_instance;
     }
 
-
     void quantifier_model_checker::model_check_node(model_node& node) {
         TRACE("pdr", node.display(tout, 0););
         pred_transformer& pt = node.pt();
@@ -411,9 +265,6 @@ namespace pdr {
         expr_ref A(m), B(m), C(m);
         expr_ref_vector As(m);
         m_Bs.reset();
-        if (!pt.has_quantifiers()) {
-            return;
-        }
         //
         // nodes from leaves that are repeated 
         // inside the search tree don't have models.
@@ -427,10 +278,12 @@ namespace pdr {
         if (!m_current_rule) { 
             return;
         }
-        qinst* qi = pt.get_quantifiers(m_current_rule);
+        
-        if (!qi) {
+        quantifier_ref_vector* qis = 0;
+        m_quantifiers.find(m_current_rule, qis);
+        if (!qis) {
             return;
-        }        
+        }
         unsigned level = node.level();
         unsigned previous_level = (level == 0)?0:(level-1);
 
@@ -440,42 +293,69 @@ namespace pdr {
         m_A = pm.mk_and(As);
 
         // Add quantifiers:
-        scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
+        
-        for (unsigned j = 0; j < qi->quantifiers.size(); ++j) {
+        {
-            quantifier* q = qi->quantifiers[j].get();         
+            datalog::scoped_no_proof _no_proof(m);
-            app* a = to_app(q->get_expr());
+            scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
-            func_decl* f = a->get_decl();
+            for (unsigned j = 0; j < qis->size(); ++j) {
-            pred_transformer& pt2 = m_ctx.get_pred_transformer(f);
+                quantifier* q = (*qis)[j].get();
-            B = pt2.get_formulas(previous_level, true);
+                app* a = to_app(q->get_expr());
-            TRACE("pdr", tout << mk_pp(B, m) << "\n";);
+                func_decl* f = a->get_decl();
-            
+                pred_transformer& pt2 = m_ctx.get_pred_transformer(f);
-            expr_substitution sub(m);  
+                B = pt2.get_formulas(previous_level, true);
-            for (unsigned i = 0; i < a->get_num_args(); ++i) {
+                
-                expr* v = m.mk_const(pm.o2n(pt2.sig(i),0));
+                expr_substitution sub(m);  
-                sub.insert(v, a->get_arg(i));
+                expr_ref_vector refs(m);
+                for (unsigned i = 0; i < a->get_num_args(); ++i) {
+                    expr* v = m.mk_const(pm.o2n(pt2.sig(i),0));
+                    sub.insert(v, a->get_arg(i));
+                    refs.push_back(v);
+                }
+                rep->set_substitution(&sub);
+                (*rep)(B);
+                app_ref_vector& inst      = pt.get_inst(m_current_rule);
+                ptr_vector<app>& aux_vars = pt.get_aux_vars(*m_current_rule);
+                pt.ground_free_vars(B, inst, aux_vars);
+                var_subst vs(m, false);
+                vs(B, inst.size(), (expr*const*)inst.c_ptr(), B);
+                m_Bs.push_back(B);
             }
-            rep->set_substitution(&sub);
-            // TBD: exclude previous bindings here.
-            (*rep)(B);
-            m_Bs.push_back(B);
-            TRACE("pdr", 
-                  tout << mk_pp(q, m) << "\n";
-                  tout << "propagation formula: " << mk_pp(B, m) << "\n";);
         }
-        find_instantiations(*qi, level);
+
+        TRACE("pdr", 
+              tout << "A:\n" << mk_pp(m_A, m) << "\n";
+              tout << "B:\n";
+              for (unsigned i = 0; i < m_Bs.size(); ++i) {
+                  tout << mk_pp((*qis)[i].get(), m) << "\n" << mk_pp(m_Bs[i].get(), m) << "\n";
+              }
+              );
+
+        find_instantiations(*qis, level);
     }
 
-    void quantifier_model_checker::refine(qi& q, datalog::rule_set& rules) {
+    bool quantifier_model_checker::model_check(model_node& root) {
+        m_instantiations.reset();
+        m_instantiated_rules.reset();
+        ptr_vector<model_node> nodes;
+        get_nodes(root, nodes);
+        for (unsigned i = nodes.size(); i > 0; ) {
+            --i;
+            model_check_node(*nodes[i]);
+        }
+        return m_instantiations.empty();
+    }
+
+    void quantifier_model_checker::refine() {
         IF_VERBOSE(1, verbose_stream() << "instantiating quantifiers\n";);
-        datalog::rule_manager& rule_m = rules.get_rule_manager();
+        datalog::rule_manager& rule_m = m_rules.get_rule_manager();
-        datalog::rule_set new_rules(rules.get_context());
+        datalog::rule_set new_rules(m_rules.get_context());
-        datalog::rule_set::iterator it = rules.begin(), end = rules.end();
+        datalog::rule_set::iterator it = m_rules.begin(), end = m_rules.end();
         for (; it != end; ++it) {
             datalog::rule* r = *it;
-            app_ref_vector body(m);
+            expr_ref_vector body(m);
-            for (unsigned i = 0; i < q.size(); ++i) {
+            for (unsigned i = 0; i < m_instantiations.size(); ++i) {
-                if (r == q.get_rule(i)) {
+                if (r == m_instantiated_rules[i]) {
-                    body.push_back(q.get_app(i));
+                    body.push_back(m_instantiations[i].get());
                 }
             }
             if (body.empty()) {
@@ -485,19 +365,165 @@ namespace pdr {
                 for (unsigned i = 0; i < r->get_tail_size(); ++i) {
                     body.push_back(r->get_tail(i));
                 }
+                quantifier_ref_vector* qs = 0;
+                m_quantifiers.find(r, qs);
+                m_quantifiers.remove(r);
                 datalog::rule_ref_vector rules(rule_m);
-                expr_ref rule(m.mk_implies(m.mk_and(body.size(), (expr*const*)body.c_ptr()), r->get_head()), m);
+                expr_ref rule(m.mk_implies(m.mk_and(body.size(), body.c_ptr()), r->get_head()), m);
                 rule_m.mk_rule(rule, rules, r->name());
                 for (unsigned i = 0; i < rules.size(); ++i) {
                     new_rules.add_rule(rules[i].get());
+                    m_quantifiers.insert(rules[i].get(), qs);
                 }
             }
         }
         new_rules.close();                  
-        rules.reset();
+        m_rules.reset();
-        rules.add_rules(new_rules);
+        m_rules.add_rules(new_rules);
-        rules.close();
+        m_rules.close();
-        m_ctx.update_rules(rules);
+        m_ctx.update_rules(m_rules);
-        TRACE("pdr", rules.display(tout););
+        TRACE("pdr", m_rules.display(tout););
+    }
+
+    bool quantifier_model_checker::check() {
+        if (model_check(m_ctx.get_root())) {
+            return true;
+        }
+        refine();
+        return false;
     }
 };
+
+
+#if 0
+    //
+    // Build:
+    //
+    //    A & forall x . B1 & forall y . B2 & ...
+    // =  
+    //    not exists x y . (!A or !B1 or !B2 or ...)
+    // 
+    // Find an instance that satisfies formula.
+    // (or find all instances?)
+    //
+    bool quantifier_model_checker::find_instantiations_qe_based(quantifier_ref_vector const& qs, unsigned level) {
+        expr_ref_vector fmls(m), conjs(m), fresh_vars(m);
+        app_ref_vector all_vars(m);
+        expr_ref C(m);
+        qe::def_vector defs(m);
+        front_end_params fparams;
+        qe::expr_quant_elim qe(m, fparams);
+        for (unsigned i = 0; i < m_Bs.size(); ++i) {
+            quantifier* q = qs[i];
+            unsigned num_decls = q->get_num_decls();
+            unsigned offset = all_vars.size();
+            for (unsigned j = 0; j < num_decls; ++j) {
+                all_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j)));
+            }
+            var_subst varsubst(m, false);
+            varsubst(m_Bs[i].get(), num_decls, (expr**)(all_vars.c_ptr() + offset), C);
+            fmls.push_back(C);
+        }
+        conjs.push_back(m_A);
+        conjs.push_back(m.mk_not(m.mk_and(fmls.size(), fmls.c_ptr())));
+        // add previous instances.
+        expr* r = m.mk_and(m_Bs.size(), m_Bs.c_ptr());
+        m_trail.push_back(r);
+        expr* inst;
+        if (!m_bound.find(m_current_rule, r, inst)) {
+            TRACE("pdr", tout << "did not find: " << mk_pp(r, m) << "\n";);
+            m_trail.push_back(r);Newton Sanches
+            inst = m.mk_true();
+            m_bound.insert(m_current_rule, r, inst);
+        }
+        else {
+            TRACE("pdr", tout << "blocking: " << mk_pp(inst, m) << "\n";);
+            conjs.push_back(inst);
+        }
+        C = m.mk_and(conjs.size(), conjs.c_ptr());
+        lbool result = qe.first_elim(all_vars.size(), all_vars.c_ptr(), C, defs);
+        TRACE("pdr", tout << mk_pp(C.get(), m) << "\n" << result << "\n";);
+        if (result != l_true) {
+            return false;
+        }
+        inst = m.mk_and(inst, m.mk_not(C));
+        m_trail.push_back(inst);
+        m_bound.insert(m_current_rule, r, inst);
+        TRACE("pdr",
+              tout << "Instantiating\n";
+              for (unsigned i = 0; i < defs.size(); ++i) {
+                  tout << defs.var(i)->get_name() << " " << mk_pp(defs.def(i), m) << "\n";
+              }
+              );
+        expr_substitution sub(m);  
+        for (unsigned i = 0; i < defs.size(); ++i) {
+            sub.insert(m.mk_const(defs.var(i)), defs.def(i));
+        }
+        scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
+        rep->set_substitution(&sub);
+        for (unsigned i = 0; i < all_vars.size(); ++i) {
+            expr_ref tmp(all_vars[i].get(), m);
+            (*rep)(tmp);
+            all_vars[i] = to_app(tmp);
+            }
+        unsigned offset = 0;
+        for (unsigned i = 0; i < m_Bs.size(); ++i) {
+            quantifier* q = qs[i];
+            unsigned num_decls = q->get_num_decls();                
+            expr_ref_vector new_binding(m);
+            for (unsigned j = 0; j < num_decls; ++j) {
+                new_binding.push_back(all_vars[offset+j].get());
+            }
+            offset += num_decls;
+            add_binding(q, new_binding);
+        }
+        return true;
+    }
+
+    bool quantifier_model_checker::find_instantiations_model_based(quantifier_ref_vector const& qs, unsigned level) {
+        bool found_instance = false;
+        expr_ref C(m);
+        front_end_params fparams;
+        smt::kernel solver(m, fparams);
+        solver.assert_expr(m_A);
+        for (unsigned i = 0; i < m_Bs.size(); ++i) {
+            expr_ref_vector fresh_vars(m);
+            quantifier* q = qs[i];
+            for (unsigned j = 0; j < q->get_num_decls(); ++j) {
+                fresh_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j)));
+            }
+            var_subst varsubst(m, false);
+            varsubst(m_Bs[i].get(), fresh_vars.size(), fresh_vars.c_ptr(), C);
+            TRACE("pdr", tout << "updated propagation formula: " << mk_pp(C,m) << "\n";);
+            
+            solver.push();
+            // TBD: what to do with the different tags when unfolding the same predicate twice?
+            solver.assert_expr(m.mk_not(C));
+            lbool result = solver.check();
+            if (result == l_true) {
+                found_instance = true;
+                model_ref mr;
+                solver.get_model(mr);                
+                TRACE("pdr", model_smt2_pp(tout, m, *mr, 0););
+                
+                expr_ref_vector insts(m);
+                for (unsigned j = 0; j < fresh_vars.size(); ++j) {
+                    expr* interp = mr->get_const_interp(to_app(fresh_vars[j].get())->get_decl());
+                    if (interp) {
+                        insts.push_back(interp);
+                    }
+                    else {
+                        insts.push_back(fresh_vars[j].get());
+                    }
+                    TRACE("pdr", tout << mk_pp(insts.back(), m) << "\n";);
+                }
+                add_binding(q, insts);
+            }
+            solver.pop(1);
+        }
+        return found_instance;
+    }
+
+
+#endif
+

src/muz_qe/pdr_quantifiers.h

@@ -33,52 +33,31 @@ namespace pdr {
     class model_node;
     class pred_transformer;
     class context;
-
-    struct qinst {
-        quantifier_ref_vector  quantifiers; // quantifiers in rule body.
-        func_decl_ref_vector   predicates;  // predicates in order of bindings.
-        expr_ref_vector        bindings;    // the actual instantiations of the predicates
-        qinst(ast_manager& m): quantifiers(m), predicates(m), bindings(m) {}
-    };
-
-    class qi {
-        ptr_vector<datalog::rule const>     m_rules;
-        app_ref_vector                     m_apps;
-    public:
-        qi(ast_manager& m) : m_apps(m) {}
-        void add(datalog::rule const* r, app* a) {
-            m_rules.push_back(r);
-            m_apps.push_back(a);
-        }
-        unsigned size() const { return m_rules.size(); }
-        datalog::rule const* get_rule(unsigned i) const { return m_rules[i]; }
-        app*           get_app(unsigned i) const { return m_apps[i]; }
-    };
     
     
     class quantifier_model_checker {
         context&                      m_ctx;
         ast_manager&                  m;
-        obj_pair_map<datalog::rule const, expr, expr*> m_bound;
+        obj_map<datalog::rule const, quantifier_ref_vector*>& m_quantifiers;
+        datalog::rule_set&            m_rules;
         expr_ref_vector               m_trail;
         expr_ref                      m_A;
         expr_ref_vector               m_Bs;
         pred_transformer*             m_current_pt;
         datalog::rule const*          m_current_rule;
         model_node*                   m_current_node;
-
+        app_ref_vector                  m_instantiations;
-        ptr_vector<datalog::rule const>     m_rules;
+        ptr_vector<datalog::rule const> m_instantiated_rules;
-        app_ref_vector                      m_apps;
 
         void model_check_node(model_node& node);
 
-        bool find_instantiations(qinst& qi, unsigned level); 
+        bool find_instantiations(quantifier_ref_vector const& qs, unsigned level); 
 
-        bool find_instantiations_model_based(qinst& qi, unsigned level);
+        bool find_instantiations_model_based(quantifier_ref_vector const& qs, unsigned level);
 
-        bool find_instantiations_proof_based(qinst& qi, unsigned level);
+        bool find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level);
 
-        bool find_instantiations_qe_based(qinst& qi, unsigned level);
+        bool find_instantiations_qe_based(quantifier_ref_vector const& qs, unsigned level);
 
         void add_binding(quantifier* q, expr_ref_vector& binding);
 
@@ -88,12 +67,8 @@ namespace pdr {
 
         void generalize_binding(expr_ref_vector const& binding, unsigned idx, expr_ref_vector& new_binding, vector<expr_ref_vector>& bindings);
 
-    public:
+        void refine();
-        quantifier_model_checker(context& ctx, ast_manager& m): 
+
-            m_ctx(ctx),
-            m(m), m_trail(m), m_A(m), m_Bs(m),             
-            m_current_pt(0), m_current_rule(0), 
-            m_current_node(0), m_apps(m) {}
 
         /**
            \brief model check a potential model against quantifiers in bodies of rules.
@@ -102,9 +77,23 @@ namespace pdr {
            'false' and a set of instantiations that contradict the current model.
         */
         
-        void model_check(model_node& root);
+        bool model_check(model_node& root);
 
-        void refine(qi& q, datalog::rule_set& rules);
+    public:
+        quantifier_model_checker(
+            context& ctx, 
+            ast_manager& m, 
+            obj_map<datalog::rule const, quantifier_ref_vector*>& quantifiers, 
+            datalog::rule_set& rules) : 
+            m_ctx(ctx),
+            m(m),
+            m_quantifiers(quantifiers),
+            m_rules(rules),
+            m_trail(m), m_A(m), m_Bs(m),             
+            m_current_pt(0), m_current_rule(0), 
+            m_current_node(0), m_instantiations(m) {}
+
+        bool check();
     };
 
 };