Refactor array-proofs and uf-proofs (#1655)

This commit unifies duplicate code blocks from array_proof.cpp and uf_proof.cpp into theory_proof.cpp.

1 files changed, 105 insertions, 259 deletions

diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 746cbbc54..9f7ae7ac1 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -24,48 +24,6 @@
 
 namespace CVC4 {
 
-inline static Node eqNode(TNode n1, TNode n2) {
-  return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2);
-}
-
-// congrence matching term helper
-inline static bool match(TNode n1, TNode n2) {
-  Debug("pf::uf") << "match " << n1 << " " << n2 << std::endl;
-  if(ProofManager::currentPM()->hasOp(n1)) {
-    n1 = ProofManager::currentPM()->lookupOp(n1);
-  }
-  if(ProofManager::currentPM()->hasOp(n2)) {
-    n2 = ProofManager::currentPM()->lookupOp(n2);
-  }
-  Debug("pf::uf") << "+ match " << n1 << " " << n2 << std::endl;
-  if(n1 == n2) {
-    return true;
-  }
-  if(n1.getType().isFunction() && n2.hasOperator()) {
-    if(ProofManager::currentPM()->hasOp(n2.getOperator())) {
-      return n1 == ProofManager::currentPM()->lookupOp(n2.getOperator());
-    } else {
-      return n1 == n2.getOperator();
-    }
-  }
-  if(n2.getType().isFunction() && n1.hasOperator()) {
-    if(ProofManager::currentPM()->hasOp(n1.getOperator())) {
-      return n2 == ProofManager::currentPM()->lookupOp(n1.getOperator());
-    } else {
-      return n2 == n1.getOperator();
-    }
-  }
-  if(n1.hasOperator() && n2.hasOperator() && n1.getOperator() != n2.getOperator()) {
-    return false;
-  }
-  for(size_t i = 0; i < n1.getNumChildren() && i < n2.getNumChildren(); ++i) {
-    if(n1[i] != n2[i]) {
-      return false;
-    }
-  }
-  return true;
-}
-
 void ProofUF::toStream(std::ostream& out) const
 {
   ProofLetMap map;
@@ -101,10 +59,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
                   << std::endl
                   << "toStreamRecLFSC called. tb = " << tb
                   << " . proof:" << std::endl;
-  pf.debug_print("pf::uf");
-  Debug("pf::uf") << std::endl;
-
-  if (tb == 0) {
+  if (tb == 0)
+  {
     // Special case: false was an input, so the proof is just "false".
     if (pf.d_id == theory::eq::MERGED_THROUGH_EQUALITY &&
         pf.d_node == NodeManager::currentNM()->mkConst(false)) {
@@ -114,149 +70,38 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       return Node();
     }
 
-    Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS);
-    Assert(!pf.d_node.isNull());
-    Assert(pf.d_children.size() >= 2);
-
-    int neg = -1;
     std::shared_ptr<theory::eq::EqProof> subTrans =
         std::make_shared<theory::eq::EqProof>();
-    subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS;
-    subTrans->d_node = pf.d_node;
-
-    size_t i = 0;
-
-    while (i < pf.d_children.size()) {
-      pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node);
-
-      // Look for the negative clause, with which we will form a contradiction.
-      if(!pf.d_children[i]->d_node.isNull() && pf.d_children[i]->d_node.getKind() == kind::NOT) {
-        Assert(neg < 0);
-        Node node = pf.d_children[i]->d_node[0];
-        neg = i;
-        ++i;
-      }
-
-      // Handle congruence closures over equalities.
-      else if (pf.d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf.d_children[i]->d_node.isNull()) {
-        Debug("pf::uf") << "Handling congruence over equalities" << std::endl;
-
-        // Gather the sequence of consecutive congruence closures.
-        std::vector<std::shared_ptr<const theory::eq::EqProof>> congruenceClosures;
-        unsigned count;
-        Debug("pf::uf") << "Collecting congruence sequence" << std::endl;
-        for (count = 0;
-             i + count < pf.d_children.size() &&
-               pf.d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
-               pf.d_children[i + count]->d_node.isNull();
-             ++count) {
-          Debug("pf::uf") << "Found a congruence: " << std::endl;
-          pf.d_children[i+count]->debug_print("pf::uf");
-          congruenceClosures.push_back(pf.d_children[i+count]);
-        }
-
-        Debug("pf::uf") << "Total number of congruences found: " << congruenceClosures.size() << std::endl;
 
-        // Determine if the "target" of the congruence sequence appears right before or right after the sequence.
-        bool targetAppearsBefore = true;
-        bool targetAppearsAfter = true;
-
-        if ((i == 0) || (i == 1 && neg == 0)) {
-          Debug("pf::uf") << "Target does not appear before" << std::endl;
-          targetAppearsBefore = false;
-        }
-
-        if ((i + count >= pf.d_children.size()) ||
-            (!pf.d_children[i + count]->d_node.isNull() &&
-             pf.d_children[i + count]->d_node.getKind() == kind::NOT)) {
-          Debug("pf::uf") << "Target does not appear after" << std::endl;
-          targetAppearsAfter = false;
-        }
-
-        // Assert that we have precisely at least one possible clause.
-        Assert(targetAppearsBefore || targetAppearsAfter);
-
-        // If both are valid, assume the one after the sequence is correct
-        if (targetAppearsAfter && targetAppearsBefore)
-          targetAppearsBefore = false;
-
-        // Begin breaking up the congruences and ordering the equalities correctly.
-        std::vector<std::shared_ptr<theory::eq::EqProof>> orderedEqualities;
-
-        // Insert target clause first.
-        if (targetAppearsBefore) {
-          orderedEqualities.push_back(pf.d_children[i - 1]);
-          // The target has already been added to subTrans; remove it.
-          subTrans->d_children.pop_back();
-        } else {
-          orderedEqualities.push_back(pf.d_children[i + count]);
-        }
-
-        // Start with the congruence closure closest to the target clause, and work our way back/forward.
-        if (targetAppearsBefore) {
-          for (unsigned j = 0; j < count; ++j) {
-            if (pf.d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + j]->d_children[0]);
-            if (pf.d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + j]->d_children[1]);
-          }
-        } else {
-          for (unsigned j = 0; j < count; ++j) {
-            if (pf.d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + count - 1 - j]->d_children[0]);
-            if (pf.d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + count - 1 - j]->d_children[1]);
-          }
-        }
-
-        // Copy the result into the main transitivity proof.
-        subTrans->d_children.insert(subTrans->d_children.end(), orderedEqualities.begin(), orderedEqualities.end());
-
-        // Increase i to skip over the children that have been processed.
-        i += count;
-        if (targetAppearsAfter) {
-          ++i;
-        }
-      }
-
-      // Else, just copy the child proof as is
-      else {
-        subTrans->d_children.push_back(pf.d_children[i]);
-        ++i;
-      }
-    }
-
-    bool disequalityFound = (neg >= 0);
-    if (!disequalityFound) {
-      Debug("pf::uf") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl;
-      Debug("pf::uf") << "Proof for: " << pf.d_node << std::endl;
-      Assert(pf.d_node.getKind() == kind::EQUAL);
-      Assert(pf.d_node.getNumChildren() == 2);
-      Assert (pf.d_node[0].isConst() && pf.d_node[1].isConst());
-    }
+    int neg = tp->assertAndPrint(pf, map, subTrans);
 
     Node n1;
-    std::stringstream ss;
+    std::stringstream ss, ss2;
     Debug("pf::uf") << "\nsubtrans has " << subTrans->d_children.size() << " children\n";
+    bool disequalityFound = (neg >= 0);
 
     if(!disequalityFound || subTrans->d_children.size() >= 2) {
       n1 = toStreamRecLFSC(ss, tp, *subTrans, 1, map);
     } else {
       n1 = toStreamRecLFSC(ss, tp, *(subTrans->d_children[0]), 1, map);
-      Debug("pf::uf") << "\nsubTrans unique child " << subTrans->d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
+      Debug("pf::uf") << "\nsubTrans unique child "
+                      << subTrans->d_children[0]->d_id
+                      << " was proven\ngot: " << n1 << std::endl;
     }
 
     Debug("pf::uf") << "\nhave proven: " << n1 << std::endl;
 
     out << "(clausify_false (contra _ ";
-
     if (disequalityFound) {
       Node n2 = pf.d_children[neg]->d_node;
       Assert(n2.getKind() == kind::NOT);
 
       Debug("pf::uf") << "n2 is " << n2[0] << std::endl;
 
-      if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; }
+      if (n2[0].getNumChildren() > 0)
+      {
+        Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl;
+      }
       if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; }
 
       if(n2[0].getKind() == kind::APPLY_UF) {
@@ -289,7 +134,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
 
       out << ss.str();
       out << " ";
-      ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr(), map);
+      ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(
+          out, n1[0].toExpr(), n1[1].toExpr(), map);
       out << "))" << std::endl;
     }
 
@@ -305,7 +151,11 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
          pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE;
          pf2 = pf2->d_children[0].get()) {
       Assert(!pf2->d_node.isNull());
-      Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || pf2->d_node.getKind() == kind::APPLY_UF || pf2->d_node.getKind() == kind::SELECT || pf2->d_node.getKind() == kind::STORE);
+      Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF
+             || pf2->d_node.getKind() == kind::BUILTIN
+             || pf2->d_node.getKind() == kind::APPLY_UF
+             || pf2->d_node.getKind() == kind::SELECT
+             || pf2->d_node.getKind() == kind::STORE);
       Assert(pf2->d_children.size() == 2);
       out << "(cong _ _ _ _ _ _ ";
       stk.push(pf2);
@@ -325,7 +175,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
     Debug("pf::uf") << "           " << n1 << "\n";
     Debug("pf::uf") << "           " << n2 << "\n";
     int side = 0;
-    if(match(pf2->d_node, n1[0])) {
+    if (tp->match(pf2->d_node, n1[0]))
+    {
       //if(tb == 1) {
       Debug("pf::uf") << "SIDE IS 0\n";
       //}
@@ -334,15 +185,22 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       //if(tb == 1) {
       Debug("pf::uf") << "SIDE IS 1\n";
       //}
-      if(!match(pf2->d_node, n1[1])) {
+      if (!tp->match(pf2->d_node, n1[1]))
+      {
         Debug("pf::uf") << "IN BAD CASE, our first subproof is\n";
         pf2->d_children[0]->debug_print("pf::uf");
       }
-      Assert(match(pf2->d_node, n1[1]));
+      Assert(tp->match(pf2->d_node, n1[1]));
       side = 1;
     }
-    if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF || n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::STORE) {
-      if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF) {
+    if (n1[side].getKind() == kind::APPLY_UF
+        || n1[side].getKind() == kind::PARTIAL_APPLY_UF
+        || n1[side].getKind() == kind::SELECT
+        || n1[side].getKind() == kind::STORE)
+    {
+      if (n1[side].getKind() == kind::APPLY_UF
+          || n1[side].getKind() == kind::PARTIAL_APPLY_UF)
+      {
         b1 << n1[side].getOperator();
       } else {
         b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator());
@@ -352,7 +210,9 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       b1 << n1[side];
     }
     if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || n1[1-side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::STORE) {
-      if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || n1[1-side].getKind() == kind::APPLY_UF) {
+      if (n1[1 - side].getKind() == kind::PARTIAL_APPLY_UF
+          || n1[1 - side].getKind() == kind::APPLY_UF)
+      {
         b2 << n1[1-side].getOperator();
       } else {
         b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator());
@@ -435,7 +295,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       b2.append(n2.begin(), n2.end());
       n2 = b2;
     }
-    Node n = (side == 0 ? eqNode(n1, n2) : eqNode(n2, n1));
+    Node n = (side == 0 ? n1.eqNode(n2) : n2.eqNode(n1));
     if(tb == 1) {
       Debug("pf::uf") << "\ncong proved: " << n << "\n";
     }
@@ -443,13 +303,14 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
   }
 
   case theory::eq::MERGED_THROUGH_REFLEXIVITY:
+  {
     Assert(!pf.d_node.isNull());
     Assert(pf.d_children.empty());
     out << "(refl _ ";
     tp->printTerm(NodeManager::currentNM()->toExpr(pf.d_node), out, map);
     out << ")";
-    return eqNode(pf.d_node, pf.d_node);
-
+    return pf.d_node.eqNode(pf.d_node);
+  }
   case theory::eq::MERGED_THROUGH_EQUALITY:
     Assert(!pf.d_node.isNull());
     Assert(pf.d_children.empty());
@@ -468,128 +329,109 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
 
     Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
     Debug("pf::uf") << "\ndoing trans proof, got n1 " << n1 << "\n";
+    Node n2;
     if(tb == 1) {
       Debug("pf::uf") << "\ntrans proof[0], got n1 " << n1 << "\n";
     }
 
     bool identicalEqualities = false;
     bool evenLengthSequence;
-    Node nodeAfterEqualitySequence;
+    std::stringstream dontCare;
+    Node nodeAfterEqualitySequence =
+        toStreamRecLFSC(dontCare, tp, *(pf.d_children[0]), tb + 1, map);
 
     std::map<size_t, Node> childToStream;
-
+    std::stringstream ss1(ss.str()), ss2;
+    std::pair<Node, Node> nodePair;
     for(size_t i = 1; i < pf.d_children.size(); ++i) {
       std::stringstream ss1(ss.str()), ss2;
       ss.str("");
 
       pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node);
 
-      // It is possible that we've already converted the i'th child to stream. If so,
+      // It is possible that we've already converted the i'th child to stream.
+      // If so,
       // use previously stored result. Otherwise, convert and store.
       Node n2;
       if (childToStream.find(i) != childToStream.end())
         n2 = childToStream[i];
-      else {
+      else
+      {
         n2 = toStreamRecLFSC(ss2, tp, *(pf.d_children[i]), tb + 1, map);
         childToStream[i] = n2;
       }
 
-      // The following branch is dedicated to handling sequences of identical equalities,
+      // The following branch is dedicated to handling sequences of identical
+      // equalities,
       // i.e. trans[ a=b, a=b, a=b ].
       //
       // There are two cases:
-      //    1. The number of equalities is odd. Then, the sequence can be collapsed to just one equality,
+      //    1. The number of equalities is odd. Then, the sequence can be
+      //    collapsed to just one equality,
       //       i.e. a=b.
-      //    2. The number of equalities is even. Now, we have two options: a=a or b=b. To determine this,
-      //       we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs
-      //       b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof,
+      //    2. The number of equalities is even. Now, we have two options: a=a
+      //    or b=b. To determine this,
+      //       we look at the node after the equality sequence. If it needs a,
+      //       we go for a=a; and if it needs
+      //       b, we go for b=b. If there is no following node, we look at the
+      //       goal of the transitivity proof,
       //       and use it to determine which option we need.
-      if(n2.getKind() == kind::EQUAL) {
-        if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) {
+      if (n2.getKind() == kind::EQUAL)
+      {
+        if (((n1[0] == n2[0]) && (n1[1] == n2[1]))
+            || ((n1[0] == n2[1]) && (n1[1] == n2[0])))
+        {
           // We are in a sequence of identical equalities
 
-          Debug("pf::uf") << "Detected identical equalities: " << std::endl << "\t" << n1 << std::endl;
+          Debug("pf::uf") << "Detected identical equalities: " << std::endl
+                          << "\t" << n1 << std::endl;
 
-          if (!identicalEqualities) {
+          if (!identicalEqualities)
+          {
             // The sequence of identical equalities has started just now
             identicalEqualities = true;
 
-            Debug("pf::uf") << "The sequence is just beginning. Determining length..." << std::endl;
+            Debug("pf::uf")
+                << "The sequence is just beginning. Determining length..."
+                << std::endl;
 
             // Determine whether the length of this sequence is odd or even.
             evenLengthSequence = true;
             bool sequenceOver = false;
             size_t j = i + 1;
 
-            while (j < pf.d_children.size() && !sequenceOver) {
+            while (j < pf.d_children.size() && !sequenceOver)
+            {
               std::stringstream dontCare;
-              nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, *(pf.d_children[j]), tb + 1, map );
-
-              if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) ||
-                  ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) {
+              nodeAfterEqualitySequence = toStreamRecLFSC(
+                  dontCare, tp, *(pf.d_children[j]), tb + 1, map);
+
+              if (((nodeAfterEqualitySequence[0] == n1[0])
+                   && (nodeAfterEqualitySequence[1] == n1[1]))
+                  || ((nodeAfterEqualitySequence[0] == n1[1])
+                      && (nodeAfterEqualitySequence[1] == n1[0])))
+              {
                 evenLengthSequence = !evenLengthSequence;
-              } else {
+              }
+              else
+              {
                 sequenceOver = true;
               }
 
               ++j;
             }
 
-            if (evenLengthSequence) {
-              // If the length is even, we need to apply transitivity for the "correct" hand of the equality.
-
-              Debug("pf::uf") << "Equality sequence of even length" << std::endl;
-              Debug("pf::uf") << "n1 is: " << n1 << std::endl;
-              Debug("pf::uf") << "n2 is: " << n2 << std::endl;
-              Debug("pf::uf") << "pf-d_node is: " << pf.d_node << std::endl;
-              Debug("pf::uf") << "Next node is: " << nodeAfterEqualitySequence << std::endl;
-
-              ss << "(trans _ _ _ _ ";
-
-              // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us.
-              if (!sequenceOver) {
-                if (match(n1[0], pf.d_node[0])) {
-                  n1 = eqNode(n1[0], n1[0]);
-                  ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")";
-                } else if (match(n1[1], pf.d_node[1])) {
-                  n1 = eqNode(n1[1], n1[1]);
-                  ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str();
-                } else {
-                  Debug("pf::uf") << "Error: identical equalities over, but hands don't match what we're proving."
-                                  << std::endl;
-                  Assert(false);
-                }
-              } else {
-                // We have a "next node". Use it to guide us.
-
-                Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL);
-
-                if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) {
-
-                  // Eliminate n1[1]
-                  ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")";
-                  n1 = eqNode(n1[0], n1[0]);
-
-                } else if ((n1[1] == nodeAfterEqualitySequence[0]) || (n1[1] == nodeAfterEqualitySequence[1])) {
-
-                  // Eliminate n1[0]
-                  ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str();
-                  n1 = eqNode(n1[1], n1[1]);
-
-                } else {
-                  Debug("pf::uf") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl;
-                  Assert(false);
-                }
-              }
-
-              ss << ")";
-
-            } else {
-              Debug("pf::uf") << "Equality sequence length is odd!" << std::endl;
-              ss.str(ss1.str());
-            }
-
-            Debug("pf::uf") << "Have proven: " << n1 << std::endl;
+            nodePair =
+                tp->identicalEqualitiesPrinterHelper(evenLengthSequence,
+                                                     sequenceOver,
+                                                     pf,
+                                                     map,
+                                                     ss1.str(),
+                                                     &ss,
+                                                     n1,
+                                                     nodeAfterEqualitySequence);
+            n1 = nodePair.first;
+            nodeAfterEqualitySequence = nodePair.second;
           } else {
             ss.str(ss1.str());
           }
@@ -621,6 +463,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
           Debug("pf::uf") << (n1[1] == n2[0]) << "\n";
         }
       }
+
       ss << "(trans _ _ _ _ ";
 
       if(n2.getKind() == kind::EQUAL && n1.getKind() == kind::EQUAL)
@@ -628,20 +471,20 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       {
         if(n1[0] == n2[0]) {
           if(tb == 1) { Debug("pf::uf") << "case 1\n"; }
-          n1 = eqNode(n1[1], n2[1]);
+          n1 = n1[1].eqNode(n2[1]);
           ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str();
         } else if(n1[1] == n2[1]) {
           if(tb == 1) { Debug("pf::uf") << "case 2\n"; }
-          n1 = eqNode(n1[0], n2[0]);
+          n1 = n1[0].eqNode(n2[0]);
           ss << ss1.str() << " (symm _ _ _ " << ss2.str() << ")";
         } else if(n1[0] == n2[1]) {
           if(tb == 1) { Debug("pf::uf") << "case 3\n"; }
-          n1 = eqNode(n2[0], n1[1]);
+          n1 = n2[0].eqNode(n1[1]);
           ss << ss2.str() << " " << ss1.str();
           if(tb == 1) { Debug("pf::uf") << "++ proved " << n1 << "\n"; }
         } else if(n1[1] == n2[0]) {
           if(tb == 1) { Debug("pf::uf") << "case 4\n"; }
-          n1 = eqNode(n1[0], n2[1]);
+          n1 = n1[0].eqNode(n2[1]);
           ss << ss1.str() << " " << ss2.str();
         } else {
           Warning() << "\n\ntrans proof failure at step " << i << "\n\n";
@@ -734,6 +577,7 @@ UFProof::UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* pe)
   : TheoryProof(uf, pe)
 {}
 
+theory::TheoryId UFProof::getTheoryId() { return theory::THEORY_UF; }
 void UFProof::registerTerm(Expr term) {
   // already registered
   if (d_declarations.find(term) != d_declarations.end())
@@ -757,8 +601,10 @@ void UFProof::registerTerm(Expr term) {
     if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
       // Ensure cnf literals
       Node asNode(term);
-      ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(true)));
-      ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(false)));
+      ProofManager::currentPM()->ensureLiteral(
+          asNode.eqNode(NodeManager::currentNM()->mkConst(true)));
+      ProofManager::currentPM()->ensureLiteral(
+          asNode.eqNode(NodeManager::currentNM()->mkConst(false)));
     }
   }