1 /**++
2 Copyright (c) 2017 Microsoft Corporation and Matteo Marescotti
3
4 Module Name:
5
6 spacer_json.cpp
7
8 Abstract:
9
10 SPACER json marshalling support
11
12 Author:
13
14 Matteo Marescotti
15
16 Notes:
17
18 --*/
19
20 #include <iomanip>
21 #include "spacer_context.h"
22 #include "spacer_json.h"
23 #include "spacer_util.h"
24
25 namespace spacer {
26
json_marshal(std::ostream & out,ast * t,ast_manager & m)27 static std::ostream &json_marshal(std::ostream &out, ast *t, ast_manager &m) {
28
29 mk_epp pp = mk_epp(t, m);
30 std::ostringstream ss;
31 ss << pp;
32 out << "\"";
33 for (auto &c:ss.str()) {
34 switch (c) {
35 case '"':
36 out << "\\\"";
37 break;
38 case '\\':
39 out << "\\\\";
40 break;
41 case '\b':
42 out << "\\b";
43 break;
44 case '\f':
45 out << "\\f";
46 break;
47 case '\n':
48 out << "\\n";
49 break;
50 case '\r':
51 out << "\\r";
52 break;
53 case '\t':
54 out << "\\t";
55 break;
56 default:
57 if ('\x00' <= c && c <= '\x1f') {
58 out << "\\u"
59 << std::hex << std::setw(4) << std::setfill('0') << (int) c;
60 } else {
61 out << c;
62 }
63 }
64 }
65 out << "\"";
66 return out;
67 }
68
json_marshal(std::ostream & out,lemma * l)69 static std::ostream &json_marshal(std::ostream &out, lemma *l) {
70 out << "{"
71 << R"("init_level":")" << l->init_level()
72 << R"(", "level":")" << l->level()
73 << R"(", "expr":)";
74 json_marshal(out, l->get_expr(), l->get_ast_manager());
75 out << "}";
76 return out;
77 }
78
json_marshal(std::ostream & out,const lemma_ref_vector & lemmas)79 static std::ostream &json_marshal(std::ostream &out, const lemma_ref_vector &lemmas) {
80
81 std::ostringstream ls;
82 for (auto l:lemmas) {
83 ls << ((unsigned)ls.tellp() == 0 ? "" : ",");
84 json_marshal(ls, l);
85 }
86 out << "[" << ls.str() << "]";
87 return out;
88 }
89
90
register_lemma(lemma * l)91 void json_marshaller::register_lemma(lemma *l) {
92 if (l->has_pob()) {
93 m_relations[&*l->get_pob()][l->get_pob()->depth()].push_back(l);
94 }
95 }
96
register_pob(pob * p)97 void json_marshaller::register_pob(pob *p) {
98 m_relations[p];
99 }
100
marshal_lemmas_old(std::ostream & out) const101 void json_marshaller::marshal_lemmas_old(std::ostream &out) const {
102 unsigned pob_id = 0;
103 for (auto &pob_map:m_relations) {
104 std::ostringstream pob_lemmas;
105 for (auto &depth_lemmas : pob_map.second) {
106 pob_lemmas << ((unsigned)pob_lemmas.tellp() == 0 ? "" : ",")
107 << "\"" << depth_lemmas.first << "\":";
108 json_marshal(pob_lemmas, depth_lemmas.second);
109 }
110 if (pob_lemmas.tellp()) {
111 out << ((unsigned)out.tellp() == 0 ? "" : ",\n");
112 out << "\"" << pob_id << "\":{" << pob_lemmas.str() << "}";
113 }
114 pob_id++;
115 }
116 }
marshal_lemmas_new(std::ostream & out) const117 void json_marshaller::marshal_lemmas_new(std::ostream &out) const {
118 unsigned pob_id = 0;
119 for (auto &pob_map:m_relations) {
120 std::ostringstream pob_lemmas;
121 pob *n = pob_map.first;
122 unsigned i = 0;
123 for (auto *l : n->lemmas()) {
124 pob_lemmas << ((unsigned)pob_lemmas.tellp() == 0 ? "" : ",")
125 << "\"" << i++ << "\":";
126 lemma_ref_vector lemmas_vec;
127 lemmas_vec.push_back(l);
128 json_marshal(pob_lemmas, lemmas_vec);
129 }
130
131 if (pob_lemmas.tellp()) {
132 out << ((unsigned)out.tellp() == 0 ? "" : ",\n");
133 out << "\"" << pob_id << "\":{" << pob_lemmas.str() << "}";
134 }
135 pob_id++;
136 }
137 }
138
marshal(std::ostream & out) const139 std::ostream &json_marshaller::marshal(std::ostream &out) const {
140 std::ostringstream nodes;
141 std::ostringstream edges;
142 std::ostringstream lemmas;
143
144 if (m_old_style)
145 marshal_lemmas_old(lemmas);
146 else
147 marshal_lemmas_new(lemmas);
148
149 unsigned pob_id = 0;
150 unsigned depth = 0;
151 while (true) {
152 double root_expand_time = m_ctx->get_root().get_expand_time(depth);
153 bool a = false;
154 pob_id = 0;
155 for (auto &pob_map:m_relations) {
156 pob *n = pob_map.first;
157 double expand_time = n->get_expand_time(depth);
158 if (expand_time > 0) {
159 a = true;
160 std::ostringstream pob_expr;
161 json_marshal(pob_expr, n->post(), n->get_ast_manager());
162
163 nodes << ((unsigned)nodes.tellp() == 0 ? "" : ",\n") <<
164 "{\"id\":\"" << depth << n <<
165 "\",\"relative_time\":\"" << expand_time / root_expand_time <<
166 "\",\"absolute_time\":\"" << std::setprecision(2) << expand_time <<
167 "\",\"predicate\":\"" << n->pt().head()->get_name() <<
168 "\",\"expr_id\":\"" << n->post()->get_id() <<
169 "\",\"pob_id\":\"" << pob_id <<
170 "\",\"depth\":\"" << depth <<
171 "\",\"expr\":" << pob_expr.str() << "}";
172 if (n->parent()) {
173 edges << ((unsigned)edges.tellp() == 0 ? "" : ",\n") <<
174 "{\"from\":\"" << depth << n->parent() <<
175 "\",\"to\":\"" << depth << n << "\"}";
176 }
177 }
178 pob_id++;
179 }
180 if (!a) {
181 break;
182 }
183 depth++;
184 }
185 out << "{\n\"nodes\":[\n" << nodes.str() << "\n],\n";
186 out << "\"edges\":[\n" << edges.str() << "\n],\n";
187 out << "\"lemmas\":{\n" << lemmas.str() << "\n}\n}\n";
188 return out;
189 }
190
191 }
192