First step towards not-reusing variables

src/ast/rewriter/seq_skolem.cpp

@@ -26,6 +26,7 @@ skolem::skolem(ast_manager& m, th_rewriter& rw):
     m_suffix         = "seq.s.prefix";
     m_accept         = "aut.accept";
     m_tail           = "seq.tail";
+    m_slice          = "seq.slice";
     m_left           = "seq.left";
     m_right          = "seq.right";
     m_seq_first      = "seq.first";
@@ -159,6 +160,16 @@ bool skolem::is_tail(expr* e, expr*& s, expr*& idx) const {
     return is_tail(e) && (s = to_app(e)->get_arg(0), idx = to_app(e)->get_arg(1), true);
 }
 
+bool skolem::is_slice(expr* e, expr*& s) const {
+    expr* l = nullptr;
+    expr* r = nullptr;
+    return is_slice(e, s, l, r);
+}
+
+bool skolem::is_slice(expr* e, expr*& s, expr*& l, expr*& r) const {
+    return is_slice(e) && (s = to_app(e)->get_arg(0), l = to_app(e)->get_arg(1), r = to_app(e)->get_arg(2), true);
+}
+
 bool skolem::is_left_or_right(expr* e, expr*& x, expr*& y, expr*& z) {
     if (!is_skolem(m_left, e) && !is_skolem(m_right, e))
         return false;

src/ast/rewriter/seq_skolem.h

@@ -32,6 +32,7 @@ namespace seq {
 
         symbol         m_prefix, m_suffix;
         symbol         m_tail;
+        symbol         m_slice;
         symbol         m_left, m_right;
         symbol         m_seq_first, m_seq_last; 
         symbol         m_indexof_left, m_indexof_right;   // inverse of indexof: (indexof_left s t) + s + (indexof_right s t) = t, for s in t.
@@ -87,6 +88,7 @@ namespace seq {
         expr_ref mk_last_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk(m_lindexof_right, t, s, offset); }
 
         expr_ref mk_tail(expr* s, expr* i) { return mk(m_tail, s, i); }
+        expr_ref mk_slice(expr* s, expr* l, expr* r) { return mk(m_slice, s, l, r); }
         expr_ref mk_post(expr* s, expr* i) { return mk(m_post, s, i); }
         expr_ref mk_postp(expr* s, expr* i) { return mk(m_postp, s, i); }
         expr_ref mk_ite(expr* c, expr* t, expr* e) { return mk(symbol("seq.if"), c, t, e, nullptr, t->get_sort()); }
@@ -116,6 +118,7 @@ namespace seq {
         bool is_unit_inv(expr* e) const { return is_skolem(symbol("seq.unit-inv"), e); }
         bool is_unit_inv(expr* e, expr*& u) const { return is_unit_inv(e) && (u = to_app(e)->get_arg(0), true); }
         bool is_tail(expr* e) const { return is_skolem(m_tail, e); }
+        bool is_slice(expr* e) const { return is_skolem(m_slice, e); }
         bool is_seq_first(expr* e) const { return is_skolem(m_seq_first, e); }
         bool is_indexof_left(expr* e) const { return is_skolem(m_indexof_left, e); }
         bool is_indexof_right(expr* e) const { return is_skolem(m_indexof_right, e); }
@@ -154,6 +157,8 @@ namespace seq {
         bool is_tail(expr* e, expr*& s, expr*& idx) const;
         bool is_tail_u(expr* e, expr*& s, unsigned& idx) const;
         bool is_tail(expr* e, expr*& s) const;
+        bool is_slice(expr* e, expr*& s, expr*& l, expr*& r) const;
+        bool is_slice(expr* e, expr*& s) const;
         bool is_digit(expr* e) const { return is_skolem(symbol("seq.is_digit"), e); }
         bool is_max_unfolding(expr* e) const { return is_skolem(m_max_unfolding, e); }
         bool is_length_limit(expr* e) const { return is_skolem(m_length_limit, e); }

src/smt/seq/seq_nielsen.cpp

@@ -1155,6 +1155,37 @@ namespace seq {
         return true;
     }
 
+    euf::snode* nielsen_graph::get_slice(euf::snode* v, expr* left, expr* right) {
+        SASSERT(v && v->get_expr() && left && right);
+        SASSERT(v->is_var());
+
+        expr_ref new_arg(v->get_expr(), m);
+        expr_ref new_l(left, m), new_r(right, m);
+        expr* arg, *l, *r;
+        std::cout << "Creating slice for " << mk_pp(new_arg, m) << "; " << mk_pp(new_l, m) << "; " << mk_pp(new_r, m) << std::endl;
+
+        if (m_sk.is_slice(new_arg, arg, l, r)) {
+            new_l = a.mk_add(left, l);
+            m_rw(new_l);
+            new_r = a.mk_add(right, r);
+            m_rw(new_r);
+            new_arg = arg;
+        }
+        expr_ref slice = m_sk.mk_slice(new_arg, new_l, new_r);
+        std::cout << "Got " << mk_pp(slice, m) << std::endl;
+        return m_sg.mk(slice);
+    }
+
+
+    euf::snode* nielsen_graph::get_tail(euf::snode* v, expr* cnt, const bool fwd) {
+        if (fwd)
+            return get_slice(v, cnt, a.mk_int(0));
+        return get_slice(v, a.mk_int(0), cnt);
+    }
+
+    euf::snode* nielsen_graph::get_tail(euf::snode* v, const unsigned cnt, const bool fwd) {
+        return get_tail(v, a.mk_int(cnt), fwd);
+    }
 
     simplify_result nielsen_node::simplify_and_init(ptr_vector<nielsen_edge> const& cur_path) {
         if (m_is_extended)
@@ -1680,7 +1711,7 @@ namespace seq {
                 inc_run_idx();
                 ptr_vector<nielsen_edge> cur_path;
                 // scoped_push _scoped_push(m_dep_mgr); // gc dependencies after search
-                const search_result r = search_dfs(m_root, cur_path);
+                const search_result r = search_dfs(m_root, cur_path); // the main search loop
                 IF_VERBOSE(1, verbose_stream()
                                   << " depth_bound=" << m_depth_bound << " dfs_nodes=" << m_stats.m_num_dfs_nodes
                                   << " max_depth=" << m_stats.m_max_depth << " extensions=" << m_stats.m_num_extensions
@@ -1722,8 +1753,7 @@ namespace seq {
     }
 
     nielsen_graph::search_result nielsen_graph::search_dfs(nielsen_node* node,
-        ptr_vector<nielsen_edge>& cur_path,
+        ptr_vector<nielsen_edge>& cur_path, const unsigned depth) {
-                                                           const unsigned depth) {
 
         ++m_stats.m_num_dfs_nodes;
         // std::cout << m_stats.m_num_dfs_nodes << std::endl;
@@ -1885,6 +1915,7 @@ namespace seq {
 
         // explore children
         bool any_unknown = false;
+        bool all_general_conflict = true;
         for (nielsen_edge *e : node->outgoing()) {
             cur_path.push_back(e);
             // Push a solver scope for this edge and assert its side integer
@@ -1922,8 +1953,15 @@ namespace seq {
             cur_path.pop_back();
             if (r == search_result::unknown)
                 any_unknown = true;
+            if (!e->tgt()->is_general_conflict())
+                all_general_conflict = false;
         }
 
+        if (all_general_conflict) {
+            SASSERT(!any_unknown);
+            // mark it such that we do not have to reconsider it even after a hot-restart
+            node->set_general_conflict();
+        }
         if (!any_unknown) {
             node->set_child_conflict();
             return search_result::unsat;
@@ -2236,7 +2274,8 @@ namespace seq {
                 for (unsigned j = 1; j < i; ++j) {
                     prefix_sn = dir_concat(m_sg, prefix_sn, char_toks[j], fwd);
                 }
-                euf::snode* replacement = dir_concat(m_sg, prefix_sn, var_node, fwd);
+                euf::snode* replacement = dir_concat(m_sg, prefix_sn,
+                    get_tail(var_node, compute_length_expr(prefix_sn).get(), fwd), fwd);
                 nielsen_subst s(var_node, replacement,
                                 mk_rewrite(a.mk_sub(compute_length_expr(var_node), compute_length_expr(prefix_sn))),
                                 eq.m_dep);
@@ -2304,7 +2343,7 @@ namespace seq {
                     child->apply_subst(m_sg, s1);
 
 
-                    euf::snode* replacement = dir_concat(m_sg, char_head, var_head, fwd);
+                    euf::snode* replacement = dir_concat(m_sg, char_head, get_tail(var_head, a.mk_int(1), fwd), fwd);
                     child = mk_child(node);
                     e = mk_edge(node, child, false);
                     const nielsen_subst s2(var_head, replacement, mk_rewrite(a.mk_sub(compute_length_expr(var_head), a.mk_int(1))), eq.m_dep);
@@ -4249,7 +4288,8 @@ namespace seq {
                 SASSERT(n->m_conflict_external_literal == sat::null_literal);
                 continue;
             }
-            SASSERT(n->outgoing().empty());
+            // not true anymore since we might have done a hot-restart where we previously created the child:
+            //SASSERT(n->outgoing().empty());
             SASSERT(n->is_currently_conflict());
             if (n->m_conflict_external_literal != sat::null_literal)
                 // We know from the outer solver that this literal is assigned true and contradicts node constraint

src/smt/seq/seq_nielsen.h

@@ -475,7 +475,7 @@ namespace seq {
             // var may be s_var or s_power; sgraph::subst uses pointer identity matching
             SASSERT(var->is_var() || var->is_power() || var->is_unit());
             SASSERT(!var->is_unit() || repl->is_char_or_unit());
-            // SASSERT(!repl->collect_tokens().contains(var)); // for now - maybe we want to drop this later again
+            SASSERT(!repl->collect_tokens().contains(var)); // for now - maybe we want to drop this later again
         }
 
         // an eliminating substitution does not contain the variable in the replacement
@@ -694,6 +694,8 @@ namespace seq {
 
         backtrack_reason reason() const { return m_reason; }
 
+        void clear_reason() { m_reason = backtrack_reason::unevaluated; }
+
         void set_child_conflict() {
             SASSERT(m_reason == backtrack_reason::unevaluated);
             SASSERT(!m_conflict_internal);
@@ -1118,6 +1120,12 @@ namespace seq {
         // stores it in projection_re iff SCC coverage has grown.
         bool try_extract_partial_projection(euf::snode* root_re, euf::snode*& projection_re);
 
+        euf::snode* get_slice(euf::snode* v, expr* left, expr* right);
+
+        euf::snode* get_tail(euf::snode* v, expr* cnt, bool fwd = true);
+
+        euf::snode* get_tail(euf::snode* v, unsigned cnt, bool fwd = true);
+
         // Apply the Parikh image filter to a node: generate modular length
         // constraints from regex memberships and append them to the node's
         // constraints.  Also performs a lightweight feasibility pre-check;

src/smt/seq/seq_nielsen_pp.cpp

@@ -387,11 +387,21 @@ namespace seq {
         return dot_html_escape(os.str());
     }
 
+    std::string decode_recursive_name(expr* e, ast_manager& m) {
+        SASSERT(e && is_app(e));
+        th_rewriter rw(m);
+        const skolem sk(m, rw);
+        expr* arg = e, *l, *r;
+        while (sk.is_slice(arg, arg, l, r)) { }
+        if (to_app(arg)->get_num_args() != 0)
+            return "";
+        return dot_html_escape(to_app(arg)->get_decl()->get_name().str());
+    }
+
     // Helper: render a snode as an HTML label for DOT output.
     // Groups consecutive s_char tokens into quoted strings, renders s_var by name,
     // shows s_power with superscripts, s_unit by its inner expression,
     // and falls back to mk_pp, HTML-escaped, for other token kinds.
-
     std::string snode_label_html(euf::snode const* n, obj_map<expr, std::string>& names, uint64_t& next_id, ast_manager& m) {
         if (!n) return "null";
         seq_util seq(m);
@@ -437,8 +447,9 @@ namespace seq {
             if (!e) {
                 result += "#" + std::to_string(tok->id());
             } else if (tok->is_var()) {
-                if (to_app(e)->get_num_args() == 0) {
+                std::string name = decode_recursive_name(e, m);
-                    result += to_app(e)->get_decl()->get_name().str();
+                if (!name.empty()) {
+                    result += name;
                 }
                 else if (names.contains(e))
                     result += names[e];

src/smt/theory_nseq.cpp

@@ -713,6 +713,11 @@ namespace smt {
                     if (node->is_general_conflict())
                         // all its children are general conflicts as well - nothing to do
                         continue;
+                    if (node->reason() == seq::backtrack_reason::children_failed) {
+                        SASSERT(!node->is_general_conflict());
+                        node->clear_reason();
+                    }
+
                     if (node->is_external_conflict())
                         node->clear_local_conflict();