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.

1 files changed, 0 insertions, 4 deletions

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 */