fix bug in proof generation for PDR, add more features for handling quantifiers

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

src/muz_qe/equiv_proof_converter.cpp

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    equiv_proof_converter.cpp
+
+Abstract:
+
+    Proof converter that applies equivalence rule to leaves.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-23
+
+Revision History:  
+
+--*/
+
+#include "equiv_proof_converter.h"
+#include "ast_pp.h"
+#include "dl_util.h"
+
+void equiv_proof_converter::insert(expr* fml1, expr* fml2) {
+    datalog::scoped_fine_proof _sp(m);
+    proof_ref p1(m), p2(m), p3(m);
+    p1 = m.mk_asserted(fml1);
+    p2 = m.mk_rewrite(fml1, fml2);
+    p3 = m.mk_modus_ponens(p1, p2);
+    TRACE("proof_converter", tout << mk_pp(p3.get(), m) << "\n";);
+    SASSERT(m.has_fact(p3));
+    m_replace.insert(p3);
+}

src/muz_qe/equiv_proof_converter.h

@@ -43,13 +43,7 @@ public:
         return m_replace.translate(translator);
     }
 
-    void insert(expr* fml1, expr* fml2) {
+    void insert(expr* fml1, expr* fml2);
-        proof_ref p1(m), p2(m), p3(m);
-        p1 = m.mk_asserted(fml1);
-        p2 = m.mk_rewrite(fml1, fml2);
-        p3 = m.mk_modus_ponens(p1, p2);
-        m_replace.insert(p3);
-    }
 
     ast_manager& get_manager() { return m; }
 

src/muz_qe/pdr_context.cpp

@@ -162,9 +162,6 @@ namespace pdr {
         }
     }
 
-    void pred_transformer::find_predecessors(model_core const& model, ptr_vector<func_decl>& preds) const {
-        find_predecessors(find_rule(model), preds);        
-    }
 
     void pred_transformer::remove_predecessors(expr_ref_vector& literals) {
         // remove tags
@@ -740,6 +737,44 @@ namespace pdr {
         return expr_ref(m.mk_app(f, args.size(), args.c_ptr()), m);
     }
 
+    static bool is_ini(datalog::rule const& r) {
+        return r.get_uninterpreted_tail_size() == 0;
+    }
+
+    datalog::rule* model_node::get_rule() {
+        if (m_rule) {
+            return const_cast<datalog::rule*>(m_rule);
+        }
+        // only initial states are not set by the PDR search.
+        datalog::rule const& rl1 = pt().find_rule(*m_model);
+        if (is_ini(rl1)) {
+            set_rule(&rl1);
+            return const_cast<datalog::rule*>(m_rule);
+        }
+        ast_manager& m = pt().get_manager();
+        // otherwise, the initial state is reachable.
+        ptr_vector<datalog::rule> const& rules = pt().rules();
+        ptr_vector<datalog::rule> ini_rules;
+        expr_ref_vector tags(m);
+        expr_ref ini_tags(m), ini_state(m);
+        for (unsigned i = 0; i < rules.size(); ++i) {
+            datalog::rule* rl = rules[i];
+            if (is_ini(*rl)) {
+                tags.push_back(pt().rule2tag(rl));
+            }
+        }
+        SASSERT(!tags.empty());
+        ini_tags = m.mk_or(tags.size(), tags.c_ptr());
+        ini_state = m.mk_and(ini_tags, pt().initial_state(), state());
+        model_ref mdl;
+        pt().get_solver().set_model(&mdl);
+        VERIFY(l_true == pt().get_solver().check_conjunction_as_assumptions(ini_state));
+        datalog::rule const& rl2 = pt().find_rule(*mdl);
+        SASSERT(is_ini(rl2));
+        set_rule(&rl2);
+        return const_cast<datalog::rule*>(m_rule);                        
+    }
+
 
     void model_node::mk_instantiate(datalog::rule_ref& r0, datalog::rule_ref& r1, expr_ref_vector& binding) {
         ast_manager& m = pt().get_manager();
@@ -763,7 +798,7 @@ namespace pdr {
                 model.insert(e, m.mk_true());
             }
         }
-        r0 = const_cast<datalog::rule*>(&pt().find_rule(*m_model.get()));
+        r0 = get_rule();
         app_ref_vector& inst = pt().get_inst(r0);
         TRACE("pdr", tout << mk_pp(state(), m) << " instance: " << inst.size() << "\n";);
         for (unsigned i = 0; i < inst.size(); ++i) {
@@ -1644,7 +1679,7 @@ namespace pdr {
             switch (expand_state(n, cube, uses_level)) {
             case l_true:
                 if (n.level() == 0) {
-                    TRACE("pdr", tout << "reachable\n";);
+                    TRACE("pdr", tout << "reachable at level 0\n";);
                     close_node(n);
                 }
                 else {
@@ -1772,6 +1807,8 @@ namespace pdr {
         expr* T   = pt.get_transition(r);
         expr* phi = n.state();
 
+        n.set_rule(&r);
+
         IF_VERBOSE(3, verbose_stream() << "Model:\n";
                    model_smt2_pp(verbose_stream(), m, *M, 0);
                    verbose_stream() << "\n";

src/muz_qe/pdr_context.h

@@ -132,7 +132,6 @@ namespace pdr {
         bool is_reachable(expr* state);
         void remove_predecessors(expr_ref_vector& literals);
         void find_predecessors(datalog::rule const& r, ptr_vector<func_decl>& predicates) const;
-        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); }
         ptr_vector<app>& get_aux_vars(datalog::rule const& r) { return m_rule2vars.find(&r); }
@@ -163,6 +162,8 @@ namespace pdr {
 
         void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars);
 
+        prop_solver& get_solver() { return m_solver; }
+
     };
 
 
@@ -177,10 +178,11 @@ namespace pdr {
         unsigned               m_orig_level;
         unsigned               m_depth;
         bool                   m_closed;
+        datalog::rule const*   m_rule;
     public:
         model_node(model_node* parent, expr_ref& state, pred_transformer& pt, unsigned level):
             m_parent(parent), m_pt(pt), m_state(state), m_model(0), 
-                m_level(level), m_orig_level(level), m_depth(0), m_closed(false) {
+                m_level(level), m_orig_level(level), m_depth(0), m_closed(false), m_rule(0) {
             if (m_parent) {
                 m_parent->m_children.push_back(this);
                 SASSERT(m_parent->m_level == level+1);
@@ -217,6 +219,9 @@ namespace pdr {
         void set_pre_closed() { m_closed = true; }
         void reset() { m_children.reset(); }
 
+        void set_rule(datalog::rule const* r) { m_rule = r; }
+        datalog::rule* get_rule();
+
         expr_ref get_trace() const;
         void mk_instantiate(datalog::rule_ref& r0, datalog::rule_ref& r1, expr_ref_vector& binding);
 

src/muz_qe/pdr_quantifiers.cpp

@@ -105,7 +105,11 @@ namespace pdr {
     }
 
 
-    void quantifier_model_checker::add_binding(quantifier* q, expr_ref_vector& binding) {          
+    void quantifier_model_checker::add_binding(quantifier* q, expr_ref_vector& binding) {      
+        if (binding.size() != q->get_num_decls()) {
+            // not a full binding. It may happen that the quantifier got simplified.
+            return;
+        }
         apply_binding(q, binding);
         vector<expr_ref_vector> bindings;
         generalize_binding(binding, bindings);
@@ -126,15 +130,18 @@ namespace pdr {
         inst.append(var_inst.size(), (expr*const*)var_inst.c_ptr());
         inst.reverse();
         expr_abstract(m, 0, inst.size(), inst.c_ptr(), e, e);
+        if (m_instantiations.contains(to_app(e))) {
+            return;
+        }
         m_instantiated_rules.push_back(m_current_rule);
         m_instantiations.push_back(to_app(e));
         TRACE("pdr", tout << mk_pp(q, m) << "\n";
-              tout << "binding\n";
+              tout << "binding: ";
               for (unsigned i = 0; i < binding.size(); ++i) {
                   tout << mk_pp(binding[i].get(), m) << " ";
               }
               tout << "\n";
-              tout << "inst\n";
+              tout << "inst: ";
               for (unsigned i = 0; i < var_inst.size(); ++i) {
                   tout << mk_pp(var_inst[i].get(), m) << " ";
               }
@@ -361,6 +368,7 @@ namespace pdr {
         scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
         for (unsigned j = 0; j < qis.size(); ++j) {
             q = qis[j].get();
+            SASSERT(is_forall(q));
             app_ref_vector& inst      = pt.get_inst(m_current_rule);
             TRACE("pdr", 
                   tout << "q:\n" << mk_pp(q, m) << "\n";
@@ -433,11 +441,16 @@ namespace pdr {
         unsigned t_size  = r.get_tail_size();   
         var_subst vs(m, false);
         sort_ref_vector vars(m);
+        uint_set empty_index_set;
+        qe_lite qe(m);
+
         r.get_vars(vars);
+#if 1
         if (qis) {
             quantifier_ref_vector const& qi = *qis;
             for (unsigned i = 0; i < qi.size(); ++i) {
-                fml = qi[i]->get_expr();
+                quantifier* q = qi[i];
+                fml = q->get_expr();
                 a = to_app(fml);
                 p = a->get_decl();
                 expr* p_reach = get_reachable(p);
@@ -448,9 +461,17 @@ namespace pdr {
                     sub.insert(v, a->get_arg(j));
                 }
                 sub(p_reach, fml);
-                body.push_back(m.update_quantifier(qi[i], fml));
+                uint_set is;
+                for (unsigned j = 0; j < q->get_num_decls(); ++j) {
+                    is.insert(j);
+                }
+                fml = m.mk_not(fml);
+                qe(is, true, fml);
+                fml = m.mk_not(fml);
+                body.push_back(m.update_quantifier(q, fml));
             }
         }
+#endif
         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)));
@@ -489,8 +510,6 @@ namespace pdr {
         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));
@@ -498,7 +517,7 @@ namespace pdr {
         }
         SASSERT(is_well_sorted(m, fml));
         
-        IF_VERBOSE(0, verbose_stream() << "instantiate to\n:" << mk_pp(fml, m) << "\n";);
+        IF_VERBOSE(0, verbose_stream() << "instantiate to:\n" << mk_pp(fml, m) << "\n";);
         return fml;
     }
 

src/muz_qe/pdr_util.cpp

@@ -386,13 +386,12 @@ namespace pdr {
             for_each_expr(*this, m_visited, tocollect[i]);
         }
         unsigned sz = m_model->get_num_constants();
-        expr_ref e(m), eq(m);
+        expr_ref e(m), eq(m), val(m);
         expr_ref_vector model(m);
         for (unsigned i = 0; i < sz; i++) {
-            func_decl * d = m_model->get_constant(i); 
+            e = m.mk_const(m_model->get_constant(i));
-            expr* val = m_model->get_const_interp(d);
-            e = m.mk_const(d);
             if (m_visited.is_marked(e)) {
+                val = eval(m_model, e);
                 eq = m.mk_eq(e, val);
                 model.push_back(eq);
             }
@@ -923,6 +922,20 @@ namespace pdr {
         return !has_x;
     }
 
+    expr_ref model_evaluator::eval(model_ref& model, func_decl* d) {
+        SASSERT(d->get_arity() == 0);
+        expr_ref result(m);
+        if (m_array.is_array(d->get_range())) {
+            expr_ref e(m);
+            e = m.mk_const(d);
+            result = eval(model, e);
+        }
+        else {
+            result = model->get_const_interp(d);
+        }
+        return result;
+    }
+
     expr_ref model_evaluator::eval(model_ref& model, expr* e) {
         expr_ref result(m);
         m_model = model;

src/muz_qe/pdr_util.h

@@ -129,6 +129,8 @@ namespace pdr {
        void operator()(expr* e) {} 
 
        expr_ref eval(model_ref& mdl, expr* e);
+
+       expr_ref eval(model_ref& mdl, func_decl* d);
     };
 
     /**

src/muz_qe/qe_lite.cpp

@@ -33,6 +33,8 @@ Revision History:
 #include "dl_util.h"
 #include "th_rewriter.h"
 #include "dl_util.h"
+#include "for_each_expr.h"
+#include "expr_safe_replace.h"
 
 
 class is_variable_proc {
@@ -77,9 +79,10 @@ public:
 namespace eq {
     class der {
         ast_manager &   m;
+        arith_util      a;
         is_variable_proc* m_is_variable;
         var_subst       m_subst;
-        expr_ref_buffer m_new_exprs;
+        expr_ref_vector m_new_exprs;
         
         ptr_vector<expr> m_map;
         int_vector       m_pos2var;
@@ -225,7 +228,81 @@ namespace eq {
                 return false;
             }
         }
+
+        bool solve_arith_core(app * lhs, expr * rhs, expr * eq, var* & var, expr_ref & def) {
+            SASSERT(a.is_add(lhs));
+            bool is_int  = a.is_int(lhs);
+            expr * a1; 
+            expr * v;
+            rational a_val;
+            unsigned num = lhs->get_num_args();
+            unsigned i;
+            for (i = 0; i < num; i++) {
+                expr * arg = lhs->get_arg(i);
+                if (is_variable(arg)) {
+                    a_val = rational(1); 
+                    v     = arg;
+                    break;
+                }
+                else if (a.is_mul(arg, a1, v) && 
+                         is_variable(v) && 
+                         a.is_numeral(a1, a_val) &&
+                         !a_val.is_zero() &&
+                         (!is_int || a_val.is_minus_one())) {
+                    break;
+                }
+            }
+            if (i == num)
+                return false;
+            var = to_var(v);
+            expr_ref inv_a(m);
+            if (!a_val.is_one()) {
+                inv_a = a.mk_numeral(rational(1)/a_val, is_int);
+                rhs   = a.mk_mul(inv_a, rhs);
+            }
+            
+            ptr_buffer<expr> other_args;
+            for (unsigned j = 0; j < num; j++) {
+                if (i != j) {
+                    if (inv_a)
+                        other_args.push_back(a.mk_mul(inv_a, lhs->get_arg(j)));
+                    else
+                        other_args.push_back(lhs->get_arg(j));
+                }
+            }
+            switch (other_args.size()) {
+            case 0:
+                def = rhs;
+                break;
+            case 1:
+                def = a.mk_sub(rhs, other_args[0]);
+                break;
+            default:
+                def = a.mk_sub(rhs, a.mk_add(other_args.size(), other_args.c_ptr()));
+                break;
+            }
+            m_new_exprs.push_back(def);
+            return true;
+        }
         
+        bool arith_solve(expr * lhs, expr * rhs, expr * eq, var* & var, expr_ref & t) {
+            return 
+                (a.is_add(lhs) && solve_arith_core(to_app(lhs), rhs, eq, var, t)) ||
+                (a.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, var, t));
+        }
+
+        bool trival_solve(expr* lhs, expr* rhs, expr* eq, var* & v, expr_ref& t) {
+            if (!is_variable(lhs)) {
+                std::swap(lhs, rhs);
+            }
+            if (!is_variable(lhs)) {
+                return false;
+            }
+            v = to_var(lhs);
+            t = rhs;
+            TRACE("der", tout << mk_pp(eq, m) << "\n";);
+            return true;
+        }
         
 
         /**
@@ -251,14 +328,13 @@ namespace eq {
                     TRACE("der", tout << mk_pp(e, m) << "\n";);
                     return true;
                 }
-                if (!is_variable(lhs))
+                if (trival_solve(lhs, rhs, e, v, t)) {
-                    std::swap(lhs, rhs);
+                    return true;
-                if (!is_variable(lhs))
+                }
-                    return false;
+                if (arith_solve(lhs, rhs, e, v, t)) {
-                v = to_var(lhs);
+                    return true;
-                t = rhs;
+                }
-                TRACE("der", tout << mk_pp(e, m) << "\n";);
+                return false;
-                return true;
             }
             
             // (ite cond (= VAR t) (= VAR t2)) case
@@ -494,7 +570,7 @@ namespace eq {
         }
 
     public:
-        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) {}
+        der(ast_manager & m): m(m), a(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;}
         
@@ -538,20 +614,129 @@ namespace eq {
 namespace ar {
     class der {
         ast_manager&             m;
+        array_util               a;
         is_variable_proc*        m_is_variable;
+        ptr_vector<expr>         m_todo;
+        expr_mark                m_visited;
         
         bool is_variable(expr * e) const {
             return (*m_is_variable)(e);
         }
 
+        void mark_all(expr* e) {
+            for_each_expr(*this, m_visited, e);
+        }
+
+        void mark_all(expr_ref_vector const& fmls, unsigned j) {
+            for (unsigned i = 0; i < fmls.size(); ++i) {
+                if (i != j) {
+                    mark_all(fmls[i]);
+                }
+            }
+        }
+
+        /**
+           Ex A. A[x] = t & Phi where x \not\in A, t. 
+           =>
+           Ex A. Phi[store(A,x,t)]
+         */
+
+        bool solve_select(expr_ref_vector& conjs, unsigned i, expr* e1, expr* e2) {
+            if (a.is_select(e1)) {
+                app* a1 = to_app(e1);
+                expr* A = a1->get_arg(0);
+                if (!is_variable(A)) {
+                    return false;
+                }
+                m_visited.reset();
+                for (unsigned j = 1; j < a1->get_num_args(); ++j) {
+                    mark_all(a1->get_arg(j));
+                }
+                mark_all(e2);
+                if (m_visited.is_marked(A)) {
+                    return false;
+                }
+                ptr_vector<expr> args;
+                args.push_back(A);
+                args.append(a1->get_num_args()-1, a1->get_args()+1);
+                args.push_back(e2);
+                expr* B = a.mk_store(args.size(), args.c_ptr());
+                expr_safe_replace rep(m);
+                rep.insert(A, B);
+                expr_ref tmp(m);
+                for (unsigned j = 0; j < conjs.size(); ++j) {
+                    if (i == j) {
+                        conjs[j] = m.mk_true();
+                    }
+                    else {
+                        rep(conjs[j].get(), tmp);
+                        conjs[j] = tmp;
+                    }
+                }
+                return true;
+            }
+            return false;
+        }
+
+        bool solve_select(expr_ref_vector& conjs, unsigned i, expr* e) {
+            expr* e1, *e2;
+            return 
+                m.is_eq(e, e1, e2) &&
+                (solve_select(conjs, i, e1, e2) ||
+                 solve_select(conjs, i, e2, e1));
+        }
+
+        /**
+           Ex x. A[x] != B[x] & Phi where x \not\in A, B, Phi
+           =>
+           A != B & Phi
+         */
+        bool solve_neq_select(expr_ref_vector& conjs, unsigned i, expr* e) {
+            expr* e1, *a1, *a2;
+            if (m.is_not(e, e1) && m.is_eq(e1, a1, a2)) {
+                if (a.is_select(a1) && 
+                    a.is_select(a2) && 
+                    to_app(a1)->get_num_args() == to_app(a2)->get_num_args()) {
+                    expr* e1 = to_app(a1)->get_arg(0);
+                    expr* e2 = to_app(a2)->get_arg(0);
+                    m_visited.reset();
+                    mark_all(conjs, i);
+                    mark_all(e1);
+                    mark_all(e2);
+                    for (unsigned j = 1; j < to_app(a1)->get_num_args(); ++j) {
+                        expr* x = to_app(a1)->get_arg(j);
+                        expr* y = to_app(a2)->get_arg(j);
+                        if (!is_variable(x)) {
+                            return false;
+                        }
+                        if (x != y) {
+                            return false;
+                        }
+                        if (m_visited.is_marked(x)) {
+                            return false;
+                        }
+                    }
+                    conjs[i] = m.mk_not(m.mk_eq(e1, e2));
+                    return true;
+                }
+            }
+            return false;
+        }
+
+
     public:
 
-        der(ast_manager& m): m(m), m_is_variable(0) {}
+        der(ast_manager& m): m(m), a(m), m_is_variable(0) {}
 
         void operator()(expr_ref_vector& fmls) {
-            IF_VERBOSE(1, verbose_stream() << "Todo: eliminate arrays\n";);
+            for (unsigned i = 0; i < fmls.size(); ++i) {
+                solve_select(fmls, i, fmls[i].get());
+                solve_neq_select(fmls, i, fmls[i].get());
+            }
         }
 
+        void operator()(expr* e) {}
+
         void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
         
     };
@@ -1904,6 +2089,22 @@ class qe_lite::impl {
     fm::fm       m_fm;
     ar::der      m_array_der;
 
+    bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) {
+        index = fmls.size();
+        if (index <= 1) {
+            return false;
+        }
+        for (unsigned i = 0; i < fmls.size(); ++i) {
+            if (!is_ground(fmls[i])) {
+                if (index != fmls.size()) {
+                    return false;
+                }
+                index = i;
+            }
+        }
+        return index < fmls.size();
+    }
+
 public:
     impl(ast_manager& m): m(m), m_der(m), m_fm(m, m_params), m_array_der(m) {}
     
@@ -1970,9 +2171,21 @@ public:
 
     void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& fmls) {
         datalog::flatten_and(fmls);
+        unsigned index;
+        if (has_unique_non_ground(fmls, index)) {
+            expr_ref fml(m);
+            fml = fmls[index].get();
+            (*this)(index_set, index_of_bound, fml);
+            fmls[index] = fml;
+            return;
+        }
+        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";
+            });
         is_variable_test is_var(index_set, index_of_bound);
-        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_fm.set_is_variable_proc(is_var);
         m_array_der.set_is_variable_proc(is_var);