Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/dot/dot_printer.cpp	Lines:	1	167	0.6 %
Date:	2021-08-20	Branches:	2	386	0.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Diego Della Rocca de Camargos
 *
 * This file is part of the cvc5 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.
 * ****************************************************************************
 *
 * Implemantation of the module for printing dot proofs.
 */

#include "proof/dot/dot_printer.h"

#include <sstream>

#include "options/expr_options.h"
#include "printer/smt2/smt2_printer.h"
#include "proof/proof_checker.h"
#include "proof/proof_node_manager.h"
#include "theory/builtin/proof_checker.h"

namespace cvc5 {
namespace proof {

DotPrinter::DotPrinter()
    : d_lbind(options::defaultDagThresh() ? options::defaultDagThresh() + 1 : 0)
{
}

DotPrinter::~DotPrinter() {}

std::string DotPrinter::sanitizeStringDoubleQuotes(const std::string& s)
{
  std::string newS;
  newS.reserve(s.size());
  for (const char c : s)
  {
    switch (c)
    {
      case '\"': newS += "\\\\\\\""; break;
      case '>': newS += "\\>"; break;
      case '<': newS += "\\<"; break;
      case '{': newS += "\\{"; break;
      case '}': newS += "\\}"; break;
      case '|': newS += "\\|"; break;
      default: newS += c; break;
    }
  }

  return newS;
}

std::string DotPrinter::sanitizeString(const std::string& s)
{
  std::string newS;
  newS.reserve(s.size());
  for (const char c : s)
  {
    switch (c)
    {
      case '\"': newS += "\\\""; break;
      case '>': newS += "\\>"; break;
      case '<': newS += "\\<"; break;
      case '{': newS += "\\{"; break;
      case '}': newS += "\\}"; break;
      case '|': newS += "\\|"; break;
      default: newS += c; break;
    }
  }

  return newS;
}

void DotPrinter::countSubproofs(const ProofNode* pn)
{
  std::vector<const ProofNode*> visit;
  std::unordered_map<const ProofNode*, bool> visited;
  std::unordered_map<const ProofNode*, bool>::iterator it;
  const ProofNode* cur;
  visit.push_back(pn);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);
    if (it == visited.end())
    {
      visited[cur] = false;
      visit.push_back(cur);
      const std::vector<std::shared_ptr<ProofNode>>& children =
          cur->getChildren();
      for (const std::shared_ptr<ProofNode>& c : children)
      {
        visit.push_back(c.get());
      }
    }
    else if (!it->second)
    {
      visited[cur] = true;
      size_t counter = 1;
      const std::vector<std::shared_ptr<ProofNode>>& children =
          cur->getChildren();
      for (const std::shared_ptr<ProofNode>& c : children)
      {
        counter += d_subpfCounter[c.get()];
      }
      d_subpfCounter[cur] = counter;
    }
  } while (!visit.empty());
}

void DotPrinter::letifyResults(const ProofNode* pn)
{
  std::vector<const ProofNode*> visit;
  std::unordered_set<const ProofNode*> visited;
  std::unordered_set<const ProofNode*>::iterator it;
  const ProofNode* cur;
  visit.push_back(pn);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);
    if (it == visited.end())
    {
      d_lbind.process(cur->getResult());
      visited.insert(cur);
      const std::vector<std::shared_ptr<ProofNode>>& children =
          cur->getChildren();
      for (const std::shared_ptr<ProofNode>& c : children)
      {
        visit.push_back(c.get());
      }
    }
  } while (!visit.empty());
}

void DotPrinter::print(std::ostream& out, const ProofNode* pn)
{
  uint64_t ruleID = 0;
  countSubproofs(pn);
  letifyResults(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";
  // print let map
  std::vector<Node> letList;
  d_lbind.letify(letList);
  if (!letList.empty())
  {
    out << "\tcomment=\"{\\\"letMap\\\" : {";
    bool first = true;
    for (TNode n : letList)
    {
      size_t id = d_lbind.getId(n);
      Assert(id != 0);
      if (!first)
      {
        out << ", ";
      }
      else
      {
        first = false;
      }
      out << "\\\"let" << id << "\\\" : \\\"";
      std::ostringstream nStr;
      nStr << d_lbind.convert(n, "let", false);
      std::string astring = nStr.str();
      // we double the scaping of quotes because "simple scape" is ambiguous
      // with the scape of the delimiter of the value in the key-value map
      out << sanitizeStringDoubleQuotes(astring) << "\\\"";
    }
    out << "}}\";\n";
  }
  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)
{
  uint64_t currentRuleID = ruleID;
  const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
  std::ostringstream currentArguments, resultStr, classes, colors;

  out << "\t" << currentRuleID << " [ label = \"{";

  resultStr << d_lbind.convert(pn->getResult(), "let");
  std::string astring = resultStr.str();
  out << sanitizeString(astring);

  PfRule r = pn->getRule();
  DotPrinter::ruleArguments(currentArguments, pn);
  astring = currentArguments.str();
  out << "|" << r << sanitizeString(astring) << "}\"";
  classes << ", class = \"";
  colors << "";

  // set classes and colors, based on the view that the rule belongs
  switch (r)
  {
    case PfRule::SCOPE:
      if (scopeCounter < 1)
      {
        classes << " basic";
        colors << ", color = blue ";
        inPropositionalView = true;
      }
      scopeCounter++;
      break;
    case PfRule::ASSUME:
      // a node can belong to more than one view, so these if's must not be
      // exclusive
      if (scopeCounter < 2)
      {
        classes << " basic";
        colors << ", color = blue ";
      }
      if (inPropositionalView)
      {
        classes << " propositional";
        colors << ", fillcolor = aquamarine4, style = filled ";
      }
      break;
    case PfRule::CHAIN_RESOLUTION:
    case PfRule::FACTORING:
    case PfRule::REORDERING:
      if (inPropositionalView)
      {
        classes << " propositional";
        colors << ", fillcolor = aquamarine4, style = filled ";
      }
      break;
    default: inPropositionalView = false;
  }
  classes << " \"";
  out << classes.str() << colors.str();
  // add number of subchildren
  std::map<const ProofNode*, size_t>::const_iterator it =
      d_subpfCounter.find(pn);
  out << ", comment = \"{\\\"subProofQty\\\":" << it->second << "}\"";
  out << " ];\n";

  for (const std::shared_ptr<ProofNode>& c : children)
  {
    ++ruleID;
    out << "\t" << ruleID << " -> " << currentRuleID << ";\n";
    printInternal(out, c.get(), ruleID, scopeCounter, inPropositionalView);
  }
}

void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
                               const ProofNode* pn)
{
  const std::vector<Node>& args = pn->getArguments();
  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)
  {
    return;
  }
  currentArguments << " :args [ ";

  // 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 << d_lbind.convert(args[1], "let");
    }
    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 << d_lbind.convert(args[0], "let");
    for (size_t i = 1, size = args.size(); i < size; i++)
    {
      currentArguments << ", " << d_lbind.convert(args[i], "let");
    }
  }
  currentArguments << " ]";
}

}  // namespace proof
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Diego Della Rocca de Camargos
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* Implemantation of the module for printing dot proofs.
14		*/
15
16		#include "proof/dot/dot_printer.h"
17
18		#include <sstream>
19
20		#include "options/expr_options.h"
21		#include "printer/smt2/smt2_printer.h"
22		#include "proof/proof_checker.h"
23		#include "proof/proof_node_manager.h"
24		#include "theory/builtin/proof_checker.h"
25
26		namespace cvc5 {
27		namespace proof {
28
29		DotPrinter::DotPrinter()
30		: d_lbind(options::defaultDagThresh() ? options::defaultDagThresh() + 1 : 0)
31		{
32		}
33
34		DotPrinter::~DotPrinter() {}
35
36		std::string DotPrinter::sanitizeStringDoubleQuotes(const std::string& s)
37		{
38		std::string newS;
39		newS.reserve(s.size());
40		for (const char c : s)
41		{
42		switch (c)
43		{
44		case '\"': newS += "\\\\\\\""; break;
45		case '>': newS += "\\>"; break;
46		case '<': newS += "\\<"; break;
47		case '{': newS += "\\{"; break;
48		case '}': newS += "\\}"; break;
49		case '\|': newS += "\\\|"; break;
50		default: newS += c; break;
51		}
52		}
53
54		return newS;
55		}
56
57		std::string DotPrinter::sanitizeString(const std::string& s)
58		{
59		std::string newS;
60		newS.reserve(s.size());
61		for (const char c : s)
62		{
63		switch (c)
64		{
65		case '\"': newS += "\\\""; break;
66		case '>': newS += "\\>"; break;
67		case '<': newS += "\\<"; break;
68		case '{': newS += "\\{"; break;
69		case '}': newS += "\\}"; break;
70		case '\|': newS += "\\\|"; break;
71		default: newS += c; break;
72		}
73		}
74
75		return newS;
76		}
77
78		void DotPrinter::countSubproofs(const ProofNode* pn)
79		{
80		std::vector<const ProofNode*> visit;
81		std::unordered_map<const ProofNode*, bool> visited;
82		std::unordered_map<const ProofNode*, bool>::iterator it;
83		const ProofNode* cur;
84		visit.push_back(pn);
85		do
86		{
87		cur = visit.back();
88		visit.pop_back();
89		it = visited.find(cur);
90		if (it == visited.end())
91		{
92		visited[cur] = false;
93		visit.push_back(cur);
94		const std::vector<std::shared_ptr<ProofNode>>& children =
95		cur->getChildren();
96		for (const std::shared_ptr<ProofNode>& c : children)
97		{
98		visit.push_back(c.get());
99		}
100		}
101		else if (!it->second)
102		{
103		visited[cur] = true;
104		size_t counter = 1;
105		const std::vector<std::shared_ptr<ProofNode>>& children =
106		cur->getChildren();
107		for (const std::shared_ptr<ProofNode>& c : children)
108		{
109		counter += d_subpfCounter[c.get()];
110		}
111		d_subpfCounter[cur] = counter;
112		}
113		} while (!visit.empty());
114		}
115
116		void DotPrinter::letifyResults(const ProofNode* pn)
117		{
118		std::vector<const ProofNode*> visit;
119		std::unordered_set<const ProofNode*> visited;
120		std::unordered_set<const ProofNode*>::iterator it;
121		const ProofNode* cur;
122		visit.push_back(pn);
123		do
124		{
125		cur = visit.back();
126		visit.pop_back();
127		it = visited.find(cur);
128		if (it == visited.end())
129		{
130		d_lbind.process(cur->getResult());
131		visited.insert(cur);
132		const std::vector<std::shared_ptr<ProofNode>>& children =
133		cur->getChildren();
134		for (const std::shared_ptr<ProofNode>& c : children)
135		{
136		visit.push_back(c.get());
137		}
138		}
139		} while (!visit.empty());
140		}
141
142		void DotPrinter::print(std::ostream& out, const ProofNode* pn)
143		{
144		uint64_t ruleID = 0;
145		countSubproofs(pn);
146		letifyResults(pn);
147
148		// The dot attribute rankdir="BT" sets the direction of the graph layout,
149		// placing the root node at the top. The "node [shape..." attribute sets the
150		// shape of all nodes to record.
151		out << "digraph proof {\n\trankdir=\"BT\";\n\tnode [shape=record];\n";
152		// print let map
153		std::vector<Node> letList;
154		d_lbind.letify(letList);
155		if (!letList.empty())
156		{
157		out << "\tcomment=\"{\\\"letMap\\\" : {";
158		bool first = true;
159		for (TNode n : letList)
160		{
161		size_t id = d_lbind.getId(n);
162		Assert(id != 0);
163		if (!first)
164		{
165		out << ", ";
166		}
167		else
168		{
169		first = false;
170		}
171		out << "\\\"let" << id << "\\\" : \\\"";
172		std::ostringstream nStr;
173		nStr << d_lbind.convert(n, "let", false);
174		std::string astring = nStr.str();
175		// we double the scaping of quotes because "simple scape" is ambiguous
176		// with the scape of the delimiter of the value in the key-value map
177		out << sanitizeStringDoubleQuotes(astring) << "\\\"";
178		}
179		out << "}}\";\n";
180		}
181		DotPrinter::printInternal(out, pn, ruleID, 0, false);
182		out << "}\n";
183		}
184
185		void DotPrinter::printInternal(std::ostream& out,
186		const ProofNode* pn,
187		uint64_t& ruleID,
188		uint64_t scopeCounter,
189		bool inPropositionalView)
190		{
191		uint64_t currentRuleID = ruleID;
192		const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
193		std::ostringstream currentArguments, resultStr, classes, colors;
194
195		out << "\t" << currentRuleID << " [ label = \"{";
196
197		resultStr << d_lbind.convert(pn->getResult(), "let");
198		std::string astring = resultStr.str();
199		out << sanitizeString(astring);
200
201		PfRule r = pn->getRule();
202		DotPrinter::ruleArguments(currentArguments, pn);
203		astring = currentArguments.str();
204		out << "\|" << r << sanitizeString(astring) << "}\"";
205		classes << ", class = \"";
206		colors << "";
207
208		// set classes and colors, based on the view that the rule belongs
209		switch (r)
210		{
211		case PfRule::SCOPE:
212		if (scopeCounter < 1)
213		{
214		classes << " basic";
215		colors << ", color = blue ";
216		inPropositionalView = true;
217		}
218		scopeCounter++;
219		break;
220		case PfRule::ASSUME:
221		// a node can belong to more than one view, so these if's must not be
222		// exclusive
223		if (scopeCounter < 2)
224		{
225		classes << " basic";
226		colors << ", color = blue ";
227		}
228		if (inPropositionalView)
229		{
230		classes << " propositional";
231		colors << ", fillcolor = aquamarine4, style = filled ";
232		}
233		break;
234		case PfRule::CHAIN_RESOLUTION:
235		case PfRule::FACTORING:
236		case PfRule::REORDERING:
237		if (inPropositionalView)
238		{
239		classes << " propositional";
240		colors << ", fillcolor = aquamarine4, style = filled ";
241		}
242		break;
243		default: inPropositionalView = false;
244		}
245		classes << " \"";
246		out << classes.str() << colors.str();
247		// add number of subchildren
248		std::map<const ProofNode*, size_t>::const_iterator it =
249		d_subpfCounter.find(pn);
250		out << ", comment = \"{\\\"subProofQty\\\":" << it->second << "}\"";
251		out << " ];\n";
252
253		for (const std::shared_ptr<ProofNode>& c : children)
254		{
255		++ruleID;
256		out << "\t" << ruleID << " -> " << currentRuleID << ";\n";
257		printInternal(out, c.get(), ruleID, scopeCounter, inPropositionalView);
258		}
259		}
260
261		void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
262		const ProofNode* pn)
263		{
264		const std::vector<Node>& args = pn->getArguments();
265		PfRule r = pn->getRule();
266		// don't process arguments of rules whose conclusion is in the arguments
267		if (!args.size() \|\| r == PfRule::ASSUME \|\| r == PfRule::REORDERING
268		\|\| r == PfRule::REFL)
269		{
270		return;
271		}
272		currentArguments << " :args [ ";
273
274		// if cong, special process
275		if (r == PfRule::CONG)
276		{
277		AlwaysAssert(args.size() == 1 \|\| args.size() == 2);
278		// if two arguments, ignore first and print second
279		if (args.size() == 2)
280		{
281		currentArguments << d_lbind.convert(args[1], "let");
282		}
283		else
284		{
285		Kind k;
286		ProofRuleChecker::getKind(args[0], k);
287		currentArguments << printer::smt2::Smt2Printer::smtKindString(k);
288		}
289		}
290		// if th_rw, likewise
291		else if (r == PfRule::THEORY_REWRITE)
292		{
293		// print the second argument
294		theory::TheoryId id;
295		theory::builtin::BuiltinProofRuleChecker::getTheoryId(args[1], id);
296		std::ostringstream ss;
297		ss << id;
298		std::string s = ss.str();
299		// delete "THEORY_" prefix
300		s.erase(0, 7);
301		currentArguments << s;
302		}
303		else
304		{
305		currentArguments << d_lbind.convert(args[0], "let");
306		for (size_t i = 1, size = args.size(); i < size; i++)
307		{
308		currentArguments << ", " << d_lbind.convert(args[i], "let");
309		}
310		}
311		currentArguments << " ]";
312		}
313
314		} // namespace proof
315	29358	} // namespace cvc5