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