diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 0d7fa00cf9..6e966e4618 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -424,10 +424,8 @@ 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() { +lbool seq_monadic::decide(vector> const& memberships) { 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(); @@ -463,3 +461,42 @@ lbool seq_monadic::check() { } return decide_dnf(combined); } + +void seq_monadic::minimize_core(vector> const& memberships) { + m_core.reset(); + if (!m_min_core) { + // No minimization: the core is simply every asserted membership's dependency. + for (auto const& [term, regex, d] : memberships) + if (d) + m_core.push_back(d); + return; + } + // Deletion-based minimization: start from the full unsat set and try to drop each + // membership; a membership is kept only if removing it makes the set no longer + // provably unsat. The result is a minimal unsat subset (relevant constraints only). + vector> keep(memberships); + unsigned i = 0; + while (i < keep.size()) { + vector> trial; + for (unsigned j = 0; j < keep.size(); ++j) + if (j != i) + trial.push_back(keep[j]); + if (decide(trial) == l_false) + keep.swap(trial); // membership i is not needed for unsat + else + ++i; // membership i is needed; keep it + } + for (auto const& [term, regex, d] : keep) + if (d) + m_core.push_back(d); +} + +lbool seq_monadic::check() { + m_core.reset(); + vector> memberships; + memberships.swap(m_memberships); // consume the asserted memberships + lbool r = decide(memberships); + if (r == l_false) + minimize_core(memberships); + return r; +} diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 37340b6e2a..8410554993 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -80,9 +80,11 @@ private: 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()/check() extract a feasible model + bool m_min_core = true; // whether check() minimizes the unsat core (else: all deps) 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() + ptr_vector m_core; // dependencies of an unsat subset, filled by check() on l_false seq_util& u() const { return m_rw.u(); } seq_util::rex& re() const { return m_rw.u().re; } @@ -141,6 +143,15 @@ private: // (var -> witness). lbool decide_dnf(vector const& dnf); + // Decide a CONJUNCTION of memberships jointly (the core algorithm behind check()): + // multiplies the per-membership DNFs and decides emptiness. Does not touch + // m_memberships or m_core; fills m_model on l_true when model generation is enabled. + lbool decide(vector> const& memberships); + + // Given an unsatisfiable membership set, extract a minimal unsatisfiable subset by + // deletion and collect the (non-null) dependencies of its members into m_core. + void minimize_core(vector> const& memberships); + public: seq_monadic(seq_rewriter& rw, transition_mode mode = transition_mode::light_antimirov) : m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_mode(mode), m_pin(rw.m()) {} @@ -164,6 +175,10 @@ public: // l_true = sat, l_false = unsat, l_undef = unsupported shape / gave up. lbool solve(expr* term, expr* R); + // Enable/disable unsat-core minimization (default: enabled). When disabled, core() + // returns the dependencies of all asserted memberships (no deletion-based shrinking). + void set_min_core(bool b) { m_min_core = b; } + // 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. @@ -176,6 +191,11 @@ public: // union of DNFs; a negated membership ~(t in R) is just t in complement(R)). // 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. + // l_false = unsat, l_undef = gave up. On l_false, core() holds the dependencies + // of a minimal unsatisfiable subset. lbool check(); + + // Dependencies of a minimal unsatisfiable subset from the last check() that returned + // l_false (nullptr dependencies are omitted). Empty otherwise. + ptr_vector const& core() const { return m_core; } }; diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index c42c1d84ae..bf970499d5 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -25,6 +25,7 @@ Author: #include "ast/rewriter/seq_monadic.h" #include "ast/rewriter/expr_safe_replace.h" #include +#include namespace { @@ -41,6 +42,7 @@ class seq_monadic_test { sort_ref m_str; // String sort sort_ref m_re; // RegEx sort over m_str seq_monadic::transition_mode m_mode; + u_dependency_manager m_dm; // owns the leaf dependencies used in unsat-core tests unsigned m_fail = 0; seq_util::rex& re() { return u.re; } @@ -208,11 +210,56 @@ class seq_monadic_test { << " got=" << s(got) << " expected=" << s(expected) << "\n"; } + // collect the core ids after a check() into `ids`. + void core_ids(std::set& ids) { + ids.clear(); + for (u_dependency* d : m_mon.core()) + ids.insert(d->leaf_value()); + } + + // Assert each membership with a distinct leaf dependency (id = its index) and expect + // the conjunction to be UNSAT. With minimization ON, core() must be exactly + // `expected_core` (irrelevant constraints omitted); with minimization OFF, core() + // must be all membership dependencies. + void check_core(char const* name, vector> const& mems, + std::set const& expected_core) { + m_mon.set_gen_model(false); + std::set all_ids, got_ids; + for (unsigned i = 0; i < mems.size(); ++i) + all_ids.insert(i); + + // minimization disabled: the core is every asserted membership's dependency. + m_mon.set_min_core(false); + for (unsigned i = 0; i < mems.size(); ++i) + m_mon.add(mems[i].first, mems[i].second, m_dm.mk_leaf(i)); + lbool got0 = m_mon.check(); + core_ids(got_ids); + bool ok0 = (got0 == l_false) && (got_ids == all_ids); + + // minimization enabled: the core drops constraints irrelevant to the conflict. + m_mon.set_min_core(true); + for (unsigned i = 0; i < mems.size(); ++i) + m_mon.add(mems[i].first, mems[i].second, m_dm.mk_leaf(i)); + lbool got1 = m_mon.check(); + std::set min_ids; + core_ids(min_ids); + bool ok1 = (got1 == l_false) && (min_ids == expected_core); + m_mon.set_min_core(false); // restore the harness default + + bool ok = ok0 && ok1; + if (!ok) ++m_fail; + std::cout << (ok ? " OK " : " FAIL ") << name << " got=" << s(got1) << " core={"; + bool first = true; + for (unsigned id : min_ids) { std::cout << (first ? "" : ",") << id; first = false; } + std::cout << "} full=" << (ok0 ? "yes" : "no") << "\n"; + } + public: seq_monadic_test(seq_monadic::transition_mode mode) : m_reg(m), m_rw(m), m_mon(m_rw, mode), u(m), m_str(m), m_re(m), m_mode(mode) { m_str = u.str.mk_string_sort(); m_re = re().mk_re(m_str); + m_mon.set_min_core(false); // tests use unminimized cores by default } void run() { @@ -368,6 +415,39 @@ public: mSat2.push_back(std::make_pair((expr*)tYbX.get(), (expr*)abStar.get())); check_and("x.a.y & y.b.x in (a|b)*", mSat2, l_true); + // ---- unsat cores: the extracted core must contain only constraints that + // ---- participate in the contradiction, not independent ones. + std::cout << "=== seq_monadic: unsat cores ===\n"; + // x in a* /\ x in ~(a*) /\ y in b* -> unsat over x; core = {0,1}, not the y-constraint. + { + expr_ref aStar(star(a), m), naStar(comp(star(a)), m), bStar(star(b), m); + vector> ms; + ms.push_back(std::make_pair((expr*)x.get(), (expr*)aStar.get())); + ms.push_back(std::make_pair((expr*)x.get(), (expr*)naStar.get())); + ms.push_back(std::make_pair((expr*)y.get(), (expr*)bStar.get())); + check_core("x in a* & x in ~a* (& y in b*)", ms, std::set{0, 1}); + } + // x in (aa)* /\ x in a(aa)* /\ y in Sigma* -> unsat over x; core = {0,1}. + { + expr_ref aaS(star(cat(a, a)), m), a_aaS(cat(a, star(cat(a, a))), m), sigStar(dotstar(), m); + vector> ms; + ms.push_back(std::make_pair((expr*)x.get(), (expr*)aaS.get())); + ms.push_back(std::make_pair((expr*)x.get(), (expr*)a_aaS.get())); + ms.push_back(std::make_pair((expr*)y.get(), (expr*)sigStar.get())); + check_core("x in (aa)* & x in a(aa)* (& y in Sig*)", ms, std::set{0, 1}); + } + // Three independent constraints, contradiction only between the middle two: + // z in a* (indep) /\ x in b* /\ x in a+ (x=empty allowed by b*, a+ forbids empty) + { + expr_ref z = var("z"); + expr_ref aStarZ(star(a), m), bStarX(star(b), m), aP(cat(a, star(a)), m); // a+ = at least one a + vector> ms; + ms.push_back(std::make_pair((expr*)z.get(), (expr*)aStarZ.get())); // 0: irrelevant + ms.push_back(std::make_pair((expr*)x.get(), (expr*)bStarX.get())); // 1: x in b* + ms.push_back(std::make_pair((expr*)x.get(), (expr*)aP.get())); // 2: x in a+ + check_core("z in a* (& x in b* & x in a+)", ms, std::set{1, 2}); + } + std::cout << "=== seq_monadic: " << (m_fail == 0 ? "ALL PASS" : "FAILURES") << " (" << m_fail << " fail) ===\n"; ENSURE(m_fail == 0);