[proofs] Make cache (optionally) persistent in lazy CD proof (#8104)

Should address severe performance issues in some use cases of proofs.

diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp
index f6c9d8eb2f0b57e9b2265d5d9e7c4827cb417cc1..5b218c885fd3cd16818d307547440aa423a4ef30 100644 (file)
--- a/src/proof/lazy_proof.cpp
+++ b/src/proof/lazy_proof.cpp
@@ -27,10 +27,13 @@ LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
                          ProofGenerator* dpg,
                          context::Context* c,
                          const std::string& name,
-                         bool autoSym)
+                         bool autoSym,
+                         bool doCache)
     : CDProof(pnm, c, name, autoSym),
       d_gens(c ? c : &d_context),
-      d_defaultGen(dpg)
+      d_defaultGen(dpg),
+      d_doCache(doCache),
+      d_allVisited(c ? c : &d_context)
 {
 }
 
@@ -52,19 +55,33 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
   // otherwise, we traverse the proof opf and fill in the ASSUME leafs that
   // have generators
   std::unordered_set<ProofNode*> visited;
-  std::unordered_set<ProofNode*>::iterator it;
   std::vector<ProofNode*> visit;
   ProofNode* cur;
   visit.push_back(opf.get());
+  bool alreadyVisited;
   do
   {
     cur = visit.back();
     visit.pop_back();
-    it = visited.find(cur);
+    if (d_doCache)
+    {
+      alreadyVisited = d_allVisited.find(cur) != d_allVisited.end();
+    }
+    else
+    {
+      alreadyVisited = visited.find(cur) != visited.end();
+    }
 
-    if (it == visited.end())
+    if (!alreadyVisited)
     {
-      visited.insert(cur);
+      if (d_doCache)
+      {
+        d_allVisited.insert(cur);
+      }
+      else
+      {
+        visited.insert(cur);
+      }
       Node cfact = cur->getResult();
       if (getProof(cfact).get() != cur)
       {

diff --git a/src/proof/lazy_proof.h b/src/proof/lazy_proof.h
index e14dc8a1c0d52ea8e186b91d28d3b2ee59558efa..60170aa11ef6520dc7c42b7c6acf0b728bbf40c6 100644 (file)
--- a/src/proof/lazy_proof.h
+++ b/src/proof/lazy_proof.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__PROOF__LAZY_PROOF_H
 #define CVC5__PROOF__LAZY_PROOF_H
 
+#include "context/cdhashset.h"
 #include "proof/proof.h"
 
 namespace cvc5 {
@@ -44,12 +45,18 @@ class LazyCDProof : public CDProof
    * @param name The name of this proof generator (for debugging)
    * @param autoSym Whether symmetry steps are automatically added when adding
    * steps to this proof
+   * @param doCache Whether the proofs we process in getProofFor are cached
+   * based on the context of this class. In other words, we assume that the
+   * subproofs returned by getProofFor are not re-processed on repeated calls
+   * to getProofFor, even if new steps are provided to this class in the
+   * meantime.
    */
   LazyCDProof(ProofNodeManager* pnm,
               ProofGenerator* dpg = nullptr,
               context::Context* c = nullptr,
               const std::string& name = "LazyCDProof",
-              bool autoSym = true);
+              bool autoSym = true,
+              bool doCache = true);
   ~LazyCDProof();
   /**
    * Get lazy proof for fact, or nullptr if it does not exist. This may
@@ -97,6 +104,7 @@ class LazyCDProof : public CDProof
 
  protected:
   typedef context::CDHashMap<Node, ProofGenerator*> NodeProofGeneratorMap;
+  typedef context::CDHashSet<ProofNode*> ProofNodeSet;
   /** Maps facts that can be proven to generators */
   NodeProofGeneratorMap d_gens;
   /** The default proof generator */
@@ -107,6 +115,10 @@ class LazyCDProof : public CDProof
    * proof generator for the symmetric form of fact was provided.
    */
   ProofGenerator* getGeneratorFor(Node fact, bool& isSym);
+  /** whether d_allVisited is maintained */
+  bool d_doCache;
+  /** The set of proof nodes we have processed in getProofFor */
+  ProofNodeSet d_allVisited;
 };
 
 }  // namespace cvc5