[proof-new] Fixing resolution proof checker (#5262)

Previously the binary resolution checker was:

- Checking applications in which for a pivot (not l) the literal (not l) would be eliminated from the first clause and l from the second because double negation was handled implicitly. Now whether the binary resolution is such that the pivot is removed as is from the first clause and negated from the second, or the other way around, is marked via an argument.
- Not producing false the remaining set of literals after resolution was empty.

This commit also updates the informal description of the rule accordingly, as well as to clarify the behavior when the pivot does not occur properly in the clauses (in which case the rule application corresponds to weakening).

Co-authored-by: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>

1 files changed, 38 insertions, 7 deletions

diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index 2f06995e3..3eb523ab5 100644
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -80,21 +80,52 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
   if (id == PfRule::RESOLUTION)
   {
     Assert(children.size() == 2);
-    Assert(args.size() == 1);
+    Assert(args.size() == 2);
+    NodeManager* nm = NodeManager::currentNM();
     std::vector<Node> disjuncts;
+    Node pivots[2];
+    if (args[0] == nm->mkConst(true))
+    {
+      pivots[0] = args[1];
+      pivots[1] = args[1].notNode();
+    }
+    else
+    {
+      Assert(args[0] == nm->mkConst(false));
+      pivots[0] = args[1].notNode();
+      pivots[1] = args[1];
+    }
     for (unsigned i = 0; i < 2; ++i)
     {
-      // if first clause, eliminate pivot, otherwise its negation
-      Node elim = i == 0 ? args[0] : args[0].notNode();
-      for (unsigned j = 0, size = children[i].getNumChildren(); j < size; ++j)
+      // determine whether the clause is unit for effects of resolution, which
+      // is the case if it's not an OR node or it is an OR node but it is equal
+      // to the pivot
+      std::vector<Node> lits;
+      if (children[i].getKind() == kind::OR && pivots[i] != children[i])
       {
-        if (elim != children[i][j])
+        lits.insert(lits.end(), children[i].begin(), children[i].end());
+      }
+      else
+      {
+        lits.push_back(children[i]);
+      }
+      for (unsigned j = 0, size = lits.size(); j < size; ++j)
+      {
+        if (pivots[i] != lits[j])
         {
-          disjuncts.push_back(children[i][j]);
+          disjuncts.push_back(lits[j]);
+        }
+        else
+        {
+          // just eliminate first occurrence
+          pivots[i] = Node::null();
         }
       }
     }
-    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+    return disjuncts.empty()
+               ? nm->mkConst(false)
+               : disjuncts.size() == 1 ? disjuncts[0]
+                                       : nm->mkNode(kind::OR, disjuncts);
   }
   if (id == PfRule::FACTORING)
   {