Configurable substitution, working on TheoryEngine.

9 files changed, 361 insertions, 143 deletions

diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index f15e43553..d9a2d1711 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -60,6 +60,104 @@ 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..7cf6574cb 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -80,6 +80,12 @@ 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/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index ddc222ffb..b57bb112b 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,128 @@ 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
+      << "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 +215,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 +232,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 +247,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 +263,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 +290,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 +298,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 +312,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 +350,31 @@ 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..9291bbf9f 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,10 @@ 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 +99,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 +112,19 @@ 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/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 891f23cd2..bad121d65 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -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;
@@ -306,7 +307,7 @@ Node InferProofCons::convert(Inference infer,
         // possibly be done by CONCAT_EQ with !isRev.
         std::vector<Node> cexp;
         if (convertPredTransform(
-                mainEqCeq, conc, cexp, RewriterId::REWRITE_EQ_EXT))
+                mainEqCeq, conc, cexp, MethodId::SB_DEFAULT, MethodId::RW_REWRITE_EQ_EXT))
         {
           Trace("strings-ipc-core") << "Transformed to " << conc
                                     << " via pred transform" << std::endl;
@@ -901,7 +902,8 @@ 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))
@@ -914,10 +916,7 @@ 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())
   {
@@ -926,7 +925,7 @@ bool InferProofCons::convertPredTransform(Node src,
   }
   Trace("strings-ipc-debug")
       << "InferProofCons::convertPredTransform: success " << src
-      << " == " << tgt << " under " << exp << " via " << id << std::endl;
+      << " == " << tgt << " under " << exp << " via " << ids << "/" << idr << std::endl;
   // should definitely have concluded tgt
   Assert(res == tgt);
   return true;
@@ -934,14 +933,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,16 +950,14 @@ 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))
   {
@@ -972,6 +967,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)
diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h
index 612e67693..f5bb57996 100644
--- a/src/theory/strings/infer_proof_cons.h
+++ b/src/theory/strings/infer_proof_cons.h
@@ -126,17 +126,24 @@ 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);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 90f852f03..b571fc2b8 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2007,8 +2007,15 @@ theory::TrustNode TheoryEngine::getExplanation(
     std::vector<NodeTheoryPair>& explanationVector,
     LemmaProofRecipe* proofRecipe)
 {
-  Assert(explanationVector.size() > 0);
-
+  Assert(explanationVector.size() == 1);
+  
+  Node conclusion = explanationVector[0].d_node;
+  std::unique_ptr<LazyCDProof> lcp;
+  if (d_lazyProof!=nullptr)
+  {
+    // FIXME
+    //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
 
@@ -2021,7 +2028,6 @@ theory::TrustNode TheoryEngine::getExplanation(
     }
   });
 
-  std::vector<TrustNode> trNodes;
   while (i < explanationVector.size()) {
     // Get the current literal to explain
     NodeTheoryPair toExplain = explanationVector[i];
@@ -2032,15 +2038,20 @@ theory::TrustNode TheoryEngine::getExplanation(
         << 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)
+      {
+        // ------------------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);
+      }
       continue;
     }
 
@@ -2058,12 +2069,27 @@ theory::TrustNode TheoryEngine::getExplanation(
       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)
+      {
+        // toExplain.d_node[0] ... toExplain.d_node[n]
+        // --------------------------------------------MACRO_BSR_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);
+        lcp->addStep(toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args);
+      }
       ++ i;
       continue;
     }
@@ -2098,7 +2124,7 @@ theory::TrustNode TheoryEngine::getExplanation(
             }
           }
         })
-
+        // FIXME
         continue;
       }
     }
@@ -2120,11 +2146,20 @@ theory::TrustNode TheoryEngine::getExplanation(
           << theoryOf(toExplain.d_theory)->getId()
           << ". Explanation: " << texplanation.getNode() << std::endl;
     }
-    // process the trust node here
-    if (d_lazyProof!=nullptr)
+    if (lcp!=nullptr)
     {
-      processTrustNode(texplanation);
-      trNodes.push_back(texplanation);
+      // ----------- Via theory
+      // exp => lit                exp
+      // ---------------------------------MACRO_BSR_PRED_TRANSFORM
+      // lit
+      Node proven = texplanation.getProven();
+      lcp->addLazyStep(proven,texplanation.getGenerator());
+      std::vector<Node> children;
+      children.push_back(proven);
+      children.push_back(texplanation.getNode());
+      std::vector<Node> args;
+      args.push_back(toExplain.d_node);
+      lcp->addStep(toExplain.d_node,PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
     }
     Node explanation = texplanation.getNode();
 
@@ -2195,11 +2230,19 @@ theory::TrustNode TheoryEngine::getExplanation(
 
   Node exp = mkExplanation(explanationVector);
   
-  if (d_lazyProof!=nullptr)
+  if (lcp!=nullptr)
   {
+    Assert (lcp!=nullptr);
     // FIXME
-    // We have E1 => l1 ^ ... En => ln.
-    // Need to prove E1 ^ ... ^ En => ( l1 ^ ... ^ ln )
+    // get the proof for conclusion
+    std::shared_ptr<ProofNode> pfConc = lcp->mkProof(conclusion);
+    std::vector<Node> scopeAssumps;
+    for (size_t k = 0, esize = explanationVector.size(); k < esize; ++ k) 
+    {
+      scopeAssumps.push_back(explanationVector[k].d_node);
+    }
+    // call the scope method of proof node manager
+    std::shared_ptr<ProofNode> pf = d_pNodeManager->mkScope(pfConc, scopeAssumps);
   }
   
   return theory::TrustNode::mkTrustLemma(exp, nullptr);
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)