[proofs] [dot] Enable DAG and tree printing with dot files (#8107)

Add a proof option that allows DAG and tree print format when using dot files.

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

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index c63f9953490a0572893648d3955d2e7306d639e8..346a0dc4e159a316503f665d578fe67720fe1be4 100644 (file)
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -114,3 +114,11 @@ name   = "Proof"
   type       = "bool"
   default    = "false"
   help       = "Add pivots to Alethe resolution steps"
+
+[[option]]
+  name       = "proofDotDAG"
+  category   = "regular"
+  long       = "proof-dot-dag"
+  type       = "bool"
+  default    = "false"
+  help       = "Indicates if the dot proof will be printed as a DAG or as a tree"

diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp
index 0e8d1a057604493f32e2d2a4413f229bd8be0303..c5f97711dc6fbd2ca109c6e7ea44d7a6fcdcb313 100644 (file)
--- a/src/proof/dot/dot_printer.cpp
+++ b/src/proof/dot/dot_printer.cpp
@@ -18,6 +18,7 @@
 #include <sstream>
 
 #include "options/expr_options.h"
+#include "options/proof_options.h"
 #include "printer/smt2/smt2_printer.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_node_manager.h"
@@ -27,7 +28,9 @@ namespace cvc5 {
 namespace proof {
 
 DotPrinter::DotPrinter()
-    : d_lbind(options::defaultDagThresh() ? options::defaultDagThresh() + 1 : 0)
+    : d_lbind(options::defaultDagThresh() ? options::defaultDagThresh() + 1
+                                          : 0),
+      d_ruleID(0)
 {
 }
 
@@ -141,7 +144,6 @@ void DotPrinter::letifyResults(const ProofNode* pn)
 
 void DotPrinter::print(std::ostream& out, const ProofNode* pn)
 {
-  uint64_t ruleID = 0;
   countSubproofs(pn);
   letifyResults(pn);
 
@@ -178,18 +180,37 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn)
     }
     out << "}}\";\n";
   }
-  DotPrinter::printInternal(out, pn, ruleID, 0, false);
+
+  std::map<size_t, uint64_t> proofLet;
+  DotPrinter::printInternal(out, pn, proofLet, 0, false);
   out << "}\n";
 }
 
-void DotPrinter::printInternal(std::ostream& out,
-                               const ProofNode* pn,
-                               uint64_t& ruleID,
-                               uint64_t scopeCounter,
-                               bool inPropositionalView)
+uint64_t DotPrinter::printInternal(std::ostream& out,
+                                   const ProofNode* pn,
+                                   std::map<size_t, uint64_t>& pfLet,
+                                   uint64_t scopeCounter,
+                                   bool inPropositionalView)
 {
-  uint64_t currentRuleID = ruleID;
-  const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
+  uint64_t currentRuleID = d_ruleID;
+
+  // Print DAG option enabled
+  if (options::proofDotDAG())
+  {
+    ProofNodeHashFunction hasher;
+    size_t currentHash = hasher(pn);
+    auto proofIt = pfLet.find(currentHash);
+
+    // If this node has been already counted
+    if (proofIt != pfLet.end())
+    {
+      return proofIt->second;
+    }
+
+    pfLet[currentHash] = currentRuleID;
+  }
+  d_ruleID++;
+
   std::ostringstream currentArguments, resultStr, classes, colors;
 
   out << "\t" << currentRuleID << " [ label = \"{";
@@ -250,12 +271,15 @@ void DotPrinter::printInternal(std::ostream& out,
   out << ", comment = \"{\\\"subProofQty\\\":" << it->second << "}\"";
   out << " ];\n";
 
+  const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
   for (const std::shared_ptr<ProofNode>& c : children)
   {
-    ++ruleID;
-    out << "\t" << ruleID << " -> " << currentRuleID << ";\n";
-    printInternal(out, c.get(), ruleID, scopeCounter, inPropositionalView);
+    uint64_t childId =
+        printInternal(out, c.get(), pfLet, scopeCounter, inPropositionalView);
+    out << "\t" << childId << " -> " << currentRuleID << ";\n";
   }
+
+  return currentRuleID;
 }
 
 void DotPrinter::ruleArguments(std::ostringstream& currentArguments,

diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h
index 9cc03a2584586c15e684e2f814fd74e35a774727..c3ec82e2ddb1a71b3ae2680be398541df9deb55d 100644 (file)
--- a/src/proof/dot/dot_printer.h
+++ b/src/proof/dot/dot_printer.h
@@ -48,17 +48,18 @@ class DotPrinter
    * the child as argument.
    * @param out the output stream
    * @param pn the proof node to print
-   * @param ruleID the id of the rule to print
+   * @param pfLet the map of the hashs of proof nodes already printed to their ids
    * @param scopeCounter counter of how many SCOPE were already depth-first
    * traversed in the proof up to this point
    * @param inPropositionalView flag used to mark the proof node being traversed
    * was generated by the SAT solver and thus belong to the propositional view
+   * @return the id of the proof node printed
    */
-  void printInternal(std::ostream& out,
-                     const ProofNode* pn,
-                     uint64_t& ruleID,
-                     uint64_t scopeCounter,
-                     bool inPropositionalView);
+  uint64_t printInternal(std::ostream& out,
+                         const ProofNode* pn,
+                         std::map<size_t, uint64_t>& pfLet,
+                         uint64_t scopeCounter,
+                         bool inPropositionalView);
 
   /**
    * Return the arguments of a ProofNode
@@ -95,6 +96,9 @@ class DotPrinter
 
   /** Let binder for terms in proof nodes */
   LetBinding d_lbind;
+
+  /** Counter that indicates the current rule ID */
+  uint64_t d_ruleID;
 };
 
 }  // namespace proof

diff --git a/src/proof/proof_node.cpp b/src/proof/proof_node.cpp
index 2a141919d38c61b41393525d54ed9686a9c1c33d..a857b252ae69077809c2dc4dac3f1cebcae5f062 100644 (file)
--- a/src/proof/proof_node.cpp
+++ b/src/proof/proof_node.cpp
@@ -70,4 +70,26 @@ std::ostream& operator<<(std::ostream& out, const ProofNode& pn)
   return out;
 }
 
+size_t ProofNodeHashFunction::operator()(const ProofNode* pfn) const
+{
+  uint64_t ret = fnv1a::offsetBasis;
+
+  ret = fnv1a::fnv1a_64(ret, std::hash<Node>()(pfn->getResult()));
+  ret = fnv1a::fnv1a_64(ret, static_cast<size_t>(pfn->getRule()));
+
+  const std::vector<std::shared_ptr<ProofNode>>& children = pfn->getChildren();
+  for (const Pf& child : children)
+  {
+    ret = fnv1a::fnv1a_64(ret, std::hash<Node>()(child->getResult()));
+  }
+
+  const std::vector<Node>& args = pfn->getArguments();
+  for (const Node& arg : args)
+  {
+    ret = fnv1a::fnv1a_64(ret, std::hash<Node>()(arg));
+  }
+
+  return static_cast<size_t>(ret);
+}
+
 }  // namespace cvc5

diff --git a/src/proof/proof_node.h b/src/proof/proof_node.h
index f4552ae438c0f6b86112e6c2da3711891d3ecd42..5f7aaec3d9434118e4d451e4347bec5b9299060a 100644 (file)
--- a/src/proof/proof_node.h
+++ b/src/proof/proof_node.h
@@ -34,6 +34,7 @@ using Pf = std::shared_ptr<ProofNode>;
 struct ProofNodeHashFunction
 {
   inline size_t operator()(std::shared_ptr<ProofNode> pfn) const;
+  size_t operator()(const ProofNode* pfn) const;
 }; /* struct ProofNodeHashFunction */
 
 /** A node in a proof