mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 22:03:39 +00:00
Code Activity

re-enable saturation engine

Browse source
This commit is contained in:
Jakob Rath 2021-09-08 16:55:34 +02:00
parent 75bac21574
commit 6766c1c349
1 changed files with 10 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -30,8 +30,7 @@ namespace polysat {
for (auto* engine : ex_engines) for (auto* engine : ex_engines)
engine->set_solver(s); engine->set_solver(s);
ve_engines.push_back(alloc(ve_reduction)); ve_engines.push_back(alloc(ve_reduction));
// ve_engines.push_back(alloc(ve_forbidden_intervals)); inf_engines.push_back(alloc(inf_saturate));
// inf_engines.push_back(alloc(inf_polynomial_superposition));
for (auto* engine : inf_engines) for (auto* engine : inf_engines)
engine->set_solver(s); engine->set_solver(s);
} }
@ -253,15 +252,15 @@ namespace polysat {
m_solver->assign_core(v, m_solver->m_value[v], justification::propagation(m_solver->m_level)); m_solver->assign_core(v, m_solver->m_value[v], justification::propagation(m_solver->m_level));
} }
*/ */
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, *this, lemma)) { if (fi.perform(s(), v, *this, lemma)) {
set_bailout(); set_bailout();
m_bailout_lemma = std::move(lemma); m_bailout_lemma = std::move(lemma);
return true; return true;
} }
} }
for (auto c : cjust_v) for (auto c : cjust_v)
insert(c); insert(c);