[proof-new] Miscellaneous improvements to dot printer (#6342)

diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp
index 9763bcda3623424ccfc56d529cd50e20da691db9..4f13ef17a57cc86e86d840d6e82bd3b8eca51a40 100644 (file)
--- a/src/proof/dot/dot_printer.cpp
+++ b/src/proof/dot/dot_printer.cpp
@@ -16,7 +16,11 @@
 #include "proof/dot/dot_printer.h"
 
 #include <sstream>
+
+#include "expr/proof_checker.h"
 #include "expr/proof_node_manager.h"
+#include "printer/smt2/smt2_printer.h"
+#include "theory/builtin/proof_checker.h"
 
 namespace cvc5 {
 namespace proof {
@@ -45,20 +49,18 @@ void DotPrinter::printInternal(std::ostream& out,
                                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();
+  PfRule r = pn->getRule();
 
-  out << "\t\"" << currentRuleID << "\" [ shape = \"box\", label = \""
-      << pn->getRule() << "(";
+  out << "\t\"" << currentRuleID << "\" [ shape = \"box\", label = \"" << r;
 
+  std::ostringstream currentArguments, resultStr;
+  const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
+  DotPrinter::ruleArguments(currentArguments, pn);
   // guarantee that arguments do not have unescaped quotes
   std::string astring = currentArguments.str();
   cleanQuotes(astring);
-
-  out << astring << ")\"];\n\t\"" << currentRuleID
+  out << astring << "\"];\n\t\"" << currentRuleID
       << "c\" [ shape = \"ellipse\", label = \"";
-
   // guarantee that conclusion does not have unescaped quotes
   resultStr << pn->getResult();
   astring = resultStr.str();
@@ -79,16 +81,53 @@ void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
                                const ProofNode* pn)
 {
   const std::vector<Node>& args = pn->getArguments();
-
-  if (args.size())
+  PfRule r = pn->getRule();
+  // don't process arguments of rules whose conclusion is in the arguments
+  if (!args.size() || r == PfRule::ASSUME || r == PfRule::REORDERING
+      || r == PfRule::REFL)
   {
-    currentArguments << args[0];
+    return;
   }
+  currentArguments << " :args [ ";
 
-  for (size_t i = 1, size = args.size(); i < size; i++)
+  // if cong, special process
+  if (r == PfRule::CONG)
+  {
+    AlwaysAssert(args.size() == 1 || args.size() == 2);
+    // if two arguments, ignore first and print second
+    if (args.size() == 2)
+    {
+      currentArguments << args[1];
+    }
+    else
+    {
+      Kind k;
+      ProofRuleChecker::getKind(args[0], k);
+      currentArguments << printer::smt2::Smt2Printer::smtKindString(k);
+    }
+  }
+  // if th_rw, likewise
+  else if (r == PfRule::THEORY_REWRITE)
+  {
+    // print the second argument
+    theory::TheoryId id;
+    theory::builtin::BuiltinProofRuleChecker::getTheoryId(args[1], id);
+    std::ostringstream ss;
+    ss << id;
+    std::string s = ss.str();
+    // delete "THEORY_" prefix
+    s.erase(0, 7);
+    currentArguments << s;
+  }
+  else
   {
-    currentArguments << ", " << args[i];
+    currentArguments << args[0];
+    for (size_t i = 1, size = args.size(); i < size; i++)
+    {
+      currentArguments << ", " << args[i];
+    }
   }
+  currentArguments << " ]";
 }
 
 }  // namespace proof