mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

Missing justification added

Browse source 
Added check for correctness of conflict core
This commit is contained in:
CEisenhofer 2026-04-08 10:15:27 +02:00
parent c7e7b40d40
commit 26d36ba6ee
5 changed files with 56 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/smt/seq/seq_nielsen.cpp
View file

@ -248,18 +248,24 @@ namespace seq {
}
bool nielsen_node::add_constraint(constraint const &c) {
if (graph().get_manager().is_and(c.fml)) {
auto& m = graph().get_manager();
if (m.is_and(c.fml)) {
for (const auto f : *to_app(c.fml)) {
if (!add_constraint(constraint(f, c.dep, graph().get_manager())))
if (!add_constraint(constraint(f, c.dep, m)))
return false;
}
return true;
}
expr* l, *r;
if (m.is_eq(c.fml, l, r)) {
if (l == r)
return true;
}
m_constraints.push_back(c);
if (m_graph.m_literal_if_false) {
auto lit = m_graph.m_literal_if_false(c.fml);
if (lit != sat::null_literal) {
set_external_conflict(lit);
set_external_conflict(lit, c.dep);
return false;
}
}
@ -1762,13 +1768,13 @@ namespace seq {
var = r;
def = l;
}
else if (l->is_unit() && l->arg(0)->is_var() && r->is_char_or_unit()) {
var = l->arg(0);
def = r->arg(0);
else if (l->is_unit() && r->is_char_or_unit()) {
var = l;
def = r;
}
else if (r->is_unit() && r->arg(0)->is_var() && l->is_char_or_unit()) {
var = r->arg(0);
def = l->arg(0);
else if (r->is_unit() && l->is_char_or_unit()) {
var = r;
def = l;
}
if (var) {
@ -3663,22 +3669,20 @@ namespace seq {
if (n->m_conflict_external_literal != sat::null_literal) {
// We know from the outer solver that this literal is assigned false
deps = m_dep_mgr.mk_join(deps, m_dep_mgr.mk_leaf(n->m_conflict_external_literal));
if (n->m_conflict_internal)
deps = m_dep_mgr.mk_join(deps, n->m_conflict_internal);
continue;
}
SASSERT(n->outgoing().empty());
SASSERT(n->m_conflict_internal);
deps = m_dep_mgr.mk_join(deps, n->m_conflict_internal);
// for (str_eq const& eq : n->str_eqs())
// deps = m_dep_mgr.mk_join(deps, eq.m_dep);
// for (str_mem const& mem : n->str_mems())
// deps = m_dep_mgr.mk_join(deps, mem.m_dep);
}
return deps;
}
// NSB review: this is one of several methods exposed for testing
void nielsen_graph::explain_conflict(svector<enode_pair>& eqs,
void nielsen_graph::test_aux_explain_conflict(svector<enode_pair>& eqs,
svector<sat::literal>& mem_literals) const {
SASSERT(m_root);
auto deps = collect_conflict_deps();

5
src/smt/seq/seq_nielsen.h
View file

@ -628,11 +628,12 @@ namespace seq {
m_conflict_internal = confl;
}
void set_external_conflict(sat::literal lit) {
void set_external_conflict(sat::literal lit, dep_tracker confl) {
if (m_reason != backtrack_reason::unevaluated)
return;
m_reason = backtrack_reason::external;
m_conflict_external_literal = ~lit;
m_conflict_internal = confl;
}
bool is_progress() const { return m_is_progress; }
@ -900,7 +901,7 @@ namespace seq {
// explain a conflict: partition the dep_source leaves into str_eq indices
// (kind::eq) and str_mem indices (kind::mem).
// Must be called after solve() returns unsat.
void explain_conflict(svector<enode_pair> &eqs,
void test_aux_explain_conflict(svector<enode_pair> &eqs,
svector<sat::literal> &mem_literals) const;

37
src/smt/theory_nseq.cpp
View file

@ -735,14 +735,37 @@ namespace smt {
#ifdef Z3DEBUG
#if 1
std::vector<std::pair<unsigned, unsigned>> confl;
for (auto& lit : lits) {
std::cout << mk_pp(ctx.literal2expr(lit), m) << "\n-----------\n";
// Pass constraints to a subsolver to check correctness modulo legacy solver
{
smt_params p;
p.m_string_solver = "seq";
kernel kernel(m, p);
for (seq::dep_source const& d : m_nielsen.conflict_sources()) {
if (std::holds_alternative<enode_pair>(d))
kernel.assert_expr(
m.mk_eq(
std::get<enode_pair>(d).first->get_expr(),
std::get<enode_pair>(d).second->get_expr()
)
);
else
kernel.assert_expr(ctx.literal2expr(std::get<sat::literal>(d)));
}
const auto res = kernel.check();
if (res == l_true) {
std::cout << "Insufficient justification:\n";
for (auto& lit : lits) {
std::cout << mk_pp(ctx.literal2expr(lit), m) << "\n-----------\n";
}
for (auto& eq : eqs) {
std::cout << mk_pp(eq.first->get_expr(), m) << " == " << mk_pp(eq.second->get_expr(), m) << "\n-----------\n";
}
auto dot = m_nielsen.to_dot();
std::cout << std::endl;
}
VERIFY(res != l_true);
}
for (auto& eq : eqs) {
std::cout << mk_pp(eq.first->get_expr(), m) << " == " << mk_pp(eq.second->get_expr(), m) << "\n-----------\n";
}
std::cout << std::endl;
#endif
#endif

2
src/test/nseq_basic.cpp
View file

@ -160,7 +160,7 @@ static void test_nseq_symbol_clash() {
// verify conflict explanation returns the equality index
smt::enode_pair_vector eqs;
sat::literal_vector mem_idx;
ng.explain_conflict(eqs, mem_idx);
ng.test_aux_explain_conflict(eqs, mem_idx);
SASSERT(eqs.size() == 1);
SASSERT(eqs[0].first == nullptr);
SASSERT(mem_idx.empty());

8
src/test/seq_nielsen.cpp
View file

@ -1496,7 +1496,7 @@ static void test_explain_conflict_single_eq() {
// but the conflict should still be detected
svector<seq::enode_pair> eqs;
svector<sat::literal> mem_literals;
ng.explain_conflict(eqs, mem_literals);
ng.test_aux_explain_conflict(eqs, mem_literals);
// with test-friendly overload (null deps), eqs will be empty
// the important check is that the conflict was detected
}
@ -1526,7 +1526,7 @@ static void test_explain_conflict_multi_eq() {
// the important check is that the conflict was detected
svector<seq::enode_pair> eqs;
svector<sat::literal> mem_literals;
ng.explain_conflict(eqs, mem_literals);
ng.test_aux_explain_conflict(eqs, mem_literals);
}
// test that is_extended is set after solve generates extensions
@ -2117,7 +2117,7 @@ static void test_explain_conflict_mem_only() {
// with test-friendly overload (null deps), explain_conflict won't return deps
svector<seq::enode_pair> eqs;
svector<sat::literal> mem_literals;
ng.explain_conflict(eqs, mem_literals);
ng.test_aux_explain_conflict(eqs, mem_literals);
}
// test explain_conflict: mixed eq + mem conflict
@ -2151,7 +2151,7 @@ static void test_explain_conflict_mixed_eq_mem() {
// with test-friendly overload (null deps), explain_conflict won't return deps
svector<seq::enode_pair> eqs;
svector<sat::literal> mem_literals;
ng.explain_conflict(eqs, mem_literals);
ng.test_aux_explain_conflict(eqs, mem_literals);
}
// test subsumption pruning during solve: a node whose constraint set