Use substitutions for implementing defined functions (#6437)

This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions.
In other words, the effect of:

(define-fun f X t)
is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when
(= f (lambda X t)) was an equality solved by non-clausal simplification

The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula.

In this PR:

define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline.
Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit.
The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions.
The proof manager does not require a special case of using the define-function maps.
Define-function maps are eliminated from SmtEngine.
Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR.

21 files changed, 225 insertions, 488 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e59832896..af206c14d 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -220,7 +220,6 @@ libcvc5_add_sources(
   smt/check_models.h
   smt/command.cpp
   smt/command.h
-  smt/defined_function.h
   smt/dump.cpp
   smt/dump.h
   smt/dump_manager.cpp
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 4be6b4aac..99798e7d7 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -16,6 +16,7 @@
 #include "preprocessing/preprocessing_pass_context.h"
 
 #include "expr/node_algorithm.h"
+#include "smt/env.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
 
@@ -24,23 +25,33 @@ namespace preprocessing {
 
 PreprocessingPassContext::PreprocessingPassContext(
     SmtEngine* smt,
-    theory::booleans::CircuitPropagator* circuitPropagator,
-    ProofNodeManager* pnm)
+    Env& env,
+    theory::booleans::CircuitPropagator* circuitPropagator)
     : d_smt(smt),
-      d_resourceManager(smt->getResourceManager()),
-      d_topLevelSubstitutions(smt->getUserContext(), pnm),
+      d_env(env),
       d_circuitPropagator(circuitPropagator),
-      d_pnm(pnm),
-      d_symsInAssertions(smt->getUserContext())
+      d_symsInAssertions(env.getUserContext())
 {
 }
 
 theory::TrustSubstitutionMap&
 PreprocessingPassContext::getTopLevelSubstitutions()
 {
-  return d_topLevelSubstitutions;
+  return d_env.getTopLevelSubstitutions();
 }
 
+context::Context* PreprocessingPassContext::getUserContext()
+{
+  return d_env.getUserContext();
+}
+context::Context* PreprocessingPassContext::getDecisionContext()
+{
+  return d_env.getContext();
+}
+void PreprocessingPassContext::spendResource(Resource r)
+{
+  d_env.getResourceManager()->spendResource(r);
+}
 void PreprocessingPassContext::recordSymbolsInAssertions(
     const std::vector<Node>& assertions)
 {
@@ -67,14 +78,24 @@ void PreprocessingPassContext::addSubstitution(const Node& lhs,
                                                const Node& rhs,
                                                ProofGenerator* pg)
 {
-  d_topLevelSubstitutions.addSubstitution(lhs, rhs, pg);
+  getTopLevelSubstitutions().addSubstitution(lhs, rhs, pg);
+  // also add as a model substitution
+  addModelSubstitution(lhs, rhs);
+}
+
+void PreprocessingPassContext::addSubstitution(const Node& lhs,
+                                               const Node& rhs,
+                                               PfRule id,
+                                               const std::vector<Node>& args)
+{
+  getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args);
   // also add as a model substitution
   addModelSubstitution(lhs, rhs);
 }
 
 ProofNodeManager* PreprocessingPassContext::getProofNodeManager()
 {
-  return d_pnm;
+  return d_env.getProofNodeManager();
 }
 
 }  // namespace preprocessing
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index a7e9b0deb..a4ca166d8 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -43,14 +43,14 @@ class PreprocessingPassContext
  public:
   PreprocessingPassContext(
       SmtEngine* smt,
-      theory::booleans::CircuitPropagator* circuitPropagator,
-      ProofNodeManager* pnm);
+      Env& env,
+      theory::booleans::CircuitPropagator* circuitPropagator);
 
   SmtEngine* getSmt() { return d_smt; }
   TheoryEngine* getTheoryEngine() { return d_smt->getTheoryEngine(); }
   prop::PropEngine* getPropEngine() { return d_smt->getPropEngine(); }
-  context::Context* getUserContext() { return d_smt->getUserContext(); }
-  context::Context* getDecisionContext() { return d_smt->getContext(); }
+  context::Context* getUserContext();
+  context::Context* getDecisionContext();
 
   theory::booleans::CircuitPropagator* getCircuitPropagator()
   {
@@ -62,10 +62,7 @@ class PreprocessingPassContext
     return d_symsInAssertions;
   }
 
-  void spendResource(Resource r)
-  {
-    d_resourceManager->spendResource(r);
-  }
+  void spendResource(Resource r);
 
   /** Get the current logic info of the SmtEngine */
   const LogicInfo& getLogicInfo() { return d_smt->getLogicInfo(); }
@@ -97,6 +94,11 @@ class PreprocessingPassContext
   void addSubstitution(const Node& lhs,
                        const Node& rhs,
                        ProofGenerator* pg = nullptr);
+  /** Same as above, with proof id */
+  void addSubstitution(const Node& lhs,
+                       const Node& rhs,
+                       PfRule id,
+                       const std::vector<Node>& args);
 
   /** The the proof node manager associated with this context, if it exists */
   ProofNodeManager* getProofNodeManager();
@@ -104,18 +106,10 @@ class PreprocessingPassContext
  private:
   /** Pointer to the SmtEngine that this context was created in. */
   SmtEngine* d_smt;
-
-  /** Pointer to the ResourceManager for this context. */
-  ResourceManager* d_resourceManager;
-
-  /* The top level substitutions */
-  theory::TrustSubstitutionMap d_topLevelSubstitutions;
-
+  /** Reference to the environment. */
+  Env& d_env;
   /** Instance of the circuit propagator */
   theory::booleans::CircuitPropagator* d_circuitPropagator;
-  /** Pointer to the proof node manager, if it exists */
-  ProofNodeManager* d_pnm;
-
   /**
    * The (user-context-dependent) set of symbols that occur in at least one
    * assertion in the current user context.
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 779a63c29..7dc2e915d 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -25,7 +25,9 @@
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
 #include "smt/abstract_values.h"
+#include "smt/env.h"
 #include "smt/smt_engine.h"
+#include "theory/trust_substitutions.h"
 
 using namespace cvc5::theory;
 using namespace cvc5::kind;
@@ -33,10 +35,11 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace smt {
 
-Assertions::Assertions(context::UserContext* u, AbstractValues& absv)
-    : d_userContext(u),
+Assertions::Assertions(Env& env, AbstractValues& absv)
+    : d_env(env),
       d_absValues(absv),
-      d_assertionList(nullptr),
+      d_produceAssertions(false),
+      d_assertionList(env.getUserContext()),
       d_globalNegation(false),
       d_assertions()
 {
@@ -44,10 +47,6 @@ Assertions::Assertions(context::UserContext* u, AbstractValues& absv)
 
 Assertions::~Assertions()
 {
-  if (d_assertionList != nullptr)
-  {
-    d_assertionList->deleteSelf();
-  }
 }
 
 void Assertions::finishInit()
@@ -60,8 +59,8 @@ void Assertions::finishInit()
   {
     // In the case of incremental solving, we appear to need these to
     // ensure the relevant Nodes remain live.
-    d_assertionList = new (true) AssertionList(d_userContext);
-    d_globalDefineFunRecLemmas.reset(new std::vector<Node>());
+    d_produceAssertions = true;
+    d_globalDefineFunLemmas.reset(new std::vector<Node>());
   }
 }
 
@@ -107,16 +106,16 @@ void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
     Node n = d_absValues.substituteAbstractValues(e);
     // Ensure expr is type-checked at this point.
     ensureBoolean(n);
-    addFormula(n, inUnsatCore, true, true, false);
+    addFormula(n, inUnsatCore, true, true, false, false);
   }
-  if (d_globalDefineFunRecLemmas != nullptr)
+  if (d_globalDefineFunLemmas != nullptr)
   {
     // Global definitions are asserted at check-sat-time because we have to
     // make sure that they are always present (they are essentially level
     // zero assertions)
-    for (const Node& lemma : *d_globalDefineFunRecLemmas)
+    for (const Node& lemma : *d_globalDefineFunLemmas)
     {
-      addFormula(lemma, false, true, false, false);
+      addFormula(lemma, false, true, false, true, false);
     }
   }
 }
@@ -125,7 +124,7 @@ void Assertions::assertFormula(const Node& n, bool inUnsatCore)
 {
   ensureBoolean(n);
   bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
-  addFormula(n, inUnsatCore, true, false, maybeHasFv);
+  addFormula(n, inUnsatCore, true, false, false, maybeHasFv);
 }
 
 std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
@@ -139,27 +138,43 @@ preprocessing::AssertionPipeline& Assertions::getAssertionPipeline()
 
 context::CDList<Node>* Assertions::getAssertionList()
 {
-  return d_assertionList;
+  return d_produceAssertions ? &d_assertionList : nullptr;
 }
 
-void Assertions::addFormula(
-    TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv)
+void Assertions::addFormula(TNode n,
+                            bool inUnsatCore,
+                            bool inInput,
+                            bool isAssumption,
+                            bool isFunDef,
+                            bool maybeHasFv)
 {
   // add to assertion list if it exists
-  if (d_assertionList != nullptr)
+  if (d_produceAssertions)
   {
-    d_assertionList->push_back(n);
+    d_assertionList.push_back(n);
   }
   if (n.isConst() && n.getConst<bool>())
   {
     // true, nothing to do
     return;
   }
-
   Trace("smt") << "SmtEnginePrivate::addFormula(" << n
                << "), inUnsatCore = " << inUnsatCore
                << ", inInput = " << inInput
-               << ", isAssumption = " << isAssumption << std::endl;
+               << ", isAssumption = " << isAssumption
+               << ", isFunDef = " << isFunDef << std::endl;
+  if (isFunDef)
+  {
+    // if a non-recursive define-fun, just add as a top-level substitution
+    if (n.getKind() == EQUAL && n[0].isVar())
+    {
+      // A define-fun is an assumption in the overall proof, thus
+      // we justify the substitution with ASSUME here.
+      d_env.getTopLevelSubstitutions().addSubstitution(
+          n[0], n[1], PfRule::ASSUME, {}, {n});
+      return;
+    }
+  }
 
   // Ensure that it does not contain free variables
   if (maybeHasFv)
@@ -201,24 +216,21 @@ void Assertions::addFormula(
   d_assertions.push_back(n, isAssumption, true);
 }
 
-void Assertions::addDefineFunRecDefinition(Node n, bool global)
+void Assertions::addDefineFunDefinition(Node n, bool global)
 {
   n = d_absValues.substituteAbstractValues(n);
-  if (d_assertionList != nullptr)
-  {
-    d_assertionList->push_back(n);
-  }
-  if (global && d_globalDefineFunRecLemmas != nullptr)
+  if (global && d_globalDefineFunLemmas != nullptr)
   {
     // Global definitions are asserted at check-sat-time because we have to
     // make sure that they are always present
     Assert(!language::isInputLangSygus(options::inputLanguage()));
-    d_globalDefineFunRecLemmas->emplace_back(n);
+    d_globalDefineFunLemmas->emplace_back(n);
   }
   else
   {
-    bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
-    addFormula(n, false, true, false, maybeHasFv);
+    // we don't check for free variables here, since even if we are sygus,
+    // we could contain functions-to-synthesize within definitions.
+    addFormula(n, false, true, false, true, false);
   }
 }
 
diff --git a/src/smt/assertions.h b/src/smt/assertions.h
index 6ac3e58f5..c922cbaea 100644
--- a/src/smt/assertions.h
+++ b/src/smt/assertions.h
@@ -25,6 +25,9 @@
 #include "preprocessing/assertion_pipeline.h"
 
 namespace cvc5 {
+
+class Env;
+
 namespace smt {
 
 class AbstractValues;
@@ -42,7 +45,7 @@ class Assertions
   typedef context::CDList<Node> AssertionList;
 
  public:
-  Assertions(context::UserContext* u, AbstractValues& absv);
+  Assertions(Env& env, AbstractValues& absv);
   ~Assertions();
   /**
    * Finish initialization, called once after options are finalized. Sets up
@@ -81,12 +84,13 @@ class Assertions
    */
   void assertFormula(const Node& n, bool inUnsatCore = true);
   /**
-   * Assert that n corresponds to an assertion from a define-fun-rec command.
+   * Assert that n corresponds to an assertion from a define-fun or
+   * define-fun-rec command.
    * This assertion is added to the set of assertions maintained by this class.
    * If this has a global definition, this assertion is persistent for any
    * subsequent check-sat calls.
    */
-  void addDefineFunRecDefinition(Node n, bool global);
+  void addDefineFunDefinition(Node n, bool global);
   /**
    * Get the assertions pipeline, which contains the set of assertions we are
    * currently processing.
@@ -144,21 +148,24 @@ class Assertions
                   bool inUnsatCore,
                   bool inInput,
                   bool isAssumption,
+                  bool isFunDef,
                   bool maybeHasFv);
-  /** pointer to the user context */
-  context::UserContext* d_userContext;
+  /** Reference to the environment. */
+  Env& d_env;
   /** Reference to the abstract values utility */
   AbstractValues& d_absValues;
+  /** Whether we are producing assertions */
+  bool d_produceAssertions;
   /**
    * The assertion list (before any conversion) for supporting
    * getAssertions().  Only maintained if in incremental mode.
    */
-  AssertionList* d_assertionList;
+  AssertionList d_assertionList;
   /**
-   * List of lemmas generated for global recursive function definitions. We
+   * List of lemmas generated for global (recursive) function definitions. We
    * assert this list of definitions in each check-sat call.
    */
-  std::unique_ptr<std::vector<Node>> d_globalDefineFunRecLemmas;
+  std::unique_ptr<std::vector<Node>> d_globalDefineFunLemmas;
   /**
    * The list of assumptions from the previous call to checkSatisfiability.
    * Note that if the last call to checkSatisfiability was an entailment check,
diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h
deleted file mode 100644
index 89e636a65..000000000
--- a/src/smt/defined_function.h
+++ /dev/null
@@ -1,61 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Morgan Deters
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Defined function data structure.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__SMT__DEFINED_FUNCTION_H
-#define CVC5__SMT__DEFINED_FUNCTION_H
-
-#include <vector>
-
-#include "expr/node.h"
-
-namespace cvc5 {
-namespace smt {
-
-/**
- * Representation of a defined function.  We keep these around in
- * SmtEngine to permit expanding definitions late (and lazily), to
- * support getValue() over defined functions, to support user output
- * in terms of defined functions, etc.
- */
-class DefinedFunction
-{
- public:
-  DefinedFunction() {}
-  DefinedFunction(Node func, const std::vector<Node>& formals, Node formula)
-      : d_func(func), d_formals(formals), d_formula(formula)
-  {
-  }
-  /** get the function */
-  Node getFunction() const { return d_func; }
-  /** get the formal argument list of the function */
-  const std::vector<Node>& getFormals() const { return d_formals; }
-  /** get the formula that defines it */
-  Node getFormula() const { return d_formula; }
-
- private:
-  /** the function */
-  Node d_func;
-  /** the formal argument list */
-  std::vector<Node> d_formals;
-  /** the formula */
-  Node d_formula;
-}; /* class DefinedFunction */
-
-}  // namespace smt
-}  // namespace cvc5
-
-#endif /* CVC5__SMT__DEFINED_FUNCTION_H */
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 9bb66f649..f9e2a8458 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -24,6 +24,7 @@
 #include "smt/dump_manager.h"
 #include "smt/smt_engine_stats.h"
 #include "theory/rewriter.h"
+#include "theory/trust_substitutions.h"
 #include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 
@@ -37,6 +38,7 @@ Env::Env(NodeManager* nm, Options* opts)
       d_nodeManager(nm),
       d_proofNodeManager(nullptr),
       d_rewriter(new theory::Rewriter()),
+      d_topLevelSubs(new theory::TrustSubstitutionMap(d_userContext.get())),
       d_dumpManager(new DumpManager(d_userContext.get())),
       d_logic(),
       d_statisticsRegistry(std::make_unique<StatisticsRegistry>()),
@@ -54,8 +56,11 @@ Env::~Env() {}
 
 void Env::setProofNodeManager(ProofNodeManager* pnm)
 {
+  Assert(pnm != nullptr);
+  Assert(d_proofNodeManager == nullptr);
   d_proofNodeManager = pnm;
   d_rewriter->setProofNodeManager(pnm);
+  d_topLevelSubs->setProofNodeManager(pnm);
 }
 
 void Env::shutdown()
@@ -76,6 +81,11 @@ ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
 
 theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); }
 
+theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions()
+{
+  return *d_topLevelSubs.get();
+}
+
 DumpManager* Env::getDumpManager() { return d_dumpManager.get(); }
 
 const LogicInfo& Env::getLogicInfo() const { return d_logic; }
diff --git a/src/smt/env.h b/src/smt/env.h
index 12e0983cb..667497683 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -44,6 +44,7 @@ class DumpManager;
 
 namespace theory {
 class Rewriter;
+class TrustSubstitutionMap;
 }
 
 /**
@@ -84,6 +85,9 @@ class Env
   /** Get a pointer to the Rewriter owned by this Env. */
   theory::Rewriter* getRewriter();
 
+  /** Get a reference to the top-level substitution map */
+  theory::TrustSubstitutionMap& getTopLevelSubstitutions();
+
   /** Get a pointer to the underlying dump manager. */
   smt::DumpManager* getDumpManager();
 
@@ -122,8 +126,6 @@ class Env
  private:
   /* Private initialization ------------------------------------------------- */
 
-  /** Set the statistics registry */
-  void setStatisticsRegistry(StatisticsRegistry* statReg);
   /** Set proof node manager if it exists */
   void setProofNodeManager(ProofNodeManager* pnm);
 
@@ -157,6 +159,8 @@ class Env
    * specific to an SmtEngine/TheoryEngine instance.
    */
   std::unique_ptr<theory::Rewriter> d_rewriter;
+  /** The top level substitutions */
+  std::unique_ptr<theory::TrustSubstitutionMap> d_topLevelSubs;
   /** The dump manager */
   std::unique_ptr<smt::DumpManager> d_dumpManager;
   /**
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index d331e8e78..14182a46d 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -20,7 +20,7 @@
 
 #include "expr/node_manager_attributes.h"
 #include "preprocessing/assertion_pipeline.h"
-#include "smt/defined_function.h"
+#include "smt/env.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_stats.h"
 #include "theory/theory_engine.h"
@@ -32,10 +32,8 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace smt {
 
-ExpandDefs::ExpandDefs(SmtEngine& smt,
-                       ResourceManager& rm,
-                       SmtEngineStatistics& stats)
-    : d_smt(smt), d_resourceManager(rm), d_smtStats(stats), d_tpg(nullptr)
+ExpandDefs::ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats)
+    : d_smt(smt), d_env(env), d_smtStats(stats), d_tpg(nullptr)
 {
 }
 
@@ -57,7 +55,6 @@ TrustNode ExpandDefs::expandDefinitions(
     TConvProofGenerator* tpg)
 {
   const TNode orig = n;
-  NodeManager* nm = d_smt.getNodeManager();
   std::stack<std::tuple<Node, Node, bool>> worklist;
   std::stack<Node> result;
   worklist.push(std::make_tuple(Node(n), Node(n), false));
@@ -67,7 +64,7 @@ TrustNode ExpandDefs::expandDefinitions(
 
   do
   {
-    d_resourceManager.spendResource(Resource::PreprocessStep);
+    d_env.getResourceManager()->spendResource(Resource::PreprocessStep);
 
     // n is the input / original
     // node is the output / result
@@ -79,38 +76,9 @@ TrustNode ExpandDefs::expandDefinitions(
     // Working downwards
     if (!childrenPushed)
     {
-      Kind k = n.getKind();
-
       // we can short circuit (variable) leaves
       if (n.isVar())
       {
-        SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
-        SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(n);
-        if (i != dfuns->end())
-        {
-          Node f = (*i).second.getFormula();
-          const std::vector<Node>& formals = (*i).second.getFormals();
-          // replacement must be closed
-          if (!formals.empty())
-          {
-            f = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, formals), f);
-          }
-          // are we are producing proofs for this call?
-          if (tpg != nullptr)
-          {
-            // if this is a variable, we can simply assume it
-            // ------- ASSUME
-            // n = f
-            Node conc = n.eqNode(f);
-            tpg->addRewriteStep(n, f, PfRule::ASSUME, {}, {conc}, true);
-          }
-          // must recursively expand its definition
-          TrustNode tfe = expandDefinitions(f, cache, expandOnly, tpg);
-          Node fe = tfe.isNull() ? f : tfe.getNode();
-          // don't bother putting in the cache
-          result.push(fe);
-          continue;
-        }
         // don't bother putting in the cache
         result.push(n);
         continue;
@@ -125,132 +93,7 @@ TrustNode ExpandDefs::expandDefinitions(
         result.push(ret.isNull() ? n : ret);
         continue;
       }
-
-      // otherwise expand it
-      bool doExpand = false;
-      if (k == APPLY_UF)
-      {
-        // Always do beta-reduction here. The reason is that there may be
-        // operators such as INTS_MODULUS in the body of the lambda that would
-        // otherwise be introduced by beta-reduction via the rewriter, but are
-        // not expanded here since the traversal in this function does not
-        // traverse the operators of nodes. Hence, we beta-reduce here to
-        // ensure terms in the body of the lambda are expanded during this
-        // call.
-        if (n.getOperator().getKind() == LAMBDA)
-        {
-          doExpand = true;
-        }
-        else
-        {
-          // We always check if this operator corresponds to a defined function.
-          doExpand = d_smt.isDefinedFunction(n.getOperator());
-        }
-      }
-      // the premise of the proof of expansion (if we are expanding a definition
-      // and proofs are enabled)
-      std::vector<Node> pfExpChildren;
-      if (doExpand)
-      {
-        std::vector<Node> formals;
-        TNode fm;
-        if (n.getOperator().getKind() == LAMBDA)
-        {
-          TNode op = n.getOperator();
-          // lambda
-          for (unsigned i = 0; i < op[0].getNumChildren(); i++)
-          {
-            formals.push_back(op[0][i]);
-          }
-          fm = op[1];
-        }
-        else
-        {
-          // application of a user-defined symbol
-          TNode func = n.getOperator();
-          SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
-          SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func);
-          if (i == dfuns->end())
-          {
-            throw TypeCheckingExceptionPrivate(
-                n,
-                std::string("Undefined function: `") + func.toString() + "'");
-          }
-          DefinedFunction def = (*i).second;
-          formals = def.getFormals();
-
-          if (Debug.isOn("expand"))
-          {
-            Debug("expand") << "found: " << n << std::endl;
-            Debug("expand") << " func: " << func << std::endl;
-            std::string name = func.getAttribute(expr::VarNameAttr());
-            Debug("expand") << "     : \"" << name << "\"" << std::endl;
-          }
-          if (Debug.isOn("expand"))
-          {
-            Debug("expand") << " defn: " << def.getFunction() << std::endl
-                            << "       [";
-            if (formals.size() > 0)
-            {
-              copy(formals.begin(),
-                   formals.end() - 1,
-                   std::ostream_iterator<Node>(Debug("expand"), ", "));
-              Debug("expand") << formals.back();
-            }
-            Debug("expand")
-                << "]" << std::endl
-                << "       " << def.getFunction().getType() << std::endl
-                << "       " << def.getFormula() << std::endl;
-          }
-
-          fm = def.getFormula();
-          // are we producing proofs for this call?
-          if (tpg != nullptr)
-          {
-            Node pfRhs = fm;
-            if (!formals.empty())
-            {
-              Node bvl = nm->mkNode(BOUND_VAR_LIST, formals);
-              pfRhs = nm->mkNode(LAMBDA, bvl, pfRhs);
-            }
-            Assert(func.getType().isComparableTo(pfRhs.getType()));
-            pfExpChildren.push_back(func.eqNode(pfRhs));
-          }
-        }
-
-        Node instance = fm.substitute(formals.begin(),
-                                      formals.end(),
-                                      n.begin(),
-                                      n.begin() + formals.size());
-        Debug("expand") << "made : " << instance << std::endl;
-        // are we producing proofs for this call?
-        if (tpg != nullptr)
-        {
-          if (n != instance)
-          {
-            // This code is run both when we are doing expand definitions and
-            // simple beta reduction.
-            //
-            // f = (lambda ((x T)) t)  [if we are expanding a definition]
-            // ---------------------- MACRO_SR_PRED_INTRO
-            // n = instance
-            Node conc = n.eqNode(instance);
-            tpg->addRewriteStep(n,
-                                instance,
-                                PfRule::MACRO_SR_PRED_INTRO,
-                                pfExpChildren,
-                                {conc},
-                                true);
-          }
-        }
-        // now, call expand definitions again on the result
-        TrustNode texp = expandDefinitions(instance, cache, expandOnly, tpg);
-        Node expanded = texp.isNull() ? instance : texp.getNode();
-        cache[n] = n == expanded ? Node::null() : expanded;
-        result.push(expanded);
-        continue;
-      }
-      else if (!expandOnly)
+      if (!expandOnly)
       {
         // do not do any theory stuff if expandOnly is true
 
@@ -331,35 +174,12 @@ TrustNode ExpandDefs::expandDefinitions(
   return TrustNode::mkTrustRewrite(orig, res, tpg);
 }
 
-void ExpandDefs::expandAssertions(AssertionPipeline& assertions,
-                                  bool expandOnly)
-{
-  Chat() << "expanding definitions in assertions..." << std::endl;
-  Trace("exp-defs") << "ExpandDefs::simplify(): expanding definitions"
-                    << std::endl;
-  TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime);
-  std::unordered_map<Node, Node, NodeHashFunction> cache;
-  for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i)
-  {
-    Node assert = assertions[i];
-    // notice we call this method with only one value of expandOnly currently,
-    // hence we maintain only a single set of proof steps in d_tpg.
-    TrustNode expd = expandDefinitions(assert, cache, expandOnly, d_tpg.get());
-    if (!expd.isNull())
-    {
-      Trace("exp-defs") << "ExpandDefs::expandAssertions: " << assert << " -> "
-                        << expd.getNode() << std::endl;
-      assertions.replaceTrusted(i, expd);
-    }
-  }
-}
-
 void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm)
 {
   if (d_tpg == nullptr)
   {
     d_tpg.reset(new TConvProofGenerator(pnm,
-                                        d_smt.getUserContext(),
+                                        d_env.getUserContext(),
                                         TConvPolicy::FIXPOINT,
                                         TConvCachePolicy::NEVER,
                                         "ExpandDefs::TConvProofGenerator",
diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index c0a92214a..d6fe8ba0d 100644
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -25,8 +25,8 @@
 
 namespace cvc5 {
 
+class Env;
 class ProofNodeManager;
-class ResourceManager;
 class SmtEngine;
 class TConvProofGenerator;
 
@@ -47,7 +47,7 @@ struct SmtEngineStatistics;
 class ExpandDefs
 {
  public:
-  ExpandDefs(SmtEngine& smt, ResourceManager& rm, SmtEngineStatistics& stats);
+  ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats);
   ~ExpandDefs();
   /**
    * Expand definitions in term n. Return the expanded form of n.
@@ -62,12 +62,6 @@ class ExpandDefs
       TNode n,
       std::unordered_map<Node, Node, NodeHashFunction>& cache,
       bool expandOnly = false);
-  /**
-   * Expand defintitions in assertions. This applies this above method to each
-   * assertion in the given pipeline.
-   */
-  void expandAssertions(preprocessing::AssertionPipeline& assertions,
-                        bool expandOnly = false);
 
   /**
    * Set proof node manager, which signals this class to enable proofs using the
@@ -87,8 +81,8 @@ class ExpandDefs
       TConvProofGenerator* tpg);
   /** Reference to the SMT engine */
   SmtEngine& d_smt;
-  /** Reference to resource manager */
-  ResourceManager& d_resourceManager;
+  /** Reference to the environment. */
+  Env& d_env;
   /** Reference to the SMT stats */
   SmtEngineStatistics& d_smtStats;
   /** A proof generator for the term conversion. */
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
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index c590b7164..e0ad2cc14 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -25,6 +25,7 @@
 #include "theory/booleans/circuit_propagator.h"
 
 namespace cvc5 {
+class Env;
 namespace preprocessing {
 class PreprocessingPassContext;
 }
@@ -46,7 +47,7 @@ class Preprocessor
 {
  public:
   Preprocessor(SmtEngine& smt,
-               context::UserContext* u,
+               Env& env,
                AbstractValues& abs,
                SmtEngineStatistics& stats);
   ~Preprocessor();
@@ -94,17 +95,16 @@ class Preprocessor
       const Node& n,
       std::unordered_map<Node, Node, NodeHashFunction>& cache,
       bool expandOnly = false);
-
   /**
    * Set proof node manager. Enables proofs in this preprocessor.
    */
   void setProofGenerator(PreprocessProofGenerator* pppg);
 
  private:
-  /** A copy of the current context */
-  context::Context* d_context;
   /** Reference to the parent SmtEngine */
   SmtEngine& d_smt;
+  /** Reference to the env */
+  Env& d_env;
   /** Reference to the abstract values utility */
   AbstractValues& d_absValues;
   /**
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index fa230cd54..cf747c360 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -31,7 +31,6 @@
 #include "preprocessing/preprocessing_pass_registry.h"
 #include "printer/printer.h"
 #include "smt/assertions.h"
-#include "smt/defined_function.h"
 #include "smt/dump.h"
 #include "smt/expand_definitions.h"
 #include "smt/smt_engine.h"
@@ -59,11 +58,9 @@ class ScopeCounter
 };
 
 ProcessAssertions::ProcessAssertions(SmtEngine& smt,
-                                     ExpandDefs& exDefs,
                                      ResourceManager& rm,
                                      SmtEngineStatistics& stats)
     : d_smt(smt),
-      d_exDefs(exDefs),
       d_resourceManager(rm),
       d_smtStats(stats),
       d_preprocessingPassContext(nullptr)
@@ -136,11 +133,11 @@ bool ProcessAssertions::apply(Assertions& as)
       << "ProcessAssertions::processAssertions() : pre-definition-expansion"
       << endl;
   dumpAssertions("pre-definition-expansion", assertions);
-  // Expand definitions, which replaces defined functions with their definition
-  // and does beta reduction. Notice we pass true as the second argument since
-  // we do not want to call theories to expand definitions here, since we want
+  // Apply substitutions first. If we are non-incremental, this has only the
+  // effect of replacing defined functions with their definitions.
+  // We do not call theory-specific expand definitions here, since we want
   // to give the opportunity to rewrite/preprocess terms before expansion.
-  d_exDefs.expandAssertions(assertions, true);
+  d_passes["apply-substs"]->apply(&assertions);
   Trace("smt-proc")
       << "ProcessAssertions::processAssertions() : post-definition-expansion"
       << endl;
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index aeea68ef6..3cdf8a463 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -37,7 +37,6 @@ class PreprocessingPassContext;
 namespace smt {
 
 class Assertions;
-class ExpandDefs;
 struct SmtEngineStatistics;
 
 /**
@@ -62,7 +61,6 @@ class ProcessAssertions
 
  public:
   ProcessAssertions(SmtEngine& smt,
-                    ExpandDefs& exDefs,
                     ResourceManager& rm,
                     SmtEngineStatistics& stats);
   ~ProcessAssertions();
@@ -85,8 +83,6 @@ class ProcessAssertions
  private:
   /** Reference to the SMT engine */
   SmtEngine& d_smt;
-  /** Reference to expand definitions module */
-  ExpandDefs& d_exDefs;
   /** Reference to resource manager */
   ResourceManager& d_resourceManager;
   /** Reference to the SMT stats */
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 422efac6a..53633a123 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -23,7 +23,6 @@
 #include "options/smt_options.h"
 #include "proof/dot/dot_printer.h"
 #include "smt/assertions.h"
-#include "smt/defined_function.h"
 #include "smt/preprocess_proof_generator.h"
 #include "smt/proof_post_processor.h"
 
@@ -85,9 +84,7 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
 
 PfManager::~PfManager() {}
 
-void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn,
-                              Assertions& as,
-                              DefinedFunctionMap& df)
+void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn, Assertions& as)
 {
   // Note this assumes that setFinalProof is only called once per unsat
   // response. This method would need to cache its result otherwise.
@@ -102,7 +99,7 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn,
   }
 
   std::vector<Node> assertions;
-  getAssertions(as, df, assertions);
+  getAssertions(as, assertions);
 
   if (Trace.isOn("smt-proof"))
   {
@@ -140,11 +137,10 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn,
 
 void PfManager::printProof(std::ostream& out,
                            std::shared_ptr<ProofNode> pfn,
-                           Assertions& as,
-                           DefinedFunctionMap& df)
+                           Assertions& as)
 {
   Trace("smt-proof") << "PfManager::printProof: start" << std::endl;
-  std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df);
+  std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as);
   // if we are in incremental mode, we don't want to invalidate the proof
   // nodes in fp, since these may be reused in further check-sat calls
   if (options::incrementalSolving()
@@ -166,12 +162,10 @@ void PfManager::printProof(std::ostream& out,
     out << "\n)\n";
   }
 }
-void PfManager::checkProof(std::shared_ptr<ProofNode> pfn,
-                           Assertions& as,
-                           DefinedFunctionMap& df)
+void PfManager::checkProof(std::shared_ptr<ProofNode> pfn, Assertions& as)
 {
   Trace("smt-proof") << "PfManager::checkProof: start" << std::endl;
-  std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df);
+  std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as);
   Trace("smt-proof-debug") << "PfManager::checkProof: returned " << *fp.get()
                            << std::endl;
 }
@@ -186,15 +180,14 @@ smt::PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const
 }
 
 std::shared_ptr<ProofNode> PfManager::getFinalProof(
-    std::shared_ptr<ProofNode> pfn, Assertions& as, DefinedFunctionMap& df)
+    std::shared_ptr<ProofNode> pfn, Assertions& as)
 {
-  setFinalProof(pfn, as, df);
+  setFinalProof(pfn, as);
   Assert(d_finalProof);
   return d_finalProof;
 }
 
 void PfManager::getAssertions(Assertions& as,
-                              DefinedFunctionMap& df,
                               std::vector<Node>& assertions)
 {
   context::CDList<Node>* al = as.getAssertionList();
@@ -204,20 +197,6 @@ void PfManager::getAssertions(Assertions& as,
   {
     assertions.push_back(*i);
   }
-  NodeManager* nm = NodeManager::currentNM();
-  for (const std::pair<const Node, const smt::DefinedFunction>& dfn : df)
-  {
-    Node def = dfn.second.getFormula();
-    const std::vector<Node>& formals = dfn.second.getFormals();
-    if (!formals.empty())
-    {
-      Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, formals);
-      def = nm->mkNode(kind::LAMBDA, bvl, def);
-    }
-    // assume the (possibly higher order) equality
-    Node eq = dfn.first.eqNode(def);
-    assertions.push_back(eq);
-  }
 }
 
 }  // namespace smt
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index 60e93306a..57478573c 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -31,7 +31,6 @@ class SmtEngine;
 namespace smt {
 
 class Assertions;
-class DefinedFunction;
 class PreprocessProofGenerator;
 class ProofPostproccess;
 
@@ -70,10 +69,6 @@ class ProofPostproccess;
  */
 class PfManager
 {
-  /** The type of our internal map of defined functions */
-  using DefinedFunctionMap =
-      context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>;
-
  public:
   PfManager(context::UserContext* u, SmtEngine* smte);
   ~PfManager();
@@ -83,20 +78,17 @@ class PfManager
    * The argument pfn is the proof for false in the current context.
    *
    * Throws an assertion failure if pg cannot provide a closed proof with
-   * respect to assertions in as and df. For the latter, entries in the defined
-   * function map correspond to equalities of the form (= f (lambda (...) t)),
-   * which are considered assertions in the final proof.
+   * respect to assertions in as. Note this includes equalities of the form
+   * (= f (lambda (...) t)) which originate from define-fun commands for f.
+   * These are considered assertions in the final proof.
    */
   void printProof(std::ostream& out,
                   std::shared_ptr<ProofNode> pfn,
-                  Assertions& as,
-                  DefinedFunctionMap& df);
+                  Assertions& as);
   /**
    * Check proof, same as above, without printing.
    */
-  void checkProof(std::shared_ptr<ProofNode> pfn,
-                  Assertions& as,
-                  DefinedFunctionMap& df);
+  void checkProof(std::shared_ptr<ProofNode> pfn, Assertions& as);
 
   /**
    * Get final proof.
@@ -104,8 +96,7 @@ class PfManager
    * The argument pfn is the proof for false in the current context.
    */
   std::shared_ptr<ProofNode> getFinalProof(std::shared_ptr<ProofNode> pfn,
-                                           Assertions& as,
-                                           DefinedFunctionMap& df);
+                                           Assertions& as);
   //--------------------------- access to utilities
   /** Get a pointer to the ProofChecker owned by this. */
   ProofChecker* getProofChecker() const;
@@ -119,14 +110,11 @@ class PfManager
    * Set final proof, which initializes d_finalProof to the given proof node of
    * false, postprocesses it, and stores it in d_finalProof.
    */
-  void setFinalProof(std::shared_ptr<ProofNode> pfn,
-                     Assertions& as,
-                     DefinedFunctionMap& df);
+  void setFinalProof(std::shared_ptr<ProofNode> pfn, Assertions& as);
   /**
    * Get assertions from the assertions
    */
   void getAssertions(Assertions& as,
-                     DefinedFunctionMap& df,
                      std::vector<Node>& assertions);
   /** The false node */
   Node d_false;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ef338fdfe..cee07a3dc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -40,7 +40,6 @@
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
 #include "smt/check_models.h"
-#include "smt/defined_function.h"
 #include "smt/dump.h"
 #include "smt/dump_manager.h"
 #include "smt/env.h"
@@ -88,7 +87,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
     : d_env(new Env(nm, optr)),
       d_state(new SmtEngineState(getContext(), getUserContext(), *this)),
       d_absValues(new AbstractValues(getNodeManager())),
-      d_asserts(new Assertions(getUserContext(), *d_absValues.get())),
+      d_asserts(new Assertions(*d_env.get(), *d_absValues.get())),
       d_routListener(new ResourceOutListener(*this)),
       d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)),
       d_smtSolver(nullptr),
@@ -97,7 +96,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
       d_checkModels(nullptr),
       d_pfManager(nullptr),
       d_ucManager(nullptr),
-      d_definedFunctions(nullptr),
       d_sygusSolver(nullptr),
       d_abductSolver(nullptr),
       d_interpolSolver(nullptr),
@@ -131,8 +129,8 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
   // make statistics
   d_stats.reset(new SmtEngineStatistics());
   // reset the preprocessor
-  d_pp.reset(new smt::Preprocessor(
-      *this, getUserContext(), *d_absValues.get(), *d_stats));
+  d_pp.reset(
+      new smt::Preprocessor(*this, *d_env.get(), *d_absValues.get(), *d_stats));
   // make the SMT solver
   d_smtSolver.reset(
       new SmtSolver(*this, *d_state, getResourceManager(), *d_pp, *d_stats));
@@ -151,8 +149,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
   // being parsed from the input file. Because of this, we cannot trust
   // that d_env->getOption(options::unsatCores) is set correctly yet.
   d_proofManager.reset(new ProofManager(getUserContext()));
-
-  d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
 }
 
 bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); }
@@ -318,8 +314,6 @@ SmtEngine::~SmtEngine()
     // of context-dependent data structures
     d_state->cleanup();
 
-    d_definedFunctions->deleteSelf();
-
     //destroy all passes before destroying things that they refer to
     d_pp->cleanup();
 
@@ -646,36 +640,26 @@ void SmtEngine::defineFunction(Node func,
   ss << language::SetLanguage(
             language::SetLanguage::getLanguage(Dump.getStream()))
      << func;
-  std::vector<Node> nFormals;
-  nFormals.reserve(formals.size());
 
-  for (const Node& formal : formals)
-  {
-    nFormals.push_back(formal);
-  }
-
-  DefineFunctionNodeCommand nc(ss.str(), func, nFormals, formula);
+  DefineFunctionNodeCommand nc(ss.str(), func, formals, formula);
   getDumpManager()->addToDump(nc, "declarations");
 
   // type check body
   debugCheckFunctionBody(formula, formals, func);
 
   // Substitute out any abstract values in formula
-  Node formNode = d_absValues->substituteAbstractValues(formula);
-  DefinedFunction def(func, formals, formNode);
-  // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
-  // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
-  // d_haveAdditions = true;
-  Debug("smt") << "definedFunctions insert " << func << " " << formNode << endl;
-
-  if (global)
-  {
-    d_definedFunctions->insertAtContextLevelZero(func, def);
-  }
-  else
+  Node def = d_absValues->substituteAbstractValues(formula);
+  if (!formals.empty())
   {
-    d_definedFunctions->insert(func, def);
+    NodeManager* nm = NodeManager::currentNM();
+    def = nm->mkNode(
+        kind::LAMBDA, nm->mkNode(kind::BOUND_VAR_LIST, formals), def);
   }
+  // A define-fun is treated as a (higher-order) assertion. It is provided
+  // to the assertions object. It will be added as a top-level substitution
+  // within this class, possibly multiple times if global is true.
+  Node feq = func.eqNode(def);
+  d_asserts->addDefineFunDefinition(feq, global);
 }
 
 void SmtEngine::defineFunctionsRec(
@@ -748,7 +732,7 @@ void SmtEngine::defineFunctionsRec(
     //   notice we don't call assertFormula directly, since this would
     //   duplicate the output on raw-benchmark.
     // add define recursive definition to the assertions
-    d_asserts->addDefineFunRecDefinition(lem, global);
+    d_asserts->addDefineFunDefinition(lem, global);
   }
 }
 
@@ -766,12 +750,6 @@ void SmtEngine::defineFunctionRec(Node func,
   defineFunctionsRec(funcs, formals_multi, formulas, global);
 }
 
-bool SmtEngine::isDefinedFunction(Node func)
-{
-  Debug("smt") << "isDefined function " << func << "?" << std::endl;
-  return d_definedFunctions->find(func) != d_definedFunctions->end();
-}
-
 Result SmtEngine::quickCheck() {
   Assert(d_state->isFullyInited());
   Trace("smt") << "SMT quickCheck()" << endl;
@@ -1295,6 +1273,7 @@ Result SmtEngine::blockModel()
       ModelBlocker::getModelBlocker(eassertsProc,
                                     m->getTheoryModel(),
                                     d_env->getOption(options::blockModelsMode));
+  Trace("smt") << "Block formula: " << eblocker << std::endl;
   return assertFormula(eblocker);
 }
 
@@ -1402,7 +1381,7 @@ void SmtEngine::checkProof()
   std::shared_ptr<ProofNode> pePfn = pe->getProof();
   if (d_env->getOption(options::checkProofs))
   {
-    d_pfManager->checkProof(pePfn, *d_asserts, *d_definedFunctions);
+    d_pfManager->checkProof(pePfn, *d_asserts);
   }
 }
 
@@ -1445,8 +1424,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
     pepf = pe->getProof();
   }
   Assert(pepf != nullptr);
-  std::shared_ptr<ProofNode> pfn =
-      d_pfManager->getFinalProof(pepf, *d_asserts, *d_definedFunctions);
+  std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(pepf, *d_asserts);
   std::vector<Node> core;
   d_ucManager->getUnsatCore(pfn, *d_asserts, core);
   return UnsatCore(core);
@@ -1539,8 +1517,8 @@ void SmtEngine::getRelevantInstantiationTermVectors(
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
   Assert(pe->getProof() != nullptr);
-  std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(
-      pe->getProof(), *d_asserts, *d_definedFunctions);
+  std::shared_ptr<ProofNode> pfn =
+      d_pfManager->getFinalProof(pe->getProof(), *d_asserts);
   d_ucManager->getRelevantInstantiations(pfn, insts);
 }
 
@@ -1569,7 +1547,7 @@ std::string SmtEngine::getProof()
   Assert(pe->getProof() != nullptr);
   Assert(d_pfManager);
   std::ostringstream ss;
-  d_pfManager->printProof(ss, pe->getProof(), *d_asserts, *d_definedFunctions);
+  d_pfManager->printProof(ss, pe->getProof(), *d_asserts);
   return ss.str();
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 860caffa8..a7e39e004 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -94,13 +94,6 @@ class SygusSolver;
 class AbductionSolver;
 class InterpolationSolver;
 class QuantElimSolver;
-/**
- * Representation of a defined function.  We keep these around in
- * SmtEngine to permit expanding definitions late (and lazily), to
- * support getValue() over defined functions, to support user output
- * in terms of defined functions, etc.
- */
-class DefinedFunction;
 
 struct SmtEngineStatistics;
 class SmtScope;
@@ -335,9 +328,6 @@ class CVC5_EXPORT SmtEngine
                       Node formula,
                       bool global = false);
 
-  /** Return true if given expression is a defined function. */
-  bool isDefinedFunction(Node func);
-
   /**
    * Define functions recursive
    *
@@ -891,13 +881,6 @@ class CVC5_EXPORT SmtEngine
 
   /** Get a pointer to the Rewriter owned by this SmtEngine. */
   theory::Rewriter* getRewriter();
-
-  /** The type of our internal map of defined functions */
-  using DefinedFunctionMap =
-      context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>;
-
-  /** Get the defined function map */
-  DefinedFunctionMap* getDefinedFunctionMap() { return d_definedFunctions; }
   /**
    * Get expanded assertions.
    *
@@ -1115,9 +1098,6 @@ class CVC5_EXPORT SmtEngine
    * from refutations. */
   std::unique_ptr<smt::UnsatCoreManager> d_ucManager;
 
-  /** An index of our defined functions */
-  DefinedFunctionMap* d_definedFunctions;
-
   /** The solver for sygus queries */
   std::unique_ptr<smt::SygusSolver> d_sygusSolver;
 
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 0976442e1..317bb2646 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -31,6 +31,7 @@
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/sygus_utils.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace cvc5::theory;
@@ -384,7 +385,12 @@ void SygusSolver::checkSynthSolution(Assertions& as)
     // definitions that were added as assertions to the sygus problem.
     for (Node a : auxAssertions)
     {
-      solChecker->assertFormula(a);
+      // We require rewriting here, e.g. so that define-fun from the original
+      // problem are rewritten to true. If this is not the case, then the
+      // assertions module of the subsolver will complain about assertions
+      // with free variables.
+      Node ar = theory::Rewriter::rewrite(a);
+      solChecker->assertFormula(ar);
     }
     Result r = solChecker->checkSat();
     Notice() << "SygusSolver::checkSynthSolution(): result is " << r
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index 4088deb94..47507bfe0 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -27,21 +27,32 @@ TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c,
                                            MethodId ids)
     : d_ctx(c),
       d_subs(c),
-      d_pnm(pnm),
       d_tsubs(c),
-      d_tspb(pnm ? new TheoryProofStepBuffer(pnm->getChecker()) : nullptr),
-      d_subsPg(
-          pnm ? new LazyCDProof(pnm, nullptr, c, "TrustSubstitutionMap::subsPg")
-              : nullptr),
-      d_applyPg(pnm ? new LazyCDProof(
-                          pnm, nullptr, c, "TrustSubstitutionMap::applyPg")
-                    : nullptr),
-      d_helperPf(pnm, c),
+      d_tspb(nullptr),
+      d_subsPg(nullptr),
+      d_applyPg(nullptr),
+      d_helperPf(nullptr),
       d_name(name),
       d_trustId(trustId),
       d_ids(ids),
       d_eqtIndex(c)
 {
+  setProofNodeManager(pnm);
+}
+
+void TrustSubstitutionMap::setProofNodeManager(ProofNodeManager* pnm)
+{
+  if (pnm != nullptr)
+  {
+    // should not set the proof node manager more than once
+    Assert(d_tspb == nullptr);
+    d_tspb.reset(new TheoryProofStepBuffer(pnm->getChecker())),
+        d_subsPg.reset(new LazyCDProof(
+            pnm, nullptr, d_ctx, "TrustSubstitutionMap::subsPg"));
+    d_applyPg.reset(
+        new LazyCDProof(pnm, nullptr, d_ctx, "TrustSubstitutionMap::applyPg"));
+    d_helperPf.reset(new CDProofSet<LazyCDProof>(pnm, d_ctx));
+  }
 }
 
 void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg)
@@ -69,7 +80,7 @@ void TrustSubstitutionMap::addSubstitution(TNode x,
     addSubstitution(x, t, nullptr);
     return;
   }
-  LazyCDProof* stepPg = d_helperPf.allocateProof(nullptr, d_ctx);
+  LazyCDProof* stepPg = d_helperPf->allocateProof(nullptr, d_ctx);
   Node eq = x.eqNode(t);
   stepPg->addStep(eq, id, children, args);
   addSubstitution(x, t, stepPg);
@@ -100,7 +111,7 @@ ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x,
     Trace("trust-subs") << "...use generator directly" << std::endl;
     return tn.getGenerator();
   }
-  LazyCDProof* solvePg = d_helperPf.allocateProof(nullptr, d_ctx);
+  LazyCDProof* solvePg = d_helperPf->allocateProof(nullptr, d_ctx);
   // Try to transform tn.getProven() to (= x t) here, if necessary
   if (!d_tspb->applyPredTransform(proven, eq, {}))
   {
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index e8b627249..ec5b2ffb5 100644
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -42,10 +42,12 @@ class TrustSubstitutionMap : public ProofGenerator
 
  public:
   TrustSubstitutionMap(context::Context* c,
-                       ProofNodeManager* pnm,
+                       ProofNodeManager* pnm = nullptr,
                        std::string name = "TrustSubstitutionMap",
                        PfRule trustId = PfRule::PREPROCESS_LEMMA,
                        MethodId ids = MethodId::SB_DEFAULT);
+  /** Set proof node manager */
+  void setProofNodeManager(ProofNodeManager* pnm);
   /** Gets a reference to the underlying substitution map */
   SubstitutionMap& get();
   /**
@@ -105,8 +107,6 @@ class TrustSubstitutionMap : public ProofGenerator
   context::Context* d_ctx;
   /** The substitution map */
   SubstitutionMap d_subs;
-  /** The proof node manager */
-  ProofNodeManager* d_pnm;
   /** A context-dependent list of trust nodes */
   context::CDList<TrustNode> d_tsubs;
   /** Theory proof step buffer */
@@ -118,7 +118,7 @@ class TrustSubstitutionMap : public ProofGenerator
   /**
    * A context-dependent list of LazyCDProof, allocated for internal steps.
    */
-  CDProofSet<LazyCDProof> d_helperPf;
+  std::unique_ptr<CDProofSet<LazyCDProof>> d_helperPf;
   /** Name for debugging */
   std::string d_name;
   /**