[proof] [dot] Make dot printer stateful (#6799)

In preparation for further changes in the printer.

diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp
index 08be1728b5a95ac4dd270b9650497b6083748951..496085372c1c46db2074e28734b0f859ee1b7717 100644 (file)
--- a/src/proof/dot/dot_printer.cpp
+++ b/src/proof/dot/dot_printer.cpp
@@ -25,6 +25,9 @@
 namespace cvc5 {
 namespace proof {
 
+DotPrinter::DotPrinter() {}
+DotPrinter::~DotPrinter() {}
+
 std::string DotPrinter::sanitizeString(const std::string& s)
 {
   std::string newS;
@@ -46,8 +49,7 @@ std::string DotPrinter::sanitizeString(const std::string& s)
   return newS;
 }
 
-void DotPrinter::countSubproofs(
-    const ProofNode* pn, std::map<const ProofNode*, size_t>& subpfCounter)
+void DotPrinter::countSubproofs(const ProofNode* pn)
 {
   std::vector<const ProofNode*> visit;
   std::unordered_map<const ProofNode*, bool> visited;
@@ -78,9 +80,9 @@ void DotPrinter::countSubproofs(
           cur->getChildren();
       for (const std::shared_ptr<ProofNode>& c : children)
       {
-        counter += subpfCounter[c.get()];
+        counter += d_subpfCounter[c.get()];
       }
-      subpfCounter[cur] = counter;
+      d_subpfCounter[cur] = counter;
     }
   } while (!visit.empty());
 }
@@ -88,24 +90,21 @@ void DotPrinter::countSubproofs(
 void DotPrinter::print(std::ostream& out, const ProofNode* pn)
 {
   uint64_t ruleID = 0;
-  std::map<const ProofNode*, size_t> subpfCounter;
-  countSubproofs(pn, subpfCounter);
+  countSubproofs(pn);
 
   // The dot attribute rankdir="BT" sets the direction of the graph layout,
   // placing the root node at the top. The "node [shape..." attribute sets the
   // shape of all nodes to record.
   out << "digraph proof {\n\trankdir=\"BT\";\n\tnode [shape=record];\n";
-  DotPrinter::printInternal(out, pn, ruleID, 0, false, subpfCounter);
+  DotPrinter::printInternal(out, pn, ruleID, 0, false);
   out << "}\n";
 }
 
-void DotPrinter::printInternal(
-    std::ostream& out,
-    const ProofNode* pn,
-    uint64_t& ruleID,
-    uint64_t scopeCounter,
-    bool inPropositionalView,
-    const std::map<const ProofNode*, size_t>& subpfCounter)
+void DotPrinter::printInternal(std::ostream& out,
+                               const ProofNode* pn,
+                               uint64_t& ruleID,
+                               uint64_t scopeCounter,
+                               bool inPropositionalView)
 {
   uint64_t currentRuleID = ruleID;
   const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
@@ -164,7 +163,8 @@ void DotPrinter::printInternal(
   classes << " \"";
   out << classes.str() << colors.str();
   // add number of subchildren
-  std::map<const ProofNode*, size_t>::const_iterator it = subpfCounter.find(pn);
+  std::map<const ProofNode*, size_t>::const_iterator it =
+      d_subpfCounter.find(pn);
   out << ", comment = \"\{\"subProofQty\":" << it->second << "}\"";
   out << " ];\n";
 
@@ -172,8 +172,7 @@ void DotPrinter::printInternal(
   {
     ++ruleID;
     out << "\t" << ruleID << " -> " << currentRuleID << ";\n";
-    printInternal(
-        out, c.get(), ruleID, scopeCounter, inPropositionalView, subpfCounter);
+    printInternal(out, c.get(), ruleID, scopeCounter, inPropositionalView);
   }
 }
 

diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h
index a877efe9bddf118c004fa13fc4d53d5349ab4150..2d25fe0e7d6b8bf52cc8be8f7ff2160ac55e86db 100644 (file)
--- a/src/proof/dot/dot_printer.h
+++ b/src/proof/dot/dot_printer.h
@@ -29,14 +29,14 @@ class DotPrinter
 {
  public:
   DotPrinter();
-  ~DotPrinter() {}
+  ~DotPrinter();
 
   /**
    * Print the full proof of assertions => false by pn using the dot format.
    * @param out the output stream
    * @param pn the root node of the proof to print
    */
-  static void print(std::ostream& out, const ProofNode* pn);
+  void print(std::ostream& out, const ProofNode* pn);
 
  private:
   /**
@@ -53,13 +53,11 @@ class DotPrinter
    * @param inPropositionalView flag used to mark the proof node being traversed
    * was generated by the SAT solver and thus belong to the propositional view
    */
-  static void printInternal(
-      std::ostream& out,
-      const ProofNode* pn,
-      uint64_t& ruleID,
-      uint64_t scopeCounter,
-      bool inPropositionalView,
-      const std::map<const ProofNode*, size_t>& subpfCounter);
+  void printInternal(std::ostream& out,
+                     const ProofNode* pn,
+                     uint64_t& ruleID,
+                     uint64_t scopeCounter,
+                     bool inPropositionalView);
 
   /**
    * Return the arguments of a ProofNode
@@ -67,8 +65,7 @@ class DotPrinter
    * pn formatted as "$ARG[0], $ARG[1], ..., $ARG[N-1]"
    * @param pn a ProofNode
    */
-  static void ruleArguments(std::ostringstream& currentArguments,
-                            const ProofNode* pn);
+  void ruleArguments(std::ostringstream& currentArguments, const ProofNode* pn);
 
   /** Add an escape character before special characters of the given string.
    * @param s The string to have the characters processed.
@@ -76,14 +73,16 @@ class DotPrinter
    */
   static std::string sanitizeString(const std::string& s);
 
-  /** Traverse proof node and map each proof node to the number of subproofs it
-   * contains, including itself
+  /** Traverse proof node and populate d_subpfCounter, mapping each proof node
+   * to the number of subproofs it contains, including itself
    *
    * @param pn the proof node to be traversed
-   * @param subpfCounter the map to be populated
    */
-  static void countSubproofs(const ProofNode* pn,
-                             std::map<const ProofNode*, size_t>& subpfCounter);
+  void countSubproofs(const ProofNode* pn);
+
+  /** All unique subproofs of a given proof node (counting itself). */
+  std::map<const ProofNode*, size_t> d_subpfCounter;
+
 };
 
 }  // namespace proof

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 55cfc1f15b3765953d5bae5aa457a8e6f3faeda0..eb5d8e7afa109dc2f1f4df4127e4543c894896d0 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -153,7 +153,8 @@ void PfManager::printProof(std::ostream& out,
 
   if (options::proofFormatMode() == options::ProofFormatMode::DOT)
   {
-    proof::DotPrinter::print(out, fp.get());
+    proof::DotPrinter dotPrinter;
+    dotPrinter.print(out, fp.get());
   }
   else
   {