seq_monadic: add unsat-core extraction with minimization toggle

check() now records the dependencies of an unsat subset in m_core, exposed via
ptr_vector<u_dependency> const& core(). On l_false it calls minimize_core:
with the new m_min_core flag (set_min_core, default true) it deletion-minimizes
to a minimal unsat subset containing only constraints that participate in the
contradiction; with the flag off it returns all membership dependencies.

Add unit tests asserting the core omits irrelevant constraints (e.g. x in a*,
x in ~a*, y in b* has core {x-constraints} only), exercising both flag states.
The test harness runs with minimization disabled by default.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9

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<std::tuple<expr_ref, expr_ref, u_dependency*>> const& memberships) {
     m_model.reset();
-    vector<std::tuple<expr_ref, expr_ref, u_dependency*>> 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<std::tuple<expr_ref, expr_ref, u_dependency*>> 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<std::tuple<expr_ref, expr_ref, u_dependency*>> keep(memberships);
+    unsigned i = 0;
+    while (i < keep.size()) {
+        vector<std::tuple<expr_ref, expr_ref, u_dependency*>> 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<std::tuple<expr_ref, expr_ref, u_dependency*>> memberships;
+    memberships.swap(m_memberships);              // consume the asserted memberships
+    lbool r = decide(memberships);
+    if (r == l_false)
+        minimize_core(memberships);
+    return r;
+}

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<expr, expr*> m_model;           // last extracted model (var -> witness); see get_model()
     obj_map<expr, expr_ref_pair_vector*> m_cofactor_cache;  // memoizes derivative_cofactors per regex
     vector<std::tuple<expr_ref, expr_ref, u_dependency*>> m_memberships;  // asserted (term in regex, dep) for check()
+    ptr_vector<u_dependency> 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<disjunct> 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<std::tuple<expr_ref, expr_ref, u_dependency*>> 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<std::tuple<expr_ref, expr_ref, u_dependency*>> 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<u_dependency> const& core() const { return m_core; }
 };

src/test/seq_monadic.cpp

@@ -25,6 +25,7 @@ Author:
 #include "ast/rewriter/seq_monadic.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include <iostream>
+#include <set>
 
 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<unsigned>& 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<std::pair<expr*, expr*>> const& mems,
+                    std::set<unsigned> const& expected_core) {
+        m_mon.set_gen_model(false);
+        std::set<unsigned> 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<unsigned> 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<std::pair<expr*, expr*>> 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<unsigned>{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<std::pair<expr*, expr*>> 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<unsigned>{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<std::pair<expr*, expr*>> 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<unsigned>{1, 2});
+        }
+
         std::cout << "=== seq_monadic: " << (m_fail == 0 ? "ALL PASS" : "FAILURES") << " ("
                   << m_fail << " fail) ===\n";
         ENSURE(m_fail == 0);