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.

diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp
index f71cacbe916d959967ced2d8363600a81ffca669..6d2752ea6cdca5f1d2ebbbc179fe169537d76c8b 100644 (file)
--- 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<TNode> 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<Node> 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))
     {