mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 19:32:04 +00:00
Code Activity

Track FI lemma in core; remove bailout_lemma

Browse source
This commit is contained in:
Jakob Rath 2021-09-14 11:01:06 +02:00
parent d36a658139
commit d935714874
2 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/polysat/conflict_core.cpp
View file

@ -68,7 +68,6 @@ namespace polysat {
m_conflict_var = null_var; m_conflict_var = null_var;
m_saturation_premises.reset(); m_saturation_premises.reset();
m_bailout = false; m_bailout = false;
m_bailout_lemma.reset();
SASSERT(empty()); SASSERT(empty());
} }
@ -245,10 +244,7 @@ namespace polysat {
} }
clause_builder conflict_core::build_lemma() { clause_builder conflict_core::build_lemma() {
if (m_bailout_lemma) return build_core_lemma();
return *std::move(m_bailout_lemma);
else
return build_core_lemma();
} }
bool conflict_core::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) { bool conflict_core::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {
@ -257,15 +253,20 @@ namespace polysat {
// - cjust_v contains true constraints // - cjust_v contains true constraints
// - core contains both false and true constraints (originally only false ones, but additional true ones may come from saturation) // - core contains both false and true constraints (originally only false ones, but additional true ones may come from saturation)
if (is_bailout()) if (is_bailout()) // TODO: don't we still need to track cjust/m_vars?
return false; return false;
if (conflict_var() == v) { if (conflict_var() == v) {
clause_builder lemma(s()); clause_builder lemma(s());
forbidden_intervals fi; forbidden_intervals fi;
if (fi.perform(s(), v, cjust_v, lemma)) { if (fi.perform(s(), v, cjust_v, lemma)) {
// TODO: pass core to FI instead of a clause_builder?
reset();
for (auto lit : lemma) {
auto c = cm().lookup(lit);
insert(~c);
}
set_bailout(); set_bailout();
m_bailout_lemma = std::move(lemma);
return true; return true;
} }
// TODO: add a dummy value for v? // TODO: add a dummy value for v?

1
src/math/polysat/conflict_core.h
View file

@ -51,7 +51,6 @@ namespace polysat {
/** Whether we are in a bailout state. We enter a bailout state when we give up on proper conflict resolution. */ /** Whether we are in a bailout state. We enter a bailout state when we give up on proper conflict resolution. */
bool m_bailout = false; bool m_bailout = false;
std::optional<clause_builder> m_bailout_lemma;
solver* m_solver = nullptr; solver* m_solver = nullptr;
solver& s() const { return *m_solver; } solver& s() const { return *m_solver; }