From e7c9a99d08ea07fac4f3213fe02667351f7b8830 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 7 Oct 2022 16:29:14 +0200 Subject: [PATCH] Add note as comment --- src/math/polysat/conflict.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 3041fb0c6..6b621c4f7 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -331,6 +331,14 @@ namespace polysat { lemma->set_redundant(true); LOG("Side lemma: " << *lemma); m_lemmas.push_back(std::move(lemma)); + // If possible, we should set the new constraint to l_true; + // and re-enable the assertions marked with "tag:true_by_side_lemma". + // Or we adjust the conflict invariant: + // - l_true constraints is the default case as before, + // - l_undef constraints are new and justified by some side lemma, but + // should be treated by the conflict resolution methods like l_true + // constraints, + // - l_false constraints are disallowed in the conflict (as before). } void conflict::add_lemma(std::initializer_list cs) {