1 | /*
|
2 | * Souffle - A Datalog Compiler
|
3 | * Copyright (c) 2017, The Souffle Developers. All rights reserved
|
4 | * Licensed under the Universal Permissive License v 1.0 as shown at:
|
5 | * - https://opensource.org/licenses/UPL
|
6 | * - <souffle root>/licenses/SOUFFLE-UPL.txt
|
7 | */
|
8 |
|
9 | /************************************************************************
|
10 | *
|
11 | * @file ExplainTree.h
|
12 | *
|
13 | * Classes for storing a derivation tree
|
14 | *
|
15 | ***********************************************************************/
|
16 |
|
17 | #pragma once
|
18 |
|
19 | #include "souffle/utility/ContainerUtil.h"
|
20 | #include "souffle/utility/StringUtil.h"
|
21 | #include <algorithm>
|
22 | #include <cassert>
|
23 | #include <cstdint>
|
24 | #include <cstring>
|
25 | #include <memory>
|
26 | #include <sstream>
|
27 | #include <string>
|
28 | #include <utility>
|
29 | #include <vector>
|
30 |
|
31 | namespace souffle {
|
32 |
|
33 | class ScreenBuffer {
|
34 | public:
|
35 | // constructor
|
36 | ScreenBuffer(uint32_t w, uint32_t h) : width(w), height(h), buffer(nullptr) {
|
37 | assert(width > 0 && height > 0 && "wrong dimensions");
|
38 | buffer = new char[width * height];
|
39 | memset(buffer, ' ', width * height);
|
40 | }
|
41 |
|
42 | ~ScreenBuffer() {
|
43 | delete[] buffer;
|
44 | }
|
45 |
|
46 | // write into screen buffer at a specific location
|
47 | void write(uint32_t x, uint32_t y, const std::string& s) {
|
48 | assert(x < width && "wrong x dimension");
|
49 | assert(y < height && "wrong y dimension");
|
50 | assert(x + s.length() <= width && "string too long");
|
51 | for (std::size_t i = 0; i < s.length(); i++) {
|
52 | buffer[y * width + x + i] = s[i];
|
53 | }
|
54 | }
|
55 |
|
56 | std::string getString() {
|
57 | std::stringstream ss;
|
58 | print(ss);
|
59 | return ss.str();
|
60 | }
|
61 |
|
62 | // print screen buffer
|
63 | void print(std::ostream& os) {
|
64 | if (height > 0 && width > 0) {
|
65 | for (int i = height - 1; i >= 0; i--) {
|
66 | for (std::size_t j = 0; j < width; j++) {
|
67 | os << buffer[width * i + j];
|
68 | }
|
69 | os << std::endl;
|
70 | }
|
71 | }
|
72 | }
|
73 |
|
74 | private:
|
75 | uint32_t width; // width of the screen buffer
|
76 | uint32_t height; // height of the screen buffer
|
77 | char* buffer; // screen contents
|
78 | };
|
79 |
|
80 | /***
|
81 | * Abstract Class for a Proof Tree Node
|
82 | *
|
83 | */
|
84 | class TreeNode {
|
85 | public:
|
86 | TreeNode(std::string t = "") : txt(std::move(t)) {}
|
87 | virtual ~TreeNode() = default;
|
88 |
|
89 | // get width
|
90 | uint32_t getWidth() const {
|
91 | return width;
|
92 | }
|
93 |
|
94 | // get height
|
95 | uint32_t getHeight() const {
|
96 | return height;
|
97 | }
|
98 |
|
99 | // place the node
|
100 | virtual void place(uint32_t xpos, uint32_t ypos) = 0;
|
101 |
|
102 | // render node in screen buffer
|
103 | virtual void render(ScreenBuffer& s) = 0;
|
104 |
|
105 | std::size_t getSize() {
|
106 | return size;
|
107 | }
|
108 |
|
109 | void setSize(std::size_t s) {
|
110 | size = s;
|
111 | }
|
112 |
|
113 | virtual void printJSON(std::ostream& os, int pos) = 0;
|
114 |
|
115 | protected:
|
116 | std::string txt; // text of tree node
|
117 | uint32_t width = 0; // width of node (including sub-trees)
|
118 | uint32_t height = 0; // height of node (including sub-trees)
|
119 | int xpos = 0; // x-position of text
|
120 | int ypos = 0; // y-position of text
|
121 | uint32_t size = 0;
|
122 | };
|
123 |
|
124 | /***
|
125 | * Concrete class
|
126 | */
|
127 | class InnerNode : public TreeNode {
|
128 | public:
|
129 | InnerNode(const std::string& nodeText = "", std::string label = "")
|
130 | : TreeNode(nodeText), label(std::move(label)) {}
|
131 |
|
132 | // add child to node
|
133 | void add_child(Own<TreeNode> child) {
|
134 | children.push_back(std::move(child));
|
135 | }
|
136 |
|
137 | // place node and its sub-trees
|
138 | void place(uint32_t x, uint32_t y) override {
|
139 | // there must exist at least one kid
|
140 | assert(!children.empty() && "no children");
|
141 |
|
142 | // set x/y pos
|
143 | xpos = x;
|
144 | ypos = y;
|
145 |
|
146 | height = 0;
|
147 |
|
148 | // compute size of bounding box
|
149 | for (const Own<TreeNode>& k : children) {
|
150 | k->place(x, y + 2);
|
151 | x += k->getWidth() + 1;
|
152 | width += k->getWidth() + 1;
|
153 | height = std::max(height, k->getHeight());
|
154 | }
|
155 | height += 2;
|
156 |
|
157 | // text of inner node is longer than all its sub-trees
|
158 | if (width < txt.length()) {
|
159 | width = txt.length();
|
160 | }
|
161 | };
|
162 |
|
163 | // render node text and separator line
|
164 | void render(ScreenBuffer& s) override {
|
165 | s.write(xpos + (width - txt.length()) / 2, ypos, txt);
|
166 | for (const Own<TreeNode>& k : children) {
|
167 | k->render(s);
|
168 | }
|
169 | std::string separator(width - label.length(), '-');
|
170 | separator += label;
|
171 | s.write(xpos, ypos + 1, separator);
|
172 | }
|
173 |
|
174 | // print JSON
|
175 | void printJSON(std::ostream& os, int pos) override {
|
176 | std::string tab(pos, '\t');
|
177 | os << tab << R"({ "premises": ")" << stringify(txt) << "\",\n";
|
178 | os << tab << R"( "rule-number": ")" << label << "\",\n";
|
179 | os << tab << " \"children\": [\n";
|
180 | bool first = true;
|
181 | for (const Own<TreeNode>& k : children) {
|
182 | if (first) {
|
183 | first = false;
|
184 | } else {
|
185 | os << ",\n";
|
186 | }
|
187 | k->printJSON(os, pos + 1);
|
188 | }
|
189 | os << tab << "]\n";
|
190 | os << tab << "}";
|
191 | }
|
192 |
|
193 | private:
|
194 | VecOwn<TreeNode> children;
|
195 | std::string label;
|
196 | };
|
197 |
|
198 | /***
|
199 | * Concrete class for leafs
|
200 | */
|
201 | class LeafNode : public TreeNode {
|
202 | public:
|
203 | LeafNode(const std::string& t = "") : TreeNode(t) {
|
204 | setSize(1);
|
205 | }
|
206 |
|
207 | // place leaf node
|
208 | void place(uint32_t x, uint32_t y) override {
|
209 | xpos = x;
|
210 | ypos = y;
|
211 | width = txt.length();
|
212 | height = 1;
|
213 | }
|
214 |
|
215 | // render text of leaf node
|
216 | void render(ScreenBuffer& s) override {
|
217 | s.write(xpos, ypos, txt);
|
218 | }
|
219 |
|
220 | // print JSON
|
221 | void printJSON(std::ostream& os, int pos) override {
|
222 | std::string tab(pos, '\t');
|
223 | os << tab << R"({ "axiom": ")" << stringify(txt) << "\"}";
|
224 | }
|
225 | };
|
226 |
|
227 | } // end of namespace souffle
|