Removes old proof code (#4964)

This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.

It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).

1 files changed, 0 insertions, 1207 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
deleted file mode 100644
index 635767b97..000000000
--- a/src/proof/arith_proof.cpp
+++ /dev/null
@@ -1,1207 +0,0 @@
-/*********************                                                        */
-/*! \file arith_proof.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Alex Ozdemir, Liana Hadarean, Guy Katz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** [[ Add lengthier description here ]]
-
- ** \todo document this file
-
-**/
-#include "proof/arith_proof.h"
-
-#include <memory>
-#include <stack>
-
-#include "base/check.h"
-#include "expr/node.h"
-#include "expr/type_checker_util.h"
-#include "proof/proof_manager.h"
-#include "proof/theory_proof.h"
-#include "theory/arith/constraint_forward.h"
-#include "theory/arith/normal_form.h"
-#include "theory/arith/theory_arith.h"
-
-#define CVC4_ARITH_VAR_TERM_PREFIX "term."
-
-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::arith") << "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::arith") << "+ 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 ProofArith::toStream(std::ostream& out) const
-{
-  Trace("theory-proof-debug") << "; Print Arith proof..." << std::endl;
-  //AJR : carry this further?
-  ProofLetMap map;
-  toStreamLFSC(out, ProofManager::getArithProof(), *d_proof, map);
-}
-
-void ProofArith::toStreamLFSC(std::ostream& out,
-                              TheoryProof* tp,
-                              const theory::eq::EqProof& pf,
-                              const ProofLetMap& map)
-{
-  Debug("lfsc-arith") << "Printing arith proof in LFSC : " << std::endl;
-  pf.debug_print("lfsc-arith");
-  Debug("lfsc-arith") << std::endl;
-  toStreamRecLFSC(out, tp, pf, 0, map);
-}
-
-Node ProofArith::toStreamRecLFSC(std::ostream& out,
-                                 TheoryProof* tp,
-                                 const theory::eq::EqProof& pf,
-                                 unsigned tb,
-                                 const ProofLetMap& map)
-{
-  Debug("pf::arith") << std::endl
-                     << std::endl
-                     << "toStreamRecLFSC called. tb = " << tb
-                     << " . proof:" << std::endl;
-  pf.debug_print("pf::arith");
-  Debug("pf::arith") << std::endl;
-
-  if(tb == 0) {
-    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()) {
-      // 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);
-        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::arith") << "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::arith") << "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::arith") << "Found a congruence: " << std::endl;
-          pf.d_children[i+count]->debug_print("pf::arith");
-          congruenceClosures.push_back(pf.d_children[i+count]);
-        }
-
-        Debug("pf::arith") << "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::arith") << "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::arith") << "Target does not appear after" << std::endl;
-          targetAppearsAfter = false;
-        }
-
-        // Assert that we have precisely one target clause.
-        Assert(targetAppearsBefore != targetAppearsAfter);
-
-        // 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;
-      }
-    }
-    Assert(neg >= 0);
-
-    Node n1;
-    std::stringstream ss;
-    //Assert(subTrans->d_children.size() == pf.d_children.size() - 1);
-    Debug("pf::arith") << "\nsubtrans has " << subTrans->d_children.size() << " children\n";
-    if(pf.d_children.size() > 2) {
-      n1 = toStreamRecLFSC(ss, tp, *subTrans, 1, map);
-    } else {
-      n1 = toStreamRecLFSC(ss, tp, *(subTrans->d_children[0]), 1, map);
-      Debug("pf::arith") << "\nsubTrans unique child " << subTrans->d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
-    }
-
-    Node n2 = pf.d_children[neg]->d_node;
-    Assert(n2.getKind() == kind::NOT);
-    out << "(clausify_false (contra _ ";
-    Debug("pf::arith") << "\nhave proven: " << n1 << std::endl;
-    Debug("pf::arith") << "n2 is " << n2[0] << std::endl;
-
-    if (n2[0].getNumChildren() > 0) { Debug("pf::arith") << "\nn2[0]: " << n2[0][0] << std::endl; }
-    if (n1.getNumChildren() > 1) { Debug("pf::arith") << "n1[1]: " << n1[1] << std::endl; }
-
-    if(n2[0].getKind() == kind::APPLY_UF) {
-      out << "(trans _ _ _ _ ";
-      out << "(symm _ _ _ ";
-      out << ss.str();
-      out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
-    } else {
-      Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1])
-             || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
-      if(n1[1] == n2[0][0]) {
-        out << "(symm _ _ _ " << ss.str() << ")";
-      } else {
-        out << ss.str();
-      }
-      out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
-    }
-    return Node();
-  }
-
-  switch(pf.d_id) {
-  case theory::eq::MERGED_THROUGH_CONGRUENCE: {
-    Debug("pf::arith") << "\nok, looking at congruence:\n";
-    pf.debug_print("pf::arith");
-    std::stack<const theory::eq::EqProof*> stk;
-    for (const theory::eq::EqProof* pf2 = &pf;
-         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_children.size() == 2);
-      out << "(cong _ _ _ _ _ _ ";
-      stk.push(pf2);
-    }
-    Assert(stk.top()->d_children[0]->d_id
-           != theory::eq::MERGED_THROUGH_CONGRUENCE);
-    NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF);
-    const theory::eq::EqProof* pf2 = stk.top();
-    stk.pop();
-    Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
-    Node n1 = toStreamRecLFSC(out, tp, *(pf2->d_children[0]), tb + 1, map);
-    out << " ";
-    std::stringstream ss;
-    Node n2 = toStreamRecLFSC(ss, tp, *(pf2->d_children[1]), tb + 1, map);
-    Debug("pf::arith") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
-    pf2->debug_print("pf::arith");
-    Debug("pf::arith") << "looking at " << pf2->d_node << "\n";
-    Debug("pf::arith") << "           " << n1 << "\n";
-    Debug("pf::arith") << "           " << n2 << "\n";
-    int side = 0;
-    if(match(pf2->d_node, n1[0])) {
-      //if(tb == 1) {
-      Debug("pf::arith") << "SIDE IS 0\n";
-      //}
-      side = 0;
-    } else {
-      //if(tb == 1) {
-      Debug("pf::arith") << "SIDE IS 1\n";
-      //}
-      if(!match(pf2->d_node, n1[1])) {
-      Debug("pf::arith") << "IN BAD CASE, our first subproof is\n";
-      pf2->d_children[0]->debug_print("pf::arith");
-      }
-      Assert(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) {
-        b1 << n1[side].getOperator();
-      } else {
-        b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator());
-      }
-      b1.append(n1[side].begin(), n1[side].end());
-    } else {
-      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) {
-        b2 << n1[1-side].getOperator();
-      } else {
-        b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator());
-      }
-      b2.append(n1[1-side].begin(), n1[1-side].end());
-    } else {
-      b2 << n1[1-side];
-    }
-    Debug("pf::arith") << "pf2->d_node " << pf2->d_node << std::endl;
-    Debug("pf::arith") << "b1.getNumChildren() " << b1.getNumChildren() << std::endl;
-    Debug("pf::arith") << "n1 " << n1 << std::endl;
-    Debug("pf::arith") << "n2 " << n2 << std::endl;
-    Debug("pf::arith") << "side " << side << std::endl;
-    if(pf2->d_node[b1.getNumChildren() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[side]) {
-      b1 << n2[side];
-      b2 << n2[1-side];
-      out << ss.str();
-    } else {
-      Assert(pf2->d_node[b1.getNumChildren()
-                         - (pf2->d_node.getMetaKind()
-                                    == kind::metakind::PARAMETERIZED
-                                ? 0
-                                : 1)]
-             == n2[1 - side]);
-      b1 << n2[1-side];
-      b2 << n2[side];
-      out << "(symm _ _ _ " << ss.str() << ")";
-    }
-    out << ")";
-    while(!stk.empty()) {
-      if(tb == 1) {
-      Debug("pf::arith") << "\nMORE TO DO\n";
-      }
-      pf2 = stk.top();
-      stk.pop();
-      Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
-      out << " ";
-      ss.str("");
-      n2 = toStreamRecLFSC(ss, tp, *(pf2->d_children[1]), tb + 1, map);
-      Debug("pf::arith") << "\nok, in cong[" << stk.size() << "]" << "\n";
-      Debug("pf::arith") << "looking at " << pf2->d_node << "\n";
-      Debug("pf::arith") << "           " << n1 << "\n";
-      Debug("pf::arith") << "           " << n2 << "\n";
-      Debug("pf::arith") << "           " << b1 << "\n";
-      Debug("pf::arith") << "           " << b2 << "\n";
-      if(pf2->d_node[b1.getNumChildren()] == n2[side]) {
-        b1 << n2[side];
-        b2 << n2[1-side];
-        out << ss.str();
-      } else {
-        Assert(pf2->d_node[b1.getNumChildren()] == n2[1 - side]);
-        b1 << n2[1-side];
-        b2 << n2[side];
-        out << "(symm _ _ _ " << ss.str() << ")";
-      }
-      out << ")";
-    }
-    n1 = b1;
-    n2 = b2;
-    Debug("pf::arith") << "at end assert, got " << pf2->d_node << "  and  " << n1 << std::endl;
-    if(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF) {
-      Assert(n1 == pf2->d_node);
-    }
-    if(n1.getOperator().getType().getNumChildren() == n1.getNumChildren() + 1) {
-      if(ProofManager::currentPM()->hasOp(n1.getOperator())) {
-        b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>());
-      } else {
-        b1.clear(kind::APPLY_UF);
-        b1 << n1.getOperator();
-      }
-      b1.append(n1.begin(), n1.end());
-      n1 = b1;
-      Debug("pf::arith") << "at[2] end assert, got " << pf2->d_node << "  and  " << n1 << std::endl;
-      if(pf2->d_node.getKind() == kind::APPLY_UF) {
-        Assert(n1 == pf2->d_node);
-      }
-    }
-    if(n2.getOperator().getType().getNumChildren() == n2.getNumChildren() + 1) {
-      if(ProofManager::currentPM()->hasOp(n2.getOperator())) {
-        b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>());
-      } else {
-        b2.clear(kind::APPLY_UF);
-        b2 << n2.getOperator();
-      }
-      b2.append(n2.begin(), n2.end());
-      n2 = b2;
-    }
-    Node n = (side == 0 ? eqNode(n1, n2) : eqNode(n2, n1));
-    if(tb == 1) {
-    Debug("pf::arith") << "\ncong proved: " << n << "\n";
-    }
-    return n;
-  }
-
-  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);
-
-  case theory::eq::MERGED_THROUGH_EQUALITY:
-    Assert(!pf.d_node.isNull());
-    Assert(pf.d_children.empty());
-    out << ProofManager::getLitName(pf.d_node.negate());
-    return pf.d_node;
-
-  case theory::eq::MERGED_THROUGH_TRANS: {
-    Assert(!pf.d_node.isNull());
-    Assert(pf.d_children.size() >= 2);
-    std::stringstream ss;
-    Debug("pf::arith") << "\ndoing trans proof[[\n";
-    pf.debug_print("pf::arith");
-    Debug("pf::arith") << "\n";
-    Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
-    Debug("pf::arith") << "\ndoing trans proof, got n1 " << n1 << "\n";
-    if(tb == 1) {
-      Debug("pf::arith") << "\ntrans proof[0], got n1 " << n1 << "\n";
-    }
-
-    bool identicalEqualities = false;
-    bool evenLengthSequence;
-    Node nodeAfterEqualitySequence;
-
-    std::map<size_t, Node> childToStream;
-
-    for(size_t i = 1; i < pf.d_children.size(); ++i) {
-      std::stringstream ss1(ss.str()), ss2;
-      ss.str("");
-
-      // 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 {
-        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,
-      // 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,
-      //       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,
-      //       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]))) {
-          // We are in a sequence of identical equalities
-
-          Debug("pf::arith") << "Detected identical equalities: " << std::endl << "\t" << n1 << std::endl;
-
-          if (!identicalEqualities) {
-            // The sequence of identical equalities has started just now
-            identicalEqualities = true;
-
-            Debug("pf::arith") << "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) {
-              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]))) {
-                evenLengthSequence = !evenLengthSequence;
-              } 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::arith") << "Equality sequence of even length" << std::endl;
-              Debug("pf::arith") << "n1 is: " << n1 << std::endl;
-              Debug("pf::arith") << "n2 is: " << n2 << std::endl;
-              Debug("pf::arith") << "pf-d_node is: " << pf.d_node << std::endl;
-              Debug("pf::arith") << "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::arith") << "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::arith") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl;
-                  Assert(false);
-                }
-              }
-
-              ss << ")";
-
-            } else {
-              Debug("pf::arith") << "Equality sequence length is odd!" << std::endl;
-              ss.str(ss1.str());
-            }
-
-            Debug("pf::arith") << "Have proven: " << n1 << std::endl;
-          } else {
-            ss.str(ss1.str());
-          }
-
-          // Ignore the redundancy.
-          continue;
-        }
-      }
-
-      if (identicalEqualities) {
-        // We were in a sequence of identical equalities, but it has now ended. Resume normal operation.
-        identicalEqualities = false;
-      }
-
-      Debug("pf::arith") << "\ndoing trans proof, got n2 " << n2 << "\n";
-      if(tb == 1) {
-        Debug("pf::arith") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n";
-        Debug("pf::arith") << (n2.getKind() == kind::EQUAL) << "\n";
-
-        if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) {
-          Debug("pf::arith") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n";
-          Debug("pf::arith") << n1[0].getId() << " " << n1[0] << "\n";
-          Debug("pf::arith") << n1[1].getId() << " " << n1[1] << "\n";
-          Debug("pf::arith") << n2[0].getId() << " " << n2[0] << "\n";
-          Debug("pf::arith") << n2[1].getId() << " " << n2[1] << "\n";
-          Debug("pf::arith") << (n1[0] == n2[0]) << "\n";
-          Debug("pf::arith") << (n1[1] == n2[1]) << "\n";
-          Debug("pf::arith") << (n1[0] == n2[1]) << "\n";
-          Debug("pf::arith") << (n1[1] == n2[0]) << "\n";
-        }
-      }
-      ss << "(trans _ _ _ _ ";
-
-      if((n2.getKind() == kind::EQUAL) && (n1.getKind() == kind::EQUAL))
-        // Both elements of the transitivity rule are equalities/iffs
-      {
-        if(n1[0] == n2[0]) {
-            if(tb == 1) { Debug("pf::arith") << "case 1\n"; }
-            n1 = eqNode(n1[1], n2[1]);
-            ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str();
-        } else if(n1[1] == n2[1]) {
-          if(tb == 1) { Debug("pf::arith") << "case 2\n"; }
-          n1 = eqNode(n1[0], n2[0]);
-          ss << ss1.str() << " (symm _ _ _ " << ss2.str() << ")";
-        } else if(n1[0] == n2[1]) {
-            if(tb == 1) { Debug("pf::arith") << "case 3\n"; }
-            n1 = eqNode(n2[0], n1[1]);
-            ss << ss2.str() << " " << ss1.str();
-            if(tb == 1) { Debug("pf::arith") << "++ proved " << n1 << "\n"; }
-        } else if(n1[1] == n2[0]) {
-          if(tb == 1) { Debug("pf::arith") << "case 4\n"; }
-          n1 = eqNode(n1[0], n2[1]);
-          ss << ss1.str() << " " << ss2.str();
-        } else {
-          Warning() << "\n\ntrans proof failure at step " << i << "\n\n";
-          Warning() << "0 proves " << n1 << "\n";
-          Warning() << "1 proves " << n2 << "\n\n";
-          pf.debug_print("pf::arith",0);
-          //toStreamRec(Warning.getStream(), pf, 0);
-          Warning() << "\n\n";
-          Unreachable();
-        }
-        Debug("pf::arith") << "++ trans proof[" << i << "], now have " << n1 << std::endl;
-      } else if(n1.getKind() == kind::EQUAL) {
-        // n1 is an equality/iff, but n2 is a predicate
-        if(n1[0] == n2) {
-          n1 = n1[1];
-          ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")";
-        } else if(n1[1] == n2) {
-          n1 = n1[0];
-          ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")";
-        } else {
-          Unreachable();
-        }
-      } else if(n2.getKind() == kind::EQUAL) {
-        // n2 is an equality/iff, but n1 is a predicate
-        if(n2[0] == n1) {
-          n1 = n2[1];
-          ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")";
-        } else if(n2[1] == n1) {
-          n1 = n2[0];
-          ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")";
-        } else {
-          Unreachable();
-        }
-      } else {
-        // Both n1 and n2 are prediacates. Don't know what to do...
-        Unreachable();
-      }
-
-      ss << ")";
-    }
-    out << ss.str();
-    Debug("pf::arith") << "\n++ trans proof done, have proven " << n1 << std::endl;
-    return n1;
-  }
-
-  default:
-    Assert(!pf.d_node.isNull());
-    Assert(pf.d_children.empty());
-    Debug("pf::arith") << "theory proof: " << pf.d_node << " by rule " << int(pf.d_id) << std::endl;
-    AlwaysAssert(false);
-    return pf.d_node;
-  }
-}
-
-ArithProof::ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* pe)
-  : TheoryProof(arith, pe), d_recorder()
-{
-  arith->setProofRecorder(&d_recorder);
-}
-
-theory::TheoryId ArithProof::getTheoryId() { return theory::THEORY_ARITH; }
-void ArithProof::registerTerm(Expr term) {
-  Debug("pf::arith") << "Arith register term: " << term << ". Kind: " << term.getKind()
-                            << ". Type: " << term.getType() << std::endl;
-
-  if (term.getType().isReal() && !term.getType().isInteger()) {
-    Debug("pf::arith") << "Entering real mode" << std::endl;
-  }
-
-  if (term.isVariable() && !ProofManager::getSkolemizationManager()->isSkolem(term)) {
-    d_declarations.insert(term);
-  }
-
-  // recursively declare all other terms
-  for (unsigned i = 0; i < term.getNumChildren(); ++i) {
-    // could belong to other theories
-    d_proofEngine->registerTerm(term[i]);
-  }
-}
-
-void LFSCArithProof::printOwnedTermAsType(Expr term,
-                                          std::ostream& os,
-                                          const ProofLetMap& map,
-                                          TypeNode expectedType)
-{
-  Debug("pf::arith") << "Arith print term: " << term << ". Kind: " << term.getKind()
-                     << ". Type: " << term.getType()
-                     << ". Number of children: " << term.getNumChildren() << std::endl;
-
-  // !d_realMode <--> term.getType().isInteger()
-
-  Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARITH);
-  std::ostringstream closing;
-  if (!expectedType.isNull() && !expectedType.isInteger() && term.getType().isInteger()) {
-    os << "(term_int_to_real ";
-    closing << ")";
-  }
-  switch (term.getKind())
-  {
-    case kind::CONST_RATIONAL:
-    {
-      Assert(term.getNumChildren() == 0);
-      Assert(term.getType().isInteger() || term.getType().isReal());
-
-      const Rational& r = term.getConst<Rational>();
-      bool neg = (r < 0);
-
-      os << (term.getType().isInteger() ? "(a_int " : "(a_real ");
-      closing << ") ";
-
-      if (neg)
-      {
-        os << "(~ ";
-        closing << ")";
-      }
-
-      if (term.getType().isInteger())
-      {
-        os << r.abs();
-      }
-      else
-      {
-        printRational(os, r.abs());
-      }
-
-      break;
-    }
-
-    case kind::PLUS:
-    case kind::MINUS:
-    case kind::MULT:
-    case kind::DIVISION:
-    case kind::DIVISION_TOTAL:
-    {
-      Assert(term.getNumChildren() >= 1);
-      TypeNode ty = Node::fromExpr(term).getType();
-
-      std::string lfscFunction = getLfscFunction(term);
-      for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
-      {
-        os << "(" << lfscFunction << " ";
-        closing << ")";
-        d_proofEngine->printBoundTerm(term[i], os, map, ty);
-        os << " ";
-      }
-
-      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map, ty);
-      break;
-    }
-
-    case kind::UMINUS:
-    {
-      Assert(term.getNumChildren() == 1);
-      os << "(" << getLfscFunction(term) << " ";
-      closing << ")";
-      d_proofEngine->printBoundTerm(term[0], os, map, Node::fromExpr(term).getType());
-      break;
-    }
-
-    case kind::GT:
-    case kind::GEQ:
-    case kind::LT:
-    case kind::LEQ:
-    {
-      Assert(term.getNumChildren() == 2);
-      Assert(term.getType().isBoolean());
-
-      std::string lfscFunction = getLfscFunction(term);
-      TypeNode realType = NodeManager::currentNM()->realType();
-
-      os << "(" << lfscFunction << " ";
-      closing << ")";
-
-      d_proofEngine->printBoundTerm(term[0], os, map);
-      os << " ";
-      d_proofEngine->printBoundTerm(term[1], os, map, realType);
-      break;
-    }
-    case kind::EQUAL:
-    {
-      Assert(term.getType().isBoolean());
-      Assert(term.getNumChildren() == 2);
-
-      TypeNode eqType = equalityType(term[0], term[1]);
-
-      os << "(= " << eqType << " ";
-      closing << ")";
-
-      d_proofEngine->printBoundTerm(term[0], os, map, eqType);
-      d_proofEngine->printBoundTerm(term[1], os, map, eqType);
-      break;
-    }
-
-    case kind::VARIABLE:
-    case kind::SKOLEM:
-      os << CVC4_ARITH_VAR_TERM_PREFIX << ProofManager::sanitize(term);
-      break;
-
-    default:
-      Debug("pf::arith") << "Default printing of term: " << term << std::endl;
-      os << term;
-      break;
-  }
-  os << closing.str();
-}
-
-void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) {
-  Debug("pf::arith") << "Arith print sort: " << type << std::endl;
-  os << type;
-}
-
-std::string LFSCArithProof::getLfscFunction(const Node & n) {
-  Assert(n.getType().isInteger() || n.getType().isReal() || n.getType().isBoolean());
-  std::string opString;
-  switch (n.getKind()) {
-    case kind::UMINUS:
-      opString = "u-_";
-      break;
-    case kind::PLUS:
-      opString = "+_";
-      break;
-    case kind::MINUS:
-      opString = "-_";
-      break;
-    case kind::MULT:
-      opString = "*_";
-      break;
-    case kind::DIVISION:
-    case kind::DIVISION_TOTAL:
-      opString = "/_";
-      break;
-    case kind::GT:
-      opString = ">_";
-      break;
-    case kind::GEQ:
-      opString = ">=_";
-      break;
-    case kind::LT:
-      opString = "<_";
-      break;
-    case kind::LEQ:
-      opString = "<=_";
-      break;
-    default:
-      Unreachable() << "Tried to get the operator for a non-operator kind: " << n.getKind();
-  }
-  std::string typeString;
-  if (n.getType().isInteger()) {
-    typeString = "Int";
-  } else if (n.getType().isReal()) {
-    typeString = "Real";
-  } else { // Boolean
-    if (n[0].getType().isInteger()) {
-      typeString = "IntReal";
-    } else {
-      typeString = "Real";
-    }
-  }
-  return opString + typeString;
-}
-
-void LFSCArithProof::printRational(std::ostream& o, const Rational& r)
-{
-  if (r.sgn() < 0)
-  {
-    o << "(~ " << r.getNumerator().abs() << "/" << r.getDenominator().abs()
-      << ")";
-  }
-  else
-  {
-    o << r.getNumerator() << "/" << r.getDenominator();
-  }
-}
-
-void LFSCArithProof::printInteger(std::ostream& o, const Integer& i)
-{
-  if (i.sgn() < 0)
-  {
-    o << "(~ " << i.abs() << ")";
-  }
-  else
-  {
-    o << i;
-  }
-}
-
-void LFSCArithProof::printLinearPolynomialNormalizer(std::ostream& o,
-                                                     const Node& n)
-{
-  switch (n.getKind())
-  {
-    case kind::PLUS:
-    {
-      // Since our axioms are binary, but n may be n-ary, we rig up
-      // a right-associative tree.
-      size_t nchildren = n.getNumChildren();
-      for (size_t i = 0; i < nchildren; ++i)
-      {
-        if (i < nchildren - 1)
-        {
-          o << "\n      (is_aff_+ _ _ _ _ _ ";
-        }
-        printLinearMonomialNormalizer(o, n[i]);
-      }
-      std::fill_n(std::ostream_iterator<char>(o), nchildren - 1, ')');
-      break;
-    }
-    case kind::MULT:
-    case kind::VARIABLE:
-    case kind::CONST_RATIONAL:
-    case kind::SKOLEM:
-    {
-      printLinearMonomialNormalizer(o, n);
-      break;
-    }
-    default:
-      Unreachable() << "Invalid operation " << n.getKind()
-                    << " in linear polynomial";
-      break;
-  }
-}
-
-void LFSCArithProof::printLinearMonomialNormalizer(std::ostream& o,
-                                                   const Node& n)
-{
-  switch (n.getKind())
-  {
-    case kind::MULT: {
-      Assert((n[0].getKind() == kind::CONST_RATIONAL
-              && (n[1].getKind() == kind::VARIABLE
-                  || n[1].getKind() == kind::SKOLEM)))
-          << "node " << n << " is not a linear monomial"
-          << " " << n[0].getKind() << " " << n[1].getKind();
-
-      o << "\n        (is_aff_mul_c_L _ _ _ ";
-      printConstRational(o, n[0]);
-      o << " ";
-      printVariableNormalizer(o, n[1]);
-      o << ")";
-      break;
-    }
-    case kind::CONST_RATIONAL:
-    {
-      o << "\n        (is_aff_const ";
-      printConstRational(o, n);
-      o << ")";
-      break;
-    }
-    case kind::VARIABLE:
-    case kind::SKOLEM:
-    {
-      o << "\n        ";
-      printVariableNormalizer(o, n);
-      break;
-    }
-    default:
-      Unreachable() << "Invalid operation " << n.getKind()
-                    << " in linear monomial";
-      break;
-  }
-}
-
-void LFSCArithProof::printConstRational(std::ostream& o, const Node& n)
-{
-  Assert(n.getKind() == kind::CONST_RATIONAL);
-  const Rational value = n.getConst<Rational>();
-  printRational(o, value);
-}
-
-void LFSCArithProof::printVariableNormalizer(std::ostream& o, const Node& n)
-{
-  std::ostringstream msg;
-  Assert(n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM)
-      << "Invalid variable kind " << n.getKind() << " in linear monomial";
-  if (n.getType().isInteger()) {
-    o << "(is_aff_var_int ";
-  } else if (n.getType().isReal()) {
-    o << "(is_aff_var_real ";
-  } else {
-    Unreachable();
-  }
-  o << n << ")";
-}
-
-void LFSCArithProof::printLinearPolynomialPredicateNormalizer(std::ostream& o,
-                                                              const Node& n)
-{
-  Assert(n.getKind() == kind::GEQ)
-      << "can only print normalization witnesses for (>=) nodes";
-  Assert(n[1].getKind() == kind::CONST_RATIONAL);
-  o << "\n    (is_aff_- _ _ _ _ _ ";
-  printLinearPolynomialNormalizer(o, n[0]);
-  o << "\n      (is_aff_const ";
-  printConstRational(o, n[1]);
-  o << "))";
-}
-
-std::pair<Node, std::string> LFSCArithProof::printProofAndMaybeTighten(
-    const Node& bound)
-{
-  const Node & nonNegBound = bound.getKind() == kind::NOT ? bound[0] : bound;
-  std::ostringstream pfOfPossiblyTightenedPredicate;
-  if (nonNegBound[0].getType().isInteger()) {
-    switch(bound.getKind())
-    {
-      case kind::NOT:
-      {
-        // Tighten ~[i >= r] to [i < r] to [i <= {r}] to [-i >= -{r}]
-        // where
-        //    * i is an integer
-        //    * r is a real
-        //    * {r} denotes the greatest int less than r
-        //      it is equivalent to (ceil(r) - 1)
-        Assert(nonNegBound[1].getKind() == kind::CONST_RATIONAL);
-        Rational oldBound = nonNegBound[1].getConst<Rational>();
-        Integer newBound = -(oldBound.ceiling() - 1);
-        // Since the arith theory rewrites bounds to be purely integral or
-        // purely real, mixed bounds should not appear in proofs
-        AlwaysAssert(oldBound.isIntegral()) << "Mixed int/real bound in arith proof";
-        pfOfPossiblyTightenedPredicate
-            << "(tighten_not_>=_IntInt"
-            << " _ _ _ _ ("
-            << "check_neg_of_greatest_integer_below_int ";
-        printInteger(pfOfPossiblyTightenedPredicate, newBound);
-        pfOfPossiblyTightenedPredicate << " ";
-        printInteger(pfOfPossiblyTightenedPredicate, oldBound.ceiling());
-        pfOfPossiblyTightenedPredicate << ") " << ProofManager::getLitName(bound.negate(), "") << ")";
-        Node newLeft = (theory::arith::Polynomial::parsePolynomial(nonNegBound[0]) * -1).getNode();
-        Node newRight = NodeManager::currentNM()->mkConst(Rational(newBound));
-        Node newTerm = NodeManager::currentNM()->mkNode(kind::GEQ, newLeft, newRight);
-        return std::make_pair(newTerm, pfOfPossiblyTightenedPredicate.str());
-      }
-      case kind::GEQ:
-      {
-        // Tighten [i >= r] to [i >= ceil(r)]
-        // where
-        //    * i is an integer
-        //    * r is a real
-        Assert(nonNegBound[1].getKind() == kind::CONST_RATIONAL);
-
-        Rational oldBound = nonNegBound[1].getConst<Rational>();
-        // Since the arith theory rewrites bounds to be purely integral or
-        // purely real, mixed bounds should not appear in proofs
-        AlwaysAssert(oldBound.isIntegral()) << "Mixed int/real bound in arith proof";
-        pfOfPossiblyTightenedPredicate << ProofManager::getLitName(bound.negate(), "");
-        return std::make_pair(bound, pfOfPossiblyTightenedPredicate.str());
-      }
-      default: Unreachable();
-    }
-  } else {
-    return std::make_pair(bound, ProofManager::getLitName(bound.negate(), ""));
-  }
-  // Silence compiler warnings about missing a return.
-  Unreachable();
-}
-
-void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
-                                           std::ostream& os,
-                                           std::ostream& paren,
-                                           const ProofLetMap& map)
-{
-  Debug("pf::arith") << "Printing proof for lemma " << lemma << std::endl;
-  if (Debug.isOn("pf::arith::printTheoryLemmaProof")) {
-    Debug("pf::arith::printTheoryLemmaProof") << "Printing proof for lemma:" << std::endl;
-    for (const auto & conjunct : lemma) {
-      Debug("pf::arith::printTheoryLemmaProof") << "  " << conjunct << std::endl;
-    }
-  }
-  // Prefixes for the names of linearity witnesses
-  const char* linearizedProofPrefix = "pf_aff";
-  std::ostringstream lemmaParen;
-
-  // Construct the set of conflicting literals
-  std::set<Node> conflictSet;
-  std::transform(lemma.begin(),
-                 lemma.end(),
-                 std::inserter(conflictSet, conflictSet.begin()),
-                 [](const Expr& e) {
-                   return NodeManager::currentNM()->fromExpr(e).negate();
-                 });
-
-  // If we have Farkas coefficients stored for this lemma, use them to write a
-  // proof. Otherwise, just `trust` the lemma.
-  if (d_recorder.hasFarkasCoefficients(conflictSet))
-  {
-    // Get farkas coefficients & literal order
-    const auto& farkasInfo = d_recorder.getFarkasCoefficients(conflictSet);
-    const Node& conflict = farkasInfo.first;
-    theory::arith::RationalVectorCP farkasCoefficients = farkasInfo.second;
-    Assert(farkasCoefficients != theory::arith::RationalVectorCPSentinel);
-    Assert(conflict.getNumChildren() == farkasCoefficients->size());
-    const size_t nAntecedents = conflict.getNumChildren();
-
-    // Print proof
-    if (Debug.isOn("pf::arith::printTheoryLemmaProof")) {
-      os << "Farkas:" << std::endl;
-      for (const auto & n : *farkasCoefficients) {
-        os << "  " << n << std::endl;
-      }
-    }
-
-    // Prove affine function bounds from term bounds
-    os << "\n;; Farkas Proof ;;" << std::endl;
-    os << "\n;  Linear Polynomial Proof Conversions";
-    for (size_t i = 0; i != nAntecedents; ++i)
-    {
-      const Node& antecedent = conflict[i];
-      os << "\n  (@ "
-         << ProofManager::getLitName(antecedent.negate(), linearizedProofPrefix)
-         << " ";
-      lemmaParen << ")";
-      const std::pair<Node, std::string> tightened = printProofAndMaybeTighten(antecedent);
-      switch (tightened.first.getKind())
-      {
-        case kind::NOT:
-        {
-          Assert(conflict[i][0].getKind() == kind::GEQ);
-          os << "(aff_>_from_term _ _ _ _ ";
-          break;
-        }
-        case kind::GEQ:
-        {
-          os << "(aff_>=_from_term _ _ _ ";
-          break;
-        }
-        default: Unreachable();
-      }
-      const Node& nonNegTightened = tightened.first.getKind() == kind::NOT ? tightened.first[0] : tightened.first;
-      printLinearPolynomialPredicateNormalizer(os, nonNegTightened);
-      os << " (pf_reified_arith_pred _ _ " << tightened.second << "))";
-    }
-
-    // Now, print the proof of bottom, from affine function bounds
-    os << "\n;  Farkas Combination";
-    os << "\n  (clausify_false (bounded_aff_contra _ _";
-    lemmaParen << "))";
-    for (size_t i = 0; i != nAntecedents; ++i)
-    {
-      const Node& lit = conflict[i];
-      os << "\n    (bounded_aff_add _ _ _ _ _";
-      os << "\n       (bounded_aff_mul_c _ _ _ ";
-      printRational(os, (*farkasCoefficients)[i].abs());
-      os << " " << ProofManager::getLitName(lit.negate(), linearizedProofPrefix)
-         << ")"
-         << " ; " << lit;
-      lemmaParen << ")";
-    }
-
-    os << "\n    bounded_aff_ax_0_>=_0";
-    os << lemmaParen.str();  // Close lemma proof
-  }
-  else
-  {
-    os << "\n; Arithmetic proofs which use reasoning more complex than Farkas "
-          "proofs and bound tightening are currently unsupported\n"
-          "(clausify_false trust)\n";
-  }
-}
-
-void LFSCArithProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
-  // Nothing to do here at this point.
-}
-
-void LFSCArithProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
-  for (ExprSet::const_iterator it = d_declarations.begin();
-       it != d_declarations.end();
-       ++it)
-  {
-    Expr term = *it;
-    Assert(term.isVariable());
-    bool isInt = term.getType().isInteger();
-    const char * var_type = isInt ? "int_var" : "real_var";
-    os << "(% " << ProofManager::sanitize(term) << " " << var_type << "\n";
-    os << "(@ " << CVC4_ARITH_VAR_TERM_PREFIX << ProofManager::sanitize(term)
-       << " ";
-    os << "(term_" << var_type << " " << ProofManager::sanitize(term) << ")\n";
-    paren << ")";
-    paren << ")";
-  }
-}
-
-void LFSCArithProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
-  // Nothing to do here at this point.
-}
-
-void LFSCArithProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
-  // Nothing to do here at this point.
-}
-
-bool LFSCArithProof::printsAsBool(const Node& n)
-{
-  // Our boolean variables and constants print as sort Bool.
-  // All complex booleans print as formulas.
-  return n.getType().isBoolean() and (n.isVar() or n.isConst());
-}
-
-TypeNode LFSCArithProof::equalityType(const Expr& left, const Expr& right)
-{
-  return TypeNode::fromType(!left.getType().isInteger() ? left.getType() : right.getType());
-}
-
-} /* CVC4  namespace */