preparing handling of arrays/quantifiers, fix cover-related bugs reported by Arie

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

src/ast/array_decl_plugin.h

@@ -144,7 +144,21 @@ public:
     bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); }
     bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
     bool is_as_array_tree(expr * n);
+    bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); }
+    bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); }
+    bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
+    bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); }
+    bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
     func_decl * get_as_array_func_decl(app * n) const { SASSERT(is_as_array(n)); return to_func_decl(n->get_decl()->get_parameter(0).get_ast()); }
+
+    app * mk_store(unsigned num_args, expr * const * args) {
+        return m_manager.mk_app(m_fid, OP_STORE, 0, 0, num_args, args);
+    }
+
+    app * mk_select(unsigned num_args, expr * const * args) {
+        return m_manager.mk_app(m_fid, OP_SELECT, 0, 0, num_args, args);
+    }
+
     app * mk_map(func_decl * f, unsigned num_args, expr * const * args) {
         parameter p(f);
         return m_manager.mk_app(m_fid, OP_ARRAY_MAP, 1, &p, num_args, args);

src/ast/dl_decl_plugin.cpp

@@ -44,8 +44,7 @@ namespace datalog {
         m_num_sym("N"),
         m_lt_sym("<"),
         m_le_sym("<="),
-        m_rule_sym("R"),
+        m_rule_sym("R")
-        m_hyper_resolve_sym("hyper-res")
     {
     }
 

src/ast/dl_decl_plugin.h

@@ -69,7 +69,6 @@ namespace datalog {
         symbol m_lt_sym;
         symbol m_le_sym;
         symbol m_rule_sym;
-        symbol m_hyper_resolve_sym;
 
         bool check_bounds(char const* msg, unsigned low, unsigned up, unsigned val) const;
         bool check_domain(unsigned low, unsigned up, unsigned val) const;
@@ -93,7 +92,6 @@ namespace datalog {
         func_decl * mk_compare(decl_kind k, symbol const& sym, sort*const* domain);
         func_decl * mk_clone(sort* r);
         func_decl * mk_rule(unsigned arity);
-        func_decl * mk_hyper_res(unsigned num_params, parameter const* params, unsigned arity, sort *const* domain);
                                 
         sort * mk_finite_sort(unsigned num_params, parameter const* params);
         sort * mk_relation_sort(unsigned num_params, parameter const* params);

src/muz_qe/dl_context.cpp

@@ -54,6 +54,7 @@ Revision History:
 #include"expr_functors.h"
 #include"dl_mk_partial_equiv.h"
 #include"dl_mk_bit_blast.h"
+#include"dl_mk_array_blast.h"
 #include"datatype_decl_plugin.h"
 #include"expr_abstract.h"
 
@@ -944,6 +945,7 @@ namespace datalog {
         transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34880));
 
         transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000));
+        transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000));
         transform_rules(transf, mc, pc);
     }
 

src/muz_qe/dl_mk_array_blast.cpp

@@ -0,0 +1,139 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_array_blast.cpp
+
+Abstract:
+
+    Remove array variables from rules.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-23
+
+Revision History:
+
+--*/
+
+#include "dl_mk_array_blast.h"
+#include "expr_replacer.h"
+
+namespace datalog {
+
+
+    mk_array_blast::mk_array_blast(context & ctx, unsigned priority) : 
+        rule_transformer::plugin(priority, false),
+        m_ctx(ctx),
+        m(ctx.get_manager()), 
+        a(m),
+        rm(ctx.get_rule_manager()),
+        m_rewriter(m, m_params){
+        m_params.set_bool(":expand-select-store",true);
+        m_rewriter.updt_params(m_params);
+    }
+
+    mk_array_blast::~mk_array_blast() {
+    }
+
+    bool mk_array_blast::is_store_def(expr* e, expr*& x, expr*& y) {
+        if (m.is_iff(e, x, y) || m.is_eq(e, x, y)) {
+            if (!a.is_store(y)) {
+                std::swap(x,y);
+            }
+            if (is_var(x) && a.is_store(y)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    bool mk_array_blast::blast(rule& r, rule_set& rules) {
+        unsigned utsz = r.get_uninterpreted_tail_size();
+        unsigned tsz = r.get_tail_size();
+        expr_ref_vector conjs(m), new_conjs(m);
+        for (unsigned i = 0; i < utsz; ++i) {
+            new_conjs.push_back(r.get_tail(i));
+        }
+        for (unsigned i = utsz; i < tsz; ++i) {
+            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;
+            if (is_store_def(conjs[i].get(), x, y)) {
+                // enforce topological order consistency:
+                uint_set lhs;
+                collect_vars(m, x, lhs_vars);
+                collect_vars(m, y, rhs_vars);
+                lhs = lhs_vars;
+                lhs &= rhs_vars;
+                if (!lhs.empty()) {
+                    new_conjs.push_back(conjs[i].get());
+                }
+                else {
+                    sub.insert(x, y);
+                }
+            }
+            else {
+                new_conjs.push_back(conjs[i].get());
+            }
+        }
+        if (sub.empty()) {
+            rules.add_rule(&r);
+            return false;
+        }
+        
+        rule_ref_vector new_rules(rm);
+        expr_ref fml1(m), fml2(m), body(m), head(m);
+        r.to_formula(fml1);
+        body = m.mk_and(new_conjs.size(), new_conjs.c_ptr());
+        head = r.get_head();
+        scoped_ptr<expr_replacer> replace = mk_default_expr_replacer(m);
+        replace->set_substitution(&sub);
+        (*replace)(body);
+        m_rewriter(body);
+        (*replace)(head);
+        m_rewriter(head);
+        fml2 = m.mk_implies(body, head);
+        rm.mk_rule(fml2, new_rules, r.name());
+        SASSERT(new_rules.size() == 1);
+        
+        rules.add_rule(new_rules[0].get());
+        if (m_pc) {
+            new_rules[0]->to_formula(fml2);
+            m_pc->insert(fml1, fml2);
+        }
+        return true;
+    }
+    
+    rule_set * mk_array_blast::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
+        ref<equiv_proof_converter> epc;
+        if (pc) {
+            epc = alloc(equiv_proof_converter, m);
+        }
+        m_pc = epc.get();
+
+        rule_set* rules = alloc(rule_set, m_ctx);
+        rule_set::iterator it = source.begin(), end = source.end();
+        bool change = false;
+        for (; it != end; ++it) {
+            change = blast(**it, *rules) || change;
+        }
+        if (!change) {
+            dealloc(rules);
+            rules = 0;
+        }        
+        if (pc) {
+            pc = concat(pc.get(), epc.get());
+        }
+        return rules;        
+
+    }
+
+};
+
+

src/muz_qe/dl_mk_array_blast.h

@@ -0,0 +1,61 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_array_blast.h
+
+Abstract:
+
+    Remove array variables from rules.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-23
+
+Revision History:
+
+--*/
+#ifndef _DL_MK_ARRAY_BLAST_H_
+#define _DL_MK_ARRAY_BLAST_H_
+
+#include"dl_context.h"
+#include"dl_rule_set.h"
+#include"dl_rule_transformer.h"
+#include "equiv_proof_converter.h"
+#include "array_decl_plugin.h"
+
+namespace datalog {
+
+    /**
+       \brief Blast occurrences of arrays in rules
+    */
+    class mk_array_blast : public rule_transformer::plugin {
+        context&        m_ctx;
+        ast_manager&    m;
+        array_util      a;
+        rule_manager&   rm;
+        params_ref      m_params;
+        th_rewriter     m_rewriter;
+        equiv_proof_converter* m_pc;
+
+        bool blast(rule& r, rule_set& new_rules);
+
+        bool is_store_def(expr* e, expr*& x, expr*& y);
+
+    public:
+        /**
+           \brief Create rule transformer that extracts universal quantifiers (over recursive predicates).
+        */
+        mk_array_blast(context & ctx, unsigned priority);
+
+        virtual ~mk_array_blast();
+        
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+
+    };
+
+};
+
+#endif /* _DL_MK_ARRAY_BLAST_H_ */
+

src/muz_qe/dl_mk_extract_quantifiers.cpp

@@ -40,29 +40,32 @@ namespace datalog {
 
 
     void mk_extract_quantifiers::extract(rule& r, rule_set& new_rules) {
-        app_ref_vector tail(m);
+        expr_ref_vector tail(m);
-        svector<bool>  neg_tail;
         quantifier_ref_vector quantifiers(m);
         unsigned utsz = r.get_uninterpreted_tail_size();
         unsigned tsz = r.get_tail_size();
         for (unsigned i = 0; i < utsz; ++i) {
             tail.push_back(r.get_tail(i));
-            neg_tail.push_back(r.is_neg_tail(i));
+            if (r.is_neg_tail(i)) {
+                new_rules.add_rule(&r);
+                return;
+            }
         }
         for (unsigned i = utsz; i < tsz; ++i) {
-            SASSERT(!r.is_neg_tail(i));
             app* t = r.get_tail(i);
             expr_ref_vector conjs(m);
             datalog::flatten_and(t, conjs);
+            quantifier_ref qe(m);
+            quantifier* q = 0;
             for (unsigned j = 0; j < conjs.size(); ++j) {
                 expr* e = conjs[j].get();
-                quantifier* q = 0;
                 if (rule_manager::is_forall(m, e, q)) {
                     quantifiers.push_back(q);
+                    qe = m.mk_exists(q->get_num_decls(), q->get_decl_sorts(), q->get_decl_names(), q->get_expr());
+                    tail.push_back(qe);
                 }
                 else {
-                    tail.push_back(is_app(e)?to_app(e):m.mk_eq(e, m.mk_true()));
+                    tail.push_back(e);
-                    neg_tail.push_back(false);
                 }
             }
         }
@@ -70,11 +73,16 @@ namespace datalog {
             new_rules.add_rule(&r);
         }
         else {
-            rule* new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), neg_tail.c_ptr(), r.name(), false);
+            expr_ref fml(m);
-            new_rules.add_rule(new_rule);
+            rule_ref_vector rules(rm);
+            fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), r.get_head());
+            rm.mk_rule(fml, rules, r.name());
             quantifier_ref_vector* qs = alloc(quantifier_ref_vector, quantifiers);
-            m_quantifiers.insert(new_rule, qs);
             m_refs.push_back(qs);
+            for (unsigned i = 0; i < rules.size(); ++i) {
+                m_quantifiers.insert(rules[i].get(), qs);
+                new_rules.add_rule(rules[i].get());
+            }
         }
     }
     

src/muz_qe/dl_util.h

@@ -196,6 +196,12 @@ namespace datalog {
         scoped_no_proof(ast_manager& m): scoped_proof_mode(m, PGM_DISABLED) {}
     };
 
+    class scoped_restore_proof : public scoped_proof_mode {
+    public:
+        scoped_restore_proof(ast_manager& m): scoped_proof_mode(m, m.proof_mode()) {}
+    };
+
+
     
 
     class variable_intersection

src/muz_qe/equiv_proof_converter.h

@@ -0,0 +1,58 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    equiv_proof_converter.h
+
+Abstract:
+
+    Proof converter that applies equivalence rule to leaves.
+
+    Given a proof P with occurrences of [asserted fml] 
+    replace [asserted fml] by a proof of the form
+    [mp [asserted fml'] [~ fml fml']]
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-23
+
+Revision History:  
+
+--*/
+
+#ifndef _EQUIV_PROOF_CONVERTER_H_
+#define _EQUIV_PROOF_CONVERTER_H_
+
+#include "replace_proof_converter.h"
+
+class equiv_proof_converter : public proof_converter {
+    ast_manager&            m;
+    replace_proof_converter m_replace;
+public:
+
+    equiv_proof_converter(ast_manager& m): m(m), m_replace(m) {}
+
+    virtual ~equiv_proof_converter() {}
+
+    virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) {
+        m_replace(m, num_source, source, result);
+    }
+
+    virtual proof_converter * translate(ast_translation & translator) {
+        return m_replace.translate(translator);
+    }
+
+    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; }
+
+};
+
+#endif

src/muz_qe/pdr_context.cpp

@@ -35,7 +35,6 @@ Notes:
 #include "pdr_generalizers.h"
 #include "datatype_decl_plugin.h"
 #include "for_each_expr.h"
-#include "model_v2_pp.h"
 #include "dl_rule_set.h"
 #include "unit_subsumption_tactic.h"
 #include "model_smt2_pp.h"
@@ -146,7 +145,6 @@ namespace pdr {
         expr_ref vl(m);
         for (; it != end; ++it) {
             expr* pred = it->m_key;
-            TRACE("pdr", tout << mk_pp(pred, m) << "\n";);
             if (model.eval(to_app(pred)->get_decl(), vl) && m.is_true(vl)) {
                 return *it->m_value;
             }
@@ -362,7 +360,7 @@ namespace pdr {
         }
         // replace local constants by bound variables.
         expr_substitution sub(m);        
-        for (unsigned i = 0; i < m_sig.size(); ++i) {
+        for (unsigned i = 0; i < sig_size(); ++i) {
             c = m.mk_const(pm.o2n(sig(i), 0));
             v = m.mk_var(i, sig(i)->get_range());
             sub.insert(c, v);
@@ -397,7 +395,7 @@ namespace pdr {
         // replace bound variables by local constants.
         expr_ref result(property, m), v(m), c(m);
         expr_substitution sub(m);        
-        for (unsigned i = 0; i < m_sig.size(); ++i) {
+        for (unsigned i = 0; i < sig_size(); ++i) {
             c = m.mk_const(pm.o2n(sig(i), 0));
             v = m.mk_var(i, sig(i)->get_range());
             sub.insert(v, c);
@@ -602,6 +600,12 @@ namespace pdr {
         }
         m_rule2inst.insert(&rule,&var_reprs);
         m_rule2vars.insert(&rule, aux_vars);
+        TRACE("pdr", 
+              tout << rule.get_decl()->get_name() << "\n";
+              for (unsigned i = 0; i < var_reprs.size(); ++i) {
+                  tout << mk_pp(var_reprs[i].get(), m) << " ";
+              }
+              tout << "\n";);
     }
 
     bool pred_transformer::check_filled(app_ref_vector const& v) const {
@@ -723,7 +727,7 @@ namespace pdr {
         pred_transformer& p = pt();
         ast_manager& m = p.get_manager();
         manager& pm = p.get_pdr_manager();
-        TRACE("pdr", model_v2_pp(tout, get_model()););
+        TRACE("pdr", model_smt2_pp(tout, m, get_model(), 0););
         func_decl* f = p.head();
         unsigned arity = f->get_arity();
         expr_ref_vector args(m);

src/muz_qe/pdr_context.h

@@ -116,6 +116,7 @@ namespace pdr {
         ptr_vector<datalog::rule> const& rules() const { return m_rules; }
         func_decl* sig(unsigned i) { init_sig(); return m_sig[i].get(); } // signature 
         func_decl* const* sig() { init_sig(); return m_sig.c_ptr(); }
+        unsigned  sig_size() { init_sig(); return m_sig.size(); }
         expr*  transition() const { return m_transition; }
         expr*  initial_state() const { return m_initial_state; }
         expr*  rule2tag(datalog::rule const* r) { return m_rule2tag.find(r); }

src/muz_qe/pdr_dl_interface.cpp

@@ -59,17 +59,17 @@ dl_interface::~dl_interface() {
 void dl_interface::check_reset() {
     datalog::rule_ref_vector const& new_rules = m_ctx.get_rules().get_rules();
     datalog::rule_ref_vector const& old_rules = m_old_rules.get_rules();  
-    for (unsigned i = 0; i < new_rules.size(); ++i) {
+    bool is_subsumed = !old_rules.empty();
-        bool found = false;
+    for (unsigned i = 0; is_subsumed && i < new_rules.size(); ++i) {
-        for (unsigned j = 0; !found && j < old_rules.size(); ++j) {
+        is_subsumed = false;
+        for (unsigned j = 0; !is_subsumed && j < old_rules.size(); ++j) {
             if (m_ctx.check_subsumes(*old_rules[j], *new_rules[i])) {
-                found = true;
+                is_subsumed = true;
             }
         }
-        if (!found) {
+        if (!is_subsumed) {
-            CTRACE("pdr", (old_rules.size() > 0), new_rules[i]->display(m_ctx, tout << "Fresh rule "););
+            TRACE("pdr", new_rules[i]->display(m_ctx, tout << "Fresh rule "););
             m_context->reset();
-            break;
         }
     }
     m_old_rules.reset();
@@ -161,6 +161,8 @@ lbool dl_interface::query(expr * query) {
 
     quantifier_model_checker quantifier_mc(*m_context, m, extract_quantifiers->quantifiers(), m_pdr_rules);
     
+    datalog::scoped_restore_proof _sc(m); // update_rules may overwrite the proof mode.
+
     m_context->set_proof_converter(pc);
     m_context->set_model_converter(mc);
     m_context->set_query(query_pred);

src/muz_qe/pdr_quantifiers.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include "qe.h"
 #include "var_subst.h"
 #include "dl_rule_set.h"
+#include "model_smt2_pp.h"
 
 
 namespace pdr {
@@ -181,25 +182,21 @@ namespace pdr {
         bool found_instance = false;
         TRACE("pdr", tout << mk_pp(m_A,m) << "\n";);
  
-        ast_manager mp(PGM_COARSE);        
+        datalog::scoped_coarse_proof _scp(m);
-        ast_translation tr(m, mp);
+
-        ast_translation rev_tr(mp, m);
+        expr_ref_vector fmls(m);
-        expr_ref_vector fmls(mp);
         front_end_params fparams;
         fparams.m_proof_mode = PGM_COARSE;
         // TBD: does not work on integers: fparams.m_mbqi = true;
-        expr_ref C(m);
+
-        fmls.push_back(tr(m_A.get()));
+        fmls.push_back(m_A.get());
-        for (unsigned i = 0; i < m_Bs.size(); ++i) {
+        fmls.append(m_Bs);
-            C = m.update_quantifier(qs[i], m_Bs[i].get());
-            fmls.push_back(tr(C.get()));
-        }        
         TRACE("pdr",
               tout << "assert\n";
               for (unsigned i = 0; i < fmls.size(); ++i) {
-                  tout << mk_pp(fmls[i].get(), mp) << "\n";
+                  tout << mk_pp(fmls[i].get(), m) << "\n";
               });
-        smt::kernel solver(mp, fparams);
+        smt::kernel solver(m, fparams);
         for (unsigned i = 0; i < fmls.size(); ++i) {
             solver.assert_expr(fmls[i].get());
         }
@@ -216,8 +213,8 @@ namespace pdr {
         }
 
         proof* p = solver.get_proof();
-        TRACE("pdr", tout << mk_ismt2_pp(p, mp) << "\n";);
+        TRACE("pdr", tout << mk_ismt2_pp(p, m) << "\n";);
-        collect_insts collector(mp);
+        collect_insts collector(m);
         for_each_expr(collector, p);
         ptr_vector<quantifier> const& quants = collector.quantifiers();
 
@@ -225,20 +222,20 @@ namespace pdr {
             symbol qid = quants[i]->get_qid();
             if (!qid_map.find(qid, q)) {
                 TRACE("pdr", tout << "Could not find quantifier " 
-                      << mk_pp(quants[i], mp) << "\n";);
+                      << mk_pp(quants[i], m) << "\n";);
                 continue;
             }
             expr_ref_vector const& binding = collector.bindings()[i];
 
-            TRACE("pdr", tout << "Instantiating:\n" << mk_pp(quants[i], mp) << "\n";
+            TRACE("pdr", tout << "Instantiating:\n" << mk_pp(quants[i], m) << "\n";
                   for (unsigned j = 0; j < binding.size(); ++j) {
-                      tout << mk_pp(binding[j], mp) << " ";
+                      tout << mk_pp(binding[j], m) << " ";
                   }
                   tout << "\n";);
 
             expr_ref_vector new_binding(m);
             for (unsigned j = 0; j < binding.size(); ++j) {
-                new_binding.push_back(rev_tr(binding[j]));
+                new_binding.push_back(binding[j]);
             }
             add_binding(q, new_binding);
             found_instance = true;
@@ -258,11 +255,32 @@ namespace pdr {
         return found_instance;
     }
 
+    /**
+       Given node:
+
+         - pt - predicate transformer for rule:
+                P(x) :- Body1(x,y) || Body2(x,z) & (Fa u . Q(u,x,z)).
+         - rule - P(x) :- Body2(x,z)
+
+         - qis - Fa u . Q(u,x,z)
+
+         - 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::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);
+        expr_ref A(m), B(m), C(m), v(m);
         expr_ref_vector As(m);
         m_Bs.reset();
         //
@@ -285,7 +303,11 @@ namespace pdr {
             return;
         }
         unsigned level = node.level();
-        unsigned previous_level = (level == 0)?0:(level-1);
+        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());
@@ -296,28 +318,42 @@ namespace pdr {
         
         {
             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) {
-                quantifier* q = (*qis)[j].get();
+                q = (*qis)[j].get();
+                app_ref_vector& inst      = pt.get_inst(m_current_rule);
+                ptr_vector<app>& aux_vars = pt.get_aux_vars(*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, true);
+                TRACE("pdr", tout << "B:\n" << mk_pp(B, m) << "\n";);
+
                 
                 expr_substitution sub(m);  
-                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));
+                    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);
+                TRACE("pdr", tout << "B substituted:\n" << mk_pp(B, m) << "\n";);
-                ptr_vector<app>& aux_vars = pt.get_aux_vars(*m_current_rule);
+                
-                pt.ground_free_vars(B, inst, aux_vars);
+                B = m.update_quantifier(q, B);
-                var_subst vs(m, false);
-                vs(B, inst.size(), (expr*const*)inst.c_ptr(), B);
                 m_Bs.push_back(B);
             }
         }

src/muz_qe/pdr_util.cpp

@@ -86,13 +86,57 @@ namespace pdr {
         return res.str();
     }
 
+    /////////////////////////
+    // select elimination rewriter
+    //
 
-/////////////////////////
+    class select_elim {
-// model_evaluator
+        ast_manager& m;
-//
+        array_util   a;
+        model_ref    m_model;
+    public:
+        select_elim(ast_manager& m, model_ref& md): m(m), a(m), m_model(md) {}
+        
+        br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
+            if (a.is_select(f)) {
+                expr_ref tmp(m);
+                tmp = m.mk_app(f, num_args, args);
+                m_model->eval(tmp, result);
+                return BR_DONE;
+            }
+            else {
+                return BR_FAILED;
+            }
+        }
+    };
+
+    struct select_elim_cfg: public default_rewriter_cfg {
+        select_elim m_r;
+        bool rewrite_patterns() const { return false; }
+        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+            return m_r.mk_app_core(f, num, args, result);
+        }
+        select_elim_cfg(ast_manager & m, model_ref& md, params_ref const & p):m_r(m, md) {}        
+    };
+
+    template class rewriter_tpl<select_elim_cfg>;
+
+    class select_elim_star : public rewriter_tpl<select_elim_cfg> {
+        select_elim_cfg m_cfg;
+    public:
+        select_elim_star(ast_manager & m, model_ref& md, params_ref const & p = params_ref()):
+            rewriter_tpl<select_elim_cfg>(m, false, m_cfg),
+            m_cfg(m, md, p) {}
+    };
 
 
-void model_evaluator::assign_value(expr* e, expr* val) {
+
+    /////////////////////////
+    // model_evaluator
+    //
+    
+
+    void model_evaluator::assign_value(expr* e, expr* val) {
         rational r;
         if (m.is_true(val)) {
             set_true(e);
@@ -111,9 +155,9 @@ void model_evaluator::assign_value(expr* e, expr* val) {
             TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << "\n";);
             set_x(e);
         }
-}
+    }
 
-void model_evaluator::setup_model(model_ref& model) {
+    void model_evaluator::setup_model(model_ref& model) {
         m_numbers.reset();
         m_values.reset();
         m_model = model;
@@ -126,9 +170,9 @@ void model_evaluator::setup_model(model_ref& model) {
             m_refs.push_back(e);
             assign_value(e, val);
         }
-}
+    }
     
-void model_evaluator::reset() {
+    void model_evaluator::reset() {
         m1.reset();
         m2.reset();
         m_values.reset();
@@ -136,9 +180,9 @@ void model_evaluator::reset() {
         m_numbers.reset();
         m_refs.reset();
         m_model = 0;
-}
+    }
     
-expr_ref_vector model_evaluator::minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl) {
+    expr_ref_vector model_evaluator::minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl) {
         setup_model(mdl);
         
         TRACE("pdr_verbose", 
@@ -159,9 +203,9 @@ expr_ref_vector model_evaluator::minimize_model(ptr_vector<expr> const & formula
             reset(););
         
         return model;
-}
+    }
     
-expr_ref_vector model_evaluator::minimize_literals(ptr_vector<expr> const& formulas, model_ref& mdl) {
+    expr_ref_vector model_evaluator::minimize_literals(ptr_vector<expr> const& formulas, model_ref& mdl) {
         
         TRACE("pdr", 
               tout << "formulas:\n";
@@ -169,6 +213,7 @@ expr_ref_vector model_evaluator::minimize_literals(ptr_vector<expr> const& formu
               );
         
         expr_ref_vector result(m);
+        expr_ref tmp(m);
         ptr_vector<expr> tocollect;
         
         setup_model(mdl);
@@ -184,11 +229,21 @@ expr_ref_vector model_evaluator::minimize_literals(ptr_vector<expr> const& formu
                 result.push_back(m.mk_not(e));
             }
         }
+        select_elim_star select_elim(m, m_model);
+        for (unsigned i = 0; i < result.size(); ++i) {
+            select_elim(result[i].get(), tmp);
+            result[i] = tmp;
+        }
         reset();
-    return result;
+        TRACE("pdr", 
-}
+              tout << "minimized model:\n";
+              for (unsigned i = 0; i < result.size(); ++i) tout << mk_pp(result[i].get(), m) << "\n"; 
+              );
         
-void model_evaluator::process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect) {
+        return result;
+    }
+    
+    void model_evaluator::process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect) {
         SASSERT(m.is_bool(e));
         SASSERT(is_true(e) || is_false(e));
         unsigned v = is_true(e);
@@ -292,9 +347,9 @@ void model_evaluator::process_formula(app* e, ptr_vector<expr>& todo, ptr_vector
         else {
             tocollect.push_back(e);
         }
-}
+    }
     
-void model_evaluator::collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect) {
+    void model_evaluator::collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect) {
         ptr_vector<expr> todo;
         todo.append(formulas);
         m_visited.reset();
@@ -310,9 +365,9 @@ void model_evaluator::collect(ptr_vector<expr> const& formulas, ptr_vector<expr>
             }
         }
         m_visited.reset();
-}
+    }
     
-expr_ref_vector model_evaluator::prune_by_cone_of_influence(ptr_vector<expr> const & formulas) {
+    expr_ref_vector model_evaluator::prune_by_cone_of_influence(ptr_vector<expr> const & formulas) {
         ptr_vector<expr> tocollect;
         collect(formulas, tocollect);
         m1.reset();
@@ -337,9 +392,9 @@ expr_ref_vector model_evaluator::prune_by_cone_of_influence(ptr_vector<expr> con
         TRACE("pdr", tout << sz << " ==> " << model.size() << "\n";);
         return model;
         
-}
+    }
     
-void model_evaluator::eval_arith(app* e) {
+    void model_evaluator::eval_arith(app* e) {
         rational r, r2;
         
 #define ARG1 e->get_arg(0)
@@ -462,9 +517,9 @@ void model_evaluator::eval_arith(app* e) {
             UNREACHABLE();
             break;
         }
-}
+    }
     
-void model_evaluator::inherit_value(expr* e, expr* v) {
+    void model_evaluator::inherit_value(expr* e, expr* v) {
         expr* w;
         SASSERT(!is_unknown(v));
         SASSERT(m.get_sort(e) == m.get_sort(v));
@@ -493,16 +548,128 @@ void model_evaluator::inherit_value(expr* e, expr* v) {
             TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
             set_x(e);
         }
-}
+    }
     
-void model_evaluator::eval_iff(app* e, expr* arg1, expr* arg2) {
+    bool model_evaluator::extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref else_case) {
+        SASSERT(m_array.is_array(a));
+        
+        while (m_array.is_store(a)) {
+            expr_ref_vector store(m);
+            store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
+            stores.push_back(store);
+            a = to_app(a)->get_arg(0);
+        }
+        
+        if (m_array.is_const(a)) {
+            else_case = to_app(a)->get_arg(0);
+            return true;
+        }
+        
+        if (m_array.is_as_array(a)) {
+            func_decl* f = m_array.get_as_array_func_decl(to_app(a));
+            func_interp* g = m_model->get_func_interp(f);
+            unsigned sz = g->num_entries();
+            unsigned arity = f->get_arity();
+            for (unsigned i = 0; i < sz; ++i) {
+                expr_ref_vector store(m);
+                func_entry const* fe = g->get_entry(i);
+                store.append(arity, fe->get_args());
+                store.push_back(fe->get_result());
+                for (unsigned j = 0; j < store.size(); ++j) {
+                    if (!is_ground(store[j].get())) {
+                        return false;
+                    }
+                }
+                stores.push_back(store);
+            }        
+            else_case = g->get_else();
+            if (!is_ground(else_case)) {
+                return false;
+            }
+            return true;
+        }
+        
+        return false;
+    }
+    
+    /**
+       best effort evaluator of extensional array equality.
+     */
+    void model_evaluator::eval_array_eq(app* e, expr* arg1, expr* arg2) {
+        expr_ref v1(m), v2(m);
+        m_model->eval(arg1, v1);
+        m_model->eval(arg2, v2);
+        if (v1 == v2) {
+            set_true(e);
+            return;
+        }
+        sort* s = m.get_sort(arg1);
+        sort* r = get_array_range(s);
+        if (!r->is_infinite() && !r->is_very_big()) {
+            TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
+            set_x(e);
+            return;
+        }
+        vector<expr_ref_vector> store;
+        expr_ref else1(m), else2(m);
+        if (!extract_array_func_interp(v1, store, else1) ||
+            !extract_array_func_interp(v2, store, else2)) {
+            TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
+            set_x(e);
+            return;
+        }
+
+        if (else1 != else2) {
+            if (m.is_value(else1) && m.is_value(else2)) {
+                set_bool(e, false);
+            }
+            else {
+                TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
+                set_x(e);
+            }
+            return;
+        }
+
+        expr_ref s1(m), s2(m), w1(m), w2(m);        
+        expr_ref_vector args1(m), args2(m);
+        args1.push_back(v1);
+        args2.push_back(v2);        
+        for (unsigned i = 0; i < store.size(); ++i) {
+            args1.resize(1);
+            args2.resize(1);
+            args1.append(store[i].size()-1, store[i].c_ptr());
+            args2.append(store[i].size()-1, store[i].c_ptr());
+            s1 = m_array.mk_select(args1.size(), args1.c_ptr());
+            s2 = m_array.mk_select(args2.size(), args2.c_ptr());
+            m_model->eval(s1, w1);
+            m_model->eval(s2, w2);
+            if (w1 == w2) {
+                continue;
+            }
+            else if (m.is_value(w1) && m.is_value(w2)) {
+                set_bool(e, false);
+                return;
+            }
+            else {
+                TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
+                set_x(e);
+                return;
+            }
+        }
+        set_bool(e, true);                
+    }
+
+    void model_evaluator::eval_eq(app* e, expr* arg1, expr* arg2) {
         if (arg1 == arg2) {
             set_true(e);
         }
+        else if (m_array.is_array(arg1)) {
+            eval_array_eq(e, arg1, arg2);
+        }
         else if (is_x(arg1) || is_x(arg2)) {
             set_x(e);
         }
-    else {
+        else if (m.is_bool(arg1)) {
             bool val = is_true(arg1) == is_true(arg2);
             SASSERT(val == (is_false(arg1) == is_false(arg2)));
             if (val) {
@@ -512,9 +679,26 @@ void model_evaluator::eval_iff(app* e, expr* arg1, expr* arg2) {
                 set_false(e);
             }            
         }
-}
+        else if (m_arith.is_int_real(arg1)) {
+            set_bool(e, get_number(arg1) == get_number(arg2));
+        }
+        else {
+            expr* e1 = get_value(arg1);
+            expr* e2 = get_value(arg2);
+            if (m.is_value(e1) && m.is_value(e2)) {
+                set_bool(e, e1 == e2);
+            }
+            else if (e1 == e2) {
+                set_bool(e, true);
+            }
+            else {
+                TRACE("pdr", tout << "not value equal:\n" << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";);
+                set_x(e);
+            }
+        }
+    }
 
-void model_evaluator::eval_basic(app* e) {
+    void model_evaluator::eval_basic(app* e) {
         expr* arg1, *arg2;
         expr *argCond, *argThen, *argElse, *arg;
         bool has_x = false;
@@ -593,7 +777,7 @@ void model_evaluator::eval_basic(app* e) {
             break;
         case OP_IFF: 
             VERIFY(m.is_iff(e, arg1, arg2));
-        eval_iff(e, arg1, arg2);
+            eval_eq(e, arg1, arg2);
             break;
         case OP_ITE: 
             VERIFY(m.is_ite(e, argCond, argThen, argElse));
@@ -630,29 +814,7 @@ void model_evaluator::eval_basic(app* e) {
             break;
         case OP_EQ:
             VERIFY(m.is_eq(e, arg1, arg2));
-        if (m.is_bool(arg1)) {
+            eval_eq(e, arg1, arg2);
-            eval_iff(e, arg1, arg2);
-        }
-        else if (arg1 == arg2) {
-            set_true(e);
-        }
-        else if (is_x(arg1) || is_x(arg2)) {
-            set_x(e);
-        }
-        else if (m_arith.is_int_real(arg1)) {
-            set_bool(e, get_number(arg1) == get_number(arg2));
-        }
-        else {
-            expr* e1 = get_value(arg1);
-            expr* e2 = get_value(arg2);
-            if (m.is_value(e1) && m.is_value(e2)) {
-                set_bool(e, e1 == e2);
-            }
-            else {
-                TRACE("pdr", tout << "not value equal:\n" << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";);
-                set_x(e);
-            }
-        }
             break;
         case OP_DISTINCT: {
             vector<rational> values;
@@ -678,9 +840,9 @@ void model_evaluator::eval_basic(app* e) {
             IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
             UNREACHABLE();        
         }
-}
+    }
     
-bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
+    bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
         ptr_vector<expr> todo(formulas);
         
         while (!todo.empty()) {
@@ -740,70 +902,6 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
             }
         }
         return !has_x;
-}
-
-    func_decl * mk_store(ast_manager& m, sort * arr_sort)
-    {
-        family_id array_fid = m.get_family_id(symbol("array"));
-        
-        unsigned num_params = arr_sort->get_num_parameters();
-        
-        ptr_vector<sort> domain;
-        domain.push_back(arr_sort);
-        
-        //we push params of the array as remaining arguments of the store. The first 
-        //num_params-1 parameters are indices and the last one is the range of the array
-        for (unsigned i=0; i<num_params; ++i) {
-            domain.push_back(to_sort(arr_sort->get_parameter(i).get_ast()));
-        }
-        
-        return m.mk_func_decl(array_fid, OP_STORE, 
-                              arr_sort->get_num_parameters(), arr_sort->get_parameters(), 
-                              domain.size(), domain.c_ptr(), arr_sort);
-    }
-
-    void get_as_array_value(const model_core & mdl, expr * arr_e, expr_ref& res) {
-        ast_manager& m = mdl.get_manager();
-        array_util pl(m);
-        SASSERT(pl.is_as_array(arr_e));
-        
-        app * arr = to_app(arr_e);
-    
-        unsigned sz = 0;
-        func_decl_ref f(pl.get_as_array_func_decl(arr), m);
-        sort * arr_sort = arr->get_decl()->get_range();
-        func_interp* g = mdl.get_func_interp(f);
-        
-        res = pl.mk_const_array(arr_sort, g->get_else());
-
-        unsigned arity = f->get_arity();
-        
-        sz = g->num_entries();
-        if (sz) {
-            func_decl_ref store_fn(mk_store(m, arr_sort), m);
-            ptr_vector<expr> store_args;
-            for (unsigned i = 0; i < sz; ++i) {
-                const func_entry * fe = g->get_entry(i);
-                store_args.reset();
-                store_args.push_back(res);
-                store_args.append(arity, fe->get_args());
-                store_args.push_back(fe->get_result());
-                res = m.mk_app(store_fn, store_args.size(), store_args.c_ptr());
-            }
-        }
-    }
-
-    void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res) {
-        SASSERT(f->get_arity()==0);
-        ast_manager& m = mdl.get_manager();
-        
-        res = mdl.get_const_interp(f);
-        
-        array_util pl(m);
-        
-        if (pl.is_as_array(res)) {
-            get_as_array_value(mdl, res, res);
-        }
     }
 
     void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
@@ -915,7 +1013,6 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
             return m_r.mk_app_core(f, num, args, result);
         }
         ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {}        
-        
     };
 
     class ite_hoister_star : public rewriter_tpl<ite_hoister_cfg> {

src/muz_qe/pdr_util.h

@@ -28,6 +28,7 @@ Revision History:
 #include "trace.h"
 #include "vector.h"
 #include "arith_decl_plugin.h"
+#include "array_decl_plugin.h"
 #include "bv_decl_plugin.h"
 
 
@@ -56,6 +57,7 @@ namespace pdr {
     class model_evaluator {
         ast_manager&           m;
         arith_util             m_arith;
+        array_util             m_array;
         obj_map<expr,rational> m_numbers;
         expr_ref_vector        m_refs;
         obj_map<expr, expr*>   m_values;
@@ -78,7 +80,8 @@ namespace pdr {
         expr_ref_vector prune_by_cone_of_influence(ptr_vector<expr> const & formulas);
         void eval_arith(app* e);
         void eval_basic(app* e);
-        void eval_iff(app* e, expr* arg1, expr* arg2);
+        void eval_eq(app* e, expr* arg1, expr* arg2);
+        void eval_array_eq(app* e, expr* arg1, expr* arg2);
         void inherit_value(expr* e, expr* v);
         
         inline bool is_unknown(expr* x)  { return !m1.is_marked(x) && !m2.is_marked(x); }
@@ -100,8 +103,10 @@ namespace pdr {
         
         bool check_model(ptr_vector<expr> const & formulas);
 
+        bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref else_case);
+        
     public:
-        model_evaluator(ast_manager& m) : m(m), m_arith(m), m_refs(m) {}
+        model_evaluator(ast_manager& m) : m(m), m_arith(m), m_array(m), m_refs(m) {}
             
         /**
            \brief extract equalities from model that suffice to satisfy formula.
@@ -118,13 +123,12 @@ namespace pdr {
        */
        expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, model_ref& mdl);
 
-
+       /** 
-       // for_each_expr visitor.
+           for_each_expr visitor.
+       */
        void operator()(expr* e) {} 
     };
 
-    void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res);
-
     /**
        \brief replace variables that are used in many disequalities by
        an equality using the model.