From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 21 Mar 2022 14:41:54 +0000 (-0500)
Subject: Fix learned literals for top-level AND (#8336)
X-Git-Tag: cvc5-1.0.0~222
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b63c05876c2b5f2cd8c26beb85b8e1bee10344c3;p=cvc5.git

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 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<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))
     {