1 files changed, 88 insertions, 0 deletions
diff --git a/src/proof/proof_node_algorithm.cpp b/src/proof/proof_node_algorithm.cpp
index 5f56d785e..ce8ca55c3 100644
--- a/src/proof/proof_node_algorithm.cpp
+++ b/src/proof/proof_node_algorithm.cpp
@@ -237,5 +237,93 @@ bool containsSubproof(ProofNode* pn,
   return false;
 }
 
+bool isSingletonClause(TNode res,
+                       const std::vector<Node>& children,
+                       const std::vector<Node>& args)
+{
+  if (res.getKind() != kind::OR)
+  {
+    return true;
+  }
+  size_t i;
+  Node trueNode = NodeManager::currentNM()->mkConst(true);
+  // Find out the last child to introduced res, if any. We only need to
+  // look at the last one because any previous introduction would have
+  // been eliminated.
+  //
+  // After the loop finishes i is the index of the child C_i that
+  // introduced res. If i=0 none of the children introduced res as a
+  // subterm and therefore it cannot be a singleton clause.
+  for (i = children.size(); i > 0; --i)
+  {
+    // only non-singleton clauses may be introducing
+    // res, 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[i - 1].getKind() != kind::OR)
+    {
+      continue;
+    }
+    size_t pivotIndex = (i != 1) ? 2 * (i - 1) - 1 : 1;
+    if (args[pivotIndex] == children[i - 1]
+        || args[pivotIndex].notNode() == children[i - 1])
+    {
+      continue;
+    }
+    // if res occurs as a subterm of a non-singleton premise
+    if (std::find(children[i - 1].begin(), children[i - 1].end(), res)
+        != children[i - 1].end())
+    {
+      break;
+    }
+  }
+
+  // If res is a subterm of one of the children we still need to check if
+  // that subterm is eliminated
+  if (i > 0)
+  {
+    bool posFirst = (i == 1) ? (args[0] == trueNode)
+                             : (args[(2 * (i - 1)) - 2] == trueNode);
+    Node pivot = (i == 1) ? args[1] : args[(2 * (i - 1)) - 1];
+
+    // Check if it is eliminated by the previous resolution step
+    if ((res == pivot && !posFirst) || (res.notNode() == pivot && posFirst)
+        || (pivot.notNode() == res && posFirst))
+    {
+      // We decrease i by one, since it could have been the case that i
+      // was equal to children.size(), so that we return false in the end
+      --i;
+    }
+    else
+    {
+      // Otherwise check if any subsequent premise eliminates it
+      for (; i < children.size(); ++i)
+      {
+        posFirst = args[(2 * i) - 2] == trueNode;
+        pivot = args[(2 * i) - 1];
+        // To eliminate res, the clause must contain it with opposite
+        // polarity. There are three successful cases, according to the
+        // pivot and its sign
+        //
+        // - res is the same as the pivot and posFirst is true, which
+        // means that the clause contains its negation and eliminates it
+        //
+        // - res is the negation of the pivot and posFirst is false, so
+        // the clause contains the node whose negation is res. Note that
+        // this case may either be res.notNode() == pivot or res ==
+        // pivot.notNode().
+        if ((res == pivot && posFirst) || (res.notNode() == pivot && !posFirst)
+            || (pivot.notNode() == res && !posFirst))
+        {
+          break;
+        }
+      }
+    }
+  }
+  // if not eliminated (loop went to the end), then it's a singleton
+  // clause
+  return i == children.size();
+}
+
 }  // namespace expr
 }  // namespace cvc5