(proof-new) Proofs for expand definitions (#5562)

3 files changed, 126 insertions, 18 deletions

diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index 20c4f8ef6..b0460fcc5 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -32,7 +32,7 @@ namespace smt {
 ExpandDefs::ExpandDefs(SmtEngine& smt,
                        ResourceManager& rm,
                        SmtEngineStatistics& stats)
-    : d_smt(smt), d_resourceManager(rm), d_smtStats(stats)
+    : d_smt(smt), d_resourceManager(rm), d_smtStats(stats), d_tpg(nullptr)
 {
 }
 
@@ -43,6 +43,17 @@ Node ExpandDefs::expandDefinitions(
     std::unordered_map<Node, Node, NodeHashFunction>& cache,
     bool expandOnly)
 {
+  TrustNode trn = expandDefinitions(n, cache, expandOnly, nullptr);
+  return trn.isNull() ? Node(n) : trn.getNode();
+}
+
+TrustNode ExpandDefs::expandDefinitions(
+    TNode n,
+    std::unordered_map<Node, Node, NodeHashFunction>& cache,
+    bool expandOnly,
+    TConvProofGenerator* tpg)
+{
+  const TNode orig = n;
   NodeManager* nm = d_smt.getNodeManager();
   std::stack<std::tuple<Node, Node, bool>> worklist;
   std::stack<Node> result;
@@ -75,17 +86,24 @@ Node ExpandDefs::expandDefinitions(
         if (i != dfuns->end())
         {
           Node f = (*i).second.getFormula();
-          // must expand its definition
-          Node fe = expandDefinitions(f, cache, expandOnly);
+          const std::vector<Node>& formals = (*i).second.getFormals();
           // replacement must be closed
-          if ((*i).second.getFormals().size() > 0)
+          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)
           {
-            result.push(
-                nm->mkNode(LAMBDA,
-                           nm->mkNode(BOUND_VAR_LIST, (*i).second.getFormals()),
-                           fe));
-            continue;
+            // 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});
           }
+          // 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;
@@ -126,6 +144,9 @@ Node ExpandDefs::expandDefinitions(
           doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr());
         }
       }
+      // 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;
@@ -180,6 +201,18 @@ Node ExpandDefs::expandDefinitions(
           }
 
           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(),
@@ -187,9 +220,29 @@ Node ExpandDefs::expandDefinitions(
                                       n.begin(),
                                       n.begin() + formals.size());
         Debug("expand") << "made : " << instance << std::endl;
-
-        Node expanded = expandDefinitions(instance, cache, expandOnly);
-        cache[n] = (n == expanded ? Node::null() : expanded);
+        // 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});
+          }
+        }
+        // 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;
       }
@@ -201,7 +254,19 @@ Node ExpandDefs::expandDefinitions(
 
         Assert(t != NULL);
         TrustNode trn = t->expandDefinition(n);
-        node = trn.isNull() ? Node(n) : trn.getNode();
+        if (!trn.isNull())
+        {
+          node = trn.getNode();
+          if (tpg != nullptr)
+          {
+            tpg->addRewriteStep(
+                n, node, trn.getGenerator(), PfRule::THEORY_EXPAND_DEF);
+          }
+        }
+        else
+        {
+          node = n;
+        }
       }
 
       // the partial functions can fall through, in which case we still
@@ -252,27 +317,51 @@ Node ExpandDefs::expandDefinitions(
 
   AlwaysAssert(result.size() == 1);
 
-  return result.top();
+  Node res = result.top();
+
+  if (res == orig)
+  {
+    return TrustNode::null();
+  }
+  return TrustNode::mkTrustRewrite(orig, res, tpg);
 }
 
 void ExpandDefs::expandAssertions(AssertionPipeline& assertions,
                                   bool expandOnly)
 {
   Chat() << "expanding definitions in assertions..." << std::endl;
-  Trace("simplify") << "ExpandDefs::simplify(): expanding definitions"
+  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];
-    Node expd = expandDefinitions(assert, cache, expandOnly);
-    if (expd != assert)
+    // 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())
     {
-      assertions.replace(i, expd);
+      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(),
+                                        TConvPolicy::FIXPOINT,
+                                        TConvCachePolicy::NEVER,
+                                        "ExpandDefs::TConvProofGenerator",
+                                        nullptr,
+                                        true));
+  }
+}
+
 }  // namespace smt
 }  // namespace CVC4
diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index f40ee4a4e..5b75ddadd 100644
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -20,6 +20,7 @@
 #include <unordered_map>
 
 #include "expr/node.h"
+#include "expr/term_conversion_proof_generator.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "smt/smt_engine_stats.h"
 #include "util/resource_manager.h"
@@ -61,13 +62,30 @@ class ExpandDefs
   void expandAssertions(preprocessing::AssertionPipeline& assertions,
                         bool expandOnly = false);
 
+  /**
+   * Set proof node manager, which signals this class to enable proofs using the
+   * given proof node manager.
+   */
+  void setProofNodeManager(ProofNodeManager* pnm);
+
  private:
+  /**
+   * Helper function for above, called to specify if we want proof production
+   * based on the optional argument tpg.
+   */
+  theory::TrustNode expandDefinitions(
+      TNode n,
+      std::unordered_map<Node, Node, NodeHashFunction>& cache,
+      bool expandOnly,
+      TConvProofGenerator* tpg);
   /** Reference to the SMT engine */
   SmtEngine& d_smt;
   /** Reference to resource manager */
   ResourceManager& d_resourceManager;
   /** Reference to the SMT stats */
   SmtEngineStatistics& d_smtStats;
+  /** A proof generator for the term conversion. */
+  std::unique_ptr<TConvProofGenerator> d_tpg;
 };
 
 }  // namespace smt
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 2c8592657..9f2c8f3e7 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -159,6 +159,7 @@ void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg)
 {
   Assert(pppg != nullptr);
   d_pnm = pppg->getManager();
+  d_exDefs.setProofNodeManager(d_pnm);
   d_propagator.setProof(d_pnm, d_context, pppg);
   d_rtf.setProofNodeManager(d_pnm);
 }