From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 11 Jul 2020 00:03:24 +0000 (-0500)
Subject: (proof-new) Update Theory interface for proof-new (#4648)
X-Git-Tag: cvc5-1.0.0~3131
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c5a6aa2e03b05a5db6150563a4d5994abf5b24e9;p=cvc5.git

(proof-new) Update Theory interface for proof-new (#4648)

This includes 4 changes:

Theory constructor takes a ProofNodeManager,
Theory::explain returns a TrustNode (of kind PROP_EXP),
Theory::expandDefinitions returns a TrustNode (of kind REWRITE),
Theory::ppRewrite returns a TrustNode (of kind REWRITE).
These are all currently planned updates to the interface of Theory.
This PR also connects some of the existing proof rule checkers into the proof checker, if one is provided to the constructor. It updates TheoryEngine and other places to process TrustNode in trivial ways (converting them into Node). These calls will later be updated as needed for proof support.

This PR is also contingent on the performance tests for proof-new on SMT-LIB.
---

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 66109bfac..3103557c8 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -1069,13 +1069,22 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
   Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl;
 
   if (d_theory->getId()==theory::THEORY_UF) {
-    th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v,
+    th = new theory::uf::TheoryUF(&fakeContext,
+                                  &fakeContext,
+                                  oc,
+                                  v,
                                   ProofManager::currentPM()->getLogicInfo(),
+                                  nullptr,
                                   "replay::");
   } else if (d_theory->getId()==theory::THEORY_ARRAYS) {
-    th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v,
-                                          ProofManager::currentPM()->getLogicInfo(),
-                                          "replay::");
+    th = new theory::arrays::TheoryArrays(
+        &fakeContext,
+        &fakeContext,
+        oc,
+        v,
+        ProofManager::currentPM()->getLogicInfo(),
+        nullptr,
+        "replay::");
   } else if (d_theory->getId() == theory::THEORY_ARITH) {
     Trace("theory-proof-debug") << "Arith proofs currently not supported. Use 'trust'" << std::endl;
     os << " (clausify_false trust)";
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 44944d0c2..4eedfd863 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -738,7 +738,8 @@ Node ProcessAssertions::expandDefinitions(
         theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
 
         Assert(t != NULL);
-        node = t->expandDefinition(n);
+        TrustNode trn = t->expandDefinition(n);
+        node = trn.isNull() ? Node(n) : trn.getNode();
       }
 
       // the partial functions can fall through, in which case we still
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 8b4747927..83ae5a032 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -31,13 +31,17 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
-                         OutputChannel& out, Valuation valuation,
-                         const LogicInfo& logicInfo)
-    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
-    , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
-    , d_ppRewriteTimer("theory::arith::ppRewriteTimer")
-    , d_proofRecorder(nullptr)
+TheoryArith::TheoryArith(context::Context* c,
+                         context::UserContext* u,
+                         OutputChannel& out,
+                         Valuation valuation,
+                         const LogicInfo& logicInfo,
+                         ProofNodeManager* pnm)
+    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm),
+      d_internal(
+          new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)),
+      d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
+      d_proofRecorder(nullptr)
 {
   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
   // if logic is non-linear
@@ -82,9 +86,10 @@ void TheoryArith::finishInit()
   }
 }
 
-Node TheoryArith::expandDefinition(Node node)
+TrustNode TheoryArith::expandDefinition(Node node)
 {
-  return d_internal->expandDefinition(node);
+  Node expNode = d_internal->expandDefinition(node);
+  return TrustNode::mkTrustRewrite(node, expNode, nullptr);
 }
 
 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -95,9 +100,15 @@ void TheoryArith::addSharedTerm(TNode n){
   d_internal->addSharedTerm(n);
 }
 
-Node TheoryArith::ppRewrite(TNode atom) {
+TrustNode TheoryArith::ppRewrite(TNode atom)
+{
   CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
-  return d_internal->ppRewrite(atom);
+  Node ret = d_internal->ppRewrite(atom);
+  if (ret != atom)
+  {
+    return TrustNode::mkTrustRewrite(atom, ret, nullptr);
+  }
+  return TrustNode::null();
 }
 
 Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
@@ -117,8 +128,10 @@ bool TheoryArith::needsCheckLastEffort() {
   return d_internal->needsCheckLastEffort();
 }
 
-Node TheoryArith::explain(TNode n) {
-  return d_internal->explain(n);
+TrustNode TheoryArith::explain(TNode n)
+{
+  Node exp = d_internal->explain(n);
+  return TrustNode::mkTrustPropExp(n, exp, nullptr);
 }
 
 bool TheoryArith::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 5b68e3e7a..9381b7341 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -34,7 +34,7 @@ namespace arith {
  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
  */
 class TheoryArith : public Theory {
-private:
+ private:
   friend class TheoryArithPrivate;
 
   TheoryArithPrivate* d_internal;
@@ -46,9 +46,13 @@ private:
    */
   proof::ArithProofRecorder * d_proofRecorder;
 
-public:
-  TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out,
-              Valuation valuation, const LogicInfo& logicInfo);
+ public:
+  TheoryArith(context::Context* c,
+              context::UserContext* u,
+              OutputChannel& out,
+              Valuation valuation,
+              const LogicInfo& logicInfo,
+              ProofNodeManager* pnm = nullptr);
   virtual ~TheoryArith();
 
   TheoryRewriter* getTheoryRewriter() override;
@@ -60,14 +64,14 @@ public:
 
   void finishInit() override;
 
-  Node expandDefinition(Node node) override;
+  TrustNode expandDefinition(Node node) override;
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
   void check(Effort e) override;
   bool needsCheckLastEffort() override;
   void propagate(Effort e) override;
-  Node explain(TNode n) override;
+  TrustNode explain(TNode n) override;
   bool getCurrentSubstitution(int effort,
                               std::vector<Node>& vars,
                               std::vector<Node>& subs,
@@ -84,7 +88,7 @@ public:
   void presolve() override;
   void notifyRestart() override;
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
-  Node ppRewrite(TNode atom) override;
+  TrustNode ppRewrite(TNode atom) override;
   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
 
   std::string identify() const override { return std::string("TheoryArith"); }
@@ -100,7 +104,7 @@ public:
       const EntailmentCheckParameters* params,
       EntailmentCheckSideEffects* out) override;
 
-  void setProofRecorder(proof::ArithProofRecorder * proofRecorder)
+  void setProofRecorder(proof::ArithProofRecorder* proofRecorder)
   {
     d_proofRecorder = proofRecorder;
   }
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 71e040ccc..49f93286e 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -62,8 +62,9 @@ TheoryArrays::TheoryArrays(context::Context* c,
                            OutputChannel& out,
                            Valuation valuation,
                            const LogicInfo& logicInfo,
+                           ProofNodeManager* pnm,
                            std::string name)
-    : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, name),
+    : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, pnm, name),
       d_numRow(name + "theory::arrays::number of Row lemmas", 0),
       d_numExt(name + "theory::arrays::number of Ext lemmas", 0),
       d_numProp(name + "theory::arrays::number of propagations", 0),
@@ -315,16 +316,20 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck
   return term;
 }
 
-
-Node TheoryArrays::ppRewrite(TNode term) {
-  if (!d_preprocess) return term;
+TrustNode TheoryArrays::ppRewrite(TNode term)
+{
+  if (!d_preprocess)
+  {
+    return TrustNode::null();
+  }
   d_ppEqualityEngine.addTerm(term);
+  Node ret;
   switch (term.getKind()) {
     case kind::SELECT: {
       // select(store(a,i,v),j) = select(a,j)
       //    IF i != j
       if (term[0].getKind() == kind::STORE && ppDisequal(term[0][1], term[1])) {
-        return NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1];
+        ret = NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1];
       }
       break;
     }
@@ -334,18 +339,22 @@ Node TheoryArrays::ppRewrite(TNode term) {
       if (term[0].getKind() == kind::STORE && (term[1] < term[0][1]) && ppDisequal(term[1],term[0][1])) {
         Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2];
         Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2];
-        return outer;
+        ret = outer;
       }
       break;
     }
     case kind::EQUAL: {
-      return solveWrite(term, d_solveWrite, d_solveWrite2, true);
+      ret = solveWrite(term, d_solveWrite, d_solveWrite2, true);
       break;
     }
     default:
       break;
   }
-  return term;
+  if (!ret.isNull() && ret != term)
+  {
+    return TrustNode::mkTrustRewrite(term, ret, nullptr);
+  }
+  return TrustNode::null();
 }
 
 
@@ -848,10 +857,10 @@ void TheoryArrays::propagate(Effort e)
   // direct propagation now
 }
 
-
-Node TheoryArrays::explain(TNode literal) {
+TrustNode TheoryArrays::explain(TNode literal)
+{
   Node explanation = explain(literal, NULL);
-  return explanation;
+  return TrustNode::mkTrustPropExp(literal, explanation, nullptr);
 }
 
 Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) {
@@ -2312,7 +2321,7 @@ std::string TheoryArrays::TheoryArraysDecisionStrategy::identify() const
   return std::string("th_arrays_dec");
 }
 
-Node TheoryArrays::expandDefinition(Node node)
+TrustNode TheoryArrays::expandDefinition(Node node)
 {
   NodeManager* nm = NodeManager::currentNM();
   Kind kind = node.getKind();
@@ -2362,9 +2371,10 @@ Node TheoryArrays::expandDefinition(Node node)
                          nm->mkNode(kind::SELECT, a, k),
                          nm->mkNode(kind::SELECT, b, k));
     Node implies = nm->mkNode(kind::IMPLIES, range, eq);
-    return nm->mkNode(kind::FORALL, bvl, implies);
+    Node ret = nm->mkNode(kind::FORALL, bvl, implies);
+    return TrustNode::mkTrustRewrite(node, ret, nullptr);
   }
-  return node;
+  return TrustNode::null();
 }
 
 }/* CVC4::theory::arrays namespace */
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index c5cd24fd3..a4416ab8c 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -139,9 +139,12 @@ class TheoryArrays : public Theory {
   unsigned d_reasonExt;
 
  public:
-
-  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
-               Valuation valuation, const LogicInfo& logicInfo,
+  TheoryArrays(context::Context* c,
+               context::UserContext* u,
+               OutputChannel& out,
+               Valuation valuation,
+               const LogicInfo& logicInfo,
+               ProofNodeManager* pnm = nullptr,
                std::string name = "");
   ~TheoryArrays();
 
@@ -151,7 +154,7 @@ class TheoryArrays : public Theory {
 
   std::string identify() const override { return std::string("TheoryArrays"); }
 
-  Node expandDefinition(Node node) override;
+  TrustNode expandDefinition(Node node) override;
 
   /////////////////////////////////////////////////////////////////////////////
   // PREPROCESSING
@@ -185,7 +188,7 @@ class TheoryArrays : public Theory {
 
  public:
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
-  Node ppRewrite(TNode atom) override;
+  TrustNode ppRewrite(TNode atom) override;
 
   /////////////////////////////////////////////////////////////////////////////
   // T-PROPAGATION / REGISTRATION
@@ -215,7 +218,7 @@ class TheoryArrays : public Theory {
   void preRegisterTerm(TNode n) override;
   void propagate(Effort e) override;
   Node explain(TNode n, eq::EqProof* proof);
-  Node explain(TNode n) override;
+  TrustNode explain(TNode n) override;
 
   /////////////////////////////////////////////////////////////////////////////
   // SHARING
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 04a1675a4..022249808 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -19,6 +19,7 @@
 #include <stack>
 #include <vector>
 
+#include "expr/proof_node_manager.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/booleans/circuit_propagator.h"
 #include "theory/booleans/theory_bool_rewriter.h"
@@ -37,9 +38,16 @@ TheoryBool::TheoryBool(context::Context* c,
                        context::UserContext* u,
                        OutputChannel& out,
                        Valuation valuation,
-                       const LogicInfo& logicInfo)
-    : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo)
+                       const LogicInfo& logicInfo,
+                       ProofNodeManager* pnm)
+    : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, pnm)
 {
+  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
+  if (pc != nullptr)
+  {
+    // add checkers
+    d_bProofChecker.registerTo(pc);
+  }
 }
 
 Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
@@ -67,22 +75,6 @@ Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubsti
   return Theory::ppAssert(in, outSubstitutions);
 }
 
-/*
-void TheoryBool::check(Effort level) {
-  if (done() && !fullEffort(level)) {
-    return;
-  }
-  while (!done())
-  {
-    // Get all the assertions
-    Assertion assertion = get();
-    TNode fact = assertion.assertion;
-  }
-  if( Theory::fullEffort(level) ){
-  }
-}  
-*/
-
 }/* CVC4::theory::booleans namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 99c80dd4a..2f882e257 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -20,6 +20,7 @@
 #define CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
 
 #include "context/context.h"
+#include "theory/booleans/proof_checker.h"
 #include "theory/booleans/theory_bool_rewriter.h"
 #include "theory/theory.h"
 
@@ -33,19 +34,20 @@ class TheoryBool : public Theory {
              context::UserContext* u,
              OutputChannel& out,
              Valuation valuation,
-             const LogicInfo& logicInfo);
+             const LogicInfo& logicInfo,
+             ProofNodeManager* pnm = nullptr);
 
   TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
-  //void check(Effort);
-
   std::string identify() const override { return std::string("TheoryBool"); }
 
  private:
   /** The theory rewriter for this theory. */
   TheoryBoolRewriter d_rewriter;
+  /** Proof rule checker */
+  BoolProofRuleChecker d_bProofChecker;
 };/* class TheoryBool */
 
 }/* CVC4::theory::booleans namespace */
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 695d5b91b..f6ce4414e 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -17,6 +17,7 @@
 #include "theory/builtin/theory_builtin.h"
 
 #include "expr/kind.h"
+#include "expr/proof_node_manager.h"
 #include "theory/builtin/theory_builtin_rewriter.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
@@ -31,9 +32,16 @@ TheoryBuiltin::TheoryBuiltin(context::Context* c,
                              context::UserContext* u,
                              OutputChannel& out,
                              Valuation valuation,
-                             const LogicInfo& logicInfo)
-    : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo)
+                             const LogicInfo& logicInfo,
+                             ProofNodeManager* pnm)
+    : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, pnm)
 {
+  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
+  if (pc != nullptr)
+  {
+    // add checkers
+    d_bProofChecker.registerTo(pc);
+  }
 }
 
 std::string TheoryBuiltin::identify() const
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index e4767645e..beca0b76a 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -19,6 +19,7 @@
 #ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
 #define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
 
+#include "theory/builtin/proof_checker.h"
 #include "theory/builtin/theory_builtin_rewriter.h"
 #include "theory/theory.h"
 
@@ -33,7 +34,8 @@ class TheoryBuiltin : public Theory
                 context::UserContext* u,
                 OutputChannel& out,
                 Valuation valuation,
-                const LogicInfo& logicInfo);
+                const LogicInfo& logicInfo,
+                ProofNodeManager* pnm = nullptr);
 
   TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
@@ -45,6 +47,8 @@ class TheoryBuiltin : public Theory
  private:
   /** The theory rewriter for this theory. */
   TheoryBuiltinRewriter d_rewriter;
+  /** Proof rule checker */
+  BuiltinProofRuleChecker d_bProofChecker;
 }; /* class TheoryBuiltin */
 
 }  // namespace builtin
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 1bbcc05ce..c8e585d88 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -49,8 +49,9 @@ TheoryBV::TheoryBV(context::Context* c,
                    OutputChannel& out,
                    Valuation valuation,
                    const LogicInfo& logicInfo,
+                   ProofNodeManager* pnm,
                    std::string name)
-    : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name),
+    : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
       d_context(c),
       d_alreadyPropagatedSet(c),
       d_sharedTermsSet(c),
@@ -194,15 +195,16 @@ void TheoryBV::finishInit()
   tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
 }
 
-Node TheoryBV::expandDefinition(Node node)
+TrustNode TheoryBV::expandDefinition(Node node)
 {
   Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
 
+  Node ret;
   switch (node.getKind()) {
   case kind::BITVECTOR_SDIV:
   case kind::BITVECTOR_SREM:
   case kind::BITVECTOR_SMOD:
-    return TheoryBVRewriter::eliminateBVSDiv(node);
+    ret = TheoryBVRewriter::eliminateBVSDiv(node);
     break;
 
   case kind::BITVECTOR_UDIV:
@@ -212,7 +214,8 @@ Node TheoryBV::expandDefinition(Node node)
 
     if (options::bitvectorDivByZeroConst()) {
       Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL;
-      return nm->mkNode(kind, node[0], node[1]);
+      ret = nm->mkNode(kind, node[0], node[1]);
+      break;
     }
 
     TNode num = node[0], den = node[1];
@@ -221,17 +224,18 @@ Node TheoryBV::expandDefinition(Node node)
 				     kind::BITVECTOR_UREM_TOTAL, num, den);
     Node divByZero = getBVDivByZero(node.getKind(), width);
     Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
-    node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
-    return node;
+    ret = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
   }
     break;
 
   default:
-    return node;
     break;
   }
-
-  Unreachable();
+  if (!ret.isNull() && node != ret)
+  {
+    return TrustNode::mkTrustRewrite(node, ret, nullptr);
+  }
+  return TrustNode::null();
 }
 
 void TheoryBV::preRegisterTerm(TNode node) {
@@ -709,7 +713,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
   return PP_ASSERT_STATUS_UNSOLVED;
 }
 
-Node TheoryBV::ppRewrite(TNode t)
+TrustNode TheoryBV::ppRewrite(TNode t)
 {
   Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
   Node res = t;
@@ -790,7 +794,11 @@ Node TheoryBV::ppRewrite(TNode t)
     d_abstractionModule->addInputAtom(res);
   }
   Debug("bv-pp-rewrite") << "to   " << res << "\n";
-  return res;
+  if (res != t)
+  {
+    return TrustNode::mkTrustRewrite(t, res, nullptr);
+  }
+  return TrustNode::null();
 }
 
 void TheoryBV::presolve() {
@@ -851,22 +859,26 @@ void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
   d_subtheoryMap[sub]->explain(literal, assumptions);
 }
 
-
-Node TheoryBV::explain(TNode node) {
+TrustNode TheoryBV::explain(TNode node)
+{
   Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
   std::vector<TNode> assumptions;
 
   // Ask for the explanation
   explain(node, assumptions);
   // this means that it is something true at level 0
+  Node explanation;
   if (assumptions.size() == 0) {
-    return utils::mkTrue();
+    explanation = utils::mkTrue();
+  }
+  else
+  {
+    // return the explanation
+    explanation = utils::mkAnd(assumptions);
   }
-  // return the explanation
-  Node explanation = utils::mkAnd(assumptions);
   Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
   Debug("bitvector::explain") << "TheoryBV::explain done. \n";
-  return explanation;
+  return TrustNode::mkTrustPropExp(node, explanation, nullptr);
 }
 
 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 513ed6bc0..c98de0f18 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -65,10 +65,13 @@ class TheoryBV : public Theory {
   std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
   std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
 
-public:
-
-  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
-           Valuation valuation, const LogicInfo& logicInfo,
+ public:
+  TheoryBV(context::Context* c,
+           context::UserContext* u,
+           OutputChannel& out,
+           Valuation valuation,
+           const LogicInfo& logicInfo,
+           ProofNodeManager* pnm = nullptr,
            std::string name = "");
 
   ~TheoryBV();
@@ -79,7 +82,7 @@ public:
 
   void finishInit() override;
 
-  Node expandDefinition(Node node) override;
+  TrustNode expandDefinition(Node node) override;
 
   void preRegisterTerm(TNode n) override;
 
@@ -89,7 +92,7 @@ public:
 
   void propagate(Effort e) override;
 
-  Node explain(TNode n) override;
+  TrustNode explain(TNode n) override;
 
   bool collectModelInfo(TheoryModel* m) override;
 
@@ -100,27 +103,28 @@ public:
   bool getCurrentSubstitution(int effort,
                               std::vector<Node>& vars,
                               std::vector<Node>& subs,
-                              std::map<Node, std::vector<Node> >& exp) override;
+                              std::map<Node, std::vector<Node>>& exp) override;
   int getReduction(int effort, Node n, Node& nr) override;
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
   void enableCoreTheorySlicer();
 
-  Node ppRewrite(TNode t) override;
+  TrustNode ppRewrite(TNode t) override;
 
   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
 
   void presolve() override;
 
-  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+  bool applyAbstraction(const std::vector<Node>& assertions,
+                        std::vector<Node>& new_assertions);
 
   void setProofLog(proof::BitVectorProof* bvp);
 
  private:
-
-  class Statistics {
-  public:
+  class Statistics
+  {
+   public:
     AverageStat d_avgConflictSize;
     IntStat     d_solveSubstitutions;
     TimerStat   d_solveTimer;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 30ee07d27..e19beb7f3 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -45,8 +45,9 @@ TheoryDatatypes::TheoryDatatypes(Context* c,
                                  UserContext* u,
                                  OutputChannel& out,
                                  Valuation valuation,
-                                 const LogicInfo& logicInfo)
-    : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
+                                 const LogicInfo& logicInfo,
+                                 ProofNodeManager* pnm)
+    : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, pnm),
       d_infer(c),
       d_infer_exp(c),
       d_term_sk(u),
@@ -558,7 +559,7 @@ void TheoryDatatypes::finishInit() {
   }
 }
 
-Node TheoryDatatypes::expandDefinition(Node n)
+TrustNode TheoryDatatypes::expandDefinition(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
   // must ensure the type is well founded and has no nested recursion if
@@ -583,6 +584,7 @@ Node TheoryDatatypes::expandDefinition(Node n)
       }
     }
   }
+  Node ret;
   switch (n.getKind())
   {
     case kind::APPLY_SELECTOR:
@@ -608,34 +610,31 @@ Node TheoryDatatypes::expandDefinition(Node n)
       Node sel = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, selector_use, n[0]);
       if (options::dtRewriteErrorSel())
       {
-        return sel;
+        ret = sel;
       }
       else
       {
         Node tester = c.getTester();
         Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]);
         tst = Rewriter::rewrite(tst);
-        Node n_ret;
         if (tst == d_true)
         {
-          n_ret = sel;
+          ret = sel;
         }else{
           mkExpDefSkolem(selector, ndt, n.getType());
           Node sk =
               nm->mkNode(kind::APPLY_UF, d_exp_def_skolem[ndt][selector], n[0]);
           if (tst == nm->mkConst(false))
           {
-            n_ret = sk;
+            ret = sk;
           }
           else
           {
-            n_ret = nm->mkNode(kind::ITE, tst, sel, sk);
+            ret = nm->mkNode(kind::ITE, tst, sel, sk);
           }
         }
-        // n_ret = Rewriter::rewrite( n_ret );
-        Trace("dt-expand") << "Expand def : " << n << " to " << n_ret
+        Trace("dt-expand") << "Expand def : " << n << " to " << ret
                            << std::endl;
-        return n_ret;
       }
     }
     break;
@@ -681,14 +680,17 @@ Node TheoryDatatypes::expandDefinition(Node n)
                           << b[b.getNumChildren() - 1] << std::endl;
         }
       }
-      Node n_ret = b;
-      Debug("tuprec") << "return " << n_ret << std::endl;
-      return n_ret;
+      ret = b;
+      Debug("tuprec") << "return " << ret << std::endl;
     }
     break;
-    default: return n; break;
+    default: break;
   }
-  Unreachable();
+  if (!ret.isNull() && n != ret)
+  {
+    return TrustNode::mkTrustRewrite(n, ret, nullptr);
+  }
+  return TrustNode::null();
 }
 
 void TheoryDatatypes::presolve()
@@ -696,7 +698,7 @@ void TheoryDatatypes::presolve()
   Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
 }
 
-Node TheoryDatatypes::ppRewrite(TNode in)
+TrustNode TheoryDatatypes::ppRewrite(TNode in)
 {
   Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
 
@@ -712,12 +714,14 @@ Node TheoryDatatypes::ppRewrite(TNode in)
       nn = rew.size()==0 ? d_true :
                 ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
     }
-    return nn;
+    if (in != nn)
+    {
+      return TrustNode::mkTrustRewrite(in, nn, nullptr);
+    }
   }
 
   // nothing to do
-  return in;
-
+  return TrustNode::null();
 }
 
 void TheoryDatatypes::addSharedTerm(TNode t) {
@@ -800,7 +804,14 @@ void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){
   }
 }
 
-Node TheoryDatatypes::explain( TNode literal ){
+TrustNode TheoryDatatypes::explain(TNode literal)
+{
+  Node exp = explainLit(literal);
+  return TrustNode::mkTrustPropExp(literal, exp, nullptr);
+}
+
+Node TheoryDatatypes::explainLit(TNode literal)
+{
   std::vector< TNode > assumptions;
   explain( literal, assumptions );
   return mkAnd( assumptions );
@@ -816,7 +827,8 @@ Node TheoryDatatypes::explain( std::vector< Node >& lits ) {
 
 /** Conflict when merging two constants */
 void TheoryDatatypes::conflict(TNode a, TNode b){
-  d_conflictNode = explain( a.eqNode(b) );
+  Node eq = a.eqNode(b);
+  d_conflictNode = explainLit(eq);
   Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl;
   d_out->conflict( d_conflictNode );
   d_conflict = true;
@@ -869,7 +881,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
           std::vector< Node > rew;
           if (utils::checkClash(cons1, cons2, rew))
           {
-            d_conflictNode = explain( unifEq );
+            d_conflictNode = explainLit(unifEq);
             Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
             d_out->conflict( d_conflictNode );
             d_conflict = true;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 11c6b5f36..b2d416ecf 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -267,9 +267,12 @@ private:
   void computeCareGraph() override;
 
  public:
-  TheoryDatatypes(context::Context* c, context::UserContext* u,
-                  OutputChannel& out, Valuation valuation,
-                  const LogicInfo& logicInfo);
+  TheoryDatatypes(context::Context* c,
+                  context::UserContext* u,
+                  OutputChannel& out,
+                  Valuation valuation,
+                  const LogicInfo& logicInfo,
+                  ProofNodeManager* pnm = nullptr);
   ~TheoryDatatypes();
 
   TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
@@ -285,7 +288,8 @@ private:
   void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions );
   void explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions );
   void explain( TNode literal, std::vector<TNode>& assumptions );
-  Node explain(TNode literal) override;
+  TrustNode explain(TNode literal) override;
+  Node explainLit(TNode literal);
   Node explain( std::vector< Node >& lits );
   /** Conflict when merging two constants */
   void conflict(TNode a, TNode b);
@@ -302,8 +306,8 @@ private:
   bool needsCheckLastEffort() override;
   void preRegisterTerm(TNode n) override;
   void finishInit() override;
-  Node expandDefinition(Node n) override;
-  Node ppRewrite(TNode n) override;
+  TrustNode expandDefinition(Node n) override;
+  TrustNode ppRewrite(TNode n) override;
   void presolve() override;
   void addSharedTerm(TNode t) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 50c66919f..bffcda7bc 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -99,12 +99,13 @@ Node buildConjunct(const std::vector<TNode> &assumptions) {
 }  // namespace helper
 
 /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-TheoryFp::TheoryFp(context::Context *c,
-                   context::UserContext *u,
-                   OutputChannel &out,
+TheoryFp::TheoryFp(context::Context* c,
+                   context::UserContext* u,
+                   OutputChannel& out,
                    Valuation valuation,
-                   const LogicInfo &logicInfo)
-    : Theory(THEORY_FP, c, u, out, valuation, logicInfo),
+                   const LogicInfo& logicInfo,
+                   ProofNodeManager* pnm)
+    : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm),
       d_notification(*this),
       d_equalityEngine(d_notification, c, "theory::fp::ee", true),
       d_registeredTerms(u),
@@ -382,7 +383,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
   return uf;
 }
 
-Node TheoryFp::expandDefinition(Node node)
+TrustNode TheoryFp::expandDefinition(Node node)
 {
   Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
                                << std::endl;
@@ -429,12 +430,12 @@ Node TheoryFp::expandDefinition(Node node)
   if (res != node) {
     Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
                                  << " rewritten to " << res << std::endl;
+    return TrustNode::mkTrustRewrite(node, res, nullptr);
   }
-
-  return res;
+  return TrustNode::null();
 }
 
-Node TheoryFp::ppRewrite(TNode node)
+TrustNode TheoryFp::ppRewrite(TNode node)
 {
   Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl;
 
@@ -492,9 +493,10 @@ Node TheoryFp::ppRewrite(TNode node)
   {
     Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): node " << node
                           << " rewritten to " << res << std::endl;
+    return TrustNode::mkTrustRewrite(node, res, nullptr);
   }
 
-  return res;
+  return TrustNode::null();
 }
 
 bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
@@ -1010,7 +1012,8 @@ void TheoryFp::setMasterEqualityEngine(eq::EqualityEngine *eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
 
-Node TheoryFp::explain(TNode n) {
+TrustNode TheoryFp::explain(TNode n)
+{
   Trace("fp") << "TheoryFp::explain(): explain " << n << std::endl;
 
   // All things we assert directly (and not via bit-vector) should
@@ -1025,7 +1028,8 @@ Node TheoryFp::explain(TNode n) {
     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
   }
 
-  return helper::buildConjunct(assumptions);
+  Node exp = helper::buildConjunct(assumptions);
+  return TrustNode::mkTrustPropExp(n, exp, nullptr);
 }
 
 Node TheoryFp::getModelValue(TNode var) {
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 52cd39863..a3e0dd94a 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -36,17 +36,21 @@ namespace fp {
 class TheoryFp : public Theory {
  public:
   /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-  TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out,
-           Valuation valuation, const LogicInfo& logicInfo);
+  TheoryFp(context::Context* c,
+           context::UserContext* u,
+           OutputChannel& out,
+           Valuation valuation,
+           const LogicInfo& logicInfo,
+           ProofNodeManager* pnm = nullptr);
 
   TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
-  Node expandDefinition(Node node) override;
+  TrustNode expandDefinition(Node node) override;
 
   void preRegisterTerm(TNode node) override;
   void addSharedTerm(TNode node) override;
 
-  Node ppRewrite(TNode node) override;
+  TrustNode ppRewrite(TNode node) override;
 
   void check(Effort) override;
 
@@ -58,7 +62,7 @@ class TheoryFp : public Theory {
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
-  Node explain(TNode n) override;
+  TrustNode explain(TNode n) override;
 
  protected:
   /** Equality engine */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5a8cde21e..e7d5d36a3 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -18,6 +18,7 @@
 
 #include "base/check.h"
 #include "expr/kind.h"
+#include "expr/proof_node_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/instantiation_engine.h"
 #include "theory/quantifiers/fmf/model_engine.h"
@@ -35,8 +36,13 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo)
+TheoryQuantifiers::TheoryQuantifiers(Context* c,
+                                     context::UserContext* u,
+                                     OutputChannel& out,
+                                     Valuation valuation,
+                                     const LogicInfo& logicInfo,
+                                     ProofNodeManager* pnm)
+    : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm)
 {
   out.handleUserAttribute( "fun-def", this );
   out.handleUserAttribute( "sygus", this );
@@ -46,6 +52,13 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
   out.handleUserAttribute( "quant-inst-max-level", this );
   out.handleUserAttribute( "quant-elim", this );
   out.handleUserAttribute( "quant-elim-partial", this );
+
+  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
+  if (pc != nullptr)
+  {
+    // add the proof rules
+    d_qChecker.registerTo(pc);
+  }
 }
 
 TheoryQuantifiers::~TheoryQuantifiers() {
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 0dab150ed..3168af195 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -19,13 +19,12 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 #define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 
-#include "context/cdhashmap.h"
 #include "context/context.h"
 #include "expr/node.h"
 #include "theory/output_channel.h"
+#include "theory/quantifiers/proof_checker.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/theory.h"
-#include "theory/theory_engine.h"
 #include "theory/valuation.h"
 #include "util/statistics_registry.h"
 
@@ -35,9 +34,12 @@ namespace quantifiers {
 
 class TheoryQuantifiers : public Theory {
  public:
-  TheoryQuantifiers(context::Context* c, context::UserContext* u,
-                    OutputChannel& out, Valuation valuation,
-                    const LogicInfo& logicInfo);
+  TheoryQuantifiers(context::Context* c,
+                    context::UserContext* u,
+                    OutputChannel& out,
+                    Valuation valuation,
+                    const LogicInfo& logicInfo,
+                    ProofNodeManager* pnm = nullptr);
   ~TheoryQuantifiers();
 
   TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
@@ -62,6 +64,8 @@ class TheoryQuantifiers : public Theory {
  private:
   /** The theory rewriter for this theory. */
   QuantifiersRewriter d_rewriter;
+  /** The proof rule checker */
+  QuantifiersProofRuleChecker d_qChecker;
 };/* class TheoryQuantifiers */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 4becfe731..372800b2b 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -39,16 +39,21 @@ namespace CVC4 {
 namespace theory {
 namespace sep {
 
-TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-  Theory(THEORY_SEP, c, u, out, valuation, logicInfo),
-  d_lemmas_produced_c(u),
-  d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::sep::ee", true),
-  d_conflict(c, false),
-  d_reduce(u),
-  d_infer(c),
-  d_infer_exp(c),
-  d_spatial_assertions(c)
+TheorySep::TheorySep(context::Context* c,
+                     context::UserContext* u,
+                     OutputChannel& out,
+                     Valuation valuation,
+                     const LogicInfo& logicInfo,
+                     ProofNodeManager* pnm)
+    : Theory(THEORY_SEP, c, u, out, valuation, logicInfo, pnm),
+      d_lemmas_produced_c(u),
+      d_notify(*this),
+      d_equalityEngine(d_notify, c, "theory::sep::ee", true),
+      d_conflict(c, false),
+      d_reduce(u),
+      d_infer(c),
+      d_infer_exp(c),
+      d_spatial_assertions(c)
 {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
@@ -84,12 +89,6 @@ Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) {
 /////////////////////////////////////////////////////////////////////////////
 
 
-
-Node TheorySep::ppRewrite(TNode term) {
-  Trace("sep-pp") << "ppRewrite : " << term << std::endl;
-  return term;
-}
-
 Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
 
   return PP_ASSERT_STATUS_UNSOLVED;
@@ -139,13 +138,13 @@ void TheorySep::propagate(Effort e){
 
 }
 
-
-Node TheorySep::explain(TNode literal)
+TrustNode TheorySep::explain(TNode literal)
 {
   Debug("sep") << "TheorySep::explain(" << literal << ")" << std::endl;
   std::vector<TNode> assumptions;
   explain(literal, assumptions);
-  return mkAnd(assumptions);
+  Node exp = mkAnd(assumptions);
+  return TrustNode::mkTrustPropExp(literal, exp, nullptr);
 }
 
 
@@ -833,7 +832,10 @@ bool TheorySep::needsCheckLastEffort() {
 
 void TheorySep::conflict(TNode a, TNode b) {
   Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl;
-  Node conflictNode = explain(a.eqNode(b));
+  Node eq = a.eqNode(b);
+  std::vector<TNode> assumptions;
+  explain(eq, assumptions);
+  Node conflictNode = mkAnd(assumptions);
   d_conflict = true;
   d_out->conflict( conflictNode );
 }
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 935170adf..3685ea063 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -66,7 +66,12 @@ class TheorySep : public Theory {
                         bool pol, bool hasPol, bool underSpatial );
 
  public:
-  TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheorySep(context::Context* c,
+            context::UserContext* u,
+            OutputChannel& out,
+            Valuation valuation,
+            const LogicInfo& logicInfo,
+            ProofNodeManager* pnm = nullptr);
   ~TheorySep();
 
   TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
@@ -81,7 +86,6 @@ class TheorySep : public Theory {
 
  public:
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
-  Node ppRewrite(TNode atom) override;
 
   void ppNotifyAssertions(const std::vector<Node>& assertions) override;
   /////////////////////////////////////////////////////////////////////////////
@@ -97,7 +101,7 @@ class TheorySep : public Theory {
 
  public:
   void propagate(Effort e) override;
-  Node explain(TNode n) override;
+  TrustNode explain(TNode n) override;
 
  public:
   void addSharedTerm(TNode t) override;
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 7eea7926b..c4e3e9add 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -31,8 +31,9 @@ TheorySets::TheorySets(context::Context* c,
                        context::UserContext* u,
                        OutputChannel& out,
                        Valuation valuation,
-                       const LogicInfo& logicInfo)
-    : Theory(THEORY_SETS, c, u, out, valuation, logicInfo),
+                       const LogicInfo& logicInfo,
+                       ProofNodeManager* pnm)
+    : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
       d_internal(new TheorySetsPrivate(*this, c, u))
 {
   // Do not move me to the header.
@@ -81,8 +82,10 @@ void TheorySets::computeCareGraph() {
   d_internal->computeCareGraph();
 }
 
-Node TheorySets::explain(TNode node) {
-  return d_internal->explain(node);
+TrustNode TheorySets::explain(TNode node)
+{
+  Node exp = d_internal->explain(node);
+  return TrustNode::mkTrustPropExp(node, exp, nullptr);
 }
 
 EqualityStatus TheorySets::getEqualityStatus(TNode a, TNode b) {
@@ -97,7 +100,7 @@ void TheorySets::preRegisterTerm(TNode node) {
   d_internal->preRegisterTerm(node);
 }
 
-Node TheorySets::expandDefinition(Node n)
+TrustNode TheorySets::expandDefinition(Node n)
 {
   Kind nk = n.getKind();
   if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 2fd1c2145..e81412ba9 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -39,7 +39,8 @@ class TheorySets : public Theory
              context::UserContext* u,
              OutputChannel& out,
              Valuation valuation,
-             const LogicInfo& logicInfo);
+             const LogicInfo& logicInfo,
+             ProofNodeManager* pnm);
   ~TheorySets() override;
 
   TheoryRewriter* getTheoryRewriter() override;
@@ -50,12 +51,12 @@ class TheorySets : public Theory
   void check(Effort) override;
   bool collectModelInfo(TheoryModel* m) override;
   void computeCareGraph() override;
-  Node explain(TNode) override;
+  TrustNode explain(TNode) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   Node getModelValue(TNode) override;
   std::string identify() const override { return "THEORY_SETS"; }
   void preRegisterTerm(TNode node) override;
-  Node expandDefinition(Node n) override;
+  TrustNode expandDefinition(Node n) override;
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
   void presolve() override;
   void propagate(Effort) override;
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 83b5b1c25..fc2a992a9 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1482,7 +1482,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
   }
 }
 
-Node TheorySetsPrivate::expandDefinition(Node node)
+TrustNode TheorySetsPrivate::expandDefinition(Node node)
 {
   Debug("sets-proc") << "expandDefinition : " << node << std::endl;
 
@@ -1511,10 +1511,10 @@ Node TheorySetsPrivate::expandDefinition(Node node)
     Node ite = nm->mkNode(kind::ITE, isEmpty, equal, memberAndEqual);
     Node witnessVariables = nm->mkNode(BOUND_VAR_LIST, witnessVariable);
     Node witness = nm->mkNode(WITNESS, witnessVariables, ite);
-    return witness;
+    return TrustNode::mkTrustRewrite(node, witness, nullptr);
   }
 
-  return node;
+  return TrustNode::null();
 }
 
 Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType)
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 83c58f094..c65c86795 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -208,8 +208,8 @@ class TheorySetsPrivate {
    * Another option to fix this is to make TheoryModel::getValue more general
    * so that it makes theory-specific calls to evaluate interpreted symbols.
    */
-  Node expandDefinition(Node n);
-  
+  TrustNode expandDefinition(Node n);
+
   void presolve();
 
   void propagate(Theory::Effort);
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index d1b18df13..942c8d216 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -38,8 +38,9 @@ TheoryStrings::TheoryStrings(context::Context* c,
                              context::UserContext* u,
                              OutputChannel& out,
                              Valuation valuation,
-                             const LogicInfo& logicInfo)
-    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
+                             const LogicInfo& logicInfo,
+                             ProofNodeManager* pnm)
+    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm),
       d_notify(*this),
       d_statistics(),
       d_equalityEngine(d_notify, c, "theory::strings::ee", true),
@@ -189,18 +190,20 @@ bool TheoryStrings::propagate(TNode literal) {
   return ok;
 }
 
-
-Node TheoryStrings::explain( TNode literal ){
+TrustNode TheoryStrings::explain(TNode literal)
+{
   Debug("strings-explain") << "explain called on " << literal << std::endl;
   std::vector< TNode > assumptions;
   d_im->explain(literal, assumptions);
+  Node ret;
   if( assumptions.empty() ){
-    return d_true;
+    ret = d_true;
   }else if( assumptions.size()==1 ){
-    return assumptions[0];
+    ret = assumptions[0];
   }else{
-    return NodeManager::currentNM()->mkNode( kind::AND, assumptions );
+    ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions);
   }
+  return TrustNode::mkTrustPropExp(literal, ret, nullptr);
 }
 
 bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& vars, 
@@ -577,7 +580,7 @@ void TheoryStrings::preRegisterTerm(TNode n)
   d_termReg.preRegisterTerm(n);
 }
 
-Node TheoryStrings::expandDefinition(Node node)
+TrustNode TheoryStrings::expandDefinition(Node node)
 {
   Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl;
 
@@ -593,14 +596,15 @@ Node TheoryStrings::expandDefinition(Node node)
     Node k = nm->mkBoundVar(nm->stringType());
     Node bvl = nm->mkNode(BOUND_VAR_LIST, k);
     Node emp = Word::mkEmptyWord(node.getType());
-    node = nm->mkNode(
+    Node ret = nm->mkNode(
         WITNESS,
         bvl,
         nm->mkNode(
             ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp)));
+    return TrustNode::mkTrustRewrite(node, ret, nullptr);
   }
 
-  return node;
+  return TrustNode::null();
 }
 
 void TheoryStrings::check(Effort e) {
@@ -712,11 +716,12 @@ void TheoryStrings::conflict(TNode a, TNode b){
   {
     Debug("strings-conflict") << "Making conflict..." << std::endl;
     d_state.setConflict();
-    Node conflictNode;
-    conflictNode = explain( a.eqNode(b) );
-    Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
+    TrustNode conflictNode = explain(a.eqNode(b));
+    Trace("strings-conflict")
+        << "CONFLICT: Eq engine conflict : " << conflictNode.getNode()
+        << std::endl;
     ++(d_statistics.d_conflictsEqEngine);
-    d_out->conflict( conflictNode );
+    d_out->conflict(conflictNode.getNode());
   }
 }
 
@@ -957,39 +962,48 @@ void TheoryStrings::checkRegisterTermsNormalForms()
   }
 }
 
-Node TheoryStrings::ppRewrite(TNode atom) {
+TrustNode TheoryStrings::ppRewrite(TNode atom)
+{
   Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
-  Node atomElim;
+  Node atomRet = atom;
   if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
   {
     // aggressive elimination of regular expression membership
-    atomElim = d_regexp_elim.eliminate(atom);
+    Node atomElim = d_regexp_elim.eliminate(atomRet);
     if (!atomElim.isNull())
     {
       Trace("strings-ppr") << "  rewrote " << atom << " -> " << atomElim
                            << " via regular expression elimination."
                            << std::endl;
-      atom = atomElim;
+      atomRet = atomElim;
     }
   }
   if( !options::stringLazyPreproc() ){
     //eager preprocess here
     std::vector< Node > new_nodes;
     StringsPreprocess* p = d_esolver->getPreprocess();
-    Node ret = p->processAssertion(atom, new_nodes);
-    if( ret!=atom ){
-      Trace("strings-ppr") << "  rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl; 
-      for( unsigned i=0; i<new_nodes.size(); i++ ){
-        Trace("strings-ppr") << "    lemma : " << new_nodes[i] << std::endl;
+    Node ret = p->processAssertion(atomRet, new_nodes);
+    if (ret != atomRet)
+    {
+      Trace("strings-ppr") << "  rewrote " << atomRet << " -> " << ret
+                           << ", with " << new_nodes.size() << " lemmas."
+                           << std::endl;
+      for (const Node& lem : new_nodes)
+      {
+        Trace("strings-ppr") << "    lemma : " << lem << std::endl;
         ++(d_statistics.d_lemmasEagerPreproc);
-        d_out->lemma( new_nodes[i] );
+        d_out->lemma(lem);
       }
-      return ret;
+      atomRet = ret;
     }else{
       Assert(new_nodes.empty());
     }
   }
-  return atom;
+  if (atomRet != atom)
+  {
+    return TrustNode::mkTrustRewrite(atom, atomRet, nullptr);
+  }
+  return TrustNode::null();
 }
 
 /** run the given inference step */
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 368c13a2d..dfaa99c06 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -61,9 +61,12 @@ class TheoryStrings : public Theory {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> TypeNodeSet;
  public:
-  TheoryStrings(context::Context* c, context::UserContext* u,
-                OutputChannel& out, Valuation valuation,
-                const LogicInfo& logicInfo);
+  TheoryStrings(context::Context* c,
+                context::UserContext* u,
+                OutputChannel& out,
+                Valuation valuation,
+                const LogicInfo& logicInfo,
+                ProofNodeManager* pnm);
   ~TheoryStrings();
   /** finish initialization */
   void finishInit() override;
@@ -76,7 +79,7 @@ class TheoryStrings : public Theory {
   /** Propagate */
   void propagate(Effort e) override;
   /** Explain */
-  Node explain(TNode literal) override;
+  TrustNode explain(TNode literal) override;
   /** Get the equality engine */
   eq::EqualityEngine* getEqualityEngine() override;
   /** Get current substitution */
@@ -95,7 +98,7 @@ class TheoryStrings : public Theory {
   /** preregister term */
   void preRegisterTerm(TNode n) override;
   /** Expand definition */
-  Node expandDefinition(Node n) override;
+  TrustNode expandDefinition(Node n) override;
   /** Check at effort e */
   void check(Effort e) override;
   /** needs check last effort */
@@ -105,7 +108,7 @@ class TheoryStrings : public Theory {
   /** called when a new equivalence class is created */
   void eqNotifyNewClass(TNode t);
   /** preprocess rewrite */
-  Node ppRewrite(TNode atom) override;
+  TrustNode ppRewrite(TNode atom) override;
   /**
    * Get all relevant information in this theory regarding the current
    * model. Return false if a contradiction is discovered.
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 9e72371d0..6fb739aa4 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -60,12 +60,14 @@ Theory::Theory(TheoryId id,
                OutputChannel& out,
                Valuation valuation,
                const LogicInfo& logicInfo,
+               ProofNodeManager* pnm,
                std::string name)
     : d_id(id),
       d_instanceName(name),
       d_satContext(satContext),
       d_userContext(userContext),
       d_logicInfo(logicInfo),
+      d_pnm(pnm),
       d_facts(satContext),
       d_factsHead(satContext, 0),
       d_sharedTermsIndex(satContext, 0),
diff --git a/src/theory/theory.h b/src/theory/theory.h
index a5234cf25..0cea604bf 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -43,12 +43,14 @@
 #include "theory/output_channel.h"
 #include "theory/theory_id.h"
 #include "theory/theory_rewriter.h"
+#include "theory/trust_node.h"
 #include "theory/valuation.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 
 class TheoryEngine;
+class ProofNodeManager;
 
 namespace theory {
 
@@ -105,6 +107,9 @@ class Theory {
   /** Information about the logic we're operating within. */
   const LogicInfo& d_logicInfo;
 
+  /** Pointer to proof node manager */
+  ProofNodeManager* d_pnm;
+
   /**
    * The assertFact() queue.
    *
@@ -199,6 +204,7 @@ class Theory {
          OutputChannel& out,
          Valuation valuation,
          const LogicInfo& logicInfo,
+         ProofNodeManager* pnm,
          std::string instance = "");  // taking : No default.
 
   /**
@@ -440,6 +446,19 @@ class Theory {
   virtual void finishInit() { }
 
   /**
+   * Expand definitions in the term node. This returns a term that is
+   * equivalent to node. It wraps this term in a TrustNode of kind
+   * TrustNodeKind::REWRITE. If node is unchanged by this method, the
+   * null TrustNode may be returned. This is an optimization to avoid
+   * constructing the trivial equality (= node node) internally within
+   * TrustNode.
+   *
+   * The purpose of this method is typically to eliminate the operators in node
+   * that are syntax sugar that cannot otherwise be eliminated during rewriting.
+   * For example, division relies on the introduction of an uninterpreted
+   * function for the divide-by-zero case, which we do not introduce with
+   * the rewriter, since this function may be cached in a non-global fashion.
+   *
    * Some theories have kinds that are effectively definitions and should be
    * expanded before they are handled.  Definitions allow a much wider range of
    * actions than the normal forms given by the rewriter. However no
@@ -453,10 +472,10 @@ class Theory {
    * a theory wants to be notified about a term before preprocessing
    * and simplification but doesn't necessarily want to rewrite it.
    */
-  virtual Node expandDefinition(Node node)
+  virtual TrustNode expandDefinition(Node node)
   {
     // by default, do nothing
-    return node;
+    return TrustNode::null();
   }
 
   /**
@@ -534,7 +553,8 @@ class Theory {
    * Return an explanation for the literal represented by parameter n
    * (which was previously propagated by this theory).
    */
-  virtual Node explain(TNode n) {
+  virtual TrustNode explain(TNode n)
+  {
     Unimplemented() << "Theory " << identify()
                     << " propagated a node but doesn't implement the "
                        "Theory::explain() interface!";
@@ -579,9 +599,12 @@ class Theory {
    * Given an atom of the theory coming from the input formula, this
    * method can be overridden in a theory implementation to rewrite
    * the atom into an equivalent form.  This is only called just
-   * before an input atom to the engine.
+   * before an input atom to the engine. This method returns a TrustNode of
+   * kind TrustNodeKind::REWRITE, which carries information about the proof
+   * generator for the rewrite. Similarly to expandDefinition, this method may
+   * return the null TrustNode if atom is unchanged.
    */
-  virtual Node ppRewrite(TNode atom) { return atom; }
+  virtual TrustNode ppRewrite(TNode atom) { return TrustNode::null(); }
 
   /**
    * Notify preprocessed assertions. Called on new assertions after
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0b84893ae..851ae414e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1402,7 +1402,8 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe
                              << " Responsible theory is: "
                              << theoryOf(atom)->getId() << std::endl;
 
-    Node explanation = theoryOf(atom)->explain(node);
+    TrustNode texplanation = theoryOf(atom)->explain(node);
+    Node explanation = texplanation.getNode();
     Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
     PROOF({
         if(proofRecipe) {
@@ -1877,7 +1878,8 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     }
     else
     {
-      explanation = theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
+      TrustNode texp = theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
+      explanation = texp.getNode();
       Debug("theory::explain") << "\tTerm was propagated by owner theory: "
                                << theoryOf(toExplain.d_theory)->getId()
                                << ". Explanation: " << explanation << std::endl;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index c29ba1b4d..59d6f9583 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -388,7 +388,8 @@ class TheoryEngine {
                                               d_userContext,
                                               *d_theoryOut[theoryId],
                                               theory::Valuation(this),
-                                              d_logicInfo);
+                                              d_logicInfo,
+                                              nullptr);
     theory::Rewriter::registerTheoryRewriter(
         theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
   }
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index d5a66ef9b..b12916b7d 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -201,7 +201,8 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
   unsigned nc = term.getNumChildren();
   if (nc == 0)
   {
-    return d_engine.theoryOf(term)->ppRewrite(term);
+    TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term);
+    return trn.isNull() ? Node(term) : trn.getNode();
   }
   Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
 
@@ -225,7 +226,8 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
     }
     newTerm = Rewriter::rewrite(Node(newNode));
   }
-  Node newTerm2 = d_engine.theoryOf(newTerm)->ppRewrite(newTerm);
+  TrustNode trn = d_engine.theoryOf(newTerm)->ppRewrite(newTerm);
+  Node newTerm2 = trn.isNull() ? newTerm : trn.getNode();
   if (newTerm != newTerm2)
   {
     newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2));
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 8334f29d1..5d47cef4a 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -20,6 +20,7 @@
 #include <memory>
 
 #include "expr/node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
@@ -45,8 +46,9 @@ TheoryUF::TheoryUF(context::Context* c,
                    OutputChannel& out,
                    Valuation valuation,
                    const LogicInfo& logicInfo,
+                   ProofNodeManager* pnm,
                    std::string instanceName)
-    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, instanceName),
+    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, pnm, instanceName),
       d_notify(*this),
       /* The strong theory solver can be notified by EqualityEngine::init(),
        * so make sure it's initialized first. */
@@ -61,6 +63,12 @@ TheoryUF::TheoryUF(context::Context* c,
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF, false, options::ufHo());
+
+  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
+  if (pc != nullptr)
+  {
+    d_ufProofChecker.registerTo(pc);
+  }
 }
 
 TheoryUF::~TheoryUF() {
@@ -159,7 +167,7 @@ void TheoryUF::check(Effort level) {
         }else{
           // support for cardinality constraints is not enabled, set incomplete
           d_out->setIncomplete();
-        } 
+        }
       }
       //needed for models
       if( options::produceModels() ){
@@ -201,7 +209,7 @@ unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) {
   return node.getKind()==kind::APPLY_UF ? 0 : 1;
 }
 
-Node TheoryUF::expandDefinition(Node node)
+TrustNode TheoryUF::expandDefinition(Node node)
 {
   Trace("uf-exp-def") << "TheoryUF::expandDefinition: expanding definition : "
                       << node << std::endl;
@@ -216,10 +224,10 @@ Node TheoryUF::expandDefinition(Node node)
     {
       Trace("uf-exp-def") << "TheoryUF::expandDefinition: higher-order: "
                           << node << " to " << ret << std::endl;
-      return ret;
+      return TrustNode::mkTrustRewrite(node, ret, nullptr);
     }
   }
-  return node;
+  return TrustNode::null();
 }
 
 void TheoryUF::preRegisterTerm(TNode node) {
@@ -304,8 +312,10 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro
   Debug("pf::uf") << std::endl;
 }
 
-Node TheoryUF::explain(TNode literal) {
-  return explain(literal, NULL);
+TrustNode TheoryUF::explain(TNode literal)
+{
+  Node exp = explain(literal, NULL);
+  return TrustNode::mkTrustPropExp(literal, exp, nullptr);
 }
 
 Node TheoryUF::explain(TNode literal, eq::EqProof* pf) {
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index a3e908b1f..58f4f18a5 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -25,6 +25,7 @@
 #include "expr/node_trie.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/uf/proof_checker.h"
 #include "theory/uf/symmetry_breaker.h"
 #include "theory/uf/theory_uf_rewriter.h"
 
@@ -183,8 +184,12 @@ private:
  public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out,
-           Valuation valuation, const LogicInfo& logicInfo,
+  TheoryUF(context::Context* c,
+           context::UserContext* u,
+           OutputChannel& out,
+           Valuation valuation,
+           const LogicInfo& logicInfo,
+           ProofNodeManager* pnm = nullptr,
            std::string instanceName = "");
 
   ~TheoryUF();
@@ -195,9 +200,9 @@ private:
   void finishInit() override;
 
   void check(Effort) override;
-  Node expandDefinition(Node node) override;
+  TrustNode expandDefinition(Node node) override;
   void preRegisterTerm(TNode term) override;
-  Node explain(TNode n) override;
+  TrustNode explain(TNode n) override;
 
   bool collectModelInfo(TheoryModel* m) override;
 
@@ -228,6 +233,8 @@ private:
                     unsigned depth);
 
   TheoryUfRewriter d_rewriter;
+  /** Proof rule checker */
+  UfProofRuleChecker d_ufProofChecker;
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 369447249..5a16fdc20 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -118,8 +118,9 @@ class FakeTheory : public Theory
              context::UserContext* uctxt,
              OutputChannel& out,
              Valuation valuation,
-             const LogicInfo& logicInfo)
-      : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo)
+             const LogicInfo& logicInfo,
+             ProofNodeManager* pnm)
+      : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, pnm)
   {
   }
 
@@ -155,10 +156,10 @@ class FakeTheory : public Theory
   void registerTerm(TNode) { Unimplemented(); }
   void check(Theory::Effort) override { Unimplemented(); }
   void propagate(Theory::Effort) override { Unimplemented(); }
-  Node explain(TNode) override
+  TrustNode explain(TNode) override
   {
     Unimplemented();
-    return Node::null();
+    return TrustNode::null();
   }
   Node getValue(TNode n) { return Node::null(); }
 
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 2722c4df9..0ff4e918b 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -97,9 +97,14 @@ class DummyTheory : public Theory {
   set<Node> d_registered;
   vector<Node> d_getSequence;
 
-  DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out,
-              Valuation valuation, const LogicInfo& logicInfo)
-      : Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo)
+  DummyTheory(Context* ctxt,
+              UserContext* uctxt,
+              OutputChannel& out,
+              Valuation valuation,
+              const LogicInfo& logicInfo,
+              ProofNodeManager* pnm)
+      : Theory(
+            theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, pnm)
   {}
 
   TheoryRewriter* getTheoryRewriter() { return nullptr; }
@@ -136,7 +141,7 @@ class DummyTheory : public Theory {
   void presolve() override { Unimplemented(); }
   void preRegisterTerm(TNode n) override {}
   void propagate(Effort level) override {}
-  Node explain(TNode n) override { return Node::null(); }
+  TrustNode explain(TNode n) override { return TrustNode::null(); }
   Node getValue(TNode n) { return Node::null(); }
   string identify() const override { return "DummyTheory"; }
 };/* class DummyTheory */
@@ -180,8 +185,12 @@ class TheoryBlack : public CxxTest::TestSuite {
     d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL;
     d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL;
 
-    d_dummy = new DummyTheory(
-        d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo);
+    d_dummy = new DummyTheory(d_ctxt,
+                              d_uctxt,
+                              d_outputChannel,
+                              Valuation(NULL),
+                              *d_logicInfo,
+                              nullptr);
     d_outputChannel.clear();
     atom0 = d_nm->mkConst(true);
     atom1 = d_nm->mkConst(false);