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, 61 deletions

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