From 85a8dfddd887a041f397d1ff2c3a6c34900c5775 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 12 Aug 2020 16:34:47 -0500
Subject: [PATCH] (proof-new) Improve robustness of CONG rule (#4882)

This makes it so that the explicit Kind is wrapped in a Node as an argument to the CONG proof rule. This allows us to distinguish applications with the same parameterized operator but different kinds (e.g. APPLY_SELECTOR vs APPLY_SELECTOR_TOTAL).
---
 src/expr/proof_rule.h           |  9 ++++++---
 src/theory/uf/proof_checker.cpp | 22 +++++++++++++++-------
 2 files changed, 21 insertions(+), 10 deletions(-)

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index beff92bd4..364598cf4 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -481,11 +481,14 @@ enum class PfRule : uint32_t
   // -----------------------
   // Conclusion: (= t1 tn)
   TRANS,
-  // ======== Congruence  (subsumed by Substitute?)
+  // ======== Congruence
   // Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
-  // Arguments: (f)
+  // Arguments: (<kind> f?)
   // ---------------------------------------------
-  // Conclusion: (= (f t1 ... tn) (f s1 ... sn))
+  // Conclusion: (= (<kind> f? t1 ... tn) (<kind> f? s1 ... sn))
+  // Notice that f must be provided iff <kind> is a parameterized kind, e.g.
+  // APPLY_UF. The actual node for <kind> is constructible via
+  // ProofRuleChecker::mkKindNode.
   CONG,
   // ======== True intro
   // Children: (P:F)
diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp
index f866e77dd..b010b6d17 100644
--- a/src/theory/uf/proof_checker.cpp
+++ b/src/theory/uf/proof_checker.cpp
@@ -86,15 +86,15 @@ Node UfProofRuleChecker::checkInternal(PfRule id,
   else if (id == PfRule::CONG)
   {
     Assert(children.size() > 0);
-    Assert(args.size() == 1);
+    Assert(args.size() >= 1 && args.size() <= 2);
     // We do congruence over builtin kinds using operatorToKind
     std::vector<Node> lchildren;
     std::vector<Node> rchildren;
-    // get the expected kind for args[0]
-    Kind k = NodeManager::getKindForFunction(args[0]);
-    if (k == kind::UNDEFINED_KIND)
+    // get the kind encoded as args[0]
+    Kind k;
+    if (!getKind(args[0], k))
     {
-      k = NodeManager::operatorToKind(args[0]);
+      return Node::null();
     }
     if (k == kind::UNDEFINED_KIND)
     {
@@ -104,9 +104,17 @@ Node UfProofRuleChecker::checkInternal(PfRule id,
                         << ", metakind=" << kind::metaKindOf(k) << std::endl;
     if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
     {
+      if (args.size() <= 1)
+      {
+        return Node::null();
+      }
       // parameterized kinds require the operator
-      lchildren.push_back(args[0]);
-      rchildren.push_back(args[0]);
+      lchildren.push_back(args[1]);
+      rchildren.push_back(args[1]);
+    }
+    else if (args.size() > 1)
+    {
+      return Node::null();
     }
     for (size_t i = 0, nchild = children.size(); i < nchild; i++)
     {
-- 
2.30.2