From ee64bf27d10a014a71e12023b27788c62429f11e Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Sat, 18 Mar 2023 07:58:55 +0100 Subject: [PATCH] correct version of reverted commit --- src/math/polysat/conflict.cpp | 23 +++++------------------ 1 file changed, 5 insertions(+), 18 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 55349a66d..6ebca4a3b 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -393,29 +393,16 @@ namespace polysat { unsigned const lvl = s.m_bvars.level(lit); signed_constraint c = s.lit2cnstr(lit); - // If evaluation depends on a decision, - // then we rather keep the more general constraint c instead of inserting "x = v" - // TODO: the old implementation based on bail_vars is broken because it may skip relevant decisions. - // is there a way to keep the same effect by adding a side lemma at this point? - bool has_decision = false; -#if 0 - for (pvar v : c->vars()) - if (s.is_assigned(v) && s.m_justification[v].is_decision()) - m_bail_vars.insert(v), has_decision = true; -#endif - - if (!has_decision) { - unsigned const eval_idx = s.m_search.get_bool_index(lit); - for (pvar v : c->vars()) { - if (s.is_assigned(v) && s.m_search.get_pvar_index(v) <= eval_idx) { - m_vars.insert(v); + unsigned const eval_idx = s.m_search.get_bool_index(lit); + for (pvar v : c->vars()) { + if (s.is_assigned(v) && s.m_search.get_pvar_index(v) <= eval_idx) { + m_vars.insert(v); // TODO - figure out what to do with constraints from conflict lemma that disappear here. // if (s.m_bvars.is_false(lit)) // m_resolver->infer_lemmas_for_value(v, ~c, *this); - } } - remove(c); } + remove(c); SASSERT(!contains(lit)); SASSERT(!contains(~lit));