diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 18661651e1..0d7fa00cf9 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -420,9 +420,16 @@ lbool seq_monadic::decide_dnf(vector const& dnf) { return any_undef ? l_undef : l_false; } -lbool seq_monadic::solve_and(vector> const& mems) { - if (mems.empty()) - return l_undef; +void seq_monadic::add(expr* term, expr* regex, u_dependency* d) { + m_memberships.push_back({ expr_ref(term, m), expr_ref(regex, m), d }); +} + +lbool seq_monadic::check() { + m_model.reset(); + vector> memberships; + memberships.swap(m_memberships); // consume the asserted memberships + if (memberships.empty()) + return l_true; // empty conjunction is vacuously true m_pin.reset(); reset_cofactor_cache(); m_budget = 200000; @@ -434,16 +441,16 @@ lbool seq_monadic::solve_and(vector> const& mems) { vector combined; combined.push_back(disjunct()); // { true } const unsigned DNF_CAP = 1u << 14; - for (auto const& tr : mems) { + for (auto const& [term, regex, d] : memberships) { vector dnf_i; - if (!build_membership_dnf(tr.first, tr.second, dnf_i)) + if (!build_membership_dnf(term, regex, dnf_i)) return l_undef; vector next; - for (disjunct const& d : combined) { + for (disjunct const& cd : combined) { for (disjunct const& e : dnf_i) { if (next.size() > DNF_CAP || m_budget == 0) { m_giveup = true; return l_undef; } --m_budget; - disjunct D(d); + disjunct D(cd); for (auto const& c : e) D.push_back(c); next.push_back(D); diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 29231f2024..37340b6e2a 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -43,7 +43,7 @@ Abstract: 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`. + membership passed to `add` and decided by `check`. Author: @@ -57,7 +57,9 @@ Author: #include "ast/rewriter/th_rewriter.h" #include "util/lbool.h" #include "util/obj_hashtable.h" +#include "util/dependency.h" #include +#include class seq_monadic { public: @@ -77,9 +79,10 @@ private: expr_ref_vector m_pin; // pins derivative states / witnesses referenced later unsigned m_budget = 0; // global work budget (decompose disjuncts + product pops) bool m_giveup = false; // set when the budget is exhausted - bool m_gen_model = true; // whether solve()/solve_and() extract a feasible model + bool m_gen_model = true; // whether solve()/check() extract a feasible model obj_map m_model; // last extracted model (var -> witness); see get_model() obj_map m_cofactor_cache; // memoizes derivative_cofactors per regex + vector> m_memberships; // asserted (term in regex, dep) for check() seq_util& u() const { return m_rw.u(); } seq_util::rex& re() const { return m_rw.u().re; } @@ -100,7 +103,7 @@ private: // Symbolic transition cofactors in the selected mode. Memoized per regex `r`: the // returned vector is owned by the cofactor cache and stays valid until the next - // top-level solve()/solve_and() (which resets the cache). + // top-level solve()/check() (which resets the cache). expr_ref_pair_vector const& derivative_cofactors(expr* r); // Drop all memoized cofactors and free their owned vectors. @@ -147,13 +150,13 @@ public: transition_mode mode() const { return m_mode; } // Enable/disable model generation (default: enabled). When enabled, a successful - // solve()/solve_and() extracts a feasible model retrievable via get_model(). + // solve()/check() extracts a feasible model retrievable via get_model(). void set_gen_model(bool b) { m_gen_model = b; } - // The model extracted by the last successful solve()/solve_and(): var -> witness, + // The model extracted by the last successful solve()/check(): 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 solve()/solve_and(). Only valid when model generation is enabled. + // until the next solve()/check(). Only valid when model generation is enabled. obj_map const& get_model() const { return m_model; } // Decide (str.in_re term R) for a term that is a concatenation of string variables @@ -161,12 +164,18 @@ public: // l_true = sat, l_false = unsat, l_undef = unsupported shape / gave up. lbool solve(expr* term, expr* R); - // Decide a CONJUNCTION of memberships AND_i (term_i in R_i) jointly: a variable + // Assert a membership (term in regex) to be decided jointly by the next check(). + // `d` carries the dependency used for unsat-core tracking and may be nullptr. + // Memberships accumulate until check() consumes them. + void add(expr* term, expr* regex, u_dependency* d); + + // Decide the CONJUNCTION of all memberships asserted via add() 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)). - // Per-variable extra constraints are expressed here as extra memberships (v in R'). - // l_true = sat, l_false = unsat, l_undef = gave up. - lbool solve_and(vector> const& mems); + // Per-variable extra constraints are expressed as extra memberships (v in R'). + // Consumes the asserted memberships. l_true = sat (empty conjunction is sat), + // l_false = unsat, l_undef = gave up. + lbool check(); }; diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index 7bf05bbf98..c42c1d84ae 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -129,21 +129,19 @@ 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)); + // assert the membership list: the primary (term in R) plus one (var in R') per extra + // constraint, decided jointly by check(). + void add_extra(expr* term, expr* R, obj_map const& ve) { + m_mon.add(term, R, nullptr); + for (auto const& [k, v] : ve) + m_mon.add(k, v, nullptr); } void check_extra(char const* name, expr* term, expr* R, obj_map const& ve, lbool expected) { - vector> mems; - add_extra(mems, term, R, ve); + add_extra(term, R, ve); m_mon.set_gen_model(false); // this check does not use the model - lbool got = m_mon.solve_and(mems); + lbool got = m_mon.check(); bool ok = (got == expected); if (!ok) ++m_fail; std::cout << (ok ? " OK " : " FAIL ") << name @@ -179,10 +177,9 @@ class seq_monadic_test { // term a member of R (substitute var -> witness and re-decide by derivatives). void check_witness(char const* name, expr* term, expr* R, obj_map const& ve) { - vector> mems; - add_extra(mems, term, R, ve); + add_extra(term, R, ve); m_mon.set_gen_model(true); // this check verifies the extracted model - lbool got = m_mon.solve_and(mems); + lbool got = m_mon.check(); obj_map const& model = m_mon.get_model(); bool ok = (got == l_true) && !model.empty(); if (ok) { @@ -201,8 +198,10 @@ 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) { + for (auto const& [t, r] : mems) + m_mon.add(t, r, nullptr); m_mon.set_gen_model(false); // this check does not use the model - lbool got = m_mon.solve_and(mems); + lbool got = m_mon.check(); bool ok = (got == expected); if (!ok) ++m_fail; std::cout << (ok ? " OK " : " FAIL ") << name @@ -335,10 +334,10 @@ public: check_extra("([1]|[2])* & yi[2]* xi.[1].yi", xiyi, re12s, veI, l_true); check_witness("([1]|[2])* & yi[2]* xi.[1].yi", xiyi, re12s, veI); - // ---- conjunction of memberships (solve_and): a variable shared across memberships + // ---- conjunction of memberships (add + check): a variable shared across memberships // ---- is constrained jointly. These are cases that are individually SAT but // ---- jointly UNSAT -- exactly what independent per-membership solving gets wrong. - std::cout << "=== seq_monadic: conjunction of memberships (solve_and) ===\n"; + std::cout << "=== seq_monadic: conjunction of memberships (add + check) ===\n"; expr_ref aaS(star(cat(a, a)), m); // (aa)* : even number of a's expr_ref a_aaS(cat(a, star(cat(a, a))), m); // a(aa)* : odd number of a's expr_ref abS(star(ab), m); // (ab)* diff --git a/src/test/seq_monadic_bench.cpp b/src/test/seq_monadic_bench.cpp index bc343f2557..3481f2935b 100644 --- a/src/test/seq_monadic_bench.cpp +++ b/src/test/seq_monadic_bench.cpp @@ -128,20 +128,23 @@ lbool run_file( for (expr* assertion : ctx.assertions()) complete = collect(assertion) && complete; - vector> memberships; + unsigned n_added = 0; for (expr* term : terms) { expr* r = nullptr; term_re.find(term, r); - memberships.push_back(std::make_pair(term, r)); + mon.add(term, r, nullptr); + ++n_added; + } + for (auto const& [k, v] : var_re) { + mon.add(k, v, nullptr); + ++n_added; } - for (auto const& entry : var_re) - memberships.push_back(std::make_pair(entry.m_key, entry.m_value)); auto start = std::chrono::high_resolution_clock::now(); mon.set_gen_model(false); // benchmark only needs the verdict - lbool verdict = memberships.empty() + lbool verdict = n_added == 0 ? l_undef - : mon.solve_and(memberships); + : mon.check(); solve_ms = std::chrono::duration( std::chrono::high_resolution_clock::now() - start).count(); return verdict;