mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Add note as comment

Browse source
This commit is contained in:
Jakob Rath 2022-10-07 16:29:14 +02:00
parent 23a747235d
commit e7c9a99d08
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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<signed_constraint> cs) {