Eagerly rewrite bodies of define-fun

ajreynol · Jan 15, 2025 · 2665e3d · 2665e3d
1 parent 8bfe8c9
commit 2665e3d
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 4 deletions.
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
@@ -26,6 +26,8 @@
 #include "smt/env.h"
 #include "theory/trust_substitutions.h"
 #include "util/result.h"
+#include "proof/lazy_proof.h"
+#include "proof/proof_node_algorithm.h"
 
 using namespace cvc5::internal::theory;
 using namespace cvc5::internal::kind;
@@ -120,12 +122,37 @@ void Assertions::addFormula(TNode n,
   if (isFunDef)
   {
     // if a non-recursive define-fun, just add as a top-level substitution
-    if (n.getKind() == Kind::EQUAL && n[0].isVar())
+    if (n.getKind() == Kind::EQUAL && n[0].isVar() && n[1].getKind()==Kind::LAMBDA)
     {
-      // 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;
+      NodeManager * nm = nodeManager();
+      TrustSubstitutionMap& tsm = d_env.getTopLevelSubstitutions();
+      TrustNode defRewBody = tsm.applyTrusted(n[1][1], d_env.getRewriter());
+      Node defRew = defRewBody.isNull() ? Node(n[1]) : nm->mkNode(Kind::LAMBDA, n[1][0], defRewBody.getNode());
+      if (d_env.isProofProducing())
+      {
+        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);
+          std::vector<Node> cargs;
+          ProofRule cr = expr::getCongRule(n[1], cargs);
+          d_defFunRewPf->addStep(eqRew, cr, {eqBody}, cargs);
+          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