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, 6 insertions, 186 deletions

diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index d331e8e78..14182a46d 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -20,7 +20,7 @@
 
 #include "expr/node_manager_attributes.h"
 #include "preprocessing/assertion_pipeline.h"
-#include "smt/defined_function.h"
+#include "smt/env.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_stats.h"
 #include "theory/theory_engine.h"
@@ -32,10 +32,8 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace smt {
 
-ExpandDefs::ExpandDefs(SmtEngine& smt,
-                       ResourceManager& rm,
-                       SmtEngineStatistics& stats)
-    : d_smt(smt), d_resourceManager(rm), d_smtStats(stats), d_tpg(nullptr)
+ExpandDefs::ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats)
+    : d_smt(smt), d_env(env), d_smtStats(stats), d_tpg(nullptr)
 {
 }
 
@@ -57,7 +55,6 @@ TrustNode ExpandDefs::expandDefinitions(
     TConvProofGenerator* tpg)
 {
   const TNode orig = n;
-  NodeManager* nm = d_smt.getNodeManager();
   std::stack<std::tuple<Node, Node, bool>> worklist;
   std::stack<Node> result;
   worklist.push(std::make_tuple(Node(n), Node(n), false));
@@ -67,7 +64,7 @@ TrustNode ExpandDefs::expandDefinitions(
 
   do
   {
-    d_resourceManager.spendResource(Resource::PreprocessStep);
+    d_env.getResourceManager()->spendResource(Resource::PreprocessStep);
 
     // n is the input / original
     // node is the output / result
@@ -79,38 +76,9 @@ TrustNode ExpandDefs::expandDefinitions(
     // Working downwards
     if (!childrenPushed)
     {
-      Kind k = n.getKind();
-
       // we can short circuit (variable) leaves
       if (n.isVar())
       {
-        SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
-        SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(n);
-        if (i != dfuns->end())
-        {
-          Node f = (*i).second.getFormula();
-          const std::vector<Node>& formals = (*i).second.getFormals();
-          // replacement must be closed
-          if (!formals.empty())
-          {
-            f = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, formals), f);
-          }
-          // are we are producing proofs for this call?
-          if (tpg != nullptr)
-          {
-            // if this is a variable, we can simply assume it
-            // ------- ASSUME
-            // n = f
-            Node conc = n.eqNode(f);
-            tpg->addRewriteStep(n, f, PfRule::ASSUME, {}, {conc}, true);
-          }
-          // must recursively expand its definition
-          TrustNode tfe = expandDefinitions(f, cache, expandOnly, tpg);
-          Node fe = tfe.isNull() ? f : tfe.getNode();
-          // don't bother putting in the cache
-          result.push(fe);
-          continue;
-        }
         // don't bother putting in the cache
         result.push(n);
         continue;
@@ -125,132 +93,7 @@ TrustNode ExpandDefs::expandDefinitions(
         result.push(ret.isNull() ? n : ret);
         continue;
       }
-
-      // otherwise expand it
-      bool doExpand = false;
-      if (k == APPLY_UF)
-      {
-        // Always do beta-reduction here. The reason is that there may be
-        // operators such as INTS_MODULUS in the body of the lambda that would
-        // otherwise be introduced by beta-reduction via the rewriter, but are
-        // not expanded here since the traversal in this function does not
-        // traverse the operators of nodes. Hence, we beta-reduce here to
-        // ensure terms in the body of the lambda are expanded during this
-        // call.
-        if (n.getOperator().getKind() == LAMBDA)
-        {
-          doExpand = true;
-        }
-        else
-        {
-          // We always check if this operator corresponds to a defined function.
-          doExpand = d_smt.isDefinedFunction(n.getOperator());
-        }
-      }
-      // the premise of the proof of expansion (if we are expanding a definition
-      // and proofs are enabled)
-      std::vector<Node> pfExpChildren;
-      if (doExpand)
-      {
-        std::vector<Node> formals;
-        TNode fm;
-        if (n.getOperator().getKind() == LAMBDA)
-        {
-          TNode op = n.getOperator();
-          // lambda
-          for (unsigned i = 0; i < op[0].getNumChildren(); i++)
-          {
-            formals.push_back(op[0][i]);
-          }
-          fm = op[1];
-        }
-        else
-        {
-          // application of a user-defined symbol
-          TNode func = n.getOperator();
-          SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
-          SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func);
-          if (i == dfuns->end())
-          {
-            throw TypeCheckingExceptionPrivate(
-                n,
-                std::string("Undefined function: `") + func.toString() + "'");
-          }
-          DefinedFunction def = (*i).second;
-          formals = def.getFormals();
-
-          if (Debug.isOn("expand"))
-          {
-            Debug("expand") << "found: " << n << std::endl;
-            Debug("expand") << " func: " << func << std::endl;
-            std::string name = func.getAttribute(expr::VarNameAttr());
-            Debug("expand") << "     : \"" << name << "\"" << std::endl;
-          }
-          if (Debug.isOn("expand"))
-          {
-            Debug("expand") << " defn: " << def.getFunction() << std::endl
-                            << "       [";
-            if (formals.size() > 0)
-            {
-              copy(formals.begin(),
-                   formals.end() - 1,
-                   std::ostream_iterator<Node>(Debug("expand"), ", "));
-              Debug("expand") << formals.back();
-            }
-            Debug("expand")
-                << "]" << std::endl
-                << "       " << def.getFunction().getType() << std::endl
-                << "       " << def.getFormula() << std::endl;
-          }
-
-          fm = def.getFormula();
-          // are we producing proofs for this call?
-          if (tpg != nullptr)
-          {
-            Node pfRhs = fm;
-            if (!formals.empty())
-            {
-              Node bvl = nm->mkNode(BOUND_VAR_LIST, formals);
-              pfRhs = nm->mkNode(LAMBDA, bvl, pfRhs);
-            }
-            Assert(func.getType().isComparableTo(pfRhs.getType()));
-            pfExpChildren.push_back(func.eqNode(pfRhs));
-          }
-        }
-
-        Node instance = fm.substitute(formals.begin(),
-                                      formals.end(),
-                                      n.begin(),
-                                      n.begin() + formals.size());
-        Debug("expand") << "made : " << instance << std::endl;
-        // are we producing proofs for this call?
-        if (tpg != nullptr)
-        {
-          if (n != instance)
-          {
-            // This code is run both when we are doing expand definitions and
-            // simple beta reduction.
-            //
-            // f = (lambda ((x T)) t)  [if we are expanding a definition]
-            // ---------------------- MACRO_SR_PRED_INTRO
-            // n = instance
-            Node conc = n.eqNode(instance);
-            tpg->addRewriteStep(n,
-                                instance,
-                                PfRule::MACRO_SR_PRED_INTRO,
-                                pfExpChildren,
-                                {conc},
-                                true);
-          }
-        }
-        // now, call expand definitions again on the result
-        TrustNode texp = expandDefinitions(instance, cache, expandOnly, tpg);
-        Node expanded = texp.isNull() ? instance : texp.getNode();
-        cache[n] = n == expanded ? Node::null() : expanded;
-        result.push(expanded);
-        continue;
-      }
-      else if (!expandOnly)
+      if (!expandOnly)
       {
         // do not do any theory stuff if expandOnly is true
 
@@ -331,35 +174,12 @@ TrustNode ExpandDefs::expandDefinitions(
   return TrustNode::mkTrustRewrite(orig, res, tpg);
 }
 
-void ExpandDefs::expandAssertions(AssertionPipeline& assertions,
-                                  bool expandOnly)
-{
-  Chat() << "expanding definitions in assertions..." << std::endl;
-  Trace("exp-defs") << "ExpandDefs::simplify(): expanding definitions"
-                    << std::endl;
-  TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime);
-  std::unordered_map<Node, Node, NodeHashFunction> cache;
-  for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i)
-  {
-    Node assert = assertions[i];
-    // notice we call this method with only one value of expandOnly currently,
-    // hence we maintain only a single set of proof steps in d_tpg.
-    TrustNode expd = expandDefinitions(assert, cache, expandOnly, d_tpg.get());
-    if (!expd.isNull())
-    {
-      Trace("exp-defs") << "ExpandDefs::expandAssertions: " << assert << " -> "
-                        << expd.getNode() << std::endl;
-      assertions.replaceTrusted(i, expd);
-    }
-  }
-}
-
 void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm)
 {
   if (d_tpg == nullptr)
   {
     d_tpg.reset(new TConvProofGenerator(pnm,
-                                        d_smt.getUserContext(),
+                                        d_env.getUserContext(),
                                         TConvPolicy::FIXPOINT,
                                         TConvCachePolicy::NEVER,
                                         "ExpandDefs::TConvProofGenerator",