1 files changed, 23 insertions, 21 deletions

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 859eb84fc..f434e13ca 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -22,8 +22,10 @@
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
 #include "smt/dump.h"
+#include "smt/env.h"
 #include "smt/preprocess_proof_generator.h"
 #include "smt/smt_engine.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace cvc5::theory;
@@ -33,16 +35,16 @@ namespace cvc5 {
 namespace smt {
 
 Preprocessor::Preprocessor(SmtEngine& smt,
-                           context::UserContext* u,
+                           Env& env,
                            AbstractValues& abs,
                            SmtEngineStatistics& stats)
-    : d_context(u),
-      d_smt(smt),
+    : d_smt(smt),
+      d_env(env),
       d_absValues(abs),
       d_propagator(true, true),
-      d_assertionsProcessed(u, false),
-      d_exDefs(smt, *smt.getResourceManager(), stats),
-      d_processor(smt, d_exDefs, *smt.getResourceManager(), stats),
+      d_assertionsProcessed(env.getUserContext(), false),
+      d_exDefs(smt, d_env, stats),
+      d_processor(smt, *smt.getResourceManager(), stats),
       d_pnm(nullptr)
 {
 }
@@ -59,7 +61,7 @@ Preprocessor::~Preprocessor()
 void Preprocessor::finishInit()
 {
   d_ppContext.reset(new preprocessing::PreprocessingPassContext(
-      &d_smt, &d_propagator, d_pnm));
+      &d_smt, d_env, &d_propagator));
 
   // initialize the preprocessing passes
   d_processor.finishInit(d_ppContext.get());
@@ -111,7 +113,7 @@ void Preprocessor::cleanup() { d_processor.cleanup(); }
 Node Preprocessor::expandDefinitions(const Node& n, bool expandOnly)
 {
   std::unordered_map<Node, Node, NodeHashFunction> cache;
-  return d_exDefs.expandDefinitions(n, cache, expandOnly);
+  return expandDefinitions(n, cache, expandOnly);
 }
 
 Node Preprocessor::expandDefinitions(
@@ -127,8 +129,15 @@ Node Preprocessor::expandDefinitions(
     // Ensure node is type-checked at this point.
     n.getType(true);
   }
-  // expand only = true
-  return d_exDefs.expandDefinitions(n, cache, expandOnly);
+  // we apply substitutions here, before expanding definitions
+  theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
+  n = sm.apply(n);
+  if (!expandOnly)
+  {
+    // expand only = true
+    n = d_exDefs.expandDefinitions(n, cache, expandOnly);
+  }
+  return n;
 }
 
 Node Preprocessor::simplify(const Node& node)
@@ -139,17 +148,10 @@ Node Preprocessor::simplify(const Node& node)
     d_smt.getOutputManager().getPrinter().toStreamCmdSimplify(
         d_smt.getOutputManager().getDumpOut(), node);
   }
-  Node nas = d_absValues.substituteAbstractValues(node);
-  if (options::typeChecking())
-  {
-    // ensure node is type-checked at this point
-    nas.getType(true);
-  }
   std::unordered_map<Node, Node, NodeHashFunction> cache;
-  Node n = d_exDefs.expandDefinitions(nas, cache);
-  TrustNode ts = d_ppContext->getTopLevelSubstitutions().apply(n);
-  Node ns = ts.isNull() ? n : ts.getNode();
-  return ns;
+  Node ret = expandDefinitions(node, cache, false);
+  ret = theory::Rewriter::rewrite(ret);
+  return ret;
 }
 
 void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg)
@@ -157,7 +159,7 @@ void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg)
   Assert(pppg != nullptr);
   d_pnm = pppg->getManager();
   d_exDefs.setProofNodeManager(d_pnm);
-  d_propagator.setProof(d_pnm, d_context, pppg);
+  d_propagator.setProof(d_pnm, d_env.getUserContext(), pppg);
 }
 
 }  // namespace smt