Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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/attribute.h"
19 : : #include "expr/dtype.h"
20 : : #include "expr/node_algorithm.h"
21 : : #include "expr/node_converter.h"
22 : : #include "printer/printer.h"
23 : : #include "expr/skolem_manager.h"
24 : :
25 : : using namespace cvc5::internal::kind;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace smt {
29 : :
30 : : /**
31 : : * Attribute true for symbols that should be excluded from the output of this
32 : : * utility.
33 : : */
34 : : struct BenchmarkNoPrintAttributeId
35 : : {
36 : : };
37 : : using BenchmarkNoPrintAttribute =
38 : : expr::Attribute<BenchmarkNoPrintAttributeId, bool>;
39 : :
40 : 1628 : void PrintBenchmark::printDeclarationsFrom(std::ostream& outDecl,
41 : : std::ostream& outDef,
42 : : const std::vector<Node>& defs,
43 : : const std::vector<Node>& terms)
44 : : {
45 : 3256 : std::unordered_set<TypeNode> unorderedTypes;
46 : 3256 : std::unordered_set<TNode> typeVisited;
47 [ + + ]: 2033 : for (const Node& a : defs)
48 : : {
49 : 405 : expr::getTypes(a, unorderedTypes, typeVisited);
50 : : }
51 [ + + ]: 17631 : for (const Node& a : terms)
52 : : {
53 : 16003 : expr::getTypes(a, unorderedTypes, typeVisited);
54 : : }
55 : 3256 : std::vector<TypeNode> types{unorderedTypes.begin(), unorderedTypes.end()};
56 [ + + ]: 1628 : if (d_sorted)
57 : : {
58 : : // We want to print declarations in a deterministic order, independent of
59 : : // the implementation of data structures. Hence, we insert into a vector
60 : : // and reorder. Note that collecting the types in an std::unordered_map,
61 : : // then inserting them into a vector and sorting the vector is faster than
62 : : // immediately using an std::set instead.
63 : 15 : std::sort(types.begin(), types.end());
64 : : }
65 : : // print the declared types first
66 : 3256 : std::unordered_set<TypeNode> alreadyPrintedDeclSorts;
67 [ + + ]: 8114 : for (const TypeNode& st : types)
68 : : {
69 : : // note that we must get all "component types" of a type, so that
70 : : // e.g. U is printed as a sort declaration when we have type (Array U Int).
71 : : // get all connected datatypes to this one
72 : 12972 : std::vector<TypeNode> connectedTypes;
73 : 6486 : getConnectedSubfieldTypes(st, connectedTypes, alreadyPrintedDeclSorts);
74 : : // now, separate into sorts and datatypes
75 : 12972 : std::vector<TypeNode> datatypeBlock;
76 [ + + ]: 13028 : for (const TypeNode& ctn : connectedTypes)
77 : : {
78 [ + + ]: 7819 : if ((ctn.isUninterpretedSort() && ctn.getNumChildren() == 0)
79 [ + + ][ + + ]: 7819 : || ctn.isUninterpretedSortConstructor())
[ + + ]
80 : : {
81 : 2554 : TypeNode ctnp = ctn;
82 [ + - ]: 1277 : if (d_converter != nullptr)
83 : : {
84 : 1277 : ctnp = d_converter->convertType(ctnp);
85 : : }
86 : 1277 : d_printer->toStreamCmdDeclareType(outDecl, ctn);
87 : 1277 : outDecl << std::endl;
88 : : }
89 [ + + ][ + + ]: 5265 : else if (ctn.isDatatype() && !ctn.isTuple() && !ctn.isNullable())
[ + + ][ + + ]
90 : : {
91 : 236 : datatypeBlock.push_back(ctn);
92 : : }
93 : : }
94 : : // print the mutually recursive datatype block if necessary
95 [ + + ]: 6486 : if (!datatypeBlock.empty())
96 : : {
97 : 184 : d_printer->toStreamCmdDatatypeDeclaration(outDecl, datatypeBlock);
98 : 184 : outDecl << std::endl;
99 : : }
100 : : }
101 : :
102 : : // global visited cache for expr::getSymbols calls
103 : 3256 : std::unordered_set<TNode> visited;
104 : :
105 : : // print the definitions
106 : 3256 : std::unordered_map<Node, std::pair<bool, Node>> defMap;
107 : 3256 : std::vector<Node> defSyms;
108 : : // first, record all the defined symbols
109 [ + + ]: 2033 : for (const Node& a : defs)
110 : : {
111 : 405 : bool isRec = false;
112 : 405 : Node defSym;
113 : 405 : Node defBody;
114 [ - + ]: 405 : if (!decomposeDefinition(a, isRec, defSym, defBody))
115 : : {
116 : 0 : continue;
117 : : }
118 [ + - ]: 405 : if (!defSym.isNull())
119 : : {
120 [ - + ][ - + ]: 405 : Assert(defMap.find(defSym) == defMap.end());
[ - - ]
121 : 405 : defMap[defSym] = std::pair<bool, Node>(isRec, defBody);
122 : 405 : defSyms.push_back(defSym);
123 : : }
124 : : }
125 : : // go back and print the definitions
126 : 3256 : std::unordered_set<Node> alreadyPrintedDecl;
127 : 3256 : std::unordered_set<Node> alreadyPrintedDef;
128 : :
129 : 1628 : std::unordered_map<Node, std::pair<bool, Node>>::const_iterator itd;
130 [ + + ]: 2033 : for (const Node& s : defSyms)
131 : : {
132 : 810 : std::vector<Node> recDefs;
133 : 810 : std::vector<Node> ordinaryDefs;
134 : 810 : std::unordered_set<Node> unorderedSyms;
135 : 405 : getConnectedDefinitions(s,
136 : : recDefs,
137 : : ordinaryDefs,
138 : : unorderedSyms,
139 : : defMap,
140 : : alreadyPrintedDef,
141 : : visited);
142 : 810 : std::vector<Node> syms{unorderedSyms.begin(), unorderedSyms.end()};
143 [ + + ]: 405 : if (d_sorted)
144 : : {
145 : : // We want to print declarations in a deterministic order, independent of
146 : : // the implementation of data structures. Hence, we insert into a vector
147 : : // and reorder. Note that collecting `syms` in an std::unordered_map,
148 : : // then inserting them into a vector and sorting the vector is faster than
149 : : // immediately using an std::set instead.
150 : 6 : std::sort(syms.begin(), syms.end());
151 : : }
152 : : // print the declarations that are encountered for the first time in this
153 : : // block
154 : 405 : printDeclaredFuns(outDecl, syms, alreadyPrintedDecl);
155 [ + + ]: 405 : if (d_sorted)
156 : : {
157 : : // Sort recursive definitions for deterministic order.
158 : 6 : std::sort(recDefs.begin(), recDefs.end());
159 : : // In general, we cannot sort the ordinary definitions since they were
160 : : // added to the vector in an order which ensures the functions they
161 : : // depend on are defined first.
162 : : }
163 : : // print the ordinary definitions
164 [ + + ]: 810 : for (const Node& f : ordinaryDefs)
165 : : {
166 : 405 : itd = defMap.find(f);
167 [ - + ][ - + ]: 405 : Assert(itd != defMap.end());
[ - - ]
168 [ - + ][ - + ]: 405 : Assert(!itd->second.first);
[ - - ]
169 : 810 : Node def = itd->second.second;
170 [ + + ]: 405 : if (d_converter != nullptr)
171 : : {
172 : 399 : def = d_converter->convert(def);
173 : : }
174 : 405 : d_printer->toStreamCmdDefineFunction(outDef, f, def);
175 : 405 : outDef << std::endl;
176 : : // a definition is also a declaration
177 : 405 : alreadyPrintedDecl.insert(f);
178 : : }
179 : : // print a recursive function definition block
180 [ - + ]: 405 : if (!recDefs.empty())
181 : : {
182 : 0 : std::vector<Node> lambdas;
183 [ - - ]: 0 : for (const Node& f : recDefs)
184 : : {
185 : 0 : Node lam = defMap[f].second;
186 [ - - ]: 0 : if (d_converter != nullptr)
187 : : {
188 : 0 : lam = d_converter->convert(lam);
189 : : }
190 : 0 : lambdas.push_back(lam);
191 : : // a recursive definition is also a declaration
192 : 0 : alreadyPrintedDecl.insert(f);
193 : : }
194 : 0 : d_printer->toStreamCmdDefineFunctionRec(outDef, recDefs, lambdas);
195 : 0 : outDef << std::endl;
196 : : }
197 : : }
198 : :
199 : : // print the remaining declared symbols
200 : 3256 : std::unordered_set<Node> unorderedSyms;
201 [ + + ]: 17631 : for (const Node& a : terms)
202 : : {
203 : 16003 : expr::getSymbols(a, unorderedSyms, visited);
204 : : }
205 : 3256 : std::vector<Node> syms{unorderedSyms.begin(), unorderedSyms.end()};
206 [ + + ]: 1628 : if (d_sorted)
207 : : {
208 : : // We want to print declarations in a deterministic order, independent of
209 : : // the implementation of data structures. Hence, we insert into a vector
210 : : // and reorder. Note that collecting `syms` in an std::unordered_map,
211 : : // then inserting them into a vector and sorting the vector is faster than
212 : : // immediately using an std::set instead.
213 : 15 : std::sort(syms.begin(), syms.end());
214 : : }
215 : 1628 : printDeclaredFuns(outDecl, syms, alreadyPrintedDecl);
216 : 1628 : }
217 : :
218 : 15 : void PrintBenchmark::printAssertions(std::ostream& out,
219 : : const std::vector<Node>& defs,
220 : : const std::vector<Node>& assertions)
221 : : {
222 : 15 : printDeclarationsFrom(out, out, defs, assertions);
223 : : // print the assertions
224 [ + + ]: 38 : for (const Node& a : assertions)
225 : : {
226 : 46 : Node ap = a;
227 [ - + ]: 23 : if (d_converter != nullptr)
228 : : {
229 : 0 : ap = d_converter->convert(ap);
230 : : }
231 : 23 : d_printer->toStreamCmdAssert(out, ap);
232 : 23 : out << std::endl;
233 : : }
234 : 15 : }
235 : :
236 : 0 : void PrintBenchmark::printAssertions(std::ostream& out,
237 : : const std::vector<Node>& assertions)
238 : : {
239 : 0 : std::vector<Node> defs;
240 : 0 : printAssertions(out, defs, assertions);
241 : 0 : }
242 : :
243 : 2033 : void PrintBenchmark::printDeclaredFuns(std::ostream& out,
244 : : const std::vector<Node>& funs,
245 : : std::unordered_set<Node>& alreadyPrinted)
246 : : {
247 : 2033 : bool printSkolemDefs = options::ioutils::getPrintSkolemDefinitions(out);
248 : 2033 : SkolemManager* sm = d_nm->getSkolemManager();
249 : : BenchmarkNoPrintAttribute bnpa;
250 [ + + ]: 18274 : for (const Node& f : funs)
251 : : {
252 [ - + ][ - + ]: 16241 : Assert(f.isVar());
[ - - ]
253 : : // do not print selectors, constructors
254 [ + + ]: 16241 : if (!f.getType().isFirstClass())
255 : : {
256 : 541 : continue;
257 : : }
258 : : // don't print symbols that have been marked
259 [ + + ]: 15700 : if (f.getAttribute(bnpa))
260 : : {
261 : 12 : continue;
262 : : }
263 : : // if print skolem definitions is true, we shouldn't print declarations for
264 : : // (exported) skolems, as they are printed as parsable terms.
265 [ + + ][ + + ]: 15688 : if (printSkolemDefs && f.getKind() == Kind::SKOLEM)
[ + + ]
266 : : {
267 [ + - ]: 1 : if (sm->getId(f)!= SkolemId::INTERNAL)
268 : : {
269 : 1 : continue;
270 : : }
271 : : }
272 [ + + ]: 15687 : if (alreadyPrinted.find(f) == alreadyPrinted.end())
273 : : {
274 : 15596 : d_printer->toStreamCmdDeclareFunction(out, f);
275 : 15596 : out << std::endl;
276 : : }
277 : : }
278 : 2033 : alreadyPrinted.insert(funs.begin(), funs.end());
279 : 2033 : }
280 : :
281 : 8821 : void PrintBenchmark::getConnectedSubfieldTypes(
282 : : TypeNode tn,
283 : : std::vector<TypeNode>& connectedTypes,
284 : : std::unordered_set<TypeNode>& processed)
285 : : {
286 [ + + ]: 8821 : if (processed.find(tn) != processed.end())
287 : : {
288 : 2272 : return;
289 : : }
290 : 6549 : processed.insert(tn);
291 [ + + ]: 6549 : if (tn.isParametricDatatype())
292 : : {
293 : 7 : const DType& dt = tn.getDType();
294 : : // ignore its parameters
295 [ + + ]: 16 : for (size_t i = 0, nparams = dt.getNumParameters(); i < nparams; i++)
296 : : {
297 : 9 : processed.insert(dt.getParameter(i));
298 : : }
299 : : // we do not process the datatype here, instead we will traverse to the
300 : : // head of the parameteric datatype (tn[0]), which will subsequently
301 : : // process its subfield types.
302 : : }
303 : : else
304 : : {
305 : 6542 : connectedTypes.push_back(tn);
306 [ + + ]: 6542 : if (tn.isDatatype())
307 : : {
308 : : std::unordered_set<TypeNode> subfieldTypes =
309 : 656 : tn.getDType().getSubfieldTypes();
310 [ + + ]: 742 : for (const TypeNode& ctn : subfieldTypes)
311 : : {
312 : 414 : getConnectedSubfieldTypes(ctn, connectedTypes, processed);
313 : : }
314 : : }
315 : : }
316 [ + + ]: 8470 : for (unsigned i = 0, nchild = tn.getNumChildren(); i < nchild; i++)
317 : : {
318 : 1921 : getConnectedSubfieldTypes(tn[i], connectedTypes, processed);
319 : : }
320 : : }
321 : :
322 : 792 : void PrintBenchmark::getConnectedDefinitions(
323 : : Node n,
324 : : std::vector<Node>& recDefs,
325 : : std::vector<Node>& ordinaryDefs,
326 : : std::unordered_set<Node>& syms,
327 : : const std::unordered_map<Node, std::pair<bool, Node>>& defMap,
328 : : std::unordered_set<Node>& processedDefs,
329 : : std::unordered_set<TNode>& visited)
330 : : {
331 : : // does it have a definition?
332 : : std::unordered_map<Node, std::pair<bool, Node>>::const_iterator it =
333 : 792 : defMap.find(n);
334 [ + + ]: 792 : if (it == defMap.end())
335 : : {
336 : : // an ordinary declared symbol
337 : 238 : syms.insert(n);
338 : 387 : return;
339 : : }
340 [ + + ]: 554 : if (processedDefs.find(n) != processedDefs.end())
341 : : {
342 : 149 : return;
343 : : }
344 : 405 : processedDefs.insert(n);
345 : : // get the symbols in the body
346 : 810 : std::unordered_set<Node> symsBody;
347 : 405 : expr::getSymbols(it->second.second, symsBody, visited);
348 [ + + ]: 792 : for (const Node& s : symsBody)
349 : : {
350 : 387 : getConnectedDefinitions(
351 : : s, recDefs, ordinaryDefs, syms, defMap, processedDefs, visited);
352 : : }
353 : : // add the symbol after we add the definitions
354 [ + - ]: 405 : if (!it->second.first)
355 : : {
356 : : // an ordinary define-fun symbol
357 : 405 : ordinaryDefs.push_back(n);
358 : : }
359 : : else
360 : : {
361 : : // a recursively defined symbol
362 : 0 : recDefs.push_back(n);
363 : : }
364 : : }
365 : :
366 : 405 : bool PrintBenchmark::decomposeDefinition(Node a,
367 : : bool& isRecDef,
368 : : Node& sym,
369 : : Node& body)
370 : : {
371 [ + - ][ + - ]: 405 : if (a.getKind() == Kind::EQUAL && a[0].isVar())
[ + - ][ + - ]
[ - - ]
372 : : {
373 : : // an ordinary define-fun
374 : 405 : isRecDef = false;
375 : 405 : sym = a[0];
376 : 405 : body = a[1];
377 : 405 : return true;
378 : : }
379 : 0 : else if (a.getKind() == Kind::FORALL && a[1].getKind() == Kind::EQUAL
380 : 0 : && a[1][0].getKind() == Kind::APPLY_UF)
381 : : {
382 : 0 : isRecDef = true;
383 : 0 : sym = a[1][0].getOperator();
384 : 0 : body = NodeManager::currentNM()->mkNode(Kind::LAMBDA, a[0], a[1][1]);
385 : 0 : return true;
386 : : }
387 : : else
388 : : {
389 [ - - ]: 0 : Warning() << "Unhandled definition: " << a << std::endl;
390 : : }
391 : 0 : return false;
392 : : }
393 : :
394 : 15 : void PrintBenchmark::printBenchmark(std::ostream& out,
395 : : const std::string& logic,
396 : : const std::vector<Node>& defs,
397 : : const std::vector<Node>& assertions)
398 : : {
399 : 15 : d_printer->toStreamCmdSetBenchmarkLogic(out, logic);
400 : 15 : out << std::endl;
401 : 15 : printAssertions(out, defs, assertions);
402 : 15 : d_printer->toStreamCmdCheckSat(out);
403 : 15 : out << std::endl;
404 : 15 : }
405 : :
406 : 2575 : void PrintBenchmark::markNoPrint(Node& sym)
407 : : {
408 : : BenchmarkNoPrintAttribute bnpa;
409 : 2575 : sym.setAttribute(bnpa, true);
410 : 2575 : }
411 : :
412 : : } // namespace smt
413 : : } // namespace cvc5::internal
|
