[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>

3 files changed, 59 insertions, 14 deletions

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 9c955d067..e24d5c522 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -246,14 +246,28 @@ enum class PfRule : uint32_t
   //================================================= Boolean rules
   // ======== Resolution
   // Children:
-  //  (P1:(or F_1 ... F_i-1 F_i F_i+1 ... F_n),
-  //   P2:(or G_1 ... G_j-1 G_j G_j+1 ... G_m))
-  //
-  // Arguments: (F_i)
+  //  (P1:C1, P2:C2)
+  // Arguments: (id, L)
   // ---------------------
-  // Conclusion: (or F_1 ... F_i-1 F_i+1 ... F_n G_1 ... G_j-1 G_j+1 ... G_m)
+  // Conclusion: C
   // where
-  //   G_j = (not F_i)
+  //   - C1 and C2 are nodes viewed as clauses, i.e., either an OR node with
+  //     each children viewed as a literal or a node viewed as a literal. Note
+  //     that an OR node could also be a literal.
+  //   - id is either true or false
+  //   - L is the pivot of the resolution, which occurs as is (resp. under a
+  //     NOT) in C1 and negatively (as is) in C2 if id = true (id = false).
+  //   C is a clause resulting from collecting all the literals in C1, minus the
+  //   first occurrence of the pivot or its negation, and C2, minus the first
+  //   occurrence of the pivot or its negation, according to the policy above.
+  //   If the resulting clause has a single literal, that literal itself is the
+  //   result; if it has no literals, then the result is false; otherwise it's
+  //   an OR node of the resulting literals.
+  //
+  //   Note that it may be the case that the pivot does not occur in the
+  //   clauses. In this case the rule is not unsound, but it does not correspond
+  //   to resolution but rather to a weakening of the clause that did not have a
+  //   literal eliminated.
   RESOLUTION,
   // ======== Chain Resolution
   // Children: (P1:(or F_{1,1} ... F_{1,n1}), ..., Pm:(or F_{m,1} ... F_{m,nm}))
diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index c7dd288af..b2d33a61d 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -548,7 +548,7 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn)
     d_proof.addStep(clauseExp,
                     PfRule::RESOLUTION,
                     {clauseAndNeg, clauseImpliesElim},
-                    {proven[0]});
+                    {nm->mkConst(true), proven[0]});
   }
   else
   {
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)
   {