update unstable branch with qhc changes that don't have dependencies

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

src/muz_qe/dl_bmc_engine.h

@@ -35,83 +35,23 @@ namespace datalog {
         ast_manager&     m;
         smt_params       m_fparams;
         smt::kernel      m_solver;
-        obj_map<func_decl, sort*> m_pred2sort;
-        obj_map<sort, func_decl*> m_sort2pred;
-        obj_map<func_decl, func_decl*> m_pred2newpred;
-        obj_map<func_decl, ptr_vector<func_decl> > m_pred2args;
-        ast_ref_vector   m_pinned;
         rule_set         m_rules;
         func_decl_ref    m_query_pred;
         expr_ref         m_answer;
         volatile bool    m_cancel;
         proof_converter_ref m_pc;
-        sort_ref         m_path_sort;
-        bv_util          m_bv;
-        unsigned         m_bit_width;
-
-        lbool check_query();
-
-        proof_ref get_proof(model_ref& md, app* trace, app* path);
 
         void checkpoint();
 
-        void declare_datatypes();
+        class nonlinear_dt;
-
+        class nonlinear;
-        void compile_nonlinear();
+        class qlinear;
-
+        class linear;
-        void mk_rule_vars_nonlinear(rule& r, unsigned rule_id, expr* trace_arg, expr* path_arg, expr_ref_vector& sub);
-
-        expr_ref mk_var_nonlinear(func_decl* pred, sort* s, unsigned idx, expr* path_arg, expr* trace_arg);
-
-        expr_ref mk_arg_nonlinear(func_decl* pred, unsigned idx, expr* path_arg, expr* trace_arg);
-
-        void mk_subst(rule& r, expr* path, app* trace, expr_ref_vector& sub);
 
         bool is_linear() const;
         
-        lbool check_nonlinear();
-        void  setup_nonlinear();
-        bool check_model_nonlinear(model_ref& md, expr* trace);
-        void mk_answer_nonlinear(model_ref& md, expr_ref& trace, expr_ref& path);
-        
-        func_decl_ref mk_predicate(func_decl* p);
-
-        func_decl_ref mk_rule(func_decl* p, unsigned rule_idx);
-
-        // linear check
-        lbool check_linear();
-        lbool check_linear(unsigned level);
-        void compile_linear();
-        void compile_linear(unsigned level);
-        void compile_linear(rule& r, unsigned level);
-        expr_ref mk_level_predicate(symbol const& name, unsigned level);
-        expr_ref mk_level_predicate(func_decl* p, unsigned level);
-        expr_ref mk_level_arg(func_decl* pred, unsigned idx, unsigned level);
-        expr_ref mk_level_rule(func_decl* p, unsigned rule_idx, unsigned level);
-        expr_ref mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level);
-        void get_model_linear(unsigned level);
-        void setup_linear();
-
         void assert_expr(expr* e);
 
-        void mk_rule_vars(rule& r, unsigned level, unsigned rule_id, expr_ref_vector& sub);
-
-        // quantified linear check
-        void  compile_qlinear();
-        void  setup_qlinear();
-        lbool check_qlinear();
-        lbool get_model_qlinear();
-        sort_ref mk_index_sort();
-        var_ref mk_index_var();
-        void mk_qrule_vars(datalog::rule const& r, unsigned i, expr_ref_vector& sub);
-        expr_ref mk_q_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx);
-        expr_ref mk_q_arg(func_decl* pred, unsigned idx, bool is_current);
-        expr_ref mk_q_one();
-        expr_ref mk_q_num(unsigned i);
-        expr_ref eval_q(model_ref& model, expr* t, unsigned i);
-        expr_ref eval_q(model_ref& model, func_decl* f, unsigned i);
-        func_decl_ref mk_q_rule(func_decl* f, unsigned rule_id);
-        func_decl_ref mk_q_func_decl(func_decl* f);
 
     public:
         bmc(context& ctx);
@@ -131,6 +71,10 @@ namespace datalog {
         void reset_statistics(); 
 
         expr_ref get_answer();
+
+        // direct access to (new) non-linear compiler.
+        void compile(rule_set const& rules, expr_ref_vector& fmls, unsigned level);
+        expr_ref compile_query(func_decl* query_pred, unsigned level);
     };
 };
 

src/muz_qe/dl_context.cpp

@@ -715,6 +715,8 @@ namespace datalog {
             check_positive_predicates(r);
             break;
         case BMC_ENGINE:
+            check_positive_predicates(r);
+            break;            
         case QBMC_ENGINE:
             check_existential_tail(r);
             check_positive_predicates(r);

src/muz_qe/dl_mk_array_blast.cpp

@@ -18,7 +18,8 @@ Revision History:
 --*/
 
 #include "dl_mk_array_blast.h"
-#include "expr_replacer.h"
+#include "expr_safe_replace.h"
+
 
 namespace datalog {
 
@@ -54,9 +55,10 @@ namespace datalog {
         unsigned tsz = r.get_tail_size();
         expr_ref_vector conjs(m), new_conjs(m);
         expr_ref tmp(m);
-        expr_substitution sub(m);
+        expr_safe_replace sub(m);
         uint_set lhs_vars, rhs_vars;
         bool change = false;
+        bool inserted = false;
 
         for (unsigned i = 0; i < utsz; ++i) {
             new_conjs.push_back(r.get_tail(i));
@@ -81,6 +83,7 @@ namespace datalog {
                 }
                 else {
                     sub.insert(x, y);
+                    inserted = true;
                 }
             }
             else {
@@ -89,7 +92,7 @@ namespace datalog {
                 new_conjs.push_back(tmp);
             }
         }
-        if (sub.empty() && !change) {
+        if (!inserted && !change) {
             rules.add_rule(&r);
             return false;
         }
@@ -99,11 +102,9 @@ namespace datalog {
         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);
+        sub(body);
-        replace->set_substitution(&sub);
-        (*replace)(body);
         m_rewriter(body);
-        (*replace)(head);
+        sub(head);
         m_rewriter(head);
         fml2 = m.mk_implies(body, head);
         rm.mk_rule(fml2, new_rules, r.name());

src/muz_qe/dl_mk_coalesce.cpp

@@ -60,7 +60,7 @@ namespace datalog {
         obj_map<expr, unsigned> indices;
         bool_rewriter bwr(m);
         rule_ref r(const_cast<rule*>(&rl), rm);
-        sort_ref_vector sorts(m);
+        ptr_vector<sort> sorts;
         expr_ref_vector revsub(m), conjs(m);
         rl.get_vars(sorts);
         revsub.resize(sorts.size());  
@@ -72,8 +72,8 @@ namespace datalog {
             if (is_var(e)) {
                 unsigned v = to_var(e)->get_idx();
                 SASSERT(v < valid.size());
-                if (sorts[v].get()) {
+                if (sorts[v]) {
-                    SASSERT(s == sorts[v].get());
+                    SASSERT(s == sorts[v]);
                     if (valid[v]) {
                         revsub[v] = w;
                         valid[v] = false;
@@ -92,8 +92,8 @@ namespace datalog {
             }
         }
         for (unsigned i = 0; i < sorts.size(); ++i) {
-            if (valid[i] && sorts[i].get() && !revsub[i].get()) {
+            if (valid[i] && sorts[i] && !revsub[i].get()) {
-                revsub[i] = m.mk_var(m_idx++, sorts[i].get());
+                revsub[i] = m.mk_var(m_idx++, sorts[i]);
             }
         }
         var_subst vs(m, false);
@@ -112,7 +112,7 @@ namespace datalog {
         app_ref pred(m), head(m);
         expr_ref fml1(m), fml2(m), fml(m);
         app_ref_vector tail(m);
-        sort_ref_vector sorts1(m), sorts2(m);
+        ptr_vector<sort> sorts1, sorts2;
         expr_ref_vector conjs1(m), conjs(m);
         rule_ref res(rm);
         bool_rewriter bwr(m);

src/muz_qe/dl_mk_extract_quantifiers2.cpp

@@ -0,0 +1,366 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_extract_quantifiers2.cpp
+
+Abstract:
+
+    Remove universal quantifiers over interpreted predicates in the body.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-21
+
+Revision History:
+
+--*/
+
+#include"dl_mk_extract_quantifiers2.h"
+#include"ast_pp.h"
+#include"dl_bmc_engine.h"
+#include"smt_quantifier.h"
+#include"smt_context.h"
+
+namespace datalog {
+
+
+    mk_extract_quantifiers2::mk_extract_quantifiers2(context & ctx) : 
+        rule_transformer::plugin(101, false),
+        m_ctx(ctx),
+        m(ctx.get_manager()),
+        rm(ctx.get_rule_manager()),
+        m_query_pred(m),
+        m_quantifiers(m),
+        m_refs(m)
+    {}
+
+    mk_extract_quantifiers2::~mk_extract_quantifiers2() {
+        reset();
+    }
+
+    void mk_extract_quantifiers2::set_query(func_decl* q) {
+        m_query_pred = q;
+    }
+
+    bool mk_extract_quantifiers2::matches_signature(func_decl* head, expr_ref_vector const& binding) {
+        unsigned sz = head->get_arity();
+        if (sz != binding.size()) {
+            return false;
+        }
+        for (unsigned i = 0; i < sz; ++i) {
+            if (head->get_domain(i) != m.get_sort(binding[sz-i-1])) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    bool mk_extract_quantifiers2::matches_quantifier(quantifier* q, expr_ref_vector const& binding) {
+        unsigned sz = q->get_num_decls();
+        if (sz != binding.size()) {
+            return false;
+        }
+        for (unsigned i = 0; i < sz; ++i) {
+            if (q->get_decl_sort(i) != m.get_sort(binding[sz-i-1])) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    bool mk_extract_quantifiers2::mk_abstract_expr(expr_ref& term) {
+        if (!is_app(term)) {
+            return false;
+        }
+        expr* r;
+        if (m_map.find(term, r)) {
+            term = r;
+            return true;
+        }
+        if (to_app(term)->get_family_id() == null_family_id) {
+            return false;
+        }
+        expr_ref_vector args(m);
+        expr_ref tmp(m);
+        for (unsigned i = 0; i < to_app(term)->get_num_args(); ++i) {
+            tmp = to_app(term)->get_arg(i);
+            if (!mk_abstract_expr(tmp)) {
+                return false;
+            }
+            args.push_back(tmp);
+        }
+        tmp = m.mk_app(to_app(term)->get_decl(), args.size(), args.c_ptr());
+        m_refs.push_back(tmp);
+        m_map.insert(term, tmp);
+        term = tmp;
+        return true;
+    }
+    
+    bool mk_extract_quantifiers2::mk_abstract_binding(expr_ref_vector const& binding, expr_ref_vector& result) {
+        for (unsigned i = 0; i < binding.size(); ++i) {
+            expr_ref tmp(m);
+            tmp = binding[i];
+            if (!mk_abstract_expr(tmp)) {
+                return false;
+            }
+            result.push_back(tmp);
+        }
+        return true;
+    }
+    
+    void mk_extract_quantifiers2::mk_abstraction_map(rule& r, expr_ref_vector const& binding) {
+        m_map.reset();
+        unsigned sz = binding.size();
+        SASSERT(sz == r.get_decl()->get_arity());
+        for (unsigned i = 0; i < sz; ++i) {
+            m_map.insert(binding[sz-i-1], r.get_head()->get_arg(i));
+            SASSERT(m.get_sort(binding[sz-i-1]) == m.get_sort(r.get_head()->get_arg(i)));
+        }
+        // todo: also make bindings for variables in rule body.
+    }
+
+    void mk_extract_quantifiers2::match_bindings(unsigned i, unsigned j, unsigned k) {
+        expr_ref_vector resb(m);
+        rule* r = m_qrules[i];
+        quantifier* q = m_quantifiers[i].get();
+        expr_ref_vector const& ruleb = m_rule_bindings[i][j];
+        expr_ref_vector const& quantb = m_quantifier_bindings[i][k];
+        mk_abstraction_map(*r, ruleb);
+        if (!mk_abstract_binding(quantb, resb)) {
+            return;
+        }
+        expr_ref inst(m), tmp(m);
+        var_shifter shift(m);
+        
+        for (unsigned l = 0; l < resb.size(); ++l) {
+            tmp = resb[l].get();
+            shift(tmp, q->get_num_decls(), tmp);
+            resb[l] = tmp;
+        }
+
+        instantiate(m, q, resb.c_ptr(), inst);
+        if (!m_seen.contains(r)) {
+            m_seen.insert(r, alloc(obj_hashtable<expr>));
+        }
+        obj_hashtable<expr>& seen = *m_seen.find(r);
+        if (seen.contains(inst)) {
+            return;
+        }
+        seen.insert(inst);
+        m_refs.push_back(inst);
+        if (!m_quantifier_instantiations.contains(r, q)) {
+            m_quantifier_instantiations.insert(r, q, alloc(expr_ref_vector, m));
+        }
+        expr_ref_vector* vec = 0;
+        VERIFY(m_quantifier_instantiations.find(r, q, vec));
+        vec->push_back(inst);
+        TRACE("dl", tout << "matched: " << mk_pp(q, m) << "\n" << mk_pp(inst, m) << "\n";);
+    }
+
+    app_ref mk_extract_quantifiers2::ensure_app(expr* e) {
+        if (is_app(e)) {
+            return app_ref(to_app(e), m);
+        }
+        else {
+            return app_ref(m.mk_eq(e, m.mk_true()), m);
+        }
+    }
+
+    void mk_extract_quantifiers2::extract(rule& r, rule_set& new_rules) {
+        unsigned utsz = r.get_uninterpreted_tail_size();
+        unsigned tsz = r.get_tail_size();
+        bool has_quantifier = false;
+        expr_ref_vector conjs(m);
+        for (unsigned i = utsz; i < tsz; ++i) {
+            conjs.push_back(r.get_tail(i));
+        }
+        datalog::flatten_and(conjs);
+        for (unsigned j = 0; j < conjs.size(); ++j) {
+            expr* e = conjs[j].get();
+            quantifier* q;
+            if (rule_manager::is_forall(m, e, q)) {
+                m_quantifiers.push_back(q);
+                m_qrules.push_back(&r);
+                m_rule_bindings.push_back(vector<expr_ref_vector>());
+                m_quantifier_bindings.push_back(vector<expr_ref_vector>());
+                has_quantifier = true;
+            }
+        }
+        if (!has_quantifier) {
+            new_rules.add_rule(&r);
+        }
+    }
+
+    void mk_extract_quantifiers2::apply(rule& r, rule_set& new_rules) {
+        expr_ref_vector tail(m), conjs(m);
+        expr_ref fml(m);
+        unsigned utsz = r.get_uninterpreted_tail_size();
+        unsigned tsz = r.get_tail_size();
+        for (unsigned i = 0; i < utsz; ++i) {
+            SASSERT(!r.is_neg_tail(i));
+            tail.push_back(r.get_tail(i));
+        }
+        bool has_quantifier = false;
+        for (unsigned i = utsz; i < tsz; ++i) {
+            conjs.push_back(r.get_tail(i));
+        }
+        datalog::flatten_and(conjs);
+        for (unsigned j = 0; j < conjs.size(); ++j) {
+            expr* e = conjs[j].get();
+            quantifier* q;
+            if (rule_manager::is_forall(m, e, q)) {
+                expr_ref_vector* ls;
+                if (m_quantifier_instantiations.find(&r,q,ls)) {
+                    tail.append(*ls);
+                }
+                has_quantifier = true;
+            }
+            else {
+                tail.push_back(e);
+            }
+        }
+        if (has_quantifier) {
+            fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), r.get_head());
+            rule_ref_vector rules(rm);
+            rm.mk_rule(fml, rules, r.name());
+            for (unsigned i = 0; i < rules.size(); ++i) {
+                new_rules.add_rule(rules[i].get());
+            }
+        }
+    }
+
+#if 0
+    class mk_extract_quantifiers2::instance_plugin : public smt::quantifier_instance_plugin {
+        mk_extract_quantifiers2& ex;
+        ast_manager&        m;
+        expr_ref_vector     m_refs;
+        obj_hashtable<expr> m_bindings;
+    public:
+        instance_plugin(mk_extract_quantifiers2& ex): ex(ex), m(ex.m), m_refs(m) {}
+
+        virtual void operator()(quantifier* q, unsigned num_bindings, smt::enode*const* bindings) {
+            expr_ref_vector binding(m);
+            ptr_vector<sort> sorts;
+            for (unsigned i = 0; i < num_bindings; ++i) {
+                binding.push_back(bindings[i]->get_owner());
+                sorts.push_back(m.get_sort(binding[i].get()));
+            }
+            func_decl* f = m.mk_func_decl(symbol("T"), sorts.size(), sorts.c_ptr(), m.mk_bool_sort());
+            expr_ref tup(m);
+            tup = m.mk_app(f, binding.size(), binding.c_ptr());
+            if (!m_bindings.contains(tup)) {
+                m_bindings.insert(tup);
+                m_refs.push_back(tup);
+                ex.m_bindings.push_back(binding);
+                TRACE("dl", tout << "insert\n" << mk_pp(q, m) << "\n" << mk_pp(tup, m) << "\n";);
+            }
+        }
+    };
+
+#endif
+
+    void mk_extract_quantifiers2::reset() {
+        {
+            obj_pair_map<rule,quantifier, expr_ref_vector*>::iterator 
+                it  = m_quantifier_instantiations.begin(),
+                end = m_quantifier_instantiations.end();
+            for (; it != end; ++it) {
+                dealloc(it->get_value());
+            }        
+        }
+        {
+            obj_map<rule,obj_hashtable<expr>*>::iterator 
+                it  = m_seen.begin(), 
+                end = m_seen.end();
+            for (; it != end; ++it) {
+                dealloc(it->m_value);
+            }
+        }
+        m_quantifier_instantiations.reset();
+        m_seen.reset();
+        m_has_quantifiers = false;
+        m_quantifiers.reset();
+        m_qrules.reset();
+        m_bindings.reset();
+        m_rule_bindings.reset();
+        m_quantifier_bindings.reset();
+        m_refs.reset();
+    }
+    
+    rule_set * mk_extract_quantifiers2::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
+        reset();
+        rule_set::iterator it = source.begin(), end = source.end();
+        for (; !m_has_quantifiers && it != end; ++it) {
+            m_has_quantifiers = (*it)->has_quantifiers();
+        }
+        if (!m_has_quantifiers) {
+            return 0;
+        }
+
+        rule_set* rules = alloc(rule_set, m_ctx);
+        it = source.begin();
+        for (; it != end; ++it) {
+            extract(**it, *rules);
+        }
+
+        bmc bmc(m_ctx);
+        expr_ref_vector fmls(m);
+        bmc.compile(source, fmls, 0); // TBD: use cancel_eh to terminate without base-case.
+        bmc.compile(source, fmls, 1);
+        bmc.compile(source, fmls, 2);
+//        bmc.compile(source, fmls, 3);
+        expr_ref query = bmc.compile_query(m_query_pred, 2);
+        fmls.push_back(query);
+        smt_params fparams;
+        fparams.m_relevancy_lvl = 0;
+        fparams.m_model = true;
+        fparams.m_model_compact = true;
+        fparams.m_mbqi = true;
+        smt::kernel solver(m, fparams);
+        TRACE("dl", 
+              for (unsigned i = 0; i < fmls.size(); ++i) {
+                  tout << mk_pp(fmls[i].get(), m) << "\n";
+              });
+
+        for (unsigned i = 0; i < fmls.size(); ++i) {
+            solver.assert_expr(fmls[i].get());
+        }
+#if 0
+        smt::context& ctx = solver.get_context();
+        smt::quantifier_manager* qm = ctx.get_quantifier_manager();
+        qm->get_plugin()->set_instance_plugin(alloc(instance_plugin, *this));
+#endif
+        lbool res = solver.check();
+
+        for (unsigned i = 0; i < m_bindings.size(); ++i) {
+            expr_ref_vector& binding = m_bindings[i];
+            for (unsigned j = 0; j < m_qrules.size(); ++j) {
+                rule* r = m_qrules[j];
+                if (matches_signature(r->get_decl(), binding)) {
+                    m_rule_bindings[j].push_back(binding);
+                }
+                else if (matches_quantifier(m_quantifiers[j].get(), binding)) {
+                    m_quantifier_bindings[j].push_back(binding);
+                }
+            }
+        }
+        for (unsigned i = 0; i < m_qrules.size(); ++i) {
+            for (unsigned j = 0; j < m_rule_bindings[i].size(); ++j) {
+                for (unsigned k = 0; k < m_quantifier_bindings[i].size(); ++k) {
+                    match_bindings(i, j, k);
+                }
+            }
+        }
+        it = source.begin();
+        for (; it != end; ++it) {
+            apply(**it, *rules);
+        }
+
+        return rules;
+    }
+
+};
+
+

src/muz_qe/dl_mk_extract_quantifiers2.h

@@ -0,0 +1,91 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_extract_quantifiers2.h
+
+Abstract:
+
+    Replace universal quantifiers over interpreted predicates in the body
+    by instantiations mined using bounded model checking search.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-21
+
+Revision History:
+
+--*/
+#ifndef _DL_MK_EXTRACT_QUANTIFIERS2_H_
+#define _DL_MK_EXTRACT_QUANTIFIERS2_H_
+
+#include"dl_context.h"
+#include"dl_rule_set.h"
+#include"dl_rule_transformer.h"
+#include"obj_pair_hashtable.h"
+
+namespace datalog {
+
+    /**
+       \brief Extract universal quantifiers from rules.
+    */
+    class mk_extract_quantifiers2 : public rule_transformer::plugin {
+        context&        m_ctx;
+        ast_manager&    m;
+        rule_manager&   rm;
+        func_decl_ref   m_query_pred;
+        quantifier_ref_vector   m_quantifiers;
+        ptr_vector<rule>        m_qrules;
+        vector<expr_ref_vector>m_bindings;
+        vector<vector<expr_ref_vector> > m_rule_bindings;
+        vector<vector<expr_ref_vector> > m_quantifier_bindings;
+        obj_pair_map<rule,quantifier, expr_ref_vector*> m_quantifier_instantiations;
+        obj_map<rule, obj_hashtable<expr>*>  m_seen;
+        
+        bool                    m_has_quantifiers;
+        obj_map<expr,expr*>     m_map;
+        expr_ref_vector         m_refs;
+
+        class instance_plugin;
+
+        void reset();
+
+        void extract(rule& r, rule_set& new_rules);
+
+        void apply(rule& r, rule_set& new_rules);
+
+        app_ref ensure_app(expr* e);
+
+        bool matches_signature(func_decl* head, expr_ref_vector const& binding);
+
+        bool matches_quantifier(quantifier* q, expr_ref_vector const& binding);
+
+        void match_bindings(unsigned i, unsigned j, unsigned k);
+
+        bool mk_abstract_expr(expr_ref& term);
+
+        bool mk_abstract_binding(expr_ref_vector const& binding, expr_ref_vector& result);
+
+        void mk_abstraction_map(rule& r, expr_ref_vector const& binding);
+
+    public:
+        /**
+           \brief Create rule transformer that extracts universal quantifiers (over recursive predicates).
+         */
+        mk_extract_quantifiers2(context & ctx);
+
+        virtual ~mk_extract_quantifiers2();
+
+        void set_query(func_decl* q);
+        
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+
+        bool has_quantifiers() { return m_has_quantifiers; }
+
+    };
+
+};
+
+#endif /* _DL_MK_EXTRACT_QUANTIFIERS2_H_ */
+

src/muz_qe/dl_mk_rule_inliner.cpp

@@ -136,14 +136,14 @@ namespace datalog {
     expr_ref_vector rule_unifier::get_rule_subst(const rule& r, bool is_tgt) {
         SASSERT(m_ready);
         expr_ref_vector result(m);
-        sort_ref_vector sorts(m);
+        ptr_vector<sort> sorts;
         expr_ref v(m), w(m);
         r.get_vars(sorts);
         for (unsigned i = 0; i < sorts.size(); ++i) {
-            if (!sorts[i].get()) {
+            if (!sorts[i]) {
                 sorts[i] = m.mk_bool_sort();
             }
-            v = m.mk_var(i, sorts[i].get());
+            v = m.mk_var(i, sorts[i]);
             m_subst.apply(2, m_deltas, expr_offset(v, is_tgt?0:1), w);
             result.push_back(w);            
         }        

src/muz_qe/dl_rule.cpp

@@ -41,6 +41,7 @@ Revision History:
 #include"expr_replacer.h"
 #include"bool_rewriter.h"
 #include"qe_lite.h"
+#include"expr_safe_replace.h"
 
 namespace datalog {
 
@@ -130,17 +131,15 @@ namespace datalog {
             return index;
         }
         // replace vars by de-bruijn indices
-        expr_substitution sub(m);
+        expr_safe_replace rep(m);
         for (unsigned i = 0; i < vars.size(); ++i) {
             app* v = vars[i].get();
             if (names) {
                 names->push_back(v->get_decl()->get_name());
             }                
-            sub.insert(v, m.mk_var(index++,m.get_sort(v)));
+            rep.insert(v, m.mk_var(index++,m.get_sort(v)));
         }
-        scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m); 
+        rep(fml);
-        rep->set_substitution(&sub);
-        (*rep)(fml);
         return index;
     }
 
@@ -936,7 +935,7 @@ namespace datalog {
         }        
     }
 
-    void rule::get_vars(sort_ref_vector& sorts) const {
+    void rule::get_vars(ptr_vector<sort>& sorts) const {
         sorts.reset();
         used_vars used;
         get_used_vars(used);

src/muz_qe/dl_rule.h

@@ -244,7 +244,7 @@ namespace datalog {
 
         void norm_vars(rule_manager & rm);
 
-        void get_vars(sort_ref_vector& sorts) const;
+        void get_vars(ptr_vector<sort>& sorts) const;
 
         void to_formula(expr_ref& result) const;
 

src/muz_qe/pdr_quantifiers.cpp

@@ -440,7 +440,7 @@ namespace pdr {
         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);
+        ptr_vector<sort> vars;
         uint_set empty_index_set;
         qe_lite qe(m);