mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-02 20:23:27 +00:00
Code Activity

seq_monadic: add unsat-core extraction with minimization toggle

Browse source 
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
This commit is contained in:
Nikolaj Bjorner 2026-07-31 20:53:30 -07:00
parent 1e09b4e6ae
commit 1ba30df028
3 changed files with 141 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

80
src/test/seq_monadic.cpp
View file

@ -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);