Move proof utilities to src/proof/ (#6611)

This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.

It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").

34 files changed, 0 insertions, 7650 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 9bf63dcfc..094c7bcbd 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -24,8 +24,6 @@ libcvc5_add_sources(
   attribute_unique_id.h
   bound_var_manager.cpp
   bound_var_manager.h
-  buffered_proof_generator.cpp
-  buffered_proof_generator.h
   emptyset.cpp
   emptyset.h
   emptybag.cpp
@@ -33,10 +31,6 @@ libcvc5_add_sources(
   expr_iomanip.cpp
   expr_iomanip.h
   kind_map.h
-  lazy_proof.cpp
-  lazy_proof.h
-  lazy_proof_chain.cpp
-  lazy_proof_chain.h
   match_trie.cpp
   match_trie.h
   node.cpp
@@ -58,37 +52,12 @@ libcvc5_add_sources(
   sequence.cpp
   sequence.h
   node_visitor.h
-  proof.cpp
-  proof.h
-  proof_checker.cpp
-  proof_checker.h
-  proof_ensure_closed.cpp
-  proof_ensure_closed.h
-  proof_generator.cpp
-  proof_generator.h
-  proof_node.cpp
-  proof_node.h
-  proof_node_algorithm.cpp
-  proof_node_algorithm.h
-  proof_node_to_sexpr.cpp
-  proof_node_to_sexpr.h
-  proof_node_manager.cpp
-  proof_node_manager.h
-  proof_node_updater.cpp
-  proof_node_updater.h
-  proof_rule.cpp
-  proof_rule.h
-  proof_set.h
-  proof_step_buffer.cpp
-  proof_step_buffer.h
   skolem_manager.cpp
   skolem_manager.h
   symbol_manager.cpp
   symbol_manager.h
   symbol_table.cpp
   symbol_table.h
-  tconv_seq_proof_generator.cpp
-  tconv_seq_proof_generator.h
   term_canonize.cpp
   term_canonize.h
   term_context.cpp
@@ -97,8 +66,6 @@ libcvc5_add_sources(
   term_context_node.h
   term_context_stack.cpp
   term_context_stack.h
-  term_conversion_proof_generator.cpp
-  term_conversion_proof_generator.h
   type_checker.h
   type_matcher.cpp
   type_matcher.h
diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp
deleted file mode 100644
index 2cbbd7e91..000000000
--- a/src/expr/buffered_proof_generator.cpp
+++ /dev/null
@@ -1,103 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of a proof generator for buffered proof steps.
- */
-
-#include "expr/buffered_proof_generator.h"
-
-#include "expr/proof.h"
-#include "expr/proof_node_manager.h"
-
-namespace cvc5 {
-
-BufferedProofGenerator::BufferedProofGenerator(context::Context* c,
-                                               ProofNodeManager* pnm)
-    : ProofGenerator(), d_facts(c), d_pnm(pnm)
-{
-}
-
-bool BufferedProofGenerator::addStep(Node fact,
-                                     ProofStep ps,
-                                     CDPOverwrite opolicy)
-{
-  // check duplicates if we are not always overwriting
-  if (opolicy != CDPOverwrite::ALWAYS)
-  {
-    if (d_facts.find(fact) != d_facts.end())
-    {
-      // duplicate
-      return false;
-    }
-    Node symFact = CDProof::getSymmFact(fact);
-    if (!symFact.isNull())
-    {
-      if (d_facts.find(symFact) != d_facts.end())
-      {
-        // duplicate due to symmetry
-        return false;
-      }
-    }
-  }
-  // note that this replaces the value fact is mapped to if there is already one
-  d_facts.insert(fact, std::make_shared<ProofStep>(ps));
-  return true;
-}
-
-std::shared_ptr<ProofNode> BufferedProofGenerator::getProofFor(Node fact)
-{
-  Trace("pfee-fact-gen") << "BufferedProofGenerator::getProofFor: " << fact
-                         << std::endl;
-  NodeProofStepMap::iterator it = d_facts.find(fact);
-  if (it == d_facts.end())
-  {
-    Node symFact = CDProof::getSymmFact(fact);
-    if (symFact.isNull())
-    {
-      Trace("pfee-fact-gen") << "...cannot find step" << std::endl;
-      Assert(false);
-      return nullptr;
-    }
-    it = d_facts.find(symFact);
-    if (it == d_facts.end())
-    {
-      Assert(false);
-      Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl;
-      return nullptr;
-    }
-  }
-  Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl;
-  CDProof cdp(d_pnm);
-  cdp.addStep(fact, *(*it).second);
-  return cdp.getProofFor(fact);
-}
-
-bool BufferedProofGenerator::hasProofFor(Node f)
-{
-  NodeProofStepMap::iterator it = d_facts.find(f);
-  if (it == d_facts.end())
-  {
-    Node symFact = CDProof::getSymmFact(f);
-    if (symFact.isNull())
-    {
-      return false;
-    }
-    it = d_facts.find(symFact);
-    if (it == d_facts.end())
-    {
-      return false;
-    }
-  }
-  return true;
-}
-
-}  // namespace cvc5
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
deleted file mode 100644
index 2e1ef6c53..000000000
--- a/src/expr/buffered_proof_generator.h
+++ /dev/null
@@ -1,64 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Haniel Barbosa, Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * A proof generator for buffered proof steps.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H
-#define CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H
-
-#include "context/cdhashmap.h"
-#include "expr/proof_generator.h"
-
-namespace cvc5 {
-
-class ProofNodeManager;
-class ProofStep;
-
-/**
- * The proof generator for buffered steps. This class is a context-dependent
- * mapping from formulas to proof steps. It does not generate ProofNodes until it
- * is asked to provide a proof for a given fact.
- */
-class BufferedProofGenerator : public ProofGenerator
-{
-  typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>> NodeProofStepMap;
-
- public:
-  BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm);
-  ~BufferedProofGenerator() {}
-  /** add step
-   * Unless the overwrite policy is ALWAYS it does not replace previously
-   * registered steps (modulo (dis)equality symmetry).
-   */
-  bool addStep(Node fact,
-               ProofStep ps,
-               CDPOverwrite opolicy = CDPOverwrite::NEVER);
-  /** Get proof for. It is robust to (dis)equality symmetry. */
-  std::shared_ptr<ProofNode> getProofFor(Node f) override;
-  /** Whether a step has been registered for f. */
-  bool hasProofFor(Node f) override;
-  /** identify */
-  std::string identify() const override { return "BufferedProofGenerator"; }
-
- private:
-  /** maps expected to ProofStep */
-  NodeProofStepMap d_facts;
-  /** the proof node manager */
-  ProofNodeManager* d_pnm;
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H */
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
deleted file mode 100644
index 8a54637fa..000000000
--- a/src/expr/lazy_proof.cpp
+++ /dev/null
@@ -1,232 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of lazy proof utility.
- */
-
-#include "expr/lazy_proof.h"
-
-#include "expr/proof_ensure_closed.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
-
-using namespace cvc5::kind;
-
-namespace cvc5 {
-
-LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
-                         ProofGenerator* dpg,
-                         context::Context* c,
-                         std::string name)
-    : CDProof(pnm, c, name), d_gens(c ? c : &d_context), d_defaultGen(dpg)
-{
-}
-
-LazyCDProof::~LazyCDProof() {}
-
-std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
-{
-  Trace("lazy-cdproof") << "LazyCDProof::mkLazyProof " << fact << std::endl;
-  // make the proof, which should always be non-null, since we construct an
-  // assumption in the worst case.
-  std::shared_ptr<ProofNode> opf = CDProof::getProofFor(fact);
-  Assert(opf != nullptr);
-  if (!hasGenerators())
-  {
-    Trace("lazy-cdproof") << "...no generators, finished" << std::endl;
-    // optimization: no generators, we are done
-    return opf;
-  }
-  // otherwise, we traverse the proof opf and fill in the ASSUME leafs that
-  // have generators
-  std::unordered_set<ProofNode*> visited;
-  std::unordered_set<ProofNode*>::iterator it;
-  std::vector<ProofNode*> visit;
-  ProofNode* cur;
-  visit.push_back(opf.get());
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    it = visited.find(cur);
-
-    if (it == visited.end())
-    {
-      visited.insert(cur);
-      Node cfact = cur->getResult();
-      if (getProof(cfact).get() != cur)
-      {
-        // We don't own this proof, skip it. This is to ensure that this method
-        // is idempotent, since it may be the case that a previous call to
-        // getProofFor connected a proof from a proof generator as a child of
-        // a ProofNode in the range of the map in CDProof. Thus, this ensures
-        // we don't touch such proofs.
-        Trace("lazy-cdproof") << "...skip unowned proof" << std::endl;
-      }
-      else if (cur->getRule() == PfRule::ASSUME)
-      {
-        bool isSym = false;
-        ProofGenerator* pg = getGeneratorFor(cfact, isSym);
-        if (pg != nullptr)
-        {
-          Trace("lazy-cdproof")
-              << "LazyCDProof: Call generator " << pg->identify()
-              << " for assumption " << cfact << std::endl;
-          Node cfactGen = isSym ? CDProof::getSymmFact(cfact) : cfact;
-          Assert(!cfactGen.isNull());
-          // Do not use the addProofTo interface, instead use the update node
-          // interface, since this ensures that we don't take ownership for
-          // the current proof. Instead, it is only linked, and ignored on
-          // future calls to getProofFor due to the check above.
-          std::shared_ptr<ProofNode> pgc = pg->getProofFor(cfactGen);
-          // If the proof was null, then the update is not performed. This is
-          // not considered an error, since this behavior is equivalent to
-          // if pg had provided the proof (ASSUME cfactGen). Ensuring the
-          // proper behavior wrt closed proofs should be done outside this
-          // method.
-          if (pgc != nullptr)
-          {
-            Trace("lazy-cdproof-gen")
-                << "LazyCDProof: stored proof: " << *pgc.get() << std::endl;
-
-            if (isSym)
-            {
-              d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {});
-            }
-            else
-            {
-              d_manager->updateNode(cur, pgc.get());
-            }
-            Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for "
-                                  << cfactGen << std::endl;
-          }
-        }
-        else
-        {
-          Trace("lazy-cdproof") << "LazyCDProof: " << identify()
-                                << " : No generator for " << cfact << std::endl;
-        }
-        // Notice that we do not traverse the proofs that have been generated
-        // lazily by the proof generators here.  In other words, we assume that
-        // the proofs from provided proof generators are final and need
-        // no further modification by this class.
-      }
-      else
-      {
-        const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
-        for (const std::shared_ptr<ProofNode>& cp : cc)
-        {
-          visit.push_back(cp.get());
-        }
-      }
-    }
-  } while (!visit.empty());
-  // we have now updated the ASSUME leafs of opf, return it
-  Trace("lazy-cdproof") << "...finished" << std::endl;
-  Assert(opf->getResult() == fact);
-  return opf;
-}
-
-void LazyCDProof::addLazyStep(Node expected,
-                              ProofGenerator* pg,
-                              PfRule idNull,
-                              bool isClosed,
-                              const char* ctx,
-                              bool forceOverwrite)
-{
-  if (pg == nullptr)
-  {
-    // null generator, should have given a proof rule
-    if (idNull == PfRule::ASSUME)
-    {
-      Unreachable() << "LazyCDProof::addLazyStep: " << identify()
-                    << ": failed to provide proof generator for " << expected;
-      return;
-    }
-    Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
-                          << " set (trusted) step " << idNull << "\n";
-    addStep(expected, idNull, {}, {expected});
-    return;
-  }
-  Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
-                        << " set to generator " << pg->identify() << "\n";
-  if (!forceOverwrite)
-  {
-    NodeProofGeneratorMap::const_iterator it = d_gens.find(expected);
-    if (it != d_gens.end())
-    {
-      // don't overwrite something that is already there
-      return;
-    }
-  }
-  // just store now
-  d_gens.insert(expected, pg);
-  // debug checking
-  if (isClosed)
-  {
-    Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl;
-    pfgEnsureClosed(expected, pg, "lazy-cdproof-debug", ctx);
-  }
-}
-
-ProofGenerator* LazyCDProof::getGeneratorFor(Node fact,
-                                             bool& isSym)
-{
-  isSym = false;
-  NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
-  if (it != d_gens.end())
-  {
-    return (*it).second;
-  }
-  Node factSym = CDProof::getSymmFact(fact);
-  // could be symmetry
-  if (factSym.isNull())
-  {
-    // can't be symmetry, return the default generator
-    return d_defaultGen;
-  }
-  it = d_gens.find(factSym);
-  if (it != d_gens.end())
-  {
-    isSym = true;
-    return (*it).second;
-  }
-  // return the default generator
-  return d_defaultGen;
-}
-
-bool LazyCDProof::hasGenerators() const
-{
-  return !d_gens.empty() || d_defaultGen != nullptr;
-}
-
-bool LazyCDProof::hasGenerator(Node fact) const
-{
-  if (d_defaultGen != nullptr)
-  {
-    return true;
-  }
-  NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
-  if (it != d_gens.end())
-  {
-    return true;
-  }
-  // maybe there is a symmetric fact?
-  Node factSym = CDProof::getSymmFact(fact);
-  if (!factSym.isNull())
-  {
-    it = d_gens.find(factSym);
-  }
-  return it != d_gens.end();
-}
-
-}  // namespace cvc5
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
deleted file mode 100644
index efcda94bd..000000000
--- a/src/expr/lazy_proof.h
+++ /dev/null
@@ -1,110 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Lazy proof utility.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__LAZY_PROOF_H
-#define CVC5__EXPR__LAZY_PROOF_H
-
-#include "expr/proof.h"
-
-namespace cvc5 {
-
-class ProofGenerator;
-class ProofNodeManager;
-
-/**
- * A (context-dependent) lazy proof. This class is an extension of CDProof
- * that additionally maps facts to proof generators in a context-dependent
- * manner. It extends CDProof with an additional method, addLazyStep for adding
- * steps to a proof via a given proof generator.
- */
-class LazyCDProof : public CDProof
-{
- public:
-  /** Constructor
-   *
-   * @param pnm The proof node manager for constructing ProofNode objects.
-   * @param dpg The (optional) default proof generator, which is called
-   * for facts that have no explicitly provided generator.
-   * @param c The context that this class depends on. If none is provided,
-   * this class is context-independent.
-   */
-  LazyCDProof(ProofNodeManager* pnm,
-              ProofGenerator* dpg = nullptr,
-              context::Context* c = nullptr,
-              std::string name = "LazyCDProof");
-  ~LazyCDProof();
-  /**
-   * Get lazy proof for fact, or nullptr if it does not exist. This may
-   * additionally call proof generators to generate proofs for ASSUME nodes that
-   * don't yet have a concrete proof.
-   */
-  std::shared_ptr<ProofNode> getProofFor(Node fact) override;
-  /** Add step by generator
-   *
-   * This method stores that expected can be proven by proof generator pg if
-   * it is required to do so. This mapping is maintained in the remainder of
-   * the current context (according to the context c provided to this class).
-   *
-   * It is important to note that pg is asked to provide a proof for expected
-   * only when no other call for the fact expected is provided via the addStep
-   * method of this class. In particular, pg is asked to prove expected when it
-   * appears as the conclusion of an ASSUME leaf within CDProof::getProofFor.
-   *
-   * @param expected The fact that can be proven.
-   * @param pg The generator that can proof expected.
-   * @param trustId If a null proof generator is provided, we add a step to
-   * the proof that has trustId as the rule and expected as the sole argument.
-   * We do this only if trustId is not PfRule::ASSUME. This is primarily used
-   * for identifying the kind of hole when a proof generator is not given.
-   * @param isClosed Whether to expect that pg can provide a closed proof for
-   * this fact.
-   * @param ctx The context we are in (for debugging).
-   * @param forceOverwrite If this flag is true, then this call overwrites
-   * an existing proof generator provided for expected, if one was provided
-   * via a previous call to addLazyStep in the current context.
-   */
-  void addLazyStep(Node expected,
-                   ProofGenerator* pg,
-                   PfRule trustId = PfRule::ASSUME,
-                   bool isClosed = false,
-                   const char* ctx = "LazyCDProof::addLazyStep",
-                   bool forceOverwrite = false);
-  /**
-   * Does this have any proof generators? This method always returns true
-   * if the default is non-null.
-   */
-  bool hasGenerators() const;
-  /** Does the given fact have an explicitly provided generator? */
-  bool hasGenerator(Node fact) const;
-
- protected:
-  typedef context::CDHashMap<Node, ProofGenerator*> NodeProofGeneratorMap;
-  /** Maps facts that can be proven to generators */
-  NodeProofGeneratorMap d_gens;
-  /** The default proof generator */
-  ProofGenerator* d_defaultGen;
-  /**
-   * Get generator for fact, or nullptr if it doesnt exist. This method is
-   * robust to symmetry of (dis)equality. It updates isSym to true if a
-   * proof generator for the symmetric form of fact was provided.
-   */
-  ProofGenerator* getGeneratorFor(Node fact, bool& isSym);
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__LAZY_PROOF_H */
diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
deleted file mode 100644
index 3ce2212be..000000000
--- a/src/expr/lazy_proof_chain.cpp
+++ /dev/null
@@ -1,327 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Haniel Barbosa, Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of lazy proof utility.
- */
-
-#include "expr/lazy_proof_chain.h"
-
-#include "expr/proof.h"
-#include "expr/proof_ensure_closed.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_algorithm.h"
-#include "expr/proof_node_manager.h"
-#include "options/proof_options.h"
-
-namespace cvc5 {
-
-LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
-                                   bool cyclic,
-                                   context::Context* c,
-                                   ProofGenerator* defGen,
-                                   bool defRec)
-    : d_manager(pnm),
-      d_cyclic(cyclic),
-      d_defRec(defRec),
-      d_context(),
-      d_gens(c ? c : &d_context),
-      d_defGen(defGen)
-{
-}
-
-LazyCDProofChain::~LazyCDProofChain() {}
-
-const std::map<Node, std::shared_ptr<ProofNode>> LazyCDProofChain::getLinks()
-    const
-{
-  std::map<Node, std::shared_ptr<ProofNode>> links;
-  for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
-  {
-    Assert(link.second);
-    std::shared_ptr<ProofNode> pfn = link.second->getProofFor(link.first);
-    Assert(pfn);
-    links[link.first] = pfn;
-  }
-  return links;
-}
-
-std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
-{
-  Trace("lazy-cdproofchain")
-      << "LazyCDProofChain::getProofFor " << fact << "\n";
-  // which facts have had proofs retrieved for. This is maintained to avoid
-  // cycles. It also saves the proof node of the fact
-  std::unordered_map<Node, std::shared_ptr<ProofNode>> toConnect;
-  // leaves of proof node links in the chain, i.e. assumptions, yet to be
-  // expanded
-  std::unordered_map<Node, std::vector<std::shared_ptr<ProofNode>>>
-      assumptionsToExpand;
-  // invariant of the loop below, the first iteration notwithstanding:
-  //   visit = domain(assumptionsToExpand) \ domain(toConnect)
-  std::vector<Node> visit{fact};
-  std::unordered_map<Node, bool> visited;
-  Node cur;
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    auto itVisited = visited.find(cur);
-    // pre-traversal
-    if (itVisited == visited.end())
-    {
-      Trace("lazy-cdproofchain")
-          << "LazyCDProofChain::getProofFor: check " << cur << "\n";
-      Assert(toConnect.find(cur) == toConnect.end());
-      bool rec = true;
-      ProofGenerator* pg = getGeneratorForInternal(cur, rec);
-      if (!pg)
-      {
-        Trace("lazy-cdproofchain")
-            << "LazyCDProofChain::getProofFor: nothing to do\n";
-        // nothing to do for this fact, it'll be a leaf in the final proof
-        // node, don't post-traverse.
-        visited[cur] = true;
-        continue;
-      }
-      Trace("lazy-cdproofchain")
-          << "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
-          << " for chain link " << cur << "\n";
-      std::shared_ptr<ProofNode> curPfn = pg->getProofFor(cur);
-      if (curPfn == nullptr)
-      {
-        Trace("lazy-cdproofchain")
-            << "LazyCDProofChain::getProofFor: No proof found, skip\n";
-        visited[cur] = true;
-        continue;
-      }
-      // map node whose proof node must be expanded to the respective poof node
-      toConnect[cur] = curPfn;
-      if (!rec)
-      {
-        // we don't want to recursively connect this proof
-        visited[cur] = true;
-        continue;
-      }
-      Trace("lazy-cdproofchain-debug")
-          << "LazyCDProofChain::getProofFor: stored proof: " << *curPfn.get()
-          << "\n";
-      // retrieve free assumptions and their respective proof nodes
-      std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
-      expr::getFreeAssumptionsMap(curPfn, famap);
-      if (Trace.isOn("lazy-cdproofchain"))
-      {
-        unsigned alreadyToVisit = 0;
-        Trace("lazy-cdproofchain")
-            << "LazyCDProofChain::getProofFor: " << famap.size()
-            << " free assumptions:\n";
-        for (auto fap : famap)
-        {
-          Trace("lazy-cdproofchain")
-              << "LazyCDProofChain::getProofFor:  - " << fap.first << "\n";
-          alreadyToVisit +=
-              std::find(visit.begin(), visit.end(), fap.first) != visit.end()
-                  ? 1
-                  : 0;
-        }
-        Trace("lazy-cdproofchain")
-            << "LazyCDProofChain::getProofFor: " << alreadyToVisit
-            << " already to visit\n";
-      }
-      // mark for post-traversal if we are controlling cycles
-      if (d_cyclic)
-      {
-        Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: marking "
-                                   << cur << " for cycle check\n";
-        visit.push_back(cur);
-        visited[cur] = false;
-      }
-      else
-      {
-        visited[cur] = true;
-      }
-      // enqueue free assumptions to process
-      for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
-               fap : famap)
-      {
-        // check cycles
-        if (d_cyclic)
-        {
-          // cycles are assumptions being *currently* expanded and seen again,
-          // i.e. in toConnect and not yet post-visited
-          auto itToConnect = toConnect.find(fap.first);
-          if (itToConnect != toConnect.end() && !visited[fap.first])
-          {
-            // Since we have a cycle with an assumption, this fact will be an
-            // assumption in the final proof node produced by this
-            // method. Thus we erase it as something to be connected, which
-            // will keep it as an assumption.
-            Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: "
-                                          "removing cyclic assumption "
-                                       << fap.first << " from expansion\n";
-            continue;
-          }
-        }
-        // We always add assumptions to visit so that their last seen occurrence
-        // is expanded (rather than the first seen occurrence, if we were not
-        // adding assumptions, say, in assumptionsToExpand). This is so because
-        // in the case where we are checking cycles this is necessary (and
-        // harmless when we are not). For example the cycle
-        //
-        //                 a2
-        //                ...
-        //               ----
-        //                a1
-        //               ...
-        //             --------
-        //   a0   a1    a2
-        //       ...
-        //  ---------------
-        //       n
-        //
-        // in which a2 has a1 as an assumption, which has a2 an assumption,
-        // would not be captured if we did not revisit a1, which is an
-        // assumption of n and this already occur in assumptionsToExpand when
-        // it shows up again as an assumption of a2.
-        visit.push_back(fap.first);
-        // add assumption proof nodes to be updated
-        assumptionsToExpand[fap.first].insert(
-            assumptionsToExpand[fap.first].end(),
-            fap.second.begin(),
-            fap.second.end());
-      }
-      if (d_cyclic)
-      {
-        Trace("lazy-cdproofchain") << push;
-        Trace("lazy-cdproofchain-debug") << push;
-      }
-    }
-    else if (!itVisited->second)
-    {
-      visited[cur] = true;
-      Trace("lazy-cdproofchain") << pop;
-      Trace("lazy-cdproofchain-debug") << pop;
-      Trace("lazy-cdproofchain")
-          << "LazyCDProofChain::getProofFor: post-visited " << cur << "\n";
-    }
-    else
-    {
-      Trace("lazy-cdproofchain")
-          << "LazyCDProofChain::getProofFor: already fully processed " << cur
-          << "\n";
-    }
-  } while (!visit.empty());
-  // expand all assumptions marked to be connected
-  for (const std::pair<const Node, std::shared_ptr<ProofNode>>& npfn :
-       toConnect)
-  {
-    auto it = assumptionsToExpand.find(npfn.first);
-    if (it == assumptionsToExpand.end())
-    {
-      Assert(npfn.first == fact);
-      continue;
-    }
-    Assert(npfn.second);
-    Trace("lazy-cdproofchain")
-        << "LazyCDProofChain::getProofFor: expand assumption " << npfn.first
-        << "\n";
-    Trace("lazy-cdproofchain-debug")
-        << "LazyCDProofChain::getProofFor: ...expand to " << *npfn.second.get()
-        << "\n";
-    // update each assumption proof node
-    for (std::shared_ptr<ProofNode> pfn : it->second)
-    {
-      d_manager->updateNode(pfn.get(), npfn.second.get());
-    }
-  }
-  // final proof of fact
-  auto it = toConnect.find(fact);
-  if (it == toConnect.end())
-  {
-    return nullptr;
-  }
-  return it->second;
-}
-
-void LazyCDProofChain::addLazyStep(Node expected, ProofGenerator* pg)
-{
-  Assert(pg != nullptr);
-  Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
-                             << " set to generator " << pg->identify() << "\n";
-  // note this will replace the generator for expected, if any
-  d_gens.insert(expected, pg);
-}
-
-void LazyCDProofChain::addLazyStep(Node expected,
-                                   ProofGenerator* pg,
-                                   const std::vector<Node>& assumptions,
-                                   const char* ctx)
-{
-  Assert(pg != nullptr);
-  Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
-                             << " set to generator " << pg->identify() << "\n";
-  // note this will rewrite the generator for expected, if any
-  d_gens.insert(expected, pg);
-  // check if chain is closed if options::proofEagerChecking() is on
-  if (options::proofEagerChecking())
-  {
-    Trace("lazy-cdproofchain")
-        << "LazyCDProofChain::addLazyStep: Checking closed proof...\n";
-    std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected);
-    std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()};
-    // add all current links in the chain
-    for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
-    {
-      allowedLeaves.push_back(link.first);
-    }
-    if (Trace.isOn("lazy-cdproofchain"))
-    {
-      Trace("lazy-cdproofchain") << "Checking relative to leaves...\n";
-      for (const Node& n : allowedLeaves)
-      {
-        Trace("lazy-cdproofchain") << "  - " << n << "\n";
-      }
-      Trace("lazy-cdproofchain") << "\n";
-    }
-    pfnEnsureClosedWrt(pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx);
-  }
-}
-
-bool LazyCDProofChain::hasGenerator(Node fact) const
-{
-  return d_gens.find(fact) != d_gens.end();
-}
-
-ProofGenerator* LazyCDProofChain::getGeneratorFor(Node fact)
-{
-  bool rec = true;
-  return getGeneratorForInternal(fact, rec);
-}
-
-ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec)
-{
-  auto it = d_gens.find(fact);
-  if (it != d_gens.end())
-  {
-    return (*it).second;
-  }
-  // otherwise, if no explicit generators, we use the default one
-  if (d_defGen != nullptr)
-  {
-    rec = d_defRec;
-    return d_defGen;
-  }
-  return nullptr;
-}
-
-std::string LazyCDProofChain::identify() const { return "LazyCDProofChain"; }
-
-}  // namespace cvc5
diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
deleted file mode 100644
index 1abb3f84e..000000000
--- a/src/expr/lazy_proof_chain.h
+++ /dev/null
@@ -1,154 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Haniel Barbosa, Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Lazy proof chain utility.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__LAZY_PROOF_CHAIN_H
-#define CVC5__EXPR__LAZY_PROOF_CHAIN_H
-
-#include <vector>
-
-#include "context/cdhashmap.h"
-#include "expr/proof_generator.h"
-
-namespace cvc5 {
-
-class ProofNodeManager;
-
-/**
- * A (context-dependent) lazy generator for proof chains. This class is an
- * extension of ProofGenerator that additionally that maps facts to proof
- * generators in a context-dependent manner. The map is built with the addition
- * of lazy steps mapping facts to proof generators. More importantly, its
- * getProofFor method expands the proof generators registered to this class by
- * connecting, for the proof generated to one fact, assumptions to the proofs
- * generated for those assumptinos that are registered in the chain.
- */
-class LazyCDProofChain : public ProofGenerator
-{
- public:
-  /** Constructor
-   *
-   * @param pnm The proof node manager for constructing ProofNode objects.
-   * @param cyclic Whether this instance is robust to cycles in the chain.
-   * @param c The context that this class depends on. If none is provided,
-   * this class is context-independent.
-   * @param defGen The default generator to be used if no generator exists
-   * for a step.
-   * @param defRec Whether this instance expands proofs from defGen recursively.
-   */
-  LazyCDProofChain(ProofNodeManager* pnm,
-                   bool cyclic = true,
-                   context::Context* c = nullptr,
-                   ProofGenerator* defGen = nullptr,
-                   bool defRec = true);
-  ~LazyCDProofChain();
-  /**
-   * Get lazy proof for fact, or nullptr if it does not exist, by connecting the
-   * proof nodes generated for each intermediate relevant fact registered in the
-   * chain (i.e., in the domain of d_gens).
-   *
-   * For example, if d_gens consists of the following pairs
-   *
-   * --- (A, PG1)
-   * --- (B, PG2)
-   * --- (C, PG3)
-   *
-   * and getProofFor(A) is called, with PG1 generating a proof with assumptions
-   * B and D, then B is expanded, with its assumption proof node being updated
-   * to the expanded proof node, while D is not. Assuming PG2 provides a proof
-   * with assumptions C and E, then C is expanded and E is not. Suppose PG3
-   * gives a closed proof, thus the call getProofFor(A) produces a proof node
-   *
-   *  A : ( ... B : ( ... C : (...), ... ASSUME( E ) ), ... ASSUME( D ) )
-   *
-   * Note that the expansions are done directly on the proof nodes produced by
-   * the generators.
-   *
-   * If this instance has been set to be robust to cyclic proofs (i.e., d_cyclic
-   * is true), then the construction of the proof chain checks that there are no
-   * cycles, i.e., a given fact would have itself as an assumption when
-   * connecting the chain links. If such a cycle were to be detected then the
-   * fact will be marked as an assumption and not expanded in the final proof
-   * node. The method does not fail.
-   */
-  std::shared_ptr<ProofNode> getProofFor(Node fact) override;
-  /** Add step by generator
-   *
-   * This method stores that expected can be proven by proof generator pg if
-   * it is required to do so. This mapping is maintained in the remainder of
-   * the current context (according to the context c provided to this class).
-   *
-   * Moreover the lazy steps of this class are expected to fulfill the
-   * requirement that pg.getProofFor(expected) generates a proof node closed
-   * with relation to
-   *  (1) a fixed set F1, ..., Fn,
-   *  (2) formulas in the current domain of d_gens.
-   *
-   * This is so that we only add links to the chain that depend on a fixed set
-   * of assumptions or in other links.
-   *
-   * @param expected The fact that can be proven.
-   * @param pg The generator that can proof expected.
-   * @param assumptions The fixed set of assumptions with relation to which the
-   * chain, now augmented with expect, must be closed.
-   * @param ctx The context we are in (for debugging).
-   */
-  void addLazyStep(Node expected,
-                   ProofGenerator* pg,
-                   const std::vector<Node>& assumptions,
-                   const char* ctx = "LazyCDProofChain::addLazyStep");
-
-  /** As above but does not do the closedness check. */
-  void addLazyStep(Node expected, ProofGenerator* pg);
-
-  /** Does the given fact have an explicitly provided generator? */
-  bool hasGenerator(Node fact) const;
-
-  /**
-   * Get generator for fact, or nullptr if it doesnt exist.
-   */
-  ProofGenerator* getGeneratorFor(Node fact);
-
-  /** identify */
-  std::string identify() const override;
-
-  /** Retrieve, for each fact in d_gens, it mapped to the proof node generated
-   * by its generator in d_gens.  */
-  const std::map<Node, std::shared_ptr<ProofNode>> getLinks() const;
-
- private:
-  /**
-   * Get generator for fact, or nullptr if it doesnt exist. Updates rec to
-   * true if we should recurse on its proof.
-   */
-  ProofGenerator* getGeneratorForInternal(Node fact, bool& rec);
-  /** The proof manager, used for allocating new ProofNode objects */
-  ProofNodeManager* d_manager;
-  /** Whether this instance is robust to cycles in the chain. */
-  bool d_cyclic;
-  /** Whether we expand recursively (for the default generator) */
-  bool d_defRec;
-  /** A dummy context used by this class if none is provided */
-  context::Context d_context;
-  /** Maps facts that can be proven to generators */
-  context::CDHashMap<Node, ProofGenerator*> d_gens;
-  /** The default proof generator (if one exists) */
-  ProofGenerator* d_defGen;
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__LAZY_PROOF_CHAIN_H */
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
deleted file mode 100644
index 289a5be5b..000000000
--- a/src/expr/proof.cpp
+++ /dev/null
@@ -1,459 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of proof.
- */
-
-#include "expr/proof.h"
-
-#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
-
-using namespace cvc5::kind;
-
-namespace cvc5 {
-
-CDProof::CDProof(ProofNodeManager* pnm,
-                 context::Context* c,
-                 std::string name,
-                 bool autoSymm)
-    : d_manager(pnm),
-      d_context(),
-      d_nodes(c ? c : &d_context),
-      d_name(name),
-      d_autoSymm(autoSymm)
-{
-}
-
-CDProof::~CDProof() {}
-
-std::shared_ptr<ProofNode> CDProof::getProofFor(Node fact)
-{
-  std::shared_ptr<ProofNode> pf = getProofSymm(fact);
-  if (pf != nullptr)
-  {
-    return pf;
-  }
-  // add as assumption
-  std::vector<Node> pargs = {fact};
-  std::vector<std::shared_ptr<ProofNode>> passume;
-  std::shared_ptr<ProofNode> pfa =
-      d_manager->mkNode(PfRule::ASSUME, passume, pargs, fact);
-  d_nodes.insert(fact, pfa);
-  return pfa;
-}
-
-std::shared_ptr<ProofNode> CDProof::getProof(Node fact) const
-{
-  NodeProofNodeMap::iterator it = d_nodes.find(fact);
-  if (it != d_nodes.end())
-  {
-    return (*it).second;
-  }
-  return nullptr;
-}
-
-std::shared_ptr<ProofNode> CDProof::getProofSymm(Node fact)
-{
-  Trace("cdproof") << "CDProof::getProofSymm: " << fact << std::endl;
-  std::shared_ptr<ProofNode> pf = getProof(fact);
-  if (pf != nullptr && !isAssumption(pf.get()))
-  {
-    Trace("cdproof") << "...existing non-assume " << pf->getRule() << std::endl;
-    return pf;
-  }
-  else if (!d_autoSymm)
-  {
-    Trace("cdproof") << "...not auto considering symmetry" << std::endl;
-    return pf;
-  }
-  Node symFact = getSymmFact(fact);
-  if (symFact.isNull())
-  {
-    Trace("cdproof") << "...no possible symm" << std::endl;
-    // no symmetry possible, return original proof (possibly assumption)
-    return pf;
-  }
-  // See if a proof exists for the opposite direction, if so, add the step.
-  // Notice that SYMM is also disallowed.
-  std::shared_ptr<ProofNode> pfs = getProof(symFact);
-  if (pfs != nullptr)
-  {
-    // The symmetric fact exists, and the current one either does not, or is
-    // an assumption. We make a new proof that applies SYMM to pfs.
-    std::vector<std::shared_ptr<ProofNode>> pschild;
-    pschild.push_back(pfs);
-    std::vector<Node> args;
-    if (pf == nullptr)
-    {
-      Trace("cdproof") << "...fresh make symm" << std::endl;
-      std::shared_ptr<ProofNode> psym =
-          d_manager->mkNode(PfRule::SYMM, pschild, args, fact);
-      Assert(psym != nullptr);
-      d_nodes.insert(fact, psym);
-      return psym;
-    }
-    else if (!isAssumption(pfs.get()))
-    {
-      // if its not an assumption, make the connection
-      Trace("cdproof") << "...update symm" << std::endl;
-      // update pf
-      bool sret = d_manager->updateNode(pf.get(), PfRule::SYMM, pschild, args);
-      AlwaysAssert(sret);
-    }
-  }
-  else
-  {
-    Trace("cdproof") << "...no symm, return "
-                     << (pf == nullptr ? "null" : "non-null") << std::endl;
-  }
-  // return original proof (possibly assumption)
-  return pf;
-}
-
-bool CDProof::addStep(Node expected,
-                      PfRule id,
-                      const std::vector<Node>& children,
-                      const std::vector<Node>& args,
-                      bool ensureChildren,
-                      CDPOverwrite opolicy)
-{
-  Trace("cdproof") << "CDProof::addStep: " << identify() << " : " << id << " "
-                   << expected << ", ensureChildren = " << ensureChildren
-                   << ", overwrite policy = " << opolicy << std::endl;
-  Trace("cdproof-debug") << "CDProof::addStep: " << identify()
-                         << " : children: " << children << "\n";
-  Trace("cdproof-debug") << "CDProof::addStep: " << identify()
-                         << " : args: " << args << "\n";
-  // We must always provide expected to this method
-  Assert(!expected.isNull());
-
-  std::shared_ptr<ProofNode> pprev = getProofSymm(expected);
-  if (pprev != nullptr)
-  {
-    if (!shouldOverwrite(pprev.get(), id, opolicy))
-    {
-      // we should not overwrite the current step
-      Trace("cdproof") << "...success, no overwrite" << std::endl;
-      return true;
-    }
-    Trace("cdproof") << "existing proof " << pprev->getRule()
-                     << ", overwrite..." << std::endl;
-    // we will overwrite the existing proof node by updating its contents below
-  }
-  // collect the child proofs, for each premise
-  std::vector<std::shared_ptr<ProofNode>> pchildren;
-  for (const Node& c : children)
-  {
-    Trace("cdproof") << "- get child " << c << std::endl;
-    std::shared_ptr<ProofNode> pc = getProofSymm(c);
-    if (pc == nullptr)
-    {
-      if (ensureChildren)
-      {
-        // failed to get a proof for a child, fail
-        Trace("cdproof") << "...fail, no child" << std::endl;
-        return false;
-      }
-      Trace("cdproof") << "--- add assume" << std::endl;
-      // otherwise, we initialize it as an assumption
-      std::vector<Node> pcargs = {c};
-      std::vector<std::shared_ptr<ProofNode>> pcassume;
-      pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c);
-      // assumptions never fail to check
-      Assert(pc != nullptr);
-      d_nodes.insert(c, pc);
-    }
-    pchildren.push_back(pc);
-  }
-
-  // the user may have provided SYMM of an assumption
-  if (id == PfRule::SYMM)
-  {
-    Assert(pchildren.size() == 1);
-    if (isAssumption(pchildren[0].get()))
-    {
-      // the step we are constructing is a (symmetric fact of an) assumption, so
-      // there is no use adding it to the proof.
-      return true;
-    }
-  }
-
-  bool ret = true;
-  // create or update it
-  std::shared_ptr<ProofNode> pthis;
-  if (pprev == nullptr)
-  {
-    Trace("cdproof") << "  new node " << expected << "..." << std::endl;
-    pthis = d_manager->mkNode(id, pchildren, args, expected);
-    if (pthis == nullptr)
-    {
-      // failed to construct the node, perhaps due to a proof checking failure
-      Trace("cdproof") << "...fail, proof checking" << std::endl;
-      return false;
-    }
-    d_nodes.insert(expected, pthis);
-  }
-  else
-  {
-    Trace("cdproof") << "  update node " << expected << "..." << std::endl;
-    // update its value
-    pthis = pprev;
-    // We return the value of updateNode here. This means this method may return
-    // false if this call failed, regardless of whether we already have a proof
-    // step for expected.
-    ret = d_manager->updateNode(pthis.get(), id, pchildren, args);
-  }
-  if (ret)
-  {
-    // the result of the proof node should be expected
-    Assert(pthis->getResult() == expected);
-
-    // notify new proof
-    notifyNewProof(expected);
-  }
-
-  Trace("cdproof") << "...return " << ret << std::endl;
-  return ret;
-}
-
-void CDProof::notifyNewProof(Node expected)
-{
-  if (!d_autoSymm)
-  {
-    return;
-  }
-  // ensure SYMM proof is also linked to an existing proof, if it is an
-  // assumption.
-  Node symExpected = getSymmFact(expected);
-  if (!symExpected.isNull())
-  {
-    Trace("cdproof") << "  check connect symmetry " << symExpected << std::endl;
-    // if it exists, we may need to update it
-    std::shared_ptr<ProofNode> pfs = getProof(symExpected);
-    if (pfs != nullptr)
-    {
-      Trace("cdproof") << "  connect via getProofSymm method..." << std::endl;
-      // call the get function with symmetry, which will do the update
-      std::shared_ptr<ProofNode> pfss = getProofSymm(symExpected);
-    }
-    else
-    {
-      Trace("cdproof") << "  no connect" << std::endl;
-    }
-  }
-}
-
-bool CDProof::addStep(Node expected,
-                      const ProofStep& step,
-                      bool ensureChildren,
-                      CDPOverwrite opolicy)
-{
-  return addStep(expected,
-                 step.d_rule,
-                 step.d_children,
-                 step.d_args,
-                 ensureChildren,
-                 opolicy);
-}
-
-bool CDProof::addSteps(const ProofStepBuffer& psb,
-                       bool ensureChildren,
-                       CDPOverwrite opolicy)
-{
-  const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
-  for (const std::pair<Node, ProofStep>& ps : steps)
-  {
-    if (!addStep(ps.first, ps.second, ensureChildren, opolicy))
-    {
-      return false;
-    }
-  }
-  return true;
-}
-
-bool CDProof::addProof(std::shared_ptr<ProofNode> pn,
-                       CDPOverwrite opolicy,
-                       bool doCopy)
-{
-  if (!doCopy)
-  {
-    // If we aren't doing a deep copy, we either store pn or link its top
-    // node into the existing pointer
-    Node curFact = pn->getResult();
-    std::shared_ptr<ProofNode> cur = getProofSymm(curFact);
-    if (cur == nullptr)
-    {
-      // Assert that the checker of this class agrees with (the externally
-      // provided) pn. This ensures that if pn was checked by a different
-      // checker than the one of the manager in this class, then it is double
-      // checked here, so that this class maintains the invariant that all of
-      // its nodes in d_nodes have been checked by the underlying checker.
-      Assert(d_manager->getChecker() == nullptr
-             || d_manager->getChecker()->check(pn.get(), curFact) == curFact);
-      // just store the proof for fact
-      d_nodes.insert(curFact, pn);
-    }
-    else if (shouldOverwrite(cur.get(), pn->getRule(), opolicy))
-    {
-      // We update cur to have the structure of the top node of pn. Notice that
-      // the interface to update this node will ensure that the proof apf is a
-      // proof of the assumption. If it does not, then pn was wrong.
-      if (!d_manager->updateNode(
-              cur.get(), pn->getRule(), pn->getChildren(), pn->getArguments()))
-      {
-        return false;
-      }
-    }
-    // also need to connect via SYMM if necessary
-    notifyNewProof(curFact);
-    return true;
-  }
-  std::unordered_map<ProofNode*, bool> visited;
-  std::unordered_map<ProofNode*, bool>::iterator it;
-  std::vector<ProofNode*> visit;
-  ProofNode* cur;
-  Node curFact;
-  visit.push_back(pn.get());
-  bool retValue = true;
-  do
-  {
-    cur = visit.back();
-    curFact = cur->getResult();
-    visit.pop_back();
-    it = visited.find(cur);
-    if (it == visited.end())
-    {
-      // visit the children
-      visited[cur] = false;
-      visit.push_back(cur);
-      const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
-      for (const std::shared_ptr<ProofNode>& c : cs)
-      {
-        visit.push_back(c.get());
-      }
-    }
-    else if (!it->second)
-    {
-      // we always call addStep, which may or may not overwrite the
-      // current step
-      std::vector<Node> pexp;
-      const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
-      for (const std::shared_ptr<ProofNode>& c : cs)
-      {
-        Assert(!c->getResult().isNull());
-        pexp.push_back(c->getResult());
-      }
-      // can ensure children at this point
-      bool res = addStep(
-          curFact, cur->getRule(), pexp, cur->getArguments(), true, opolicy);
-      // should always succeed
-      Assert(res);
-      retValue = retValue && res;
-      visited[cur] = true;
-    }
-  } while (!visit.empty());
-
-  return retValue;
-}
-
-bool CDProof::hasStep(Node fact)
-{
-  std::shared_ptr<ProofNode> pf = getProof(fact);
-  if (pf != nullptr && !isAssumption(pf.get()))
-  {
-    return true;
-  }
-  else if (!d_autoSymm)
-  {
-    return false;
-  }
-  Node symFact = getSymmFact(fact);
-  if (symFact.isNull())
-  {
-    return false;
-  }
-  pf = getProof(symFact);
-  if (pf != nullptr && !isAssumption(pf.get()))
-  {
-    return true;
-  }
-  return false;
-}
-
-ProofNodeManager* CDProof::getManager() const { return d_manager; }
-
-bool CDProof::shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol)
-{
-  Assert(pn != nullptr);
-  // we overwrite only if opol is CDPOverwrite::ALWAYS, or if
-  // opol is CDPOverwrite::ASSUME_ONLY and the previously
-  // provided proof pn was an assumption and the currently provided step is not
-  return opol == CDPOverwrite::ALWAYS
-         || (opol == CDPOverwrite::ASSUME_ONLY && isAssumption(pn)
-             && newId != PfRule::ASSUME);
-}
-
-bool CDProof::isAssumption(ProofNode* pn)
-{
-  PfRule rule = pn->getRule();
-  if (rule == PfRule::ASSUME)
-  {
-    return true;
-  }
-  else if (rule == PfRule::SYMM)
-  {
-    const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren();
-    Assert(pc.size() == 1);
-    return pc[0]->getRule() == PfRule::ASSUME;
-  }
-  return false;
-}
-
-bool CDProof::isSame(TNode f, TNode g)
-{
-  if (f == g)
-  {
-    return true;
-  }
-  Kind fk = f.getKind();
-  Kind gk = g.getKind();
-  if (fk == EQUAL && gk == EQUAL && f[0] == g[1] && f[1] == g[0])
-  {
-    // symmetric equality
-    return true;
-  }
-  if (fk == NOT && gk == NOT && f[0].getKind() == EQUAL
-      && g[0].getKind() == EQUAL && f[0][0] == g[0][1] && f[0][1] == g[0][0])
-  {
-    // symmetric disequality
-    return true;
-  }
-  return false;
-}
-
-Node CDProof::getSymmFact(TNode f)
-{
-  bool polarity = f.getKind() != NOT;
-  TNode fatom = polarity ? f : f[0];
-  if (fatom.getKind() != EQUAL || fatom[0] == fatom[1])
-  {
-    return Node::null();
-  }
-  Node symFact = fatom[1].eqNode(fatom[0]);
-  return polarity ? symFact : symFact.notNode();
-}
-
-std::string CDProof::identify() const { return d_name; }
-
-}  // namespace cvc5
diff --git a/src/expr/proof.h b/src/expr/proof.h
deleted file mode 100644
index 496815938..000000000
--- a/src/expr/proof.h
+++ /dev/null
@@ -1,278 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Proof utility.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_H
-#define CVC5__EXPR__PROOF_H
-
-#include <vector>
-
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-#include "expr/proof_generator.h"
-#include "expr/proof_step_buffer.h"
-
-namespace cvc5 {
-
-class ProofNode;
-class ProofNodeManager;
-
-/**
- * A (context-dependent) proof.
- *
- * This maintains a context-dependent map from formulas to ProofNode shared
- * pointers. When a step is added, it internally uses mutable ProofNode pointers
- * to link the steps in the proof together.
- *
- * It is important to note that the premises of proof steps given to this class
- * are *Node* not *ProofNode*. In other words, the user of this class does
- * not have to manage ProofNode pointers while using this class. Instead,
- * ProofNode is the final product of this class, via the getProof interface,
- * which returns a ProofNode object that has linked together the proof steps
- * added to this object.
- *
- * Its main interface is the function addStep, which registers a single
- * step in the proof. Its interface is:
- *   addStep( <conclusion>, <rule>, <premises>, <args>, ...<options>... )
- * where conclusion is what to be proven, rule is an identifier, premises
- * are the formulas that imply conclusion, and args are additional arguments to
- * the proof rule application. The options include whether we ensure children
- * proofs already exist for the premises and our policty for overwriting
- * existing steps.
- *
- * As an example, let A, B, C, D be formulas represented by Nodes. If we
- * call:
- * - addStep( A, ID_A, { B, C }, {} )
- * - addStep( B, ID_B, { D }, {} )
- * - addStep( E, ID_E, {}, {} )
- * with default options, then getProof( A ) returns the ProofNode of the form:
- *   ID_A( ID_B( ASSUME( D ) ), ASSUME( C ) )
- * Notice that the above calls to addStep can be made in either order. The
- * proof step for E was not involved in the proof of A.
- *
- * If the user wants to combine proofs, then a addProof interface is
- * available. The method addProof can be seen as syntax sugar for making
- * multiple calls to addStep. Continuing the above example, if we call:
- * - addProof( F, ID_F( ASSUME( A ), ASSUME( E ) ) )
- * is the same as calling steps corresponding the steps in the provided proof
- * bottom-up, starting from the leaves.
- * --- addStep( A, ASSUME, {}, {}, true )
- * --- addStep( E, ASSUME, {}, {}, true )
- * --- addStep( F, ID_F, { A, E }, {}, true )
- * The fifth argument provided indicates that we want to ensure child proofs
- * are already available for the step (see ensureChildren in addStep below).
- * This will result in getProof( F ) returning:
- *   ID_F( ID_A( ID_B( ASSUME( D ) ), ASSUME( C ) ), ID_E() )
- * Notice that the proof of A by ID_A was not overwritten by ASSUME in the
- * addStep call above.
- *
- * The default policy for overwriting proof steps (CDPOverwrite::ASSUME_ONLY)
- * gives ASSUME a special status. An ASSUME step can be seen as a step whose
- * justification has not yet been provided. Thus, it is always overwritten.
- * Other proof rules are never overwritten, unless the argument opolicy is
- * CDPOverwrite::ALWAYS.
- *
- * As an another example, say that we call:
- * - addStep( B, ID_B1 {}, {} )
- * - addStep( A, ID_A1, {B, C}, {} )
- * At this point, getProof( A ) returns:
- *   ID_A1( ID_B1(), ASSUME(C) )
- * Now, assume an additional call is made to addProof, where notice
- * the overwrite policy is CDPOverwrite::ASSUME_ONLY by default:
- * - addProof( D, ID_D( ID_A2( ID_B2(), ID_C() ) ) )
- * where assume ID_B2() and ID_C() prove B and C respectively. This call is
- * equivalent to calling:
- * --- addStep( B, ID_B2, {}, {}, true )
- * --- addStep( C, ID_C, {}, {}, true )
- * --- addStep( A, ID_A2, {B, C}, {}, true )
- * --- addStep( D, ID_D, {A}, {}, true )
- * Afterwards, getProof( D ) returns:
- *   ID_D( ID_A1( ID_B1(), ID_C() ) )
- * Notice that the steps with ID_A1 and ID_B1 were not overwritten by this call,
- * whereas the assumption of C was overwritten by the proof ID_C(). Notice that
- * the proof of D was completely traversed in addProof, despite encountering
- * formulas, A and B, that were already given proof steps.
- *
- * This class requires a ProofNodeManager object, which is a trusted way of
- * allocating ProofNode pointers. This manager may have an underlying checker,
- * although this is not required. It also (optionally) takes a context c.
- * If no context is provided, then this proof is context-independent. This
- * is implemented internally by using a dummy context that is never pushed
- * or popped. The map from Nodes to ProofNodes is context-dependent and is
- * backtracked when its context backtracks.
- *
- * An important invariant of this object is that there exists (at most) one
- * proof step for each Node. Thus, the ProofNode objects returned by this
- * class share proofs for common subformulas, as guaranteed by the fact that
- * Node objects have perfect sharing.
- *
- * Notice that this class is agnostic to symmetry of equality. In other
- * words, adding a step that concludes (= x y) is effectively the same as
- * providing a step that concludes (= y x) from the point of view of a user
- * of this class. This is accomplished by adding SYMM steps on demand when
- * a formula is looked up. For example say we call:
- * - addStep( (= x y), ID_1 {}, {} )
- * - addStep( P, ID_2, {(= y x)}, {} )
- * Afterwards, getProof( P ) returns:
- *   ID_2( SYMM( ID_1() ) )
- * where notice SYMM was added so that (= y x) is a premise of the application
- * of ID_2. More generally, CDProof::isSame(F,G) returns true if F and G are
- * essentially the same formula according to this class.
- */
-class CDProof : public ProofGenerator
-{
- public:
-  /**
-   * @param pnm The proof node manager responsible for constructor ProofNode
-   * @param c The context this proof depends on
-   * @param name The name of this proof (for debugging)
-   * @param autoSymm Whether this proof automatically adds symmetry steps based
-   * on policy documented above.
-   */
-  CDProof(ProofNodeManager* pnm,
-          context::Context* c = nullptr,
-          std::string name = "CDProof",
-          bool autoSymm = true);
-  virtual ~CDProof();
-  /**
-   * Make proof for fact.
-   *
-   * This method always returns a non-null ProofNode. It may generate new
-   * steps so that a ProofNode can be constructed for fact. In particular,
-   * if no step exists for fact, then we may construct and return ASSUME(fact).
-   * If fact is of the form (= t s), no step exists for fact, but a proof
-   * P for (= s t) exists, then this method returns SYMM(P).
-   *
-   * Notice that this call does *not* clone the ProofNode object. Hence, the
-   * returned proof may be updated by further calls to this class. The caller
-   * should call ProofNode::clone if they want to own it.
-   */
-  std::shared_ptr<ProofNode> getProofFor(Node fact) override;
-  /** Add step
-   *
-   * @param expected The intended conclusion of this proof step. This must be
-   * non-null.
-   * @param id The identifier for the proof step.
-   * @param children The antecendants of the proof step. Each children[i] should
-   * be a fact previously added as a conclusion of an addStep call when
-   * ensureChildren is true.
-   * @param args The arguments of the proof step.
-   * @param ensureChildren Whether we wish to ensure steps have been added
-   * for all nodes in children
-   * @param opolicy Policy for whether to overwrite if a step for
-   * expected was already provided (via a previous call to addStep)
-   * @return The true if indeed the proof step proves expected, or
-   * false otherwise. The latter can happen if the proof has a different (or
-   * invalid) conclusion, or if one of the children does not have a proof and
-   * ensureChildren is true.
-   *
-   * This method may create proofs justified by ASSUME of the facts in
-   * children that have not already been proven when ensureChildren is false.
-   * Notice that ensureChildren should be true if the proof is being
-   * constructed is a strictly eager fashion (bottom up from its leaves), while
-   * ensureChildren should be false if the steps are added lazily or out
-   * of order.
-   *
-   * This method only overwrites proofs for facts that were added as
-   * steps with id ASSUME when opolicy is CDPOverwrite::ASSUME_ONLY, and always
-   * (resp. never) overwrites an existing step if one was provided when opolicy
-   * is CDPOverwrite::ALWAYS (resp. CDPOverwrite::NEVER).
-   */
-  bool addStep(Node expected,
-               PfRule id,
-               const std::vector<Node>& children,
-               const std::vector<Node>& args,
-               bool ensureChildren = false,
-               CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY);
-  /** Version with ProofStep */
-  bool addStep(Node expected,
-               const ProofStep& step,
-               bool ensureChildren = false,
-               CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY);
-  /** Version with ProofStepBuffer */
-  bool addSteps(const ProofStepBuffer& psb,
-                bool ensureChildren = false,
-                CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY);
-  /** Add proof
-   *
-   * @param pn The proof of the given fact.
-   * @param opolicy Policy for whether to force overwriting if a step
-   * was already provided. This is used for each node in the proof if doCopy
-   * is true.
-   * @param doCopy Whether we make a deep copy of the pn.
-   * @return true if all steps were successfully added to this class. If it
-   * returns true, it registers a copy of all of the subnodes of pn to this
-   * proof class.
-   *
-   * If doCopy is true, this method is implemented by calling addStep above for
-   * all subnodes of pn, traversed as a dag. This means that fresh ProofNode
-   * objects may be generated by this call, and further modifications to pn do
-   * not impact the internal data of this class.
-   */
-  bool addProof(std::shared_ptr<ProofNode> pn,
-                CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY,
-                bool doCopy = false);
-  /** Return true if fact already has a proof step */
-  bool hasStep(Node fact);
-  /** Get the proof manager for this proof */
-  ProofNodeManager* getManager() const;
-  /**
-   * Is same? Returns true if f and g are the same formula, or if they are
-   * symmetric equalities. If two nodes f and g are the same, then a proof for
-   * f suffices as a proof for g according to this class.
-   */
-  static bool isSame(TNode f, TNode g);
-  /** Get proof for fact, or nullptr if it does not exist. */
-  std::shared_ptr<ProofNode> getProof(Node fact) const;
-  /**
-   * Get symmetric fact (a g such that isSame returns true for isSame(f,g)), or
-   * null if none exist.
-   */
-  static Node getSymmFact(TNode f);
-  /** identify */
-  std::string identify() const override;
-
- protected:
-  typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap;
-  /** The proof manager, used for allocating new ProofNode objects */
-  ProofNodeManager* d_manager;
-  /** A dummy context used by this class if none is provided */
-  context::Context d_context;
-  /** The nodes of the proof */
-  NodeProofNodeMap d_nodes;
-  /** Name identifier */
-  std::string d_name;
-  /** Whether we automatically add symmetry steps */
-  bool d_autoSymm;
-  /** Ensure fact sym */
-  std::shared_ptr<ProofNode> getProofSymm(Node fact);
-  /**
-   * Returns true if we should overwrite proof node pn with a step having id
-   * newId, based on policy opol.
-   */
-  static bool shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol);
-  /** Returns true if pn is an assumption. */
-  static bool isAssumption(ProofNode* pn);
-  /**
-   * Notify new proof, called when a new proof of expected is provided. This is
-   * used internally to connect proofs of symmetric facts, when necessary.
-   */
-  void notifyNewProof(Node expected);
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__PROOF_MANAGER_H */
diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
deleted file mode 100644
index 69f880ed5..000000000
--- a/src/expr/proof_checker.cpp
+++ /dev/null
@@ -1,345 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of proof checker.
- */
-
-#include "expr/proof_checker.h"
-
-#include "expr/proof_node.h"
-#include "expr/skolem_manager.h"
-#include "options/proof_options.h"
-#include "smt/smt_statistics_registry.h"
-
-using namespace cvc5::kind;
-
-namespace cvc5 {
-
-Node ProofRuleChecker::check(PfRule id,
-                             const std::vector<Node>& children,
-                             const std::vector<Node>& args)
-{
-  // call instance-specific checkInternal method
-  return checkInternal(id, children, args);
-}
-
-bool ProofRuleChecker::getUInt32(TNode n, uint32_t& i)
-{
-  // must be a non-negative integer constant that fits an unsigned int
-  if (n.isConst() && n.getType().isInteger()
-      && n.getConst<Rational>().sgn() >= 0
-      && n.getConst<Rational>().getNumerator().fitsUnsignedInt())
-  {
-    i = n.getConst<Rational>().getNumerator().toUnsignedInt();
-    return true;
-  }
-  return false;
-}
-
-bool ProofRuleChecker::getBool(TNode n, bool& b)
-{
-  if (n.isConst() && n.getType().isBoolean())
-  {
-    b = n.getConst<bool>();
-    return true;
-  }
-  return false;
-}
-
-bool ProofRuleChecker::getKind(TNode n, Kind& k)
-{
-  uint32_t i;
-  if (!getUInt32(n, i))
-  {
-    return false;
-  }
-  k = static_cast<Kind>(i);
-  return true;
-}
-
-Node ProofRuleChecker::mkKindNode(Kind k)
-{
-  if (k == UNDEFINED_KIND)
-  {
-    // UNDEFINED_KIND is negative, hence return null to avoid cast
-    return Node::null();
-  }
-  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(k)));
-}
-
-ProofCheckerStatistics::ProofCheckerStatistics()
-    : d_ruleChecks(smtStatisticsRegistry().registerHistogram<PfRule>(
-        "ProofCheckerStatistics::ruleChecks")),
-      d_totalRuleChecks(smtStatisticsRegistry().registerInt(
-          "ProofCheckerStatistics::totalRuleChecks"))
-{
-}
-
-Node ProofChecker::check(ProofNode* pn, Node expected)
-{
-  return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected);
-}
-
-Node ProofChecker::check(
-    PfRule id,
-    const std::vector<std::shared_ptr<ProofNode>>& children,
-    const std::vector<Node>& args,
-    Node expected)
-{
-  // optimization: immediately return for ASSUME
-  if (id == PfRule::ASSUME)
-  {
-    Assert(children.empty());
-    Assert(args.size() == 1 && args[0].getType().isBoolean());
-    Assert(expected.isNull() || expected == args[0]);
-    return expected;
-  }
-  // record stat
-  d_stats.d_ruleChecks << id;
-  ++d_stats.d_totalRuleChecks;
-  Trace("pfcheck") << "ProofChecker::check: " << id << std::endl;
-  std::vector<Node> cchildren;
-  for (const std::shared_ptr<ProofNode>& pc : children)
-  {
-    Assert(pc != nullptr);
-    Node cres = pc->getResult();
-    if (cres.isNull())
-    {
-      Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl;
-      Unreachable()
-          << "ProofChecker::check: child proof was invalid (null conclusion)"
-          << std::endl;
-      // should not have been able to create such a proof node
-      return Node::null();
-    }
-    cchildren.push_back(cres);
-    if (Trace.isOn("pfcheck"))
-    {
-      std::stringstream ssc;
-      pc->printDebug(ssc);
-      Trace("pfcheck") << "     child: " << ssc.str() << " : " << cres
-                       << std::endl;
-    }
-  }
-  Trace("pfcheck") << "      args: " << args << std::endl;
-  Trace("pfcheck") << "  expected: " << expected << std::endl;
-  std::stringstream out;
-  // we use trusted (null) checkers here, since we want the proof generation to
-  // proceed without failing here. We always enable output since a failure
-  // implies that we will exit with the error message below.
-  Node res = checkInternal(id, cchildren, args, expected, out, true, true);
-  if (res.isNull())
-  {
-    Trace("pfcheck") << "ProofChecker::check: failed" << std::endl;
-    Unreachable() << "ProofChecker::check: failed, " << out.str() << std::endl;
-    // it did not match the given expectation, fail
-    return Node::null();
-  }
-  Trace("pfcheck") << "ProofChecker::check: success!" << std::endl;
-  return res;
-}
-
-Node ProofChecker::checkDebug(PfRule id,
-                              const std::vector<Node>& cchildren,
-                              const std::vector<Node>& args,
-                              Node expected,
-                              const char* traceTag)
-{
-  std::stringstream out;
-  bool traceEnabled = Trace.isOn(traceTag);
-  // Since we are debugging, we want to treat trusted (null) checkers as
-  // a failure. We only enable output if the trace is enabled for efficiency.
-  Node res =
-      checkInternal(id, cchildren, args, expected, out, false, traceEnabled);
-  if (traceEnabled)
-  {
-    Trace(traceTag) << "ProofChecker::checkDebug: " << id;
-    if (res.isNull())
-    {
-      Trace(traceTag) << " failed, " << out.str() << std::endl;
-    }
-    else
-    {
-      Trace(traceTag) << " success" << std::endl;
-    }
-    Trace(traceTag) << "cchildren: " << cchildren << std::endl;
-    Trace(traceTag) << "     args: " << args << std::endl;
-  }
-  return res;
-}
-
-Node ProofChecker::checkInternal(PfRule id,
-                                 const std::vector<Node>& cchildren,
-                                 const std::vector<Node>& args,
-                                 Node expected,
-                                 std::stringstream& out,
-                                 bool useTrustedChecker,
-                                 bool enableOutput)
-{
-  std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
-  if (it == d_checker.end())
-  {
-    // no checker for the rule
-    if (enableOutput)
-    {
-      out << "no checker for rule " << id << std::endl;
-    }
-    return Node::null();
-  }
-  else if (it->second == nullptr)
-  {
-    if (useTrustedChecker)
-    {
-      Notice() << "ProofChecker::check: trusting PfRule " << id << std::endl;
-      // trusted checker
-      return expected;
-    }
-    else
-    {
-      if (enableOutput)
-      {
-        out << "trusted checker for rule " << id << std::endl;
-      }
-      return Node::null();
-    }
-  }
-  // check it with the corresponding checker
-  Node res = it->second->check(id, cchildren, args);
-  if (!expected.isNull())
-  {
-    Node expectedw = expected;
-    if (res != expectedw)
-    {
-      if (enableOutput)
-      {
-        out << "result does not match expected value." << std::endl
-            << "    PfRule: " << id << std::endl;
-        for (const Node& c : cchildren)
-        {
-          out << "     child: " << c << std::endl;
-        }
-        for (const Node& a : args)
-        {
-          out << "       arg: " << a << std::endl;
-        }
-        out << "    result: " << res << std::endl
-            << "  expected: " << expected << std::endl;
-      }
-      // it did not match the given expectation, fail
-      return Node::null();
-    }
-  }
-  // fails if pedantic level is not met
-  if (options::proofEagerChecking())
-  {
-    std::stringstream serr;
-    if (isPedanticFailure(id, serr, enableOutput))
-    {
-      if (enableOutput)
-      {
-        out << serr.str() << std::endl;
-        if (Trace.isOn("proof-pedantic"))
-        {
-          Trace("proof-pedantic")
-              << "Failed pedantic check for " << id << std::endl;
-          Trace("proof-pedantic") << "Expected: " << expected << std::endl;
-          out << "Expected: " << expected << std::endl;
-        }
-      }
-      return Node::null();
-    }
-  }
-  return res;
-}
-
-void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc)
-{
-  std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
-  if (it != d_checker.end())
-  {
-    // checker is already provided
-    Notice() << "ProofChecker::registerChecker: checker already exists for "
-             << id << std::endl;
-    return;
-  }
-  d_checker[id] = psc;
-}
-
-void ProofChecker::registerTrustedChecker(PfRule id,
-                                          ProofRuleChecker* psc,
-                                          uint32_t plevel)
-{
-  AlwaysAssert(plevel <= 10) << "ProofChecker::registerTrustedChecker: "
-                                "pedantic level must be 0-10, got "
-                             << plevel << " for " << id;
-  registerChecker(id, psc);
-  // overwrites if already there
-  if (d_plevel.find(id) != d_plevel.end())
-  {
-    Notice() << "ProofChecker::registerTrustedRule: already provided pedantic "
-                "level for "
-             << id << std::endl;
-  }
-  d_plevel[id] = plevel;
-}
-
-ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id)
-{
-  std::map<PfRule, ProofRuleChecker*>::const_iterator it = d_checker.find(id);
-  if (it == d_checker.end())
-  {
-    return nullptr;
-  }
-  return it->second;
-}
-
-uint32_t ProofChecker::getPedanticLevel(PfRule id) const
-{
-  std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);
-  if (itp != d_plevel.end())
-  {
-    return itp->second;
-  }
-  return 0;
-}
-
-bool ProofChecker::isPedanticFailure(PfRule id,
-                                     std::ostream& out,
-                                     bool enableOutput) const
-{
-  if (d_pclevel == 0)
-  {
-    return false;
-  }
-  std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);
-  if (itp != d_plevel.end())
-  {
-    if (itp->second <= d_pclevel)
-    {
-      if (enableOutput)
-      {
-        out << "pedantic level for " << id << " not met (rule level is "
-            << itp->second << " which is at or below the pedantic level "
-            << d_pclevel << ")";
-        bool pedanticTraceEnabled = Trace.isOn("proof-pedantic");
-        if (!pedanticTraceEnabled)
-        {
-          out << ", use -t proof-pedantic for details";
-        }
-      }
-      return true;
-    }
-  }
-  return false;
-}
-
-}  // namespace cvc5
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
deleted file mode 100644
index e778f687e..000000000
--- a/src/expr/proof_checker.h
+++ /dev/null
@@ -1,206 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Proof checker utility.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_CHECKER_H
-#define CVC5__EXPR__PROOF_CHECKER_H
-
-#include <map>
-
-#include "expr/node.h"
-#include "expr/proof_rule.h"
-#include "util/statistics_stats.h"
-
-namespace cvc5 {
-
-class ProofChecker;
-class ProofNode;
-
-/** A virtual base class for checking a proof rule */
-class ProofRuleChecker
-{
- public:
-  ProofRuleChecker() {}
-  virtual ~ProofRuleChecker() {}
-  /**
-   * This checks a single step in a proof.
-   *
-   * Return the formula that is proven by a proof node with the given id,
-   * premises and arguments, or null if such a proof node is not well-formed.
-   *
-   * Note that the input/output of this method expects to be terms in *Skolem
-   * form*, which is passed to checkInternal below. Rule checkers may
-   * convert premises to witness form when necessary.
-   *
-   * @param id The id of the proof node to check
-   * @param children The premises of the proof node to check. These are nodes
-   * corresponding to the conclusion (ProofNode::getResult) of the children
-   * of the proof node we are checking in Skolem form.
-   * @param args The arguments of the proof node to check
-   * @return The conclusion of the proof node, in Skolem form, if successful or
-   * null if such a proof node is malformed.
-   */
-  Node check(PfRule id,
-             const std::vector<Node>& children,
-             const std::vector<Node>& args);
-
-  /** get an index from a node, return false if we fail */
-  static bool getUInt32(TNode n, uint32_t& i);
-  /** get a Boolean from a node, return false if we fail */
-  static bool getBool(TNode n, bool& b);
-  /** get a Kind from a node, return false if we fail */
-  static bool getKind(TNode n, Kind& k);
-  /** Make a Kind into a node */
-  static Node mkKindNode(Kind k);
-
-  /** Register all rules owned by this rule checker into pc. */
-  virtual void registerTo(ProofChecker* pc) {}
-
- protected:
-  /**
-   * This checks a single step in a proof.
-   *
-   * @param id The id of the proof node to check
-   * @param children The premises of the proof node to check. These are nodes
-   * corresponding to the conclusion (ProofNode::getResult) of the children
-   * of the proof node we are checking.
-   * @param args The arguments of the proof node to check
-   * @return The conclusion of the proof node if successful or null if such a
-   * proof node is malformed.
-   */
-  virtual Node checkInternal(PfRule id,
-                             const std::vector<Node>& children,
-                             const std::vector<Node>& args) = 0;
-};
-
-/** Statistics class */
-class ProofCheckerStatistics
-{
- public:
-  ProofCheckerStatistics();
-  /** Counts the number of checks for each kind of proof rule */
-  HistogramStat<PfRule> d_ruleChecks;
-  /** Total number of rule checks */
-  IntStat d_totalRuleChecks;
-};
-
-/** A class for checking proofs */
-class ProofChecker
-{
- public:
-  ProofChecker(uint32_t pclevel = 0) : d_pclevel(pclevel) {}
-  ~ProofChecker() {}
-  /**
-   * Return the formula that is proven by proof node pn, or null if pn is not
-   * well-formed. If expected is non-null, then we return null if pn does not
-   * prove expected.
-   *
-   * @param pn The proof node to check
-   * @param expected The (optional) formula that is the expected conclusion of
-   * the proof node.
-   * @return The conclusion of the proof node if successful or null if the
-   * proof is malformed, or if no checker is available for id.
-   */
-  Node check(ProofNode* pn, Node expected = Node::null());
-  /** Same as above, with explicit arguments
-   *
-   * @param id The id of the proof node to check
-   * @param children The children of the proof node to check
-   * @param args The arguments of the proof node to check
-   * @param expected The (optional) formula that is the expected conclusion of
-   * the proof node.
-   * @return The conclusion of the proof node if successful or null if the
-   * proof is malformed, or if no checker is available for id.
-   */
-  Node check(PfRule id,
-             const std::vector<std::shared_ptr<ProofNode>>& children,
-             const std::vector<Node>& args,
-             Node expected = Node::null());
-  /**
-   * Same as above, without conclusions instead of proof node children. This
-   * is used for debugging. In particular, this function does not throw an
-   * assertion failure when a proof step is malformed and can be used without
-   * constructing proof nodes.
-   *
-   * @param id The id of the proof node to check
-   * @param children The conclusions of the children of the proof node to check
-   * @param args The arguments of the proof node to check
-   * @param expected The (optional) formula that is the expected conclusion of
-   * the proof node.
-   * @param traceTag The trace tag to print debug information to
-   * @return The conclusion of the proof node if successful or null if the
-   * proof is malformed, or if no checker is available for id.
-   */
-  Node checkDebug(PfRule id,
-                  const std::vector<Node>& cchildren,
-                  const std::vector<Node>& args,
-                  Node expected = Node::null(),
-                  const char* traceTag = "");
-  /** Indicate that psc is the checker for proof rule id */
-  void registerChecker(PfRule id, ProofRuleChecker* psc);
-  /**
-   * Indicate that id is a trusted rule with the given pedantic level, e.g.:
-   *  0: (mandatory) always a failure to use the given id
-   *  1: (major) failure on all (non-zero) pedantic levels
-   * 10: (minor) failure only on pedantic levels >= 10.
-   */
-  void registerTrustedChecker(PfRule id,
-                              ProofRuleChecker* psc,
-                              uint32_t plevel = 10);
-  /** get checker for */
-  ProofRuleChecker* getCheckerFor(PfRule id);
-
-  /**
-   * Get the pedantic level for id if it has been assigned a pedantic
-   * level via registerTrustedChecker above, or zero otherwise.
-   */
-  uint32_t getPedanticLevel(PfRule id) const;
-
-  /**
-   * Is pedantic failure? If so, we return true and write a debug message on the
-   * output stream out if enableOutput is true.
-   */
-  bool isPedanticFailure(PfRule id,
-                         std::ostream& out,
-                         bool enableOutput = true) const;
-
- private:
-  /** statistics class */
-  ProofCheckerStatistics d_stats;
-  /** Maps proof rules to their checker */
-  std::map<PfRule, ProofRuleChecker*> d_checker;
-  /** Maps proof trusted rules to their pedantic level */
-  std::map<PfRule, uint32_t> d_plevel;
-  /** The pedantic level of this checker */
-  uint32_t d_pclevel;
-  /**
-   * Check internal. This is used by check and checkDebug above. It writes
-   * checking errors on out when enableOutput is true. We treat trusted checkers
-   * (nullptr in the range of the map d_checker) as failures if
-   * useTrustedChecker = false.
-   */
-  Node checkInternal(PfRule id,
-                     const std::vector<Node>& cchildren,
-                     const std::vector<Node>& args,
-                     Node expected,
-                     std::stringstream& out,
-                     bool useTrustedChecker,
-                     bool enableOutput);
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__PROOF_CHECKER_H */
diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp
deleted file mode 100644
index e89bd6692..000000000
--- a/src/expr/proof_ensure_closed.cpp
+++ /dev/null
@@ -1,183 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of debug checks for ensuring proofs are closed.
- */
-
-#include "expr/proof_ensure_closed.h"
-
-#include <sstream>
-
-#include "expr/proof_generator.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_algorithm.h"
-#include "options/proof_options.h"
-#include "options/smt_options.h"
-
-namespace cvc5 {
-
-/**
- * Ensure closed with respect to assumptions, internal version, which
- * generalizes the check for a proof generator or a proof node.
- */
-void ensureClosedWrtInternal(Node proven,
-                             ProofGenerator* pg,
-                             ProofNode* pnp,
-                             const std::vector<Node>& assumps,
-                             const char* c,
-                             const char* ctx,
-                             bool reqGen)
-{
-  if (!options::produceProofs())
-  {
-    // proofs not enabled, do not do check
-    return;
-  }
-  bool isTraceDebug = Trace.isOn(c);
-  if (!options::proofEagerChecking() && !isTraceDebug)
-  {
-    // trace is off and proof new eager checking is off, do not do check
-    return;
-  }
-  std::stringstream sdiag;
-  bool isTraceOn = Trace.isOn(c);
-  if (!isTraceOn)
-  {
-    sdiag << ", use -t " << c << " for details";
-  }
-  bool dumpProofTraceOn = Trace.isOn("dump-proof-error");
-  if (!dumpProofTraceOn)
-  {
-    sdiag << ", use -t dump-proof-error for details on proof";
-  }
-  // get the proof node in question, which is either provided or built by the
-  // proof generator
-  std::shared_ptr<ProofNode> pn;
-  std::stringstream ss;
-  if (pnp != nullptr)
-  {
-    Assert(pg == nullptr);
-    ss << "ProofNode in context " << ctx;
-  }
-  else
-  {
-    ss << "ProofGenerator: " << (pg == nullptr ? "null" : pg->identify())
-       << " in context " << ctx;
-    if (pg == nullptr)
-    {
-      // only failure if flag is true
-      if (reqGen)
-      {
-        Unreachable() << "...ensureClosed: no generator in context " << ctx
-                      << sdiag.str();
-      }
-    }
-    else
-    {
-      Assert(!proven.isNull());
-      pn = pg->getProofFor(proven);
-      pnp = pn.get();
-    }
-  }
-  Trace(c) << "=== ensureClosed: " << ss.str() << std::endl;
-  Trace(c) << "Proven: " << proven << std::endl;
-  if (pnp == nullptr)
-  {
-    if (pg == nullptr)
-    {
-      // did not require generator
-      Assert(!reqGen);
-      Trace(c) << "...ensureClosed: no generator in context " << ctx
-               << std::endl;
-      return;
-    }
-  }
-  // if we don't have a proof node, a generator failed
-  if (pnp == nullptr)
-  {
-    Assert(pg != nullptr);
-    AlwaysAssert(false) << "...ensureClosed: null proof from " << ss.str()
-                        << sdiag.str();
-  }
-  std::vector<Node> fassumps;
-  expr::getFreeAssumptions(pnp, fassumps);
-  bool isClosed = true;
-  std::stringstream ssf;
-  for (const Node& fa : fassumps)
-  {
-    if (std::find(assumps.begin(), assumps.end(), fa) == assumps.end())
-    {
-      isClosed = false;
-      ssf << "- " << fa << std::endl;
-    }
-  }
-  if (!isClosed)
-  {
-    Trace(c) << "Free assumptions:" << std::endl;
-    Trace(c) << ssf.str();
-    if (!assumps.empty())
-    {
-      Trace(c) << "Expected assumptions:" << std::endl;
-      for (const Node& a : assumps)
-      {
-        Trace(c) << "- " << a << std::endl;
-      }
-    }
-    if (dumpProofTraceOn)
-    {
-      Trace("dump-proof-error") << " Proof: " << *pnp << std::endl;
-    }
-  }
-  AlwaysAssert(isClosed) << "...ensureClosed: open proof from " << ss.str()
-                         << sdiag.str();
-  Trace(c) << "...ensureClosed: success" << std::endl;
-  Trace(c) << "====" << std::endl;
-}
-
-void pfgEnsureClosed(Node proven,
-                     ProofGenerator* pg,
-                     const char* c,
-                     const char* ctx,
-                     bool reqGen)
-{
-  Assert(!proven.isNull());
-  // proof generator may be null
-  std::vector<Node> assumps;
-  ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen);
-}
-
-void pfgEnsureClosedWrt(Node proven,
-                        ProofGenerator* pg,
-                        const std::vector<Node>& assumps,
-                        const char* c,
-                        const char* ctx,
-                        bool reqGen)
-{
-  Assert(!proven.isNull());
-  // proof generator may be null
-  ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen);
-}
-
-void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx)
-{
-  ensureClosedWrtInternal(Node::null(), nullptr, pn, {}, c, ctx, false);
-}
-
-void pfnEnsureClosedWrt(ProofNode* pn,
-                        const std::vector<Node>& assumps,
-                        const char* c,
-                        const char* ctx)
-{
-  ensureClosedWrtInternal(Node::null(), nullptr, pn, assumps, c, ctx, false);
-}
-
-}  // namespace cvc5
diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h
deleted file mode 100644
index 3d126a4a1..000000000
--- a/src/expr/proof_ensure_closed.h
+++ /dev/null
@@ -1,73 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Debug checks for ensuring proofs are closed.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_ENSURE_CLOSED_H
-#define CVC5__EXPR__PROOF_ENSURE_CLOSED_H
-
-#include "expr/node.h"
-
-namespace cvc5 {
-
-class ProofGenerator;
-class ProofNode;
-
-/**
- * Debug check closed on Trace c. Context ctx is string for debugging.
- * This method throws an assertion failure if pg cannot provide a closed
- * proof for fact proven. This is checked only if --proof-eager-checking
- * is enabled or the Trace c is enabled.
- *
- * @param reqGen Whether we consider a null generator to be a failure.
- */
-void pfgEnsureClosed(Node proven,
-                     ProofGenerator* pg,
-                     const char* c,
-                     const char* ctx,
-                     bool reqGen = true);
-
-/**
- * Debug check closed with Trace c. Context ctx is string for debugging and
- * assumps is the set of allowed open assertions. This method throws an
- * assertion failure if pg cannot provide a proof for fact proven whose
- * free assumptions are contained in assumps.
- *
- * @param reqGen Whether we consider a null generator to be a failure.
- */
-void pfgEnsureClosedWrt(Node proven,
-                        ProofGenerator* pg,
-                        const std::vector<Node>& assumps,
-                        const char* c,
-                        const char* ctx,
-                        bool reqGen = true);
-
-/**
- * Debug check closed with Trace c, proof node versions. This gives an
- * assertion failure if pn is not closed. Detailed information is printed
- * on trace c. Context ctx is a string used for debugging.
- */
-void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx);
-/**
- * Same as above, but throws an assertion failure only if the free assumptions
- * of pn are not contained in assumps.
- */
-void pfnEnsureClosedWrt(ProofNode* pn,
-                        const std::vector<Node>& assumps,
-                        const char* c,
-                        const char* ctx);
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__PROOF_ENSURE_CLOSED_H */
diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
deleted file mode 100644
index 7c034c10d..000000000
--- a/src/expr/proof_generator.cpp
+++ /dev/null
@@ -1,77 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of proof generator utility.
- */
-
-#include "expr/proof_generator.h"
-
-#include <sstream>
-
-#include "expr/proof.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_algorithm.h"
-#include "options/smt_options.h"
-
-namespace cvc5 {
-
-std::ostream& operator<<(std::ostream& out, CDPOverwrite opol)
-{
-  switch (opol)
-  {
-    case CDPOverwrite::ALWAYS: out << "ALWAYS"; break;
-    case CDPOverwrite::ASSUME_ONLY: out << "ASSUME_ONLY"; break;
-    case CDPOverwrite::NEVER: out << "NEVER"; break;
-    default: out << "CDPOverwrite:unknown"; break;
-  }
-  return out;
-}
-
-ProofGenerator::ProofGenerator() {}
-
-ProofGenerator::~ProofGenerator() {}
-
-std::shared_ptr<ProofNode> ProofGenerator::getProofFor(Node f)
-{
-  Unreachable() << "ProofGenerator::getProofFor: " << identify()
-                << " has no implementation" << std::endl;
-  return nullptr;
-}
-
-bool ProofGenerator::addProofTo(Node f,
-                                CDProof* pf,
-                                CDPOverwrite opolicy,
-                                bool doCopy)
-{
-  Trace("pfgen") << "ProofGenerator::addProofTo: " << f << "..." << std::endl;
-  Assert(pf != nullptr);
-  // plug in the proof provided by the generator, if it exists
-  std::shared_ptr<ProofNode> apf = getProofFor(f);
-  if (apf != nullptr)
-  {
-    Trace("pfgen") << "...got proof " << *apf.get() << std::endl;
-    if (pf->addProof(apf, opolicy, doCopy))
-    {
-      Trace("pfgen") << "...success!" << std::endl;
-      return true;
-    }
-    Trace("pfgen") << "...failed to add proof" << std::endl;
-  }
-  else
-  {
-    Trace("pfgen") << "...failed, no proof" << std::endl;
-    Assert(false) << "Failed to get proof from generator for fact " << f;
-  }
-  return false;
-}
-
-}  // namespace cvc5
diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
deleted file mode 100644
index 2e87ab756..000000000
--- a/src/expr/proof_generator.h
+++ /dev/null
@@ -1,113 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * The abstract proof generator class.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_GENERATOR_H
-#define CVC5__EXPR__PROOF_GENERATOR_H
-
-#include "expr/node.h"
-
-namespace cvc5 {
-
-class CDProof;
-class ProofNode;
-
-/** An overwrite policy for CDProof */
-enum class CDPOverwrite : uint32_t
-{
-  // always overwrite an existing step.
-  ALWAYS,
-  // overwrite ASSUME with non-ASSUME steps.
-  ASSUME_ONLY,
-  // never overwrite an existing step.
-  NEVER,
-};
-/** Writes a overwrite policy name to a stream. */
-std::ostream& operator<<(std::ostream& out, CDPOverwrite opol);
-
-/**
- * An abstract proof generator class.
- *
- * A proof generator is intended to be used as a utility e.g. in theory
- * solvers for constructing and storing proofs internally. A theory may have
- * multiple instances of ProofGenerator objects, e.g. if it has more than one
- * way of justifying lemmas or conflicts.
- *
- * A proof generator has two main interfaces for generating proofs:
- * (1) getProofFor, and (2) addProofTo. The latter is optional.
- *
- * The addProofTo method can be used as an optimization for avoiding
- * the construction of the ProofNode for a given fact.
- *
- * If no implementation of addProofTo is provided, then addProofTo(f, pf)
- * calls getProofFor(f) and links the topmost ProofNode of the returned proof
- * into pf. Note this top-most ProofNode can be avoided in the addProofTo
- * method.
- */
-class ProofGenerator
-{
- public:
-  ProofGenerator();
-  virtual ~ProofGenerator();
-  /** Get the proof for formula f
-   *
-   * This forces the proof generator to construct a proof for formula f and
-   * return it. If this is an "eager" proof generator, this function is expected
-   * to be implemented as a map lookup. If this is a "lazy" proof generator,
-   * this function is expected to invoke a proof producing procedure of the
-   * generator.
-   *
-   * It should be the case that hasProofFor(f) is true.
-   *
-   * @param f The fact to get the proof for.
-   * @return The proof for f.
-   */
-  virtual std::shared_ptr<ProofNode> getProofFor(Node f);
-  /**
-   * Add the proof for formula f to proof pf. The proof of f is overwritten in
-   * pf based on the policy opolicy.
-   *
-   * @param f The fact to get the proof for.
-   * @param pf The CDProof object to add the proof to.
-   * @param opolicy The overwrite policy for adding to pf.
-   * @param doCopy Whether to do a deep copy of the proof steps into pf.
-   * @return True if this call was sucessful.
-   */
-  virtual bool addProofTo(Node f,
-                          CDProof* pf,
-                          CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY,
-                          bool doCopy = false);
-  /**
-   * Can we give the proof for formula f? This is used for debugging. This
-   * returns false if the generator cannot provide a proof of formula f.
-   *
-   * Also notice that this function does not require the proof for f to be
-   * constructed at the time of this call. Thus, if this is a "lazy" proof
-   * generator, it is expected that this call is implemented as a map lookup
-   * into the bookkeeping maintained by the generator only.
-   *
-   * Notice the default return value is true. In other words, a proof generator
-   * may choose to override this function to verify the construction, although
-   * we do not insist this is the case.
-   */
-  virtual bool hasProofFor(Node f) { return true; }
-  /** Identify this generator (for debugging, etc..) */
-  virtual std::string identify() const = 0;
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__PROOF_GENERATOR_H */
diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp
deleted file mode 100644
index 92daad8ed..000000000
--- a/src/expr/proof_node.cpp
+++ /dev/null
@@ -1,72 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of proof node utility.
- */
-
-#include "expr/proof_node.h"
-
-#include "expr/proof_node_algorithm.h"
-#include "expr/proof_node_to_sexpr.h"
-
-namespace cvc5 {
-
-ProofNode::ProofNode(PfRule id,
-                     const std::vector<std::shared_ptr<ProofNode>>& children,
-                     const std::vector<Node>& args)
-{
-  setValue(id, children, args);
-}
-
-PfRule ProofNode::getRule() const { return d_rule; }
-
-const std::vector<std::shared_ptr<ProofNode>>& ProofNode::getChildren() const
-{
-  return d_children;
-}
-
-const std::vector<Node>& ProofNode::getArguments() const { return d_args; }
-
-Node ProofNode::getResult() const { return d_proven; }
-
-bool ProofNode::isClosed()
-{
-  std::vector<Node> assumps;
-  expr::getFreeAssumptions(this, assumps);
-  return assumps.empty();
-}
-
-void ProofNode::setValue(
-    PfRule id,
-    const std::vector<std::shared_ptr<ProofNode>>& children,
-    const std::vector<Node>& args)
-{
-  d_rule = id;
-  d_children = children;
-  d_args = args;
-}
-
-void ProofNode::printDebug(std::ostream& os) const
-{
-  // convert to sexpr and print
-  ProofNodeToSExpr pnts;
-  Node ps = pnts.convertToSExpr(this);
-  os << ps;
-}
-
-std::ostream& operator<<(std::ostream& out, const ProofNode& pn)
-{
-  pn.printDebug(out);
-  return out;
-}
-
-}  // namespace cvc5
diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
deleted file mode 100644
index f8d71f703..000000000
--- a/src/expr/proof_node.h
+++ /dev/null
@@ -1,145 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa, Alex Ozdemir
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Proof node utility.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_NODE_H
-#define CVC5__EXPR__PROOF_NODE_H
-
-#include <vector>
-
-#include "expr/node.h"
-#include "expr/proof_rule.h"
-
-namespace cvc5 {
-
-class ProofNodeManager;
-class ProofNode;
-
-// Alias for shared pointer to a proof node
-using Pf = std::shared_ptr<ProofNode>;
-
-struct ProofNodeHashFunction
-{
-  inline size_t operator()(std::shared_ptr<ProofNode> pfn) const;
-}; /* struct ProofNodeHashFunction */
-
-/** A node in a proof
- *
- * A ProofNode represents a single step in a proof. It contains:
- * (1) d_id, an identifier indicating the kind of inference,
- * (2) d_children, the child ProofNode objects indicating its premises,
- * (3) d_args, additional arguments used to determine the conclusion,
- * (4) d_proven, cache of the formula that this ProofNode proves.
- *
- * Overall, a ProofNode and its children form a directed acyclic graph.
- *
- * A ProofNode is partially mutable in that (1), (2) and (3) can be
- * modified. A motivating example of when this is useful is when a ProofNode
- * is established to be a "hole" for something to be proven later. On the other
- * hand, (4) is intended to be immutable.
- *
- * The method setValue is private and can be called by objects that manage
- * ProofNode objects in trusted ways that ensure that the node maintains
- * the invariant above. Furthermore, notice that this class is not responsible
- * for setting d_proven; this is done externally by a ProofNodeManager class.
- *
- * Notice that all fields of ProofNode are stored in ***Skolem form***. Their
- * correctness is checked in ***witness form*** (for details on this
- * terminology, see expr/skolem_manager.h). As a simple example, say a
- * theory solver has a term t, and wants to introduce a unit lemma (= k t)
- * where k is a fresh Skolem variable. It creates this variable via:
- *   k = SkolemManager::mkPurifySkolem(t,"k");
- * A checked ProofNode for the fact (= k t) then may have fields:
- *   d_rule := MACRO_SR_PRED_INTRO,
- *   d_children := {},
- *   d_args := {(= k t)}
- *   d_proven := (= k t).
- * Its justification via the rule MACRO_SR_PRED_INTRO (see documentation
- * in theory/builtin/proof_kinds) is in terms of the witness form of the
- * argument:
- *   (= (witness ((z T)) (= z t)) t)
- * which, by that rule's side condition, is such that:
- *   Rewriter::rewrite((= (witness ((z T)) (= z t)) t)) = true.
- * Notice that the correctness of the rule is justified here by rewriting
- * the witness form of (= k t). The conversion to/from witness form is
- * managed by ProofRuleChecker::check.
- *
- * An external proof checker is expected to formalize the ProofNode only in
- * terms of *witness* forms.
- *
- * However, the rest of cvc5 sees only the *Skolem* form of arguments and
- * conclusions in ProofNode, since this is what is used throughout cvc5.
- */
-class ProofNode
-{
-  friend class ProofNodeManager;
-
- public:
-  ProofNode(PfRule id,
-            const std::vector<std::shared_ptr<ProofNode>>& children,
-            const std::vector<Node>& args);
-  ~ProofNode() {}
-  /** get the rule of this proof node */
-  PfRule getRule() const;
-  /** Get children */
-  const std::vector<std::shared_ptr<ProofNode>>& getChildren() const;
-  /** Get arguments */
-  const std::vector<Node>& getArguments() const;
-  /** get what this node proves, or the null node if this is an invalid proof */
-  Node getResult() const;
-  /**
-   * Returns true if this is a closed proof (i.e. it has no free assumptions).
-   */
-  bool isClosed();
-  /** Print debug on output strem os */
-  void printDebug(std::ostream& os) const;
-
- private:
-  /**
-   * Set value, called to overwrite the contents of this ProofNode with the
-   * given arguments.
-   */
-  void setValue(PfRule id,
-                const std::vector<std::shared_ptr<ProofNode>>& children,
-                const std::vector<Node>& args);
-  /** The proof rule */
-  PfRule d_rule;
-  /** The children of this proof node */
-  std::vector<std::shared_ptr<ProofNode>> d_children;
-  /** arguments of this node */
-  std::vector<Node> d_args;
-  /** The cache of the fact that has been proven, modifiable by ProofChecker */
-  Node d_proven;
-};
-
-inline size_t ProofNodeHashFunction::operator()(
-    std::shared_ptr<ProofNode> pfn) const
-{
-  return pfn->getResult().getId() + static_cast<unsigned>(pfn->getRule());
-}
-
-/**
- * Serializes a given proof node to the given stream.
- *
- * @param out the output stream to use
- * @param pn the proof node to output to the stream
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out, const ProofNode& pn);
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__PROOF_NODE_H */
diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
deleted file mode 100644
index 4bb35b5dc..000000000
--- a/src/expr/proof_node_algorithm.cpp
+++ /dev/null
@@ -1,176 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of proof node algorithm utilities.
- */
-
-#include "expr/proof_node_algorithm.h"
-
-#include "expr/proof_node.h"
-
-namespace cvc5 {
-namespace expr {
-
-void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
-{
-  std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap;
-  std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>(
-      pn->getRule(), pn->getChildren(), pn->getArguments());
-  getFreeAssumptionsMap(spn, amap);
-  for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p :
-       amap)
-  {
-    assump.push_back(p.first);
-  }
-}
-
-void getFreeAssumptionsMap(
-    std::shared_ptr<ProofNode> pn,
-    std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap)
-{
-  // proof should not be cyclic
-  // visited set false after preorder traversal, true after postorder traversal
-  std::unordered_map<ProofNode*, bool> visited;
-  std::unordered_map<ProofNode*, bool>::iterator it;
-  std::vector<std::shared_ptr<ProofNode>> visit;
-  std::vector<std::shared_ptr<ProofNode>> traversing;
-  // Maps a bound assumption to the number of bindings it is under
-  // e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at
-  // (ASSUME x), and x would be mapped to 1.
-  //
-  // This map is used to track which nodes are in scope while traversing the
-  // DAG. The in-scope assumptions are keys in the map. They're removed when
-  // their binding count drops to zero. Let's annotate the above example to
-  // serve as an illustration:
-  //
-  //   (SCOPE0 (SCOPE1 (ASSUME x) (x y)) (y))
-  //
-  // This is how the map changes during the traversal:
-  //   after  previsiting SCOPE0: { y: 1 }
-  //   after  previsiting SCOPE1: { y: 2, x: 1 }
-  //   at                 ASSUME: { y: 2, x: 1 } (so x is in scope!)
-  //   after postvisiting SCOPE1: { y: 1 }
-  //   after postvisiting SCOPE2: {}
-  //
-  std::unordered_map<Node, uint32_t> scopeDepth;
-  std::shared_ptr<ProofNode> cur;
-  visit.push_back(pn);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    it = visited.find(cur.get());
-    const std::vector<Node>& cargs = cur->getArguments();
-    if (it == visited.end())
-    {
-      PfRule id = cur->getRule();
-      if (id == PfRule::ASSUME)
-      {
-        visited[cur.get()] = true;
-        Assert(cargs.size() == 1);
-        Node f = cargs[0];
-        if (!scopeDepth.count(f))
-        {
-          amap[f].push_back(cur);
-        }
-      }
-      else
-      {
-        if (id == PfRule::SCOPE)
-        {
-          // mark that its arguments are bound in the current scope
-          for (const Node& a : cargs)
-          {
-            scopeDepth[a] += 1;
-          }
-          // will need to unbind the variables below
-        }
-        // The following loop cannot be merged with the loop above because the
-        // same subproof
-        visited[cur.get()] = false;
-        visit.push_back(cur);
-        traversing.push_back(cur);
-        const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
-        for (const std::shared_ptr<ProofNode>& cp : cs)
-        {
-          if (std::find(traversing.begin(), traversing.end(), cp)
-              != traversing.end())
-          {
-            Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use "
-                           "--proof-eager-checking)"
-                        << std::endl;
-          }
-          visit.push_back(cp);
-        }
-      }
-    }
-    else if (!it->second)
-    {
-      Assert(!traversing.empty());
-      traversing.pop_back();
-      visited[cur.get()] = true;
-      if (cur->getRule() == PfRule::SCOPE)
-      {
-        // unbind its assumptions
-        for (const Node& a : cargs)
-        {
-          auto scopeCt = scopeDepth.find(a);
-          Assert(scopeCt != scopeDepth.end());
-          scopeCt->second -= 1;
-          if (scopeCt->second == 0)
-          {
-            scopeDepth.erase(scopeCt);
-          }
-        }
-      }
-    }
-  } while (!visit.empty());
-}
-
-bool containsSubproof(ProofNode* pn, ProofNode* pnc)
-{
-  std::unordered_set<const ProofNode*> visited;
-  return containsSubproof(pn, pnc, visited);
-}
-
-bool containsSubproof(ProofNode* pn,
-                      ProofNode* pnc,
-                      std::unordered_set<const ProofNode*>& visited)
-{
-  std::unordered_map<const ProofNode*, bool>::iterator it;
-  std::vector<const ProofNode*> visit;
-  visit.push_back(pn);
-  const ProofNode* cur;
-  while (!visit.empty())
-  {
-    cur = visit.back();
-    visit.pop_back();
-    if (visited.find(cur) == visited.end())
-    {
-      visited.insert(cur);
-      if (cur == pnc)
-      {
-        return true;
-      }
-      const std::vector<std::shared_ptr<ProofNode>>& children =
-          cur->getChildren();
-      for (const std::shared_ptr<ProofNode>& cp : children)
-      {
-        visit.push_back(cp.get());
-      }
-    }
-  }
-  return false;
-}
-
-}  // namespace expr
-}  // namespace cvc5
diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h
deleted file mode 100644
index 4c89dd4bc..000000000
--- a/src/expr/proof_node_algorithm.h
+++ /dev/null
@@ -1,76 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Proof node algorithm utilities.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_NODE_ALGORITHM_H
-#define CVC5__EXPR__PROOF_NODE_ALGORITHM_H
-
-#include <vector>
-
-#include "expr/node.h"
-
-namespace cvc5 {
-
-class ProofNode;
-
-namespace expr {
-
-/**
- * This adds to the vector assump all formulas that are "free assumptions" of
- * the proof whose root is ProofNode pn. A free assumption is a formula F
- * that is an argument (in d_args) of a ProofNode whose kind is ASSUME, and
- * that proof node is not beneath an application of SCOPE containing F as an
- * argument.
- *
- * This traverses the structure of the dag represented by this ProofNode.
- * Its implementation is analogous to expr::getFreeVariables.
- *
- * @param pn The proof node.
- * @param assump The vector to add the free asumptions of pn to.
- */
-void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump);
-/**
- * Same as above, but maps assumptions to the proof pointer(s) for that
- * assumption. Notice that depending on how pn is constructed, there may be
- * multiple ProofNode that are ASSUME proofs of the same assumption, which
- * are each added to the range of the assumption.
- *
- * @param pn The proof node.
- * @param amap The mapping to add the free asumptions of pn and their
- * corresponding proof nodes to.
- */
-void getFreeAssumptionsMap(
-    std::shared_ptr<ProofNode> pn,
-    std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap);
-
-/**
- * @return true if pn contains pnc.
- */
-bool containsSubproof(ProofNode* pn, ProofNode* pnc);
-
-/**
- * Same as above, with a visited cache.
- *
- * @return true if pn contains pnc.
- */
-bool containsSubproof(ProofNode* pn,
-                      ProofNode* pnc,
-                      std::unordered_set<const ProofNode*>& visited);
-
-}  // namespace expr
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__PROOF_NODE_ALGORITHM_H */
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
deleted file mode 100644
index c2c72f35d..000000000
--- a/src/expr/proof_node_manager.cpp
+++ /dev/null
@@ -1,408 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of proof node manager.
- */
-
-#include "expr/proof_node_manager.h"
-
-#include <sstream>
-
-#include "expr/proof.h"
-#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_algorithm.h"
-#include "options/proof_options.h"
-#include "theory/rewriter.h"
-
-using namespace cvc5::kind;
-
-namespace cvc5 {
-
-ProofNodeManager::ProofNodeManager(ProofChecker* pc)
-    : d_checker(pc)
-{
-  d_true = NodeManager::currentNM()->mkConst(true);
-}
-
-std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
-    PfRule id,
-    const std::vector<std::shared_ptr<ProofNode>>& children,
-    const std::vector<Node>& args,
-    Node expected)
-{
-  Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId()
-               << "} " << expected << "\n";
-  Node res = checkInternal(id, children, args, expected);
-  if (res.isNull())
-  {
-    // if it was invalid, then we return the null node
-    return nullptr;
-  }
-  // otherwise construct the proof node and set its proven field
-  std::shared_ptr<ProofNode> pn =
-      std::make_shared<ProofNode>(id, children, args);
-  pn->d_proven = res;
-  return pn;
-}
-
-std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact)
-{
-  Assert(!fact.isNull());
-  Assert(fact.getType().isBoolean());
-  return mkNode(PfRule::ASSUME, {}, {fact}, fact);
-}
-
-std::shared_ptr<ProofNode> ProofNodeManager::mkTrans(
-    const std::vector<std::shared_ptr<ProofNode>>& children, Node expected)
-{
-  Assert(!children.empty());
-  if (children.size() == 1)
-  {
-    Assert(expected.isNull() || children[0]->getResult() == expected);
-    return children[0];
-  }
-  return mkNode(PfRule::TRANS, children, {}, expected);
-}
-
-std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
-    std::shared_ptr<ProofNode> pf,
-    std::vector<Node>& assumps,
-    bool ensureClosed,
-    bool doMinimize,
-    Node expected)
-{
-  if (!ensureClosed)
-  {
-    return mkNode(PfRule::SCOPE, {pf}, assumps, expected);
-  }
-  Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl;
-  // we first ensure the assumptions are flattened
-  std::unordered_set<Node> ac{assumps.begin(), assumps.end()};
-  // map from the rewritten form of assumptions to the original. This is only
-  // computed in the rare case when we need rewriting to match the
-  // assumptions. An example of this is for Boolean constant equalities in
-  // scoped proofs from the proof equality engine.
-  std::unordered_map<Node, Node> acr;
-  // whether we have compute the map above
-  bool computedAcr = false;
-
-  // The free assumptions of the proof
-  std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
-  expr::getFreeAssumptionsMap(pf, famap);
-  std::unordered_set<Node> acu;
-  for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
-           fa : famap)
-  {
-    Node a = fa.first;
-    if (ac.find(a) != ac.end())
-    {
-      // already covered by an assumption
-      acu.insert(a);
-      continue;
-    }
-    // trivial assumption
-    if (a == d_true)
-    {
-      Trace("pnm-scope") << "- justify trivial True assumption\n";
-      for (std::shared_ptr<ProofNode> pfs : fa.second)
-      {
-        Assert(pfs->getResult() == a);
-        updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a});
-      }
-      Trace("pnm-scope") << "...finished" << std::endl;
-      acu.insert(a);
-      continue;
-    }
-    Trace("pnm-scope") << "- try matching free assumption " << a << "\n";
-    // otherwise it may be due to symmetry?
-    Node aeqSym = CDProof::getSymmFact(a);
-    Trace("pnm-scope") << "  - try sym " << aeqSym << "\n";
-    Node aMatch;
-    if (!aeqSym.isNull() && ac.count(aeqSym))
-    {
-      Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a
-                         << " for " << fa.second.size() << " proof nodes"
-                         << std::endl;
-      aMatch = aeqSym;
-    }
-    else
-    {
-      // Otherwise, may be derivable by rewriting. Note this is used in
-      // ensuring that proofs from the proof equality engine that involve
-      // equality with Boolean constants are closed.
-      if (!computedAcr)
-      {
-        computedAcr = true;
-        for (const Node& acc : ac)
-        {
-          Node accr = theory::Rewriter::rewrite(acc);
-          if (accr != acc)
-          {
-            acr[accr] = acc;
-          }
-        }
-      }
-      Node ar = theory::Rewriter::rewrite(a);
-      std::unordered_map<Node, Node>::iterator itr = acr.find(ar);
-      if (itr != acr.end())
-      {
-        aMatch = itr->second;
-      }
-    }
-
-    // if we found a match either by symmetry or rewriting, then we connect
-    // the assumption here.
-    if (!aMatch.isNull())
-    {
-      std::shared_ptr<ProofNode> pfaa = mkAssume(aMatch);
-      // must correct the orientation on this leaf
-      std::vector<std::shared_ptr<ProofNode>> children;
-      children.push_back(pfaa);
-      for (std::shared_ptr<ProofNode> pfs : fa.second)
-      {
-        Assert(pfs->getResult() == a);
-        // use SYMM if possible
-        if (aMatch == aeqSym)
-        {
-          updateNode(pfs.get(), PfRule::SYMM, children, {});
-        }
-        else
-        {
-          updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, {a});
-        }
-      }
-      Trace("pnm-scope") << "...finished" << std::endl;
-      acu.insert(aMatch);
-      continue;
-    }
-    // If we did not find a match, it is an error, since all free assumptions
-    // should be arguments to SCOPE.
-    std::stringstream ss;
-
-    bool dumpProofTraceOn = Trace.isOn("dump-proof-error");
-    if (dumpProofTraceOn)
-    {
-      ss << "The proof : " << *pf << std::endl;
-    }
-    ss << std::endl << "Free assumption: " << a << std::endl;
-    for (const Node& aprint : ac)
-    {
-      ss << "- assumption: " << aprint << std::endl;
-    }
-    if (!dumpProofTraceOn)
-    {
-      ss << "Use -t dump-proof-error for details on proof" << std::endl;
-    }
-    Unreachable() << "Generated a proof that is not closed by the scope: "
-                  << ss.str() << std::endl;
-  }
-  if (acu.size() < ac.size())
-  {
-    // All assumptions should match a free assumption; if one does not, then
-    // the explanation could have been smaller.
-    for (const Node& a : ac)
-    {
-      if (acu.find(a) == acu.end())
-      {
-        Notice() << "ProofNodeManager::mkScope: assumption " << a
-                 << " does not match a free assumption in proof" << std::endl;
-      }
-    }
-  }
-  if (doMinimize && acu.size() < ac.size())
-  {
-    assumps.clear();
-    assumps.insert(assumps.end(), acu.begin(), acu.end());
-  }
-  else if (ac.size() < assumps.size())
-  {
-    // remove duplicates to avoid redundant literals in clauses
-    assumps.clear();
-    assumps.insert(assumps.end(), ac.begin(), ac.end());
-  }
-  Node minExpected;
-  NodeManager* nm = NodeManager::currentNM();
-  Node exp;
-  if (assumps.empty())
-  {
-    // SCOPE with no arguments is a no-op, just return original
-    return pf;
-  }
-  Node conc = pf->getResult();
-  exp = assumps.size() == 1 ? assumps[0] : nm->mkNode(AND, assumps);
-  if (conc.isConst() && !conc.getConst<bool>())
-  {
-    minExpected = exp.notNode();
-  }
-  else
-  {
-    minExpected = nm->mkNode(IMPLIES, exp, conc);
-  }
-  return mkNode(PfRule::SCOPE, {pf}, assumps, minExpected);
-}
-
-bool ProofNodeManager::updateNode(
-    ProofNode* pn,
-    PfRule id,
-    const std::vector<std::shared_ptr<ProofNode>>& children,
-    const std::vector<Node>& args)
-{
-  return updateNodeInternal(pn, id, children, args, true);
-}
-
-bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr)
-{
-  Assert(pn != nullptr);
-  Assert(pnr != nullptr);
-  if (pn->getResult() != pnr->getResult())
-  {
-    return false;
-  }
-  // can shortcut re-check of rule
-  return updateNodeInternal(
-      pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false);
-}
-
-Node ProofNodeManager::checkInternal(
-    PfRule id,
-    const std::vector<std::shared_ptr<ProofNode>>& children,
-    const std::vector<Node>& args,
-    Node expected)
-{
-  Node res;
-  if (d_checker)
-  {
-    // check with the checker, which takes expected as argument
-    res = d_checker->check(id, children, args, expected);
-    Assert(!res.isNull())
-        << "ProofNodeManager::checkInternal: failed to check proof";
-  }
-  else
-  {
-    // otherwise we trust the expected value, if it exists
-    Assert(!expected.isNull()) << "ProofNodeManager::checkInternal: no checker "
-                                  "or expected value provided";
-    res = expected;
-  }
-  return res;
-}
-
-ProofChecker* ProofNodeManager::getChecker() const { return d_checker; }
-
-std::shared_ptr<ProofNode> ProofNodeManager::clone(
-    std::shared_ptr<ProofNode> pn)
-{
-  const ProofNode* orig = pn.get();
-  std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>> visited;
-  std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>>::iterator it;
-  std::vector<const ProofNode*> visit;
-  std::shared_ptr<ProofNode> cloned;
-  visit.push_back(orig);
-  const ProofNode* cur;
-  while (!visit.empty())
-  {
-    cur = visit.back();
-    it = visited.find(cur);
-    if (it == visited.end())
-    {
-      visited[cur] = nullptr;
-      const std::vector<std::shared_ptr<ProofNode>>& children =
-          cur->getChildren();
-      for (const std::shared_ptr<ProofNode>& cp : children)
-      {
-        visit.push_back(cp.get());
-      }
-      continue;
-    }
-    visit.pop_back();
-    if (it->second.get() == nullptr)
-    {
-      std::vector<std::shared_ptr<ProofNode>> cchildren;
-      const std::vector<std::shared_ptr<ProofNode>>& children =
-          cur->getChildren();
-      for (const std::shared_ptr<ProofNode>& cp : children)
-      {
-        it = visited.find(cp.get());
-        Assert(it != visited.end());
-        Assert(it->second != nullptr);
-        cchildren.push_back(it->second);
-      }
-      cloned = std::make_shared<ProofNode>(
-          cur->getRule(), cchildren, cur->getArguments());
-      visited[cur] = cloned;
-      // we trust the above cloning does not change what is proven
-      cloned->d_proven = cur->d_proven;
-    }
-  }
-  Assert(visited.find(orig) != visited.end());
-  return visited[orig];
-}
-
-bool ProofNodeManager::updateNodeInternal(
-    ProofNode* pn,
-    PfRule id,
-    const std::vector<std::shared_ptr<ProofNode>>& children,
-    const std::vector<Node>& args,
-    bool needsCheck)
-{
-  Assert(pn != nullptr);
-  // ---------------- check for cyclic
-  if (options::proofEagerChecking())
-  {
-    std::unordered_set<const ProofNode*> visited;
-    for (const std::shared_ptr<ProofNode>& cpc : children)
-    {
-      if (expr::containsSubproof(cpc.get(), pn, visited))
-      {
-        std::stringstream ss;
-        ss << "ProofNodeManager::updateNode: attempting to make cyclic proof! "
-           << id << " " << pn->getResult() << ", children = " << std::endl;
-        for (const std::shared_ptr<ProofNode>& cp : children)
-        {
-          ss << "  " << cp->getRule() << " " << cp->getResult() << std::endl;
-        }
-        ss << "Full children:" << std::endl;
-        for (const std::shared_ptr<ProofNode>& cp : children)
-        {
-          ss << "  - ";
-          cp->printDebug(ss);
-          ss << std::endl;
-        }
-        Unreachable() << ss.str();
-      }
-    }
-  }
-  // ---------------- end check for cyclic
-
-  // should have already computed what is proven
-  Assert(!pn->d_proven.isNull())
-      << "ProofNodeManager::updateProofNode: invalid proof provided";
-  if (needsCheck)
-  {
-    // We expect to prove the same thing as before
-    Node res = checkInternal(id, children, args, pn->d_proven);
-    if (res.isNull())
-    {
-      // if it was invalid, then we do not update
-      return false;
-    }
-    // proven field should already be the same as the result
-    Assert(res == pn->d_proven);
-  }
-
-  // we update its value
-  pn->setValue(id, children, args);
-  return true;
-}
-
-}  // namespace cvc5
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
deleted file mode 100644
index 853d22de7..000000000
--- a/src/expr/proof_node_manager.h
+++ /dev/null
@@ -1,206 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Proof node manager utility.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_NODE_MANAGER_H
-#define CVC5__EXPR__PROOF_NODE_MANAGER_H
-
-#include <vector>
-
-#include "expr/node.h"
-#include "expr/proof_rule.h"
-
-namespace cvc5 {
-
-class ProofChecker;
-class ProofNode;
-
-/**
- * A manager for proof node objects. This is a trusted interface for creating
- * and updating ProofNode objects.
- *
- * In more detail, we say a ProofNode is "well-formed (with respect to checker
- * X)" if its d_proven field is non-null, and corresponds to the formula that
- * the ProofNode proves according to X. The ProofNodeManager class constructs
- * and update nodes that are well-formed with respect to its underlying checker.
- *
- * If no checker is provided, then the ProofNodeManager assigns the d_proven
- * field of ProofNode based on the provided "expected" argument in mkNode below,
- * which must be provided in this case.
- *
- * The ProofNodeManager is used as a trusted way of updating ProofNode objects
- * via updateNode below. In particular, this method leaves the d_proven field
- * unchanged and updates (if possible) the remaining content of a given proof
- * node.
- *
- * Notice that ProofNode objects are mutable, and hence this class does not
- * cache the results of mkNode. A version of this class that caches
- * immutable version of ProofNode objects could be built as an extension
- * or layer on top of this class.
- */
-class ProofNodeManager
-{
- public:
-  ProofNodeManager(ProofChecker* pc = nullptr);
-  ~ProofNodeManager() {}
-  /**
-   * This constructs a ProofNode with the given arguments. The expected
-   * argument, when provided, indicates the formula that the returned node
-   * is expected to prove. If we find that it does not, based on the underlying
-   * checker, this method returns nullptr.
-   *
-   * @param id The id of the proof node.
-   * @param children The children of the proof node.
-   * @param args The arguments of the proof node.
-   * @param expected (Optional) the expected conclusion of the proof node.
-   * @return the proof node, or nullptr if the given arguments do not
-   * consistute a proof of the expected conclusion according to the underlying
-   * checker, if both are provided. It also returns nullptr if neither the
-   * checker nor the expected field is provided, since in this case the
-   * conclusion is unknown.
-   */
-  std::shared_ptr<ProofNode> mkNode(
-      PfRule id,
-      const std::vector<std::shared_ptr<ProofNode>>& children,
-      const std::vector<Node>& args,
-      Node expected = Node::null());
-  /**
-   * Make the proof node corresponding to the assumption of fact.
-   *
-   * @param fact The fact to assume.
-   * @return The ASSUME proof of fact.
-   */
-  std::shared_ptr<ProofNode> mkAssume(Node fact);
-  /**
-   * Make transitivity proof, where children contains one or more proofs of
-   * equalities that form an ordered chain. In other words, the vector children
-   * is a legal set of children for an application of TRANS.
-   */
-  std::shared_ptr<ProofNode> mkTrans(
-      const std::vector<std::shared_ptr<ProofNode>>& children,
-      Node expected = Node::null());
-
-  /**
-   * Make scope having body pf and arguments (assumptions-to-close) assumps.
-   * If ensureClosed is true, then this method throws an assertion failure if
-   * the returned proof is not closed. This is the case if a free assumption
-   * of pf is missing from the vector assumps.
-   *
-   * For conveinence, the proof pf may be modified to ensure that the overall
-   * result is closed. For instance, given input:
-   *   pf = TRANS( ASSUME( x=y ), ASSUME( y=z ) )
-   *   assumps = { y=x, y=z }
-   * This method will modify pf to be:
-   *   pf = TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) )
-   * so that y=x matches the free assumption. The returned proof is:
-   *   SCOPE(TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) :args { y=x, y=z })
-   *
-   * When ensureClosed is true, duplicates are eliminated from assumps. The
-   * reason for this is due to performance, since in this method, assumps is
-   * converted to an unordered_set to do the above check and hence it is a
-   * convienient time to eliminate duplicate literals.
-   *
-   * Additionally, if both ensureClosed and doMinimize are true, assumps is
-   * updated to contain exactly the free asumptions of pf. This also includes
-   * having no duplicates. Furthermore, if assumps is empty after minimization,
-   * this method is a no-op.
-   *
-   * In each case, the update vector assumps is passed as arguments to SCOPE.
-   *
-   * @param pf The body of the proof,
-   * @param assumps The assumptions-to-close of the scope,
-   * @param ensureClosed Whether to ensure that the proof is closed,
-   * @param doMinimize Whether to minimize assumptions.
-   * @param expected the node that the scope should prove.
-   * @return The scoped proof.
-   */
-  std::shared_ptr<ProofNode> mkScope(std::shared_ptr<ProofNode> pf,
-                                     std::vector<Node>& assumps,
-                                     bool ensureClosed = true,
-                                     bool doMinimize = false,
-                                     Node expected = Node::null());
-  /**
-   * This method updates pn to be a proof of the form <id>( children, args ),
-   * while maintaining its d_proven field. This method returns false if this
-   * proof manager is using a checker, and we compute that the above proof
-   * is not a proof of the fact that pn previously proved.
-   *
-   * @param pn The proof node to update.
-   * @param id The updated id of the proof node.
-   * @param children The updated children of the proof node.
-   * @param args The updated arguments of the proof node.
-   * @return true if the update was successful.
-   *
-   * Notice that updateNode always returns true if there is no underlying
-   * checker.
-   */
-  bool updateNode(ProofNode* pn,
-                  PfRule id,
-                  const std::vector<std::shared_ptr<ProofNode>>& children,
-                  const std::vector<Node>& args);
-  /**
-   * Update node pn to have the contents of pnr. It should be the case that
-   * pn and pnr prove the same fact, otherwise false is returned and pn is
-   * unchanged.
-   */
-  bool updateNode(ProofNode* pn, ProofNode* pnr);
-  /** Get the underlying proof checker */
-  ProofChecker* getChecker() const;
-  /**
-   * Clone a proof node, which creates a deep copy of pn and returns it. The
-   * dag structure of pn is the same as that in the returned proof node.
-   *
-   * @param pn The proof node to clone
-   * @return the cloned proof node.
-   */
-  std::shared_ptr<ProofNode> clone(std::shared_ptr<ProofNode> pn);
-
- private:
-  /** The (optional) proof checker */
-  ProofChecker* d_checker;
-  /** the true node */
-  Node d_true;
-  /** Check internal
-   *
-   * This returns the result of proof checking a ProofNode with the provided
-   * arguments with an expected conclusion, which may not null if there is
-   * no expected conclusion.
-   *
-   * This throws an assertion error if we fail to check such a proof node, or
-   * if expected is provided (non-null) and is different what is proven by the
-   * other arguments.
-   */
-  Node checkInternal(PfRule id,
-                     const std::vector<std::shared_ptr<ProofNode>>& children,
-                     const std::vector<Node>& args,
-                     Node expected);
-  /**
-   * Update node internal, return true if successful. This is called by
-   * the update node methods above. The argument needsCheck is whether we
-   * need to check the correctness of the rule application. This is false
-   * for the updateNode routine where pnr is an (already checked) proof node.
-   */
-  bool updateNodeInternal(
-      ProofNode* pn,
-      PfRule id,
-      const std::vector<std::shared_ptr<ProofNode>>& children,
-      const std::vector<Node>& args,
-      bool needsCheck);
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__PROOF_NODE_H */
diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
deleted file mode 100644
index 033232959..000000000
--- a/src/expr/proof_node_to_sexpr.cpp
+++ /dev/null
@@ -1,148 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of proof node to s-expression.
- */
-
-#include "expr/proof_node_to_sexpr.h"
-
-#include <iostream>
-#include <sstream>
-
-#include "expr/proof_node.h"
-#include "options/proof_options.h"
-
-using namespace cvc5::kind;
-
-namespace cvc5 {
-
-ProofNodeToSExpr::ProofNodeToSExpr()
-{
-  NodeManager* nm = NodeManager::currentNM();
-  d_conclusionMarker = nm->mkBoundVar(":conclusion", nm->sExprType());
-  d_argsMarker = nm->mkBoundVar(":args", nm->sExprType());
-}
-
-Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
-{
-  NodeManager* nm = NodeManager::currentNM();
-  std::map<const ProofNode*, Node>::iterator it;
-  std::vector<const ProofNode*> visit;
-  std::vector<const ProofNode*> traversing;
-  const ProofNode* cur;
-  visit.push_back(pn);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    it = d_pnMap.find(cur);
-
-    if (it == d_pnMap.end())
-    {
-      d_pnMap[cur] = Node::null();
-      traversing.push_back(cur);
-      visit.push_back(cur);
-      const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
-      for (const std::shared_ptr<ProofNode>& cp : pc)
-      {
-        if (std::find(traversing.begin(), traversing.end(), cp.get())
-            != traversing.end())
-        {
-          Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use "
-                         "--proof-eager-checking)"
-                      << std::endl;
-          return Node::null();
-        }
-        visit.push_back(cp.get());
-      }
-    }
-    else if (it->second.isNull())
-    {
-      Assert(!traversing.empty());
-      traversing.pop_back();
-      std::vector<Node> children;
-      // add proof rule
-      children.push_back(getOrMkPfRuleVariable(cur->getRule()));
-      if (options::proofPrintConclusion())
-      {
-        children.push_back(d_conclusionMarker);
-        children.push_back(cur->getResult());
-      }
-      const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
-      for (const std::shared_ptr<ProofNode>& cp : pc)
-      {
-        it = d_pnMap.find(cp.get());
-        Assert(it != d_pnMap.end());
-        Assert(!it->second.isNull());
-        children.push_back(it->second);
-      }
-      // add arguments
-      const std::vector<Node>& args = cur->getArguments();
-      if (!args.empty())
-      {
-        children.push_back(d_argsMarker);
-        // needed to ensure builtin operators are not treated as operators
-        // this can be the case for CONG where d_args may contain a builtin
-        // operator
-        std::vector<Node> argsSafe;
-        for (const Node& a : args)
-        {
-          Node av = a;
-          if (a.getNumChildren() == 0
-              && NodeManager::operatorToKind(a) != UNDEFINED_KIND)
-          {
-            av = getOrMkNodeVariable(a);
-          }
-          argsSafe.push_back(av);
-        }
-        Node argsC = nm->mkNode(SEXPR, argsSafe);
-        children.push_back(argsC);
-      }
-      d_pnMap[cur] = nm->mkNode(SEXPR, children);
-    }
-  } while (!visit.empty());
-  Assert(d_pnMap.find(pn) != d_pnMap.end());
-  Assert(!d_pnMap.find(pn)->second.isNull());
-  return d_pnMap[pn];
-}
-
-Node ProofNodeToSExpr::getOrMkPfRuleVariable(PfRule r)
-{
-  std::map<PfRule, Node>::iterator it = d_pfrMap.find(r);
-  if (it != d_pfrMap.end())
-  {
-    return it->second;
-  }
-  std::stringstream ss;
-  ss << r;
-  NodeManager* nm = NodeManager::currentNM();
-  Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
-  d_pfrMap[r] = var;
-  return var;
-}
-
-Node ProofNodeToSExpr::getOrMkNodeVariable(Node n)
-{
-  std::map<Node, Node>::iterator it = d_nodeMap.find(n);
-  if (it != d_nodeMap.end())
-  {
-    return it->second;
-  }
-  std::stringstream ss;
-  ss << n;
-  NodeManager* nm = NodeManager::currentNM();
-  Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
-  d_nodeMap[n] = var;
-  return var;
-}
-
-}  // namespace cvc5
diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h
deleted file mode 100644
index d4cca8eae..000000000
--- a/src/expr/proof_node_to_sexpr.h
+++ /dev/null
@@ -1,70 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Conversion from ProofNode to s-expressions.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_NODE_TO_SEXPR_H
-#define CVC5__EXPR__PROOF_NODE_TO_SEXPR_H
-
-#include <map>
-
-#include "expr/node.h"
-#include "expr/proof_rule.h"
-
-namespace cvc5 {
-
-class ProofNode;
-
-/** A class to convert ProofNode objects to s-expressions */
-class ProofNodeToSExpr
-{
- public:
-  ProofNodeToSExpr();
-  ~ProofNodeToSExpr() {}
-  /** Convert the given proof node to an s-expression
-   *
-   * This is useful for operations where it is useful to view a ProofNode as
-   * a Node. Printing is one such example, where a ProofNode can be printed
-   * as a dag after this conversion.
-   *
-   * The s-expression for a ProofNode has the form:
-   *   (SEXPR (VAR "<d_rule>") S1 ... Sn (VAR ":args") (SEXPR <d_args>))
-   * where S1, ..., Sn are the s-expressions for its <d_children>.
-   */
-  Node convertToSExpr(const ProofNode* pn);
-
- private:
-  /** map proof rules to a variable */
-  std::map<PfRule, Node> d_pfrMap;
-  /** Dummy ":args" marker */
-  Node d_argsMarker;
-  /** Dummy ":conclusion" marker */
-  Node d_conclusionMarker;
-  /** map proof nodes to their s-expression */
-  std::map<const ProofNode*, Node> d_pnMap;
-  /**
-   * map nodes to a bound variable, used for nodes that have special AST status
-   * like builtin operators
-   */
-  std::map<Node, Node> d_nodeMap;
-  /** get or make pf rule variable */
-  Node getOrMkPfRuleVariable(PfRule r);
-  /** get or make node variable */
-  Node getOrMkNodeVariable(Node n);
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__PROOF_RULE_H */
diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
deleted file mode 100644
index e2fd0c566..000000000
--- a/src/expr/proof_node_updater.cpp
+++ /dev/null
@@ -1,258 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of a utility for updating proof nodes.
- */
-
-#include "expr/proof_node_updater.h"
-
-#include "expr/lazy_proof.h"
-#include "expr/proof_ensure_closed.h"
-#include "expr/proof_node_algorithm.h"
-#include "expr/proof_node_manager.h"
-
-namespace cvc5 {
-
-ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {}
-ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {}
-
-bool ProofNodeUpdaterCallback::update(Node res,
-                                      PfRule id,
-                                      const std::vector<Node>& children,
-                                      const std::vector<Node>& args,
-                                      CDProof* cdp,
-                                      bool& continueUpdate)
-{
-  return false;
-}
-
-ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm,
-                                   ProofNodeUpdaterCallback& cb,
-                                   bool mergeSubproofs,
-                                   bool autoSym)
-    : d_pnm(pnm),
-      d_cb(cb),
-      d_debugFreeAssumps(false),
-      d_mergeSubproofs(mergeSubproofs),
-      d_autoSym(autoSym)
-{
-}
-
-void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf)
-{
-  if (d_debugFreeAssumps)
-  {
-    if (Trace.isOn("pfnu-debug"))
-    {
-      Trace("pfnu-debug2") << "Initial proof: " << *pf.get() << std::endl;
-      Trace("pfnu-debug") << "ProofNodeUpdater::process" << std::endl;
-      Trace("pfnu-debug") << "Expected free assumptions: " << std::endl;
-      for (const Node& fa : d_freeAssumps)
-      {
-        Trace("pfnu-debug") << "- " << fa << std::endl;
-      }
-      std::vector<Node> assump;
-      expr::getFreeAssumptions(pf.get(), assump);
-      Trace("pfnu-debug") << "Current free assumptions: " << std::endl;
-      for (const Node& fa : assump)
-      {
-        Trace("pfnu-debug") << "- " << fa << std::endl;
-      }
-    }
-  }
-  std::vector<std::shared_ptr<ProofNode>> traversing;
-  processInternal(pf, d_freeAssumps, traversing);
-}
-
-void ProofNodeUpdater::processInternal(
-    std::shared_ptr<ProofNode> pf,
-    const std::vector<Node>& fa,
-    std::vector<std::shared_ptr<ProofNode>>& traversing)
-{
-  Trace("pf-process") << "ProofNodeUpdater::process" << std::endl;
-  std::unordered_map<std::shared_ptr<ProofNode>, bool> visited;
-  std::unordered_map<std::shared_ptr<ProofNode>, bool>::iterator it;
-  std::vector<std::shared_ptr<ProofNode>> visit;
-  std::shared_ptr<ProofNode> cur;
-  visit.push_back(pf);
-  std::map<Node, std::shared_ptr<ProofNode>>::iterator itc;
-  // A cache from formulas to proof nodes that are in the current scope.
-  // Notice that we make a fresh recursive call to process if the current
-  // rule is SCOPE below.
-  std::map<Node, std::shared_ptr<ProofNode>> resCache;
-  Node res;
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    it = visited.find(cur);
-    res = cur->getResult();
-    if (it == visited.end())
-    {
-      if (d_mergeSubproofs)
-      {
-        itc = resCache.find(res);
-        if (itc != resCache.end())
-        {
-          // already have a proof, merge it into this one
-          visited[cur] = true;
-          d_pnm->updateNode(cur.get(), itc->second.get());
-          continue;
-        }
-      }
-      // run update to a fixed point
-      bool continueUpdate = true;
-      while (runUpdate(cur, fa, continueUpdate) && continueUpdate)
-      {
-        Trace("pf-process-debug") << "...updated proof." << std::endl;
-      }
-      visited[cur] = !continueUpdate;
-      if (!continueUpdate)
-      {
-        // no further changes should be made to cur according to the callback
-        Trace("pf-process-debug")
-            << "...marked to not continue update." << std::endl;
-        runFinalize(cur, fa, resCache);
-        continue;
-      }
-      traversing.push_back(cur);
-      visit.push_back(cur);
-      // If we are not the top-level proof, we were a scope, or became a scope
-      // after updating, we do a separate recursive call to this method. This
-      // allows us to properly track the assumptions in scope, which is
-      // important for example to merge or to determine updates based on free
-      // assumptions.
-      if (cur->getRule() == PfRule::SCOPE && cur != pf)
-      {
-        std::vector<Node> nfa;
-        nfa.insert(nfa.end(), fa.begin(), fa.end());
-        const std::vector<Node>& args = cur->getArguments();
-        nfa.insert(nfa.end(), args.begin(), args.end());
-        Trace("pfnu-debug2") << "Process new scope with " << args << std::endl;
-        // Process in new call separately
-        processInternal(cur, nfa, traversing);
-        continue;
-      }
-      const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
-      // now, process children
-      for (const std::shared_ptr<ProofNode>& cp : ccp)
-      {
-        if (std::find(traversing.begin(), traversing.end(), cp)
-            != traversing.end())
-        {
-          Unhandled()
-              << "ProofNodeUpdater::processInternal: cyclic proof! (use "
-                 "--proof-eager-checking)"
-              << std::endl;
-        }
-        visit.push_back(cp);
-      }
-    }
-    else if (!it->second)
-    {
-      Assert(!traversing.empty());
-      traversing.pop_back();
-      visited[cur] = true;
-      // finalize the node
-      runFinalize(cur, fa, resCache);
-    }
-  } while (!visit.empty());
-  Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl;
-}
-
-bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
-                                 const std::vector<Node>& fa,
-                                 bool& continueUpdate)
-{
-  // should it be updated?
-  if (!d_cb.shouldUpdate(cur, fa, continueUpdate))
-  {
-    return false;
-  }
-  PfRule id = cur->getRule();
-  // use CDProof to open a scope for which the callback updates
-  CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym);
-  const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
-  std::vector<Node> ccn;
-  for (const std::shared_ptr<ProofNode>& cp : cc)
-  {
-    Node cpres = cp->getResult();
-    ccn.push_back(cpres);
-    // store in the proof
-    cpf.addProof(cp);
-  }
-  Node res = cur->getResult();
-  Trace("pf-process-debug")
-      << "Updating (" << cur->getRule() << "): " << res << std::endl;
-  // only if the callback updated the node
-  if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate))
-  {
-    std::shared_ptr<ProofNode> npn = cpf.getProofFor(res);
-    std::vector<Node> fullFa;
-    if (d_debugFreeAssumps)
-    {
-      expr::getFreeAssumptions(cur.get(), fullFa);
-      Trace("pfnu-debug") << "Original proof : " << *cur << std::endl;
-    }
-    // then, update the original proof node based on this one
-    Trace("pf-process-debug") << "Update node..." << std::endl;
-    d_pnm->updateNode(cur.get(), npn.get());
-    Trace("pf-process-debug") << "...update node finished." << std::endl;
-    if (d_debugFreeAssumps)
-    {
-      fullFa.insert(fullFa.end(), fa.begin(), fa.end());
-      // We have that npn is a node we occurring the final updated version of
-      // the proof. We can now debug based on the expected set of free
-      // assumptions.
-      Trace("pfnu-debug") << "Ensure update closed..." << std::endl;
-      pfnEnsureClosedWrt(
-          npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate");
-    }
-    Trace("pf-process-debug") << "..finished" << std::endl;
-    return true;
-  }
-  Trace("pf-process-debug") << "..finished" << std::endl;
-  return false;
-}
-
-void ProofNodeUpdater::runFinalize(
-    std::shared_ptr<ProofNode> cur,
-    const std::vector<Node>& fa,
-    std::map<Node, std::shared_ptr<ProofNode>>& resCache)
-{
-  if (d_mergeSubproofs)
-  {
-    Node res = cur->getResult();
-    // cache result if we are merging subproofs
-    resCache[res] = cur;
-  }
-  if (d_debugFreeAssumps)
-  {
-    // We have that npn is a node we occurring the final updated version of
-    // the proof. We can now debug based on the expected set of free
-    // assumptions.
-    Trace("pfnu-debug") << "Ensure update closed..." << std::endl;
-    pfnEnsureClosedWrt(
-        cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize");
-  }
-}
-
-void ProofNodeUpdater::setDebugFreeAssumptions(
-    const std::vector<Node>& freeAssumps)
-{
-  d_freeAssumps.clear();
-  d_freeAssumps.insert(
-      d_freeAssumps.end(), freeAssumps.begin(), freeAssumps.end());
-  d_debugFreeAssumps = true;
-}
-
-}  // namespace cvc5
diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
deleted file mode 100644
index 215c61210..000000000
--- a/src/expr/proof_node_updater.h
+++ /dev/null
@@ -1,164 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * A utility for updating proof nodes.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_NODE_UPDATER_H
-#define CVC5__EXPR__PROOF_NODE_UPDATER_H
-
-#include <map>
-#include <memory>
-
-#include "expr/node.h"
-#include "expr/proof_node.h"
-
-namespace cvc5 {
-
-class CDProof;
-class ProofNode;
-class ProofNodeManager;
-
-/**
- * A virtual callback class for updating ProofNode. An example use case of this
- * class is to eliminate a proof rule by expansion.
- */
-class ProofNodeUpdaterCallback
-{
- public:
-  ProofNodeUpdaterCallback();
-  virtual ~ProofNodeUpdaterCallback();
-  /** Should proof pn be updated?
-   *
-   * @param pn the proof node that maybe should be updated
-   * @param fa the assumptions in scope
-   * @param continueUpdate whether we should continue recursively updating pn
-   * @return whether we should run the update method on pn
-   */
-  virtual bool shouldUpdate(std::shared_ptr<ProofNode> pn,
-                            const std::vector<Node>& fa,
-                            bool& continueUpdate) = 0;
-  /**
-   * Update the proof rule application, store steps in cdp. Return true if
-   * the proof changed. It can be assumed that cdp contains proofs of each
-   * fact in children.
-   *
-   * If continueUpdate is set to false in this method, then the resulting
-   * proof (the proof of res in cdp) is *not* called back to update by the
-   * proof node updater, nor are its children recursed. Otherwise, by default,
-   * the proof node updater will continue updating the resulting proof and will
-   * recursively update its children. This is analogous to marking REWRITE_DONE
-   * in a rewrite response.
-   */
-  virtual bool update(Node res,
-                      PfRule id,
-                      const std::vector<Node>& children,
-                      const std::vector<Node>& args,
-                      CDProof* cdp,
-                      bool& continueUpdate);
-};
-
-/**
- * A generic class for updating ProofNode. It is parameterized by a callback
- * class. Its process method runs this callback on all subproofs of a provided
- * ProofNode application that meet some criteria
- * (ProofNodeUpdaterCallback::shouldUpdate)
- * and overwrites them based on the update procedure of the callback
- * (ProofNodeUpdaterCallback::update), which uses local CDProof objects that
- * should be filled in the callback for each ProofNode to update. This update
- * process is applied in a *pre-order* traversal.
- */
-class ProofNodeUpdater
-{
- public:
-  /**
-   * @param pnm The proof node manager we are using
-   * @param cb The callback to apply to each node
-   * @param mergeSubproofs Whether to automatically merge subproofs within
-   * the same SCOPE that prove the same fact.
-   * @param autoSym Whether intermediate CDProof objects passed to updater
-   * callbacks automatically introduce SYMM steps.
-   */
-  ProofNodeUpdater(ProofNodeManager* pnm,
-                   ProofNodeUpdaterCallback& cb,
-                   bool mergeSubproofs = false,
-                   bool autoSym = true);
-  /**
-   * Post-process, which performs the main post-processing technique described
-   * above.
-   */
-  void process(std::shared_ptr<ProofNode> pf);
-
-  /**
-   * Set free assumptions to freeAssumps. This indicates that we expect
-   * the proof we are processing to have free assumptions that are in
-   * freeAssumps. This enables checking when this is violated, which is
-   * expensive in general. It is not recommended that this method is called
-   * by default.
-   */
-  void setDebugFreeAssumptions(const std::vector<Node>& freeAssumps);
-
- private:
-  /** The proof node manager */
-  ProofNodeManager* d_pnm;
-  /** The callback */
-  ProofNodeUpdaterCallback& d_cb;
-  /**
-   * Post-process, which performs the main post-processing technique described
-   * above.
-   *
-   * @param pf The proof to process
-   * @param fa The assumptions of the scope that fa is a subproof of with
-   * respect to the original proof. For example, if (SCOPE P :args (A B)), we
-   * may call this method on P with fa = { A, B }.
-   * @param traversing The list of proof nodes we are currently traversing
-   * beneath. This is used for checking for cycles in the overall proof.
-   */
-  void processInternal(std::shared_ptr<ProofNode> pf,
-                       const std::vector<Node>& fa,
-                       std::vector<std::shared_ptr<ProofNode>>& traversing);
-  /**
-   * Update proof node cur based on the callback. This modifies curr using
-   * ProofNodeManager::updateNode based on the proof node constructed to
-   * replace it by the callback. Return true if cur was updated. If
-   * continueUpdate is updated to false, then cur is not updated further
-   * and its children are not traversed.
-   */
-  bool runUpdate(std::shared_ptr<ProofNode> cur,
-                 const std::vector<Node>& fa,
-                 bool& continueUpdate);
-  /**
-   * Finalize the node cur. This is called at the moment that it is established
-   * that cur will appear in the final proof. We do any final debug checking
-   * and add it to the results cache resCache if we are merging subproofs.
-   */
-  void runFinalize(std::shared_ptr<ProofNode> cur,
-                   const std::vector<Node>& fa,
-                   std::map<Node, std::shared_ptr<ProofNode>>& resCache);
-  /** Are we debugging free assumptions? */
-  bool d_debugFreeAssumps;
-  /** The initial free assumptions */
-  std::vector<Node> d_freeAssumps;
-  /** Whether we are merging subproofs */
-  bool d_mergeSubproofs;
-  /**
-   * Whether intermediate CDProof objects passed to updater callbacks
-   * automatically introduce SYMM steps.
-   */
-  bool d_autoSym;
-};
-
-}  // namespace cvc5
-
-#endif
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
deleted file mode 100644
index f4e8078dc..000000000
--- a/src/expr/proof_rule.cpp
+++ /dev/null
@@ -1,258 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of proof rule.
- */
-
-#include "expr/proof_rule.h"
-
-#include <iostream>
-
-namespace cvc5 {
-
-const char* toString(PfRule id)
-{
-  switch (id)
-  {
-    //================================================= Core rules
-    case PfRule::ASSUME: return "ASSUME";
-    case PfRule::SCOPE: return "SCOPE";
-    case PfRule::SUBS: return "SUBS";
-    case PfRule::REWRITE: return "REWRITE";
-    case PfRule::EVALUATE: return "EVALUATE";
-    case PfRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO";
-    case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO";
-    case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
-    case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
-    case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM";
-    //================================================= Trusted rules
-    case PfRule::THEORY_LEMMA: return "THEORY_LEMMA";
-    case PfRule::THEORY_REWRITE: return "THEORY_REWRITE";
-    case PfRule::PREPROCESS: return "PREPROCESS";
-    case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA";
-    case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS";
-    case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA";
-    case PfRule::THEORY_EXPAND_DEF: return "THEORY_EXPAND_DEF";
-    case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM";
-    case PfRule::TRUST_REWRITE: return "TRUST_REWRITE";
-    case PfRule::TRUST_SUBS: return "TRUST_SUBS";
-    case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP";
-    //================================================= Boolean rules
-    case PfRule::RESOLUTION: return "RESOLUTION";
-    case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION";
-    case PfRule::FACTORING: return "FACTORING";
-    case PfRule::REORDERING: return "REORDERING";
-    case PfRule::MACRO_RESOLUTION: return "MACRO_RESOLUTION";
-    case PfRule::MACRO_RESOLUTION_TRUST: return "MACRO_RESOLUTION_TRUST";
-    case PfRule::SPLIT: return "SPLIT";
-    case PfRule::EQ_RESOLVE: return "EQ_RESOLVE";
-    case PfRule::MODUS_PONENS: return "MODUS_PONENS";
-    case PfRule::NOT_NOT_ELIM: return "NOT_NOT_ELIM";
-    case PfRule::CONTRA: return "CONTRA";
-    case PfRule::AND_ELIM: return "AND_ELIM";
-    case PfRule::AND_INTRO: return "AND_INTRO";
-    case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM";
-    case PfRule::IMPLIES_ELIM: return "IMPLIES_ELIM";
-    case PfRule::NOT_IMPLIES_ELIM1: return "NOT_IMPLIES_ELIM1";
-    case PfRule::NOT_IMPLIES_ELIM2: return "NOT_IMPLIES_ELIM2";
-    case PfRule::EQUIV_ELIM1: return "EQUIV_ELIM1";
-    case PfRule::EQUIV_ELIM2: return "EQUIV_ELIM2";
-    case PfRule::NOT_EQUIV_ELIM1: return "NOT_EQUIV_ELIM1";
-    case PfRule::NOT_EQUIV_ELIM2: return "NOT_EQUIV_ELIM2";
-    case PfRule::XOR_ELIM1: return "XOR_ELIM1";
-    case PfRule::XOR_ELIM2: return "XOR_ELIM2";
-    case PfRule::NOT_XOR_ELIM1: return "NOT_XOR_ELIM1";
-    case PfRule::NOT_XOR_ELIM2: return "NOT_XOR_ELIM2";
-    case PfRule::ITE_ELIM1: return "ITE_ELIM1";
-    case PfRule::ITE_ELIM2: return "ITE_ELIM2";
-    case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1";
-    case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2";
-    //================================================= De Morgan rules
-    case PfRule::NOT_AND: return "NOT_AND";
-    //================================================= CNF rules
-    case PfRule::CNF_AND_POS: return "CNF_AND_POS";
-    case PfRule::CNF_AND_NEG: return "CNF_AND_NEG";
-    case PfRule::CNF_OR_POS: return "CNF_OR_POS";
-    case PfRule::CNF_OR_NEG: return "CNF_OR_NEG";
-    case PfRule::CNF_IMPLIES_POS: return "CNF_IMPLIES_POS";
-    case PfRule::CNF_IMPLIES_NEG1: return "CNF_IMPLIES_NEG1";
-    case PfRule::CNF_IMPLIES_NEG2: return "CNF_IMPLIES_NEG2";
-    case PfRule::CNF_EQUIV_POS1: return "CNF_EQUIV_POS1";
-    case PfRule::CNF_EQUIV_POS2: return "CNF_EQUIV_POS2";
-    case PfRule::CNF_EQUIV_NEG1: return "CNF_EQUIV_NEG1";
-    case PfRule::CNF_EQUIV_NEG2: return "CNF_EQUIV_NEG2";
-    case PfRule::CNF_XOR_POS1: return "CNF_XOR_POS1";
-    case PfRule::CNF_XOR_POS2: return "CNF_XOR_POS2";
-    case PfRule::CNF_XOR_NEG1: return "CNF_XOR_NEG1";
-    case PfRule::CNF_XOR_NEG2: return "CNF_XOR_NEG2";
-    case PfRule::CNF_ITE_POS1: return "CNF_ITE_POS1";
-    case PfRule::CNF_ITE_POS2: return "CNF_ITE_POS2";
-    case PfRule::CNF_ITE_POS3: return "CNF_ITE_POS3";
-    case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1";
-    case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2";
-    case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3";
-    //================================================= Equality rules
-    case PfRule::REFL: return "REFL";
-    case PfRule::SYMM: return "SYMM";
-    case PfRule::TRANS: return "TRANS";
-    case PfRule::CONG: return "CONG";
-    case PfRule::TRUE_INTRO: return "TRUE_INTRO";
-    case PfRule::TRUE_ELIM: return "TRUE_ELIM";
-    case PfRule::FALSE_INTRO: return "FALSE_INTRO";
-    case PfRule::FALSE_ELIM: return "FALSE_ELIM";
-    case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE";
-    case PfRule::HO_CONG: return "HO_CONG";
-    //================================================= Array rules
-    case PfRule::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
-    case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA:
-      return "ARRAYS_READ_OVER_WRITE_CONTRA";
-    case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
-    case PfRule::ARRAYS_EXT: return "ARRAYS_EXT";
-    case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST";
-    //================================================= Bit-Vector rules
-    case PfRule::BV_BITBLAST: return "BV_BITBLAST";
-    case PfRule::BV_BITBLAST_CONST: return "BV_BITBLAST_CONST";
-    case PfRule::BV_BITBLAST_VAR: return "BV_BITBLAST_VAR";
-    case PfRule::BV_BITBLAST_EQUAL: return "BV_BITBLAST_EQUAL";
-    case PfRule::BV_BITBLAST_ULT: return "BV_BITBLAST_ULT";
-    case PfRule::BV_BITBLAST_ULE: return "BV_BITBLAST_ULE";
-    case PfRule::BV_BITBLAST_UGT: return "BV_BITBLAST_UGT";
-    case PfRule::BV_BITBLAST_UGE: return "BV_BITBLAST_UGE";
-    case PfRule::BV_BITBLAST_SLT: return "BV_BITBLAST_SLT";
-    case PfRule::BV_BITBLAST_SLE: return "BV_BITBLAST_SLE";
-    case PfRule::BV_BITBLAST_SGT: return "BV_BITBLAST_SGT";
-    case PfRule::BV_BITBLAST_SGE: return "BV_BITBLAST_SGE";
-    case PfRule::BV_BITBLAST_NOT: return "BV_BITBLAST_NOT";
-    case PfRule::BV_BITBLAST_CONCAT: return "BV_BITBLAST_CONCAT";
-    case PfRule::BV_BITBLAST_AND: return "BV_BITBLAST_AND";
-    case PfRule::BV_BITBLAST_OR: return "BV_BITBLAST_OR";
-    case PfRule::BV_BITBLAST_XOR: return "BV_BITBLAST_XOR";
-    case PfRule::BV_BITBLAST_XNOR: return "BV_BITBLAST_XNOR";
-    case PfRule::BV_BITBLAST_NAND: return "BV_BITBLAST_NAND";
-    case PfRule::BV_BITBLAST_NOR: return "BV_BITBLAST_NOR";
-    case PfRule::BV_BITBLAST_COMP: return "BV_BITBLAST_COMP";
-    case PfRule::BV_BITBLAST_MULT: return "BV_BITBLAST_MULT";
-    case PfRule::BV_BITBLAST_ADD: return "BV_BITBLAST_ADD";
-    case PfRule::BV_BITBLAST_SUB: return "BV_BITBLAST_SUB";
-    case PfRule::BV_BITBLAST_NEG: return "BV_BITBLAST_NEG";
-    case PfRule::BV_BITBLAST_UDIV: return "BV_BITBLAST_UDIV";
-    case PfRule::BV_BITBLAST_UREM: return "BV_BITBLAST_UREM";
-    case PfRule::BV_BITBLAST_SDIV: return "BV_BITBLAST_SDIV";
-    case PfRule::BV_BITBLAST_SREM: return "BV_BITBLAST_SREM";
-    case PfRule::BV_BITBLAST_SMOD: return "BV_BITBLAST_SMOD";
-    case PfRule::BV_BITBLAST_SHL: return "BV_BITBLAST_SHL";
-    case PfRule::BV_BITBLAST_LSHR: return "BV_BITBLAST_LSHR";
-    case PfRule::BV_BITBLAST_ASHR: return "BV_BITBLAST_ASHR";
-    case PfRule::BV_BITBLAST_ULTBV: return "BV_BITBLAST_ULTBV";
-    case PfRule::BV_BITBLAST_SLTBV: return "BV_BITBLAST_SLTBV";
-    case PfRule::BV_BITBLAST_ITE: return "BV_BITBLAST_ITE";
-    case PfRule::BV_BITBLAST_EXTRACT: return "BV_BITBLAST_EXTRACT";
-    case PfRule::BV_BITBLAST_REPEAT: return "BV_BITBLAST_REPEAT";
-    case PfRule::BV_BITBLAST_ZERO_EXTEND: return "BV_BITBLAST_ZERO_EXTEND";
-    case PfRule::BV_BITBLAST_SIGN_EXTEND: return "BV_BITBLAST_SIGN_EXTEND";
-    case PfRule::BV_BITBLAST_ROTATE_RIGHT: return "BV_BITBLAST_ROTATE_RIGHT";
-    case PfRule::BV_BITBLAST_ROTATE_LEFT: return "BV_BITBLAST_ROTATE_LEFT";
-    case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM";
-    //================================================= Datatype rules
-    case PfRule::DT_UNIF: return "DT_UNIF";
-    case PfRule::DT_INST: return "DT_INST";
-    case PfRule::DT_COLLAPSE: return "DT_COLLAPSE";
-    case PfRule::DT_SPLIT: return "DT_SPLIT";
-    case PfRule::DT_CLASH: return "DT_CLASH";
-    case PfRule::DT_TRUST: return "DT_TRUST";
-    //================================================= Quantifiers rules
-    case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO";
-    case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
-    case PfRule::SKOLEMIZE: return "SKOLEMIZE";
-    case PfRule::INSTANTIATE: return "INSTANTIATE";
-    //================================================= String rules
-    case PfRule::CONCAT_EQ: return "CONCAT_EQ";
-    case PfRule::CONCAT_UNIFY: return "CONCAT_UNIFY";
-    case PfRule::CONCAT_CONFLICT: return "CONCAT_CONFLICT";
-    case PfRule::CONCAT_SPLIT: return "CONCAT_SPLIT";
-    case PfRule::CONCAT_CSPLIT: return "CONCAT_CSPLIT";
-    case PfRule::CONCAT_LPROP: return "CONCAT_LPROP";
-    case PfRule::CONCAT_CPROP: return "CONCAT_CPROP";
-    case PfRule::STRING_DECOMPOSE: return "STRING_DECOMPOSE";
-    case PfRule::STRING_LENGTH_POS: return "STRING_LENGTH_POS";
-    case PfRule::STRING_LENGTH_NON_EMPTY: return "STRING_LENGTH_NON_EMPTY";
-    case PfRule::STRING_REDUCTION: return "STRING_REDUCTION";
-    case PfRule::STRING_EAGER_REDUCTION: return "STRING_EAGER_REDUCTION";
-    case PfRule::RE_INTER: return "RE_INTER";
-    case PfRule::RE_UNFOLD_POS: return "RE_UNFOLD_POS";
-    case PfRule::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG";
-    case PfRule::RE_UNFOLD_NEG_CONCAT_FIXED:
-      return "RE_UNFOLD_NEG_CONCAT_FIXED";
-    case PfRule::RE_ELIM: return "RE_ELIM";
-    case PfRule::STRING_CODE_INJ: return "STRING_CODE_INJ";
-    case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ";
-    case PfRule::STRING_TRUST: return "STRING_TRUST";
-    //================================================= Arith rules
-    case PfRule::MACRO_ARITH_SCALE_SUM_UB:
-      return "ARITH_SCALE_SUM_UPPER_BOUNDS";
-    case PfRule::ARITH_SUM_UB: return "ARITH_SUM_UB";
-    case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY";
-    case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB";
-    case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB";
-    case PfRule::INT_TRUST: return "INT_TRUST";
-    case PfRule::ARITH_MULT_SIGN: return "ARITH_MULT_SIGN";
-    case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS";
-    case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG";
-    case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT";
-    case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
-    case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI";
-    case PfRule::ARITH_TRANS_EXP_NEG: return "ARITH_TRANS_EXP_NEG";
-    case PfRule::ARITH_TRANS_EXP_POSITIVITY:
-      return "ARITH_TRANS_EXP_POSITIVITY";
-    case PfRule::ARITH_TRANS_EXP_SUPER_LIN: return "ARITH_TRANS_EXP_SUPER_LIN";
-    case PfRule::ARITH_TRANS_EXP_ZERO: return "ARITH_TRANS_EXP_ZERO";
-    case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG:
-      return "ARITH_TRANS_EXP_APPROX_ABOVE_NEG";
-    case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS:
-      return "ARITH_TRANS_EXP_APPROX_ABOVE_POS";
-    case PfRule::ARITH_TRANS_EXP_APPROX_BELOW:
-      return "ARITH_TRANS_EXP_APPROX_BELOW";
-    case PfRule::ARITH_TRANS_SINE_BOUNDS: return "ARITH_TRANS_SINE_BOUNDS";
-    case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT";
-    case PfRule::ARITH_TRANS_SINE_SYMMETRY: return "ARITH_TRANS_SINE_SYMMETRY";
-    case PfRule::ARITH_TRANS_SINE_TANGENT_ZERO:
-      return "ARITH_TRANS_SINE_TANGENT_ZERO";
-    case PfRule::ARITH_TRANS_SINE_TANGENT_PI:
-      return "ARITH_TRANS_SINE_TANGENT_PI";
-    case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG:
-      return "ARITH_TRANS_SINE_APPROX_ABOVE_NEG";
-    case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS:
-      return "ARITH_TRANS_SINE_APPROX_ABOVE_POS";
-    case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG:
-      return "ARITH_TRANS_SINE_APPROX_BELOW_NEG";
-    case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS:
-      return "ARITH_TRANS_SINE_APPROX_BELOW_POS";
-    case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT";
-    case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE";
-    //================================================= Unknown rule
-    case PfRule::UNKNOWN: return "UNKNOWN";
-    default: return "?";
-  }
-}
-
-std::ostream& operator<<(std::ostream& out, PfRule id)
-{
-  out << toString(id);
-  return out;
-}
-
-size_t PfRuleHashFunction::operator()(PfRule id) const
-{
-  return static_cast<size_t>(id);
-}
-
-}  // namespace cvc5
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
deleted file mode 100644
index 9771dda31..000000000
--- a/src/expr/proof_rule.h
+++ /dev/null
@@ -1,1453 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Proof rule enumeration.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_RULE_H
-#define CVC5__EXPR__PROOF_RULE_H
-
-#include <iosfwd>
-
-namespace cvc5 {
-
-/**
- * An enumeration for proof rules. This enumeration is analogous to Kind for
- * Node objects. In the documentation below, P:F denotes a ProofNode that
- * proves formula F.
- *
- * Conceptually, the following proof rules form a calculus whose target
- * user is the Node-level theory solvers. This means that the rules below
- * are designed to reason about, among other things, common operations on Node
- * objects like Rewriter::rewrite or Node::substitute. It is intended to be
- * translated or printed in other formats.
- *
- * The following PfRule values include core rules and those categorized by
- * theory, including the theory of equality.
- *
- * The "core rules" include two distinguished rules which have special status:
- * (1) ASSUME, which represents an open leaf in a proof.
- * (2) SCOPE, which closes the scope of assumptions.
- * The core rules additionally correspond to generic operations that are done
- * internally on nodes, e.g. calling Rewriter::rewrite.
- *
- * Rules with prefix MACRO_ are those that can be defined in terms of other
- * rules. These exist for convienience. We provide their definition in the line
- * "Macro:".
- */
-enum class PfRule : uint32_t
-{
-  //================================================= Core rules
-  //======================== Assume and Scope
-  // ======== Assumption (a leaf)
-  // Children: none
-  // Arguments: (F)
-  // --------------
-  // Conclusion: F
-  //
-  // This rule has special status, in that an application of assume is an
-  // open leaf in a proof that is not (yet) justified. An assume leaf is
-  // analogous to a free variable in a term, where we say "F is a free
-  // assumption in proof P" if it contains an application of F that is not
-  // bound by SCOPE (see below).
-  ASSUME,
-  // ======== Scope (a binder for assumptions)
-  // Children: (P:F)
-  // Arguments: (F1, ..., Fn)
-  // --------------
-  // Conclusion: (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)) if F is false
-  //
-  // This rule has a dual purpose with ASSUME. It is a way to close
-  // assumptions in a proof. We require that F1 ... Fn are free assumptions in
-  // P and say that F1, ..., Fn are not free in (SCOPE P). In other words, they
-  // are bound by this application. For example, the proof node:
-  //   (SCOPE (ASSUME F) :args F)
-  // has the conclusion (=> F F) and has no free assumptions. More generally, a
-  // proof with no free assumptions always concludes a valid formula.
-  SCOPE,
-
-  //======================== Builtin theory (common node operations)
-  // ======== Substitution
-  // Children: (P1:F1, ..., Pn:Fn)
-  // Arguments: (t, (ids)?)
-  // ---------------------------------------------------------------
-  // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1))
-  // where sigma{ids}(Fi) are substitutions, which notice are applied in
-  // reverse order.
-  // Notice that ids is a MethodId identifier, which determines how to convert
-  // the formulas F1, ..., Fn into substitutions.
-  SUBS,
-  // ======== Rewrite
-  // Children: none
-  // Arguments: (t, (idr)?)
-  // ----------------------------------------
-  // Conclusion: (= t Rewriter{idr}(t))
-  // where idr is a MethodId identifier, which determines the kind of rewriter
-  // to apply, e.g. Rewriter::rewrite.
-  REWRITE,
-  // ======== Evaluate
-  // Children: none
-  // Arguments: (t)
-  // ----------------------------------------
-  // Conclusion: (= t Evaluator::evaluate(t))
-  // Note this is equivalent to:
-  //   (REWRITE t MethodId::RW_EVALUATE)
-  EVALUATE,
-  // ======== Substitution + Rewriting equality introduction
-  //
-  // In this rule, we provide a term t and conclude that it is equal to its
-  // rewritten form under a (proven) substitution.
-  //
-  // Children: (P1:F1, ..., Pn:Fn)
-  // Arguments: (t, (ids (ida (idr)?)?)?)
-  // ---------------------------------------------------------------
-  // Conclusion: (= t t')
-  // where
-  //   t' is
-  //   Rewriter{idr}(t*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1))
-  //
-  // In other words, from the point of view of Skolem forms, this rule
-  // transforms t to t' by standard substitution + rewriting.
-  //
-  // The arguments ids, ida and idr are optional and specify the identifier of
-  // the substitution, the substitution application and rewriter respectively to
-  // be used. For details, see theory/builtin/proof_checker.h.
-  MACRO_SR_EQ_INTRO,
-  // ======== Substitution + Rewriting predicate introduction
-  //
-  // In this rule, we provide a formula F and conclude it, under the condition
-  // that it rewrites to true under a proven substitution.
-  //
-  // Children: (P1:F1, ..., Pn:Fn)
-  // Arguments: (F, (ids (ida (idr)?)?)?)
-  // ---------------------------------------------------------------
-  // Conclusion: F
-  // where
-  //   Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) == true
-  // where ids and idr are method identifiers.
-  //
-  // More generally, this rule also holds when:
-  //   Rewriter::rewrite(toOriginal(F')) == true
-  // where F' is the result of the left hand side of the equality above. Here,
-  // notice that we apply rewriting on the original form of F', meaning that
-  // this rule may conclude an F whose Skolem form is justified by the
-  // definition of its (fresh) Skolem variables. For example, this rule may
-  // justify the conclusion (= k t) where k is the purification Skolem for t,
-  // e.g. where the original form of k is t.
-  //
-  // Furthermore, notice that the rewriting and substitution is applied only
-  // within the side condition, meaning the rewritten form of the original form
-  // of F does not escape this rule.
-  MACRO_SR_PRED_INTRO,
-  // ======== Substitution + Rewriting predicate elimination
-  //
-  // In this rule, if we have proven a formula F, then we may conclude its
-  // rewritten form under a proven substitution.
-  //
-  // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
-  // Arguments: ((ids (ida (idr)?)?)?)
-  // ----------------------------------------
-  // Conclusion: F'
-  // where
-  //   F' is
-  //   Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)).
-  // where ids and idr are method identifiers.
-  //
-  // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
-  MACRO_SR_PRED_ELIM,
-  // ======== Substitution + Rewriting predicate transform
-  //
-  // In this rule, if we have proven a formula F, then we may provide a formula
-  // G and conclude it if F and G are equivalent after rewriting under a proven
-  // substitution.
-  //
-  // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
-  // Arguments: (G, (ids (ida (idr)?)?)?)
-  // ----------------------------------------
-  // Conclusion: G
-  // where
-  //   Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) ==
-  //   Rewriter{idr}(G*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1))
-  //
-  // More generally, this rule also holds when:
-  //   Rewriter::rewrite(toOriginal(F')) == Rewriter::rewrite(toOriginal(G'))
-  // where F' and G' are the result of each side of the equation above. Here,
-  // original forms are used in a similar manner to MACRO_SR_PRED_INTRO above.
-  MACRO_SR_PRED_TRANSFORM,
-  //================================================= Processing rules
-  // ======== Remove Term Formulas Axiom
-  // Children: none
-  // Arguments: (t)
-  // ---------------------------------------------------------------
-  // Conclusion: RemoveTermFormulas::getAxiomFor(t).
-  REMOVE_TERM_FORMULA_AXIOM,
-
-  //================================================= Trusted rules
-  // ======== Theory lemma
-  // Children: none
-  // Arguments: (F, tid)
-  // ---------------------------------------------------------------
-  // Conclusion: F
-  // where F is a (T-valid) theory lemma generated by theory with TheoryId tid.
-  // This is a "coarse-grained" rule that is used as a placeholder if a theory
-  // did not provide a proof for a lemma or conflict.
-  THEORY_LEMMA,
-  // ======== Theory Rewrite
-  // Children: none
-  // Arguments: (F, tid, rid)
-  // ----------------------------------------
-  // Conclusion: F
-  // where F is an equality of the form (= t t') where t' is obtained by
-  // applying the kind of rewriting given by the method identifier rid, which
-  // is one of:
-  //  { RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT }
-  // Notice that the checker for this rule does not replay the rewrite to ensure
-  // correctness, since theory rewriter methods are not static. For example,
-  // the quantifiers rewriter involves constructing new bound variables that are
-  // not guaranteed to be consistent on each call.
-  THEORY_REWRITE,
-  // The remaining rules in this section have the signature of a "trusted rule":
-  //
-  // Children: none
-  // Arguments: (F)
-  // ---------------------------------------------------------------
-  // Conclusion: F
-  //
-  // where F is an equality of the form t = t' where t was replaced by t'
-  // based on some preprocessing pass, or otherwise F was added as a new
-  // assertion by some preprocessing pass.
-  PREPROCESS,
-  // where F was added as a new assertion by some preprocessing pass.
-  PREPROCESS_LEMMA,
-  // where F is an equality of the form t = Theory::ppRewrite(t) for some
-  // theory. Notice this is a "trusted" rule.
-  THEORY_PREPROCESS,
-  // where F was added as a new assertion by theory preprocessing.
-  THEORY_PREPROCESS_LEMMA,
-  // where F is an equality of the form t = t' where t was replaced by t'
-  // based on theory expand definitions.
-  THEORY_EXPAND_DEF,
-  // where F is an existential (exists ((x T)) (P x)) used for introducing
-  // a witness term (witness ((x T)) (P x)).
-  WITNESS_AXIOM,
-  // where F is an equality (= t t') that holds by a form of rewriting that
-  // could not be replayed during proof postprocessing.
-  TRUST_REWRITE,
-  // where F is an equality (= t t') that holds by a form of substitution that
-  // could not be replayed during proof postprocessing.
-  TRUST_SUBS,
-  // where F is an equality (= t t') that holds by a form of substitution that
-  // could not be determined by the TrustSubstitutionMap.
-  TRUST_SUBS_MAP,
-  // ========= SAT Refutation for assumption-based unsat cores
-  // Children: (P1, ..., Pn)
-  // Arguments: none
-  // ---------------------
-  // Conclusion: false
-  // Note: P1, ..., Pn correspond to the unsat core determined by the SAT
-  // solver.
-  SAT_REFUTATION,
-
-  //================================================= Boolean rules
-  // ======== Resolution
-  // Children:
-  //  (P1:C1, P2:C2)
-  // Arguments: (pol, L)
-  // ---------------------
-  // Conclusion: C
-  // where
-  //   - C1 and C2 are nodes viewed as clauses, i.e., either an OR node with
-  //     each children viewed as a literal or a node viewed as a literal. Note
-  //     that an OR node could also be a literal.
-  //   - pol is either true or false, representing the polarity of the pivot on
-  //     the first clause
-  //   - L is the pivot of the resolution, which occurs as is (resp. under a
-  //     NOT) in C1 and negatively (as is) in C2 if pol = true (pol = false).
-  //   C is a clause resulting from collecting all the literals in C1, minus the
-  //   first occurrence of the pivot or its negation, and C2, minus the first
-  //   occurrence of the pivot or its negation, according to the policy above.
-  //   If the resulting clause has a single literal, that literal itself is the
-  //   result; if it has no literals, then the result is false; otherwise it's
-  //   an OR node of the resulting literals.
-  //
-  //   Note that it may be the case that the pivot does not occur in the
-  //   clauses. In this case the rule is not unsound, but it does not correspond
-  //   to resolution but rather to a weakening of the clause that did not have a
-  //   literal eliminated.
-  RESOLUTION,
-  // ======== N-ary Resolution
-  // Children: (P1:C_1, ..., Pm:C_n)
-  // Arguments: (pol_1, L_1, ..., pol_{n-1}, L_{n-1})
-  // ---------------------
-  // Conclusion: C
-  // where
-  //   - let C_1 ... C_n be nodes viewed as clauses, as defined above
-  //   - let "C_1 <>_{L,pol} C_2" represent the resolution of C_1 with C_2 with
-  //     pivot L and polarity pol, as defined above
-  //   - let C_1' = C_1 (from P1),
-  //   - for each i > 1, let C_i' = C_{i-1} <>_{L_{i-1}, pol_{i-1}} C_i'
-  //   The result of the chain resolution is C = C_n'
-  CHAIN_RESOLUTION,
-  // ======== Factoring
-  // Children: (P:C1)
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: C2
-  // where
-  //  Set representations of C1 and C2 is the same and the number of literals in
-  //  C2 is smaller than that of C1
-  FACTORING,
-  // ======== Reordering
-  // Children: (P:C1)
-  // Arguments: (C2)
-  // ---------------------
-  // Conclusion: C2
-  // where
-  //  Set representations of C1 and C2 are the same and the number of literals
-  //  in C2 is the same of that of C1
-  REORDERING,
-  // ======== N-ary Resolution + Factoring + Reordering
-  // Children: (P1:C_1, ..., Pm:C_n)
-  // Arguments: (C, pol_1, L_1, ..., pol_{n-1}, L_{n-1})
-  // ---------------------
-  // Conclusion: C
-  // where
-  //   - let C_1 ... C_n be nodes viewed as clauses, as defined in RESOLUTION
-  //   - let "C_1 <>_{L,pol} C_2" represent the resolution of C_1 with C_2 with
-  //     pivot L and polarity pol, as defined in RESOLUTION
-  //   - let C_1' be equal, in its set representation, to C_1 (from P1),
-  //   - for each i > 1, let C_i' be equal, it its set representation, to
-  //     C_{i-1} <>_{L_{i-1}, pol_{i-1}} C_i'
-  //   The result of the chain resolution is C, which is equal, in its set
-  //   representation, to C_n'
-  MACRO_RESOLUTION,
-  // As above but not checked
-  MACRO_RESOLUTION_TRUST,
-
-  // ======== Split
-  // Children: none
-  // Arguments: (F)
-  // ---------------------
-  // Conclusion: (or F (not F))
-  SPLIT,
-  // ======== Equality resolution
-  // Children: (P1:F1, P2:(= F1 F2))
-  // Arguments: none
-  // ---------------------
-  // Conclusion: (F2)
-  // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION.
-  EQ_RESOLVE,
-  // ======== Modus ponens
-  // Children: (P1:F1, P2:(=> F1 F2))
-  // Arguments: none
-  // ---------------------
-  // Conclusion: (F2)
-  // Note this can optionally be seen as a macro for IMPLIES_ELIM+RESOLUTION.
-  MODUS_PONENS,
-  // ======== Double negation elimination
-  // Children: (P:(not (not F)))
-  // Arguments: none
-  // ---------------------
-  // Conclusion: (F)
-  NOT_NOT_ELIM,
-  // ======== Contradiction
-  // Children: (P1:F P2:(not F))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: false
-  CONTRA,
-  // ======== And elimination
-  // Children: (P:(and F1 ... Fn))
-  // Arguments: (i)
-  // ---------------------
-  // Conclusion: (Fi)
-  AND_ELIM,
-  // ======== And introduction
-  // Children: (P1:F1 ... Pn:Fn))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (and P1 ... Pn)
-  AND_INTRO,
-  // ======== Not Or elimination
-  // Children: (P:(not (or F1 ... Fn)))
-  // Arguments: (i)
-  // ---------------------
-  // Conclusion: (not Fi)
-  NOT_OR_ELIM,
-  // ======== Implication elimination
-  // Children: (P:(=> F1 F2))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or (not F1) F2)
-  IMPLIES_ELIM,
-  // ======== Not Implication elimination version 1
-  // Children: (P:(not (=> F1 F2)))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (F1)
-  NOT_IMPLIES_ELIM1,
-  // ======== Not Implication elimination version 2
-  // Children: (P:(not (=> F1 F2)))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (not F2)
-  NOT_IMPLIES_ELIM2,
-  // ======== Equivalence elimination version 1
-  // Children: (P:(= F1 F2))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or (not F1) F2)
-  EQUIV_ELIM1,
-  // ======== Equivalence elimination version 2
-  // Children: (P:(= F1 F2))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or F1 (not F2))
-  EQUIV_ELIM2,
-  // ======== Not Equivalence elimination version 1
-  // Children: (P:(not (= F1 F2)))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or F1 F2)
-  NOT_EQUIV_ELIM1,
-  // ======== Not Equivalence elimination version 2
-  // Children: (P:(not (= F1 F2)))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or (not F1) (not F2))
-  NOT_EQUIV_ELIM2,
-  // ======== XOR elimination version 1
-  // Children: (P:(xor F1 F2)))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or F1 F2)
-  XOR_ELIM1,
-  // ======== XOR elimination version 2
-  // Children: (P:(xor F1 F2)))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or (not F1) (not F2))
-  XOR_ELIM2,
-  // ======== Not XOR elimination version 1
-  // Children: (P:(not (xor F1 F2)))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or F1 (not F2))
-  NOT_XOR_ELIM1,
-  // ======== Not XOR elimination version 2
-  // Children: (P:(not (xor F1 F2)))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or (not F1) F2)
-  NOT_XOR_ELIM2,
-  // ======== ITE elimination version 1
-  // Children: (P:(ite C F1 F2))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or (not C) F1)
-  ITE_ELIM1,
-  // ======== ITE elimination version 2
-  // Children: (P:(ite C F1 F2))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or C F2)
-  ITE_ELIM2,
-  // ======== Not ITE elimination version 1
-  // Children: (P:(not (ite C F1 F2)))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or (not C) (not F1))
-  NOT_ITE_ELIM1,
-  // ======== Not ITE elimination version 1
-  // Children: (P:(not (ite C F1 F2)))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or C (not F2))
-  NOT_ITE_ELIM2,
-
-  //================================================= De Morgan rules
-  // ======== Not And
-  // Children: (P:(not (and F1 ... Fn))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (or (not F1) ... (not Fn))
-  NOT_AND,
-  //================================================= CNF rules
-  // ======== CNF And Pos
-  // Children: ()
-  // Arguments: ((and F1 ... Fn), i)
-  // ---------------------
-  // Conclusion: (or (not (and F1 ... Fn)) Fi)
-  CNF_AND_POS,
-  // ======== CNF And Neg
-  // Children: ()
-  // Arguments: ((and F1 ... Fn))
-  // ---------------------
-  // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn))
-  CNF_AND_NEG,
-  // ======== CNF Or Pos
-  // Children: ()
-  // Arguments: ((or F1 ... Fn))
-  // ---------------------
-  // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn)
-  CNF_OR_POS,
-  // ======== CNF Or Neg
-  // Children: ()
-  // Arguments: ((or F1 ... Fn), i)
-  // ---------------------
-  // Conclusion: (or (or F1 ... Fn) (not Fi))
-  CNF_OR_NEG,
-  // ======== CNF Implies Pos
-  // Children: ()
-  // Arguments: ((implies F1 F2))
-  // ---------------------
-  // Conclusion: (or (not (implies F1 F2)) (not F1) F2)
-  CNF_IMPLIES_POS,
-  // ======== CNF Implies Neg version 1
-  // Children: ()
-  // Arguments: ((implies F1 F2))
-  // ---------------------
-  // Conclusion: (or (implies F1 F2) F1)
-  CNF_IMPLIES_NEG1,
-  // ======== CNF Implies Neg version 2
-  // Children: ()
-  // Arguments: ((implies F1 F2))
-  // ---------------------
-  // Conclusion: (or (implies F1 F2) (not F2))
-  CNF_IMPLIES_NEG2,
-  // ======== CNF Equiv Pos version 1
-  // Children: ()
-  // Arguments: ((= F1 F2))
-  // ---------------------
-  // Conclusion: (or (not (= F1 F2)) (not F1) F2)
-  CNF_EQUIV_POS1,
-  // ======== CNF Equiv Pos version 2
-  // Children: ()
-  // Arguments: ((= F1 F2))
-  // ---------------------
-  // Conclusion: (or (not (= F1 F2)) F1 (not F2))
-  CNF_EQUIV_POS2,
-  // ======== CNF Equiv Neg version 1
-  // Children: ()
-  // Arguments: ((= F1 F2))
-  // ---------------------
-  // Conclusion: (or (= F1 F2) F1 F2)
-  CNF_EQUIV_NEG1,
-  // ======== CNF Equiv Neg version 2
-  // Children: ()
-  // Arguments: ((= F1 F2))
-  // ---------------------
-  // Conclusion: (or (= F1 F2) (not F1) (not F2))
-  CNF_EQUIV_NEG2,
-  // ======== CNF Xor Pos version 1
-  // Children: ()
-  // Arguments: ((xor F1 F2))
-  // ---------------------
-  // Conclusion: (or (not (xor F1 F2)) F1 F2)
-  CNF_XOR_POS1,
-  // ======== CNF Xor Pos version 2
-  // Children: ()
-  // Arguments: ((xor F1 F2))
-  // ---------------------
-  // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2))
-  CNF_XOR_POS2,
-  // ======== CNF Xor Neg version 1
-  // Children: ()
-  // Arguments: ((xor F1 F2))
-  // ---------------------
-  // Conclusion: (or (xor F1 F2) (not F1) F2)
-  CNF_XOR_NEG1,
-  // ======== CNF Xor Neg version 2
-  // Children: ()
-  // Arguments: ((xor F1 F2))
-  // ---------------------
-  // Conclusion: (or (xor F1 F2) F1 (not F2))
-  CNF_XOR_NEG2,
-  // ======== CNF ITE Pos version 1
-  // Children: ()
-  // Arguments: ((ite C F1 F2))
-  // ---------------------
-  // Conclusion: (or (not (ite C F1 F2)) (not C) F1)
-  CNF_ITE_POS1,
-  // ======== CNF ITE Pos version 2
-  // Children: ()
-  // Arguments: ((ite C F1 F2))
-  // ---------------------
-  // Conclusion: (or (not (ite C F1 F2)) C F2)
-  CNF_ITE_POS2,
-  // ======== CNF ITE Pos version 3
-  // Children: ()
-  // Arguments: ((ite C F1 F2))
-  // ---------------------
-  // Conclusion: (or (not (ite C F1 F2)) F1 F2)
-  CNF_ITE_POS3,
-  // ======== CNF ITE Neg version 1
-  // Children: ()
-  // Arguments: ((ite C F1 F2))
-  // ---------------------
-  // Conclusion: (or (ite C F1 F2) (not C) (not F1))
-  CNF_ITE_NEG1,
-  // ======== CNF ITE Neg version 2
-  // Children: ()
-  // Arguments: ((ite C F1 F2))
-  // ---------------------
-  // Conclusion: (or (ite C F1 F2) C (not F2))
-  CNF_ITE_NEG2,
-  // ======== CNF ITE Neg version 3
-  // Children: ()
-  // Arguments: ((ite C F1 F2))
-  // ---------------------
-  // Conclusion: (or (ite C F1 F2) (not F1) (not F2))
-  CNF_ITE_NEG3,
-
-  //================================================= Equality rules
-  // ======== Reflexive
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (= t t)
-  REFL,
-  // ======== Symmetric
-  // Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
-  // Arguments: none
-  // -----------------------
-  // Conclusion: (= t2 t1) or (not (= t2 t1))
-  SYMM,
-  // ======== Transitivity
-  // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
-  // Arguments: none
-  // -----------------------
-  // Conclusion: (= t1 tn)
-  TRANS,
-  // ======== Congruence
-  // Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
-  // Arguments: (<kind> f?)
-  // ---------------------------------------------
-  // 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)
-  // Arguments: none
-  // ----------------------------------------
-  // Conclusion: (= F true)
-  TRUE_INTRO,
-  // ======== True elim
-  // Children: (P:(= F true))
-  // Arguments: none
-  // ----------------------------------------
-  // Conclusion: F
-  TRUE_ELIM,
-  // ======== False intro
-  // Children: (P:(not F))
-  // Arguments: none
-  // ----------------------------------------
-  // Conclusion: (= F false)
-  FALSE_INTRO,
-  // ======== False elim
-  // Children: (P:(= F false))
-  // Arguments: none
-  // ----------------------------------------
-  // Conclusion: (not F)
-  FALSE_ELIM,
-  // ======== HO trust
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (= t TheoryUfRewriter::getHoApplyForApplyUf(t))
-  // For example, this rule concludes (f x y) = (HO_APPLY (HO_APPLY f x) y)
-  HO_APP_ENCODE,
-  // ======== Congruence
-  // Children: (P1:(= f g), P2:(= t1 s1), ..., Pn+1:(= tn sn))
-  // Arguments: ()
-  // ---------------------------------------------
-  // Conclusion: (= (f t1 ... tn) (g s1 ... sn))
-  // Notice that this rule is only used when the application kinds are APPLY_UF.
-  HO_CONG,
-
-  //================================================= Array rules
-  // ======== Read over write
-  // Children: (P:(not (= i1 i2)))
-  // Arguments: ((select (store a i2 e) i1))
-  // ----------------------------------------
-  // Conclusion: (= (select (store a i2 e) i1) (select a i1))
-  ARRAYS_READ_OVER_WRITE,
-  // ======== Read over write, contrapositive
-  // Children: (P:(not (= (select (store a i2 e) i1) (select a i1)))
-  // Arguments: none
-  // ----------------------------------------
-  // Conclusion: (= i1 i2)
-  ARRAYS_READ_OVER_WRITE_CONTRA,
-  // ======== Read over write 1
-  // Children: none
-  // Arguments: ((select (store a i e) i))
-  // ----------------------------------------
-  // Conclusion: (= (select (store a i e) i) e)
-  ARRAYS_READ_OVER_WRITE_1,
-  // ======== Extensionality
-  // Children: (P:(not (= a b)))
-  // Arguments: none
-  // ----------------------------------------
-  // Conclusion: (not (= (select a k) (select b k)))
-  // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))).
-  ARRAYS_EXT,
-  // ======== Array Trust
-  // Children: (P1 ... Pn)
-  // Arguments: (F)
-  // ---------------------
-  // Conclusion: F
-  ARRAYS_TRUST,
-
-  //================================================= Bit-Vector rules
-  // Note: bitblast() represents the result of the bit-blasted term as a
-  //       bit-vector consisting of the output bits of the bit-blasted circuit
-  //       representation of the term. Terms are bit-blasted according to the
-  //       strategies defined in
-  //       theory/bv/bitblast/bitblast_strategies_template.h.
-  // ======== Bitblast
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (= t bitblast(t))
-  BV_BITBLAST,
-  // ======== Bitblast Bit-Vector Constant
-  // Children: none
-  // Arguments: (= t bitblast(t))
-  // ---------------------
-  // Conclusion: (= t bitblast(t))
-  BV_BITBLAST_CONST,
-  // ======== Bitblast Bit-Vector Variable
-  // Children: none
-  // Arguments: (= t bitblast(t))
-  // ---------------------
-  // Conclusion: (= t bitblast(t))
-  BV_BITBLAST_VAR,
-  // ======== Bitblast Bit-Vector Terms
-  // TODO cvc4-projects issue #275
-  // Children: none
-  // Arguments: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t))
-  // ---------------------
-  // Conclusion: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t))
-  BV_BITBLAST_EQUAL,
-  BV_BITBLAST_ULT,
-  BV_BITBLAST_ULE,
-  BV_BITBLAST_UGT,
-  BV_BITBLAST_UGE,
-  BV_BITBLAST_SLT,
-  BV_BITBLAST_SLE,
-  BV_BITBLAST_SGT,
-  BV_BITBLAST_SGE,
-  BV_BITBLAST_NOT,
-  BV_BITBLAST_CONCAT,
-  BV_BITBLAST_AND,
-  BV_BITBLAST_OR,
-  BV_BITBLAST_XOR,
-  BV_BITBLAST_XNOR,
-  BV_BITBLAST_NAND,
-  BV_BITBLAST_NOR,
-  BV_BITBLAST_COMP,
-  BV_BITBLAST_MULT,
-  BV_BITBLAST_ADD,
-  BV_BITBLAST_SUB,
-  BV_BITBLAST_NEG,
-  BV_BITBLAST_UDIV,
-  BV_BITBLAST_UREM,
-  BV_BITBLAST_SDIV,
-  BV_BITBLAST_SREM,
-  BV_BITBLAST_SMOD,
-  BV_BITBLAST_SHL,
-  BV_BITBLAST_LSHR,
-  BV_BITBLAST_ASHR,
-  BV_BITBLAST_ULTBV,
-  BV_BITBLAST_SLTBV,
-  BV_BITBLAST_ITE,
-  BV_BITBLAST_EXTRACT,
-  BV_BITBLAST_REPEAT,
-  BV_BITBLAST_ZERO_EXTEND,
-  BV_BITBLAST_SIGN_EXTEND,
-  BV_BITBLAST_ROTATE_RIGHT,
-  BV_BITBLAST_ROTATE_LEFT,
-  // ======== Eager Atom
-  // Children: none
-  // Arguments: (F)
-  // ---------------------
-  // Conclusion: (= F F[0])
-  // where F is of kind BITVECTOR_EAGER_ATOM
-  BV_EAGER_ATOM,
-
-  //================================================= Datatype rules
-  // ======== Unification
-  // Children: (P:(= (C t1 ... tn) (C s1 ... sn)))
-  // Arguments: (i)
-  // ----------------------------------------
-  // Conclusion: (= ti si)
-  // where C is a constructor.
-  DT_UNIF,
-  // ======== Instantiate
-  // Children: none
-  // Arguments: (t, n)
-  // ----------------------------------------
-  // Conclusion: (= ((_ is C) t) (= t (C (sel_1 t) ... (sel_n t))))
-  // where C is the n^th constructor of the type of T, and (_ is C) is the
-  // discriminator (tester) for C.
-  DT_INST,
-  // ======== Collapse
-  // Children: none
-  // Arguments: ((sel_i (C_j t_1 ... t_n)))
-  // ----------------------------------------
-  // Conclusion: (= (sel_i (C_j t_1 ... t_n)) r)
-  // where C_j is a constructor, r is t_i if sel_i is a correctly applied
-  // selector, or TypeNode::mkGroundTerm() of the proper type otherwise. Notice
-  // that the use of mkGroundTerm differs from the rewriter which uses
-  // mkGroundValue in this case.
-  DT_COLLAPSE,
-  // ======== Split
-  // Children: none
-  // Arguments: (t)
-  // ----------------------------------------
-  // Conclusion: (or ((_ is C1) t) ... ((_ is Cn) t))
-  DT_SPLIT,
-  // ======== Clash
-  // Children: (P1:((_ is Ci) t), P2: ((_ is Cj) t))
-  // Arguments: none
-  // ----------------------------------------
-  // Conclusion: false
-  // for i != j.
-  DT_CLASH,
-  // ======== Datatype Trust
-  // Children: (P1 ... Pn)
-  // Arguments: (F)
-  // ---------------------
-  // Conclusion: F
-  DT_TRUST,
-
-  //================================================= Quantifiers rules
-  // ======== Skolem intro
-  // Children: none
-  // Arguments: (k)
-  // ----------------------------------------
-  // Conclusion: (= k t)
-  // where t is the original form of skolem k.
-  SKOLEM_INTRO,
-  // ======== Exists intro
-  // Children: (P:F[t])
-  // Arguments: ((exists ((x T)) F[x]))
-  // ----------------------------------------
-  // Conclusion: (exists ((x T)) F[x])
-  // This rule verifies that F[x] indeed matches F[t] with a substitution
-  // over x.
-  EXISTS_INTRO,
-  // ======== Skolemize
-  // Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
-  // Arguments: none
-  // ----------------------------------------
-  // Conclusion: F*sigma
-  // sigma maps x1 ... xn to their representative skolems obtained by
-  // SkolemManager::mkSkolemize, returned in the skolems argument of that
-  // method. Alternatively, can use negated forall as a premise. The witness
-  // terms for the returned skolems can be obtained by
-  // SkolemManager::getWitnessForm.
-  SKOLEMIZE,
-  // ======== Instantiate
-  // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
-  // Arguments: (t1 ... tn)
-  // ----------------------------------------
-  // Conclusion: F*sigma
-  // sigma maps x1 ... xn to t1 ... tn.
-  INSTANTIATE,
-
-  //================================================= String rules
-  //======================== Core solver
-  // ======== Concat eq
-  // Children: (P1:(= (str.++ t1 ... tn t) (str.++ t1 ... tn s)))
-  // Arguments: (b), indicating if reverse direction
-  // ---------------------
-  // Conclusion: (= t s)
-  //
-  // Notice that t or s may be empty, in which case they are implicit in the
-  // concatenation above. For example, if
-  // P1 concludes (= x (str.++ x z)), then
-  // (CONCAT_EQ P1 :args false) concludes (= "" z)
-  //
-  // Also note that constants are split, such that if
-  // P1 concludes (= (str.++ "abc" x) (str.++ "a" y)), then
-  // (CONCAT_EQ P1 :args false) concludes (= (str.++ "bc" x) y)
-  // This splitting is done only for constants such that Word::splitConstant
-  // returns non-null.
-  CONCAT_EQ,
-  // ======== Concat unify
-  // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
-  //            P2:(= (str.len t1) (str.len s1)))
-  // Arguments: (b), indicating if reverse direction
-  // ---------------------
-  // Conclusion: (= t1 s1)
-  CONCAT_UNIFY,
-  // ======== Concat conflict
-  // Children: (P1:(= (str.++ c1 t) (str.++ c2 s)))
-  // Arguments: (b), indicating if reverse direction
-  // ---------------------
-  // Conclusion: false
-  // Where c1, c2 are constants such that Word::splitConstant(c1,c2,index,b)
-  // is null, in other words, neither is a prefix of the other.
-  CONCAT_CONFLICT,
-  // ======== Concat split
-  // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
-  //            P2:(not (= (str.len t1) (str.len s1))))
-  // Arguments: (false)
-  // ---------------------
-  // Conclusion: (or (= t1 (str.++ s1 r_t)) (= s1 (str.++ t1 r_s)))
-  // where
-  //   r_t = (skolem (suf t1 (str.len s1)))),
-  //   r_s = (skolem (suf s1 (str.len t1)))).
-  //
-  // or the reverse form of the above:
-  //
-  // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
-  //            P2:(not (= (str.len t2) (str.len s2))))
-  // Arguments: (true)
-  // ---------------------
-  // Conclusion: (or (= t2 (str.++ r_t s2)) (= s2 (str.++ r_s t2)))
-  // where
-  //   r_t = (skolem (pre t2 (- (str.len t2) (str.len s2))))),
-  //   r_s = (skolem (pre s2 (- (str.len s2) (str.len t2))))).
-  //
-  // Above, (suf x n) is shorthand for (str.substr x n (- (str.len x) n)) and
-  // (pre x n) is shorthand for (str.substr x 0 n).
-  CONCAT_SPLIT,
-  // ======== Concat constant split
-  // Children: (P1:(= (str.++ t1 t2) (str.++ c s2)),
-  //            P2:(not (= (str.len t1) 0)))
-  // Arguments: (false)
-  // ---------------------
-  // Conclusion: (= t1 (str.++ c r))
-  // where
-  //   r = (skolem (suf t1 1)).
-  //
-  // or the reverse form of the above:
-  //
-  // Children: (P1:(= (str.++ t1 t2) (str.++ s1 c)),
-  //            P2:(not (= (str.len t2) 0)))
-  // Arguments: (true)
-  // ---------------------
-  // Conclusion: (= t2 (str.++ r c))
-  // where
-  //   r = (skolem (pre t2 (- (str.len t2) 1))).
-  CONCAT_CSPLIT,
-  // ======== Concat length propagate
-  // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
-  //            P2:(> (str.len t1) (str.len s1)))
-  // Arguments: (false)
-  // ---------------------
-  // Conclusion: (= t1 (str.++ s1 r_t))
-  // where
-  //   r_t = (skolem (suf t1 (str.len s1)))
-  //
-  // or the reverse form of the above:
-  //
-  // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
-  //            P2:(> (str.len t2) (str.len s2)))
-  // Arguments: (false)
-  // ---------------------
-  // Conclusion: (= t2 (str.++ r_t s2))
-  // where
-  //   r_t = (skolem (pre t2 (- (str.len t2) (str.len s2)))).
-  CONCAT_LPROP,
-  // ======== Concat constant propagate
-  // Children: (P1:(= (str.++ t1 w1 t2) (str.++ w2 s)),
-  //            P2:(not (= (str.len t1) 0)))
-  // Arguments: (false)
-  // ---------------------
-  // Conclusion: (= t1 (str.++ w3 r))
-  // where
-  //   w1, w2, w3, w4 are words,
-  //   w3 is (pre w2 p),
-  //   w4 is (suf w2 p),
-  //   p = Word::overlap((suf w2 1), w1),
-  //   r = (skolem (suf t1 (str.len w3))).
-  // In other words, w4 is the largest suffix of (suf w2 1) that can contain a
-  // prefix of w1; since t1 is non-empty, w3 must therefore be contained in t1.
-  //
-  // or the reverse form of the above:
-  //
-  // Children: (P1:(= (str.++ t1 w1 t2) (str.++ s w2)),
-  //            P2:(not (= (str.len t2) 0)))
-  // Arguments: (true)
-  // ---------------------
-  // Conclusion: (= t2 (str.++ r w3))
-  // where
-  //   w1, w2, w3, w4 are words,
-  //   w3 is (suf w2 (- (str.len w2) p)),
-  //   w4 is (pre w2 (- (str.len w2) p)),
-  //   p = Word::roverlap((pre w2 (- (str.len w2) 1)), w1),
-  //   r = (skolem (pre t2 (- (str.len t2) (str.len w3)))).
-  // In other words, w4 is the largest prefix of (pre w2 (- (str.len w2) 1))
-  // that can contain a suffix of w1; since t2 is non-empty, w3 must therefore
-  // be contained in t2.
-  CONCAT_CPROP,
-  // ======== String decompose
-  // Children: (P1: (>= (str.len t) n)
-  // Arguments: (false)
-  // ---------------------
-  // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w1) n))
-  // or
-  // Children: (P1: (>= (str.len t) n)
-  // Arguments: (true)
-  // ---------------------
-  // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w2) n))
-  // where
-  //   w1 is (skolem (pre t n))
-  //   w2 is (skolem (suf t n))
-  STRING_DECOMPOSE,
-  // ======== Length positive
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
-  STRING_LENGTH_POS,
-  // ======== Length non-empty
-  // Children: (P1:(not (= t "")))
-  // Arguments: none
-  // ---------------------
-  // Conclusion: (not (= (str.len t) 0))
-  STRING_LENGTH_NON_EMPTY,
-  //======================== Extended functions
-  // ======== Reduction
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (and R (= t w))
-  // where w = strings::StringsPreprocess::reduce(t, R, ...).
-  // In other words, R is the reduction predicate for extended term t, and w is
-  //   (skolem t)
-  // Notice that the free variables of R are w and the free variables of t.
-  STRING_REDUCTION,
-  // ======== Eager Reduction
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: R
-  // where R = strings::TermRegistry::eagerReduce(t).
-  STRING_EAGER_REDUCTION,
-  //======================== Regular expressions
-  // ======== Regular expression intersection
-  // Children: (P:(str.in.re t R1), P:(str.in.re t R2))
-  // Arguments: none
-  // ---------------------
-  // Conclusion: (str.in.re t (re.inter R1 R2)).
-  RE_INTER,
-  // ======== Regular expression unfold positive
-  // Children: (P:(str.in.re t R))
-  // Arguments: none
-  // ---------------------
-  // Conclusion:(RegExpOpr::reduceRegExpPos((str.in.re t R))),
-  // corresponding to the one-step unfolding of the premise.
-  RE_UNFOLD_POS,
-  // ======== Regular expression unfold negative
-  // Children: (P:(not (str.in.re t R)))
-  // Arguments: none
-  // ---------------------
-  // Conclusion:(RegExpOpr::reduceRegExpNeg((not (str.in.re t R)))),
-  // corresponding to the one-step unfolding of the premise.
-  RE_UNFOLD_NEG,
-  // ======== Regular expression unfold negative concat fixed
-  // Children: (P:(not (str.in.re t R)))
-  // Arguments: none
-  // ---------------------
-  // Conclusion:(RegExpOpr::reduceRegExpNegConcatFixed((not (str.in.re t
-  // R)),L,i)) where RegExpOpr::getRegExpConcatFixed((not (str.in.re t R)), i) =
-  // L. corresponding to the one-step unfolding of the premise, optimized for
-  // fixed length of component i of the regular expression concatenation R.
-  RE_UNFOLD_NEG_CONCAT_FIXED,
-  // ======== Regular expression elimination
-  // Children: none
-  // Arguments: (F, b)
-  // ---------------------
-  // Conclusion: (= F strings::RegExpElimination::eliminate(F, b))
-  // where b is a Boolean indicating whether we are using aggressive
-  // eliminations. Notice this rule concludes (= F F) if no eliminations
-  // are performed for F.
-  RE_ELIM,
-  //======================== Code points
-  // Children: none
-  // Arguments: (t, s)
-  // ---------------------
-  // Conclusion:(or (= (str.code t) (- 1))
-  //                (not (= (str.code t) (str.code s)))
-  //                (not (= t s)))
-  STRING_CODE_INJ,
-  //======================== Sequence unit
-  // Children: (P:(= (seq.unit x) (seq.unit y)))
-  // Arguments: none
-  // ---------------------
-  // Conclusion:(= x y)
-  // Also applies to the case where (seq.unit y) is a constant sequence
-  // of length one.
-  STRING_SEQ_UNIT_INJ,
-  // ======== String Trust
-  // Children: none
-  // Arguments: (Q)
-  // ---------------------
-  // Conclusion: (Q)
-  STRING_TRUST,
-
-  //================================================= Arithmetic rules
-  // ======== Adding Inequalities
-  // Note: an ArithLiteral is a term of the form (>< poly const)
-  // where
-  //   >< is >=, >, ==, <, <=, or not(== ...).
-  //   poly is a polynomial
-  //   const is a rational constant
-
-  // Children: (P1:l1, ..., Pn:ln)
-  //           where each li is an ArithLiteral
-  //           not(= ...) is dis-allowed!
-  //
-  // Arguments: (k1, ..., kn), non-zero reals
-  // ---------------------
-  // Conclusion: (>< t1 t2)
-  //    where >< is the fusion of the combination of the ><i, (flipping each it
-  //    its ki is negative). >< is always one of <, <=
-  //    NB: this implies that lower bounds must have negative ki,
-  //                      and upper bounds must have positive ki.
-  //    t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n *
-  //    poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n
-  //    * const_n)
-  MACRO_ARITH_SCALE_SUM_UB,
-  // ======== Sum Upper Bounds
-  // Children: (P1, ... , Pn)
-  //           where each Pi has form (><i, Li, Ri)
-  //           for ><i in {<, <=, ==}
-  // Conclusion: (>< L R)
-  //           where >< is < if any ><i is <, and <= otherwise.
-  //                 L is (+ L1 ... Ln)
-  //                 R is (+ R1 ... Rn)
-  ARITH_SUM_UB,
-  // ======== Tightening Strict Integer Upper Bounds
-  // Children: (P:(< i c))
-  //         where i has integer type.
-  // Arguments: none
-  // ---------------------
-  // Conclusion: (<= i greatestIntLessThan(c)})
-  INT_TIGHT_UB,
-  // ======== Tightening Strict Integer Lower Bounds
-  // Children: (P:(> i c))
-  //         where i has integer type.
-  // Arguments: none
-  // ---------------------
-  // Conclusion: (>= i leastIntGreaterThan(c)})
-  INT_TIGHT_LB,
-  // ======== Trichotomy of the reals
-  // Children: (A B)
-  // Arguments: (C)
-  // ---------------------
-  // Conclusion: (C),
-  //                 where (not A) (not B) and C
-  //                   are (> x c) (< x c) and (= x c)
-  //                   in some order
-  //                 note that "not" here denotes arithmetic negation, flipping
-  //                 >= to <, etc.
-  ARITH_TRICHOTOMY,
-  // ======== Arithmetic operator elimination
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: arith::OperatorElim::getAxiomFor(t)
-  ARITH_OP_ELIM_AXIOM,
-  // ======== Int Trust
-  // Children: (P1 ... Pn)
-  // Arguments: (Q)
-  // ---------------------
-  // Conclusion: (Q)
-  INT_TRUST,
-
-  //======== Multiplication sign inference
-  // Children: none
-  // Arguments: (f1, ..., fk, m)
-  // ---------------------
-  // Conclusion: (=> (and f1 ... fk) (~ m 0))
-  // Where f1, ..., fk are variables compared to zero (less, greater or not
-  // equal), m is a monomial from these variables, and ~ is the comparison (less
-  // or greater) that results from the signs of the variables. All variables
-  // with even exponent in m should be given as not equal to zero while all
-  // variables with odd exponent in m should be given as less or greater than
-  // zero.
-  ARITH_MULT_SIGN,
-  //======== Multiplication with positive factor
-  // Children: none
-  // Arguments: (m, (rel lhs rhs))
-  // ---------------------
-  // Conclusion: (=> (and (> m 0) (rel lhs rhs)) (rel (* m lhs) (* m rhs)))
-  // Where rel is a relation symbol.
-  ARITH_MULT_POS,
-  //======== Multiplication with negative factor
-  // Children: none
-  // Arguments: (m, (rel lhs rhs))
-  // ---------------------
-  // Conclusion: (=> (and (< m 0) (rel lhs rhs)) (rel_inv (* m lhs) (* m rhs)))
-  // Where rel is a relation symbol and rel_inv the inverted relation symbol.
-  ARITH_MULT_NEG,
-  //======== Multiplication tangent plane
-  // Children: none
-  // Arguments: (t, x, y, a, b, sgn)
-  // ---------------------
-  // Conclusion:
-  //   sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y
-  //   b))) sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a)
-  //   (>= y b)))
-  // Where x,y are real terms (variables or extended terms), t = (* x y)
-  // (possibly under rewriting), a,b are real constants, and sgn is either -1
-  // or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b
-  ARITH_MULT_TANGENT,
-
-  // ================ Lemmas for transcendentals
-  //======== Assert bounds on PI
-  // Children: none
-  // Arguments: (l, u)
-  // ---------------------
-  // Conclusion: (and (>= real.pi l) (<= real.pi u))
-  // Where l (u) is a valid lower (upper) bound on pi.
-  ARITH_TRANS_PI,
-  //======== Exp at negative values
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (= (< t 0) (< (exp t) 1))
-  ARITH_TRANS_EXP_NEG,
-  //======== Exp is always positive
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (> (exp t) 0)
-  ARITH_TRANS_EXP_POSITIVITY,
-  //======== Exp grows super-linearly for positive values
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (or (<= t 0) (> exp(t) (+ t 1)))
-  ARITH_TRANS_EXP_SUPER_LIN,
-  //======== Exp at zero
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (= (= t 0) (= (exp t) 1))
-  ARITH_TRANS_EXP_ZERO,
-  //======== Exp is approximated from above for negative values
-  // Children: none
-  // Arguments: (d, t, l, u)
-  // ---------------------
-  // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant exp l u t))
-  // Where d is an even positive number, t an arithmetic term and l (u) a lower
-  // (upper) bound on t. Let p be the d'th taylor polynomial at zero (also
-  // called the Maclaurin series) of the exponential function. (secant exp l u
-  // t) denotes the secant of p from (l, exp(l)) to (u, exp(u)) evaluated at t,
-  // calculated as follows:
-  //    (p(l) - p(u)) / (l - u) * (t - l) + p(l)
-  // The lemma states that if t is between l and u, then (exp t) is below the
-  // secant of p from l to u.
-  ARITH_TRANS_EXP_APPROX_ABOVE_NEG,
-  //======== Exp is approximated from above for positive values
-  // Children: none
-  // Arguments: (d, t, l, u)
-  // ---------------------
-  // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant-pos exp l u t))
-  // Where d is an even positive number, t an arithmetic term and l (u) a lower
-  // (upper) bound on t. Let p* be a modification of the d'th taylor polynomial
-  // at zero (also called the Maclaurin series) of the exponential function as
-  // follows where p(d-1) is the regular Maclaurin series of degree d-1:
-  //    p* = p(d-1) * (1 + t^n / n!)
-  // (secant-pos exp l u t) denotes the secant of p from (l, exp(l)) to (u,
-  // exp(u)) evaluated at t, calculated as follows:
-  //    (p(l) - p(u)) / (l - u) * (t - l) + p(l)
-  // The lemma states that if t is between l and u, then (exp t) is below the
-  // secant of p from l to u.
-  ARITH_TRANS_EXP_APPROX_ABOVE_POS,
-  //======== Exp is approximated from below
-  // Children: none
-  // Arguments: (d, t)
-  // ---------------------
-  // Conclusion: (>= (exp t) (maclaurin exp d t))
-  // Where d is an odd positive number and (maclaurin exp d t) is the d'th
-  // taylor polynomial at zero (also called the Maclaurin series) of the
-  // exponential function evaluated at t. The Maclaurin series for the
-  // exponential function is the following:
-  //   e^x = \sum_{n=0}^{\infty} x^n / n!
-  ARITH_TRANS_EXP_APPROX_BELOW,
-  //======== Sine is always between -1 and 1
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (and (<= (sin t) 1) (>= (sin t) (- 1)))
-  ARITH_TRANS_SINE_BOUNDS,
-  //======== Sine arg shifted to -pi..pi
-  // Children: none
-  // Arguments: (x, y, s)
-  // ---------------------
-  // Conclusion: (and
-  //   (<= -pi y pi)
-  //   (= (sin y) (sin x))
-  //   (ite (<= -pi x pi) (= x y) (= x (+ y (* 2 pi s))))
-  // )
-  // Where x is the argument to sine, y is a new real skolem that is x shifted
-  // into -pi..pi and s is a new integer skolem that is the number of phases y
-  // is shifted.
-  ARITH_TRANS_SINE_SHIFT,
-  //======== Sine is symmetric with respect to negation of the argument
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (= (- (sin t) (sin (- t))) 0)
-  ARITH_TRANS_SINE_SYMMETRY,
-  //======== Sine is bounded by the tangent at zero
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (and
-  //   (=> (> t 0) (< (sin t) t))
-  //   (=> (< t 0) (> (sin t) t))
-  // )
-  ARITH_TRANS_SINE_TANGENT_ZERO,
-  //======== Sine is bounded by the tangents at -pi and pi
-  // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (and
-  //   (=> (> t -pi) (> (sin t) (- -pi t)))
-  //   (=> (< t pi) (< (sin t) (- pi t)))
-  // )
-  ARITH_TRANS_SINE_TANGENT_PI,
-  //======== Sine is approximated from above for negative values
-  // Children: none
-  // Arguments: (d, t, lb, ub, l, u)
-  // ---------------------
-  // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (secant sin l u t))
-  // Where d is an even positive number, t an arithmetic term, lb (ub) a
-  // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the
-  // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at
-  // zero (also called the Maclaurin series) of the sine function. (secant sin l
-  // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at
-  // t, calculated as follows:
-  //    (p(l) - p(u)) / (l - u) * (t - l) + p(l)
-  // The lemma states that if t is between l and u, then (sin t) is below the
-  // secant of p from l to u.
-  ARITH_TRANS_SINE_APPROX_ABOVE_NEG,
-  //======== Sine is approximated from above for positive values
-  // Children: none
-  // Arguments: (d, t, c, lb, ub)
-  // ---------------------
-  // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (upper sin c))
-  // Where d is an even positive number, t an arithmetic term, c an arithmetic
-  // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly
-  // containing pi). Let p be the d'th taylor polynomial at zero (also called
-  // the Maclaurin series) of the sine function. (upper sin c) denotes the upper
-  // bound on sin(c) given by p and lb,ub are such that sin(t) is the maximum of
-  // the sine function on (lb,ub).
-  ARITH_TRANS_SINE_APPROX_ABOVE_POS,
-  //======== Sine is approximated from below for negative values
-  // Children: none
-  // Arguments: (d, t, c, lb, ub)
-  // ---------------------
-  // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (lower sin c))
-  // Where d is an even positive number, t an arithmetic term, c an arithmetic
-  // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly
-  // containing pi). Let p be the d'th taylor polynomial at zero (also called
-  // the Maclaurin series) of the sine function. (lower sin c) denotes the lower
-  // bound on sin(c) given by p and lb,ub are such that sin(t) is the minimum of
-  // the sine function on (lb,ub).
-  ARITH_TRANS_SINE_APPROX_BELOW_NEG,
-  //======== Sine is approximated from below for positive values
-  // Children: none
-  // Arguments: (d, t, lb, ub, l, u)
-  // ---------------------
-  // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (secant sin l u t))
-  // Where d is an even positive number, t an arithmetic term, lb (ub) a
-  // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the
-  // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at
-  // zero (also called the Maclaurin series) of the sine function. (secant sin l
-  // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at
-  // t, calculated as follows:
-  //    (p(l) - p(u)) / (l - u) * (t - l) + p(l)
-  // The lemma states that if t is between l and u, then (sin t) is above the
-  // secant of p from l to u.
-  ARITH_TRANS_SINE_APPROX_BELOW_POS,
-
-  // ================ CAD Lemmas
-  // We use IRP for IndexedRootPredicate.
-  //
-  // A formula "Interval" describes that a variable (xn is none is given) is
-  // within a particular interval whose bounds are given as IRPs. It is either
-  // an open interval or a point interval:
-  //   (IRP k poly) < xn < (IRP k poly)
-  //   xn == (IRP k poly)
-  //
-  // A formula "Cell" describes a portion
-  // of the real space in the following form:
-  //   Interval(x1) and Interval(x2) and ...
-  // We implicitly assume a Cell to go up to n-1 (and can be empty).
-  //
-  // A formula "Covering" is a set of Intervals, implying that xn can be in
-  // neither of these intervals. To be a covering (of the real line), the union
-  // of these intervals should be the real numbers.
-  // ======== CAD direct conflict
-  // Children (Cell, A)
-  // ---------------------
-  // Conclusion: (false)
-  // A direct interval is generated from an assumption A (in variables x1...xn)
-  // over a Cell (in variables x1...xn). It derives that A evaluates to false
-  // over the Cell. In the actual algorithm, it means that xn can not be in the
-  // topmost interval of the Cell.
-  ARITH_NL_CAD_DIRECT,
-  // ======== CAD recursive interval
-  // Children (Cell, Covering)
-  // ---------------------
-  // Conclusion: (false)
-  // A recursive interval is generated from a Covering (for xn) over a Cell
-  // (in variables x1...xn-1). It generates the conclusion that no xn exists
-  // that extends the Cell and satisfies all assumptions.
-  ARITH_NL_CAD_RECURSIVE,
-
-  //================================================= Unknown rule
-  UNKNOWN,
-};
-
-/**
- * Converts a proof rule to a string. Note: This function is also used in
- * `safe_print()`. Changing this function name or signature will result in
- * `safe_print()` printing "<unsupported>" instead of the proper strings for
- * the enum values.
- *
- * @param id The proof rule
- * @return The name of the proof rule
- */
-const char* toString(PfRule id);
-
-/**
- * Writes a proof rule name to a stream.
- *
- * @param out The stream to write to
- * @param id The proof rule to write to the stream
- * @return The stream
- */
-std::ostream& operator<<(std::ostream& out, PfRule id);
-
-/** Hash function for proof rules */
-struct PfRuleHashFunction
-{
-  size_t operator()(PfRule id) const;
-}; /* struct PfRuleHashFunction */
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__PROOF_RULE_H */
diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h
deleted file mode 100644
index 5ea9c1021..000000000
--- a/src/expr/proof_set.h
+++ /dev/null
@@ -1,76 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Gereon Kremer, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Proof set utility.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_SET_H
-#define CVC5__EXPR__PROOF_SET_H
-
-#include <memory>
-
-#include "context/cdlist.h"
-#include "context/context.h"
-#include "expr/proof_node_manager.h"
-
-namespace cvc5 {
-
-/**
- * A (context-dependent) set of proofs, which is used for memory
- * management purposes.
- */
-template <typename T>
-class CDProofSet
-{
- public:
-  CDProofSet(ProofNodeManager* pnm,
-             context::Context* c,
-             std::string namePrefix = "Proof")
-      : d_pnm(pnm), d_proofs(c), d_namePrefix(namePrefix)
-  {
-  }
-  /**
-   * Allocate a new proof.
-   *
-   * This returns a fresh proof object that remains alive in the context given
-   * to this class. Internally, this adds a new proof of type T to a
-   * context-dependent list of proofs and passes the following arguments to the
-   * T constructor:
-   *   pnm, args..., name
-   * where pnm is the proof node manager
-   * provided to this proof set upon construction, args... are the arguments to
-   * allocateProof() and name is the namePrefix with an appended index.
-   */
-  template <typename... Args>
-  T* allocateProof(Args&&... args)
-  {
-    d_proofs.push_back(std::make_shared<T>(
-        d_pnm,
-        std::forward<Args>(args)...,
-        d_namePrefix + "_" + std::to_string(d_proofs.size())));
-    return d_proofs.back().get();
-  }
-
- protected:
-  /** The proof node manager */
-  ProofNodeManager* d_pnm;
-  /** A context-dependent list of lazy proofs. */
-  context::CDList<std::shared_ptr<T>> d_proofs;
-  /** The name prefix of the lazy proofs */
-  std::string d_namePrefix;
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__LAZY_PROOF_SET_H */
diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp
deleted file mode 100644
index 84cfc040c..000000000
--- a/src/expr/proof_step_buffer.cpp
+++ /dev/null
@@ -1,112 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of proof step and proof step buffer utilities.
- */
-
-#include "expr/proof_step_buffer.h"
-
-#include "expr/proof_checker.h"
-
-using namespace cvc5::kind;
-
-namespace cvc5 {
-
-ProofStep::ProofStep() : d_rule(PfRule::UNKNOWN) {}
-ProofStep::ProofStep(PfRule r,
-                     const std::vector<Node>& children,
-                     const std::vector<Node>& args)
-    : d_rule(r), d_children(children), d_args(args)
-{
-}
-std::ostream& operator<<(std::ostream& out, ProofStep step)
-{
-  out << "(step " << step.d_rule;
-  for (const Node& c : step.d_children)
-  {
-    out << " " << c;
-  }
-  if (!step.d_args.empty())
-  {
-    out << " :args";
-    for (const Node& a : step.d_args)
-    {
-      out << " " << a;
-    }
-  }
-  out << ")";
-  return out;
-}
-
-ProofStepBuffer::ProofStepBuffer(ProofChecker* pc) : d_checker(pc) {}
-
-Node ProofStepBuffer::tryStep(PfRule id,
-                              const std::vector<Node>& children,
-                              const std::vector<Node>& args,
-                              Node expected)
-{
-  if (d_checker == nullptr)
-  {
-    Assert(false) << "ProofStepBuffer::ProofStepBuffer: no proof checker.";
-    return Node::null();
-  }
-  Node res =
-      d_checker->checkDebug(id, children, args, expected, "pf-step-buffer");
-  if (!res.isNull())
-  {
-    // add proof step
-    d_steps.push_back(
-        std::pair<Node, ProofStep>(res, ProofStep(id, children, args)));
-  }
-  return res;
-}
-
-void ProofStepBuffer::addStep(PfRule id,
-                              const std::vector<Node>& children,
-                              const std::vector<Node>& args,
-                              Node expected)
-{
-  d_steps.push_back(
-      std::pair<Node, ProofStep>(expected, ProofStep(id, children, args)));
-}
-
-void ProofStepBuffer::addSteps(ProofStepBuffer& psb)
-{
-  const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
-  for (const std::pair<Node, ProofStep>& step : steps)
-  {
-    addStep(step.second.d_rule,
-            step.second.d_children,
-            step.second.d_args,
-            step.first);
-  }
-}
-
-void ProofStepBuffer::popStep()
-{
-  Assert(!d_steps.empty());
-  if (!d_steps.empty())
-  {
-    d_steps.pop_back();
-  }
-}
-
-size_t ProofStepBuffer::getNumSteps() const { return d_steps.size(); }
-
-const std::vector<std::pair<Node, ProofStep>>& ProofStepBuffer::getSteps() const
-{
-  return d_steps;
-}
-
-void ProofStepBuffer::clear() { d_steps.clear(); }
-
-}  // namespace cvc5
diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h
deleted file mode 100644
index b9350cf45..000000000
--- a/src/expr/proof_step_buffer.h
+++ /dev/null
@@ -1,98 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Proof step and proof step buffer utilities.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_STEP_BUFFER_H
-#define CVC5__EXPR__PROOF_STEP_BUFFER_H
-
-#include <vector>
-
-#include "expr/node.h"
-#include "expr/proof_rule.h"
-
-namespace cvc5 {
-
-class ProofChecker;
-
-/**
- * Information for constructing a step in a CDProof. Notice that the conclusion
- * of the proof step is intentionally not included in this data structure.
- * Instead, it is intended that conclusions may be associated with proof steps
- * based on e.g. the result of proof checking.
- */
-class ProofStep
-{
- public:
-  ProofStep();
-  ProofStep(PfRule r,
-            const std::vector<Node>& children,
-            const std::vector<Node>& args);
-  /** The proof rule */
-  PfRule d_rule;
-  /** The proof children */
-  std::vector<Node> d_children;
-  /** The proof arguments */
-  std::vector<Node> d_args;
-};
-std::ostream& operator<<(std::ostream& out, ProofStep step);
-
-/**
- * Class used to speculatively try and buffer a set of proof steps before
- * sending them to a proof object.
- */
-class ProofStepBuffer
-{
- public:
-  ProofStepBuffer(ProofChecker* pc = nullptr);
-  ~ProofStepBuffer() {}
-  /**
-   * Returns the conclusion of the proof step, as determined by the proof
-   * checker of the given proof. If this is non-null, then the given step
-   * is added to the buffer maintained by this class.
-   *
-   * If expected is non-null, then this method returns null if the result of
-   * checking is not equal to expected.
-   */
-  Node tryStep(PfRule id,
-               const std::vector<Node>& children,
-               const std::vector<Node>& args,
-               Node expected = Node::null());
-  /** Same as above, without checking */
-  void addStep(PfRule id,
-               const std::vector<Node>& children,
-               const std::vector<Node>& args,
-               Node expected);
-  /** Multi-step version */
-  void addSteps(ProofStepBuffer& psb);
-  /** pop step */
-  void popStep();
-  /** Get num steps */
-  size_t getNumSteps() const;
-  /** Get steps */
-  const std::vector<std::pair<Node, ProofStep>>& getSteps() const;
-  /** Clear */
-  void clear();
-
- private:
-  /** The proof checker*/
-  ProofChecker* d_checker;
-  /** the queued proof steps */
-  std::vector<std::pair<Node, ProofStep>> d_steps;
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__PROOF_STEP_BUFFER_H */
diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp
deleted file mode 100644
index 00e961628..000000000
--- a/src/expr/tconv_seq_proof_generator.cpp
+++ /dev/null
@@ -1,172 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Term conversion sequence proof generator utility.
- */
-
-#include "expr/tconv_seq_proof_generator.h"
-
-#include <sstream>
-
-#include "expr/proof_node_manager.h"
-
-namespace cvc5 {
-
-TConvSeqProofGenerator::TConvSeqProofGenerator(
-    ProofNodeManager* pnm,
-    const std::vector<ProofGenerator*>& ts,
-    context::Context* c,
-    std::string name)
-    : d_pnm(pnm), d_converted(c), d_name(name)
-{
-  d_tconvs.insert(d_tconvs.end(), ts.begin(), ts.end());
-  AlwaysAssert(!d_tconvs.empty())
-      << "TConvSeqProofGenerator::TConvSeqProofGenerator: expecting non-empty "
-         "sequence";
-}
-
-TConvSeqProofGenerator::~TConvSeqProofGenerator() {}
-
-void TConvSeqProofGenerator::registerConvertedTerm(Node t, Node s, size_t index)
-{
-  if (t == s)
-  {
-    // no need
-    return;
-  }
-  std::pair<Node, size_t> key = std::pair<Node, size_t>(t, index);
-  d_converted[key] = s;
-}
-
-std::shared_ptr<ProofNode> TConvSeqProofGenerator::getProofFor(Node f)
-{
-  Trace("tconv-seq-pf-gen")
-      << "TConvSeqProofGenerator::getProofFor: " << identify() << ": " << f
-      << std::endl;
-  return getSubsequenceProofFor(f, 0, d_tconvs.size() - 1);
-}
-
-std::shared_ptr<ProofNode> TConvSeqProofGenerator::getSubsequenceProofFor(
-    Node f, size_t start, size_t end)
-{
-  Assert(end < d_tconvs.size());
-  if (f.getKind() != kind::EQUAL)
-  {
-    std::stringstream serr;
-    serr << "TConvSeqProofGenerator::getProofFor: " << identify()
-         << ": fail, non-equality " << f;
-    Unhandled() << serr.str();
-    Trace("tconv-seq-pf-gen") << serr.str() << std::endl;
-    return nullptr;
-  }
-  // start with the left hand side of the equality
-  Node curr = f[0];
-  // proofs forming transitivity chain
-  std::vector<std::shared_ptr<ProofNode>> transChildren;
-  std::pair<Node, size_t> currKey;
-  NodeIndexNodeMap::iterator itc;
-  // convert the term in sequence
-  for (size_t i = start; i <= end; i++)
-  {
-    currKey = std::pair<Node, size_t>(curr, i);
-    itc = d_converted.find(currKey);
-    // if we provided a conversion at this index via registerConvertedTerm
-    if (itc != d_converted.end())
-    {
-      Node next = (*itc).second;
-      Trace("tconv-seq-pf-gen") << "...convert to " << next << std::endl;
-      Node eq = curr.eqNode(next);
-      std::shared_ptr<ProofNode> pf = d_tconvs[i]->getProofFor(eq);
-      transChildren.push_back(pf);
-      curr = next;
-    }
-  }
-  // should end up with the right hand side of the equality
-  if (curr != f[1])
-  {
-    // unexpected
-    std::stringstream serr;
-    serr << "TConvSeqProofGenerator::getProofFor: " << identify()
-         << ": failed, mismatch (see -t tconv-seq-pf-gen-debug for details)"
-         << std::endl;
-    serr << "                    source: " << f[0] << std::endl;
-    serr << "expected after conversions: " << f[1] << std::endl;
-    serr << "  actual after conversions: " << curr << std::endl;
-
-    if (Trace.isOn("tconv-seq-pf-gen-debug"))
-    {
-      Trace("tconv-pf-gen-debug")
-          << "Printing conversion steps..." << std::endl;
-      serr << "Conversions: " << std::endl;
-      for (NodeIndexNodeMap::const_iterator it = d_converted.begin();
-           it != d_converted.end();
-           ++it)
-      {
-        serr << "(" << (*it).first.first << ", " << (*it).first.second
-             << ") -> " << (*it).second << std::endl;
-      }
-    }
-    Unhandled() << serr.str();
-    return nullptr;
-  }
-  // otherwise, make transitivity
-  return d_pnm->mkTrans(transChildren, f);
-}
-
-theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
-    const std::vector<Node>& cterms)
-{
-  Assert(cterms.size() == d_tconvs.size() + 1);
-  if (cterms[0] == cterms[cterms.size() - 1])
-  {
-    return theory::TrustNode::null();
-  }
-  bool useThis = false;
-  ProofGenerator* pg = nullptr;
-  for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++)
-  {
-    if (cterms[i] == cterms[i + 1])
-    {
-      continue;
-    }
-    else if (pg == nullptr)
-    {
-      // Maybe the i^th generator can explain it alone, which must be the case
-      // if there is only one position in the sequence where the term changes.
-      // We may overwrite pg with this class if another step is encountered in
-      // this loop.
-      pg = d_tconvs[i];
-    }
-    else
-    {
-      // need more than a single generator, use this class
-      useThis = true;
-      break;
-    }
-  }
-  if (useThis)
-  {
-    pg = this;
-    // if more than two steps, we must register each conversion step
-    for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++)
-    {
-      registerConvertedTerm(cterms[i], cterms[i + 1], i);
-    }
-  }
-  Assert(pg != nullptr);
-  return theory::TrustNode::mkTrustRewrite(
-      cterms[0], cterms[cterms.size() - 1], pg);
-}
-
-std::string TConvSeqProofGenerator::identify() const { return d_name; }
-
-}  // namespace cvc5
diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h
deleted file mode 100644
index bc067f60a..000000000
--- a/src/expr/tconv_seq_proof_generator.h
+++ /dev/null
@@ -1,121 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Term conversion sequence proof generator utility.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H
-#define CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H
-
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-#include "expr/proof_generator.h"
-#include "theory/trust_node.h"
-
-namespace cvc5 {
-
-class ProofNodeManager;
-
-/**
- * The term conversion sequence proof generator. This is used for maintaining
- * a fixed sequence of proof generators that provide proofs for rewrites
- * (equalities). We call these the "component generators" of this sequence,
- * which are typically TConvProofGenerator.
- */
-class TConvSeqProofGenerator : public ProofGenerator
-{
- public:
-  /**
-   * @param pnm The proof node manager for constructing ProofNode objects.
-   * @param ts The list of component term conversion generators that are
-   * applied in sequence
-   * @param c The context that this class depends on. If none is provided,
-   * this class is context-independent.
-   * @param name The name of this generator (for debugging).
-   */
-  TConvSeqProofGenerator(ProofNodeManager* pnm,
-                         const std::vector<ProofGenerator*>& ts,
-                         context::Context* c = nullptr,
-                         std::string name = "TConvSeqProofGenerator");
-  ~TConvSeqProofGenerator();
-  /**
-   * Indicate that the index^th proof generator converts term t to s. This
-   * should be called for a unique s for each (t, index). It must be the
-   * case that d_tconv[index] can provide a proof for t = s in the remainder
-   * of the context maintained by this class.
-   */
-  void registerConvertedTerm(Node t, Node s, size_t index);
-  /**
-   * Get the proof for formula f. It should be the case that f is of the form
-   * t_0 = t_n, where it must be the case that t_n is obtained by the following:
-   * For each i=0, ... n, let t_{i+1} be the term such that
-   *   registerConvertedTerm(t_i, t_{i+1}, i)
-   * was called. Otherwise t_{i+1} = t_i.
-   * In other words, t_n is obtained by converting t_0, in order, based on the
-   * calls to registerConvertedTerm.
-   *
-   * @param f The equality fact to get the proof for.
-   * @return The proof for f.
-   */
-  std::shared_ptr<ProofNode> getProofFor(Node f) override;
-  /**
-   * Get subsequence proof for f, with given start and end steps (inclusive).
-   */
-  std::shared_ptr<ProofNode> getSubsequenceProofFor(Node f,
-                                                    size_t start,
-                                                    size_t end);
-  /** Identify this generator (for debugging, etc..) */
-  std::string identify() const override;
-
-  /**
-   * Make trust node from a sequence of converted terms. The number of
-   * terms in cterms should be 1 + the number of component proof generators
-   * maintained by this class. This selects a proof generator that is capable
-   * of proving cterms[0] = cterms[cterms.size()-1], which is either this
-   * generator, or one of the component proof generators, if only one step
-   * rewrote. In the former case, all steps are registered to this class.
-   * Using a component generator is an optimization that saves having to
-   * save the conversion steps or use this class. For example, if we have 2 
-   * term conversion components, and call this method on:
-   *   { a, b, c }
-   * then this method calls:
-   *   registerConvertedTerm( a, b, 0 )
-   *   registerConvertedTerm( b, c, 1 )
-   * and returns a trust node proving (= a c) with this class as the proof
-   * generator. On the other hand, if we call this method on:
-   *   { d, d, e }
-   * then we return a trust node proving (= d e) with the 2nd component proof
-   * generator, as it alone is capable of proving this equality.
-   */
-  theory::TrustNode mkTrustRewriteSequence(const std::vector<Node>& cterms);
-
- protected:
-  using NodeIndexPairHashFunction =
-      PairHashFunction<Node, size_t, std::hash<Node>>;
-  typedef context::
-      CDHashMap<std::pair<Node, size_t>, Node, NodeIndexPairHashFunction>
-          NodeIndexNodeMap;
-  /** The proof node manager */
-  ProofNodeManager* d_pnm;
-  /** The term conversion generators */
-  std::vector<ProofGenerator*> d_tconvs;
-  /** the set of converted terms */
-  NodeIndexNodeMap d_converted;
-  /** Name identifier */
-  std::string d_name;
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
deleted file mode 100644
index 0e0ed3165..000000000
--- a/src/expr/term_conversion_proof_generator.cpp
+++ /dev/null
@@ -1,624 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of term conversion proof generator utility.
- */
-
-#include "expr/term_conversion_proof_generator.h"
-
-#include <sstream>
-
-#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_algorithm.h"
-#include "expr/term_context.h"
-#include "expr/term_context_stack.h"
-
-using namespace cvc5::kind;
-
-namespace cvc5 {
-
-std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol)
-{
-  switch (tcpol)
-  {
-    case TConvPolicy::FIXPOINT: out << "FIXPOINT"; break;
-    case TConvPolicy::ONCE: out << "ONCE"; break;
-    default: out << "TConvPolicy:unknown"; break;
-  }
-  return out;
-}
-
-std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol)
-{
-  switch (tcpol)
-  {
-    case TConvCachePolicy::STATIC: out << "STATIC"; break;
-    case TConvCachePolicy::DYNAMIC: out << "DYNAMIC"; break;
-    case TConvCachePolicy::NEVER: out << "NEVER"; break;
-    default: out << "TConvCachePolicy:unknown"; break;
-  }
-  return out;
-}
-
-TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
-                                         context::Context* c,
-                                         TConvPolicy pol,
-                                         TConvCachePolicy cpol,
-                                         std::string name,
-                                         TermContext* tccb,
-                                         bool rewriteOps)
-    : d_proof(pnm, nullptr, c, name + "::LazyCDProof"),
-      d_preRewriteMap(c ? c : &d_context),
-      d_postRewriteMap(c ? c : &d_context),
-      d_policy(pol),
-      d_cpolicy(cpol),
-      d_name(name),
-      d_tcontext(tccb),
-      d_rewriteOps(rewriteOps)
-{
-}
-
-TConvProofGenerator::~TConvProofGenerator() {}
-
-void TConvProofGenerator::addRewriteStep(Node t,
-                                         Node s,
-                                         ProofGenerator* pg,
-                                         bool isPre,
-                                         PfRule trustId,
-                                         bool isClosed,
-                                         uint32_t tctx)
-{
-  Node eq = registerRewriteStep(t, s, tctx, isPre);
-  if (!eq.isNull())
-  {
-    d_proof.addLazyStep(eq, pg, trustId, isClosed);
-  }
-}
-
-void TConvProofGenerator::addRewriteStep(
-    Node t, Node s, ProofStep ps, bool isPre, uint32_t tctx)
-{
-  Node eq = registerRewriteStep(t, s, tctx, isPre);
-  if (!eq.isNull())
-  {
-    d_proof.addStep(eq, ps);
-  }
-}
-
-void TConvProofGenerator::addRewriteStep(Node t,
-                                         Node s,
-                                         PfRule id,
-                                         const std::vector<Node>& children,
-                                         const std::vector<Node>& args,
-                                         bool isPre,
-                                         uint32_t tctx)
-{
-  Node eq = registerRewriteStep(t, s, tctx, isPre);
-  if (!eq.isNull())
-  {
-    d_proof.addStep(eq, id, children, args);
-  }
-}
-
-bool TConvProofGenerator::hasRewriteStep(Node t,
-                                         uint32_t tctx,
-                                         bool isPre) const
-{
-  return !getRewriteStep(t, tctx, isPre).isNull();
-}
-
-Node TConvProofGenerator::getRewriteStep(Node t,
-                                         uint32_t tctx,
-                                         bool isPre) const
-{
-  Node thash = t;
-  if (d_tcontext != nullptr)
-  {
-    thash = TCtxNode::computeNodeHash(t, tctx);
-  }
-  return getRewriteStepInternal(thash, isPre);
-}
-
-Node TConvProofGenerator::registerRewriteStep(Node t,
-                                              Node s,
-                                              uint32_t tctx,
-                                              bool isPre)
-{
-  Assert(!t.isNull());
-  Assert(!s.isNull());
-
-  if (t == s)
-  {
-    return Node::null();
-  }
-  Node thash = t;
-  if (d_tcontext != nullptr)
-  {
-    thash = TCtxNode::computeNodeHash(t, tctx);
-  }
-  else
-  {
-    // don't use term context ids if not using term context
-    Assert(tctx == 0);
-  }
-  // should not rewrite term to two different things
-  if (!getRewriteStepInternal(thash, isPre).isNull())
-  {
-    Assert(getRewriteStepInternal(thash, isPre) == s)
-        << identify() << " rewriting " << t << " to both " << s << " and "
-        << getRewriteStepInternal(thash, isPre);
-    return Node::null();
-  }
-  NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
-  rm[thash] = s;
-  if (d_cpolicy == TConvCachePolicy::DYNAMIC)
-  {
-    // clear the cache
-    d_cache.clear();
-  }
-  return t.eqNode(s);
-}
-
-std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
-{
-  Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << identify()
-                        << ": " << f << std::endl;
-  if (f.getKind() != EQUAL)
-  {
-    std::stringstream serr;
-    serr << "TConvProofGenerator::getProofFor: " << identify()
-         << ": fail, non-equality " << f;
-    Unhandled() << serr.str();
-    Trace("tconv-pf-gen") << serr.str() << std::endl;
-    return nullptr;
-  }
-  // we use the existing proofs
-  LazyCDProof lpf(
-      d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProof");
-  if (f[0] == f[1])
-  {
-    // assertion failure in debug
-    Assert(false) << "TConvProofGenerator::getProofFor: " << identify()
-                  << ": don't ask for trivial proofs";
-    lpf.addStep(f, PfRule::REFL, {}, {f[0]});
-  }
-  else
-  {
-    Node conc = getProofForRewriting(f[0], lpf, d_tcontext);
-    if (conc != f)
-    {
-      bool debugTraceEnabled = Trace.isOn("tconv-pf-gen-debug");
-      Assert(conc.getKind() == EQUAL && conc[0] == f[0]);
-      std::stringstream serr;
-      serr << "TConvProofGenerator::getProofFor: " << toStringDebug()
-           << ": failed, mismatch";
-      if (!debugTraceEnabled)
-      {
-        serr << " (see -t tconv-pf-gen-debug for details)";
-      }
-      serr << std::endl;
-      serr << "                   source: " << f[0] << std::endl;
-      serr << "     requested conclusion: " << f[1] << std::endl;
-      serr << "conclusion from generator: " << conc[1] << std::endl;
-
-      if (debugTraceEnabled)
-      {
-        Trace("tconv-pf-gen-debug") << "Printing rewrite steps..." << std::endl;
-        for (size_t r = 0; r < 2; r++)
-        {
-          const NodeNodeMap& rm = r == 0 ? d_preRewriteMap : d_postRewriteMap;
-          serr << "Rewrite steps (" << (r == 0 ? "pre" : "post")
-               << "):" << std::endl;
-          for (NodeNodeMap::const_iterator it = rm.begin(); it != rm.end();
-               ++it)
-          {
-            serr << (*it).first << " -> " << (*it).second << std::endl;
-          }
-        }
-      }
-      Unhandled() << serr.str();
-      return nullptr;
-    }
-  }
-  std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f);
-  Trace("tconv-pf-gen") << "... success" << std::endl;
-  Assert (pfn!=nullptr);
-  Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl;
-  return pfn;
-}
-
-std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n)
-{
-  LazyCDProof lpf(
-      d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProofRew");
-  Node conc = getProofForRewriting(n, lpf, d_tcontext);
-  if (conc[1] == n)
-  {
-    // assertion failure in debug
-    Assert(false) << "TConvProofGenerator::getProofForRewriting: " << identify()
-                  << ": don't ask for trivial proofs";
-    lpf.addStep(conc, PfRule::REFL, {}, {n});
-  }
-  std::shared_ptr<ProofNode> pfn = lpf.getProofFor(conc);
-  Assert(pfn != nullptr);
-  Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl;
-  return pfn;
-}
-
-Node TConvProofGenerator::getProofForRewriting(Node t,
-                                               LazyCDProof& pf,
-                                               TermContext* tctx)
-{
-  NodeManager* nm = NodeManager::currentNM();
-  // Invariant: if visited[hash(t)] = s or rewritten[hash(t)] = s and t,s are
-  // distinct, then pf is able to generate a proof of t=s. We must
-  // Node in the domains of the maps below due to hashing creating new (SEXPR)
-  // nodes.
-
-  // the final rewritten form of terms
-  std::unordered_map<Node, Node> visited;
-  // the rewritten form of terms we have processed so far
-  std::unordered_map<Node, Node> rewritten;
-  std::unordered_map<Node, Node>::iterator it;
-  std::unordered_map<Node, Node>::iterator itr;
-  std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
-  Trace("tconv-pf-gen-rewrite")
-      << "TConvProofGenerator::getProofForRewriting: " << toStringDebug()
-      << std::endl;
-  Trace("tconv-pf-gen-rewrite") << "Input: " << t << std::endl;
-  // if provided, we use term context for cache
-  std::shared_ptr<TCtxStack> visitctx;
-  // otherwise, visit is used if we don't have a term context
-  std::vector<TNode> visit;
-  Node tinitialHash;
-  if (tctx != nullptr)
-  {
-    visitctx = std::make_shared<TCtxStack>(tctx);
-    visitctx->pushInitial(t);
-    tinitialHash = TCtxNode::computeNodeHash(t, tctx->initialValue());
-  }
-  else
-  {
-    visit.push_back(t);
-    tinitialHash = t;
-  }
-  Node cur;
-  uint32_t curCVal = 0;
-  Node curHash;
-  do
-  {
-    // pop the top element
-    if (tctx != nullptr)
-    {
-      std::pair<Node, uint32_t> curPair = visitctx->getCurrent();
-      cur = curPair.first;
-      curCVal = curPair.second;
-      curHash = TCtxNode::computeNodeHash(cur, curCVal);
-      visitctx->pop();
-    }
-    else
-    {
-      cur = visit.back();
-      curHash = cur;
-      visit.pop_back();
-    }
-    Trace("tconv-pf-gen-rewrite") << "* visit : " << curHash << std::endl;
-    // has the proof for cur been cached?
-    itc = d_cache.find(curHash);
-    if (itc != d_cache.end())
-    {
-      Node res = itc->second->getResult();
-      Assert(res.getKind() == EQUAL);
-      Assert(!res[1].isNull());
-      visited[curHash] = res[1];
-      pf.addProof(itc->second);
-      continue;
-    }
-    it = visited.find(curHash);
-    if (it == visited.end())
-    {
-      Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl;
-      visited[curHash] = Node::null();
-      // did we rewrite the current node (at pre-rewrite)?
-      Node rcur = getRewriteStepInternal(curHash, true);
-      if (!rcur.isNull())
-      {
-        Trace("tconv-pf-gen-rewrite")
-            << "*** " << curHash << " prerewrites to " << rcur << std::endl;
-        // d_proof has a proof of cur = rcur. Hence there is nothing
-        // to do here, as pf will reference d_proof to get its proof.
-        if (d_policy == TConvPolicy::FIXPOINT)
-        {
-          // It may be the case that rcur also rewrites, thus we cannot assign
-          // the final rewritten form for cur yet. Instead we revisit cur after
-          // finishing visiting rcur.
-          rewritten[curHash] = rcur;
-          if (tctx != nullptr)
-          {
-            visitctx->push(cur, curCVal);
-            visitctx->push(rcur, curCVal);
-          }
-          else
-          {
-            visit.push_back(cur);
-            visit.push_back(rcur);
-          }
-        }
-        else
-        {
-          Assert(d_policy == TConvPolicy::ONCE);
-          Trace("tconv-pf-gen-rewrite") << "-> (once, prewrite) " << curHash
-                                        << " = " << rcur << std::endl;
-          // not rewriting again, rcur is final
-          Assert(!rcur.isNull());
-          visited[curHash] = rcur;
-          doCache(curHash, cur, rcur, pf);
-        }
-      }
-      else if (tctx != nullptr)
-      {
-        visitctx->push(cur, curCVal);
-        // visit operator if apply uf
-        if (d_rewriteOps && cur.getKind() == APPLY_UF)
-        {
-          visitctx->pushOp(cur, curCVal);
-        }
-        visitctx->pushChildren(cur, curCVal);
-      }
-      else
-      {
-        visit.push_back(cur);
-        // visit operator if apply uf
-        if (d_rewriteOps && cur.getKind() == APPLY_UF)
-        {
-          visit.push_back(cur.getOperator());
-        }
-        visit.insert(visit.end(), cur.begin(), cur.end());
-      }
-    }
-    else if (it->second.isNull())
-    {
-      itr = rewritten.find(curHash);
-      if (itr != rewritten.end())
-      {
-        // only can generate partially rewritten nodes when rewrite again is
-        // true.
-        Assert(d_policy != TConvPolicy::ONCE);
-        // if it was rewritten, check the status of the rewritten node,
-        // which should be finished now
-        Node rcur = itr->second;
-        Trace("tconv-pf-gen-rewrite")
-            << "- postvisit, previously rewritten to " << rcur << std::endl;
-        Node rcurHash = rcur;
-        if (tctx != nullptr)
-        {
-          rcurHash = TCtxNode::computeNodeHash(rcur, curCVal);
-        }
-        Assert(cur != rcur);
-        // the final rewritten form of cur is the final form of rcur
-        Node rcurFinal = visited[rcurHash];
-        Assert(!rcurFinal.isNull());
-        if (rcurFinal != rcur)
-        {
-          // must connect via TRANS
-          std::vector<Node> pfChildren;
-          pfChildren.push_back(cur.eqNode(rcur));
-          pfChildren.push_back(rcur.eqNode(rcurFinal));
-          Node result = cur.eqNode(rcurFinal);
-          pf.addStep(result, PfRule::TRANS, pfChildren, {});
-        }
-        Trace("tconv-pf-gen-rewrite")
-            << "-> (rewritten postrewrite) " << curHash << " = " << rcurFinal
-            << std::endl;
-        visited[curHash] = rcurFinal;
-        doCache(curHash, cur, rcurFinal, pf);
-      }
-      else
-      {
-        Trace("tconv-pf-gen-rewrite") << "- postvisit" << std::endl;
-        Node ret = cur;
-        Node retHash = curHash;
-        bool childChanged = false;
-        std::vector<Node> children;
-        Kind ck = cur.getKind();
-        if (d_rewriteOps && ck == APPLY_UF)
-        {
-          // the operator of APPLY_UF is visited
-          Node cop = cur.getOperator();
-          if (tctx != nullptr)
-          {
-            uint32_t coval = tctx->computeValueOp(cur, curCVal);
-            Node coHash = TCtxNode::computeNodeHash(cop, coval);
-            it = visited.find(coHash);
-          }
-          else
-          {
-            it = visited.find(cop);
-          }
-          Assert(it != visited.end());
-          Assert(!it->second.isNull());
-          childChanged = childChanged || cop != it->second;
-          children.push_back(it->second);
-        }
-        else if (cur.getMetaKind() == metakind::PARAMETERIZED)
-        {
-          // all other parametrized operators are unchanged
-          children.push_back(cur.getOperator());
-        }
-        // get the results of the children
-        if (tctx != nullptr)
-        {
-          for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
-          {
-            Node cn = cur[i];
-            uint32_t cnval = tctx->computeValue(cur, curCVal, i);
-            Node cnHash = TCtxNode::computeNodeHash(cn, cnval);
-            it = visited.find(cnHash);
-            Assert(it != visited.end());
-            Assert(!it->second.isNull());
-            childChanged = childChanged || cn != it->second;
-            children.push_back(it->second);
-          }
-        }
-        else
-        {
-          // can use simple loop if not term-context-sensitive
-          for (const Node& cn : cur)
-          {
-            it = visited.find(cn);
-            Assert(it != visited.end());
-            Assert(!it->second.isNull());
-            childChanged = childChanged || cn != it->second;
-            children.push_back(it->second);
-          }
-        }
-        if (childChanged)
-        {
-          ret = nm->mkNode(ck, children);
-          rewritten[curHash] = ret;
-          // congruence to show (cur = ret)
-          PfRule congRule = PfRule::CONG;
-          std::vector<Node> pfChildren;
-          std::vector<Node> pfArgs;
-          pfArgs.push_back(ProofRuleChecker::mkKindNode(ck));
-          if (ck == APPLY_UF && children[0] != cur.getOperator())
-          {
-            // use HO_CONG if the operator changed
-            congRule = PfRule::HO_CONG;
-            pfChildren.push_back(cur.getOperator().eqNode(children[0]));
-          }
-          else if (kind::metaKindOf(ck) == kind::metakind::PARAMETERIZED)
-          {
-            pfArgs.push_back(cur.getOperator());
-          }
-          for (size_t i = 0, size = cur.getNumChildren(); i < size; i++)
-          {
-            if (cur[i] == ret[i])
-            {
-              // ensure REFL proof for unchanged children
-              pf.addStep(cur[i].eqNode(cur[i]), PfRule::REFL, {}, {cur[i]});
-            }
-            pfChildren.push_back(cur[i].eqNode(ret[i]));
-          }
-          Node result = cur.eqNode(ret);
-          pf.addStep(result, congRule, pfChildren, pfArgs);
-          // must update the hash
-          retHash = ret;
-          if (tctx != nullptr)
-          {
-            retHash = TCtxNode::computeNodeHash(ret, curCVal);
-          }
-        }
-        else if (tctx != nullptr)
-        {
-          // now we need the hash
-          retHash = TCtxNode::computeNodeHash(cur, curCVal);
-        }
-        // did we rewrite ret (at post-rewrite)?
-        Node rret = getRewriteStepInternal(retHash, false);
-        if (!rret.isNull() && d_policy == TConvPolicy::FIXPOINT)
-        {
-          Trace("tconv-pf-gen-rewrite")
-              << "*** " << retHash << " postrewrites to " << rret << std::endl;
-          // d_proof should have a proof of ret = rret, hence nothing to do
-          // here, for the same reasons as above. It also may be the case that
-          // rret rewrites, hence we must revisit ret.
-          rewritten[retHash] = rret;
-          if (tctx != nullptr)
-          {
-            if (cur != ret)
-            {
-              visitctx->push(cur, curCVal);
-            }
-            visitctx->push(ret, curCVal);
-            visitctx->push(rret, curCVal);
-          }
-          else
-          {
-            if (cur != ret)
-            {
-              visit.push_back(cur);
-            }
-            visit.push_back(ret);
-            visit.push_back(rret);
-          }
-        }
-        else
-        {
-          // If we changed due to congruence, and then rewrote, then we
-          // require a trans step to connect here
-          if (!rret.isNull() && childChanged)
-          {
-            std::vector<Node> pfChildren;
-            pfChildren.push_back(cur.eqNode(ret));
-            pfChildren.push_back(ret.eqNode(rret));
-            Node result = cur.eqNode(rret);
-            pf.addStep(result, PfRule::TRANS, pfChildren, {});
-          }
-          // take its rewrite if it rewrote and we have ONCE rewriting policy
-          ret = rret.isNull() ? ret : rret;
-          Trace("tconv-pf-gen-rewrite")
-              << "-> (postrewrite) " << curHash << " = " << ret << std::endl;
-          // it is final
-          Assert(!ret.isNull());
-          visited[curHash] = ret;
-          doCache(curHash, cur, ret, pf);
-        }
-      }
-    }
-    else
-    {
-      Trace("tconv-pf-gen-rewrite") << "- already visited" << std::endl;
-    }
-  } while (!(tctx != nullptr ? visitctx->empty() : visit.empty()));
-  Assert(visited.find(tinitialHash) != visited.end());
-  Assert(!visited.find(tinitialHash)->second.isNull());
-  Trace("tconv-pf-gen-rewrite")
-      << "...finished, return " << visited[tinitialHash] << std::endl;
-  // return the conclusion of the overall proof
-  return t.eqNode(visited[tinitialHash]);
-}
-
-void TConvProofGenerator::doCache(Node curHash,
-                                  Node cur,
-                                  Node r,
-                                  LazyCDProof& pf)
-{
-  if (d_cpolicy != TConvCachePolicy::NEVER)
-  {
-    Node eq = cur.eqNode(r);
-    d_cache[curHash] = pf.getProofFor(eq);
-  }
-}
-
-Node TConvProofGenerator::getRewriteStepInternal(Node t, bool isPre) const
-{
-  const NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
-  NodeNodeMap::const_iterator it = rm.find(t);
-  if (it == rm.end())
-  {
-    return Node::null();
-  }
-  return (*it).second;
-}
-std::string TConvProofGenerator::identify() const { return d_name; }
-
-std::string TConvProofGenerator::toStringDebug() const
-{
-  std::stringstream ss;
-  ss << identify() << " (policy=" << d_policy << ", cache policy=" << d_cpolicy
-     << (d_tcontext != nullptr ? ", term-context-sensitive" : "") << ")";
-  return ss.str();
-}
-
-}  // namespace cvc5
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
deleted file mode 100644
index 70e606db4..000000000
--- a/src/expr/term_conversion_proof_generator.h
+++ /dev/null
@@ -1,256 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Term conversion proof generator utility.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
-#define CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
-
-#include "context/cdhashmap.h"
-#include "expr/lazy_proof.h"
-#include "expr/proof_generator.h"
-
-namespace cvc5 {
-
-class ProofNodeManager;
-class TermContext;
-
-/** A policy for how rewrite steps are applied in TConvProofGenerator */
-enum class TConvPolicy : uint32_t
-{
-  // steps are applied to fix-point, common use case is PfRule::REWRITE
-  FIXPOINT,
-  // steps are applied once at pre-rewrite, common use case is PfRule::SUBS
-  ONCE,
-};
-/** Writes a term conversion policy name to a stream. */
-std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol);
-
-/** A policy for how proofs are cached in TConvProofGenerator */
-enum class TConvCachePolicy : uint32_t
-{
-  // proofs are statically cached
-  STATIC,
-  // proofs are dynamically cached, cleared when a new rewrite is added
-  DYNAMIC,
-  // proofs are never cached
-  NEVER,
-};
-/** Writes a term conversion cache policy name to a stream. */
-std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol);
-
-/**
- * The term conversion proof generator.
- *
- * This class is used for proofs of t = t', where t' is obtained from t by
- * applying (context-free) small step rewrites on subterms of t. Its main
- * interface functions are:
- * (1) addRewriteStep(t,s,<justification>) which notifies this class that t
- * rewrites to s, where justification is either a proof generator or proof
- * step,
- * (2) getProofFor(f) where f is any equality that can be justified by the
- * rewrite steps given above.
- *
- * For example, say we make the following calls:
- *   addRewriteStep(a,b,P1)
- *   addRewriteStep(f(a),c,P2)
- *   addRewriteStep(c,d,P3)
- * where P1 and P2 are proof steps. Afterwards, this class may justify any
- * equality t = s where s is obtained by applying the rewrites a->b, f(a)->c,
- * c->d, based on the strategy outlined below [***]. For example, the call to:
- *   getProofFor(g(f(a),h(a),f(e)) = g(d,h(b),f(e)))
- * will return the proof:
- *   CONG(
- *     TRANS(P2,P3),     ; f(a)=d
- *     CONG(P1 :args h), ; h(a)=h(b)
- *     REFL(:args f(e))  ; f(e)=f(e)
- *   :args g)
- *
- * [***] This class traverses the left hand side of a given equality-to-prove
- * (the term g(f(a),h(a),e) in the above example) and "replays" the rewrite
- * steps to obtain its rewritten form. To do so, it applies any available
- * rewrite step at pre-rewrite (pre-order traversal) and post-rewrite
- * (post-order traversal) based on whether the user specified pre-rewrite or a
- * post-rewrite during addRewriteStep.
- *
- * This class may additionally be used for term-context-sensitive rewrite
- * systems. An example is the term formula removal pass which rewrites
- * terms dependending on whether they occur in a "term position", for details
- * see RtfTermContext in expr/term_context.h. To use this class in a way
- * that takes into account term contexts, the user of the term conversion
- * proof generator should:
- * (1) Provide a term context callback to the constructor of this class (tccb),
- * (2) Register rewrite steps that indicate the term context identifier of
- * the rewrite, which is a uint32_t.
- *
- * For example, RtfTermContext uses hash value 2 to indicate we are in a "term
- * position". Say the user of this class calls:
- *   addRewriteStep( (and A B), BOOLEAN_TERM_VARIABLE_1, pg, true, 2)
- * This indicates that (and A B) should rewrite to BOOLEAN_TERM_VARIABLE_1 if
- * (and A B) occurs in a term position, where pg is a proof generator that can
- * provide a closed proof of:
- *   (= (and A B) BOOLEAN_TERM_VARIABLE_1)
- * Subsequently, this class may respond to a call to getProofFor on:
- *   (=
- *     (or (and A B) (P (and A B)))
- *     (or (and A B) (P BOOLEAN_TERM_VARIABLE_1)))
- * where P is a predicate Bool -> Bool. The proof returned by this class
- * involves congruence and pg's proof of the equivalence above. In particular,
- * assuming its proof of the equivalence is P1, this proof is:
- *   (CONG{=} (CONG{or} (REFL (and A B)) (CONG{P} P1)))
- * Notice the callback provided to this class ensures that the rewrite is
- * replayed in the expected way, e.g. the occurrence of (and A B) that is not
- * in term position is not rewritten.
- */
-class TConvProofGenerator : public ProofGenerator
-{
- public:
-  /**
-   * Constructor, which notice does fixpoint rewriting (since this is the
-   * most common use case) and never caches.
-   *
-   * @param pnm The proof node manager for constructing ProofNode objects.
-   * @param c The context that this class depends on. If none is provided,
-   * this class is context-independent.
-   * @param tpol The policy for applying rewrite steps of this class. For
-   * details, see d_policy.
-   * @param cpol The caching policy for this generator.
-   * @param name The name of this generator (for debugging).
-   * @param tccb The term context callback that this class depends on. If this
-   * is non-null, then this class stores a term-context-sensitive rewrite
-   * system. The rewrite steps should be given term context identifiers.
-   */
-  TConvProofGenerator(ProofNodeManager* pnm,
-                      context::Context* c = nullptr,
-                      TConvPolicy pol = TConvPolicy::FIXPOINT,
-                      TConvCachePolicy cpol = TConvCachePolicy::NEVER,
-                      std::string name = "TConvProofGenerator",
-                      TermContext* tccb = nullptr,
-                      bool rewriteOps = false);
-  ~TConvProofGenerator();
-  /**
-   * Add rewrite step t --> s based on proof generator.
-   *
-   * @param isPre Whether the rewrite is applied at prerewrite (pre-order
-   * traversal).
-   * @param trustId If a null proof generator is provided, we add a step to
-   * the proof that has trustId as the rule and expected as the sole argument.
-   * @param isClosed whether to expect that pg can provide a closed proof for
-   * this fact.
-   * @param tctx The term context identifier for the rewrite step. This
-   * value should correspond to one generated by the term context callback
-   * class provided in the argument tccb provided to the constructor of this
-   * class.
-   */
-  void addRewriteStep(Node t,
-                      Node s,
-                      ProofGenerator* pg,
-                      bool isPre = false,
-                      PfRule trustId = PfRule::ASSUME,
-                      bool isClosed = false,
-                      uint32_t tctx = 0);
-  /** Same as above, for a single step */
-  void addRewriteStep(
-      Node t, Node s, ProofStep ps, bool isPre = false, uint32_t tctx = 0);
-  /** Same as above, with explicit arguments */
-  void addRewriteStep(Node t,
-                      Node s,
-                      PfRule id,
-                      const std::vector<Node>& children,
-                      const std::vector<Node>& args,
-                      bool isPre = false,
-                      uint32_t tctx = 0);
-  /** Has rewrite step for term t */
-  bool hasRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const;
-  /** 
-   * Get rewrite step for term t, returns the s provided in a call to
-   * addRewriteStep if one exists, or null otherwise.
-   */
-  Node getRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const;
-  /**
-   * Get the proof for formula f. It should be the case that f is of the form
-   * t = t', where t' is the result of rewriting t based on the rewrite steps
-   * registered to this class.
-   *
-   * @param f The equality fact to get the proof for.
-   * @return The proof for f.
-   */
-  std::shared_ptr<ProofNode> getProofFor(Node f) override;
-  /** Identify this generator (for debugging, etc..) */
-  std::string identify() const override;
-  /**
-   * Get the proof for how term n would rewrite. This is in contrast to the
-   * above method where the user provides an equality (= n n'). The motivation
-   * for this method is when it may be expensive to compute n', and hence it
-   * is preferred that the proof checker computes the rewritten form of
-   * n, instead of verifying that n has rewritten form n'.
-   */
-  std::shared_ptr<ProofNode> getProofForRewriting(Node n);
-
- protected:
-  typedef context::CDHashMap<Node, Node> NodeNodeMap;
-  /** A dummy context used by this class if none is provided */
-  context::Context d_context;
-  /** The (lazy) context dependent proof object. */
-  LazyCDProof d_proof;
-  /** map to rewritten forms */
-  NodeNodeMap d_preRewriteMap;
-  NodeNodeMap d_postRewriteMap;
-  /**
-   * Policy for how rewrites are applied to terms. As a simple example, say we
-   * have registered the rewrite steps:
-   *   addRewriteStep( a, f(c), p1 )
-   *   addRewriteStep( c, d, p2 )
-   * Then getProofForRewriting(f(a,c),pf) returns a proof of:
-   *   f(a,c) = f(f(d),d) if d_policy is FIXPOINT,
-   *   f(a,c) = f(f(c),d) if d_policy is ONCE.
-   */
-  TConvPolicy d_policy;
-  /** The cache policy */
-  TConvCachePolicy d_cpolicy;
-  /** Name identifier */
-  std::string d_name;
-  /** The cache for terms */
-  std::map<Node, std::shared_ptr<ProofNode> > d_cache;
-  /** An (optional) term context object */
-  TermContext* d_tcontext;
-  /**
-   * Whether we rewrite operators. If this flag is true, then the main
-   * traversal algorithm of this proof generator traverses operators of
-   * APPLY_UF and uses HO_CONG to justify rewriting of subterms when necessary.
-   */
-  bool d_rewriteOps;
-  /** Get rewrite step for (hash value of) term. */
-  Node getRewriteStepInternal(Node thash, bool isPre) const;
-  /**
-   * Adds a proof of t = t' to the proof pf where t' is the result of rewriting
-   * t based on the rewrite steps registered to this class. This method then
-   * returns the proved equality t = t'.
-   */
-  Node getProofForRewriting(Node t, LazyCDProof& pf, TermContext* tc = nullptr);
-  /**
-   * Register rewrite step, returns the equality t=s if t is distinct from s
-   * and a rewrite step has not already been registered for t.
-   */
-  Node registerRewriteStep(Node t, Node s, uint32_t tctx, bool isPre);
-  /** cache that r is the rewritten form of cur, pf can provide a proof */
-  void doCache(Node curHash, Node cur, Node r, LazyCDProof& pf);
-  /** get debug information on this generator */
-  std::string toStringDebug() const;
-};
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */