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

commenting on anachornistic propagation code

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-04-17 16:21:58 -07:00
parent 8c67c23883
commit 8db3b537b1
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/solver.cpp
View file

@ -259,6 +259,14 @@ namespace polysat {
// - When building the viable lemma, one of the linking constraints happens to be L // - When building the viable lemma, one of the linking constraints happens to be L
// - L is bool-true but eval-false --> we actually have a bool/eval conflict that we didn't detect // - L is bool-true but eval-false --> we actually have a bool/eval conflict that we didn't detect
// - the viable lemma is problematic because L is bool-true // - the viable lemma is problematic because L is bool-true
// NSB comment:
// It seems the core of the issue is that conflict resolution should have identified
// L as the top-most literal that the conflict depends on instead of using L'.
// The conflict state includes the propagation of values that could be triggered by L.
// Take the SAT solver analogy, conflict resolution walks the assignment stack to find the
// youngest assignment that is part of the conflict. It then starts resolving against the youngest
// literal assignment.
auto const& item = m_search[eval_qhead++]; auto const& item = m_search[eval_qhead++];
if (item.is_assignment()) { if (item.is_assignment()) {
// LOG_H1("P2: eval pvar v" << item.var()); // LOG_H1("P2: eval pvar v" << item.var());