From 9d2244798d23e2523f94cc36409f2042274c9742 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Mar 2026 09:00:37 -0700 Subject: [PATCH] fix insertions into subst. Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 34 +++++++++++++++++++++++++++------- src/smt/seq/seq_nielsen.h | 9 +++------ src/smt/theory_nseq.cpp | 8 -------- src/smt/theory_nseq.h | 1 - 4 files changed, 30 insertions(+), 22 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 8f3fcd5e7..a47154e71 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1467,6 +1467,17 @@ namespace seq { } } + template class scoped_push { + T &t; + public: + scoped_push(T& t) : t(t) { + t.push_scope(); + } + ~scoped_push() { + t.pop_scope(1); + } + }; + nielsen_graph::search_result nielsen_graph::solve() { SASSERT(m_root); @@ -1497,6 +1508,7 @@ namespace seq { break; inc_run_idx(); ptr_vector cur_path; + // scoped_push _scoped_push(m_dep_mgr); // gc dependencies after search search_result r = search_dfs(m_root, cur_path); IF_VERBOSE(1, verbose_stream() << " depth_bound=" << m_depth_bound << " dfs_nodes=" << m_stats.m_num_dfs_nodes @@ -1517,9 +1529,8 @@ namespace seq { return r; } if (r == search_result::unsat) { - ++m_stats.m_num_unsat; - dep_tracker deps = m_dep_mgr.mk_empty(); - collect_conflict_deps(deps); + ++m_stats.m_num_unsat; + auto deps = collect_conflict_deps(); m_dep_mgr.linearize(deps, m_conflict_sources); return r; } @@ -1739,6 +1750,12 @@ namespace seq { nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); + if (lt->is_char()) { + std::swap(lt, rt); + std::swap(l, r); + } + SASSERT(lt->is_unit()); + euf::snode* lhs_rest = m_sg.drop_left(l, prefix + 1); euf::snode* rhs_rest = m_sg.drop_left(r, prefix + 1); @@ -1746,12 +1763,14 @@ namespace seq { eqs[eq_idx] = eqs.back(); eqs.pop_back(); - nielsen_subst subst(lt, rt, eq.m_dep); + nielsen_subst subst(lt->arg(0), rt->arg(0), eq.m_dep); e->add_subst(subst); child->apply_subst(m_sg, subst); if (!lhs_rest->is_empty() && !rhs_rest->is_empty()) eqs.push_back(str_eq(lhs_rest, rhs_rest, eq.m_dep)); + + // NSB review: lt->arg(0) == rt->arg(0) should also be a side constraint return true; } else @@ -3608,7 +3627,8 @@ namespace seq { return true; } - void nielsen_graph::collect_conflict_deps(dep_tracker& deps) const { + dep_tracker nielsen_graph::collect_conflict_deps() const { + dep_tracker deps = nullptr; for (nielsen_node const* n : m_nodes) { if (n->eval_idx() != m_run_idx) continue; @@ -3619,6 +3639,7 @@ namespace seq { for (str_mem const& mem : n->str_mems()) deps = m_dep_mgr.mk_join(deps, mem.m_dep); } + return deps; } @@ -3626,8 +3647,7 @@ namespace seq { void nielsen_graph::explain_conflict(svector& eqs, svector& mem_literals) const { SASSERT(m_root); - dep_tracker deps = m_dep_mgr.mk_empty(); - collect_conflict_deps(deps); + auto deps = collect_conflict_deps(); vector vs; m_dep_mgr.linearize(deps, vs); for (dep_source const& d : vs) { diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index f99e478a6..abb88de36 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -246,15 +246,11 @@ Author: #include #include "model/model.h" -namespace seq { - class seq_regex; // forward declaration (defined in smt/seq/seq_regex.h) -} namespace smt { class enode; } - namespace seq { // forward declarations @@ -262,6 +258,7 @@ namespace seq { class nielsen_edge; class nielsen_graph; class seq_parikh; + class seq_regex; // forward declaration (defined in smt/seq/seq_regex.h) std::string snode_label_html(euf::snode const* n, obj_map& names, uint64_t& next_id, ast_manager& m); @@ -426,6 +423,7 @@ namespace seq { SASSERT(repl != nullptr); // 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()); } // an eliminating substitution does not contain the variable in the replacement @@ -855,7 +853,6 @@ namespace seq { // path of edges from root to sat_node (set when sat_node is set) ptr_vector const& sat_path() const { return m_sat_path; } - // add constraints to the root node from external solver void add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r); void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l); @@ -960,7 +957,7 @@ namespace seq { dep_manager const& dep_mgr() const { return m_dep_mgr; } // collect dependency information from conflicting constraints - void collect_conflict_deps(dep_tracker& deps) const; + dep_tracker collect_conflict_deps() const; search_result search_dfs(nielsen_node *node, ptr_vector& path); diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 3c320c2a3..96c9cdc93 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -579,14 +579,6 @@ namespace smt { // Conflict explanation // ----------------------------------------------------------------------- - void theory_nseq::add_conflict_clause(seq::dep_tracker const& deps) { - enode_pair_vector eqs; - literal_vector lits; - seq::deps_to_lits(deps, eqs, lits); - ++m_num_conflicts; - set_conflict(eqs, lits); - } - void theory_nseq::explain_nielsen_conflict() { enode_pair_vector eqs; literal_vector lits; diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 1fdbbd895..e624dceb0 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -113,7 +113,6 @@ namespace smt { // private helpers void populate_nielsen_graph(); void explain_nielsen_conflict(); - void add_conflict_clause(seq::dep_tracker const& deps); void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits); euf::snode* get_snode(expr* e);