From b63c05876c2b5f2cd8c26beb85b8e1bee10344c3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 21 Mar 2022 09:41:54 -0500 Subject: [PATCH] Fix learned literals for top-level AND (#8336) This is important for a deep restart strategy where substitutions may be consolidated by the preprocessor to a single AND. --- src/prop/zero_level_learner.cpp | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp index f71cacbe9..6d2752ea6 100644 --- a/src/prop/zero_level_learner.cpp +++ b/src/prop/zero_level_learner.cpp @@ -71,14 +71,24 @@ void ZeroLevelLearner::notifyInputFormulas( { d_assertNoLearnCount = 0; std::unordered_set visited; - // We consider top level literals of assertions to be the preprocessed - // learned literals only, and not the literals tracked by the preprocessor + // We consider top level literals of assertions, including those occurring + // as children of AND to be the preprocessed learned literals only, and not + // the literals tracked by the preprocessor // (Preprocessor::getLearnedLiterals). This means that a learned literal from // e.g. circuit propagation that is not trivially a top level assertion will // be considered an ordinary learned literal. // Note that d_pplAtoms and d_ppnAtoms are disjoint - for (const Node& lit : assertions) + std::vector toProcess = assertions; + size_t index = 0; + while (index < toProcess.size()) { + TNode lit = toProcess[index]; + index++; + if (lit.getKind() == kind::AND) + { + toProcess.insert(toProcess.end(), lit.begin(), lit.end()); + continue; + } TNode atom = lit.getKind() == kind::NOT ? lit[0] : lit; if (expr::isBooleanConnective(atom)) { -- 2.30.2