move deep internalization out of theory_seq

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

src/smt/theory_seq.cpp

@@ -302,7 +302,6 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
     m_ax(*this, m_rewrite),
     m_arith_value(m),
     m_trail_stack(*this),
-    m_internalize_depth(0),
     m_ls(m), m_rs(m),
     m_lhs(m), m_rhs(m),
     m_has_seq(m_util.has_seq()),
@@ -2081,12 +2080,6 @@ bool theory_seq::internalize_term(app* term) {
         mk_var(e);
         return true;
     }
-    flet<unsigned> _depth(m_internalize_depth, m_internalize_depth+1);
-
-    if (m_internalize_depth > 50 && m_ensure_todo.empty()) {
-        ensure_enodes(term);
-        return true;
-    }
 
     for (auto arg : *term) {        
         mk_var(ensure_enode(arg));
@@ -3257,39 +3250,6 @@ expr_ref theory_seq::mk_len(expr* s) {
     return result;
 }
 
-struct theory_seq::compare_depth {
-    bool operator()(expr* a, expr* b) const {
-        unsigned d1 = get_depth(a);
-        unsigned d2 = get_depth(b);
-        return d1 < d2 || (d1 == d2 && a->get_id() < b->get_id());
-    }
-};
-
-void theory_seq::ensure_enodes(expr* e) {
-    if (!m_ensure_todo.empty()) return;
-    context& ctx = get_context();
-    if (ctx.e_internalized(e)) return;
-    m_ensure_todo.push_back(e);
-    expr_mark visited;
-    for (unsigned i = 0; i < m_ensure_todo.size(); ++i) {
-        e = m_ensure_todo[i];
-        if (is_app(e) && to_app(e)->get_family_id() == m_util.get_family_id()) {
-            for (expr* arg : *to_app(e)) {
-                if (!ctx.e_internalized(arg) && !visited.is_marked(arg)) {
-                    m_ensure_todo.push_back(arg);
-                    visited.mark(arg);
-                }
-            }
-        }
-    }	
-    compare_depth cd;
-    std::stable_sort(m_ensure_todo.begin(), m_ensure_todo.end(), cd);
-
-    for (expr* e : m_ensure_todo) {
-        ensure_enode(e);
-    }
-    m_ensure_todo.reset();
-}
 
 template <class T>
 static T* get_th_arith(context& ctx, theory_id afid, expr* e) {

src/smt/theory_seq.h

@@ -407,7 +407,6 @@ namespace smt {
         th_trail_stack   m_trail_stack;
         stats            m_stats;
         ptr_vector<expr> m_todo, m_concat;
-        unsigned         m_internalize_depth;
         expr_ref_vector  m_ls, m_rs, m_lhs, m_rhs;
         bool             m_has_seq;
 
@@ -630,8 +629,6 @@ namespace smt {
         expr_ref mk_sub(expr* a, expr* b);
         expr_ref mk_add(expr* a, expr* b);
         expr_ref mk_len(expr* s);
-        ptr_vector<expr> m_ensure_todo;
-        void ensure_enodes(expr* e);
         enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }
         dependency* mk_join(dependency* deps, literal lit);
         dependency* mk_join(dependency* deps, literal_vector const& lits);