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, 4 insertions, 7 deletions

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;