Merge branch 'stringsPf' into fix-eqproof4

30 files changed, 966 insertions, 557 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2ac73f067..f5be109ed 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -450,8 +450,6 @@ libcvc4_add_sources(
   theory/logic_info.cpp
   theory/logic_info.h
   theory/output_channel.h
-  theory/proof_engine_output_channel.cpp
-  theory/proof_engine_output_channel.h
   theory/quantifiers/alpha_equivalence.cpp
   theory/quantifiers/alpha_equivalence.h
   theory/quantifiers/anti_skolem.cpp
@@ -748,6 +746,8 @@ libcvc4_add_sources(
   theory/theory.h
   theory/theory_engine.cpp
   theory/theory_engine.h
+  theory/theory_engine_proof_generator.cpp
+  theory/theory_engine_proof_generator.h
   theory/theory_id.cpp
   theory/theory_id.h
   theory/theory_model.cpp
diff --git a/src/README b/src/README
index c7a940837..1de6ac991 100644
--- a/src/README
+++ b/src/README
@@ -80,7 +80,6 @@ PRs:
 (6) Split EngineOutputChannel from TheoryEngine to its own file
 (7) Add LazyCDProof and ProofGenerator
 (8) Add TrustNode
-(9) Add ProofEngineOutputChannel
 - Add EagerProofGenerator
 (10) ProofEqEngine 
 (11) TheoryEngine proof checker initialize
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index 8ec55d1f5..15e996684 100644
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -381,4 +381,11 @@ bool CDProof::isAssumption(ProofNode* pn)
   return false;
 }
 
+bool CDProof::isSame(TNode f, TNode g)
+{
+  return f == g
+         || (f.getKind() == EQUAL && g.getKind() == EQUAL && f[0] == g[1]
+             && f[1] == g[0]);
+}
+
 }  // namespace CVC4
diff --git a/src/expr/proof.h b/src/expr/proof.h
index e5b2775d9..2ff3604f8 100644
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -206,6 +206,13 @@ class CDProof
   /** 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);
+
  protected:
   typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
       NodeProofNodeMap;
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index f15e43553..f1ec78aab 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -60,6 +60,103 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact)
   return mkNode(PfRule::ASSUME, children, args, fact);
 }
 
+std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
+    std::shared_ptr<ProofNode> pf,
+    std::vector<Node>& assumps,
+    bool ensureClosed)
+{
+  std::vector<std::shared_ptr<ProofNode>> pfChildren;
+  pfChildren.push_back(pf);
+  if (!ensureClosed)
+  {
+    return mkNode(PfRule::SCOPE, pfChildren, assumps);
+  }
+  Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl;
+  // we first ensure the assumptions are flattened
+  std::unordered_set<Node, NodeHashFunction> ac;
+  for (const TNode& a : assumps)
+  {
+    if (a.getKind() == AND)
+    {
+      ac.insert(a.begin(), a.end());
+    }
+    else
+    {
+      ac.insert(a);
+    }
+  }
+  // The free assumptions of the proof
+  std::map<Node, std::vector<ProofNode*>> famap;
+  pf->getFreeAssumptionsMap(famap);
+  std::unordered_set<Node, NodeHashFunction> acu;
+  std::unordered_set<Node, NodeHashFunction>::iterator itf;
+  for (const std::pair<const Node, std::vector<ProofNode*>>& fa : famap)
+  {
+    Node a = fa.first;
+    if (ac.find(a) != ac.end())
+    {
+      // already covered by an assumption
+      acu.insert(a);
+      continue;
+    }
+    // otherwise it may be due to symmetry?
+    bool polarity = a.getKind() != NOT;
+    Node aeq = polarity ? a : a[0];
+    if (aeq.getKind() == EQUAL)
+    {
+      Node aeqSym = aeq[1].eqNode(aeq[0]);
+      aeqSym = polarity ? aeqSym : aeqSym.notNode();
+      itf = ac.find(aeqSym);
+      if (itf != ac.end())
+      {
+        Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a
+                           << " for " << fa.second.size() << " proof nodes"
+                           << std::endl;
+        std::shared_ptr<ProofNode> pfaa = mkAssume(aeqSym);
+        for (ProofNode* pfs : fa.second)
+        {
+          Assert(pfs->getResult() == a);
+          // must correct the orientation on this leaf
+          std::vector<std::shared_ptr<ProofNode>> children;
+          children.push_back(pfaa);
+          std::vector<Node> args;
+          args.push_back(a);
+          updateNode(pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+        }
+        Trace("pnm-scope") << "...finished" << std::endl;
+        acu.insert(aeqSym);
+        continue;
+      }
+    }
+    // All free assumptions should be arguments to SCOPE.
+    std::stringstream ss;
+    pf->printDebug(ss);
+    ss << std::endl << "Free assumption: " << a << std::endl;
+    for (const Node& aprint : ac)
+    {
+      ss << "- assumption: " << aprint << std::endl;
+    }
+    AlwaysAssert(false) << "Generated a proof that is not closed by the scope: "
+                        << ss.str() << std::endl;
+  }
+  if (acu.size() < ac.size())
+  {
+    // All assumptions should match a free assumption; if one does not, then
+    // the explanation could have been smaller.
+    for (const Node& a : ac)
+    {
+      if (acu.find(a) == acu.end())
+      {
+        Notice() << "ProofNodeManager::mkScope: assumption " << a
+                 << " does not match a free assumption in proof" << std::endl;
+      }
+    }
+  }
+  assumps.clear();
+  assumps.insert(assumps.end(), acu.begin(), acu.end());
+  return mkNode(PfRule::SCOPE, pfChildren, assumps);
+}
+
 bool ProofNodeManager::updateNode(
     ProofNode* pn,
     PfRule id,
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 9904a78ec..527f2562d 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -80,6 +80,11 @@ class ProofNodeManager
                                     Node expected = Node::null());
   /** Make assume */
   std::shared_ptr<ProofNode> mkAssume(Node fact);
+  /** Make scope */
+  std::shared_ptr<ProofNode> mkScope(std::shared_ptr<ProofNode> pf,
+                                     std::vector<Node>& assumps,
+                                     bool ensureClosed = true);
+
   /**
    * This method updates pn to be a proof of the form <id>( children, args ),
    * while maintaining its d_proven field. This method returns false if this
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 38c99f551..2c6d22d27 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -79,7 +79,9 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   LemmaProofRecipe* proofRecipe = NULL;
   PROOF(proofRecipe = new LemmaProofRecipe;);
 
-  Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe);
+  theory::TrustNode tte =
+      d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe);
+  Node theoryExplanation = tte.getNode();
 
   PROOF({
       ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index ddc222ffb..8c47bc060 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -22,23 +22,30 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace theory {
 
-const char* toString(RewriterId id)
+const char* toString(MethodId id)
 {
   switch (id)
   {
-    case RewriterId::REWRITE: return "REWRITE";
-    case RewriterId::REWRITE_EQ_EXT: return "REWRITE_EQ_EXT";
-    case RewriterId::IDENTITY: return "IDENTITY";
-    default: return "RewriterId::Unknown";
+    case MethodId::RW_REWRITE: return "RW_REWRITE";
+    case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT";
+    case MethodId::RW_IDENTITY: return "RW_IDENTITY";
+    case MethodId::SB_DEFAULT: return "SB_DEFAULT";
+    case MethodId::SB_PREDICATE: return "SB_PREDICATE";
+    default: return "MethodId::Unknown";
   };
 }
 
-std::ostream& operator<<(std::ostream& out, RewriterId id)
+std::ostream& operator<<(std::ostream& out, MethodId id)
 {
   out << toString(id);
   return out;
 }
 
+Node mkMethodId(MethodId id)
+{
+  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
+}
+
 namespace builtin {
 
 void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
@@ -55,109 +62,131 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::THEORY_LEMMA, nullptr);
 }
 
-Node BuiltinProofRuleChecker::applyRewrite(Node n, RewriterId id)
+Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
 {
   Node nk = ProofSkolemCache::getSkolemForm(n);
-  Node nkr = applyRewriteExternal(n, id);
+  Node nkr = applyRewriteExternal(n, idr);
   return ProofSkolemCache::getWitnessForm(nkr);
 }
 
-Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp)
+Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
 {
   if (exp.isNull() || exp.getKind() != EQUAL)
   {
     return Node::null();
   }
   Node nk = ProofSkolemCache::getSkolemForm(n);
-  Node nks = applySubstitutionExternal(nk, exp);
+  Node nks = applySubstitutionExternal(nk, exp, ids);
   return ProofSkolemCache::getWitnessForm(nks);
 }
 
 Node BuiltinProofRuleChecker::applySubstitution(Node n,
-                                                const std::vector<Node>& exp)
+                                                const std::vector<Node>& exp,
+                                                MethodId ids)
 {
   Node nk = ProofSkolemCache::getSkolemForm(n);
-  Node nks = applySubstitutionExternal(nk, exp);
+  Node nks = applySubstitutionExternal(nk, exp, ids);
   return ProofSkolemCache::getWitnessForm(nks);
 }
 
 Node BuiltinProofRuleChecker::applySubstitutionRewrite(
-    Node n, const std::vector<Node>& exp, RewriterId id)
+    Node n, const std::vector<Node>& exp, MethodId ids, MethodId idr)
 {
   Node nk = ProofSkolemCache::getSkolemForm(n);
-  Node nks = applySubstitutionExternal(nk, exp);
-  Node nksr = applyRewriteExternal(nks, id);
+  Node nks = applySubstitutionExternal(nk, exp, ids);
+  Node nksr = applyRewriteExternal(nks, idr);
   return ProofSkolemCache::getWitnessForm(nksr);
 }
 
-Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, RewriterId id)
+Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr)
 {
   Trace("builtin-pfcheck-debug")
-      << "applyRewriteExternal (" << id << "): " << n << std::endl;
+      << "applyRewriteExternal (" << idr << "): " << n << std::endl;
   // index determines the kind of rewriter
-  if (id == RewriterId::REWRITE)
+  if (idr == MethodId::RW_REWRITE)
   {
     return Rewriter::rewrite(n);
   }
-  else if (id == RewriterId::REWRITE_EQ_EXT)
+  else if (idr == MethodId::RW_REWRITE_EQ_EXT)
   {
     Node ret = Rewriter::rewriteEqualityExt(n);
     // also rewrite
     return Rewriter::rewrite(ret);
   }
-  else if (id == RewriterId::IDENTITY)
+  else if (idr == MethodId::RW_IDENTITY)
   {
     // does nothing
     return n;
   }
   // unknown rewriter
   Assert(false)
-      << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for " << id
-      << std::endl;
+      << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for "
+      << idr << std::endl;
   return n;
 }
 
-Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n, Node exp)
+Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n,
+                                                        Node exp,
+                                                        MethodId ids)
 {
-  Assert(!exp.isNull() && exp.getKind() == EQUAL);
+  Assert(!exp.isNull());
   Node expk = ProofSkolemCache::getSkolemForm(exp);
-  TNode var = expk[0];
-  TNode subs = expk[1];
+  TNode var, subs;
+  if (ids == MethodId::SB_DEFAULT)
+  {
+    if (expk.getKind() != EQUAL)
+    {
+      return Node::null();
+    }
+    var = expk[0];
+    subs = expk[1];
+  }
+  else if (ids == MethodId::SB_PREDICATE)
+  {
+    bool polarity = expk.getKind() != NOT;
+    var = polarity ? expk : expk[0];
+    subs = NodeManager::currentNM()->mkConst(polarity);
+  }
+  else
+  {
+    Assert(false) << "BuiltinProofRuleChecker::applySubstitutionExternal: no "
+                     "substitution for "
+                  << ids << std::endl;
+  }
   return n.substitute(var, subs);
 }
 
 Node BuiltinProofRuleChecker::applySubstitutionExternal(
-    Node n, const std::vector<Node>& exp)
+    Node n, const std::vector<Node>& exp, MethodId ids)
 {
   Node curr = n;
   // apply substitution one at a time, in reverse order
   for (size_t i = 0, nexp = exp.size(); i < nexp; i++)
   {
-    if (exp[nexp - 1 - i].isNull() || exp[nexp - 1 - i].getKind() != EQUAL)
+    if (exp[nexp - 1 - i].isNull())
     {
       return Node::null();
     }
-    curr = applySubstitutionExternal(curr, exp[nexp - 1 - i]);
+    curr = applySubstitutionExternal(curr, exp[nexp - 1 - i], ids);
+    if (curr.isNull())
+    {
+      break;
+    }
   }
   return curr;
 }
 
-bool BuiltinProofRuleChecker::getRewriterId(TNode n, RewriterId& i)
+bool BuiltinProofRuleChecker::getMethodId(TNode n, MethodId& i)
 {
   uint32_t index;
   if (!getIndex(n, index))
   {
     return false;
   }
-  i = static_cast<RewriterId>(index);
+  i = static_cast<MethodId>(index);
   return true;
 }
 
-Node BuiltinProofRuleChecker::mkRewriterId(RewriterId i)
-{
-  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(i)));
-}
-
 Node BuiltinProofRuleChecker::checkInternal(PfRule id,
                                             const std::vector<Node>& children,
                                             const std::vector<Node>& args)
@@ -189,7 +218,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
   else if (id == PfRule::SUBS)
   {
     Assert(children.size() > 0);
-    Assert(args.size() == 1);
+    Assert(1 <= args.size() && args.size() <= 2);
+    MethodId ids = MethodId::SB_DEFAULT;
+    if (args.size() == 2 && !getMethodId(args[1], ids))
+    {
+      return Node::null();
+    }
     std::vector<Node> exp;
     for (size_t i = 0, nchild = children.size(); i < nchild; i++)
     {
@@ -201,7 +235,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
   else if (id == PfRule::REWRITE)
   {
     Assert(children.empty());
-    Assert(args.size() == 1);
+    Assert(1 <= args.size() && args.size() <= 2);
+    MethodId ids = MethodId::RW_REWRITE;
+    if (args.size() == 2 && !getMethodId(args[1], ids))
+    {
+      return Node::null();
+    }
     Node res = applyRewrite(args[0]);
     return args[0].eqNode(res);
   }
@@ -211,18 +250,13 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     // (TRANS
     //   (SUBS P1 ... Pn t)
     //   (REWRITE <t.substitute(xn,tn). ... .substitute(x1,t1)>))
-    Assert(1 <= args.size() && args.size() <= 2);
-    RewriterId idRewriter = RewriterId::REWRITE;
-    if (args.size() >= 2)
+    Assert(1 <= args.size() && args.size() <= 3);
+    MethodId ids, idr;
+    if (!getMethodIds(args, ids, idr, 1))
     {
-      if (!getRewriterId(args[1], idRewriter))
-      {
-        Trace("builtin-pfcheck")
-            << "Failed to get id from " << args[1] << std::endl;
-        return Node::null();
-      }
+      return Node::null();
     }
-    Node res = applySubstitutionRewrite(args[0], children, idRewriter);
+    Node res = applySubstitutionRewrite(args[0], children, idr);
     return args[0].eqNode(res);
   }
   else if (id == PfRule::MACRO_SR_PRED_INTRO)
@@ -232,18 +266,13 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     // NOTE: technically a macro:
     // (TRUE_ELIM
     //   (MACRO_SR_EQ_INTRO <children> <args>[0]))
-    Assert(1 <= args.size() && args.size() <= 2);
-    RewriterId idRewriter = RewriterId::REWRITE;
-    if (args.size() >= 2)
+    Assert(1 <= args.size() && args.size() <= 3);
+    MethodId ids, idr;
+    if (!getMethodIds(args, ids, idr, 1))
     {
-      if (!getRewriterId(args[1], idRewriter))
-      {
-        Trace("builtin-pfcheck")
-            << "Failed to get id from " << args[1] << std::endl;
-        return Node::null();
-      }
+      return Node::null();
     }
-    Node res = applySubstitutionRewrite(args[0], children, idRewriter);
+    Node res = applySubstitutionRewrite(args[0], children, ids, idr);
     if (res.isNull())
     {
       return Node::null();
@@ -264,7 +293,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
                              << args.size() << std::endl;
     Assert(children.size() >= 1);
-    Assert(args.size() <= 1);
+    Assert(args.size() <= 2);
     // NOTE: technically a macro:
     // (TRUE_ELIM
     //   (TRANS
@@ -272,17 +301,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     //     (TRUE_INTRO <children>[0])))
     std::vector<Node> exp;
     exp.insert(exp.end(), children.begin() + 1, children.end());
-    RewriterId idRewriter = RewriterId::REWRITE;
-    if (0 < args.size())
+    MethodId ids, idr;
+    if (!getMethodIds(args, ids, idr, 0))
     {
-      if (!getRewriterId(args[0], idRewriter))
-      {
-        Trace("builtin-pfcheck")
-            << "Failed to get id from " << args[0] << std::endl;
-        return Node::null();
-      }
+      return Node::null();
     }
-    Node res1 = applySubstitutionRewrite(children[0], exp, idRewriter);
+    Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr);
     Trace("builtin-pfcheck") << "Returned " << res1 << std::endl;
     return res1;
   }
@@ -291,24 +315,19 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
                              << args.size() << std::endl;
     Assert(children.size() >= 1);
-    Assert(args.size() <= 2);
+    Assert(1 <= args.size() && args.size() <= 3);
     Assert(args[0].getType().isBoolean());
-    std::vector<Node> exp;
-    exp.insert(exp.end(), children.begin() + 1, children.end());
-    RewriterId idRewriter = RewriterId::REWRITE;
-    if (1 < args.size())
+    MethodId ids, idr;
+    if (!getMethodIds(args, ids, idr, 1))
     {
-      if (!getRewriterId(args[1], idRewriter))
-      {
-        Trace("builtin-pfcheck")
-            << "Failed to get id from " << args[1] << std::endl;
-        return Node::null();
-      }
+      return Node::null();
     }
-    Node res1 = applySubstitutionRewrite(children[0], exp, idRewriter);
+    std::vector<Node> exp;
+    exp.insert(exp.end(), children.begin() + 1, children.end());
+    Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr);
     // Trace("builtin-pfcheck")
     //    << "Returned " << res1 << std::endl;
-    Node res2 = applySubstitutionRewrite(args[0], exp, idRewriter);
+    Node res2 = applySubstitutionRewrite(args[0], exp, ids, idr);
     // Trace("builtin-pfcheck")
     //    << "Returned " << res2 << " from " << args[0] << std::endl;
     // can rewrite the witness forms
@@ -334,6 +353,34 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
   return Node::null();
 }
 
+bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args,
+                                           MethodId& ids,
+                                           MethodId& idr,
+                                           size_t index)
+{
+  ids = MethodId::SB_DEFAULT;
+  idr = MethodId::RW_REWRITE;
+  if (args.size() > index)
+  {
+    if (!getMethodId(args[index], ids))
+    {
+      Trace("builtin-pfcheck")
+          << "Failed to get id from " << args[index] << std::endl;
+      return false;
+    }
+  }
+  if (args.size() > index + 1)
+  {
+    if (!getMethodId(args[index + 1], idr))
+    {
+      Trace("builtin-pfcheck")
+          << "Failed to get id from " << args[index + 1] << std::endl;
+      return false;
+    }
+  }
+  return true;
+}
+
 }  // namespace builtin
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 7c6f29354..afd9bad5a 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -24,26 +24,36 @@
 namespace CVC4 {
 namespace theory {
 
-/** Identifiers for rewriters.
+/** Identifiers for rewriters and substitutions.
  *
  * A "rewriter" is abstractly a method from Node to Node, where the output
  * is semantically equivalent to the input. The identifiers below list
  * various methods that have this contract. This identifier is used
  * in a number of the builtin rules.
+ *
+ * A substitution is a method for turning a formula into
  */
-enum class RewriterId : uint32_t
+enum class MethodId : uint32_t
 {
+  //---------------------------- Rewriters
   // Rewriter::rewrite(n)
-  REWRITE,
+  RW_REWRITE,
   // Rewriter::rewriteExtEquality(n)
-  REWRITE_EQ_EXT,
+  RW_REWRITE_EQ_EXT,
   // identity
-  IDENTITY,
+  RW_IDENTITY,
+  //---------------------------- Substitutions
+  // (= x y) is interpreted as x -> y, using Node::substitute(...)
+  SB_DEFAULT,
+  // (= x y) is interpreted as (= x y) -> true, using Node::substitute(...)
+  SB_PREDICATE,
 };
 /** Converts a rewriter id to a string. */
-const char* toString(RewriterId id);
+const char* toString(MethodId id);
 /** Write a rewriter id to out */
-std::ostream& operator<<(std::ostream& out, RewriterId id);
+std::ostream& operator<<(std::ostream& out, MethodId id);
+/** Make a method id node */
+Node mkMethodId(MethodId id);
 
 namespace builtin {
 
@@ -62,7 +72,7 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    * @param id The identifier of the rewriter.
    * @return The rewritten form of n.
    */
-  static Node applyRewrite(Node n, RewriterId id = RewriterId::REWRITE);
+  static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
   /**
    * Apply substitution on n (in witness form). This encapsulates the exact
    * behavior of a SUBS step in a proof. Substitution is on the Skolem form of
@@ -73,8 +83,12 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    * substitution
    * @return The substituted form of n.
    */
-  static Node applySubstitution(Node n, Node exp);
-  static Node applySubstitution(Node n, const std::vector<Node>& exp);
+  static Node applySubstitution(Node n,
+                                Node exp,
+                                MethodId ids = MethodId::SB_DEFAULT);
+  static Node applySubstitution(Node n,
+                                const std::vector<Node>& exp,
+                                MethodId ids = MethodId::SB_DEFAULT);
   /** Apply substitution + rewriting
    *
    * Combines the above two steps.
@@ -87,11 +101,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    */
   static Node applySubstitutionRewrite(Node n,
                                        const std::vector<Node>& exp,
-                                       RewriterId id = RewriterId::REWRITE);
+                                       MethodId ids = MethodId::SB_DEFAULT,
+                                       MethodId idr = MethodId::RW_REWRITE);
   /** get a rewriter Id from a node, return false if we fail */
-  static bool getRewriterId(TNode n, RewriterId& i);
-  /** Make a rewriter id node */
-  static Node mkRewriterId(RewriterId i);
+  static bool getMethodId(TNode n, MethodId& i);
 
   /** Register all rules owned by this rule checker into pc. */
   void registerTo(ProofChecker* pc) override;
@@ -101,17 +114,24 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
   Node checkInternal(PfRule id,
                      const std::vector<Node>& children,
                      const std::vector<Node>& args) override;
+  /** get method ids */
+  bool getMethodIds(const std::vector<Node>& args,
+                    MethodId& ids,
+                    MethodId& idr,
+                    size_t index);
   /**
    * Apply rewrite (on Skolem form). id is the identifier of the rewriter.
    */
-  static Node applyRewriteExternal(Node n, RewriterId id = RewriterId::REWRITE);
+  static Node applyRewriteExternal(Node n, MethodId idr = MethodId::RW_REWRITE);
   /**
    * Apply substitution for n (on Skolem form), where exp is an equality
    * (or set of equalities) in Witness form. Returns the result of
    * n * { exp[0] -> exp[1] } in Skolem form.
    */
-  static Node applySubstitutionExternal(Node n, Node exp);
-  static Node applySubstitutionExternal(Node n, const std::vector<Node>& exp);
+  static Node applySubstitutionExternal(Node n, Node exp, MethodId ids);
+  static Node applySubstitutionExternal(Node n,
+                                        const std::vector<Node>& exp,
+                                        MethodId ids);
 };
 
 }  // namespace builtin
diff --git a/src/theory/builtin/proof_kinds b/src/theory/builtin/proof_kinds
index 404dfbc06..eb9643ec3 100644
--- a/src/theory/builtin/proof_kinds
+++ b/src/theory/builtin/proof_kinds
@@ -38,7 +38,7 @@ proofrule SCOPE 1 1: ::CVC4::theory::builtin::BuiltinProofRuleChecker
 
 // ======== Substitution
 // Children: (P1:(= x1 t1), ..., Pn:(= xn tn))
-// Arguments: (t)
+// Arguments: (t, id?)
 // ---------------------------------------------------------------
 // Conclusion: (= t t.substitute(xn,tn). ... .substitute(x1,t1))
 // Notice that the orientation of the premises matters.
@@ -46,7 +46,7 @@ proofrule SUBS 1: 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker
 
 // ======== Rewrite
 // Children: none
-// Arguments: (t)
+// Arguments: (t, id?)
 // ----------------------------------------
 // Conclusion: (= t Rewriter::rewrite(t))
 proofrule REWRITE 0 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker
diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp
index c2080f20e..0dc87e6ba 100644
--- a/src/theory/eager_proof_generator.cpp
+++ b/src/theory/eager_proof_generator.cpp
@@ -15,7 +15,6 @@
 #include "theory/eager_proof_generator.h"
 
 #include "expr/proof_node_manager.h"
-#include "theory/proof_engine_output_channel.h"
 
 namespace CVC4 {
 namespace theory {
@@ -30,7 +29,7 @@ void EagerProofGenerator::setProofForConflict(Node conf,
                                               std::shared_ptr<ProofNode> pf)
 {
   // Normalize based on key
-  Node ckey = TrustNode::getConflictKeyValue(conf);
+  Node ckey = TrustNode::getConflictProven(conf);
   d_proofs[ckey] = pf;
 }
 
@@ -38,7 +37,7 @@ void EagerProofGenerator::setProofForLemma(Node lem,
                                            std::shared_ptr<ProofNode> pf)
 {
   // Normalize based on key
-  Node lkey = TrustNode::getLemmaKeyValue(lem);
+  Node lkey = TrustNode::getLemmaProven(lem);
   d_proofs[lkey] = pf;
 }
 
@@ -47,7 +46,7 @@ void EagerProofGenerator::setProofForPropExp(TNode lit,
                                              std::shared_ptr<ProofNode> pf)
 {
   // Normalize based on key
-  Node pekey = TrustNode::getPropExpKeyValue(lit, exp);
+  Node pekey = TrustNode::getPropExpProven(lit, exp);
   d_proofs[pekey] = pf;
 }
 
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index 176d08acf..9e4e56543 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -298,5 +298,26 @@ void EngineOutputChannel::handleUserAttribute(const char* attr,
   d_engine->handleUserAttribute(attr, t);
 }
 
+void EngineOutputChannel::trustedConflict(TrustNode pconf)
+{
+  Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
+  d_engine->processTrustNode(pconf, d_theory);
+  TNode conf = pconf.getNode();
+  // now, call the normal interface to conflict
+  conflict(conf);
+}
+
+LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem,
+                                              bool removable,
+                                              bool preprocess,
+                                              bool sendAtoms)
+{
+  Assert(plem.getKind() == TrustNodeKind::LEMMA);
+  d_engine->processTrustNode(plem, d_theory);
+  TNode lem = plem.getNode();
+  // now, call the normal interface for lemma
+  return OutputChannel::lemma(lem, removable, preprocess, sendAtoms);
+}
+
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index 1699795a1..2d07d3f63 100644
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -31,6 +31,10 @@ namespace theory {
 /**
  * An output channel for Theory that passes messages back to a TheoryEngine
  * for a given Theory.
+ *
+ * Notice that is has interfaces trustedConflict and trustedLemma which are
+ * used for ensuring that proof generators are associated with the lemmas
+ * and conflicts sent on this output channel.
  */
 class EngineOutputChannel : public theory::OutputChannel
 {
@@ -63,6 +67,27 @@ class EngineOutputChannel : public theory::OutputChannel
 
   void handleUserAttribute(const char* attr, theory::Theory* t) override;
 
+  /**
+   * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method
+   * sends conf on the output channel of this class whose proof can be generated
+   * by the generator pfg. It calls TheoryEngine::processTrustNode,
+   * which ensures that the generator pfg is associated with conf in the
+   * lazy proof owned by the theory engine of this class.
+   */
+  void trustedConflict(TrustNode pconf) override;
+  /**
+   * Let plem be the pair (Node lem, ProofGenerator * pfg).
+   * Send lem on the output channel of this class whose proof can be generated
+   * by the generator pfg. Apart from pfg, the interface for this method is
+   * the same as OutputChannel. It calls TheoryEngine::processTrustNode,
+   * which ensures that the generator pfg is associated with lem in the
+   * lazy proof owned by the theory engine of this class.
+   */
+  LemmaStatus trustedLemma(TrustNode plem,
+                           bool removable = false,
+                           bool preprocess = false,
+                           bool sendAtoms = false) override;
+
  protected:
   /**
    * Statistics for a particular theory.
diff --git a/src/theory/proof_engine_output_channel.cpp b/src/theory/proof_engine_output_channel.cpp
deleted file mode 100644
index 4f35a7639..000000000
--- a/src/theory/proof_engine_output_channel.cpp
+++ /dev/null
@@ -1,100 +0,0 @@
-/*********************                                                        */
-/*! \file proof_engine_output_channel.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The Evaluator class
- **
- ** The Evaluator class.
- **/
-
-#include "theory/proof_engine_output_channel.h"
-
-#include "expr/lazy_proof.h"
-
-namespace CVC4 {
-namespace theory {
-
-ProofEngineOutputChannel::ProofEngineOutputChannel(TheoryEngine* engine,
-                                                   theory::TheoryId theory,
-                                                   LazyCDProof* lpf)
-    : EngineOutputChannel(engine, theory), d_lazyPf(lpf)
-{
-}
-void ProofEngineOutputChannel::trustedConflict(TrustNode pconf)
-{
-  Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
-  Node conf = pconf.getNode();
-  if (d_lazyPf != nullptr)
-  {
-    Node ckey = TrustNode::getConflictKeyValue(conf);
-    ProofGenerator* pfg = pconf.getGenerator();
-    // may or may not have supplied a generator
-    if (pfg != nullptr)
-    {
-      ++d_statistics.trustedConflicts;
-      // if we have, add it to the lazy proof object
-      d_lazyPf->addLazyStep(ckey, pfg);
-      Assert(pfg->hasProofFor(ckey));
-    }
-    else
-    {
-      // if none provided, do a very coarse-grained step
-      addTheoryLemmaStep(ckey);
-    }
-  }
-  // now, call the normal interface to conflict
-  conflict(conf);
-}
-
-LemmaStatus ProofEngineOutputChannel::trustedLemma(TrustNode plem,
-                                                   bool removable,
-                                                   bool preprocess,
-                                                   bool sendAtoms)
-{
-  Assert(plem.getKind() == TrustNodeKind::LEMMA);
-  TNode lem = plem.getNode();
-  ProofGenerator* pfg = plem.getGenerator();
-  if (d_lazyPf != nullptr)
-  {
-    Node lkey = TrustNode::getLemmaKeyValue(lem);
-    // may or may not have supplied a generator
-    if (pfg != nullptr)
-    {
-      ++d_statistics.trustedLemmas;
-      // if we have, add it to the lazy proof object
-      d_lazyPf->addLazyStep(lkey, pfg);
-      Assert(pfg->hasProofFor(lkey));
-    }
-    else
-    {
-      // if none provided, do a very coarse-grained step
-      addTheoryLemmaStep(lkey);
-    }
-  }
-  // now, call the normal interface for lemma
-  return OutputChannel::lemma(lem, removable, preprocess, sendAtoms);
-}
-
-bool ProofEngineOutputChannel::addTheoryLemmaStep(Node f)
-{
-  Assert(d_lazyPf != nullptr);
-  Assert(!f.isNull());
-  std::vector<Node> children;
-  std::vector<Node> args;
-  args.push_back(f);
-  unsigned tid = static_cast<unsigned>(d_theory);
-  Node tidn = NodeManager::currentNM()->mkConst(Rational(tid));
-  args.push_back(tidn);
-  // add the step, should always succeed;
-  return d_lazyPf->addStep(f, PfRule::THEORY_LEMMA, children, args);
-}
-
-}  // namespace theory
-}  // namespace CVC4
diff --git a/src/theory/proof_engine_output_channel.h b/src/theory/proof_engine_output_channel.h
deleted file mode 100644
index 1b1beb84d..000000000
--- a/src/theory/proof_engine_output_channel.h
+++ /dev/null
@@ -1,99 +0,0 @@
-/*********************                                                        */
-/*! \file proof_engine_output_channel.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The proof output channel class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__PROOF_ENGINE_OUTPUT_CHANNEL_H
-#define CVC4__THEORY__PROOF_ENGINE_OUTPUT_CHANNEL_H
-
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-#include "theory/engine_output_channel.h"
-
-namespace CVC4 {
-
-class LazyCDProof;
-
-namespace theory {
-
-/**
- * TODO: merge with engine output channel
- *
- * A layer on top of an output channel to ensure proofs are constructed and
- * available for conflicts and lemmas that may require proofs. It is
- * intended to be owned by TheoryEngine and passed as reference to each of
- * its Theory solvers. Its use can be summarized in two parts:
- *
- * (1) Theory objects should use the output calls to methods in this class,
- * e.g. trustedConflict(...), trustedLemma(...).
- *
- * (2) This class is responsible for adding proof steps to the provide proof
- * object that correspond to steps.
- *
- * It is implemented by requiring that calls to conflict(...) provide an
- * pointer to a proof generator object, as part of the TrustNode pair.
- *
- * In more detail, when a call to
- *   ProofOutputChannel::trustedConflict(TrustNode(conf, pfg))
- * is made
- */
-class ProofEngineOutputChannel : public EngineOutputChannel
-{
-  typedef context::CDHashMap<Node, ProofGenerator*, NodeHashFunction>
-      NodeProofGenMap;
-
- public:
-  ProofEngineOutputChannel(TheoryEngine* engine,
-                           theory::TheoryId theory,
-                           LazyCDProof* lpf);
-  ~ProofEngineOutputChannel() {}
-  /**
-   * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method
-   * sends conf on the output channel of this class whose proof can be generated
-   * by the generator pfg. It stores the mapping
-   *   getConflictKeyValue(conf) |-> pfg
-   * as a (lazy) step in the lazy proof object owned by this class.
-   */
-  void trustedConflict(TrustNode pconf) override;
-  /**
-   * Let plem be the pair (Node lem, ProofGenerator * pfg).
-   * Send lem on the output channel of this class whose proof can be generated
-   * by the generator pfg. Apart from pfg, the interface for this method is
-   * the same as OutputChannel. It stores the mapping
-   *   getLemmaKeyValue(lem) |-> pfg
-   * as a (lazy) step in the lazy proof object owned by this class.
-   */
-  LemmaStatus trustedLemma(TrustNode plem,
-                           bool removable = false,
-                           bool preprocess = false,
-                           bool sendAtoms = false) override;
-
- private:
-  /** Pointer to the lazy proof
-   *
-   * This object stores the mapping between formulas (conflicts or lemmas)
-   * and the proof generator provided for them.
-   */
-  LazyCDProof* d_lazyPf;
-  /**
-   * Add coarse grained THEORY_LEMMA step for formula f that is the key of
-   * a lemma or conflict being sent out on the output channel of this class.
-   */
-  bool addTheoryLemmaStep(Node f);
-};
-
-}  // namespace theory
-}  // namespace CVC4
-
-#endif /* CVC4__THEORY__PROOF_OUTPUT_CHANNEL_H */
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 6d87530cb..43950383b 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -23,11 +23,11 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
-// below, proofs are enabled in d_pfee if we are provided a lazy proof
 SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
                                          context::Context* context,
                                          context::UserContext* userContext,
-                ProofNodeManager* pnm, LazyCDProof* lcp)
+                                         ProofNodeManager* pnm,
+                                         bool pfEnabled)
     : ContextNotifyObj(context),
       d_statSharedTerms("theory::shared_terms", 0),
       d_addedSharedTermsSize(context, 0),
@@ -36,11 +36,11 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
       d_registeredEqualities(context),
       d_EENotify(*this),
       d_equalityEngine(d_EENotify, context, "SharedTermsDatabase", true),
-      d_pfee(context,userContext,d_equalityEngine,pnm, lcp!=nullptr),
+      d_pfee(context, userContext, d_equalityEngine, pnm, pfEnabled),
       d_theoryEngine(theoryEngine),
       d_inConflict(context, false),
-      d_conflictPolarity(),
-      d_lazyPf(lcp) {
+      d_conflictPolarity()
+{
   smtStatisticsRegistry()->registerStat(&d_statSharedTerms);
 }
 
@@ -199,12 +199,13 @@ bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const {
   }
 }
 
-void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode reason)
+void SharedTermsDatabase::assertLiteral(TNode lit)
 {
-  Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality << ", " << (polarity ? "true" : "false") << ", " << reason << ")" << endl;
+  Debug("shared-terms-database::assert")
+      << "SharedTermsDatabase::assertLiteral(" << lit << ")" << endl;
   // Add it to the equality engine
-  //d_equalityEngine.assertEquality(equality, polarity, reason);
-  d_pfee.assertAssume(reason);
+  // d_equalityEngine.assertEquality(equality, polarity, reason);
+  d_pfee.assertAssume(lit);
   // Check for conflict
   checkForConflict();
 }
@@ -218,28 +219,6 @@ bool SharedTermsDatabase::propagateEquality(TNode equality, bool polarity) {
   return true;
 }
 
-static Node mkAnd(const std::vector<TNode>& conjunctions) {
-  Assert(conjunctions.size() > 0);
-
-  std::set<TNode> all;
-  all.insert(conjunctions.begin(), conjunctions.end());
-
-  if (all.size() == 1) {
-    // All the same, or just one
-    return conjunctions[0];
-  }
-
-  NodeBuilder<> conjunction(kind::AND);
-  std::set<TNode>::const_iterator it = all.begin();
-  std::set<TNode>::const_iterator it_end = all.end();
-  while (it != it_end) {
-    conjunction << *it;
-    ++ it;
-  }
-
-  return conjunction;
-}
-
 void SharedTermsDatabase::checkForConflict() {
   if (d_inConflict) {
     d_inConflict = false;
@@ -249,12 +228,7 @@ void SharedTermsDatabase::checkForConflict() {
       conflict = conflict.notNode();
     }
     TrustNode trnc = d_pfee.assertConflict(conflict);
-    if (d_lazyPf!=nullptr)
-    {
-      // add the step to the proof
-      Node ckey = TrustNode::getConflictKeyValue(trnc.getNode());
-      d_lazyPf->addLazyStep(ckey, &d_pfee);
-    }
+    d_theoryEngine->processTrustNode(trnc, THEORY_BUILTIN);
     d_theoryEngine->conflict(trnc.getNode(), THEORY_BUILTIN);
     d_conflictLHS = d_conflictRHS = Node::null();
   }
@@ -270,7 +244,8 @@ bool SharedTermsDatabase::isKnown(TNode literal) const {
   }
 }
 
-theory::TrustNode SharedTermsDatabase::explain(TNode literal) {
+theory::TrustNode SharedTermsDatabase::explain(TNode literal)
+{
   TrustNode trn = d_pfee.explain(literal);
   return trn;
 }
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index ccee94c8d..88664544b 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -21,30 +21,26 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
+#include "expr/proof_node_manager.h"
 #include "theory/theory.h"
+#include "theory/trust_node.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_equality_engine.h"
-#include "theory/trust_node.h"
-#include "expr/proof_node_manager.h"
 #include "util/statistics_registry.h"
-#include "expr/lazy_proof.h"
 
 namespace CVC4 {
 
 class TheoryEngine;
 
 class SharedTermsDatabase : public context::ContextNotifyObj {
-
-public:
-
+ public:
   /** A container for a list of shared terms */
   typedef std::vector<TNode> shared_terms_list;
 
   /** The iterator to go through the shared terms list */
   typedef shared_terms_list::const_iterator shared_terms_iterator;
 
-private:
-
+ private:
   /** Some statistics */
   IntStat d_statSharedTerms;
 
@@ -72,8 +68,7 @@ private:
   typedef context::CDHashSet<Node, NodeHashFunction> RegisteredEqualitiesSet;
   RegisteredEqualitiesSet d_registeredEqualities;
 
-private:
-
+ private:
   /** This method removes all the un-necessary stuff from the maps */
   void backtrack();
 
@@ -118,7 +113,7 @@ private:
 
   /** Equality engine */
   theory::eq::EqualityEngine d_equalityEngine;
-  
+
   /** Proof equality engine */
   theory::eq::ProofEqEngine d_pfee;
 
@@ -162,17 +157,19 @@ private:
    */
   void checkForConflict();
 
-public:
-
-  SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context,
-                                         context::UserContext* userContext,
-                ProofNodeManager* pnm, LazyCDProof* lcp);
+ public:
+  SharedTermsDatabase(TheoryEngine* theoryEngine,
+                      context::Context* context,
+                      context::UserContext* userContext,
+                      ProofNodeManager* pnm,
+                      bool pfEnabled);
   ~SharedTermsDatabase();
 
   /**
-   * Asserts the equality to the shared terms database,
+   * Asserts the literal lit to the shared terms database, where lit is
+   * an equality or disequality.
    */
-  void assertEquality(TNode equality, bool polarity, TNode reason);
+  void assertLiteral(TNode lit);
 
   /**
    * Return whether the equality is alreday known to the engine
@@ -256,10 +253,7 @@ public:
    */
   theory::eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; }
 
-protected:
-
-  /** Pointer to the lazy proof of TheoryEngine */
-  LazyCDProof* d_lazyPf;
+ protected:
   /**
    * This method gets called on backtracks from the context manager.
    */
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index cc73da8f2..27e2520b8 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -773,17 +773,20 @@ Node CoreSolver::getConclusion(Node x,
     {
       // we can assume its length is greater than zero
       Node emp = Word::mkEmptyWord(sk1.getType());
-      conc = nm->mkNode(AND, conc, sk1.eqNode(emp).negate(),
-      nm->mkNode(GT,nm->mkNode(STRING_LENGTH,sk1), nm->mkConst(Rational(0))));
+      conc = nm->mkNode(
+          AND,
+          conc,
+          sk1.eqNode(emp).negate(),
+          nm->mkNode(
+              GT, nm->mkNode(STRING_LENGTH, sk1), nm->mkConst(Rational(0))));
     }
   }
-  else if (rule==PfRule::CONCAT_CSPLIT)
+  else if (rule == PfRule::CONCAT_CSPLIT)
   {
-    Assert (y.isConst());
+    Assert(y.isConst());
     size_t yLen = Word::getLength(y);
-    Node firstChar = yLen == 1 ? y
-                                  : (isRev ? Word::suffix(y, 1)
-                                            : Word::prefix(y, 1));
+    Node firstChar =
+        yLen == 1 ? y : (isRev ? Word::suffix(y, 1) : Word::prefix(y, 1));
     Node sk = skc->mkSkolemCached(
         x,
         isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT,
@@ -792,17 +795,15 @@ Node CoreSolver::getConclusion(Node x,
     conc = x.eqNode(isRev ? utils::mkNConcat(sk, firstChar)
                           : utils::mkNConcat(firstChar, sk));
   }
-  else if (rule==PfRule::CONCAT_CPROP)
+  else if (rule == PfRule::CONCAT_CPROP)
   {
     // expect (str.++ z c1) and c2
-    Assert (x.getKind()==STRING_CONCAT && x.getNumChildren()==2);
+    Assert(x.getKind() == STRING_CONCAT && x.getNumChildren() == 2);
     Node z = x[isRev ? 1 : 0];
     Node c1 = x[isRev ? 0 : 1];
-    Assert (c1.isConst());
+    Assert(c1.isConst());
     Node c2 = y;
-    Assert (c2.isConst());
-    
-    
+    Assert(c2.isConst());
   }
 
   return conc;
@@ -1011,14 +1012,14 @@ void CoreSolver::getNormalForms(Node eqc,
         if (!StringsEntail::canConstantContainList(c, nf.d_nf, firstc, lastc))
         {
           Node n = nf.d_base;
+          std::vector<Node> exp;
           //conflict
           Trace("strings-solve") << "Normal form for " << n << " cannot be contained in constant " << c << std::endl;
           //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = N[n] )
-          std::vector< Node > exp;
-          d_bsolver.explainConstantEqc(n,eqc,exp);
           // Notice although not implemented, this can be minimized based on
           // firstc/lastc, normal_forms_exp_depend.
           exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end());
+          d_bsolver.explainConstantEqc(n, eqc, exp);
           Node conc = d_false;
           d_im.sendInference(exp, conc, Inference::N_NCTN);
         }
@@ -1556,11 +1557,12 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       // E.g. "abc" ++ ... = nc ++ ... ---> nc = "a" ++ k
       SkolemCache* skc = d_termReg.getSkolemCache();
       std::vector<Node> newSkolems;
-      iinfo.d_conc = getConclusion(nc,nfcv[index],PfRule::CONCAT_CSPLIT,isRev,skc,newSkolems);
+      iinfo.d_conc = getConclusion(
+          nc, nfcv[index], PfRule::CONCAT_CSPLIT, isRev, skc, newSkolems);
       NormalForm::getExplanationForPrefixEq(
           nfi, nfj, index, index, iinfo.d_ant);
       iinfo.d_ant.push_back(expNonEmpty);
-      Assert(newSkolems.size()==1);
+      Assert(newSkolems.size() == 1);
       iinfo.d_new_skolem[LENGTH_SPLIT].push_back(newSkolems[0]);
       iinfo.d_id = Inference::SSPLIT_CST;
       iinfo.d_idRev = isRev;
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 9af4dc565..49a697592 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -48,7 +48,7 @@ void InferProofCons::notifyFact(const InferInfo& ii)
     Trace("strings-ipc-debug") << "...duplicate!" << std::endl;
     return;
   }
-  if (fact.getKind()==EQUAL)
+  if (fact.getKind() == EQUAL)
   {
     Node symFact = fact[1].eqNode(fact[0]);
     if (d_lazyFactMap.find(symFact) != d_lazyFactMap.end())
@@ -168,8 +168,9 @@ Node InferProofCons::convert(Inference infer,
     case Inference::INFER_EMP:
     {
       // need the "extended equality rewrite"
-      ps.d_args.push_back(builtin::BuiltinProofRuleChecker::mkRewriterId(
-          RewriterId::REWRITE_EQ_EXT));
+      MethodId ids = MethodId::SB_DEFAULT;
+      MethodId idr = MethodId::RW_REWRITE_EQ_EXT;
+      addMethodIds(ps.d_args, ids, idr);
       ps.d_rule = PfRule::MACRO_SR_PRED_ELIM;
     }
     break;
@@ -260,7 +261,7 @@ Node InferProofCons::convert(Inference infer,
                           ps.d_children.begin() + mainEqIndex);
       Node mainEqSRew =
           d_psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, emptyVec);
-      if (isSymm(mainEqSRew, mainEq))
+      if (CDProof::isSame(mainEqSRew, mainEq))
       {
         Trace("strings-ipc-core") << "...undo step" << std::endl;
         // not necessary
@@ -305,8 +306,11 @@ Node InferProofCons::convert(Inference infer,
         // optimization in processSimpleNEq. Alternatively, this could
         // possibly be done by CONCAT_EQ with !isRev.
         std::vector<Node> cexp;
-        if (convertPredTransform(
-                mainEqCeq, conc, cexp, RewriterId::REWRITE_EQ_EXT))
+        if (convertPredTransform(mainEqCeq,
+                                 conc,
+                                 cexp,
+                                 MethodId::SB_DEFAULT,
+                                 MethodId::RW_REWRITE_EQ_EXT))
         {
           Trace("strings-ipc-core") << "Transformed to " << conc
                                     << " via pred transform" << std::endl;
@@ -901,10 +905,11 @@ bool InferProofCons::convertLengthPf(Node lenReq,
 bool InferProofCons::convertPredTransform(Node src,
                                           Node tgt,
                                           const std::vector<Node>& exp,
-                                          RewriterId id)
+                                          MethodId ids,
+                                          MethodId idr)
 {
   // symmetric equalities
-  if (isSymm(src, tgt))
+  if (CDProof::isSame(src, tgt))
   {
     return true;
   }
@@ -914,19 +919,16 @@ bool InferProofCons::convertPredTransform(Node src,
   // try to prove that tgt rewrites to src
   children.insert(children.end(), exp.begin(), exp.end());
   args.push_back(tgt);
-  if (id != RewriterId::REWRITE)
-  {
-    args.push_back(builtin::BuiltinProofRuleChecker::mkRewriterId(id));
-  }
+  addMethodIds(args, ids, idr);
   Node res = d_psb.tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
   if (res.isNull())
   {
     // failed to apply
     return false;
   }
-  Trace("strings-ipc-debug")
-      << "InferProofCons::convertPredTransform: success " << src
-      << " == " << tgt << " under " << exp << " via " << id << std::endl;
+  Trace("strings-ipc-debug") << "InferProofCons::convertPredTransform: success "
+                             << src << " == " << tgt << " under " << exp
+                             << " via " << ids << "/" << idr << std::endl;
   // should definitely have concluded tgt
   Assert(res == tgt);
   return true;
@@ -934,14 +936,12 @@ bool InferProofCons::convertPredTransform(Node src,
 
 bool InferProofCons::convertPredIntro(Node tgt,
                                       const std::vector<Node>& exp,
-                                      RewriterId id)
+                                      MethodId ids,
+                                      MethodId idr)
 {
   std::vector<Node> args;
   args.push_back(tgt);
-  if (id != RewriterId::REWRITE)
-  {
-    args.push_back(builtin::BuiltinProofRuleChecker::mkRewriterId(id));
-  }
+  addMethodIds(args, ids, idr);
   Node res = d_psb.tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args);
   if (res.isNull())
   {
@@ -953,18 +953,16 @@ bool InferProofCons::convertPredIntro(Node tgt,
 
 Node InferProofCons::convertPredElim(Node src,
                                      const std::vector<Node>& exp,
-                                     RewriterId id)
+                                     MethodId ids,
+                                     MethodId idr)
 {
   std::vector<Node> children;
   children.push_back(src);
   children.insert(children.end(), exp.begin(), exp.end());
   std::vector<Node> args;
-  if (id != RewriterId::REWRITE)
-  {
-    args.push_back(builtin::BuiltinProofRuleChecker::mkRewriterId(id));
-  }
+  addMethodIds(args, ids, idr);
   Node srcRew = d_psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args);
-  if (isSymm(src, srcRew))
+  if (CDProof::isSame(src, srcRew))
   {
     d_psb.popStep();
     return src;
@@ -972,6 +970,21 @@ Node InferProofCons::convertPredElim(Node src,
   return srcRew;
 }
 
+void InferProofCons::addMethodIds(std::vector<Node>& args,
+                                  MethodId ids,
+                                  MethodId idr)
+{
+  bool ndefRewriter = (idr != MethodId::RW_REWRITE);
+  if (ids != MethodId::SB_DEFAULT || ndefRewriter)
+  {
+    args.push_back(mkMethodId(ids));
+  }
+  if (ndefRewriter)
+  {
+    args.push_back(mkMethodId(idr));
+  }
+}
+
 Node InferProofCons::convertTrans(Node eqa, Node eqb)
 {
   if (eqa.getKind() != EQUAL || eqb.getKind() != EQUAL)
@@ -997,13 +1010,6 @@ Node InferProofCons::convertTrans(Node eqa, Node eqb)
   return Node::null();
 }
 
-bool InferProofCons::isSymm(Node src, Node tgt)
-{
-  return src == tgt
-         || (src.getKind() == EQUAL && tgt.getKind() == EQUAL
-             && src[0] == tgt[1] && src[1] == tgt[0]);
-}
-
 ProofStepBuffer* InferProofCons::getBuffer() { return &d_psb; }
 
 std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
@@ -1012,9 +1018,9 @@ std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
   CDProof pf(d_pnm);
   // get the inference
   NodeInferInfoMap::iterator it = d_lazyFactMap.find(fact);
-  if (it==d_lazyFactMap.end())
+  if (it == d_lazyFactMap.end())
   {
-    if (fact.getKind()==EQUAL)
+    if (fact.getKind() == EQUAL)
     {
       // Use the symmetric fact. There is no need to explictly make a
       // SYMM proof, as this is handled by CDProof::mkProof below.
diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h
index 612e67693..18f2d0b61 100644
--- a/src/theory/strings/infer_proof_cons.h
+++ b/src/theory/strings/infer_proof_cons.h
@@ -126,22 +126,25 @@ class InferProofCons : public ProofGenerator
   bool convertPredTransform(Node src,
                             Node tgt,
                             const std::vector<Node>& exp,
-                            RewriterId id = RewriterId::REWRITE);
+                            MethodId ids = MethodId::SB_DEFAULT,
+                            MethodId idr = MethodId::RW_REWRITE);
   /**
    */
   bool convertPredIntro(Node tgt,
                         const std::vector<Node>& exp,
-                        RewriterId id = RewriterId::REWRITE);
+                        MethodId ids = MethodId::SB_DEFAULT,
+                        MethodId idr = MethodId::RW_REWRITE);
   /**
    */
   Node convertPredElim(Node src,
                        const std::vector<Node>& exp,
-                       RewriterId id = RewriterId::REWRITE);
+                       MethodId ids = MethodId::SB_DEFAULT,
+                       MethodId idr = MethodId::RW_REWRITE);
+  /** Add method ids */
+  void addMethodIds(std::vector<Node>& args, MethodId ids, MethodId idr);
   /**
    */
   Node convertTrans(Node eqa, Node eqb);
-  /** Is symm */
-  static bool isSymm(Node src, Node tgt);
   /** the proof node manager */
   ProofNodeManager* d_pnm;
   /** The lazy fact map */
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index a5a22dfa0..3b06ea447 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -307,8 +307,8 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     std::vector<Node> newSkolems;
     Node kt0 = ProofSkolemCache::getSkolemForm(t0);
     Node ks0 = ProofSkolemCache::getSkolemForm(s0);
-    Node conc = CoreSolver::getConclusion(
-        kt0, ks0, id, isRev, &skc, newSkolems);
+    Node conc =
+        CoreSolver::getConclusion(kt0, ks0, id, isRev, &skc, newSkolems);
     conc = ProofSkolemCache::getWitnessForm(conc);
     return conc;
   }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b2793fac9..3b6ffd6de 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -48,6 +48,7 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_engine_proof_generator.h"
 #include "theory/theory_model.h"
 #include "theory/theory_traits.h"
 #include "theory/uf/equality_engine.h"
@@ -131,7 +132,7 @@ std::string getTheoryString(theory::TheoryId id)
 void TheoryEngine::finishInit()
 {
   // if we are using the new proofs module
-  if (options::proofNew())
+  if (d_lazyProof != nullptr)
   {
     // ask the theories to populate the proof checking rules in the checker
     for (TheoryId theoryId = theory::THEORY_FIRST;
@@ -197,8 +198,17 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_logicInfo(logicInfo),
       d_pchecker(new ProofChecker),
       d_pNodeManager(new ProofNodeManager(d_pchecker.get())),
-      d_lazyProof(options::proofNew() ? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext) : nullptr),
-      d_sharedTerms(this, context, userContext, d_pNodeManager.get(), d_lazyProof.get()),
+      d_lazyProof(
+          options::proofNew()
+              ? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext)
+              : nullptr),
+      d_tepg(
+          new TheoryEngineProofGenerator(d_pNodeManager.get(), d_userContext)),
+      d_sharedTerms(this,
+                    context,
+                    userContext,
+                    d_pNodeManager.get(),
+                    d_lazyProof != nullptr),
       d_masterEqualityEngine(nullptr),
       d_masterEENotify(*this),
       d_quantEngine(nullptr),
@@ -637,12 +647,16 @@ void TheoryEngine::combineTheories() {
     // We need to split on it
     Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
 
-    lemma(equality.orNode(equality.notNode()),
-          RULE_INVALID,
-          false,
-          false,
-          false,
-          carePair.d_theory);
+    Node split = equality.orNode(equality.notNode());
+    if (d_lazyProof != nullptr)
+    {
+      std::vector<Node> pfChildren;
+      std::vector<Node> pfArgs;
+      pfArgs.push_back(equality);
+      d_lazyProof->addStep(split, PfRule::SPLIT, pfChildren, pfArgs);
+    }
+
+    lemma(split, RULE_INVALID, false, false, false, carePair.d_theory);
 
     // This code is supposed to force preference to follow what the theory models already have
     // but it doesn't seem to make a big difference - need to explore more -Clark
@@ -1205,18 +1219,14 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
     return;
   }
 
-  // Polarity of the assertion
-  bool polarity = assertion.getKind() != kind::NOT;
-
-  // Atom of the assertion
-  TNode atom = polarity ? assertion : assertion[0];
-
   // If sending to the shared terms database, it's also simple
   if (toTheoryId == THEORY_BUILTIN) {
-    Assert(atom.getKind() == kind::EQUAL)
-        << "atom should be an EQUALity, not `" << atom << "'";
+    Assert(assertion.getKind() == kind::EQUAL
+           || (assertion.getKind() == kind::NOT
+               && assertion[0].getKind() == kind::EQUAL))
+        << "atom should be an EQUALity, not `" << assertion << "'";
     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
-      d_sharedTerms.assertEquality(atom, polarity, assertion);
+      d_sharedTerms.assertLiteral(assertion);
     }
     return;
   }
@@ -1257,7 +1267,9 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
     return;
   }
 
-  Assert(atom.getKind() == kind::EQUAL);
+  Assert(assertion.getKind() == kind::EQUAL
+         || (assertion.getKind() == kind::NOT
+             && assertion[0].getKind() == kind::EQUAL));
 
   // Normalize
   Node normalizedLiteral = Rewriter::rewrite(assertion);
@@ -1543,7 +1555,9 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
   return conjunction;
 }
 
-Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) {
+theory::TrustNode TheoryEngine::getExplanationAndRecipe(
+    TNode node, LemmaProofRecipe* proofRecipe)
+{
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl;
 
   bool polarity = node.getKind() != kind::NOT;
@@ -1597,8 +1611,7 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe
           proofRecipe->addStep(proofStep);
         }
       });
-
-    return explanation;
+    return texplanation;
   }
 
   Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl;
@@ -1615,8 +1628,8 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe
   TheoryId explainer = nodeExplainerPair.d_theory;
 
   // Create the workplace for explanations
-  std::vector<NodeTheoryPair> explanationVector;
-  explanationVector.push_back(d_propagationMap[toExplain]);
+  std::vector<NodeTheoryPair> vec;
+  vec.push_back(d_propagationMap[toExplain]);
   // Process the explanation
   if (proofRecipe) {
     Node emptyNode;
@@ -1626,16 +1639,17 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe
     proofRecipe->addBaseAssertion(node);
   }
 
-  getExplanation(explanationVector, proofRecipe);
-  Node explanation = mkExplanation(explanationVector);
-
-  Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
+  TrustNode texplanation = getExplanation(vec, proofRecipe);
 
-  return explanation;
+  Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => "
+                           << texplanation.getNode() << endl;
+  return texplanation;
 }
 
-Node TheoryEngine::getExplanation(TNode node) {
+theory::TrustNode TheoryEngine::getExplanation(TNode node)
+{
   LemmaProofRecipe *dontCareRecipe = NULL;
+  // the trust node was processed within getExplanationAndRecipe
   return getExplanationAndRecipe(node, dontCareRecipe);
 }
 
@@ -1745,7 +1759,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
                                         theory::TheoryId atomsTo) {
   // For resource-limiting (also does a time check).
   // spendResource();
-  
+
   // Do we need to check atoms
   if (atomsTo != theory::THEORY_LAST) {
     Debug("theory::atoms") << "TheoryEngine::lemma(" << node << ", " << atomsTo << ")" << endl;
@@ -1763,16 +1777,35 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
                      << CheckSatCommand(n.toExpr());
   }
 
-  // if proofNew is enabled, then d_lazyProof contains a proof of n.
-  /*
-  Node lemma = node;
-  if (negated)
+  // if d_lazyProof is enabled, then d_lazyProof contains a proof of n.
+  if (d_lazyProof != nullptr)
   {
-    lemma = lemma.negate();
+    Node lemma = node;
+    if (negated)
+    {
+      lemma = lemma.negate();
+    }
+    if (!d_lazyProof->hasStep(lemma) && !d_lazyProof->hasGenerator(lemma))
+    {
+      Trace("te-proof") << "No proof for lemma: " << lemma << std::endl;
+      Trace("te-proof-warn")
+          << "WARNING: No proof for lemma: " << lemma << std::endl;
+    }
+    else
+    {
+      Trace("te-proof") << "Proof for lemma: " << lemma << std::endl;
+    }
   }
-  Assert (!options::proofNew() || d_lazyProof->hasStep(lemma));
-  */
-  
+
+  // FIXME
+  std::shared_ptr<LazyCDProof> lcp;
+  if (d_lazyProof != nullptr)
+  {
+    Trace("te-proof-exp") << "TheoryEngine::lemma: process " << node
+                          << std::endl;
+    lcp.reset(new LazyCDProof(d_pNodeManager.get()));
+  }
+
   AssertionPipeline additionalLemmas;
 
   // Run theory preprocessing, maybe
@@ -1799,10 +1832,12 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   // assert to prop engine
-  for (size_t i = 0, lsize = additionalLemmas.size(); i < lsize; ++ i) {
+  for (size_t i = 0, lsize = additionalLemmas.size(); i < lsize; ++i)
+  {
     Node rewritten = Rewriter::rewrite(additionalLemmas[i]);
     additionalLemmas.replace(i, rewritten);
-    d_propEngine->assertLemma(additionalLemmas[i], i==0 && negated, removable, rule, node);
+    d_propEngine->assertLemma(
+        additionalLemmas[i], i == 0 && negated, removable, rule, node);
   }
 
   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
@@ -1825,12 +1860,47 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel());
 }
 
+void TheoryEngine::processTrustNode(theory::TrustNode trn,
+                                    theory::TheoryId from)
+{
+  if (d_lazyProof == nullptr)
+  {
+    // proofs not enabled
+    return;
+  }
+  ProofGenerator* pfg = trn.getGenerator();
+  Node p = trn.getProven();
+  // may or may not have supplied a generator
+  if (pfg != nullptr)
+  {
+    // if we have, add it to the lazy proof object
+    d_lazyProof->addLazyStep(p, pfg);
+    // generator should have a proof for p
+    Assert(pfg->hasProofFor(p));
+  }
+  else
+  {
+    // all BUILTIN should be handled
+    Assert(from != THEORY_BUILTIN);
+    // untrusted theory lemma
+    std::vector<Node> children;
+    std::vector<Node> args;
+    args.push_back(p);
+    unsigned tid = static_cast<unsigned>(from);
+    Node tidn = NodeManager::currentNM()->mkConst(Rational(tid));
+    args.push_back(tidn);
+    // add the step, should always succeed;
+    d_lazyProof->addStep(p, PfRule::THEORY_LEMMA, children, args);
+  }
+}
+
 void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
 
-  // if proofNew is enabled, then d_lazyProof contains a proof of conflict.negate()
-  //Assert (!options::proofNew() || d_lazyProof->hasStep(conflict.negate()));
-  
   Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl;
+  // if proofNew is enabled, then d_lazyProof contains a proof of
+  // conflict.negate()
+  // Assert (d_lazyProof==nullptr || d_lazyProof->hasStep(conflict.negate()) ||
+  // d_lazyProof->hasGenerator(conflict.negate()) || theoryId==THEORY_ARITH);
 
   Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
 
@@ -1862,13 +1932,36 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
   // In the multiple-theories case, we need to reconstruct the conflict
   if (d_logicInfo.isSharingEnabled()) {
     // Create the workplace for explanations
-    std::vector<NodeTheoryPair> explanationVector;
-    explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
+    std::vector<NodeTheoryPair> vec;
+    vec.push_back(
+        NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
 
     // Process the explanation
-    getExplanation(explanationVector, proofRecipe);
+    TrustNode tncExp = getExplanation(vec, proofRecipe);
     PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe));
-    Node fullConflict = mkExplanation(explanationVector);
+    Node fullConflict = tncExp.getNode();
+
+    if (d_lazyProof != nullptr)
+    {
+      if (fullConflict!=conflict)
+      {
+        // store the explicit step
+        processTrustNode(tncExp, THEORY_BUILTIN);
+      }
+      Node fullConflictNeg = fullConflict.notNode();
+      // ------------------------- explained  ---------- from theory 
+      // fullConflict => conflict              ~conflict
+      // ----------------------------------------------- MACRO_SR_PRED_TRANSFORM
+      // ~fullConflict
+      std::vector<Node> children;
+      children.push_back(tncExp.getProven());
+      children.push_back(conflict.notNode());
+      std::vector<Node> args;
+      args.push_back(fullConflictNeg);
+      args.push_back(mkMethodId(MethodId::SB_PREDICATE));
+      d_lazyProof->addStep(fullConflictNeg, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+    }
+
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
     Assert(properConflict(fullConflict));
     lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST);
@@ -1954,9 +2047,22 @@ void TheoryEngine::staticInitializeBVOptions(
   }
 }
 
-void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
-  Assert(explanationVector.size() > 0);
+theory::TrustNode TheoryEngine::getExplanation(
+    std::vector<NodeTheoryPair>& explanationVector,
+    LemmaProofRecipe* proofRecipe)
+{
+  Assert(explanationVector.size() == 1);
 
+  Node conclusion = explanationVector[0].d_node;
+  std::shared_ptr<LazyCDProof> lcp;
+  bool simpleExplain = true;
+  TrustNode simpleTrn;
+  if (d_lazyProof != nullptr)
+  {
+    Trace("te-proof-exp") << "TheoryEngine::getExplanation " << conclusion
+                          << std::endl;
+    lcp.reset(new LazyCDProof(d_pNodeManager.get()));
+  }
   unsigned i = 0; // Index of the current literal we are processing
   unsigned j = 0; // Index of the last literal we are keeping
 
@@ -1979,15 +2085,25 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
         << toExplain.d_theory << endl;
 
     // If a true constant or a negation of a false constant we can ignore it
-    if (toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
-    {
-      ++ i;
-      continue;
-    }
-    if (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst()
-        && !toExplain.d_node[0].getConst<bool>())
+    if ((toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
+        || (toExplain.d_node.getKind() == kind::NOT
+            && toExplain.d_node[0].isConst()
+            && !toExplain.d_node[0].getConst<bool>()))
     {
       ++ i;
+      if (lcp != nullptr)
+      {
+        Trace("te-proof-exp")
+            << "- explain " << toExplain.d_node << " trivially..." << std::endl;
+        // ------------------MACRO_SR_PRED_INTRO
+        // toExplain.d_node
+        std::vector<Node> children;
+        std::vector<Node> args;
+        args.push_back(toExplain.d_node);
+        lcp->addStep(
+            toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args);
+        simpleExplain = false;
+      }
       continue;
     }
 
@@ -1996,6 +2112,8 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     {
       Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl;
       explanationVector[j++] = explanationVector[i++];
+      // it will be a free assumption in the proof
+      Trace("te-proof-exp") << "- keep " << toExplain.d_node << std::endl;
       continue;
     }
 
@@ -2005,12 +2123,32 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
       Debug("theory::explain")
           << "TheoryEngine::explain(): expanding " << toExplain.d_node
           << " got from " << toExplain.d_theory << endl;
-      for (unsigned k = 0; k < toExplain.d_node.getNumChildren(); ++k)
+      size_t nchild = toExplain.d_node.getNumChildren();
+      for (size_t k = 0; k < nchild; ++k)
       {
         NodeTheoryPair newExplain(
             toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp);
         explanationVector.push_back(newExplain);
       }
+      if (lcp != nullptr)
+      {
+        Trace("te-proof-exp")
+            << "- AND expand " << toExplain.d_node << std::endl;
+        // toExplain.d_node[0] ... toExplain.d_node[n]
+        // --------------------------------------------MACRO_SR_PRED_INTRO
+        // toExplain.d_node
+        std::vector<Node> children;
+        for (size_t k = 0; k < nchild; ++k)
+        {
+          children.push_back(toExplain.d_node[k]);
+        }
+        std::vector<Node> args;
+        args.push_back(toExplain.d_node);
+        args.push_back(mkMethodId(MethodId::SB_PREDICATE));
+        lcp->addStep(
+            toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args);
+        simpleExplain = false;
+      }
       ++ i;
       continue;
     }
@@ -2045,7 +2183,18 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
             }
           }
         })
-
+        if (lcp != nullptr)
+        {
+          if (!CDProof::isSame(toExplain.d_node, (*find).second.d_node))
+          {
+            Trace("te-proof-exp")
+                << "- t-explained cached: " << toExplain.d_node << " by "
+                << (*find).second.d_node << std::endl;
+            // does this ever happen?
+            Assert(false);
+            simpleExplain = false;
+          }
+        }
         continue;
       }
     }
@@ -2055,15 +2204,70 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     if (toExplain.d_theory == THEORY_BUILTIN)
     {
       texplanation = d_sharedTerms.explain(toExplain.d_node);
-      Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << texplanation.getNode() << std::endl;
+      Debug("theory::explain")
+          << "\tTerm was propagated by THEORY_BUILTIN. Explanation: "
+          << texplanation.getNode() << std::endl;
     }
     else
     {
-      texplanation =
-          theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
-      Debug("theory::explain") << "\tTerm was propagated by owner theory: "
-                               << theoryOf(toExplain.d_theory)->getId()
-                               << ". Explanation: " << texplanation.getNode() << std::endl;
+      texplanation = theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
+      Debug("theory::explain")
+          << "\tTerm was propagated by owner theory: "
+          << theoryOf(toExplain.d_theory)->getId()
+          << ". Explanation: " << texplanation.getNode() << std::endl;
+    }
+    if (lcp != nullptr)
+    {
+      Trace("te-proof-exp")
+          << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node
+          << " by " << texplanation.getNode() << std::endl;
+      // if not a trivial explanation
+      if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node))
+      {
+        // ----------- Via theory
+        // exp => lit                exp
+        // ---------------------------------MACRO_SR_PRED_TRANSFORM
+        // lit
+        Node proven = texplanation.getProven();
+        if (texplanation.getGenerator() != nullptr)
+        {
+          lcp->addLazyStep(proven, texplanation.getGenerator());
+        }
+        else
+        {
+          Trace("te-proof-exp") << "...trust THEORY_LEMMA" << std::endl;
+          // otherwise, trusted theory lemma
+          std::vector<Node> children;
+          std::vector<Node> args;
+          args.push_back(proven);
+          unsigned tid = static_cast<unsigned>(toExplain.d_theory);
+          Node tidn = NodeManager::currentNM()->mkConst(Rational(tid));
+          args.push_back(tidn);
+          lcp->addStep(proven, PfRule::THEORY_LEMMA, children, args);
+        }
+        std::vector<Node> children;
+        children.push_back(proven);
+        children.push_back(texplanation.getNode());
+        std::vector<Node> args;
+        args.push_back(toExplain.d_node);
+        args.push_back(mkMethodId(MethodId::SB_PREDICATE));
+        lcp->addStep(
+            toExplain.d_node, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+        if (simpleExplain)
+        {
+          if (simpleTrn.isNull())
+          {
+            // as an optimization, it may be a simple explanation, so we
+            // remember the trust node for now
+            simpleTrn = texplanation;
+          }
+          else
+          {
+            // multiple theories involved, not simple
+            simpleExplain = false;
+          }
+        }
+      }
     }
     Node explanation = texplanation.getNode();
 
@@ -2131,6 +2335,28 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
         }
       }
     });
+
+  Node exp = mkExplanation(explanationVector);
+
+  if (lcp != nullptr)
+  {
+    // doesn't work currently due to reordering of assumptions
+    /*
+    if (simpleExplain)
+    {
+      // single call to a theory's explain method, skip the proof generator
+      Assert (!simpleTrn.isNull());
+      Trace("te-proof-exp") << "...simple explain " << simpleTrn.getNode() <<
+    std::endl; return simpleTrn;
+    }
+    */
+    // store in the proof generator
+    TrustNode trn = d_tepg->mkTrustExplain(conclusion, exp, lcp);
+    // return the trust node
+    return trn;
+  }
+
+  return theory::TrustNode::mkTrustLemma(exp, nullptr);
 }
 
 void TheoryEngine::setUserAttribute(const std::string& attr,
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index cd3e8e122..a5b9c393f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -37,14 +37,15 @@
 #include "smt/command.h"
 #include "theory/atom_requests.h"
 #include "theory/decision_manager.h"
+#include "theory/engine_output_channel.h"
 #include "theory/interrupted.h"
-#include "theory/proof_engine_output_channel.h"
 #include "theory/rewriter.h"
 #include "theory/shared_terms_database.h"
 #include "theory/sort_inference.h"
 #include "theory/substitutions.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/theory.h"
+#include "theory/trust_node.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
 #include "util/hash.h"
@@ -57,6 +58,7 @@ namespace CVC4 {
 class ResourceManager;
 class LemmaProofRecipe;
 class LazyCDProof;
+class TheoryEngineProofGenerator;
 
 /**
  * A pair of a theory and a node. This is used to mark the flow of
@@ -155,8 +157,10 @@ class TheoryEngine {
    * This stores instructions for how to construct proofs for all theory lemmas.
    */
   std::shared_ptr<LazyCDProof> d_lazyProof;
+  /** The proof generator */
+  std::shared_ptr<TheoryEngineProofGenerator> d_tepg;
   //--------------------------------- end new proofs
-  
+
   /**
    * The database of shared terms.
    */
@@ -252,10 +256,8 @@ class TheoryEngine {
    */
   context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
 
-  /**
-   * Output channels for individual theories.
-   */
-  theory::ProofEngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
+  /** Output channels for individual theories. */
+  theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
 
   /**
    * Are we in conflict.
@@ -360,6 +362,19 @@ class TheoryEngine {
                             bool preprocess,
                             theory::TheoryId atomsTo);
 
+  /**
+   * Process trust node. This method ensures that the proof for the proven node
+   * of trn is stored as a lazy step in the lazy proof (d_lazyProof) maintained
+   * by this class, referencing the proof generator of the trust node. The
+   * argument from specifies the theory responsible for this trust node. If
+   * no generator is provided, then a (eager) THEORY_LEMMA step is added to
+   * the lazy proof.
+   *
+   * @param trn The trust node to process
+   * @param from The id of the theory responsible for the trust node.
+   */
+  void processTrustNode(theory::TrustNode trn, theory::TheoryId from);
+
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
 
@@ -401,8 +416,7 @@ class TheoryEngine {
   inline void addTheory(theory::TheoryId theoryId)
   {
     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
-    d_theoryOut[theoryId] =
-        new theory::ProofEngineOutputChannel(this, theoryId, d_lazyProof.get());
+    d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId);
     d_theoryTable[theoryId] = new TheoryClass(d_context,
                                               d_userContext,
                                               *d_theoryOut[theoryId],
@@ -514,10 +528,11 @@ class TheoryEngine {
    * theory that sent the literal. The lemmaProofRecipe will contain a list
    * of the explanation steps required to produce the original node.
    */
-  void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRecipe);
-
-public:
+  theory::TrustNode getExplanation(
+      std::vector<NodeTheoryPair>& explanationVector,
+      LemmaProofRecipe* lemmaProofRecipe);
 
+ public:
   /**
    * Signal the start of a new round of assertion preprocessing
    */
@@ -635,13 +650,14 @@ public:
   /**
    * Returns an explanation of the node propagated to the SAT solver.
    */
-  Node getExplanation(TNode node);
+  theory::TrustNode getExplanation(TNode node);
 
   /**
    * Returns an explanation of the node propagated to the SAT solver and the theory
    * that propagated it.
    */
-  Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe);
+  theory::TrustNode getExplanationAndRecipe(TNode node,
+                                            LemmaProofRecipe* proofRecipe);
 
   /**
    * collect model info
diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp
new file mode 100644
index 000000000..c11378e04
--- /dev/null
+++ b/src/theory/theory_engine_proof_generator.cpp
@@ -0,0 +1,84 @@
+/*********************                                                        */
+/*! \file theory_engine_proof_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The theory engine proof generator
+ **/
+
+#include "theory/theory_engine_proof_generator.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm,
+                                                       context::UserContext* u)
+    : d_pnm(pnm), d_proofs(u)
+{
+}
+
+theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(
+    TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf)
+{
+  theory::TrustNode trn = theory::TrustNode::mkTrustPropExp(lit, exp, this);
+  Node p = trn.getProven();
+  Assert(p.getKind() == IMPLIES && p.getNumChildren() == 2);
+  // should not already be proven
+  NodeLazyCDProofMap::iterator it = d_proofs.find(p);
+  if (it != d_proofs.end())
+  {
+    Assert(false);
+  }
+  else
+  {
+    // we will prove this
+    d_proofs.insert(p, lpf);
+  }
+  return trn;
+}
+
+std::shared_ptr<ProofNode> TheoryEngineProofGenerator::getProofFor(Node f)
+{
+  // should only ask this generator for proofs of implications
+  Assert(f.getKind() == IMPLIES && f.getNumChildren() == 2);
+  NodeLazyCDProofMap::iterator it = d_proofs.find(f);
+  if (it == d_proofs.end())
+  {
+    return nullptr;
+  }
+  std::shared_ptr<LazyCDProof> lcp = (*it).second;
+  // finalize it via scope
+  std::vector<Node> scopeAssumps;
+  if (f[0].getKind() == AND)
+  {
+    for (const Node& fc : f[0])
+    {
+      scopeAssumps.push_back(fc);
+    }
+  }
+  else
+  {
+    scopeAssumps.push_back(f[1]);
+  }
+  Node conclusion = f[1];
+
+  // get the proof for conclusion
+  std::shared_ptr<ProofNode> pfb = lcp->mkProof(conclusion);
+  // call the scope method of proof node manager
+  std::shared_ptr<ProofNode> pf = d_pnm->mkScope(pfb, scopeAssumps);
+  return pf;
+}
+
+std::string TheoryEngineProofGenerator::identify() const
+{
+  return "TheoryEngineProofGenerator";
+}
+
+}  // namespace CVC4
diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h
new file mode 100644
index 000000000..c81a2c09b
--- /dev/null
+++ b/src/theory/theory_engine_proof_generator.h
@@ -0,0 +1,58 @@
+/*********************                                                        */
+/*! \file theory_engine.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The theory engine proof generator
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY_ENGINE_PROOF_GENERATOR_H
+#define CVC4__THEORY_ENGINE_PROOF_GENERATOR_H
+
+#include <memory>
+
+#include "context/cdhashmap.h"
+#include "context/context.h"
+#include "expr/lazy_proof.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+#include "theory/trust_node.h"
+
+namespace CVC4 {
+
+class TheoryEngineProofGenerator : public ProofGenerator
+{
+  typedef context::
+      CDHashMap<Node, std::shared_ptr<LazyCDProof>, NodeHashFunction>
+          NodeLazyCDProofMap;
+
+ public:
+  TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u);
+  ~TheoryEngineProofGenerator() {}
+  /** Set proof */
+  theory::TrustNode mkTrustExplain(TNode lit,
+                                   Node exp,
+                                   std::shared_ptr<LazyCDProof> lpf);
+  /** Get proof for */
+  std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /** Identify this generator (for debugging, etc..) */
+  std::string identify() const override;
+
+ private:
+  /** The proof manager, used for allocating new ProofNode objects */
+  ProofNodeManager* d_pnm;
+  /** Map from formulas to lazy CD proofs */
+  NodeLazyCDProofMap d_proofs;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY_ENGINE_PROOF_GENERATOR_H */
diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp
index 4c6246888..ff3e89154 100644
--- a/src/theory/trust_node.cpp
+++ b/src/theory/trust_node.cpp
@@ -15,7 +15,6 @@
 #include "theory/trust_node.h"
 
 #include "expr/proof_generator.h"
-#include "theory/proof_engine_output_channel.h"
 
 namespace CVC4 {
 namespace theory {
@@ -39,22 +38,25 @@ std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk)
 
 TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g)
 {
+  Node ckey = getConflictProven(conf);
   // if a generator is provided, should confirm that it can prove it
-  Assert(g == nullptr || g->hasProofFor(getConflictKeyValue(conf)));
-  return TrustNode(TrustNodeKind::CONFLICT, conf, g);
+  Assert(g == nullptr || g->hasProofFor(ckey));
+  return TrustNode(TrustNodeKind::CONFLICT, ckey, g);
 }
 
 TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g)
 {
+  Node lkey = getLemmaProven(lem);
   // if a generator is provided, should confirm that it can prove it
-  Assert(g == nullptr || g->hasProofFor(getLemmaKeyValue(lem)));
-  return TrustNode(TrustNodeKind::LEMMA, lem, g);
+  Assert(g == nullptr || g->hasProofFor(lkey));
+  return TrustNode(TrustNodeKind::LEMMA, lkey, g);
 }
 
 TrustNode TrustNode::mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g)
 {
-  Assert(g == nullptr || g->hasProofFor(getPropExpKeyValue(lit, exp)));
-  return TrustNode(TrustNodeKind::PROP_EXP, exp, g);
+  Node pekey = getPropExpProven(lit, exp);
+  Assert(g == nullptr || g->hasProofFor(pekey));
+  return TrustNode(TrustNodeKind::PROP_EXP, pekey, g);
 }
 
 TrustNode TrustNode::null()
@@ -62,50 +64,34 @@ TrustNode TrustNode::null()
   return TrustNode(TrustNodeKind::INVALID, Node::null());
 }
 
-TrustNode::TrustNode(TrustNodeKind tnk, Node n, ProofGenerator* g)
-    : d_tnk(tnk), d_node(n), d_gen(g)
+TrustNode::TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g)
+    : d_tnk(tnk), d_proven(p), d_gen(g)
 {
   // does not make sense to provide null node with generator
-  Assert(!d_node.isNull() || d_gen == nullptr);
+  Assert(!d_proven.isNull() || d_gen == nullptr);
 }
 
 TrustNodeKind TrustNode::getKind() const { return d_tnk; }
 
-Node TrustNode::getNode() const { return d_node; }
+Node TrustNode::getNode() const
+{
+  return d_tnk == TrustNodeKind::LEMMA ? d_proven : d_proven[0];
+}
 
+Node TrustNode::getProven() const { return d_proven; }
 ProofGenerator* TrustNode::getGenerator() const { return d_gen; }
 
-bool TrustNode::isNull() const { return d_node.isNull(); }
+bool TrustNode::isNull() const { return d_proven.isNull(); }
 
-Node TrustNode::getConflictKeyValue(Node conf) { return conf.negate(); }
+Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); }
 
-Node TrustNode::getLemmaKeyValue(Node lem) { return lem; }
+Node TrustNode::getLemmaProven(Node lem) { return lem; }
 
-Node TrustNode::getPropExpKeyValue(TNode lit, Node exp)
+Node TrustNode::getPropExpProven(TNode lit, Node exp)
 {
-  if (exp.isConst())
-  {
-    Assert(exp.getConst<bool>());
-    return lit;
-  }
   return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, lit);
 }
 
-Node TrustNode::getKeyValue(TrustNodeKind tnk, Node exp, Node conc)
-{
-  if (conc.isConst())
-  {
-    Assert(!conc.getConst<bool>());
-    return exp.negate();
-  }
-  if (exp.isConst())
-  {
-    Assert(exp.getConst<bool>());
-    return conc;
-  }
-  return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc);
-}
-
 std::ostream& operator<<(std::ostream& out, TrustNode n)
 {
   out << "(trust " << n.getNode() << ")";
diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h
index 3ced7efe9..8d3548bd5 100644
--- a/src/theory/trust_node.h
+++ b/src/theory/trust_node.h
@@ -87,28 +87,48 @@ class TrustNode
   ~TrustNode() {}
   /** get kind */
   TrustNodeKind getKind() const;
-  /** get node */
+  /** get node
+   *
+   * This is the node that is used in a common interface, either:
+   * (1) A T-unsat conjunction conf to pass to OutputChannel::conflict,
+   * (2) A valid T-formula lem to pass to OutputChannel::lemma, or
+   * (3) A conjunction of literals exp to return in Theory::explain(lit).
+   *
+   * Notice that this node does not necessarily correspond to a valid formula.
+   * The call getProven() below retrieves a valid formula corresponding to
+   * the above calls.
+   */
   Node getNode() const;
+  /** get proven
+   *
+   * This is the corresponding formula that is proven by the proof generator
+   * for the above cases:
+   * (1) (not conf), for conflicts,
+   * (2) lem, for lemmas,
+   * (3) (=> exp lit), for propagations from explanations.
+   *
+   * When constructing this trust node, the proof generator should be able to
+   * provide a proof for this fact.
+   */
+  Node getProven() const;
   /** get generator */
   ProofGenerator* getGenerator() const;
   /** is null? */
   bool isNull() const;
 
-  /** Get the node key for which conflict calls are cached */
-  static Node getConflictKeyValue(Node conf);
-  /** Get the node key for which lemma calls are cached */
-  static Node getLemmaKeyValue(Node lem);
-  /** Get the node key for which explanations for propagations are cached */
-  static Node getPropExpKeyValue(TNode lit, Node exp);
-  /** Get the node key for the exp => conc */
-  static Node getKeyValue(TrustNodeKind tnk, Node exp, Node conc);
+  /** Get the proven formula corresponding to a conflict call */
+  static Node getConflictProven(Node conf);
+  /** Get the proven formula corresponding to a lemma call */
+  static Node getLemmaProven(Node lem);
+  /** Get the proven formula corresponding to explanations for propagation*/
+  static Node getPropExpProven(TNode lit, Node exp);
 
  private:
-  TrustNode(TrustNodeKind tnk, Node n, ProofGenerator* g = nullptr);
+  TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g = nullptr);
   /** The kind */
   TrustNodeKind d_tnk;
-  /** The node */
-  Node d_node;
+  /** The proven node */
+  Node d_proven;
   /** The generator */
   ProofGenerator* d_gen;
 };
diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h
index 42783d31f..49529aa2f 100644
--- a/src/theory/uf/eq_proof.h
+++ b/src/theory/uf/eq_proof.h
@@ -97,7 +97,8 @@ class EqProof
       CDProof* p,
       std::unordered_set<Node, NodeHashFunction>& assumptions) const;
 
-  bool buildTransitivityChain(Node conclusion, std::vector<Node>& premises) const;
+  bool buildTransitivityChain(Node conclusion,
+                              std::vector<Node>& premises) const;
 
   // returns whether it did reordering
   void maybeAddSymmOrTrueIntroToProof(unsigned i,
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 504f43d72..ae7477480 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -456,7 +456,11 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, un
   enqueue(MergeCandidate(t1Id, t2Id, pid, reason));
 }
 
-bool EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) {
+bool EqualityEngine::assertPredicate(TNode t,
+                                     bool polarity,
+                                     TNode reason,
+                                     unsigned pid)
+{
   Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl;
   Assert(t.getKind() != kind::EQUAL) << "Use assertEquality instead";
   TNode b = polarity ? d_true : d_false;
@@ -469,7 +473,11 @@ bool EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsig
   return true;
 }
 
-bool EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) {
+bool EqualityEngine::assertEquality(TNode eq,
+                                    bool polarity,
+                                    TNode reason,
+                                    unsigned pid)
+{
   Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl;
   if (polarity) {
     // If two terms are already equal, don't assert anything
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index d600a546b..13a1d581c 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -394,9 +394,6 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
     // assumption (= y x). We modify the proof leaves to account for this
     // below.
 
-    // The free assumptions of the proof
-    std::map<Node, std::vector<ProofNode*>> famap;
-    pfConc->getFreeAssumptionsMap(famap);
     // we first ensure the assumptions are flattened
     std::unordered_set<Node, NodeHashFunction> ac;
     for (const TNode& a : assumps)
@@ -410,6 +407,9 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
         ac.insert(a);
       }
     }
+    // The free assumptions of the proof
+    std::map<Node, std::vector<ProofNode*>> famap;
+    pfConc->getFreeAssumptionsMap(famap);
     std::unordered_set<Node, NodeHashFunction> acu;
     std::unordered_set<Node, NodeHashFunction>::iterator itf;
     for (const std::pair<const Node, std::vector<ProofNode*>>& fa : famap)