Eagerly rewriting bodies of define-fun

ajreynol · Jan 15, 2025 · cfc1626 · cfc1626
1 parent 8dca52e
commit cfc1626
Show file tree

Hide file tree

Showing 2 changed files with 63 additions and 3 deletions.
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
@@ -23,6 +23,8 @@
 #include "options/expr_options.h"
 #include "options/language.h"
 #include "options/smt_options.h"
+#include "proof/lazy_proof.h"
+#include "proof/proof_node_algorithm.h"
 #include "smt/env.h"
 #include "theory/trust_substitutions.h"
 #include "util/result.h"
@@ -122,10 +124,63 @@ void Assertions::addFormula(TNode n,
     // if a non-recursive define-fun, just add as a top-level substitution
     if (n.getKind() == Kind::EQUAL && n[0].isVar())
     {
-      // A define-fun is an assumption in the overall proof, thus
-      // we justify the substitution with ASSUME here.
+      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());
+      Node defRew = n[1];
+      if (!defRewBody.isNull())
+      {
+        defRew = defRewBody.getNode();
+        defRew = isLambda ? nm->mkNode(Kind::LAMBDA, n[1][0], defRew) : defRew;
+      }
+      // if we need to track proofs
+      if (d_env.isProofProducing())
+      {
+        // initialize the proof generator if not already done so
+        if (d_defFunRewPf==nullptr)
+        {
+          d_defFunRewPf = std::make_shared<LazyCDProof>(d_env);
+        }
+        if (defRew != n[1])
+        {
+          // A define-fun is an assumption in the overall proof, thus
+          // we justify the substitution with ASSUME here.
+          d_defFunRewPf->addStep(n, ProofRule::ASSUME, {}, {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);
+          }
+          // 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}, {});
+        }
+      }
+      Trace("smt-define-fun") << "...rewritten to " << defRew << std::endl;
       d_env.getTopLevelSubstitutions().addSubstitution(
-          n[0], n[1], ProofRule::ASSUME, {}, {n});
+          n[0], defRew, d_defFunRewPf.get());
       return;
     }
   }

diff --git a/src/smt/assertions.h b/src/smt/assertions.h
@@ -26,6 +26,9 @@
 #include "smt/env_obj.h"
 
 namespace cvc5::internal {
+
+class LazyCDProof;
+
 namespace smt {
 
 class AbstractValues;
@@ -141,6 +144,8 @@ class Assertions : protected EnvObj
    * The list of assumptions from the previous call to checkSatisfiability.
    */
   std::vector<Node> d_assumptions;
+  /** Proof generator storing proofs of rewriting for defined functions */
+  std::shared_ptr<LazyCDProof> d_defFunRewPf;
 };
 
 }  // namespace smt