fix regression for simplifying tails with quantifiers, add some more handling for quantified tails

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

src/ast/ast.cpp

@@ -2637,12 +2637,13 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
     ptr_buffer<expr> args;
     args.append(num_proofs, (expr**) proofs);
     expr * fact;
-    expr const * f1 = get_fact(proofs[0]);
+    expr * f1 = get_fact(proofs[0]);
-    expr const * f2 = get_fact(proofs[1]);
+    expr * f2 = get_fact(proofs[1]);
     if (num_proofs == 2 && is_complement(f1, f2)) {
         fact = mk_false();
     }
     else {
+        CTRACE("mk_unit_resolution_bug", !is_or(f1), tout << mk_pp(f1, *this) << " " << mk_pp(f2, *this) << "\n";);
         SASSERT(is_or(f1));
         ptr_buffer<expr> new_lits;
         app const * cls   = to_app(f1);

src/muz_qe/dl_mk_interp_tail_simplifier.cpp

@@ -463,7 +463,7 @@ namespace datalog {
 
         if (r->has_quantifiers()) {
             res = r;
-            return false;
+            return true;
         }
 
     start:

src/muz_qe/dl_util.h

@@ -191,6 +191,11 @@ namespace datalog {
         scoped_coarse_proof(ast_manager& m): scoped_proof_mode(m, PGM_COARSE) {}
     };
 
+    class scoped_fine_proof : public scoped_proof_mode {
+    public:
+        scoped_fine_proof(ast_manager& m): scoped_proof_mode(m, PGM_FINE) {}
+    };
+
     class scoped_no_proof : public scoped_proof_mode {
     public:
         scoped_no_proof(ast_manager& m): scoped_proof_mode(m, PGM_DISABLED) {}

src/muz_qe/expr_safe_replace.cpp

@@ -0,0 +1,102 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    expr_safe_replace.cpp
+
+Abstract:
+
+    Version of expr_replace/expr_substitution that is safe for quantifiers.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-30
+
+Revision History:
+
+
+--*/
+
+#include "expr_safe_replace.h"
+#include "rewriter.h"
+
+
+void expr_safe_replace::insert(expr* src, expr* dst) {
+    m_src.push_back(src);
+    m_dst.push_back(dst);
+    m_subst.insert(src, dst);
+}
+
+void expr_safe_replace::operator()(expr* e, expr_ref& res) {
+    obj_map<expr,expr*> cache;
+    ptr_vector<expr> todo, args;
+    expr_ref_vector refs(m);
+    todo.push_back(e);
+    expr* a, *b, *d;
+    todo.push_back(e);
+    
+    while (!todo.empty()) {
+        a = todo.back();
+        if (cache.contains(a)) {
+            todo.pop_back();
+        }
+        else if (m_subst.find(a, b)) {
+            cache.insert(a, b);
+            todo.pop_back();
+        }
+        else if (is_var(a)) {
+            cache.insert(a, a);
+            todo.pop_back();
+        }
+        else if (is_app(a)) {
+            app* c = to_app(a);
+            unsigned n = c->get_num_args();
+            args.reset();
+            for (unsigned i = 0; i < n; ++i) {
+                if (cache.find(c->get_arg(i), d)) {
+                    args.push_back(d);
+                }
+                else {
+                    todo.push_back(c->get_arg(i));
+                }
+            }
+            if (args.size() == n) {
+                b = m.mk_app(c->get_decl(), args.size(), args.c_ptr());
+                refs.push_back(b);
+                cache.insert(a, b);
+                todo.pop_back();
+            }
+        }
+        else {
+            SASSERT(is_quantifier(a));
+            quantifier* q = to_quantifier(a);
+            expr_safe_replace replace(m);
+            var_shifter shift(m);
+            expr_ref new_body(m), src(m), dst(m), tmp(m);
+            expr_ref_vector pats(m), nopats(m);
+            unsigned num_decls = q->get_num_decls();
+            for (unsigned i = 0; i < m_src.size(); ++i) {
+                shift(m_src[i].get(), num_decls, src);
+                shift(m_dst[i].get(), num_decls, dst);
+                replace.insert(src, dst);
+            }
+            unsigned np = q->get_num_patterns();
+            for (unsigned i = 0; i < np; ++i) {
+                replace(q->get_pattern(i), tmp);
+                pats.push_back(tmp);
+            }
+            np = q->get_num_no_patterns();
+            for (unsigned i = 0; i < np; ++i) {
+                replace(q->get_no_pattern(i), tmp);
+                nopats.push_back(tmp);
+            }
+            replace(q->get_expr(), new_body);
+            b = m.update_quantifier(q, pats.size(), pats.c_ptr(), nopats.size(), nopats.c_ptr(), new_body);
+            refs.push_back(b);
+            cache.insert(a, b);
+            todo.pop_back();
+        }        
+    }
+    res = cache.find(e);
+}

src/muz_qe/expr_safe_replace.h

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    expr_safe_replace.h
+
+Abstract:
+
+    Version of expr_replace/expr_substitution that is safe for quantifiers.
+    
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-30
+
+Revision History:
+
+
+--*/
+
+#ifndef __EXPR_SAFE_REPLACE_H__
+#define __EXPR_SAFE_REPLACE_H__
+
+#include "ast.h"
+
+class expr_safe_replace {
+    ast_manager& m;
+    expr_ref_vector m_src;
+    expr_ref_vector m_dst;
+    obj_map<expr, expr*> m_subst;
+
+public:
+    expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m) {}
+
+    void insert(expr* src, expr* dst);
+
+    void operator()(expr_ref& e) { (*this)(e.get(), e); }
+
+    void operator()(expr* src, expr_ref& e);
+};
+
+#endif /* __EXPR_SAFE_REPLACE_H__ */

src/muz_qe/pdr_quantifiers.cpp

@@ -27,6 +27,9 @@ Revision History:
 #include "ast_smt_pp.h"
 #include "expr_abstract.h"
 #include "dl_mk_extract_quantifiers.h"
+#include "qe_lite.h"
+#include "well_sorted.h"
+#include "expr_safe_replace.h"
 
 
 namespace pdr {
@@ -49,6 +52,12 @@ namespace pdr {
         }
     }
 
+    quantifier_model_checker::~quantifier_model_checker() {
+        obj_map<func_decl,expr*>::iterator it = m_reachable.begin(), end = m_reachable.end();
+        for (; it != end; ++it) {
+            m.dec_ref(it->m_value);
+        }
+    }
 
     void quantifier_model_checker::generalize_binding(expr_ref_vector const& binding, vector<expr_ref_vector>& bindings) {
         expr_ref_vector new_binding(m);
@@ -193,13 +202,12 @@ namespace pdr {
 
     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";);
  
-        datalog::scoped_coarse_proof _scp(m);
+        datalog::scoped_fine_proof _scp(m);
 
         expr_ref_vector fmls(m);
         front_end_params fparams;
-        fparams.m_proof_mode = PGM_COARSE;
+        fparams.m_proof_mode = PGM_FINE;
         fparams.m_mbqi = true;
 
         fmls.push_back(m_A.get());
@@ -209,15 +217,20 @@ namespace pdr {
               for (unsigned i = 0; i < fmls.size(); ++i) {
                   tout << mk_pp(fmls[i].get(), m) << "\n";
               });
+
         smt::kernel solver(m, fparams);
         for (unsigned i = 0; i < fmls.size(); ++i) {
             solver.assert_expr(fmls[i].get());
         }
         lbool result = solver.check();
-        if (result != l_false) {
+
         TRACE("pdr", tout << result << "\n";);
-            return found_instance;
+
+        if (result != l_false) {
+            return false;
         }
+        m_rules_model_check = false;
+
         map<symbol, quantifier*, symbol_hash_proc, symbol_eq_proc> qid_map;
         quantifier* q;
         for (unsigned i = 0; i < qs.size();  ++i) {
@@ -234,8 +247,7 @@ namespace pdr {
         for (unsigned i = 0; i < collector.size(); ++i) {
             symbol qid = quants[i]->get_qid();
             if (!qid_map.find(qid, q)) {
-                TRACE("pdr", tout << "Could not find quantifier " 
+                TRACE("pdr", tout << "Could not find quantifier " << mk_pp(quants[i], m) << "\n";);
-                      << mk_pp(quants[i], m) << "\n";);
                 continue;
             }
             expr_ref_vector const& binding = collector.bindings()[i];
@@ -256,8 +268,43 @@ namespace pdr {
         return found_instance;
     }
 
+
     /**
-       Given node:
+       For under-approximations:
+
+       m_reachable: set of reachable states, per predicate
+       
+       rules:       P(x)   :- B[x,y] & Fa z . Q(y,z)
+                    Q(y,z) :- C[y,z,u] & Fa w . R(u,w)
+       
+       qis:         Fa z . Q(y,z)
+       
+       M:           model satisfying P(x) & B[x,y]
+       
+       B'[x,y]:     body with reachable states substituted for predicates.
+       
+       Q'[y,z]:     reachable states substituted for Q.
+       
+       S'[x]:       Ex y . B'[x,y] & Fa z . Q'[y, z]
+       
+       Method:
+
+       1. M |= Fa z . Q'[y, z] => done
+          
+          Weaker variant: 
+          Check B[x,y] & Fa z . Q'[y, z] for consistency.
+
+       2. Otherwise, extract instantiations.
+      
+       3. Update reachable (for next round):
+
+          Q'[y,z] :=  Q'[y,z] \/ C'[y,z,u] & Fa w . R'(u,w)
+          
+    */
+
+
+    /**
+       For over-approximations:
 
          - pt - predicate transformer for rule:
                 P(x) :- Body1(x,y) || Body2(x,z) & (Fa u . Q(u,x,z)).
@@ -267,22 +314,201 @@ namespace pdr {
 
          - A  := node.state(x) && Body2(x,y)
 
+
          - Bs := array of Bs of the form:
                  . Fa u . Q(u, P_x, P_y)  - instantiate quantifier to P variables.
                  . B := inv(Q_0,Q_1,Q_2)
                  . B := inv(u, P_x, P_y) := B[u/Q_0, P_x/Q_1, P_y/Q_2]
                  . B := Fa u . inv(u, P_x, P_y)
        
-       
     */
 
+    void quantifier_model_checker::update_reachable(func_decl* f, expr* e) {
+        expr* e_old;
+        m.inc_ref(e);
+        if (m_reachable.find(f, e_old)) {
+            m.dec_ref(e_old);
+        }
+        m_reachable.insert(f, e);
+    }
+
+
+    expr_ref quantifier_model_checker::get_reachable(func_decl* p) {
+        expr* e = 0;
+        if (!m_reachable.find(p, e)) {
+            e = m_ctx.get_pred_transformer(p).initial_state();
+            update_reachable(p, e);
+        }
+        return expr_ref(e, m);
+    }
+
+    void quantifier_model_checker::add_over_approximations(quantifier_ref_vector& qis, model_node& n) {
+        add_approximations(qis, n, true);
+    }
+
+    void quantifier_model_checker::add_under_approximations(quantifier_ref_vector& qis, model_node& n) {
+        add_approximations(qis, n, false);
+    }
+    
+    void quantifier_model_checker::add_approximations(quantifier_ref_vector& qis, model_node& n, bool is_over) {
+        pred_transformer& pt = n.pt();
+        manager& pm = pt.get_pdr_manager();
+        unsigned level = n.level();
+        expr_ref_vector Bs(m);
+        expr_ref B(m), v(m);
+        quantifier_ref q(m);
+        datalog::scoped_no_proof _no_proof(m);
+        scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
+        for (unsigned j = 0; j < qis.size(); ++j) {
+            q = qis[j].get();
+            app_ref_vector& inst      = pt.get_inst(m_current_rule);
+            TRACE("pdr", 
+                  tout << "q:\n" << mk_pp(q, m) << "\n";
+                  tout << "level: " << level << "\n";
+                  model_smt2_pp(tout, m, n.get_model(), 0);
+                  m_current_rule->display(m_ctx.get_context(), tout << "rule:\n");                  
+                  );
+            
+            var_subst vs(m, false);
+            vs(q, inst.size(), (expr*const*)inst.c_ptr(), B);
+            q = to_quantifier(B);
+            TRACE("pdr", tout << "q instantiated:\n" << mk_pp(q, m) << "\n";);
+            
+            app* a = to_app(q->get_expr());
+            func_decl* f = a->get_decl();
+            pred_transformer& pt2 = m_ctx.get_pred_transformer(f);
+            if (is_over) {
+                B = pt2.get_formulas(level - 1, false);
+            }
+            else {
+                B = get_reachable(f);
+                SASSERT(is_well_sorted(m, B));
+            }
+            TRACE("pdr", tout << "B:\n" << mk_pp(B, m) << "\n";);
+                    
+            expr_safe_replace sub(m);
+            for (unsigned i = 0; i < a->get_num_args(); ++i) {
+                v = m.mk_const(pm.o2n(pt2.sig(i),0));
+                sub.insert(v, a->get_arg(i));
+            }
+            sub(B);
+            TRACE("pdr", tout << "B substituted:\n" << mk_pp(B, m) << "\n";);
+            datalog::flatten_and(B, Bs);
+            for (unsigned i = 0; i < Bs.size(); ++i) {
+                m_Bs.push_back(m.update_quantifier(q, Bs[i].get()));                    
+            }
+        }
+    }
+
+    /**
+       \brief compute strongest post-conditions for each predicate transformer.
+       (or at least something sufficient to change the set of current counter-examples)
+     */
+    void quantifier_model_checker::weaken_under_approximation() {
+
+        datalog::rule_set::decl2rules::iterator it = m_rules.begin_grouped_rules(), end = m_rules.end_grouped_rules();
+        
+        for (; it != end; ++it) {
+            func_decl* p = it->m_key;
+            datalog::rule_vector& rules = *it->m_value;
+            expr_ref_vector bodies(m);
+            for (unsigned i = 0; i < rules.size(); ++i) {
+                bodies.push_back(strongest_post_condition(*rules[i]));
+            }           
+            update_reachable(p, m.mk_or(bodies.size(), bodies.c_ptr()));
+        }
+    }
+
+    expr_ref quantifier_model_checker::strongest_post_condition(datalog::rule& r) {
+        pred_transformer& pt = m_ctx.get_pred_transformer(r.get_decl());
+        manager& pm = pt.get_pdr_manager();
+        quantifier_ref_vector* qis = 0;
+        m_quantifiers.find(&r, qis);        
+        expr_ref_vector body(m), inst(m);
+        expr_ref fml(m), v(m);        
+        app* a;
+        func_decl* p;
+        svector<symbol> names;
+        unsigned ut_size = r.get_uninterpreted_tail_size();
+        unsigned t_size  = r.get_tail_size();   
+        var_subst vs(m, false);
+        sort_ref_vector vars(m);
+        r.get_vars(vars);
+        if (qis) {
+            quantifier_ref_vector const& qi = *qis;
+            for (unsigned i = 0; i < qi.size(); ++i) {
+                fml = qi[i]->get_expr();
+                a = to_app(fml);
+                p = a->get_decl();
+                expr* p_reach = get_reachable(p);
+                pred_transformer& pt2 = m_ctx.get_pred_transformer(p);
+                expr_safe_replace sub(m);
+                for (unsigned j = 0; j < a->get_num_args(); ++j) {
+                    v = m.mk_const(pm.o2n(pt2.sig(j),0));
+                    sub.insert(v, a->get_arg(j));
+                }
+                sub(p_reach, fml);
+                body.push_back(m.update_quantifier(qi[i], fml));
+            }
+        }
+        a = r.get_head();
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {
+            v = m.mk_var(vars.size()+i, m.get_sort(a->get_arg(i)));
+            body.push_back(m.mk_eq(v, a->get_arg(i)));
+        }
+        for (unsigned i = 0; i < ut_size; ++i) {
+            a = r.get_tail(i);
+            p = a->get_decl();
+            pred_transformer& pt2 = m_ctx.get_pred_transformer(p);
+            expr* p_reach = get_reachable(p);
+            expr_safe_replace sub(m);
+            for (unsigned i = 0; i < a->get_num_args(); ++i) {
+                v = m.mk_const(pm.o2n(pt2.sig(i),0));
+                sub.insert(v, a->get_arg(i));
+            }
+            sub(p_reach, fml);
+            body.push_back(fml);
+        }
+        for (unsigned i = ut_size; i < t_size; ++i) {
+            body.push_back(r.get_tail(i));
+        }
+        fml = m.mk_and(body.size(), body.c_ptr());
+        vars.reverse();
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            names.push_back(symbol(i));
+        }
+        if (!vars.empty()) {
+            fml = m.mk_exists(vars.size(), vars.c_ptr(), names.c_ptr(), fml);
+            SASSERT(is_well_sorted(m, fml));
+        }
+
+        for (unsigned i = 0; i < r.get_head()->get_num_args(); ++i) {
+            inst.push_back(m.mk_const(pm.o2n(pt.sig(i),0)));
+        }
+        vs(fml, inst.size(), inst.c_ptr(), fml);
+        SASSERT(is_well_sorted(m, fml));
+        if (!vars.empty()) {
+            fml = to_quantifier(fml)->get_expr();
+            uint_set empty_index_set;
+            qe_lite qe(m);
+            qe(empty_index_set, false, fml);
+            fml = m.mk_exists(vars.size(), vars.c_ptr(), names.c_ptr(), fml);
+            SASSERT(is_well_sorted(m, fml));
+            m_ctx.get_context().get_rewriter()(fml);
+        }
+        SASSERT(is_well_sorted(m, fml));
+        
+        IF_VERBOSE(0, verbose_stream() << "instantiate to\n:" << mk_pp(fml, m) << "\n";);
+        return fml;
+    }
+
 
     void quantifier_model_checker::model_check_node(model_node& node) {
         TRACE("pdr", node.display(tout, 0););
         pred_transformer& pt = node.pt();
         manager& pm = pt.get_pdr_manager();
-        expr_ref A(m), B(m), C(m), v(m);
+        expr_ref A(m), C(m);
-        expr_ref_vector As(m), Bs(m);
+        expr_ref_vector As(m);
         m_Bs.reset();
         //
         // nodes from leaves that are repeated 
@@ -307,8 +533,6 @@ namespace pdr {
         if (level == 0) {
             return;
         }
-        unsigned previous_level = level - 1;
-
         
         As.push_back(pt.get_propagation_formula(m_ctx.get_pred_transformers(), level));
         As.push_back(node.state());
@@ -316,48 +540,8 @@ namespace pdr {
         m_A = pm.mk_and(As);
 
         // Add quantifiers:
-        
+        // add_over_approximations(*qis, node);
-        {
+        add_under_approximations(*qis, node);
-            datalog::scoped_no_proof _no_proof(m);
-            quantifier_ref q(m);
-            scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
-            for (unsigned j = 0; j < qis->size(); ++j) {
-                q = (*qis)[j].get();
-                app_ref_vector& inst      = pt.get_inst(m_current_rule);
-                TRACE("pdr", 
-                      tout << "q:\n" << mk_pp(q, m) << "\n";
-                      tout << "level: " << level << "\n";
-                      model_smt2_pp(tout, m, node.get_model(), 0);
-                      m_current_rule->display(m_ctx.get_context(), tout << "rule:\n"); 
-                      
-                      );
-
-                var_subst vs(m, false);
-                vs(q, inst.size(), (expr*const*)inst.c_ptr(), B);
-                q = to_quantifier(B);
-                TRACE("pdr", tout << "q instantiated:\n" << mk_pp(q, m) << "\n";);
-
-                app* a = to_app(q->get_expr());
-                func_decl* f = a->get_decl();
-                pred_transformer& pt2 = m_ctx.get_pred_transformer(f);
-                B = pt2.get_formulas(previous_level, false);
-                TRACE("pdr", tout << "B:\n" << mk_pp(B, m) << "\n";);
-
-                
-                expr_substitution sub(m);  
-                for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                    v = m.mk_const(pm.o2n(pt2.sig(i),0));
-                    sub.insert(v, a->get_arg(i));
-                }
-                rep->set_substitution(&sub);
-                (*rep)(B);
-                TRACE("pdr", tout << "B substituted:\n" << mk_pp(B, m) << "\n";);
-                datalog::flatten_and(B, Bs);
-                for (unsigned i = 0; i < Bs.size(); ++i) {
-                    m_Bs.push_back(m.update_quantifier(q, Bs[i].get()));                    
-                }
-            }
-        }
 
         TRACE("pdr", 
               tout << "A:\n" << mk_pp(m_A, m) << "\n";
@@ -384,13 +568,17 @@ namespace pdr {
     bool quantifier_model_checker::model_check(model_node& root) {
         m_instantiations.reset();
         m_instantiated_rules.reset();
+        m_rules_model_check = true;
         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();
+        if (!m_rules_model_check) {
+            weaken_under_approximation();
+        }
+        return m_rules_model_check;
     }
 
     void quantifier_model_checker::refine() {
@@ -446,136 +634,3 @@ namespace pdr {
     }
 };
 
-
-#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

@@ -34,23 +34,26 @@ namespace pdr {
     class pred_transformer;
     class context;
         
-    
     class quantifier_model_checker {
         context&                      m_ctx;
         ast_manager&                  m;
         obj_map<datalog::rule const, quantifier_ref_vector*>& m_quantifiers;
         datalog::rule_set&            m_rules;
-        expr_ref_vector               m_trail;
+
+        obj_map<func_decl, expr*>     m_reachable; // set of reachable states
         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;
+        bool                            m_rules_model_check;
         app_ref_vector                  m_instantiations;
         ptr_vector<datalog::rule const> m_instantiated_rules;
 
         void model_check_node(model_node& node);
 
+        void weaken_under_approximation();
+
         bool find_instantiations(quantifier_ref_vector const& qs, unsigned level); 
 
         bool find_instantiations_model_based(quantifier_ref_vector const& qs, unsigned level);
@@ -79,6 +82,18 @@ namespace pdr {
         
         bool model_check(model_node& root);
 
+        void add_over_approximations(quantifier_ref_vector& qis, model_node& n);
+
+        void add_under_approximations(quantifier_ref_vector& qis, model_node& n);
+      
+        void add_approximations(quantifier_ref_vector& qis, model_node& n, bool is_over);
+
+        expr_ref get_reachable(func_decl* f);
+
+        void update_reachable(func_decl* f, expr* e);
+
+        expr_ref strongest_post_condition(datalog::rule& r);
+
     public:
         quantifier_model_checker(
             context& ctx, 
@@ -89,9 +104,14 @@ namespace pdr {
             m(m),
             m_quantifiers(quantifiers),
             m_rules(rules),
-            m_trail(m), m_A(m), m_Bs(m),             
+            m_A(m), 
-            m_current_pt(0), m_current_rule(0), 
+            m_Bs(m),             
-            m_current_node(0), m_instantiations(m) {}
+            m_current_pt(0), 
+            m_current_rule(0), 
+            m_current_node(0), 
+            m_instantiations(m) {}
+
+        ~quantifier_model_checker();
 
         bool check();
     };

src/muz_qe/qe_lite.cpp

@@ -74,7 +74,8 @@ public:
 };
 
 
-class der2 {
+namespace eq {
+    class der {
         ast_manager &   m;
         is_variable_proc* m_is_variable;
         var_subst       m_subst;
@@ -492,9 +493,8 @@ class der2 {
             return false;
         }
 
-
     public:
-    der2(ast_manager & m): m(m), m_is_variable(0), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m) {}
+        der(ast_manager & m): m(m), m_is_variable(0), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m) {}
         
         void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
         
@@ -530,6 +530,33 @@ public:
         
         ast_manager& get_manager() const { return m; }
     };
+}; // namespace eq
+
+// ------------------------------------------------------------
+// basic destructive equality (and disequality) resolution for arrays.
+
+namespace ar {
+    class der {
+        ast_manager&             m;
+        is_variable_proc*        m_is_variable;
+        
+        bool is_variable(expr * e) const {
+            return (*m_is_variable)(e);
+        }
+
+    public:
+
+        der(ast_manager& m): m(m), m_is_variable(0) {}
+
+        void operator()(expr_ref_vector& fmls) {
+            IF_VERBOSE(1, verbose_stream() << "Todo: eliminate arrays\n";);
+        }
+
+        void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
+        
+    };
+}; // namespace ar
+
 
 // ------------------------------------------------------------
 // fm_tactic adapted to eliminate designated de-Brujin indices.
@@ -1808,7 +1835,6 @@ namespace fm {
 
         void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
 
-
         void operator()(expr_ref_vector& fmls) {
             init(fmls);
             init_use_list(fmls);
@@ -1873,12 +1899,13 @@ namespace fm {
 
 class qe_lite::impl {
     ast_manager& m;
-    der2         m_der;
     params_ref   m_params;
+    eq::der      m_der;
     fm::fm       m_fm;
+    ar::der      m_array_der;
 
 public:
-    impl(ast_manager& m): m(m), m_der(m), m_fm(m, m_params) {}
+    impl(ast_manager& m): m(m), m_der(m), m_fm(m, m_params), m_array_der(m) {}
     
     void operator()(app_ref_vector& vars, expr_ref& fml) {
         if (vars.empty()) {
@@ -1928,10 +1955,16 @@ public:
     }
 
     void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
+        expr_ref_vector disjs(m);
+        datalog::flatten_or(fml, disjs);
+        for (unsigned i = 0; i < disjs.size(); ++i) {
             expr_ref_vector conjs(m);
-        conjs.push_back(fml);
+            conjs.push_back(disjs[i].get());
             (*this)(index_set, index_of_bound, conjs);
             bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), fml);
+            disjs[i] = fml;
+        }
+        bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), fml);
     }
 
 
@@ -1941,9 +1974,11 @@ public:
         TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";);
         IF_VERBOSE(3, for (unsigned i = 0; i < fmls.size(); ++i) verbose_stream() << mk_pp(fmls[i].get(), m) << "\n";);
         m_der.set_is_variable_proc(is_var);
-        m_der(fmls);
         m_fm.set_is_variable_proc(is_var);
+        m_array_der.set_is_variable_proc(is_var);
+        m_der(fmls);
         m_fm(fmls);
+        m_array_der(fmls);
         TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";);
     }
 

src/muz_qe/qe_lite.h

@@ -1,5 +1,5 @@
 /*++
-Copyright (c) 2010 Microsoft Corporation
+Copyright (c) 2012 Microsoft Corporation
 
 Module Name: