mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-28 11:28:49 +00:00
Code Activity

Conflicts are not reported correctly in eager regex factorization

Browse source
This commit is contained in:
CEisenhofer 2026-06-09 16:14:25 +02:00
parent 64f422abc5
commit 8229bcc5fc
1 changed files with 10 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/smt/theory_nseq.cpp
View file

@ -247,7 +247,7 @@ namespace smt {
switch (m_rewriter.some_seq_in_re(r, s)) { switch (m_rewriter.some_seq_in_re(r, s)) {
case l_false: { case l_false: {
enode_pair_vector eqs; enode_pair_vector eqs;
auto lit = mk_eq(e1, e2, false); const auto lit = mk_eq(e1, e2, false);
literal_vector lits; literal_vector lits;
lits.push_back(~lit); lits.push_back(~lit);
set_conflict(eqs, lits); set_conflict(eqs, lits);
@ -269,8 +269,8 @@ namespace smt {
euf::snode *s2 = get_snode(e2); euf::snode *s2 = get_snode(e2);
const seq::dep_tracker dep = nullptr; const seq::dep_tracker dep = nullptr;
ctx.push_trail(restore_vector(m_prop_queue)); ctx.push_trail(restore_vector(m_prop_queue));
expr_ref eq_expr(m.mk_not(m.mk_eq(e1, e2)), m); const expr_ref eq_expr(m.mk_eq(e1, e2), m);
m_prop_queue.push_back(deq_item(s1, s2, ctx.get_literal(eq_expr), dep)); m_prop_queue.push_back(deq_item(s1, s2, ~ctx.get_literal(eq_expr), dep));
m_last_constraint_added = ctx.get_scope_level(); m_last_constraint_added = ctx.get_scope_level();
m_can_hot_restart = false; m_can_hot_restart = false;
} }
@ -577,7 +577,7 @@ namespace smt {
if (pairs.empty()) { if (pairs.empty()) {
// no viable splits // no viable splits
literal_vector lits; literal_vector lits;
lits.push_back(~mem.lit); lits.push_back(mem.lit);
set_conflict(lits); set_conflict(lits);
return; return;
} }
@ -1155,25 +1155,12 @@ namespace smt {
SASSERT(eq.first->get_root() == eq.second->get_root()); SASSERT(eq.first->get_root() == eq.second->get_root());
}; };
bool all_true = all_of(lits, [&](auto lit) { return ctx.get_assignment(lit) == l_true; }); SASSERT(all_of(lits, [&](auto lit) { return ctx.get_assignment(lit) == l_true; }));
if (all_true) { ctx.set_conflict(
ctx.set_conflict( ctx.mk_justification(
ctx.mk_justification( ext_theory_conflict_justification(
ext_theory_conflict_justification( get_id(), ctx, lits.size(), lits.data(), eqs.size(), eqs.data(), 0, nullptr)));
get_id(), ctx, lits.size(), lits.data(), eqs.size(), eqs.data(), 0, nullptr)));
}
else {
literal_vector clause;
for (literal lit : lits)
clause.push_back(~lit);
for (auto [a, b] : eqs)
clause.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
for (auto lit : clause)
ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), clause.size(), clause.data());
}
} }
void theory_nseq::set_propagate(enode_pair_vector const& eqs, literal_vector const& lits, literal p) { void theory_nseq::set_propagate(enode_pair_vector const& eqs, literal_vector const& lits, literal p) {
@ -1599,7 +1586,7 @@ namespace smt {
// Intersection is empty → the memberships on this variable are // Intersection is empty → the memberships on this variable are
// jointly unsatisfiable. Assert a conflict from all their literals. // jointly unsatisfiable. Assert a conflict from all their literals.
literal_vector lits; literal_vector lits;
for (unsigned i : mem_indices) { for (const unsigned i : mem_indices) {
SASSERT(ctx.get_assignment(mems[i]->lit) == l_true); // we already stored the polarity of the literal SASSERT(ctx.get_assignment(mems[i]->lit) == l_true); // we already stored the polarity of the literal
lits.push_back(mems[i]->lit); lits.push_back(mems[i]->lit);
} }