1 files changed, 28 insertions, 1 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 382b1eb63..7408f4ba3 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -18,12 +18,17 @@
 #include "expr/node_manager.h"
 #include "proof/proof.h"
 #include "proof/proof_manager.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace preprocessing {
 
 AssertionPipeline::AssertionPipeline()
-    : d_realAssertionsEnd(0), d_assumptionsStart(0), d_numAssumptions(0)
+    : d_realAssertionsEnd(0),
+      d_storeSubstsInAsserts(false),
+      d_substsIndex(0),
+      d_assumptionsStart(0),
+      d_numAssumptions(0)
 {
 }
 
@@ -84,5 +89,27 @@ void AssertionPipeline::replace(size_t i, const std::vector<Node>& ns)
   }
 }
 
+void AssertionPipeline::enableStoreSubstsInAsserts()
+{
+  d_storeSubstsInAsserts = true;
+  d_substsIndex = d_nodes.size();
+  d_nodes.push_back(NodeManager::currentNM()->mkConst<bool>(true));
+}
+
+void AssertionPipeline::disableStoreSubstsInAsserts()
+{
+  d_storeSubstsInAsserts = false;
+}
+
+void AssertionPipeline::addSubstitutionNode(Node n)
+{
+  Assert(d_storeSubstsInAsserts);
+  Assert(n.getKind() == kind::EQUAL);
+  d_nodes[d_substsIndex] = theory::Rewriter::rewrite(
+      NodeManager::currentNM()->mkNode(kind::AND, n, d_nodes[d_substsIndex]));
+  Assert(theory::Rewriter::rewrite(d_nodes[d_substsIndex])
+         == d_nodes[d_substsIndex]);
+}
+
 }  // namespace preprocessing
 }  // namespace CVC4