(proof-new) Updates to CDProof (#4565)

This updates CDProof with several new functionalities, including making it agnostic to symmetry of (dis)equalites.

4 files changed, 410 insertions, 51 deletions

diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index eff222b92..f9e50c0f4 100644
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -18,6 +18,18 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
+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;
+}
+
 CDProof::CDProof(ProofNodeManager* pnm, context::Context* c)
     : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context)
 {
@@ -25,6 +37,22 @@ CDProof::CDProof(ProofNodeManager* pnm, context::Context* c)
 
 CDProof::~CDProof() {}
 
+std::shared_ptr<ProofNode> CDProof::mkProof(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);
@@ -35,42 +63,100 @@ std::shared_ptr<ProofNode> CDProof::getProof(Node fact) const
   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;
+  }
+  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,
-                      bool forceOverwrite)
+                      CDPOverwrite opolicy)
 {
-  // we must provide expected
+  Trace("cdproof") << "CDProof::addStep: " << id << " " << expected
+                   << ", ensureChildren = " << ensureChildren
+                   << ", overwrite policy = " << opolicy << std::endl;
+  // We must always provide expected to this method
   Assert(!expected.isNull());
 
-  NodeProofNodeMap::iterator it = d_nodes.find(expected);
-  if (it != d_nodes.end())
+  std::shared_ptr<ProofNode> pprev = getProofSymm(expected);
+  if (pprev != nullptr)
   {
-    if (!forceOverwrite
-        && ((*it).second->getRule() != PfRule::ASSUME || id == PfRule::ASSUME))
+    if (!shouldOverwrite(pprev.get(), id, opolicy))
     {
-      // we do not overwrite if forceOverwrite is false and the previously
-      // provided step was not an assumption, or if the currently provided step
-      // is a (duplicate) assumption
+      // 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)
   {
-    std::shared_ptr<ProofNode> pc = getProof(c);
+    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;
@@ -82,37 +168,150 @@ bool CDProof::addStep(Node expected,
     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 (it == d_nodes.end())
+  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 = (*it).second;
-    d_manager->updateNode(pthis.get(), id, pchildren, args);
+    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)
+{
+  // 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;
+    }
   }
-  // the result of the proof node should be expected
-  Assert(pthis->getResult() == expected);
   return true;
 }
 
-bool CDProof::addProof(ProofNode* pn, bool forceOverwrite)
+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);
+  visit.push_back(pn.get());
   bool retValue = true;
   do
   {
@@ -143,12 +342,8 @@ bool CDProof::addProof(ProofNode* pn, bool forceOverwrite)
         pexp.push_back(c->getResult());
       }
       // can ensure children at this point
-      bool res = addStep(curFact,
-                         cur->getRule(),
-                         pexp,
-                         cur->getArguments(),
-                         true,
-                         forceOverwrite);
+      bool res = addStep(
+          curFact, cur->getRule(), pexp, cur->getArguments(), true, opolicy);
       // should always succeed
       Assert(res);
       retValue = retValue && res;
@@ -159,4 +354,86 @@ bool CDProof::addProof(ProofNode* pn, bool forceOverwrite)
   return retValue;
 }
 
+bool CDProof::hasStep(Node fact)
+{
+  std::shared_ptr<ProofNode> pf = getProof(fact);
+  if (pf != nullptr && !isAssumption(pf.get()))
+  {
+    return true;
+  }
+  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][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();
+}
+
 }  // namespace CVC4
diff --git a/src/expr/proof.h b/src/expr/proof.h
index c3b9698ca..94a3b6ab0 100644
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -24,9 +24,23 @@
 #include "expr/node.h"
 #include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
+#include "expr/proof_step_buffer.h"
 
 namespace CVC4 {
 
+/** An overwrite policy for CDProof below */
+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);
+
 /**
  * A (context-dependent) proof.
  *
@@ -76,10 +90,11 @@ namespace CVC4 {
  * Notice that the proof of A by ID_A was not overwritten by ASSUME in the
  * addStep call above.
  *
- * The policy for overwriting proof steps 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 forceOverwrite is true.
+ * 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 {}, {} )
@@ -87,7 +102,7 @@ namespace CVC4 {
  * At this point, getProof( A ) returns:
  *   ID_A1( ID_B1(), ASSUME(C) )
  * Now, assume an additional call is made to addProof, where notice
- * forceOverwrite is false by default:
+ * 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:
@@ -114,22 +129,39 @@ namespace CVC4 {
  * 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
 {
-  typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
-      NodeProofNodeMap;
-
  public:
   CDProof(ProofNodeManager* pnm, context::Context* c = nullptr);
-  ~CDProof();
+  virtual ~CDProof();
   /**
-   * Get proof for fact, or nullptr if it does not exist. 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.
+   * 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> getProof(Node fact) const;
+  virtual std::shared_ptr<ProofNode> mkProof(Node fact);
   /** Add step
    *
    * @param expected The intended conclusion of this proof step. This must be
@@ -141,8 +173,8 @@ class CDProof
    * @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 forceOverwrite Whether we wish to overwrite if a step for expected
-   * was already provided (via a previous call to addStep)
+   * @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
@@ -156,39 +188,85 @@ class CDProof
    * of order.
    *
    * This method only overwrites proofs for facts that were added as
-   * steps with id ASSUME when forceOverwrite is false, and otherwise always
-   * overwrites an existing step if one was provided when forceOverwrite is
-   * true.
+   * 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,
-               bool forceOverwrite = 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 forceOverwrite Whether we wish to force overwriting if a step was
-   * already provided, for each node in the proof.
+   * @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.
    *
-   * 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 does not impact the
-   * internal data of this 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(ProofNode* pn, bool forceOverwrite = false);
+  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 symmetric fact (a g such that isSame returns true for isSame(f,g)), or
+   * null if none exist.
+   */
+  static Node getSymmFact(TNode f);
 
  protected:
+  typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
+      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;
+  /** Get proof for fact, or nullptr if it does not exist. */
+  std::shared_ptr<ProofNode> getProof(Node fact) const;
+  /** 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 CVC4
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index e2f5ca2dc..b4775d915 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -86,4 +86,6 @@ Node ProofNodeManager::checkInternal(
   return res;
 }
 
+ProofChecker* ProofNodeManager::getChecker() const { return d_checker; }
+
 }  // namespace CVC4
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 17c5580bf..107223692 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -92,6 +92,8 @@ class ProofNodeManager
                   PfRule id,
                   const std::vector<std::shared_ptr<ProofNode>>& children,
                   const std::vector<Node>& args);
+  /** Get the underlying proof checker */
+  ProofChecker* getChecker() const;
 
  private:
   /** The (optional) proof checker */