[proof-new] Adding a dot printer for proof nodes (#6144)

Adds a dot printer for proof nodes. Also adds an option to choose the proof format (as a mode).

Signed-off-by: Diego Della Rocca de Camargos <diegodellarocc@gmail.com>

5 files changed, 197 insertions, 4 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 005911ca8..e65e06da3 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -140,6 +140,8 @@ libcvc4_add_sources(
   proof/clause_id.h
   proof/cnf_proof.cpp
   proof/cnf_proof.h
+  proof/dot/dot_printer.cpp
+  proof/dot/dot_printer.h
   proof/proof_manager.cpp
   proof/proof_manager.h
   proof/sat_proof.h
diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index 631a27604..ff03e70f5 100644
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -3,6 +3,21 @@ name   = "Proof"
 header = "options/proof_options.h"
 
 [[option]]
+  name       = "proofFormatMode"
+  category   = "regular"
+  long       = "proof-format-mode=MODE"
+  type       = "ProofFormatMode"
+  default    = "NONE"
+  help       = "select language of proof output"
+  help_mode  = "Proof format modes."
+[[option.mode.NONE]]
+  name       = "none"
+  help       = "Do not translate proof output"
+[[option.mode.DOT]]
+  name       = "dot"
+  help       = "Output DOT proof"
+  
+[[option]]
   name       = "proofPrintConclusion"
   category   = "regular"
   long       = "proof-print-conclusion"
diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp
new file mode 100644
index 000000000..f542924b1
--- /dev/null
+++ b/src/proof/dot/dot_printer.cpp
@@ -0,0 +1,94 @@
+/*********************                                                        */
+/*! \file dot_printer.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Diego Camargos
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implemantation of the module for printing dot proofs
+ **/
+
+#include "proof/dot/dot_printer.h"
+
+#include <sstream>
+#include "expr/proof_node_manager.h"
+
+namespace CVC4 {
+namespace proof {
+
+void DotPrinter::cleanQuotes(std::string& s)
+{
+  std::string rep("\\\"");
+  for (size_t pos = 0; (pos = s.find("\"", pos)) != std::string::npos;
+       pos += rep.length())
+  {
+    s.replace(pos, rep.length() - 1, rep);
+  }
+}
+
+void DotPrinter::print(std::ostream& out, const ProofNode* pn)
+{
+  uint64_t ruleID = 0;
+
+  out << "digraph proof {\n";
+  DotPrinter::printInternal(out, pn, ruleID);
+  out << "}\n";
+}
+
+void DotPrinter::printInternal(std::ostream& out,
+                               const ProofNode* pn,
+                               uint64_t& ruleID)
+{
+  uint64_t currentRuleID = ruleID;
+  std::ostringstream currentArguments, resultStr;
+  DotPrinter::ruleArguments(currentArguments, pn);
+  const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
+
+  out << "\t\"" << currentRuleID << "\" [ shape = \"box\", label = \""
+      << pn->getRule() << "(";
+
+  // guarantee that arguments do not have unescaped quotes
+  std::string astring = currentArguments.str();
+  cleanQuotes(astring);
+
+  out << astring << ")\"];\n\t\"" << currentRuleID
+      << "c\" [ shape = \"ellipse\", label = \"";
+
+  // guarantee that conclusion does not have unescaped quotes
+  resultStr << pn->getResult();
+  astring = resultStr.str();
+  cleanQuotes(astring);
+
+  out << astring << "\" ];\n\t\"" << currentRuleID << "\" -> \""
+      << currentRuleID << "c\";\n";
+
+  for (const std::shared_ptr<ProofNode>& c : children)
+  {
+    ++ruleID;
+    out << "\t\"" << ruleID << "c\" -> \"" << currentRuleID << "\";\n";
+    printInternal(out, c.get(), ruleID);
+  }
+}
+
+void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
+                               const ProofNode* pn)
+{
+  const std::vector<Node>& args = pn->getArguments();
+
+  if (args.size())
+  {
+    currentArguments << args[0];
+  }
+
+  for (size_t i = 1, size = args.size(); i < size; i++)
+  {
+    currentArguments << ", " << args[i];
+  }
+}
+
+}  // namespace proof
+}  // namespace CVC4
diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h
new file mode 100644
index 000000000..4b7d7660c
--- /dev/null
+++ b/src/proof/dot/dot_printer.h
@@ -0,0 +1,74 @@
+/*********************                                                        */
+/*! \file dot_printer.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Diego Camargos
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The module for printing dot proofs
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__PROOF__DOT__DOT_PRINTER_H
+#define CVC4__PROOF__DOT__DOT_PRINTER_H
+
+#include <iostream>
+
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace proof {
+
+class DotPrinter
+{
+ public:
+  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);
+
+ private:
+  /**
+   * Print the rule in the format:
+   * "$RULE_ID $RULE_NAME($RULE_ARGUMENTS)" [ shape = "box"];
+   * "$RULE_ID $RULE_NAME($RULE_ARGUMENTS)" -> "$RULE_ID $RULE_CONCLUSION";
+   * and then for each child of the rule print
+   * "$CHILD_ID $CHILD_CONCLUSION" -> "$RULE_ID $RULE_NAME($RULE_ARGUMENTS)";
+   * and then recursively call the function with 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
+   */
+  static void printInternal(std::ostream& out,
+                            const ProofNode* pn,
+                            uint64_t& ruleID);
+
+  /**
+   * Return the arguments of a ProofNode
+   * @param currentArguments an ostringstream that will store the arguments of
+   * pn formatted as "$ARG[0], $ARG[1], ..., $ARG[N-1]"
+   * @param pn a ProofNode
+   */
+  static void ruleArguments(std::ostringstream& currentArguments,
+                            const ProofNode* pn);
+
+  /** Replace all quotes but escaped quotes in given string
+   * @param s The string to have the quotes processed.
+   */
+  static void cleanQuotes(std::string& s);
+};
+
+}  // namespace proof
+}  // namespace CVC4
+
+#endif
\ No newline at end of file
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 0ae65967f..765beb9a2 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -19,6 +19,7 @@
 #include "expr/proof_node_manager.h"
 #include "options/base_options.h"
 #include "options/proof_options.h"
+#include "proof/dot/dot_printer.h"
 #include "smt/assertions.h"
 #include "smt/defined_function.h"
 #include "smt/preprocess_proof_generator.h"
@@ -122,11 +123,18 @@ void PfManager::printProof(std::ostream& out,
   std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df);
   // TODO (proj #37) according to the proof format, post process the proof node
   // TODO (proj #37) according to the proof format, print the proof node
-  out << "(proof\n";
-  out << *fp;
-  out << "\n)\n";
+  
+  if (options::proofFormatMode() == options::ProofFormatMode::DOT)
+  {
+    proof::DotPrinter::print(out, fp.get());
+  }
+  else
+  {
+    out << "(proof\n";
+    out << *fp;
+    out << "\n)\n";
+  }
 }
-
 void PfManager::checkProof(std::shared_ptr<ProofNode> pfn,
                            Assertions& as,
                            DefinedFunctionMap& df)