1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
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 |
|
* Print benchmark utility. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "smt/print_benchmark.h" |
17 |
|
|
18 |
|
#include "expr/dtype.h" |
19 |
|
#include "expr/node_algorithm.h" |
20 |
|
#include "printer/printer.h" |
21 |
|
|
22 |
|
using namespace cvc5::kind; |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace smt { |
26 |
|
|
27 |
1 |
void PrintBenchmark::printAssertions(std::ostream& out, |
28 |
|
const std::vector<Node>& defs, |
29 |
|
const std::vector<Node>& assertions) |
30 |
|
{ |
31 |
2 |
std::unordered_set<TypeNode> types; |
32 |
2 |
std::unordered_set<TNode> typeVisited; |
33 |
1 |
for (const Node& a : defs) |
34 |
|
{ |
35 |
|
expr::getTypes(a, types, typeVisited); |
36 |
|
} |
37 |
5 |
for (const Node& a : assertions) |
38 |
|
{ |
39 |
4 |
expr::getTypes(a, types, typeVisited); |
40 |
|
} |
41 |
|
// print the declared types first |
42 |
2 |
std::unordered_set<TypeNode> alreadyPrintedDeclSorts; |
43 |
3 |
for (const TypeNode& st : types) |
44 |
|
{ |
45 |
|
// note that we must get all "component types" of a type, so that |
46 |
|
// e.g. U is printed as a sort declaration when we have type (Array U Int). |
47 |
4 |
std::unordered_set<TypeNode> ctypes; |
48 |
2 |
expr::getComponentTypes(st, ctypes); |
49 |
4 |
for (const TypeNode& stc : ctypes) |
50 |
|
{ |
51 |
|
// get all connected datatypes to this one |
52 |
4 |
std::vector<TypeNode> connectedTypes; |
53 |
2 |
getConnectedSubfieldTypes(stc, connectedTypes, alreadyPrintedDeclSorts); |
54 |
|
// now, separate into sorts and datatypes |
55 |
4 |
std::vector<TypeNode> datatypeBlock; |
56 |
2 |
for (const TypeNode& ctn : connectedTypes) |
57 |
|
{ |
58 |
|
if (stc.isSort()) |
59 |
|
{ |
60 |
|
d_printer->toStreamCmdDeclareType(out, stc); |
61 |
|
} |
62 |
|
else if (stc.isDatatype()) |
63 |
|
{ |
64 |
|
datatypeBlock.push_back(ctn); |
65 |
|
} |
66 |
|
} |
67 |
|
// print the mutually recursive datatype block if necessary |
68 |
2 |
if (!datatypeBlock.empty()) |
69 |
|
{ |
70 |
|
d_printer->toStreamCmdDatatypeDeclaration(out, datatypeBlock); |
71 |
|
} |
72 |
|
} |
73 |
|
} |
74 |
|
|
75 |
|
// global visited cache for expr::getSymbols calls |
76 |
2 |
std::unordered_set<TNode> visited; |
77 |
|
|
78 |
|
// print the definitions |
79 |
2 |
std::unordered_map<Node, std::pair<bool, Node>> defMap; |
80 |
2 |
std::vector<Node> defSyms; |
81 |
|
// first, record all the defined symbols |
82 |
1 |
for (const Node& a : defs) |
83 |
|
{ |
84 |
|
bool isRec; |
85 |
|
Node defSym; |
86 |
|
Node defBody; |
87 |
|
decomposeDefinition(a, isRec, defSym, defBody); |
88 |
|
if (!defSym.isNull()) |
89 |
|
{ |
90 |
|
Assert(defMap.find(defSym) == defMap.end()); |
91 |
|
defMap[defSym] = std::pair<bool, Node>(isRec, defBody); |
92 |
|
defSyms.push_back(defSym); |
93 |
|
} |
94 |
|
} |
95 |
|
// go back and print the definitions |
96 |
2 |
std::unordered_set<Node> alreadyPrintedDecl; |
97 |
2 |
std::unordered_set<Node> alreadyPrintedDef; |
98 |
|
|
99 |
1 |
std::unordered_map<Node, std::pair<bool, Node>>::const_iterator itd; |
100 |
1 |
for (const Node& s : defSyms) |
101 |
|
{ |
102 |
|
std::vector<Node> recDefs; |
103 |
|
std::vector<Node> ordinaryDefs; |
104 |
|
std::unordered_set<Node> syms; |
105 |
|
getConnectedDefinitions( |
106 |
|
s, recDefs, ordinaryDefs, syms, defMap, alreadyPrintedDef, visited); |
107 |
|
// print the declarations that are encountered for the first time in this |
108 |
|
// block |
109 |
|
printDeclaredFuns(out, syms, alreadyPrintedDecl); |
110 |
|
// print the ordinary definitions |
111 |
|
for (const Node& f : ordinaryDefs) |
112 |
|
{ |
113 |
|
itd = defMap.find(f); |
114 |
|
Assert(itd != defMap.end()); |
115 |
|
Assert(!itd->second.first); |
116 |
|
d_printer->toStreamCmdDefineFunction(out, f, itd->second.second); |
117 |
|
// a definition is also a declaration |
118 |
|
alreadyPrintedDecl.insert(f); |
119 |
|
} |
120 |
|
// print a recursive function definition block |
121 |
|
if (!recDefs.empty()) |
122 |
|
{ |
123 |
|
std::vector<Node> lambdas; |
124 |
|
for (const Node& f : recDefs) |
125 |
|
{ |
126 |
|
lambdas.push_back(defMap[f].second); |
127 |
|
// a recursive definition is also a declaration |
128 |
|
alreadyPrintedDecl.insert(f); |
129 |
|
} |
130 |
|
d_printer->toStreamCmdDefineFunctionRec(out, recDefs, lambdas); |
131 |
|
} |
132 |
|
} |
133 |
|
|
134 |
|
// print the remaining declared symbols |
135 |
2 |
std::unordered_set<Node> syms; |
136 |
5 |
for (const Node& a : assertions) |
137 |
|
{ |
138 |
4 |
expr::getSymbols(a, syms, visited); |
139 |
|
} |
140 |
1 |
printDeclaredFuns(out, syms, alreadyPrintedDecl); |
141 |
|
|
142 |
|
// print the assertions |
143 |
5 |
for (const Node& a : assertions) |
144 |
|
{ |
145 |
4 |
d_printer->toStreamCmdAssert(out, a); |
146 |
|
} |
147 |
1 |
} |
148 |
|
void PrintBenchmark::printAssertions(std::ostream& out, |
149 |
|
const std::vector<Node>& assertions) |
150 |
|
{ |
151 |
|
std::vector<Node> defs; |
152 |
|
printAssertions(out, defs, assertions); |
153 |
|
} |
154 |
|
|
155 |
1 |
void PrintBenchmark::printDeclaredFuns(std::ostream& out, |
156 |
|
const std::unordered_set<Node>& funs, |
157 |
|
std::unordered_set<Node>& alreadyPrinted) |
158 |
|
{ |
159 |
3 |
for (const Node& f : funs) |
160 |
|
{ |
161 |
2 |
Assert(f.isVar()); |
162 |
|
// do not print selectors, constructors |
163 |
2 |
if (!f.getType().isFirstClass()) |
164 |
|
{ |
165 |
|
continue; |
166 |
|
} |
167 |
2 |
if (alreadyPrinted.find(f) == alreadyPrinted.end()) |
168 |
|
{ |
169 |
2 |
d_printer->toStreamCmdDeclareFunction(out, f); |
170 |
|
} |
171 |
|
} |
172 |
1 |
alreadyPrinted.insert(funs.begin(), funs.end()); |
173 |
1 |
} |
174 |
|
|
175 |
2 |
void PrintBenchmark::getConnectedSubfieldTypes( |
176 |
|
TypeNode tn, |
177 |
|
std::vector<TypeNode>& connectedTypes, |
178 |
|
std::unordered_set<TypeNode>& processed) |
179 |
|
{ |
180 |
2 |
if (processed.find(tn) != processed.end()) |
181 |
|
{ |
182 |
|
return; |
183 |
|
} |
184 |
2 |
processed.insert(tn); |
185 |
2 |
if (tn.isSort()) |
186 |
|
{ |
187 |
|
connectedTypes.push_back(tn); |
188 |
|
} |
189 |
2 |
else if (tn.isDatatype()) |
190 |
|
{ |
191 |
|
connectedTypes.push_back(tn); |
192 |
|
std::unordered_set<TypeNode> subfieldTypes = |
193 |
|
tn.getDType().getSubfieldTypes(); |
194 |
|
for (const TypeNode& ctn : subfieldTypes) |
195 |
|
{ |
196 |
|
getConnectedSubfieldTypes(ctn, connectedTypes, processed); |
197 |
|
} |
198 |
|
} |
199 |
|
} |
200 |
|
|
201 |
|
void PrintBenchmark::getConnectedDefinitions( |
202 |
|
Node n, |
203 |
|
std::vector<Node>& recDefs, |
204 |
|
std::vector<Node>& ordinaryDefs, |
205 |
|
std::unordered_set<Node>& syms, |
206 |
|
const std::unordered_map<Node, std::pair<bool, Node>>& defMap, |
207 |
|
std::unordered_set<Node>& processedDefs, |
208 |
|
std::unordered_set<TNode>& visited) |
209 |
|
{ |
210 |
|
// does it have a definition? |
211 |
|
std::unordered_map<Node, std::pair<bool, Node>>::const_iterator it = |
212 |
|
defMap.find(n); |
213 |
|
if (it == defMap.end()) |
214 |
|
{ |
215 |
|
// an ordinary declared symbol |
216 |
|
syms.insert(n); |
217 |
|
return; |
218 |
|
} |
219 |
|
if (processedDefs.find(n) != processedDefs.end()) |
220 |
|
{ |
221 |
|
return; |
222 |
|
} |
223 |
|
processedDefs.insert(n); |
224 |
|
if (!it->second.first) |
225 |
|
{ |
226 |
|
// an ordinary define-fun symbol |
227 |
|
ordinaryDefs.push_back(n); |
228 |
|
} |
229 |
|
else |
230 |
|
{ |
231 |
|
// a recursively defined symbol |
232 |
|
recDefs.push_back(n); |
233 |
|
// get the symbols in the body |
234 |
|
std::unordered_set<Node> symsBody; |
235 |
|
expr::getSymbols(it->second.second, symsBody, visited); |
236 |
|
for (const Node& s : symsBody) |
237 |
|
{ |
238 |
|
getConnectedDefinitions( |
239 |
|
s, recDefs, ordinaryDefs, syms, defMap, processedDefs, visited); |
240 |
|
} |
241 |
|
} |
242 |
|
} |
243 |
|
|
244 |
|
bool PrintBenchmark::decomposeDefinition(Node a, |
245 |
|
bool& isRecDef, |
246 |
|
Node& sym, |
247 |
|
Node& body) |
248 |
|
{ |
249 |
|
if (a.getKind() == EQUAL && a[0].isVar()) |
250 |
|
{ |
251 |
|
// an ordinary define-fun |
252 |
|
isRecDef = false; |
253 |
|
sym = a[0]; |
254 |
|
body = a[1]; |
255 |
|
return true; |
256 |
|
} |
257 |
|
else if (a.getKind() == FORALL && a[1].getKind() == EQUAL |
258 |
|
&& a[1][0].getKind() == APPLY_UF) |
259 |
|
{ |
260 |
|
isRecDef = true; |
261 |
|
sym = a[1][0].getOperator(); |
262 |
|
body = NodeManager::currentNM()->mkNode(LAMBDA, a[0], a[1][1]); |
263 |
|
return true; |
264 |
|
} |
265 |
|
else |
266 |
|
{ |
267 |
|
Warning() << "Unhandled definition: " << a << std::endl; |
268 |
|
} |
269 |
|
return false; |
270 |
|
} |
271 |
|
|
272 |
1 |
void PrintBenchmark::printBenchmark(std::ostream& out, |
273 |
|
const std::string& logic, |
274 |
|
const std::vector<Node>& defs, |
275 |
|
const std::vector<Node>& assertions) |
276 |
|
{ |
277 |
1 |
d_printer->toStreamCmdSetBenchmarkLogic(out, logic); |
278 |
1 |
printAssertions(out, defs, assertions); |
279 |
1 |
d_printer->toStreamCmdCheckSat(out); |
280 |
1 |
} |
281 |
|
|
282 |
|
} // namespace smt |
283 |
31137 |
} // namespace cvc5 |