Move expand definitions to its own file (#5528)

We are changing our policy on how expand definitions is handled during preprocessing.

This will require some additions to expand definitions handling. This PR makes a standalone module for expanding definitions.

1 files changed, 4 insertions, 13 deletions

diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index d260edf14..072603e7d 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -26,6 +26,7 @@
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "smt/assertions.h"
+#include "smt/expand_definitions.h"
 #include "smt/smt_engine_stats.h"
 #include "util/resource_manager.h"
 
@@ -53,11 +54,11 @@ class ProcessAssertions
 {
   /** The types for the recursive function definitions */
   typedef context::CDList<Node> NodeList;
-  typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
   typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
 
  public:
   ProcessAssertions(SmtEngine& smt,
+                    ExpandDefs& exDefs,
                     ResourceManager& rm,
                     SmtEngineStatistics& stats);
   ~ProcessAssertions();
@@ -76,22 +77,12 @@ class ProcessAssertions
    * processing the assertions.
    */
   bool apply(Assertions& as);
-  /**
-   * Expand definitions in term n. Return the expanded form of n.
-   *
-   * @param n The node to expand
-   * @param cache Cache of previous results
-   * @param expandOnly if true, then the expandDefinitions function of
-   * TheoryEngine is not called on subterms of n.
-   * @return The expanded term.
-   */
-  Node expandDefinitions(TNode n,
-                         NodeToNodeHashMap& cache,
-                         bool expandOnly = false);
 
  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 */