(proof-new) Add proof support in TheoryUF (#5002)

This makes TheoryUF use a standard theory inference manager, which thus makes it proof producing when proof-new is enabled.

This additionally cleans HoExtension so that it does not keep a backwards reference to TheoryUF and instead takes its inference manager. This additionally adds two rules for higher-order that are required to make its equality engine proofs correct.


Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

1 files changed, 30 insertions, 0 deletions

diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp
index b010b6d17..ea95c1f24 100644
--- a/src/theory/uf/proof_checker.cpp
+++ b/src/theory/uf/proof_checker.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/uf/proof_checker.h"
 
+#include "theory/uf/theory_uf_rewriter.h"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
@@ -31,6 +33,8 @@ void UfProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::TRUE_ELIM, this);
   pc->registerChecker(PfRule::FALSE_INTRO, this);
   pc->registerChecker(PfRule::FALSE_ELIM, this);
+  pc->registerChecker(PfRule::HO_CONG, this);
+  pc->registerChecker(PfRule::HO_APP_ENCODE, this);
 }
 
 Node UfProofRuleChecker::checkInternal(PfRule id,
@@ -171,6 +175,32 @@ Node UfProofRuleChecker::checkInternal(PfRule id,
     }
     return children[0][0].notNode();
   }
+  if (id == PfRule::HO_CONG)
+  {
+    Assert(children.size() > 0);
+    std::vector<Node> lchildren;
+    std::vector<Node> rchildren;
+    for (size_t i = 0, nchild = children.size(); i < nchild; ++i)
+    {
+      Node eqp = children[i];
+      if (eqp.getKind() != EQUAL)
+      {
+        return Node::null();
+      }
+      lchildren.push_back(eqp[0]);
+      rchildren.push_back(eqp[1]);
+    }
+    NodeManager* nm = NodeManager::currentNM();
+    Node l = nm->mkNode(kind::APPLY_UF, lchildren);
+    Node r = nm->mkNode(kind::APPLY_UF, rchildren);
+    return l.eqNode(r);
+  }
+  else if (id == PfRule::HO_APP_ENCODE)
+  {
+    Assert(args.size() == 1);
+    Node ret = TheoryUfRewriter::getHoApplyForApplyUf(args[0]);
+    return args[0].eqNode(ret);
+  }
   // no rule
   return Node::null();
 }