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

correct version of reverted commit

Browse source
This commit is contained in:
Jakob Rath 2023-03-18 07:58:55 +01:00
parent a8315e8558
commit ee64bf27d1
1 changed files with 5 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/math/polysat/conflict.cpp
View file

@ -393,29 +393,16 @@ namespace polysat {
unsigned const lvl = s.m_bvars.level(lit); unsigned const lvl = s.m_bvars.level(lit);
signed_constraint c = s.lit2cnstr(lit); signed_constraint c = s.lit2cnstr(lit);
// If evaluation depends on a decision, unsigned const eval_idx = s.m_search.get_bool_index(lit);
// then we rather keep the more general constraint c instead of inserting "x = v" for (pvar v : c->vars()) {
// TODO: the old implementation based on bail_vars is broken because it may skip relevant decisions. if (s.is_assigned(v) && s.m_search.get_pvar_index(v) <= eval_idx) {
// is there a way to keep the same effect by adding a side lemma at this point? m_vars.insert(v);
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);
// TODO - figure out what to do with constraints from conflict lemma that disappear here. // TODO - figure out what to do with constraints from conflict lemma that disappear here.
// if (s.m_bvars.is_false(lit)) // if (s.m_bvars.is_false(lit))
// m_resolver->infer_lemmas_for_value(v, ~c, *this); // m_resolver->infer_lemmas_for_value(v, ~c, *this);
}
} }
remove(c);
} }
remove(c);
SASSERT(!contains(lit)); SASSERT(!contains(lit));
SASSERT(!contains(~lit)); SASSERT(!contains(~lit));