From fc2633c964c810bc91d26c6b56fdf9b949a7bdb9 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 13 Apr 2022 12:45:14 +0200 Subject: [PATCH] don't saturate immediately after forbidden intervals --- src/math/polysat/solver.cpp | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 71a69753a..3c3599d37 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -572,17 +572,8 @@ namespace polysat { pvar v = m_conflict.conflict_var(); // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack. // TODO: use unsat core from m_viable_fallback if the conflict is from there + // TODO: we could try simpler backtracking loop if we get a lemma from forbidden intervals VERIFY(m_viable.resolve(v, m_conflict)); - // TBD: saturate resulting conflict to get better lemmas. - LOG("try-eliminate v" << v); - if (m_conflict.try_explain(v)) - ; - else if (m_conflict.try_eliminate(v)) - ; - else - m_conflict.try_saturate(v); - - LOG("end-try-eliminate v"); } search_iterator search_it(m_search);