From c9fb43219195a2186d4afcc755cef3248e2c1a9d Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 12 May 2026 10:30:29 +0200 Subject: [PATCH] The side-condition of the "if"-split belongs on the edges --- src/smt/seq/seq_nielsen.cpp | 20 ++++++++++++-------- src/smt/seq/seq_nielsen.h | 8 ++++---- src/smt/seq/seq_regex.cpp | 2 +- src/smt/theory_nseq.cpp | 35 ++++++++++++++++++++++++++--------- src/smt/theory_nseq.h | 1 + 5 files changed, 44 insertions(+), 22 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 0cb5ac36f..4013f46b9 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1443,7 +1443,7 @@ namespace seq { euf::snode* deriv = fwd ? sg.brzozowski_deriv(mem.m_regex, tok) : reverse_brzozowski_deriv(sg, mem.m_regex, tok); - TRACE(seq, tout << mem_pp(m, mem) << " d: " << spp(deriv, m) << "\n"); + TRACE(seq, tout << mem_pp(mem, m) << " d: " << spp(deriv, m) << "\n"); if (!deriv) break; if (deriv->is_fail()) { @@ -1529,7 +1529,7 @@ namespace seq { // check for regex memberships that are immediately infeasible for (str_mem& mem : m_str_mem) { if (mem.is_contradiction(this)) { - TRACE(seq, tout << "contradiction " << mem_pp(m, mem) << "\n"); + TRACE(seq, tout << "contradiction " << mem_pp(mem, m) << "\n"); set_general_conflict(); set_conflict(backtrack_reason::regex, mem.m_dep); return simplify_result::conflict; @@ -3521,7 +3521,7 @@ namespace seq { for (str_mem const& mem : node->str_mems()) { SASSERT(mem.well_formed()); - if (mem.is_primitive() || !mem.m_regex->is_classical()) + if (mem.m_str->is_empty() || mem.is_primitive() || !mem.m_regex->is_classical()) continue; euf::snode* first = mem.m_str->first(); @@ -3529,6 +3529,7 @@ namespace seq { SASSERT(!first->is_char()); euf::snode* tail = m_sg.drop_first(mem.m_str); SASSERT(tail); + std::cout << "Processing: " << mem_pp(mem, m) << std::endl; tau_pairs pairs; compute_tau(m, m_seq, m_sg, mem.m_regex->get_expr(), pairs); @@ -3913,14 +3914,17 @@ namespace seq { // No ite remaining: leaf → create child node with regex updated to r euf::snode *new_regex_snode = m_sg.mk(r); nielsen_node *child = mk_child(node); - for (auto f : cs) - child->add_constraint(constraint(f, mem.m_dep, m)); - mk_edge(node, child, true); - for (str_mem &cm : child->str_mems()) + nielsen_edge* e = mk_edge(node, child, true); + for (auto f : cs) { + std::cout << "sc: " << mk_pp(f, m) << std::endl; + e->add_side_constraint(constraint(f, mem.m_dep, m)); + } + for (str_mem &cm : child->str_mems()) { if (cm == mem) { cm.m_regex = new_regex_snode; break; } + } created = true; continue; } @@ -4743,7 +4747,7 @@ namespace seq { // TODO: Minimize the conflict here lbool result = m_seq_regex->is_empty_bfs(inter_sn, 5000); TRACE(seq, tout << "widen empty-intersect: " << result << " " << mk_pp(re, m) - << " <= " << mk_pp(ae, m) << "\n" << mem_pp(m, mem) << "\n"; + << " <= " << mk_pp(ae, m) << "\n" << mem_pp(mem, m) << "\n"; display(tout, &node) << "\n"); return result == l_true; } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 37376aabf..fdd63b009 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -440,9 +440,9 @@ namespace seq { }; struct mem_pp { - ast_manager &m; str_mem const& mem; - mem_pp(ast_manager &m, str_mem const&mem) : m(m), mem(mem) {} + ast_manager &m; + mem_pp(str_mem const& mem, ast_manager& m) : m(m), mem(mem) {} }; inline std::ostream &operator<<(std::ostream &out, mem_pp const &p) { return out << mk_pp(p.mem.m_str->get_expr(), p.m) << " in " << mk_pp(p.mem.m_regex->get_expr(), p.m) << "\n"; @@ -490,9 +490,9 @@ namespace seq { dep_tracker dep; // tracks which input constraints contributed static expr_ref simplify(expr* f, ast_manager& m) { - th_rewriter th(m); + //th_rewriter th(m); expr_ref fml(f, m); - th(fml); + //th(fml); return fml; } diff --git a/src/smt/seq/seq_regex.cpp b/src/smt/seq/seq_regex.cpp index 116bf95f7..6cb1aed10 100644 --- a/src/smt/seq/seq_regex.cpp +++ b/src/smt/seq/seq_regex.cpp @@ -613,7 +613,7 @@ namespace seq { SASSERT(first); if (first != var) continue; - TRACE(seq, tout << spp(first, m) << " " << mem_pp(m, mem) << "\n"); + TRACE(seq, tout << spp(first, m) << " " << mem_pp(mem, m) << "\n"); if (!result) { result = mem.m_regex; diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index e2f2eca22..a9d22d80d 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -473,10 +473,12 @@ 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; @@ -484,8 +486,12 @@ namespace smt { lits.push_back(mk_literal(in_r)); ctx.mk_th_axiom(get_id(), lits.size(), lits.data()); } + m_ignored_mem.insert(mem.lit); + ctx.push_trail(insert_map(m_ignored_mem, mem.lit)); + return; } - else if (m_seq.re.is_union(re_expr)) { + 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)) { @@ -493,14 +499,23 @@ namespace smt { lits.push_back(mk_literal(in_r)); } ctx.mk_th_axiom(get_id(), lits.size(), lits.data()); + m_ignored_mem.insert(mem.lit); + ctx.push_trail(insert_map(m_ignored_mem, mem.lit)); + return; } - else if (m_seq.re.is_complement(re_expr)) { - expr* arg = to_app(re_expr)->get_arg(0); - expr_ref in_r(m_seq.re.mk_in_re(s_expr, arg), m); - literal_vector lits; - lits.push_back(~mem.lit); - lits.push_back(~mk_literal(in_r)); - ctx.mk_th_axiom(get_id(), lits.size(), lits.data()); + if (m_seq.re.is_to_re(re_expr)) { + return; + 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))); + ctx.mk_th_axiom(get_id(), lits.size(), lits.data()); + m_ignored_mem.insert(mem.lit); + ctx.push_trail(insert_map(m_ignored_mem, mem.lit)); + } } } @@ -618,6 +633,8 @@ namespace smt { ++num_mems; continue; } + /*if (m_ignored_mem.contains(mem.lit)) + continue; // already handled via Boolean closure, skip*/ // pre-process: consume ground prefix characters vector processed; if (!m_regex.process_str_mem(mem, processed)) { @@ -997,7 +1014,7 @@ namespace smt { } idx = 0; for (auto& mem : m_nielsen.root()->str_mems()) { - std::cout << "[" << (idx++) << "]: " << seq::mem_pp(m, mem); + std::cout << "[" << (idx++) << "]: " << seq::mem_pp(mem, m); } std::flush(std::cout); #endif diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 35e07d1e7..f7867f153 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -62,6 +62,7 @@ namespace smt { unsigned m_prop_qhead = 0; obj_hashtable m_axiom_set; // dedup guard for axiom_item enqueues obj_hashtable m_no_diseq_set; // track expressions that should not trigger new disequality axioms + hashtable, default_eq> m_ignored_mem; // track membership constraints that should not be passed to Nielsen expr_ref_vector m_relevant_lengths; // track variables whose lengths are relevant obj_map m_gradient_cache; sat::literal_vector m_nielsen_literals; // literals created by a Nilsen check