[proof] Fixing CHAIN_RESOLUTION checker (#7465)

Previously the checker was doing things in a smart way that could lead to issues when a clause coincided with a singleton clause as a literal of another clause within the chain.

Fixes cvc5/cvc5-projects#310

2 files changed, 37 insertions, 61 deletions

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 04a36c1c0..a519ca6b5 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -318,8 +318,8 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
     size_t start = lastElim + 1;
     size_t end = nextGuardedElimPos - 1;
     Trace("smt-proof-pp-debug2")
-        << "res with:\n\tlastClause: " << lastClause << "\n\tstart: " << start
-        << "\n\tend: " << end << "\n";
+        << "res with:\n\t\tlastClause: " << lastClause
+        << "\n\t\tstart: " << start << "\n\t\tend: " << end << "\n";
     childrenRes.push_back(lastClause);
     // note that the interval of insert is exclusive in the end, so we add 1
     childrenRes.insert(childrenRes.end(),
@@ -328,8 +328,8 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
     childrenResArgs.insert(childrenResArgs.end(),
                            args.begin() + (2 * start) - 1,
                            args.begin() + (2 * end) + 1);
-    Trace("smt-proof-pp-debug2") << "res children: " << childrenRes << "\n";
-    Trace("smt-proof-pp-debug2") << "res args: " << childrenResArgs << "\n";
+    Trace("smt-proof-pp-debug2") << "\tres children: " << childrenRes << "\n";
+    Trace("smt-proof-pp-debug2") << "\tres args: " << childrenResArgs << "\n";
     resPlaceHolder = d_pnm->getChecker()->checkDebug(PfRule::CHAIN_RESOLUTION,
                                                      childrenRes,
                                                      childrenResArgs,
@@ -337,6 +337,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
                                                      "");
     Trace("smt-proof-pp-debug2")
         << "resPlaceHorder: " << resPlaceHolder << "\n";
+    Trace("smt-proof-pp-debug2") << "-------\n";
     cdp->addStep(
         resPlaceHolder, PfRule::CHAIN_RESOLUTION, childrenRes, childrenResArgs);
     // I need to add factoring if end < children.size(). Otherwise, this is
@@ -348,6 +349,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
       if (!lastClause.isNull())
       {
         cdp->addStep(lastClause, PfRule::FACTORING, {resPlaceHolder}, {});
+        Trace("smt-proof-pp-debug2") << "Apply factoring.\n";
       }
       else
       {
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index d0461248c..eea179ad3 100644
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -197,55 +197,32 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
     Node trueNode = nm->mkConst(true);
     Node falseNode = nm->mkConst(false);
     std::vector<Node> clauseNodes;
-    // literals to be removed from the virtual lhs clause of the resolution
-    std::unordered_map<Node, unsigned> lhsElim;
-    for (std::size_t i = 0, argsSize = args.size(); i < argsSize; i = i + 2)
-    {
-      // whether pivot should occur as is or negated depends on the polarity of
-      // each step in the chain
-      if (args[i] == trueNode)
-      {
-        lhsElim[args[i + 1]]++;
-      }
-      else
-      {
-        Assert(args[i] == falseNode);
-        lhsElim[args[i + 1].notNode()]++;
-      }
-    }
-    if (Trace.isOn("bool-pfcheck"))
-    {
-      Trace("bool-pfcheck")
-          << "Original elimination multiset for lhs clause:\n";
-      for (const auto& pair : lhsElim)
-      {
-        Trace("bool-pfcheck")
-            << "\t- " << pair.first << " {" << pair.second << "}\n";
-      }
-    }
     for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize;
          ++i)
     {
-      // literal to be removed from rhs clause. They will be negated
+      // Literals to be removed from the current clause, according to this
+      // clause being in the lhs or the rhs of a resolution. The first clause
+      // has no rhsElim and the last clause has no lhsElim. The literal to be
+      // eliminated depends ond the pivot and the polarity stored in the
+      // arguments.
+      Node lhsElim = Node::null();
       Node rhsElim = Node::null();
-      if (Trace.isOn("bool-pfcheck"))
+      if (i < childrenSize - 1)
       {
-        Trace("bool-pfcheck") << i << ": current lhsElim:\n";
-        for (const auto& pair : lhsElim)
-        {
-          Trace("bool-pfcheck")
-              << "\t- " << pair.first << " {" << pair.second << "}\n";
-        }
+        std::size_t index = 2 * i;
+        lhsElim = args[index] == trueNode ? args[index + 1]
+                                          : args[index + 1].notNode();
+        Trace("bool-pfcheck") << i << ": lhsElim: " << lhsElim << "\n";
       }
       if (i > 0)
       {
         std::size_t index = 2 * (i - 1);
         rhsElim = args[index] == trueNode ? args[index + 1].notNode()
                                           : args[index + 1];
-        Trace("bool-pfcheck") << i << ": rhs elim: " << rhsElim << "\n";
+        Trace("bool-pfcheck") << i << ": rhsElim: " << rhsElim << "\n";
       }
-      // Only add to conclusion nodes that are not in elimination set. First get
-      // the nodes.
+      // The current set of literals is what we had before plus those in the
+      // current child.
       //
       // Since a Node cannot hold an OR with a single child we need to
       // disambiguate singleton clauses that are OR nodes from non-singleton
@@ -254,10 +231,10 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
       // If the child is not an OR, it is a singleton clause and we take the
       // child itself as the clause. Otherwise the child can only be a singleton
       // clause if the child itself is used as a resolution literal, i.e. if the
-      // child is in lhsElim or is equal to rhsElim (which means that the
+      // child equal to the lhsElim or to the rhsElim (which means that the
       // negation of the child is in lhsElim).
-      std::vector<Node> lits;
-      if (children[i].getKind() == kind::OR && lhsElim.count(children[i]) == 0
+      std::vector<Node> lits{clauseNodes};
+      if (children[i].getKind() == kind::OR && children[i] != lhsElim
           && children[i] != rhsElim)
       {
         lits.insert(lits.end(), children[i].begin(), children[i].end());
@@ -267,31 +244,28 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
         lits.push_back(children[i]);
       }
       Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n";
-      std::vector<Node> added;
+      // We now compute the set of literals minus those to be eliminated in this
+      // step
+      std::vector<Node> curr;
       for (std::size_t j = 0, size = lits.size(); j < size; ++j)
       {
-        if (lits[j] == rhsElim)
+        if (lits[j] == lhsElim)
         {
-          rhsElim = Node::null();
+          lhsElim = Node::null();
+          Trace("bool-pfcheck") << "\t removed lit: " << lits[j] << "\n";
           continue;
         }
-        auto it = lhsElim.find(lits[j]);
-        if (it == lhsElim.end())
-        {
-          clauseNodes.push_back(lits[j]);
-          added.push_back(lits[j]);
-        }
-        else
+        if (lits[j] == rhsElim)
         {
-          // remove occurrence
-          it->second--;
-          if (it->second == 0)
-          {
-            lhsElim.erase(it);
-          }
+          rhsElim = Node::null();
+          Trace("bool-pfcheck") << "\t removed lit: " << lits[j] << "\n";
+          continue;
         }
+        curr.push_back(lits[j]);
       }
-      Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n";
+      Trace("bool-pfcheck") << "\n";
+      clauseNodes.clear();
+      clauseNodes.insert(clauseNodes.end(), curr.begin(), curr.end());
     }
     Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop;
     return nm->mkOr(clauseNodes);