From a6c122da21b3d5b9c37d9ec670dec766eaff7001 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 3 Feb 2021 12:11:26 -0300
Subject: [proof-new] Fix MACRO_RESOLUTION expansion for singleton clause
 corner case (#5850)

Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which the resulting clause from crowding literal elimination is a singleton. This commit makes the expansion code robust to that and adds an example of a problematic benchmark as a regression.

Also improves a bit tracing and some comments.
---
 src/smt/proof_post_processor.cpp | 38 ++++++++++++++++++++++++++++----------
 1 file changed, 28 insertions(+), 10 deletions(-)

(limited to 'src/smt/proof_post_processor.cpp')

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 4b1a05e0f..ab8dd8f92 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -137,6 +137,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
     const std::vector<Node>& args,
     CDProof* cdp)
 {
+  Trace("smt-proof-pp-debug2") << push;
   NodeManager* nm = NodeManager::currentNM();
   Node trueNode = nm->mkConst(true);
   // get crowding lits and the position of the last clause that includes
@@ -164,10 +165,10 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
       size_t j;
       for (j = children.size() - 1; j > 0; --j)
       {
-        // notice that only non-unit clauses may be introducing the crowding
-        // literal, so we only care about non-unit OR nodes. We check then
-        // against the kind and whether the whole OR node occurs as a pivot of
-        // the respective resolution
+        // notice that only non-singleton clauses may be introducing the
+        // crowding literal, so we only care about non-singleton OR nodes. We
+        // check then against the kind and whether the whole OR node occurs as a
+        // pivot of the respective resolution
         if (children[j - 1].getKind() != kind::OR)
         {
           continue;
@@ -376,6 +377,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
     Trace("smt-proof-pp-debug2")
         << "nextGuardedElimPos: " << nextGuardedElimPos << "\n";
   } while (true);
+  Trace("smt-proof-pp-debug2") << pop;
   return lastClause;
 }
 
@@ -659,10 +661,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
                                           chainConclusion.end()};
     std::set<Node> chainConclusionLitsSet{chainConclusion.begin(),
                                           chainConclusion.end()};
-    // is args[0] a unit clause? If it's not an OR node, then yes. Otherwise,
-    // it's only a unit if it occurs in chainConclusionLitsSet
+    // is args[0] a singleton clause? If it's not an OR node, then yes.
+    // Otherwise, it's only a singleton if it occurs in chainConclusionLitsSet
     std::vector<Node> conclusionLits;
-    // whether conclusion is unit
+    // whether conclusion is singleton
     if (chainConclusionLitsSet.count(args[0]))
     {
       conclusionLits.push_back(args[0]);
@@ -684,16 +686,32 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
           chainConclusionLits, conclusionLits, children, args, cdp);
       // update vector of lits. Note that the set is no longer used, so we don't
       // need to update it
+      //
+      // We need again to check whether chainConclusion is a singleton
+      // clause. As above, it's a singleton if it's in the original
+      // chainConclusionLitsSet.
       chainConclusionLits.clear();
-      chainConclusionLits.insert(chainConclusionLits.end(),
-                                 chainConclusion.begin(),
-                                 chainConclusion.end());
+      if (chainConclusionLitsSet.count(chainConclusion))
+      {
+        chainConclusionLits.push_back(chainConclusion);
+      }
+      else
+      {
+        Assert(chainConclusion.getKind() == kind::OR);
+        chainConclusionLits.insert(chainConclusionLits.end(),
+                                   chainConclusion.begin(),
+                                   chainConclusion.end());
+      }
     }
     else
     {
       cdp->addStep(
           chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs);
     }
+    Trace("smt-proof-pp-debug")
+        << "Conclusion after chain_res/elimCrowd: " << chainConclusion << "\n";
+    Trace("smt-proof-pp-debug")
+        << "Conclusion lits: " << chainConclusionLits << "\n";
     // Placeholder for running conclusion
     Node n = chainConclusion;
     // factoring
-- 
cgit v1.2.3