Trying to break cycles when printing a .dot DAG (#8698)

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 deals with cycles between proof nodes that are in a ancestor/descendant relationship. The new conditions are:

- If any proof node under a first proof node has the hash equal to the first one, this would introduces a cycle. To avoid it, then no sharing between nodes happens in this case.

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 b99dab2c1f519d11e13e496724299b8c622ded5b..a1912238078950c59cbf9bd2d3c8febc65e2c74d 100644 (file)
--- a/src/proof/dot/dot_printer.cpp
+++ b/src/proof/dot/dot_printer.cpp
@@ -197,12 +197,14 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn)
   std::map<size_t, uint64_t> proofLet;
   std::map<size_t, uint64_t> firstScopeLet;
   std::unordered_map<const ProofNode*, bool> cfaMap;
+  std::vector<size_t> ancestorHashs;
 
   DotPrinter::printInternal(out,
                             pn,
                             proofLet,
                             firstScopeLet,
                             cfaMap,
+                            ancestorHashs,
                             ProofNodeClusterType::NOT_DEFINED);
 
   if (options::printDotClusters())
@@ -222,6 +224,7 @@ uint64_t DotPrinter::printInternal(
     std::map<size_t, uint64_t>& pfLetClosed,
     std::map<size_t, uint64_t>& pfLetOpen,
     std::unordered_map<const ProofNode*, bool>& cfaMap,
+    std::vector<size_t>& ancestorHashs,
     ProofNodeClusterType parentType)
 {
   uint64_t currentRuleID = d_ruleID;
@@ -231,27 +234,44 @@ uint64_t DotPrinter::printInternal(
   {
     ProofNodeHashFunction hasher;
     size_t currentHash = hasher(pn);
-    auto openProofIt = pfLetOpen.find(currentHash);
 
-    if (openProofIt != pfLetOpen.end())
-    {
-      return openProofIt->second;
-    }
+    std::vector<size_t>::iterator oldEnd = ancestorHashs.end();
+    // Search if the current hash is in the vector
+    std::vector<size_t>::iterator it =
+        std::find(ancestorHashs.begin(), ancestorHashs.end(), currentHash);
 
-    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))
+    // Register the current proof node hash in the ancestor vector
+    ancestorHashs.push_back(currentHash);
+
+    // we only consider sharing when this would not introduce a cycle, which
+    // would be the case if this hash is occurring under a proof node with the
+    // same hash (this can happen since our hash computation only takes into
+    // account the immediate descendants of a proof node, the limit of hash
+    // representation notwithstanding)
+    if (it == oldEnd)
     {
-      pfLetClosed[currentHash] = currentRuleID;
+      auto openProofIt = pfLetOpen.find(currentHash);
+
+      if (openProofIt != pfLetOpen.end())
+      {
+        return openProofIt->second;
+      }
+
+      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;
     }
-    pfLetOpen[currentHash] = currentRuleID;
   }
 
   ProofNodeClusterType proofNodeType = ProofNodeClusterType::NOT_DEFINED;
@@ -282,17 +302,31 @@ uint64_t DotPrinter::printInternal(
                                      pfLetClosed,
                                      thisScopeLet,
                                      cfaMap,
+                                     ancestorHashs,
                                      proofNodeType);
     out << "\t" << childId << " -> " << currentRuleID << ";\n";
+    if (options::proofDotDAG())
+    {
+      ancestorHashs.pop_back();
+    }
   }
   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);
+      uint64_t childId = printInternal(out,
+                                       c.get(),
+                                       pfLetClosed,
+                                       pfLetOpen,
+                                       cfaMap,
+                                       ancestorHashs,
+                                       proofNodeType);
       out << "\t" << childId << " -> " << currentRuleID << ";\n";
+      if (options::proofDotDAG())
+      {
+        ancestorHashs.pop_back();
+      }
     }
   }
 

diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h
index 7b4b2648595405664fa287769351f05b44df7b36..ac9606c90b2e62a1c53be5c1ce9b2e4281bca6a6 100644 (file)
--- a/src/proof/dot/dot_printer.h
+++ b/src/proof/dot/dot_printer.h
@@ -95,6 +95,8 @@ class DotPrinter
    * @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 ancestorHashs a vector containing the hashs of all the proof nodes
+   * ancestors traversed to get to pn
    * @param parentType the type of the parent node
    * @return the id of the proof node printed
    */
@@ -103,6 +105,7 @@ class DotPrinter
                          std::map<size_t, uint64_t>& pfLetClosed,
                          std::map<size_t, uint64_t>& pfLetOpen,
                          std::unordered_map<const ProofNode*, bool>& cfaMap,
+                         std::vector<size_t>& ancestorHashs,
                          ProofNodeClusterType parentType);
 
   /**