From 2bbd75a1861e7a2a469a144a379955f5f21be5e5 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 28 May 2026 15:29:43 +0200 Subject: [PATCH] We should not bypass checking primitive constraints being empty --- src/smt/seq/seq_nielsen.cpp | 31 +++++++++++++------------------ src/smt/seq/seq_nielsen.h | 4 +--- src/smt/theory_nseq.cpp | 18 +++++++++--------- 3 files changed, 23 insertions(+), 30 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 8ac7c663c..7e188293c 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -35,6 +35,7 @@ NSB review: #include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/seq_skolem.h" #include "ast/rewriter/var_subst.h" +#include "smt/smt_enode.h" #include "util/statistics.h" #include #include @@ -45,12 +46,16 @@ NSB review: namespace seq { - void deps_to_lits(const dep_tracker deps, svector &eqs, svector &lits) { - vector vs; - dep_manager::s_linearize(deps, vs); + void deps_to_lits(dep_manager &dep_mgr, const dep_tracker deps, + svector &eqs, svector &lits) { + + vector vs; + dep_mgr.linearize(deps, vs); for (dep_source const &d : vs) { - if (std::holds_alternative(d)) + if (std::holds_alternative(d)) { eqs.push_back(std::get(d)); + SASSERT(eqs.back().first->get_root() == eqs.back().second->get_root()); + } else if (std::holds_alternative(d)) lits.push_back(std::get(d)); else @@ -1962,12 +1967,6 @@ namespace seq { return search_result::unsat; } - if (node->is_satisfied()) { - m_sat_node = node; - m_sat_path = cur_path; - return search_result::sat; - } - // simplify constraints (idempotent after first call) const simplify_result sr = node->simplify_and_init(cur_path); @@ -3758,7 +3757,7 @@ namespace seq { first_filter_dep = m_dep_mgr.mk_join(first_filter_dep, prev_mem.m_dep); } } - if (regexes_p.size() > 1 && m_seq_regex->check_intersection_emptiness(regexes_p, 100) == l_true) { + if (m_seq_regex->check_intersection_emptiness(regexes_p, 100) == l_true) { eliminated_dep = m_dep_mgr.mk_join(eliminated_dep, first_filter_dep); continue; } @@ -4982,15 +4981,13 @@ namespace seq { // ----------------------------------------------------------------------- bool nielsen_graph::check_leaf_regex(nielsen_node const& node, dep_tracker& dep) { - if (!m_seq_regex) - return true; + SASSERT(m_seq_regex); // Group str_mem constraints by variable (primitive constraints only) u_map, dep_tracker>> var_regexes; for (auto const& mem : node.str_mems()) { - if (!mem.is_primitive()) - continue; + SASSERT(mem.is_primitive()); const euf::snode* const first = mem.m_str->first(); SASSERT(first && first->is_var()); auto& list = var_regexes.insert_if_not_there(first->id(), std::pair, dep_tracker>()); @@ -4998,10 +4995,8 @@ namespace seq { list.second = dep_mgr().mk_join(list.second, mem.m_dep); } - // For each variable with 2+ regex constraints, check intersection non-emptiness + // check intersection non-emptiness (also for single occurrences; it could be empty) for (auto& [var_id, regexes] : var_regexes) { - if (regexes.first.size() < 2) - continue; const lbool result = m_seq_regex->check_intersection_emptiness(regexes.first, 5000); if (result == l_true) { TRACE(seq, tout << "empty intersection\n"); diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index de5c17bec..8322ea69a 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -375,9 +375,7 @@ namespace seq { // partition dep_source leaves from deps into enode pairs, sat literals, // and arithmetic <= dependencies. - void deps_to_lits(dep_tracker deps, - enode_pair_vector& eqs, - literal_vector& lits); + void deps_to_lits(dep_manager &dep_mgr, dep_tracker deps, svector &eqs, svector &lits); // string equality constraint: lhs = rhs // mirrors ZIPT's StrEq (both sides are regex-free snode trees) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index a21512c10..f94ac0651 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -1392,7 +1392,7 @@ namespace smt { // conditional constraints: propagate with justification from dep_tracker enode_pair_vector eqs; literal_vector lits; - seq::deps_to_lits(lc.m_dep, eqs, lits); + seq::deps_to_lits(m_nielsen.dep_mgr(), lc.m_dep, eqs, lits); set_propagate(eqs, lits, lit); @@ -1692,14 +1692,12 @@ namespace smt { for (unsigned i = 0; i < mems.size(); ++i) { auto const &mem = mems[i]; SASSERT(mem.well_formed()); - if (mem.is_primitive()) { - auto &vec = var_to_mems.insert_if_not_there(mem.m_str->id(), unsigned_vector()); - vec.push_back(i); - } + SASSERT(mem.is_primitive()); + auto &vec = var_to_mems.insert_if_not_there(mem.m_str->id(), unsigned_vector()); + vec.push_back(i); } - if (var_to_mems.empty()) - return true; + SASSERT(!var_to_mems.empty()); for (expr *len_expr : m_relevant_lengths) { expr *s = nullptr; @@ -1787,8 +1785,10 @@ namespace smt { enode_pair_vector eqs; literal_vector dep_lits; - for (unsigned idx : mem_indices) - seq::deps_to_lits(mems[idx].m_dep, eqs, dep_lits); + for (unsigned idx : mem_indices) { + std::cout << seq::mem_pp(mems[idx], m) << std::endl; + seq::deps_to_lits(m_nielsen.dep_mgr(), mems[idx].m_dep, eqs, dep_lits); + } set_propagate(eqs, dep_lits, lit_prop);