GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/proof/dot/dot_printer.cpp Lines: 1 41 2.4 %
Date: 2021-03-23 Branches: 2 94 2.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file dot_printer.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Diego Camargos
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory) and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Implemantation of the module for printing dot proofs
13
 **/
14
15
#include "proof/dot/dot_printer.h"
16
17
#include <sstream>
18
#include "expr/proof_node_manager.h"
19
20
namespace CVC4 {
21
namespace proof {
22
23
void DotPrinter::cleanQuotes(std::string& s)
24
{
25
  std::string rep("\\\"");
26
  for (size_t pos = 0; (pos = s.find("\"", pos)) != std::string::npos;
27
       pos += rep.length())
28
  {
29
    s.replace(pos, rep.length() - 1, rep);
30
  }
31
}
32
33
void DotPrinter::print(std::ostream& out, const ProofNode* pn)
34
{
35
  uint64_t ruleID = 0;
36
37
  out << "digraph proof {\n";
38
  DotPrinter::printInternal(out, pn, ruleID);
39
  out << "}\n";
40
}
41
42
void DotPrinter::printInternal(std::ostream& out,
43
                               const ProofNode* pn,
44
                               uint64_t& ruleID)
45
{
46
  uint64_t currentRuleID = ruleID;
47
  std::ostringstream currentArguments, resultStr;
48
  DotPrinter::ruleArguments(currentArguments, pn);
49
  const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
50
51
  out << "\t\"" << currentRuleID << "\" [ shape = \"box\", label = \""
52
      << pn->getRule() << "(";
53
54
  // guarantee that arguments do not have unescaped quotes
55
  std::string astring = currentArguments.str();
56
  cleanQuotes(astring);
57
58
  out << astring << ")\"];\n\t\"" << currentRuleID
59
      << "c\" [ shape = \"ellipse\", label = \"";
60
61
  // guarantee that conclusion does not have unescaped quotes
62
  resultStr << pn->getResult();
63
  astring = resultStr.str();
64
  cleanQuotes(astring);
65
66
  out << astring << "\" ];\n\t\"" << currentRuleID << "\" -> \""
67
      << currentRuleID << "c\";\n";
68
69
  for (const std::shared_ptr<ProofNode>& c : children)
70
  {
71
    ++ruleID;
72
    out << "\t\"" << ruleID << "c\" -> \"" << currentRuleID << "\";\n";
73
    printInternal(out, c.get(), ruleID);
74
  }
75
}
76
77
void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
78
                               const ProofNode* pn)
79
{
80
  const std::vector<Node>& args = pn->getArguments();
81
82
  if (args.size())
83
  {
84
    currentArguments << args[0];
85
  }
86
87
  for (size_t i = 1, size = args.size(); i < size; i++)
88
  {
89
    currentArguments << ", " << args[i];
90
  }
91
}
92
93
}  // namespace proof
94
26685
}  // namespace CVC4