[proofs] Fix singleton check in MACRO_RES post-processing (#7498)

Previously the check for whether the original conclusion of the MACRO_RESOULTION step was a singleton was incomplete. Now the test is made the proper way.

Depends on #7497.

Fixes cvc5/cvc5-projects#318

3 files changed, 33 insertions, 4 deletions

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index a6b5b832e..17ea2c09c 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -18,6 +18,7 @@
 #include "expr/skolem_manager.h"
 #include "options/proof_options.h"
 #include "preprocessing/assertion_pipeline.h"
+#include "proof/proof_node_algorithm.h"
 #include "proof/proof_node_manager.h"
 #include "smt/solver_engine.h"
 #include "theory/arith/arith_utilities.h"
@@ -164,6 +165,8 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
     CDProof* cdp)
 {
   Trace("smt-proof-pp-debug2") << push;
+  Trace("smt-proof-pp-debug2") << "Clause lits: " << clauseLits << "\n";
+  Trace("smt-proof-pp-debug2") << "Target lits: " << targetClauseLits << "\n\n";
   NodeManager* nm = NodeManager::currentNM();
   Node trueNode = nm->mkConst(true);
   // get crowding lits and the position of the last clause that includes
@@ -696,11 +699,29 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
                                           chainConclusion.end()};
     std::set<Node> chainConclusionLitsSet{chainConclusion.begin(),
                                           chainConclusion.end()};
-    // 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
+    Trace("smt-proof-pp-debug2")
+        << "..chainConclusionLits: " << chainConclusionLits << "\n";
+    Trace("smt-proof-pp-debug2")
+        << "..chainConclusionLitsSet: " << chainConclusionLitsSet << "\n";
     std::vector<Node> conclusionLits;
-    // whether conclusion is singleton
-    if (chainConclusionLitsSet.count(args[0]))
+    // is args[0] a singleton clause? Yes if it's not an OR node. One might also
+    // think that it is a singleton if args[0] occurs in chainConclusionLitsSet.
+    // However it's not possible to know this only looking at the sets. For
+    // example with
+    //
+    //  args[0]                : (or b c)
+    //  chairConclusionLitsSet : {b, c, (or b c)}
+    //
+    // we have that if args[0] occurs in the set but as a crowding literal, then
+    // args[0] is *not* a singleton clause. But if b and c were crowding
+    // literals, then args[0] would be a singleton clause. Since our intention
+    // is to determine who are the crowding literals exactly based on whether
+    // args[0] is a singleton or not, we must determine in another way whether
+    // args[0] is a singleton.
+    //
+    // Thus we rely on the standard utility to determine if args[0] is singleton
+    // based on the premises and arguments of the resolution
+    if (expr::isSingletonClause(args[0], children, chainResArgs))
     {
       conclusionLits.push_back(args[0]);
     }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2a96818eb..1379c7066 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -861,6 +861,7 @@ set(regress_0_tests
   regress0/proofs/qgu-fuzz-1-bool-sat.smt2
   regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2
   regress0/proofs/qgu-fuzz-3-chainres-checking.smt2
+  regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2
   regress0/proofs/scope.smt2
   regress0/proofs/trust-subs-eq-open.smt2
   regress0/push-pop/boolean/fuzz_12.smt2
diff --git a/test/regress/regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2 b/test/regress/regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2
new file mode 100644
index 000000000..8eef0674b
--- /dev/null
+++ b/test/regress/regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2
@@ -0,0 +1,7 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(assert (and (or d (ite c false true)) (not (= d (or b c))) (= d (ite c d (not d)))))
+(check-sat)