mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-01 17:03:18 +00:00
Code Activity

each overlapping variable needs to be explained only once

Browse source
This commit is contained in:
Jakob Rath 2023-12-01 15:47:54 +01:00
parent e1d23642bc
commit 6ce63154d2
1 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/math/polysat/viable.cpp
View file

@ -1973,15 +1973,20 @@ namespace polysat {
// e.g.: v^2 + w^2 == 0; w := 1 // e.g.: v^2 + w^2 == 0; w := 1
// - but we could use side constraints on the coefficients instead (coefficients when viewed as polynomial over v): // - but we could use side constraints on the coefficients instead (coefficients when viewed as polynomial over v):
// e.g.: v^2 + w^2 == 0; w^2 == 1 // e.g.: v^2 + w^2 == 0; w^2 == 1
uint_set to_explain;
for (unsigned d : us.unsat_core()) { for (unsigned d : us.unsat_core()) {
auto [x, lit] = deps[d]; auto [x, lit] = deps[d];
s.m_slicing.explain_simple_overlap(v, x, [this, &core](sat::literal l) { if (x != v)
core.insert(s.lit2cnstr(l)); to_explain.insert(x);
});
signed_constraint c = s.lit2cnstr(lit); signed_constraint c = s.lit2cnstr(lit);
core.insert(c); core.insert(c);
core.insert_vars(c); core.insert_vars(c);
} }
for (pvar x : to_explain) {
s.m_slicing.explain_simple_overlap(v, x, [this, &core](sat::literal l) {
core.insert(s.lit2cnstr(l));
});
}
SASSERT(!core.vars().contains(v)); SASSERT(!core.vars().contains(v));
core.add_lemma("viable unsat core", core.build_lemma()); core.add_lemma("viable unsat core", core.build_lemma());
IF_VERBOSE(10, verbose_stream() << "unsat core " << core << "\n";); IF_VERBOSE(10, verbose_stream() << "unsat core " << core << "\n";);