From 168b51d3321d1d222c503d8f0e13d488c27cd1ce Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Jul 2026 14:31:35 -0700 Subject: [PATCH] Remove var_extra from seq_monadic API Per-variable extra constraints are now expressed as additional (var in R') memberships passed to solve_and, so the var_extra parameter is dropped from solve/solve_and and the internal decide_dnf. Tests updated to route extra constraints through solve_and. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9 --- src/ast/rewriter/seq_monadic.cpp | 23 +++++++---------------- src/ast/rewriter/seq_monadic.h | 20 ++++++++------------ src/test/seq_monadic.cpp | 20 ++++++++++++++++---- src/test/seq_monadic_bench.cpp | 3 +-- 4 files changed, 32 insertions(+), 34 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index ecc58da3a4..71640041f8 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -356,12 +356,7 @@ void seq_monadic::simplify_dnf(vector& dnf) { } lbool seq_monadic::solve(expr* term, expr* R) { - obj_map none; - return solve(term, R, none, nullptr); -} - -lbool seq_monadic::solve(expr* term, expr* R, obj_map const& var_extra) { - return solve(term, R, var_extra, nullptr); + return solve(term, R, nullptr); } bool seq_monadic::build_membership_dnf(expr* term, expr* R, vector& dnf) { @@ -381,11 +376,10 @@ bool seq_monadic::build_membership_dnf(expr* term, expr* R, vector& dn return ok; } -lbool seq_monadic::decide_dnf(vector const& dnf, obj_map const& var_extra, - obj_map* model) { +lbool seq_monadic::decide_dnf(vector const& dnf, obj_map* model) { bool any_undef = false; for (disjunct const& D : dnf) { - // group components by variable, add the extra per-variable constraints + // group components by variable obj_map idx; vector> groups; ptr_vector group_var; @@ -399,8 +393,6 @@ lbool seq_monadic::decide_dnf(vector const& dnf, obj_map }; for (auto const& c : D) groups[bucket(c.var)].push_back(c); - for (auto const& kv : var_extra) - groups[bucket(kv.m_key)].push_back(component{ kv.m_key, kv.m_value, nullptr }); bool has_empty = false, has_undef = false; obj_map local; // var -> witness for this disjunct @@ -421,19 +413,18 @@ lbool seq_monadic::decide_dnf(vector const& dnf, obj_map return any_undef ? l_undef : l_false; } -lbool seq_monadic::solve(expr* term, expr* R, obj_map const& var_extra, - obj_map* model) { +lbool seq_monadic::solve(expr* term, expr* R, obj_map* model) { m_pin.reset(); m_budget = 200000; // global work budget: bail fast on DNF explosion m_giveup = false; vector dnf; if (!build_membership_dnf(term, R, dnf)) return l_undef; - return decide_dnf(dnf, var_extra, model); + return decide_dnf(dnf, model); } lbool seq_monadic::solve_and(vector> const& mems, - obj_map const& var_extra, obj_map* model) { + obj_map* model) { if (mems.empty()) return l_undef; m_pin.reset(); @@ -466,5 +457,5 @@ lbool seq_monadic::solve_and(vector> const& mems, if (combined.empty()) return l_false; // no viable disjunct left => unsat } - return decide_dnf(combined, var_extra, model); + return decide_dnf(combined, model); } diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 63de75cc5d..06d603d408 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -41,8 +41,9 @@ Abstract: This stays in the product-of-state-counts regime, never the path-enumeration (k!) regime of regex state-elimination. - Supports single / multiple / repeated variables, and per-variable extra constraints - (base membership + length-regex) via `var_extra`. + Supports single / multiple / repeated variables. Per-variable extra constraints + (e.g. a base membership intersected with a length-regex) are expressed as an extra + membership passed to `solve_and`. Author: @@ -126,8 +127,7 @@ private: // Decide a DNF (over primitive components): sat iff some disjunct has every variable // group non-empty. On l_true, fills `model` (var -> witness) if non-null. - lbool decide_dnf(vector const& dnf, obj_map const& var_extra, - obj_map* model); + lbool decide_dnf(vector const& dnf, obj_map* model); public: seq_monadic(seq_rewriter& rw, transition_mode mode = transition_mode::light_antimirov) : @@ -140,23 +140,19 @@ public: // l_true = sat, l_false = unsat, l_undef = unsupported shape / gave up. lbool solve(expr* term, expr* R); - // As above, with extra per-variable constraints (e.g. a base membership intersected - // with a length-regex): `var_extra` maps a variable to a regex it must also satisfy. - lbool solve(expr* term, expr* R, obj_map const& var_extra); - // As above; on l_true, if `model` is non-null it is populated with var -> witness, // where each witness is a concrete sequence term (over the element sort) giving one // satisfying assignment. Witness terms are pinned by the solver and remain valid // until the next call to solve(). - lbool solve(expr* term, expr* R, obj_map const& var_extra, - obj_map* model); + lbool solve(expr* term, expr* R, obj_map* model); // Decide a CONJUNCTION of memberships AND_i (term_i in R_i) jointly: a variable // shared across memberships is constrained consistently (the DNFs are multiplied and // each variable's constraints intersected). This is the natural extension of single- // membership solving to a Boolean combination of memberships (a disjunction is the // union of DNFs; a negated membership ~(t in R) is just t in complement(R)). - // var_extra / model as above. l_true = sat, l_false = unsat, l_undef = gave up. + // Per-variable extra constraints are expressed here as extra memberships (v in R'). + // model as above. l_true = sat, l_false = unsat, l_undef = gave up. lbool solve_and(vector> const& mems, - obj_map const& var_extra, obj_map* model = nullptr); + obj_map* model = nullptr); }; diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index b1587d77ce..621c40b73d 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -128,9 +128,20 @@ class seq_monadic_test { << " got=" << s(got) << " expected=" << s(expected) << "\n"; } + // build the membership list: the primary (term in R) plus one (var in R') per extra + // constraint, decided jointly by solve_and. + void add_extra(vector>& mems, expr* term, expr* R, + obj_map const& ve) { + mems.push_back(std::make_pair(term, R)); + for (auto const& kv : ve) + mems.push_back(std::make_pair(kv.m_key, kv.m_value)); + } + void check_extra(char const* name, expr* term, expr* R, obj_map const& ve, lbool expected) { - lbool got = m_mon.solve(term, R, ve); + vector> mems; + add_extra(mems, term, R, ve); + lbool got = m_mon.solve_and(mems, nullptr); bool ok = (got == expected); if (!ok) ++m_fail; std::cout << (ok ? " OK " : " FAIL ") << name @@ -167,7 +178,9 @@ class seq_monadic_test { void check_witness(char const* name, expr* term, expr* R, obj_map const& ve) { obj_map model; - lbool got = m_mon.solve(term, R, ve, &model); + vector> mems; + add_extra(mems, term, R, ve); + lbool got = m_mon.solve_and(mems, &model); bool ok = (got == l_true) && !model.empty(); if (ok) { expr_safe_replace rep(m); @@ -185,8 +198,7 @@ class seq_monadic_test { // decide a conjunction of memberships jointly (shared variables constrained together). void check_and(char const* name, vector> const& mems, lbool expected) { - obj_map nove; - lbool got = m_mon.solve_and(mems, nove, nullptr); + lbool got = m_mon.solve_and(mems, nullptr); bool ok = (got == expected); if (!ok) ++m_fail; std::cout << (ok ? " OK " : " FAIL ") << name diff --git a/src/test/seq_monadic_bench.cpp b/src/test/seq_monadic_bench.cpp index 36609dad31..071cc5f536 100644 --- a/src/test/seq_monadic_bench.cpp +++ b/src/test/seq_monadic_bench.cpp @@ -137,11 +137,10 @@ lbool run_file( for (auto const& entry : var_re) memberships.push_back(std::make_pair(entry.m_key, entry.m_value)); - obj_map no_extra; auto start = std::chrono::high_resolution_clock::now(); lbool verdict = memberships.empty() ? l_undef - : mon.solve_and(memberships, no_extra, nullptr); + : mon.solve_and(memberships, nullptr); solve_ms = std::chrono::duration( std::chrono::high_resolution_clock::now() - start).count(); return verdict;