OILS / vendor / souffle / provenance / ExplainTree.h View on Github | oilshell.org

227 lines, 125 significant
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
31namespace souffle {
32
33class ScreenBuffer {
34public:
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
74private:
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 */
84class TreeNode {
85public:
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
115protected:
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 */
127class InnerNode : public TreeNode {
128public:
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
193private:
194 VecOwn<TreeNode> children;
195 std::string label;
196};
197
198/***
199 * Concrete class for leafs
200 */
201class LeafNode : public TreeNode {
202public:
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