Simpler

src/smt/assertions.cpp

@@ -126,19 +126,24 @@ void Assertions::addFormula(TNode n,
     {
       Trace("smt-define-fun")
           << "Define fun: " << n[0] << " = " << n[1] << std::endl;
-      bool isLambda = n[1].getKind() == Kind::LAMBDA;
       NodeManager* nm = nodeManager();
       TrustSubstitutionMap& tsm = d_env.getTopLevelSubstitutions();
       // If it is a lambda, we rewrite the body, otherwise we rewrite itself.
       // For lambdas, we prefer rewriting only the body since we don't want
       // higher-order rewrites (e.g. value normalization) to apply by default.
-      TrustNode defRewBody =
-          tsm.applyTrusted(isLambda ? n[1][1] : n[1], d_env.getRewriter());
+      TrustNode defRewBody;
+      // For efficiency, we only do this if it is a lambda.
+      // Note this is important since some benchmarks treat define-fun as a
+      // global let. We should not eagerly rewrite in these cases.
+      if (n[1].getKind() == Kind::LAMBDA)
+      {
+        defRewBody = tsm.applyTrusted(n[1][1], d_env.getRewriter());
+      }
       Node defRew = n[1];
       if (!defRewBody.isNull())
       {
         defRew = defRewBody.getNode();
-        defRew = isLambda ? nm->mkNode(Kind::LAMBDA, n[1][0], defRew) : defRew;
+        defRew = nm->mkNode(Kind::LAMBDA, n[1][0], defRew);
       }
       // if we need to track proofs
       if (d_env.isProofProducing())
@@ -157,26 +162,18 @@ void Assertions::addFormula(TNode n,
           Node eqBody = defRewBody.getProven();
           d_defFunRewPf->addLazyStep(eqBody, defRewBody.getGenerator());
           Node eqRew = n[1].eqNode(defRew);
-          if (isLambda)
-          {
-            // congruence over the binder
-            std::vector<Node> cargs;
-            ProofRule cr = expr::getCongRule(n[1], cargs);
-            d_defFunRewPf->addStep(eqRew, cr, {eqBody}, cargs);
-          }
-          else
-          {
-            Assert(eqRew == eqBody);
-          }
+          Assert (n[1].getKind() == Kind::LAMBDA);
+          // congruence over the binder
+          std::vector<Node> cargs;
+          ProofRule cr = expr::getCongRule(n[1], cargs);
+          d_defFunRewPf->addStep(eqRew, cr, {eqBody}, cargs);
           // Proof is:
           //                            ------ from tsm
           //                            t = t'
           // ------------------ ASSUME  -------------------------- CONG
           // n = lambda x. t            lambda x. t = lambda x. t'
           // ------------------------------------------------------ TRANS
           // n = lambda x. t'
-          // where the CONG step is unecessary if not a lambda (i.e. a defined
-          // constant).
           Node eqFinal = n[0].eqNode(defRew);
           d_defFunRewPf->addStep(eqFinal, ProofRule::TRANS, {n, eqRew}, {});
         }