From d885580633abb69c20a4fcc0a2f1e26d19c8a8e6 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Mon, 20 Jul 2026 18:01:31 +0200 Subject: [PATCH] Enforce all power terms are internalized at model construction phase --- src/smt/seq_model.cpp | 24 +++++++++++------------- src/smt/theory_nseq.cpp | 30 ++++++++++++++++++++++++++---- src/smt/theory_nseq.h | 6 ++++++ 3 files changed, 43 insertions(+), 17 deletions(-) diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index fb9f8bb598..64d85d4039 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -134,6 +134,8 @@ namespace smt { return alloc(expr_wrapper_proc, to_app(e)); } + std::cout << mk_pp(n->get_expr(), m) << std::endl; + // For nth_u (underspecified nth): the Nielsen character-peel / // regex-if-split records the chosen character as a relevant // equality literal (e.g. (= (seq.nth_u x 0) (_ Char 65))), so the @@ -239,12 +241,11 @@ namespace smt { if (seen.contains(curr->id())) continue; seen.insert(curr->id()); - if (m.is_value(curr->get_expr())) - ; - else if (curr->is_empty()) - ; - else if (curr->is_char_or_unit()) { - expr *e = curr->arg(0)->get_expr(); + if (m.is_value(curr->get_expr()) || curr->is_empty()) + continue; + + if (curr->is_char_or_unit()) { + expr* e = curr->arg(0)->get_expr(); if (m_ctx.e_internalized(e)) deps.push_back(m_ctx.get_enode(e)); } @@ -283,14 +284,9 @@ namespace smt { expr_ref seq_model::snode_to_value(euf::snode const* n, enode_vector const &deps, expr_ref_vector const &values) { // var2value: leaf deps keyed by expression ID (populated from `deps`/`values`). - // node2value: computed nodes keyed by (snode_id * 2 + is_recursive). - // The recursion flag is part of the key because the SAME variable snode - // appears in two distinct roles in a Nielsen substitution such as D -> "cc" D: - // the outer variable (is_recursive == false, value == value of its replacement) - // and the inner "leftover" remainder (is_recursive == true, value == ""). u_map var2value; u_map node2value; - // resolve: check leaf deps by expression ID, computed nodes by (snode,recursive) key. + // resolve: check leaf deps by expression ID, computed nodes by snode key. auto resolve = [&](euf::snode const* s, expr*& out) -> bool { if (var2value.find(s->get_expr()->get_id(), out)) return true; @@ -307,6 +303,7 @@ namespace smt { expr *val = nullptr; while (!todo.empty()) { auto curr = todo.back(); + // std::cout << "processing: " << mk_pp(curr->get_expr(), m) << std::endl; // Early exit: already computed (as leaf dep or computed node). expr* cached = nullptr; if (resolve(curr, cached)) { @@ -445,7 +442,8 @@ namespace smt { if (a.is_numeral(e, val)) return val; - bool has_val = get_arith_value(e, val); + + bool has_val = get_arith_value(_e, val); CTRACE(seq, !has_val, tout << "no value associated with " << mk_pp(e, m) << "\n";); return val; } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 14daf55b99..bb15caab19 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -920,6 +920,8 @@ namespace smt { m_nielsen.reset(); m_nielsen.create_root(); m_nielsen.set_sat_node(m_nielsen.root()); + if (!ensure_model_internalized()) + return FC_CONTINUE; TRACE(seq, display(tout << "empty nielsen\n")); return FC_DONE; } @@ -939,6 +941,8 @@ namespace smt { m_nielsen.reset(); m_nielsen.create_root(); m_nielsen.set_sat_node(m_nielsen.root()); + if (!ensure_model_internalized()) + return FC_CONTINUE; TRACE(seq, display(tout << "empty nielsen\n")); return FC_DONE; } @@ -962,9 +966,10 @@ namespace smt { all_of(m_nielsen_literals, [&](auto lit) { return l_true == ctx.get_assignment(lit); })) { ++m_num_sat_revalidations; TRACE(seq, tout << "nseq final_check: revalidated cached SAT path, skipping rebuild\n"); - if (!check_length_coherence()) return FC_CONTINUE; - if (!check_stoi_coherence()) return FC_CONTINUE; - if (!has_unhandled_preds()) return FC_DONE; + if (!check_length_coherence()) return FC_CONTINUE; + if (!check_stoi_coherence()) return FC_CONTINUE; + if (!ensure_model_internalized()) return FC_CONTINUE; + if (!has_unhandled_preds()) return FC_DONE; return FC_GIVEUP; } // fall through - no reason to rebuild the Nielsen graph @@ -1071,6 +1076,8 @@ namespace smt { if (!check_stoi_coherence()) return FC_CONTINUE; TRACE(seq, tout << "pre-check done\n"); + if (!ensure_model_internalized()) + return FC_CONTINUE; return FC_DONE; default: break; @@ -1116,6 +1123,8 @@ namespace smt { if (!all_sat) return FC_CONTINUE; + if (!ensure_model_internalized()) + return FC_CONTINUE; if (!has_unhandled_preds()) return FC_DONE; @@ -1160,7 +1169,7 @@ namespace smt { bool all_sat = true; ctx.push_trail(reset_vector(m_nielsen_literals)); for (const auto& c : m_nielsen.sat_node()->constraints()) { - // std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl; + std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl; auto lit = mk_literal(c.fml); m_nielsen_literals.push_back(lit); // Ensure Nielsen assumptions participate in SAT search instead of @@ -2293,6 +2302,19 @@ namespace smt { return true; } + bool theory_nseq::ensure_model_internalized() const { + bool all_internalized = true; + for (const auto * n : m_nielsen.sat_path()) { + for (const auto& subst : n->subst()) { + if (ctx.e_internalized(subst.m_replacement->get_expr())) + continue; + ctx.internalize(subst.m_replacement->get_expr(), false); + all_internalized = false; + } + } + return all_internalized; + } + // ----------------------------------------------------------------------- // Use theory assumptions to bound search depth and force literal assignments // m_assumption_lit gets added as an assumption to the set of existing assumptions. diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index f3c6d9f1f2..838d8b204e 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -208,6 +208,12 @@ namespace smt { bool check_length_coherence(); + // Has to be called before model construction + // otw. some terms required for model construction would be not initialized + // e.g., X = a^{2 + n} + // term "2 + n" would not necessarily be internalized + bool ensure_model_internalized() const; + // stoi axiom helpers void add_stoi_nseq_axioms(expr* stoi_e); bool check_stoi_coherence();