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

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