From c09903288ff0aba8262586a874b17d7b5d0ab490 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 15 Sep 2014 16:14:22 -0700
Subject: [PATCH] have free variable utility use a class for more efficient
 re-use

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/ast_counter.cpp              |  13 +-
 src/ast/rewriter/ast_counter.h                |  13 +-
 src/ast/rewriter/var_subst.cpp                |  30 +++-
 src/ast/rewriter/var_subst.h                  |  18 +-
 src/muz/base/dl_context.cpp                   |  30 ++--
 src/muz/base/dl_context.h                     |   1 +
 src/muz/base/dl_rule.cpp                      | 157 ++++++++----------
 src/muz/base/dl_rule.h                        |  16 +-
 src/muz/base/dl_rule_set.h                    |   6 +-
 src/muz/base/dl_util.cpp                      |  19 ++-
 src/muz/base/dl_util.h                        |   9 +-
 src/muz/base/hnf.cpp                          |  13 +-
 src/muz/bmc/dl_bmc_engine.cpp                 |  24 +--
 src/muz/clp/clp_context.cpp                   |  14 +-
 src/muz/ddnf/ddnf.cpp                         |   6 +-
 src/muz/fp/dl_cmds.cpp                        |   1 +
 src/muz/fp/horn_tactic.cpp                    |   2 +-
 src/muz/pdr/pdr_context.cpp                   |  36 ++--
 src/muz/pdr/pdr_generalizers.cpp              |  18 +-
 src/muz/pdr/pdr_manager.cpp                   |   4 +-
 src/muz/pdr/pdr_manager.h                     |   4 +-
 src/muz/rel/dl_compiler.cpp                   |  39 ++---
 src/muz/rel/dl_compiler.h                     |  11 +-
 src/muz/rel/dl_mk_simple_joins.cpp            |   2 +-
 src/muz/rel/dl_relation_manager.cpp           |  10 +-
 src/muz/tab/tab_context.cpp                   |  20 ++-
 src/muz/transforms/dl_mk_array_blast.cpp      |   2 +-
 src/muz/transforms/dl_mk_bit_blast.cpp        |   5 +-
 src/muz/transforms/dl_mk_coalesce.cpp         |   6 +-
 .../dl_mk_quantifier_instantiation.cpp        |   2 +-
 src/muz/transforms/dl_mk_rule_inliner.cpp     |   2 +-
 .../dl_mk_separate_negated_tails.cpp          |   6 +-
 .../transforms/dl_mk_separate_negated_tails.h |   2 +-
 src/muz/transforms/dl_mk_slice.cpp            |  15 +-
 src/muz/transforms/dl_mk_unfold.cpp           |   2 +-
 src/qe/qe.cpp                                 |  15 +-
 src/smt/theory_arith.h                        |   1 +
 src/smt/theory_arith_core.h                   |   3 +-
 src/tactic/horn_subsume_model_converter.cpp   |  26 ++-
 39 files changed, 300 insertions(+), 303 deletions(-)

diff --git a/src/ast/rewriter/ast_counter.cpp b/src/ast/rewriter/ast_counter.cpp
index 6f49a232f..f1ec03528 100644
--- a/src/ast/rewriter/ast_counter.cpp
+++ b/src/ast/rewriter/ast_counter.cpp
@@ -18,12 +18,9 @@ Revision History:
 --*/
 
 #include "ast_counter.h"
-#include "var_subst.h"
 
 void counter::update(unsigned el, int delta) {
     int & counter = get(el);
-    SASSERT(!m_stay_non_negative || counter>=0);
-    SASSERT(!m_stay_non_negative || static_cast<int>(counter)>=-delta);
     counter += delta;
 }
 
@@ -92,16 +89,14 @@ int counter::get_max_counter_value() const {
 void var_counter::count_vars(ast_manager & m, const app * pred, int coef) {
     unsigned n = pred->get_num_args();
     for (unsigned i = 0; i < n; i++) {
-        m_sorts.reset();
-        m_todo.reset();
-        m_mark.reset();
-        ::get_free_vars(m_mark, m_todo, pred->get_arg(i), m_sorts);
-        for (unsigned j = 0; j < m_sorts.size(); ++j) {
-            if (m_sorts[j]) {
+        m_fv(pred->get_arg(i));
+        for (unsigned j = 0; j < m_fv.size(); ++j) {
+            if (m_fv[j]) {
                 update(j, coef);
             }
         }
     }
+    m_fv.reset();
 }
 
 
diff --git a/src/ast/rewriter/ast_counter.h b/src/ast/rewriter/ast_counter.h
index e7251079f..8b3ec3bbd 100644
--- a/src/ast/rewriter/ast_counter.h
+++ b/src/ast/rewriter/ast_counter.h
@@ -27,16 +27,16 @@ Revision History:
 #include "ast.h"
 #include "map.h"
 #include "uint_set.h"
+#include "var_subst.h"
 
 class counter {
 protected:
     typedef u_map<int> map_impl;
     map_impl m_data;
-    const bool m_stay_non_negative;
 public:
     typedef map_impl::iterator iterator;
     
-    counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
+    counter() {}
     
     void reset() { m_data.reset(); }
     iterator begin() const { return m_data.begin(); }
@@ -69,14 +69,13 @@ public:
 
 class var_counter : public counter {
 protected:
-    ptr_vector<sort> m_sorts;
     expr_fast_mark1  m_visited;
+    expr_free_vars   m_fv;
     ptr_vector<expr> m_todo;
-    ast_mark         m_mark;
     unsigned_vector  m_scopes;
     unsigned get_max_var(bool & has_var);    
 public:
-    var_counter(bool stay_non_negative = true): counter(stay_non_negative) {}
+    var_counter() {}
     void count_vars(ast_manager & m, const app * t, int coef = 1);
     unsigned get_max_var(expr* e);
     unsigned get_next_var(expr* e);
@@ -85,11 +84,10 @@ public:
 class ast_counter {
     typedef obj_map<ast, int> map_impl;
     map_impl m_data;
-    bool     m_stay_non_negative;
  public:
     typedef map_impl::iterator iterator;
     
-    ast_counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
+    ast_counter() {}
     
     iterator begin() const { return m_data.begin(); }
     iterator end() const { return m_data.end(); }
@@ -99,7 +97,6 @@ class ast_counter {
     }
     void update(ast * el, int delta){
         get(el) += delta;
-        SASSERT(!m_stay_non_negative || get(el) >= 0);
     }
     
     void inc(ast * el) { update(el, 1); }
diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp
index 930267dad..1d01ef85c 100644
--- a/src/ast/rewriter/var_subst.cpp
+++ b/src/ast/rewriter/var_subst.cpp
@@ -164,7 +164,7 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref
           tout << "\n----->\n" << mk_ismt2_pp(result, m) << "\n";);
 }
 
-static void get_free_vars_offset(ast_mark& mark, ptr_vector<expr>& todo, unsigned offset, expr* e, ptr_vector<sort>& sorts) {
+static void get_free_vars_offset(expr_sparse_mark& mark, ptr_vector<expr>& todo, unsigned offset, expr* e, ptr_vector<sort>& sorts) {
     todo.push_back(e);
     while (!todo.empty()) {
         e = todo.back();
@@ -176,7 +176,7 @@ static void get_free_vars_offset(ast_mark& mark, ptr_vector<expr>& todo, unsigne
         switch(e->get_kind()) {
         case AST_QUANTIFIER: {
             quantifier* q = to_quantifier(e);
-            ast_mark mark1;
+            expr_sparse_mark mark1;
             ptr_vector<expr> todo1;
             get_free_vars_offset(mark1, todo1, offset+q->get_num_decls(), q->get_expr(), sorts);
             break;
@@ -210,11 +210,33 @@ static void get_free_vars_offset(ast_mark& mark, ptr_vector<expr>& todo, unsigne
 
 
 void get_free_vars(expr* e, ptr_vector<sort>& sorts) {
-    ast_mark mark;
+    expr_sparse_mark mark;
     ptr_vector<expr> todo;
     get_free_vars_offset(mark, todo, 0, e, sorts);
 }
 
-void get_free_vars(ast_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts) {
+void get_free_vars(expr_sparse_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts) {
     get_free_vars_offset(mark, todo, 0, e, sorts);
 }
+
+void expr_free_vars::reset() {
+    m_mark.reset();
+    m_sorts.reset();
+    SASSERT(m_todo.empty());
+}
+
+void expr_free_vars::set_default_sort(sort *s) {
+    for (unsigned i = 0; i < m_sorts.size(); ++i) {
+        if (!m_sorts[i]) m_sorts[i] = s;
+    }
+}
+
+void expr_free_vars::operator()(expr* e) {
+    reset();
+    get_free_vars_offset(m_mark, m_todo, 0, e, m_sorts);
+}
+
+void expr_free_vars::accumulate(expr* e) {
+    SASSERT(m_todo.empty());
+    get_free_vars_offset(m_mark, m_todo, 0, e, m_sorts);
+}
diff --git a/src/ast/rewriter/var_subst.h b/src/ast/rewriter/var_subst.h
index ffc21e691..7db756d30 100644
--- a/src/ast/rewriter/var_subst.h
+++ b/src/ast/rewriter/var_subst.h
@@ -81,9 +81,23 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref
 
    Return the sorts of the free variables.
 */
-void get_free_vars(expr* e, ptr_vector<sort>& sorts);
 
-void get_free_vars(ast_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts);
+class expr_free_vars {
+    expr_sparse_mark m_mark;
+    ptr_vector<sort> m_sorts;
+    ptr_vector<expr> m_todo;
+public:    
+    void reset();
+    void operator()(expr* e);
+    void accumulate(expr* e);
+    bool empty() const { return m_sorts.empty(); }
+    unsigned size() const { return m_sorts.size(); }
+    sort* operator[](unsigned idx) const { return m_sorts[idx]; }
+    bool contains(unsigned idx) const { return idx < m_sorts.size() && m_sorts[idx] != 0; }
+    void set_default_sort(sort* s);
+    void reverse() { m_sorts.reverse(); }
+    sort*const* c_ptr() const { return m_sorts.c_ptr(); }  
+};
 
 #endif
 
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 529028606..d37e9cca8 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -334,21 +334,13 @@ namespace datalog {
         else {
             m_names.reset();
             m_abstractor(0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
-            rm.collect_vars(result);
-            ptr_vector<sort>& sorts = rm.get_var_sorts();
-            if (sorts.empty()) {
+            m_free_vars(result);
+            if (m_free_vars.empty()) {
                 result = fml;
             }
             else {
-                for (unsigned i = 0; i < sorts.size(); ++i) {
-                    if (!sorts[i]) {
-                        if (i < vars.size()) { 
-                            sorts[i] = vars[i]->get_decl()->get_range();
-                        }
-                        else {
-                            sorts[i] = m.mk_bool_sort();
-                        }
-                    }
+                m_free_vars.set_default_sort(m.mk_bool_sort());
+                for (unsigned i = 0; i < m_free_vars.size(); ++i) {
                     if (i < vars.size()) {
                         m_names.push_back(vars[i]->get_decl()->get_name());
                     }
@@ -357,8 +349,8 @@ namespace datalog {
                     }
                 }
                 quantifier_ref q(m);
-                sorts.reverse();
-                q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), m_names.c_ptr(), result); 
+                m_free_vars.reverse();
+                q = m.mk_quantifier(is_forall, m_free_vars.size(), m_free_vars.c_ptr(), m_names.c_ptr(), result); 
                 m_elim_unused_vars(q, result);
             }
         }
@@ -604,7 +596,7 @@ namespace datalog {
         unsigned ut_size = r.get_uninterpreted_tail_size();
         unsigned t_size  = r.get_tail_size();   
         
-        TRACE("dl", r.display_smt2(get_manager(), tout); tout << "\n";);
+        TRACE("dl", get_rule_manager().display_smt2(r, tout); tout << "\n";);
         for (unsigned i = ut_size; i < t_size; ++i) {
             app* t = r.get_tail(i);
             TRACE("dl", tout << "checking: " << mk_ismt2_pp(t, get_manager()) << "\n";);
@@ -1121,13 +1113,13 @@ namespace datalog {
 
     void context::get_rules_as_formulas(expr_ref_vector& rules, expr_ref_vector& queries, svector<symbol>& names) {
         expr_ref fml(m);
-        datalog::rule_manager& rm = get_rule_manager();
+        rule_manager& rm = get_rule_manager();
         
         // ensure that rules are all using bound variables.
         for (unsigned i = m_rule_fmls_head; i < m_rule_fmls.size(); ++i) {
             ptr_vector<sort> sorts;
-            get_free_vars(m_rule_fmls[i].get(), sorts);
-            if (!sorts.empty()) {
+            m_free_vars(m_rule_fmls[i].get());
+            if (!m_free_vars.empty()) {
                 rm.mk_rule(m_rule_fmls[i].get(), 0, m_rule_set, m_rule_names[i]);
                 m_rule_fmls[i] = m_rule_fmls.back();
                 m_rule_names[i] = m_rule_names.back();
@@ -1139,7 +1131,7 @@ namespace datalog {
         rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
         for (; it != end; ++it) {
             rule* r = *it;
-            r->to_formula(fml);
+            rm.to_formula(*r, fml);
             func_decl* h = r->get_decl();
             if (m_rule_set.is_output_predicate(h)) {
                 expr* body = fml;
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 66addc37c..fb49f02bc 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -191,6 +191,7 @@ namespace datalog {
         pred2syms          m_argument_var_names;
         rule_set           m_rule_set;
         rule_set           m_transformed_rule_set;
+        expr_free_vars     m_free_vars;
         unsigned           m_rule_fmls_head;
         expr_ref_vector    m_rule_fmls;
         svector<symbol>    m_rule_names;
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 017bac724..6296717da 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -111,16 +111,14 @@ namespace datalog {
     }
 
     void rule_manager::reset_collect_vars() {
-        m_vars.reset();
         m_var_idx.reset();
-        m_todo.reset();
-        m_mark.reset();
+        m_free_vars.reset();
     }
 
     var_idx_set& rule_manager::finalize_collect_vars() {
-        unsigned sz = m_vars.size();
-        for (unsigned i=0; i<sz; ++i) {
-            if (m_vars[i]) m_var_idx.insert(i); 
+        unsigned sz = m_free_vars.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            if (m_free_vars[i]) m_var_idx.insert(i); 
         }
         return m_var_idx;
     }
@@ -157,7 +155,7 @@ namespace datalog {
     }
 
     void rule_manager::accumulate_vars(expr* e) {
-        ::get_free_vars(m_mark, m_todo, e, m_vars);
+        m_free_vars.accumulate(e);
     }
 
 
@@ -188,8 +186,6 @@ namespace datalog {
     }
 
     void rule_manager::mk_rule_core(expr* fml, proof* p, rule_set& rules, symbol const& name) {
-        DEBUG_CODE(ptr_vector<sort> sorts; 
-                   ::get_free_vars(fml, sorts); );
         expr_ref_vector fmls(m);
         proof_ref_vector prs(m);
         m_hnf.reset();
@@ -200,8 +196,6 @@ namespace datalog {
             m_ctx.register_predicate(m_hnf.get_fresh_predicates()[i], false);
         }
         for (unsigned i = 0; i < fmls.size(); ++i) {
-            DEBUG_CODE(ptr_vector<sort> sorts; 
-                       ::get_free_vars(fmls[i].get(), sorts); );
             mk_horn_rule(fmls[i].get(), prs[i].get(), rules, name);
         }
     }
@@ -228,7 +222,7 @@ namespace datalog {
 
         expr_ref fml1(m);
         if (p) {
-            r->to_formula(fml1);
+            to_formula(*r, fml1);
             if (fml1 == fml) {
                 // no-op.
             }
@@ -246,7 +240,7 @@ namespace datalog {
 
         if (p) {
             expr_ref fml2(m);
-            r->to_formula(fml2);
+            to_formula(*r, fml2);
             if (fml1 != fml2) {
                 p = m.mk_modus_ponens(p, m.mk_rewrite(fml1, fml2));
             }
@@ -299,7 +293,8 @@ namespace datalog {
         quantifier_hoister qh(m);
         qh.pull_quantifier(false, q, 0, &names);
         // retrieve free variables.
-        get_free_vars(q, vars);
+        m_free_vars(q);
+        vars.append(m_free_vars.size(), m_free_vars.c_ptr());
         if (vars.contains(static_cast<sort*>(0))) {
             var_subst sub(m, false);  
             expr_ref_vector args(m);
@@ -316,7 +311,8 @@ namespace datalog {
             }
             sub(q, args.size(), args.c_ptr(), q);
             vars.reset();
-            get_free_vars(q, vars);
+            m_free_vars(q);
+            vars.append(m_free_vars.size(), m_free_vars.c_ptr());
         }
         SASSERT(!vars.contains(static_cast<sort*>(0)) && "Unused variables have been eliminated");
 
@@ -498,11 +494,6 @@ namespace datalog {
         app * * uninterp_tail = r->m_tail; //grows upwards
         app * * interp_tail = r->m_tail+n; //grows downwards
 
-        DEBUG_CODE(ptr_vector<sort> sorts; 
-                   ::get_free_vars(head, sorts);
-                   for (unsigned i = 0; i < n; ++i) {
-                       ::get_free_vars(tail[i], sorts);
-                   });
 
         bool has_neg = false;
 
@@ -556,11 +547,6 @@ namespace datalog {
         if (normalize) {
             r->norm_vars(*this);
         }
-        DEBUG_CODE(ptr_vector<sort> sorts; 
-                   ::get_free_vars(head, sorts);
-                   for (unsigned i = 0; i < n; ++i) {
-                       ::get_free_vars(tail[i], sorts);
-                   });
         return r;
     }
 
@@ -587,6 +573,55 @@ namespace datalog {
         return r;
     }
 
+    void rule_manager::to_formula(rule const& r, expr_ref& fml) {
+        ast_manager & m = fml.get_manager();
+        expr_ref_vector body(m);
+        for (unsigned i = 0; i < r.get_tail_size(); i++) {
+            body.push_back(r.get_tail(i));
+            if (r.is_neg_tail(i)) {
+                body[body.size()-1] = m.mk_not(body.back());
+            }
+        }
+        fml = r.get_head();
+        switch (body.size()) {
+        case 0:  break;
+        case 1:  fml = m.mk_implies(body[0].get(), fml); break;
+        default: fml = m.mk_implies(m.mk_and(body.size(), body.c_ptr()), fml); break;
+        }
+ 
+        m_free_vars(fml);
+        if (m_free_vars.empty()) {
+            return;
+        }
+        svector<symbol> names;
+        used_symbols<> us;
+        m_free_vars.set_default_sort(m.mk_bool_sort());
+               
+        us(fml);
+        m_free_vars.reverse();
+        for (unsigned j = 0, i = 0; i < m_free_vars.size(); ++j) {
+            for (char c = 'A'; i < m_free_vars.size() && c <= 'Z'; ++c) {
+                func_decl_ref f(m);
+                std::stringstream _name;
+                _name << c;
+                if (j > 0) _name << j;
+                symbol name(_name.str().c_str());
+                if (!us.contains(name)) {
+                    names.push_back(name);
+                    ++i;
+                }
+            }
+        }        
+        fml = m.mk_forall(m_free_vars.size(), m_free_vars.c_ptr(), names.c_ptr(), fml); 
+    }
+
+    std::ostream& rule_manager::display_smt2(rule const& r, std::ostream & out) {
+        expr_ref fml(m);
+        to_formula(r, fml);
+        return out << mk_ismt2_pp(fml, m);
+    }
+
+
     void rule_manager::reduce_unbound_vars(rule_ref& r) {
         unsigned ut_len = r->get_uninterpreted_tail_size();
         unsigned t_len = r->get_tail_size();
@@ -647,9 +682,7 @@ namespace datalog {
         svector<bool> tail_neg;
         app_ref head(r->get_head(), m);
 
-        collect_rule_vars(r);
         vctr.count_vars(m, head);
-        ptr_vector<sort>& free_rule_vars = m_vars;
 
         for (unsigned i = 0; i < ut_len; i++) {
             app * t = r->get_tail(i);
@@ -658,18 +691,16 @@ namespace datalog {
             tail_neg.push_back(r->is_neg_tail(i));
         }
 
-        ptr_vector<sort> interp_vars;
         var_idx_set unbound_vars;
         expr_ref_vector tails_with_unbound(m);
 
         for (unsigned i = ut_len; i < t_len; i++) {
             app * t = r->get_tail(i);
-            interp_vars.reset();
-            ::get_free_vars(t, interp_vars);
+            m_free_vars(t);
             bool has_unbound = false;
-            unsigned iv_size = interp_vars.size();
+            unsigned iv_size = m_free_vars.size();
             for (unsigned i=0; i<iv_size; i++) {
-                if (!interp_vars[i]) { continue; }
+                if (!m_free_vars[i]) { continue; }
                 if (vctr.get(i)==0) {
                     has_unbound = true;
                     unbound_vars.insert(i);
@@ -693,16 +724,15 @@ namespace datalog {
         bool_rewriter(m).mk_and(tails_with_unbound.size(), tails_with_unbound.c_ptr(), unbound_tail);
 
         unsigned q_var_cnt = unbound_vars.num_elems();
-        unsigned max_var = m_counter.get_max_rule_var(*r);
 
+        collect_rule_vars(r);
         expr_ref_vector subst(m);
-
         ptr_vector<sort> qsorts;
         qsorts.resize(q_var_cnt);
 
         unsigned q_idx = 0;
-        for (unsigned v = 0; v <= max_var; ++v) {
-            sort * v_sort = free_rule_vars[v];
+        for (unsigned v = 0; v < m_free_vars.size(); ++v) {
+            sort * v_sort = m_free_vars[v];
             if (!v_sort) {
                 //this variable index is not used
                 continue;
@@ -780,7 +810,7 @@ namespace datalog {
             !new_rule.get_proof() &&
             old_rule.get_proof()) {
             expr_ref fml(m);
-            new_rule.to_formula(fml);
+            to_formula(new_rule, fml);
             scoped_proof _sc(m);
             proof* p = m.mk_rewrite(m.get_fact(old_rule.get_proof()), fml);
             new_rule.set_proof(m, m.mk_modus_ponens(old_rule.get_proof(), p)); 
@@ -791,7 +821,7 @@ namespace datalog {
         if (m_ctx.generate_proof_trace()) {
             scoped_proof _scp(m);
             expr_ref fml(m);
-            r.to_formula(fml);
+            to_formula(r, fml);
             r.set_proof(m, m.mk_asserted(fml));
         }
     }
@@ -1066,57 +1096,6 @@ namespace datalog {
         }
     }
 
-    void rule::to_formula(expr_ref& fml) const {
-        ast_manager & m = fml.get_manager();
-        expr_ref_vector body(m);
-        for (unsigned i = 0; i < m_tail_size; i++) {
-            body.push_back(get_tail(i));
-            if (is_neg_tail(i)) {
-                body[body.size()-1] = m.mk_not(body.back());
-            }
-        }
-        switch(body.size()) {
-        case 0:  fml = m_head; break;
-        case 1:  fml = m.mk_implies(body[0].get(), m_head); break;
-        default: fml = m.mk_implies(m.mk_and(body.size(), body.c_ptr()), m_head); break;
-        }
- 
-        ptr_vector<sort> sorts;
-        get_free_vars(fml, sorts);        
-        if (sorts.empty()) {
-            return;
-        }
-        svector<symbol> names;
-        used_symbols<> us;
-        for (unsigned i = 0; i < sorts.size(); ++i) {
-            if (!sorts[i]) {
-                sorts[i] = m.mk_bool_sort();
-            }
-        }
-               
-        us(fml);
-        sorts.reverse();
-        for (unsigned j = 0, i = 0; i < sorts.size(); ++j) {
-            for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) {
-                func_decl_ref f(m);
-                std::stringstream _name;
-                _name << c;
-                if (j > 0) _name << j;
-                symbol name(_name.str().c_str());
-                if (!us.contains(name)) {
-                    names.push_back(name);
-                    ++i;
-                }
-            }
-        }        
-        fml = m.mk_forall(sorts.size(), sorts.c_ptr(), names.c_ptr(), fml); 
-    }
-
-    std::ostream& rule::display_smt2(ast_manager& m, std::ostream & out) const {
-        expr_ref fml(m);
-        to_formula(fml);
-        return out << mk_ismt2_pp(fml, m);
-    }
 
     bool rule_eq_proc::operator()(const rule * r1, const rule * r2) const {
         if (r1->get_head()!=r2->get_head()) { return false; }
diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h
index 7104bae1f..e90edefa1 100644
--- a/src/muz/base/dl_rule.h
+++ b/src/muz/base/dl_rule.h
@@ -30,6 +30,7 @@ Revision History:
 #include"rewriter.h"
 #include"hnf.h"
 #include"qe_lite.h"
+#include"var_subst.h"
 
 namespace datalog {
 
@@ -64,10 +65,8 @@ namespace datalog {
         context&             m_ctx;
         rule_counter         m_counter;
         used_vars            m_used;
-        ptr_vector<sort>     m_vars;
         var_idx_set          m_var_idx;
-        ptr_vector<expr>     m_todo;
-        ast_mark             m_mark;
+        expr_free_vars       m_free_vars;
         app_ref_vector       m_body;
         app_ref              m_head;
         expr_ref_vector      m_args;
@@ -143,7 +142,7 @@ namespace datalog {
 
         void accumulate_vars(expr* pred);
 
-        ptr_vector<sort>& get_var_sorts() { return m_vars; }
+        // ptr_vector<sort>& get_var_sorts() { return m_vars; }
 
         var_idx_set&      get_var_idx() { return m_var_idx; }
 
@@ -213,11 +212,14 @@ namespace datalog {
         */
         bool is_fact(app * head) const;
 
-
         static bool is_forall(ast_manager& m, expr* e, quantifier*& q);
 
         rule_counter& get_counter() { return m_counter; }
 
+        void to_formula(rule const& r, expr_ref& result);
+
+        std::ostream& display_smt2(rule const& r, std::ostream & out);
+
     };
 
     class rule : public accounted_object {
@@ -306,12 +308,8 @@ namespace datalog {
 
         void get_vars(ast_manager& m, ptr_vector<sort>& sorts) const;
 
-        void to_formula(expr_ref& result) const;
-
         void display(context & ctx, std::ostream & out) const;
 
-        std::ostream& display_smt2(ast_manager& m, std::ostream & out) const;
-
         symbol const& name() const { return m_name; }
 
         unsigned hash() const;
diff --git a/src/muz/base/dl_rule_set.h b/src/muz/base/dl_rule_set.h
index c1fc7ea3f..e13d92105 100644
--- a/src/muz/base/dl_rule_set.h
+++ b/src/muz/base/dl_rule_set.h
@@ -39,10 +39,10 @@ namespace datalog {
            Each master object is also present as a key of the map, even if its master set
            is empty.
         */
-        deps_type m_data;
-        context & m_context;
+        deps_type        m_data;
+        context &        m_context;
         ptr_vector<expr> m_todo;
-        ast_mark         m_visited;
+        expr_sparse_mark m_visited;
 
 
         //we need to take care with removing to avoid memory leaks
diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index a6647a1d2..2f60ddec8 100644
--- a/src/muz/base/dl_util.cpp
+++ b/src/muz/base/dl_util.cpp
@@ -56,9 +56,9 @@ namespace datalog {
 
 
     bool contains_var(expr * trm, unsigned var_idx) {
-        ptr_vector<sort> vars;
-        ::get_free_vars(trm, vars);
-        return var_idx < vars.size() && vars[var_idx] != 0;
+        expr_free_vars fv;
+        fv(trm);
+        return fv.contains(var_idx);
     }
     
     unsigned count_variable_arguments(app * pred)
@@ -300,14 +300,15 @@ namespace datalog {
     }
 
 
-    void resolve_rule(replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx, 
+    void resolve_rule(rule_manager& rm,
+                      replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx, 
                       expr_ref_vector const& s1, expr_ref_vector const& s2, rule const& res) {
         if (!pc) return;
         ast_manager& m = s1.get_manager();
         expr_ref fml1(m), fml2(m), fml3(m);
-        r1.to_formula(fml1);
-        r2.to_formula(fml2);
-        res.to_formula(fml3);
+        rm.to_formula(r1, fml1);
+        rm.to_formula(r2, fml2);
+        rm.to_formula(res, fml3);
         vector<expr_ref_vector> substs;
         svector<std::pair<unsigned, unsigned> > positions;
         substs.push_back(s1);
@@ -337,7 +338,7 @@ namespace datalog {
         pc->insert(pr);
     }
 
-    void resolve_rule(rule const& r1, rule const& r2, unsigned idx, 
+    void resolve_rule(rule_manager& rm, rule const& r1, rule const& r2, unsigned idx, 
                       expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res) {
         if (!r1.get_proof()) {
             return;
@@ -345,7 +346,7 @@ namespace datalog {
         SASSERT(r2.get_proof());
         ast_manager& m = s1.get_manager();
         expr_ref fml(m);
-        res.to_formula(fml);
+        rm.to_formula(res, fml);
         vector<expr_ref_vector> substs;
         svector<std::pair<unsigned, unsigned> > positions;
         substs.push_back(s1);
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index e3ba4b1cd..bf5c225ef 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -41,6 +41,7 @@ namespace datalog {
     class pentagon_relation;
     class relation_fact;
     class relation_signature;
+    class rule_manager;
 
     class verbose_action {
         unsigned  m_lvl;
@@ -345,17 +346,19 @@ namespace datalog {
 
     class rule_counter : public var_counter {        
     public:
-        rule_counter(bool stay_non_negative = true): var_counter(stay_non_negative) {}
+        rule_counter(){}
         void count_rule_vars(ast_manager & m, const rule * r, int coef = 1);
         unsigned get_max_rule_var(const rule& r);
     };
 
     void del_rule(horn_subsume_model_converter* mc, rule& r);
 
-    void resolve_rule(replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx, 
+    void resolve_rule(rule_manager& rm,
+                      replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx, 
                       expr_ref_vector const& s1, expr_ref_vector const& s2, rule const& res);
 
-    void resolve_rule(rule const& r1, rule const& r2, unsigned idx, 
+    void resolve_rule(rule_manager& rm, 
+                      rule const& r1, rule const& r2, unsigned idx, 
                       expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res);
 
     model_converter* mk_skip_model_converter();
diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp
index 90f5ad352..c30ca8b0e 100644
--- a/src/muz/base/hnf.cpp
+++ b/src/muz/base/hnf.cpp
@@ -87,6 +87,7 @@ class hnf::imp {
     expr_ref_vector       m_body;
     proof_ref_vector      m_defs;
     contains_predicate_proc m_proc;
+    expr_free_vars        m_free_vars;
 
 
 public:
@@ -350,13 +351,13 @@ private:
     }
 
     app_ref mk_fresh_head(expr* e) {
-        ptr_vector<sort> sorts0, sorts1;
-        get_free_vars(e, sorts0);
+        ptr_vector<sort> sorts1;
+        m_free_vars(e);
         expr_ref_vector args(m);
-        for (unsigned i = 0; i < sorts0.size(); ++i) {
-            if (sorts0[i]) {
-                args.push_back(m.mk_var(i, sorts0[i]));
-                sorts1.push_back(sorts0[i]);
+        for (unsigned i = 0; i < m_free_vars.size(); ++i) {
+            if (m_free_vars[i]) {
+                args.push_back(m.mk_var(i, m_free_vars[i]));
+                sorts1.push_back(m_free_vars[i]);
             }
         }
         func_decl_ref f(m);
diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index 2ad5b3b94..1d1a59e5f 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -297,7 +297,7 @@ namespace datalog {
                 vector<expr_ref_vector> substs;
                 expr_ref fml(m), concl(m);
                 
-                r->to_formula(fml);
+                rm.to_formula(*r, fml);
                 r2 = r;
                 rm.substitute(r2, sub.size(), sub.c_ptr());
                 proof_ref p(m);
@@ -307,7 +307,7 @@ namespace datalog {
                     expr_ref_vector sub2 = unifier.get_rule_subst(*r2.get(), false);
                     apply_subst(sub, sub2);
                     unifier.apply(*r0.get(), 0, *r2.get(), r1);
-                    r1->to_formula(concl);
+                    rm.to_formula(*r1.get(), concl);
                     scoped_proof _sp(m);
                     
                     p = r->get_proof();
@@ -324,7 +324,7 @@ namespace datalog {
                     r0 = r1;
                 }
                 else {
-                    r2->to_formula(concl);
+                    rm.to_formula(*r, concl);
                     scoped_proof _sp(m);
                     p = r->get_proof();
                     if (!p) {
@@ -488,7 +488,7 @@ namespace datalog {
                 return proof_ref(0, m);
             }
             TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";);
-
+            rule_manager& rm = b.m_ctx.get_rule_manager();
             expr_ref prop_r(m), prop_v(m), fml(m), prop_body(m), tmp(m), body(m);
             expr_ref_vector args(m);
             proof_ref_vector prs(m);
@@ -508,7 +508,7 @@ namespace datalog {
                 }
             }
             SASSERT(r);
-            r->to_formula(fml);
+            rm.to_formula(*r, fml);
             IF_VERBOSE(1, verbose_stream() << mk_pp(fml, m) << "\n";);
             prs.push_back(r->get_proof());
             unsigned sz = r->get_uninterpreted_tail_size();
@@ -624,11 +624,12 @@ namespace datalog {
         }
 
         expr_ref bind_vars(expr* e, expr* pat) {
-            ptr_vector<sort> vars, sorts;
+            ptr_vector<sort> sorts;
             svector<symbol> names;
             expr_ref_vector binding(m), patterns(m);
             expr_ref tmp(m), head(m);
-            get_free_vars(e, vars);
+            expr_free_vars vars;
+            vars(e);
             for (unsigned i = 0; i < vars.size(); ++i) {
                 if (vars[i]) {
                     binding.push_back(m.mk_var(sorts.size(), vars[i]));
@@ -1028,6 +1029,7 @@ namespace datalog {
         
         proof_ref get_proof(model_ref& md, app* trace, app* path) {
             datatype_util dtu(m);
+            rule_manager& rm = b.m_ctx.get_rule_manager();
             sort* trace_sort = m.get_sort(trace);
             func_decl* p = m_sort2pred.find(trace_sort);
             datalog::rule_vector const& rules = b.m_rules.get_predicate_rules(p);
@@ -1046,7 +1048,7 @@ namespace datalog {
                     
                     var_subst vs(m, false);
                     mk_subst(*rules[i], path, trace, sub);
-                    rules[i]->to_formula(fml);
+                    rm.to_formula(*rules[i], fml);
                     prs.push_back(rules[i]->get_proof());
                     unsigned sz = trace->get_num_args();
                     if (sub.empty() && sz == 0) {
@@ -1219,7 +1221,7 @@ namespace datalog {
                 vector<expr_ref_vector> substs;
                 expr_ref fml(m), concl(m);
                 
-                r->to_formula(fml);
+                rm.to_formula(*r, fml);
                 r2 = r;
                 rm.substitute(r2, sub.size(), sub.c_ptr());
                 proof_ref p(m);
@@ -1237,7 +1239,7 @@ namespace datalog {
                     expr_ref_vector sub2 = unifier.get_rule_subst(*r2.get(), false);
                     apply_subst(sub, sub2);
                     unifier.apply(*r0.get(), 0, *r2.get(), r1);
-                    r1->to_formula(concl);
+                    rm.to_formula(*r1.get(), concl);
                     
                     scoped_proof _sp(m);
                     proof* premises[2] = { pr, p };
@@ -1250,7 +1252,7 @@ namespace datalog {
                     r0 = r1;
                 }
                 else {
-                    r2->to_formula(concl);
+                    rm.to_formula(*r2.get(), concl);
                     scoped_proof _sp(m);
                     if (sub.empty()) {
                         pr = p;
diff --git a/src/muz/clp/clp_context.cpp b/src/muz/clp/clp_context.cpp
index 0cd08e5b3..2c66c3cd5 100644
--- a/src/muz/clp/clp_context.cpp
+++ b/src/muz/clp/clp_context.cpp
@@ -123,14 +123,14 @@ namespace datalog {
         }
         
         void ground(expr_ref& e) {
-            ptr_vector<sort> sorts;
-            get_free_vars(e, sorts);
-            if (m_ground.size() < sorts.size()) {
-                m_ground.resize(sorts.size());
+            expr_free_vars fv;
+            fv(e);
+            if (m_ground.size() < fv.size()) {
+                m_ground.resize(fv.size());
             }
-            for (unsigned i = 0; i < sorts.size(); ++i) {
-                if (sorts[i] && !m_ground[i].get()) {
-                    m_ground[i] = m.mk_fresh_const("c",sorts[i]);
+            for (unsigned i = 0; i < fv.size(); ++i) {
+                if (fv[i] && !m_ground[i].get()) {
+                    m_ground[i] = m.mk_fresh_const("c", fv[i]);
                 }
             }
             m_var_subst(e, m_ground.size(), m_ground.c_ptr(), e);
diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp
index 6d5dd1c80..db2981f45 100644
--- a/src/muz/ddnf/ddnf.cpp
+++ b/src/muz/ddnf/ddnf.cpp
@@ -516,13 +516,15 @@ namespace datalog {
             rule_set& old_rules = m_ctx.get_rules();
             rm.mk_query(query, old_rules);
             rule_set new_rules(m_ctx);
+            IF_VERBOSE(10, verbose_stream() << "(ddnf.preprocess)\n";);
             if (!pre_process_rules(old_rules)) {
                 return l_undef;
             }
+            IF_VERBOSE(10, verbose_stream() << "(ddnf.compile)\n";);
             if (!compile_rules1(old_rules, new_rules)) {
                 return l_undef;
             }
-            IF_VERBOSE(2, m_ddnfs.display(verbose_stream()););
+            IF_VERBOSE(15, m_ddnfs.display(verbose_stream()););
 
             dump_rules(new_rules);
             return l_undef;
@@ -728,7 +730,7 @@ namespace datalog {
             }
             rule* r_new = rm.mk(head, body.size(), body.c_ptr(), 0, r.name(), false);
             new_rules.add_rule(r_new);
-            IF_VERBOSE(2, r_new->display(m_ctx, verbose_stream()););
+            IF_VERBOSE(20, r_new->display(m_ctx, verbose_stream()););
             if (old_rules.is_output_predicate(r.get_decl())) {
                 new_rules.set_output_predicate(r_new->get_decl());
             }
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index 827b90e60..9807cec4a 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -226,6 +226,7 @@ public:
         bool query_exn = false;
         lbool status = l_undef;
         {
+            IF_VERBOSE(10, verbose_stream() << "(query)\n";);
             scoped_ctrl_c ctrlc(eh);
             scoped_timer timer(timeout, &eh);
             cmd_context::scoped_watch sw(ctx);
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index 1e7a6e617..a1c556baf 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -334,7 +334,7 @@ class horn_tactic : public tactic {
             datalog::rule_set::iterator it = rules.begin(), end = rules.end();
             for (; it != end; ++it) {
                 datalog::rule* r = *it;
-                r->to_formula(fml);
+                m_ctx.get_rule_manager().to_formula(*r, fml);
                 (*rep)(fml);
                 g->assert_expr(fml);
             }
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 00e6c0336..722661e38 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -97,8 +97,9 @@ namespace pdr {
 
     std::ostream& pred_transformer::display(std::ostream& out) const {
         if (!rules().empty()) out << "rules\n";
+        datalog::rule_manager& rm = ctx.get_context().get_rule_manager();
         for (unsigned i = 0; i < rules().size(); ++i) {
-            rules()[i]->display_smt2(m, out) << "\n";
+            rm.display_smt2(*rules()[i], out) << "\n";
         }        
         out << "transition\n" << mk_pp(transition(), m) << "\n";
         return out;
@@ -149,12 +150,13 @@ namespace pdr {
     }
 
     datalog::rule const& pred_transformer::find_rule(model_core const& model) const {
+        datalog::rule_manager& rm = ctx.get_context().get_rule_manager();
         obj_map<expr, datalog::rule const*>::iterator it = m_tag2rule.begin(), end = m_tag2rule.end();
         TRACE("pdr_verbose",
               for (; it != end; ++it) {
                   expr* pred = it->m_key;
                   tout << mk_pp(pred, m) << ":\n";
-                  if (it->m_value) it->m_value->display_smt2(m, tout) << "\n";                  
+                  if (it->m_value) rm.display_smt2(*it->m_value, tout) << "\n";                  
               }
         );
         
@@ -639,14 +641,14 @@ namespace pdr {
 
     // create constants for free variables in tail.
     void pred_transformer::ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars) {
-        ptr_vector<sort> sorts;
-        get_free_vars(e, sorts);
-        while (vars.size() < sorts.size()) {
+        expr_free_vars fv;
+        fv(e);
+        while (vars.size() < fv.size()) {
             vars.push_back(0);
         }
-        for (unsigned i = 0; i < sorts.size(); ++i) {
-            if (sorts[i] && !vars[i].get()) {
-                vars[i] = m.mk_fresh_const("aux", sorts[i]);
+        for (unsigned i = 0; i < fv.size(); ++i) {
+            if (fv[i] && !vars[i].get()) {
+                vars[i] = m.mk_fresh_const("aux", fv[i]);
                 aux_vars.push_back(vars[i].get());
             }
         }
@@ -1226,7 +1228,7 @@ namespace pdr {
                 }
 
                 expr_ref fml_concl(m);
-                reduced_rule->to_formula(fml_concl);                    
+                rm.to_formula(*reduced_rule.get(), fml_concl);                    
                 p1 = m.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs);
 
             }
@@ -1558,6 +1560,7 @@ namespace pdr {
         ex.to_model(model);
         decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
         var_subst vs(m, false);   
+        expr_free_vars fv;
         for (; it != end; ++it) {
             ptr_vector<datalog::rule> const& rules = it->m_value->rules();
             for (unsigned i = 0; i < rules.size(); ++i) {
@@ -1575,18 +1578,15 @@ namespace pdr {
                     fmls.push_back(r.get_tail(j));
                 }
                 tmp = m.mk_and(fmls.size(), fmls.c_ptr()); 
-                ptr_vector<sort> sorts;
                 svector<symbol> names;
-                get_free_vars(tmp, sorts);
-                for (unsigned i = 0; i < sorts.size(); ++i) {
-                    if (!sorts[i]) {
-                        sorts[i] = m.mk_bool_sort();
-                    }
+                fv(tmp);
+                fv.set_default_sort(m.mk_bool_sort());
+                for (unsigned i = 0; i < fv.size(); ++i) {
                     names.push_back(symbol(i));
                 }
-                sorts.reverse();
-                if (!sorts.empty()) {
-                    tmp = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp);
+                fv.reverse();
+                if (!fv.empty()) {
+                    tmp = m.mk_exists(fv.size(), fv.c_ptr(), names.c_ptr(), tmp);
                 }
                 smt::kernel solver(m, get_fparams());
                 solver.assert_expr(tmp);
diff --git a/src/muz/pdr/pdr_generalizers.cpp b/src/muz/pdr/pdr_generalizers.cpp
index 7c2557260..8b6f6a4c6 100644
--- a/src/muz/pdr/pdr_generalizers.cpp
+++ b/src/muz/pdr/pdr_generalizers.cpp
@@ -558,7 +558,6 @@ namespace pdr {
         {
             expr_ref_vector conj(m), sub(m);
             expr_ref result(m);
-            ptr_vector<sort> sorts;
             svector<symbol> names;
             unsigned ut_size = rule.get_uninterpreted_tail_size();
             unsigned t_size = rule.get_tail_size();              
@@ -599,16 +598,15 @@ namespace pdr {
                 expr_ref tmp = result;
                 var_subst(m, false)(tmp, sub.size(), sub.c_ptr(), result);
             }
-            get_free_vars(result, sorts);         
-            for (unsigned i = 0; i < sorts.size(); ++i) {
-                if (!sorts[i]) {
-                    sorts[i] = m.mk_bool_sort();
-                }
-                names.push_back(symbol(sorts.size() - i - 1));
+            expr_free_vars fv;
+            fv(result);
+            fv.set_default_sort(m.mk_bool_sort());
+            for (unsigned i = 0; i < fv.size(); ++i) {
+                names.push_back(symbol(fv.size() - i - 1));
             }
-            if (!sorts.empty()) {
-                sorts.reverse();
-                result = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), result); 
+            if (!fv.empty()) {
+                fv.reverse();
+                result = m.mk_exists(fv.size(), fv.c_ptr(), names.c_ptr(), result); 
             }            
             return result;
         }
diff --git a/src/muz/pdr/pdr_manager.cpp b/src/muz/pdr/pdr_manager.cpp
index bda54dbd7..c029d1b16 100644
--- a/src/muz/pdr/pdr_manager.cpp
+++ b/src/muz/pdr/pdr_manager.cpp
@@ -119,7 +119,7 @@ namespace pdr {
     }
 
     
-    void inductive_property::display(ptr_vector<datalog::rule> const& rules, std::ostream& out) const {
+    void inductive_property::display(datalog::rule_manager& rm, ptr_vector<datalog::rule> const& rules, std::ostream& out) const {
         func_decl_set bound_decls, aux_decls;
         collect_decls_proc collect_decls(bound_decls, aux_decls);
 
@@ -153,7 +153,7 @@ namespace pdr {
         for (unsigned i = 0; i < rules.size(); ++i) {
             out << "(push)\n";
             out << "(assert (not\n";
-            rules[i]->display_smt2(m, out);
+            rm.display_smt2(*rules[i], out);
             out << "))\n";
             out << "(check-sat)\n";
             out << "(pop)\n";
diff --git a/src/muz/pdr/pdr_manager.h b/src/muz/pdr/pdr_manager.h
index 0e8e890e8..f892e4d97 100644
--- a/src/muz/pdr/pdr_manager.h
+++ b/src/muz/pdr/pdr_manager.h
@@ -70,8 +70,8 @@ namespace pdr {
         expr_ref to_expr() const;
 
         void to_model(model_ref& md) const;
-
-        void display(ptr_vector<datalog::rule> const& rules, std::ostream& out) const;
+        
+        void display(datalog::rule_manager& rm, ptr_vector<datalog::rule> const& rules, std::ostream& out) const;
     };
 
     class manager
diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index 276e7b836..4f8be942d 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -184,7 +184,7 @@ namespace datalog {
         TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";);
             IF_VERBOSE(3, { 
                     expr_ref e(m_context.get_manager()); 
-                    compiled_rule->to_formula(e); 
+                    m_context.get_rule_manager().to_formula(*compiled_rule, e); 
                     verbose_stream() << "Compiling unsafe rule column " << col_idx << "\n" 
                                      << mk_ismt2_pp(e, m_context.get_manager()) << "\n"; 
                 });
@@ -641,14 +641,14 @@ namespace datalog {
         if (!tail.empty()) {
             app_ref filter_cond(tail.size() == 1 ? to_app(tail.back()) : m.mk_and(tail.size(), tail.c_ptr()), m);
             ptr_vector<sort> filter_vars;
-            get_free_vars(filter_cond, filter_vars);
+            m_free_vars(filter_cond);
 
             // create binding
             expr_ref_vector binding(m);
-            binding.resize(filter_vars.size()+1);
+            binding.resize(m_free_vars.size()+1);
             
-            for (unsigned v = 0; v < filter_vars.size(); ++v) {
-                if (!filter_vars[v])
+            for (unsigned v = 0; v < m_free_vars.size(); ++v) {
+                if (!m_free_vars[v])
                     continue;
 
                 int2ints::entry * entry = var_indexes.find_core(v);
@@ -657,7 +657,7 @@ namespace datalog {
                     src_col = entry->get_data().m_value.back();
                 } else {
                     // we have an unbound variable, so we add an unbound column for it
-                    relation_sort unbound_sort = filter_vars[v];
+                    relation_sort unbound_sort = m_free_vars[v];
 
                     reg_idx new_reg;
                     bool new_dealloc;
@@ -674,19 +674,18 @@ namespace datalog {
                     entry->get_data().m_value.push_back(src_col);
                 }
                 relation_sort var_sort = m_reg_signatures[filtered_res][src_col];
-                binding[filter_vars.size()-v] = m.mk_var(src_col, var_sort);
+                binding[m_free_vars.size()-v] = m.mk_var(src_col, var_sort);
             }
 
             // check if there are any columns to remove
             unsigned_vector remove_columns;
             {
                 unsigned_vector var_idx_to_remove;
-                ptr_vector<sort> vars;
-                get_free_vars(r->get_head(), vars);
+                m_free_vars(r->get_head());
                 for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end();
                     I != E; ++I) {
                     unsigned var_idx = I->m_key;
-                    if (!vars.get(var_idx, 0)) {
+                    if (!m_free_vars.contains(var_idx)) {
                         unsigned_vector & cols = I->m_value;
                         for (unsigned i = 0; i < cols.size(); ++i) {
                             remove_columns.push_back(cols[i]);
@@ -745,10 +744,9 @@ namespace datalog {
         unsigned ft_len=r->get_tail_size(); //full tail
         for(unsigned tail_index=ut_len; tail_index<ft_len; tail_index++) {
             app * t = r->get_tail(tail_index);
-            ptr_vector<sort> t_vars;
-            ::get_free_vars(t, t_vars);
+            m_free_vars(t);
             
-            if(t_vars.empty()) {
+            if (m_free_vars.empty()) {
                 expr_ref simplified(m);
                 m_context.get_rewriter()(t, simplified);
                 if(m.is_true(simplified)) {
@@ -761,23 +759,22 @@ namespace datalog {
             }
 
             //determine binding size
-            while (!t_vars.back()) {
-                t_vars.pop_back();
-            }
-            unsigned max_var = t_vars.size();
+            
+            unsigned max_var = m_free_vars.size();
+            while (max_var > 0 && !m_free_vars[max_var-1]) --max_var;
 
             //create binding
             expr_ref_vector binding(m);
-            binding.resize(max_var+1);
+            binding.resize(max_var);
             
-            for(unsigned v = 0; v < t_vars.size(); ++v) {
-                if (!t_vars[v]) {
+            for(unsigned v = 0; v < max_var; ++v) {
+                if (!m_free_vars[v]) {
                     continue;
                 }
                 int2ints::entry * e = var_indexes.find_core(v);
                 if(!e) {
                     //we have an unbound variable, so we add an unbound column for it
-                    relation_sort unbound_sort = t_vars[v];
+                    relation_sort unbound_sort = m_free_vars[v];
 
                     reg_idx new_reg;
                     TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";);
diff --git a/src/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h
index e0f9af424..92f50eb02 100644
--- a/src/muz/rel/dl_compiler.h
+++ b/src/muz/rel/dl_compiler.h
@@ -111,12 +111,13 @@ namespace datalog {
          */
         instruction_block & m_top_level_code;
         pred2idx m_pred_regs;
-        reg_idx m_new_reg;
-        vector<relation_signature> m_reg_signatures;
-        obj_pair_map<sort, app, reg_idx> m_constant_registers;
+        reg_idx                           m_new_reg;
+        vector<relation_signature>        m_reg_signatures;
+        obj_pair_map<sort, app, reg_idx>  m_constant_registers;
         obj_pair_map<sort, decl, reg_idx> m_total_registers;
-        obj_map<decl, reg_idx> m_empty_tables_registers;
-        instruction_observer m_instruction_observer;
+        obj_map<decl, reg_idx>            m_empty_tables_registers;
+        instruction_observer              m_instruction_observer;
+        expr_free_vars                    m_free_vars;
 
         /**
            If true, the union operation on the underlying structure only provides the information
diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp
index c2214dad9..e33de8c6d 100644
--- a/src/muz/rel/dl_mk_simple_joins.cpp
+++ b/src/muz/rel/dl_mk_simple_joins.cpp
@@ -326,7 +326,7 @@ namespace datalog {
             for(unsigned i=0; i<pos_tail_size; i++) {
                 rule_content.push_back(r->get_tail(i));
             }
-            for(unsigned i=0; i<pos_tail_size; i++) {
+            for(unsigned i=0; i+1 < pos_tail_size; i++) {
                 app * t1 = r->get_tail(i);
                 var_idx_set t1_vars = rm.collect_vars(t1);
                 counter.count_vars(m, t1, -1);  //temporarily remove t1 variables from counter
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 3c034ff0f..f5795df0c 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -1405,7 +1405,7 @@ namespace datalog {
         dl_decl_util & m_decl_util;
         th_rewriter & m_simp;
         app_ref m_condition;
-        ptr_vector<sort> m_var_sorts;
+        expr_free_vars m_free_vars;
         expr_ref_vector m_args;
     public:
         default_table_filter_interpreted_fn(context & ctx, unsigned col_cnt,  app* condition) 
@@ -1415,8 +1415,7 @@ namespace datalog {
                   m_simp(ctx.get_rewriter()),
                   m_condition(condition, ctx.get_manager()),
                   m_args(ctx.get_manager()) {
-            m_var_sorts.resize(col_cnt);
-            get_free_vars(m_condition, m_var_sorts);
+            m_free_vars(m_condition);
         }
 
         virtual bool should_remove(const table_fact & f) const {
@@ -1426,14 +1425,13 @@ namespace datalog {
             //arguments need to be in reverse order for the substitution
             unsigned col_cnt = f.size();
             for(int i=col_cnt-1;i>=0;i--) {
-                sort * var_sort = m_var_sorts[i];
-                if(!var_sort) {
+                if(!m_free_vars.contains(i)) {
                     args.push_back(0);
                     continue; //this variable does not occur in the condition;
                 }
 
                 table_element el = f[i];
-                args.push_back(m_decl_util.mk_numeral(el, var_sort));
+                args.push_back(m_decl_util.mk_numeral(el, m_free_vars[i]));
             }
 
             expr_ref ground(m_ast_manager);
diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp
index 83842a68b..d75ebe20e 100644
--- a/src/muz/tab/tab_context.cpp
+++ b/src/muz/tab/tab_context.cpp
@@ -216,11 +216,13 @@ namespace tb {
         }
 
         void get_free_vars(ptr_vector<sort>& vars) const {
-            ::get_free_vars(m_head, vars);
+            expr_free_vars fv;
+            fv(m_head);
             for (unsigned i = 0; i < m_predicates.size(); ++i) {
-                ::get_free_vars(m_predicates[i], vars);
+                fv.accumulate(m_predicates[i]);
             }
-            ::get_free_vars(m_constraint, vars);
+            fv.accumulate(m_constraint);
+            vars.append(fv.size(), fv.c_ptr());
         }
 
         expr_ref to_formula() const {
@@ -1107,16 +1109,16 @@ namespace tb {
             m_S1.apply(2, delta, expr_offset(tgt.get_constraint(), 0), tmp);
             m_S1.apply(2, delta, expr_offset(src.get_constraint(), 1), tmp2);
             constraint = m.mk_and(tmp, tmp2);            
-            ptr_vector<sort> vars;
 
             // perform trival quantifier-elimination:
             uint_set index_set;
-            get_free_vars(head, vars);
+            expr_free_vars fv;
+            fv(head);
             for (unsigned i = 0; i < predicates.size(); ++i) {
-                get_free_vars(predicates[i].get(), vars);
+                fv.accumulate(predicates[i].get());
             }
-            for (unsigned i = 0; i < vars.size(); ++i) {
-                if (vars[i]) {
+            for (unsigned i = 0; i < fv.size(); ++i) {
+                if (fv[i]) {
                     index_set.insert(i);
                 }
             }
@@ -1127,7 +1129,7 @@ namespace tb {
             
             // initialize rule.
             result->init(head, predicates, constraint);
-            vars.reset();
+            ptr_vector<sort> vars;
             result->get_free_vars(vars);
             bool change = false;
             var_ref w(m);
diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp
index 641d40779..fb860f2ac 100644
--- a/src/muz/transforms/dl_mk_array_blast.cpp
+++ b/src/muz/transforms/dl_mk_array_blast.cpp
@@ -294,7 +294,7 @@ namespace datalog {
         if (m_simplifier.transform_rule(new_rules.last(), new_rule)) {
             if (r.get_proof()) {
                 scoped_proof _sc(m);
-                r.to_formula(fml1);
+                rm.to_formula(r, fml1);
                 p = m.mk_rewrite(fml1, fml2);
                 p = m.mk_modus_ponens(r.get_proof(), p);
                 new_rule->set_proof(m, p);                
diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp
index fd1dbb205..fcd20d78f 100644
--- a/src/muz/transforms/dl_mk_bit_blast.cpp
+++ b/src/muz/transforms/dl_mk_bit_blast.cpp
@@ -225,7 +225,6 @@ namespace datalog {
         mk_interp_tail_simplifier m_simplifier;
         bit_blaster_rewriter m_blaster;
         expand_mkbv          m_rewriter;
-        
 
         bool blast(rule *r, expr_ref& fml) {
             proof_ref pr(m);
@@ -235,7 +234,7 @@ namespace datalog {
             if (!m_simplifier.transform_rule(r, r2)) {
                 r2 = r;
             }
-            r2->to_formula(fml1);
+            m_context.get_rule_manager().to_formula(*r2.get(), fml1);
             m_blaster(fml1, fml2, pr);
             m_rewriter(fml2, fml3);
             TRACE("dl", tout << mk_pp(fml, m) << " -> " << mk_pp(fml2, m) << " -> " << mk_pp(fml3, m) << "\n";);
@@ -274,7 +273,7 @@ namespace datalog {
             m_rewriter.m_cfg.set_dst(result);
             for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) {
                 rule * r = source.get_rule(i);
-                r->to_formula(fml);
+                rm.to_formula(*r, fml);
                 if (blast(r, fml)) {
                     proof_ref pr(m);
                     if (r->get_proof()) {
diff --git a/src/muz/transforms/dl_mk_coalesce.cpp b/src/muz/transforms/dl_mk_coalesce.cpp
index ac7a58d8d..7476a5655 100644
--- a/src/muz/transforms/dl_mk_coalesce.cpp
+++ b/src/muz/transforms/dl_mk_coalesce.cpp
@@ -134,9 +134,9 @@ namespace datalog {
         is_neg.push_back(false);
         res = rm.mk(head, tail.size(), tail.c_ptr(), is_neg.c_ptr(), tgt->name());
         if (m_ctx.generate_proof_trace()) {
-            src.to_formula(fml1);
-            tgt->to_formula(fml2);
-            res->to_formula(fml);
+            rm.to_formula(src, fml1);
+            rm.to_formula(*tgt.get(),fml2);
+            rm.to_formula(*res.get(),fml);
 #if 0
             sort* ps = m.mk_proof_sort();
             sort* domain[3] = { ps, ps, m.mk_bool_sort() };
diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
index fcb8d7b85..afb22e55f 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
@@ -238,7 +238,7 @@ namespace datalog {
             proof* p1 = r.get_proof();
             for (unsigned i = 0; i < added_rules.get_num_rules(); ++i) {
                 rule* r2 = added_rules.get_rule(i);
-                r2->to_formula(fml);
+                rm.to_formula(*r2, fml);
                 pr = m.mk_modus_ponens(m.mk_def_axiom(m.mk_implies(m.get_fact(p1), fml)), p1);
                 r2->set_proof(m, pr);
             }
diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp
index 366547575..d3eb24b9a 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.cpp
+++ b/src/muz/transforms/dl_mk_rule_inliner.cpp
@@ -179,7 +179,7 @@ namespace datalog {
             if (m_context.generate_proof_trace()) {
                 expr_ref_vector s1 = m_unifier.get_rule_subst(tgt, true);
                 expr_ref_vector s2 = m_unifier.get_rule_subst(src, false);
-                datalog::resolve_rule(tgt, src, tail_index, s1, s2, *res.get());
+                datalog::resolve_rule(m_rm, tgt, src, tail_index, s1, s2, *res.get());
             }
             return true;        
         }
diff --git a/src/muz/transforms/dl_mk_separate_negated_tails.cpp b/src/muz/transforms/dl_mk_separate_negated_tails.cpp
index 782e1011d..9a78c0d4d 100644
--- a/src/muz/transforms/dl_mk_separate_negated_tails.cpp
+++ b/src/muz/transforms/dl_mk_separate_negated_tails.cpp
@@ -37,10 +37,10 @@ namespace datalog {
     void mk_separate_negated_tails::get_private_vars(rule const& r, unsigned j) {
         m_vars.reset();
         m_fv.reset();
-        get_free_vars(r.get_head(), m_fv);
+        m_fv(r.get_head());
         for (unsigned i = 0; i < r.get_tail_size(); ++i) {
             if (i != j) {
-                get_free_vars(r.get_tail(i), m_fv);
+                m_fv.accumulate(r.get_tail(i));
             }
         }
         
@@ -49,7 +49,7 @@ namespace datalog {
             expr* v = p->get_arg(i);
             if (is_var(v)) {
                 unsigned idx = to_var(v)->get_idx();
-                if (idx >= m_fv.size() || !m_fv[idx]) {
+                if (!m_fv.contains(idx)) {
                     m_vars.push_back(v);
                 }
             }
diff --git a/src/muz/transforms/dl_mk_separate_negated_tails.h b/src/muz/transforms/dl_mk_separate_negated_tails.h
index 8cd806f43..03a52c997 100644
--- a/src/muz/transforms/dl_mk_separate_negated_tails.h
+++ b/src/muz/transforms/dl_mk_separate_negated_tails.h
@@ -42,7 +42,7 @@ namespace datalog {
         rule_manager& rm;
         context &     m_ctx;
         ptr_vector<expr> m_vars;
-        ptr_vector<sort> m_fv;
+        expr_free_vars   m_fv;
         
         bool has_private_vars(rule const& r, unsigned j);
         void get_private_vars(rule const& r, unsigned j);
diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp
index 0df75324d..f162d550f 100644
--- a/src/muz/transforms/dl_mk_slice.cpp
+++ b/src/muz/transforms/dl_mk_slice.cpp
@@ -120,7 +120,7 @@ namespace datalog {
             obj_map<rule, rule*>::iterator end = m_rule2slice.end();
             expr_ref fml(m);
             for (; it != end; ++it) {
-                it->m_value->to_formula(fml);
+                rm.to_formula(*it->m_value, fml);
                 m_pinned_exprs.push_back(fml);
                 TRACE("dl", 
                       tout << "orig: " << mk_pp(fml, m) << "\n";
@@ -238,7 +238,7 @@ namespace datalog {
                     r3->display(m_ctx, tout << "res:"););
                 r1 = r3;
             }
-            r1->to_formula(concl);
+            rm.to_formula(*r1.get(), concl);
             proof* new_p = m.mk_hyper_resolve(premises.size(), premises.c_ptr(), concl, positions, substs);
             m_pinned_exprs.push_back(new_p);
             m_pinned_rules.push_back(r1.get());
@@ -676,10 +676,10 @@ namespace datalog {
     }
 
     void mk_slice::add_free_vars(uint_set& result, expr* e) {
-        ptr_vector<sort> sorts;
-        get_free_vars(e, sorts);
-        for (unsigned i = 0; i < sorts.size(); ++i) {
-            if (sorts[i]) {
+        expr_free_vars fv;
+        fv(e);
+        for (unsigned i = 0; i < fv.size(); ++i) {
+            if (fv[i]) {
                 result.insert(i);
             }
         }
@@ -773,14 +773,11 @@ namespace datalog {
             init_vars(r);
             app_ref_vector tail(m);
             app_ref head(m);
-            ptr_vector<sort> sorts;
             update_predicate(r.get_head(), head);
-            get_free_vars(head.get(), sorts);
             for (unsigned i = 0; i < r.get_uninterpreted_tail_size(); ++i) {
                 app_ref t(m);
                 update_predicate(r.get_tail(i), t);
                 tail.push_back(t);
-                get_free_vars(t, sorts);
             }
             expr_ref_vector conjs = get_tail_conjs(r);
             
diff --git a/src/muz/transforms/dl_mk_unfold.cpp b/src/muz/transforms/dl_mk_unfold.cpp
index a9357f88a..cc460bca1 100644
--- a/src/muz/transforms/dl_mk_unfold.cpp
+++ b/src/muz/transforms/dl_mk_unfold.cpp
@@ -43,7 +43,7 @@ namespace datalog {
                     m_unify.apply(r, tail_idx, r2, new_rule)) {
                     expr_ref_vector s1 = m_unify.get_rule_subst(r, true);
                     expr_ref_vector s2 = m_unify.get_rule_subst(r2, false);                    
-                    resolve_rule(r, r2, tail_idx, s1, s2, *new_rule.get());
+                    resolve_rule(rm, r, r2, tail_idx, s1, s2, *new_rule.get());
                     expand_tail(*new_rule.get(), tail_idx+r2.get_uninterpreted_tail_size(), src, dst);
                 }
             }
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index e8fffd57e..17a1ccb1d 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -2271,17 +2271,14 @@ namespace qe {
 
 
     void expr_quant_elim::instantiate_expr(expr_ref_vector& bound, expr_ref& fml) {
-        ptr_vector<sort> sorts;
-        get_free_vars(fml, sorts);
-        if (!sorts.empty()) {
+        expr_free_vars fv;
+        fv(fml);
+        fv.set_default_sort(m.mk_bool_sort());
+        if (!fv.empty()) {
             expr_ref tmp(m);
-            for (unsigned i = sorts.size(); i > 0;) {
+            for (unsigned i = fv.size(); i > 0;) {
                 --i;
-                sort* s = sorts[i];
-                if (!s) {
-                    s = m.mk_bool_sort();
-                }
-                bound.push_back(m.mk_fresh_const("bound", s));
+                bound.push_back(m.mk_fresh_const("bound", fv[i]));
             }
             var_subst subst(m);
             subst(fml, bound.size(), bound.c_ptr(), tmp);
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 1c38ca343..cd043c8a7 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -87,6 +87,7 @@ namespace smt {
         typedef typename Ext::numeral     numeral;
         typedef typename Ext::inf_numeral inf_numeral;
         typedef vector<numeral> numeral_vector; 
+        typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
 
         static const int    dead_row_id = -1;
     protected:
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 3d95f1c72..9dae2d0c4 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -2993,7 +2993,6 @@ namespace smt {
     */
     template<typename Ext>
     void theory_arith<Ext>::refine_epsilon() {
-        typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
         while (true) {
             rational2var mapping;
             theory_var num = get_num_vars();
@@ -3001,6 +3000,8 @@ namespace smt {
             for (theory_var v = 0; v < num; v++) {
                 if (is_int(v))
                     continue;
+                if (!get_context().is_shared(get_enode(v)))
+                    continue;
                 inf_numeral const & val = get_value(v);
                 if (Ext::is_infinite(val)) {
                     continue;
diff --git a/src/tactic/horn_subsume_model_converter.cpp b/src/tactic/horn_subsume_model_converter.cpp
index ced4e657b..25da094fa 100644
--- a/src/tactic/horn_subsume_model_converter.cpp
+++ b/src/tactic/horn_subsume_model_converter.cpp
@@ -43,7 +43,7 @@ bool horn_subsume_model_converter::mk_horn(
     app* head, expr* body, func_decl_ref& pred, expr_ref& body_res) {
 
     expr_ref_vector conjs(m), subst(m);
-    ptr_vector<sort> sorts, sorts2;
+    ptr_vector<sort> sorts2;
     var_subst vs(m, false);
 
     if (!is_uninterp(head)) {
@@ -53,28 +53,27 @@ bool horn_subsume_model_converter::mk_horn(
     pred = head->get_decl();
     unsigned arity = head->get_num_args();
     
-    get_free_vars(head, sorts);
-    get_free_vars(body, sorts);
+    expr_free_vars fv;
+    fv(head);
+    fv.accumulate(body);
     
-    if (arity == 0 && sorts.empty()) {
+    if (arity == 0 && fv.empty()) {
         body_res = body;
         return true;
     }
+    fv.set_default_sort(m.mk_bool_sort());
 
     svector<symbol> names;
-    for (unsigned i = 0; i < sorts.size(); ++i) {
-        if (!sorts[i]) {
-            sorts[i] = m.mk_bool_sort();
-        }            
+    for (unsigned i = 0; i < fv.size(); ++i) {
         names.push_back(symbol(i));
     }
     names.reverse();
-    sorts.reverse();
+    fv.reverse();
     conjs.push_back(body);
     for (unsigned i = 0; i < arity; ++i) {
         expr* arg = head->get_arg(i);
         var_ref v(m);
-        v = m.mk_var(sorts.size()+i, m.get_sort(arg));
+        v = m.mk_var(fv.size()+i, m.get_sort(arg));
         
         if (is_var(arg)) {
             unsigned w = to_var(arg)->get_idx();
@@ -101,12 +100,12 @@ bool horn_subsume_model_converter::mk_horn(
         vs(tmp, subst.size(), subst.c_ptr(), body_expr);
     }    
 
-    if (sorts.empty()) {
+    if (fv.empty()) {
         SASSERT(subst.empty());
         body_res = body_expr;
     }   
     else {
-        body_res  = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), body_expr.get()); 
+        body_res  = m.mk_exists(fv.size(), fv.c_ptr(), names.c_ptr(), body_expr.get()); 
         m_rewrite(body_res);
         
     }
@@ -120,10 +119,9 @@ bool horn_subsume_model_converter::mk_horn(
 
 bool horn_subsume_model_converter::mk_horn(
     expr* clause, func_decl_ref& pred, expr_ref& body) {
-    ptr_vector<sort> sorts;
 
     // formula is closed.
-    DEBUG_CODE(get_free_vars(clause, sorts); SASSERT(sorts.empty()););
+    DEBUG_CODE(expr_free_vars fv; fv(clause); SASSERT(fv.empty()););
         
     while (is_quantifier(clause) && to_quantifier(clause)->is_forall()) {
         quantifier* q = to_quantifier(clause);