[proofs] [dot] New way to traverse the proof when printing a .dot DAG (#8610)

Change the way cvc5 traverse and print the proof when --proof-dot-dag option is used. The main change is related to the way the printer tracks visited proof nodes. The new conditions are:

- If the proof node has already been visited inside the current scope.
- If the proof node is closed (i.e. does not contains a subproof whose rule is ASSUME) and has already been visited (here the condition is global and the scope doesn't matter).

Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com

diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp
index 518c1009f1b064c0086ad418714a55136625be59..8d648140ed826f0db359df3076b8762141a63c50 100644 (file)
--- a/src/proof/dot/dot_printer.cpp
+++ b/src/proof/dot/dot_printer.cpp
@@ -23,6 +23,7 @@
 #include "options/proof_options.h"
 #include "printer/smt2/smt2_printer.h"
 #include "proof/proof_checker.h"
+#include "proof/proof_node_algorithm.h"
 #include "proof/proof_node_manager.h"
 #include "theory/builtin/proof_checker.h"
 
@@ -194,8 +195,15 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn)
   }
 
   std::map<size_t, uint64_t> proofLet;
-  DotPrinter::printInternal(
-      out, pn, proofLet, ProofNodeClusterType::NOT_DEFINED);
+  std::map<size_t, uint64_t> firstScopeLet;
+  std::unordered_map<const ProofNode*, bool> cfaMap;
+
+  DotPrinter::printInternal(out,
+                            pn,
+                            proofLet,
+                            firstScopeLet,
+                            cfaMap,
+                            ProofNodeClusterType::NOT_DEFINED);
 
   if (options::printDotClusters())
   {
@@ -208,10 +216,13 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn)
   out << "\n}\n";
 }
 
-uint64_t DotPrinter::printInternal(std::ostream& out,
-                                   const ProofNode* pn,
-                                   std::map<size_t, uint64_t>& pfLet,
-                                   ProofNodeClusterType parentType)
+uint64_t DotPrinter::printInternal(
+    std::ostream& out,
+    const ProofNode* pn,
+    std::map<size_t, uint64_t>& pfLetClosed,
+    std::map<size_t, uint64_t>& pfLetOpen,
+    std::unordered_map<const ProofNode*, bool>& cfaMap,
+    ProofNodeClusterType parentType)
 {
   uint64_t currentRuleID = d_ruleID;
 
@@ -220,15 +231,27 @@ uint64_t DotPrinter::printInternal(std::ostream& out,
   {
     ProofNodeHashFunction hasher;
     size_t currentHash = hasher(pn);
-    auto proofIt = pfLet.find(currentHash);
+    auto openProofIt = pfLetOpen.find(currentHash);
 
-    // If this node has been already counted
-    if (proofIt != pfLet.end())
+    if (openProofIt != pfLetOpen.end())
     {
-      return proofIt->second;
+      return openProofIt->second;
     }
 
-    pfLet[currentHash] = currentRuleID;
+    auto proofIt = pfLetClosed.find(currentHash);
+    // If this node has been already saved to the global cache of closed proof
+    // nodes
+    if (proofIt != pfLetClosed.end())
+    {
+      Assert(!expr::containsAssumption(pn, cfaMap));
+      return proofIt->second;
+    }
+    // If this proof node is closed, we add it to the global cache
+    if (!expr::containsAssumption(pn, cfaMap))
+    {
+      pfLetClosed[currentHash] = currentRuleID;
+    }
+    pfLetOpen[currentHash] = currentRuleID;
   }
 
   ProofNodeClusterType proofNodeType = ProofNodeClusterType::NOT_DEFINED;
@@ -249,12 +272,29 @@ uint64_t DotPrinter::printInternal(std::ostream& out,
 
   PfRule r = pn->getRule();
 
-  const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
-  for (const std::shared_ptr<ProofNode>& c : children)
+  // Scopes trigger a traversal with a new local cache for proof nodes
+  if (isSCOPE(r) && currentRuleID)
   {
-    uint64_t childId = printInternal(out, c.get(), pfLet, proofNodeType);
+    // create a new pfLet
+    std::map<size_t, uint64_t> thisScopeLet;
+    uint64_t childId = printInternal(out,
+                                     pn->getChildren()[0].get(),
+                                     pfLetClosed,
+                                     thisScopeLet,
+                                     cfaMap,
+                                     proofNodeType);
     out << "\t" << childId << " -> " << currentRuleID << ";\n";
   }
+  else
+  {
+    const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
+    for (const std::shared_ptr<ProofNode>& c : children)
+    {
+      uint64_t childId = printInternal(
+          out, c.get(), pfLetClosed, pfLetOpen, cfaMap, proofNodeType);
+      out << "\t" << childId << " -> " << currentRuleID << ";\n";
+    }
+  }
 
   // If it's a scope, then remove from the stack
   if (isSCOPE(r) && options::printDotClusters())

diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h
index f5fe8d25eb867b289e3697d89e366ba611c47532..70d89e17eeda8f1ef5a09baf0d4633b9e888f6cd 100644 (file)
--- a/src/proof/dot/dot_printer.h
+++ b/src/proof/dot/dot_printer.h
@@ -90,14 +90,19 @@ class DotPrinter
    * the child as argument.
    * @param out the output stream
    * @param pn the proof node to print
-   * @param pfLet the map of the hashs of proof nodes already printed to their
-   * ids
+   * @param pfLetClosed the map from proof node hashs, of closed proof nodes, to
+   * their printed ids
+   * @param pfLetOpen the map, local to the current scope, of proof node hashs
+   * to their printed ids
+   * @param cfaMap the map from proof nodes to whether they contain assumptions
    * @param parentType the type of the parent node
    * @return the id of the proof node printed
    */
   uint64_t printInternal(std::ostream& out,
                          const ProofNode* pn,
-                         std::map<size_t, uint64_t>& pfLet,
+                         std::map<size_t, uint64_t>& pfLetClosed,
+                         std::map<size_t, uint64_t>& pfLetOpen,
+                         std::unordered_map<const ProofNode*, bool>& cfaMap,
                          ProofNodeClusterType parentType);
 
   /**