Removed recursion from regex unwinding

src/smt/seq/seq_nielsen.cpp

@@ -346,21 +346,11 @@ namespace seq {
         for (auto &mem : m_str_mem) {
             const auto new_str = sg.subst(mem.m_str, s.m_var, s.m_replacement);
             const auto new_regex = sg.subst(mem.m_regex, s.m_var, s.m_replacement);
-            std::cout << "Applying substitution "
-                << mk_pp(s.m_var->get_expr(), graph().m) << " / "
-                << mk_pp(s.m_replacement->get_expr(), graph().m) << " to " <<
-                    mk_pp(new_regex->get_expr(), graph().m) << std::endl;
             if (new_str != mem.m_str || new_regex != mem.m_regex) {
                 mem.m_str = new_str;
                 mem.m_regex = new_regex;
                 mem.m_dep = m_graph.dep_mgr().mk_join(mem.m_dep, s.m_dep);
             }
-            if (new_regex != mem.m_regex) {
-                std::cout << "Got: " << mk_pp(new_regex->get_expr(), graph().get_manager()) << std::endl;
-            }
-            else {
-                std::cout << "No change!" << std::endl;
-            }
         }
 
         const unsigned var_id = s.m_var->id();
@@ -4023,9 +4013,12 @@ namespace seq {
             //
             euf::snode* fresh_char = m_sg.mk(get_or_create_char_var(first));
 
-            euf::snode* replacement = m_sg.mk_concat(fresh_char, first);
+
+            euf::snode* tail = get_tail(first, 1, true);
+            euf::snode* replacement = m_sg.mk_concat(fresh_char, tail);
             nielsen_node* child = mk_child(node);
             nielsen_edge* e = mk_edge(node, child, false);
+
             const nielsen_subst s(first, replacement, mk_rewrite(a.mk_sub(compute_length_expr(first), a.mk_int(1))), mem.m_dep);
             e->add_subst(s);
             child->apply_subst(m_sg, s);

src/smt/seq/seq_nielsen.h

@@ -464,12 +464,12 @@ namespace seq {
     struct nielsen_subst {
         euf::snode* m_var;
         euf::snode* m_replacement;
-        euf::snode *m_length = nullptr; // representation of length if this is a sequence variable, null otherwise.
+        // euf::snode *m_length = nullptr; // representation of length if this is a sequence variable, null otherwise.
         dep_tracker m_dep;
 
         nielsen_subst(): m_var(nullptr), m_replacement(nullptr), m_dep(nullptr) {}
         nielsen_subst(euf::snode* var, euf::snode* repl, euf::snode* length, dep_tracker const& dep):
-            m_var(var), m_replacement(repl), m_length(length), m_dep(dep) {
+            m_var(var), m_replacement(repl)/*, m_length(length)*/, m_dep(dep) {
             SASSERT(var != nullptr);
             SASSERT(repl != nullptr);
             // var may be s_var or s_power; sgraph::subst uses pointer identity matching

src/smt/seq_model.cpp

@@ -211,7 +211,6 @@ namespace smt {
             unsigned id = var->first()->id(); // TODO - first or just var->id()?
             SASSERT(!m_var_replacement.contains(id));
             m_var_replacement.insert(id, replacement);
-            std::cout << "Assignment: " << mk_pp(var->get_expr(), m) << ": " << mk_pp(replacement->get_expr(), m) << std::endl;
         }
     }
     

src/smt/theory_nseq.cpp

@@ -461,12 +461,10 @@ namespace smt {
 
         if (!get_fparams().m_nseq_regex_factorization_threshold)
             return;
-        std::cout << "Trying " << seq::mem_pp(mem, m);
 
         // Boolean Closure Propagations
         expr* re_expr = mem.m_regex->get_expr();
         if (m_seq.re.is_intersection(re_expr)) {
-            std::cout << "Propagating intersection " << seq::mem_pp(mem, m) << std::endl;
             for (expr* arg : *to_app(re_expr)) {
                 expr_ref in_r(m_seq.re.mk_in_re(s_expr, arg), m);
                 literal_vector lits;
@@ -479,7 +477,6 @@ namespace smt {
             return;
         }
         if (m_seq.re.is_union(re_expr)) {
-            std::cout << "Propagating union " << seq::mem_pp(mem, m) << std::endl;
             literal_vector lits;
             lits.push_back(~mem.lit);
             for (expr* arg : *to_app(re_expr)) {
@@ -496,7 +493,6 @@ namespace smt {
             zstring s;
             expr_ref arg(to_app(re_expr)->get_arg(0), m);
             if (m_seq.str.is_string(arg, s)) {
-                std::cout << "Propagating const matching " << seq::mem_pp(mem, m) << std::endl;
                 literal_vector lits;
                 lits.push_back(~mem.lit);
                 lits.push_back(mk_literal(m.mk_eq(s_expr, arg)));