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 "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__SMT__PRINT_BENCHMARK_H |
19 |
|
#define CVC5__SMT__PRINT_BENCHMARK_H |
20 |
|
|
21 |
|
#include <iosfwd> |
22 |
|
#include <vector> |
23 |
|
|
24 |
|
#include "expr/node.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
|
28 |
|
class Printer; |
29 |
|
|
30 |
|
namespace smt { |
31 |
|
|
32 |
|
/** |
33 |
|
* A utility for printing a benchmark. This utility requires no bookkeeping |
34 |
|
* about which commands have been executed. It reconstructs the set of |
35 |
|
* commands that would have been required for generating a benchmark based on |
36 |
|
* a list of nodes. |
37 |
|
*/ |
38 |
|
class PrintBenchmark |
39 |
|
{ |
40 |
|
public: |
41 |
1 |
PrintBenchmark(const Printer* p) : d_printer(p) {} |
42 |
|
/** |
43 |
|
* Print assertions. This prints a parsable set of commands on the output |
44 |
|
* stream out that defines (recursive) functions in defs, and asserts |
45 |
|
* assertions. It does not print a set-logic or check-sat command. |
46 |
|
* |
47 |
|
* Each node in defs is either of the form: |
48 |
|
* (1) (= s t), where s is a (non-recursively) defined function, where |
49 |
|
* the term t may be a lambda if s has non-zero arity. |
50 |
|
* (2) (forall V (= (s V) t)), where s is a recursively defined function. |
51 |
|
*/ |
52 |
|
void printAssertions(std::ostream& out, |
53 |
|
const std::vector<Node>& defs, |
54 |
|
const std::vector<Node>& assertions); |
55 |
|
/** |
56 |
|
* Print assertions, without special handling of defined functions. |
57 |
|
*/ |
58 |
|
void printAssertions(std::ostream& out, const std::vector<Node>& assertions); |
59 |
|
|
60 |
|
/** |
61 |
|
* Print benchmark, which prints a parsable benchmark on the output stream |
62 |
|
* out. It relies on the printAssertions method above, as well as printing |
63 |
|
* the logic based on given string and a final check-sat command. |
64 |
|
* |
65 |
|
* For the best printing, defs should be given in the order in which |
66 |
|
* the symbols were declared. If this is not the case, then we may e.g. |
67 |
|
* group blocks of definitions that were not grouped in the input. |
68 |
|
*/ |
69 |
|
void printBenchmark(std::ostream& out, |
70 |
|
const std::string& logic, |
71 |
|
const std::vector<Node>& defs, |
72 |
|
const std::vector<Node>& assertions); |
73 |
|
|
74 |
|
private: |
75 |
|
/** |
76 |
|
* print declared symbols in funs but not processed; updates processed to |
77 |
|
* include what was printed |
78 |
|
*/ |
79 |
|
void printDeclaredFuns(std::ostream& out, |
80 |
|
const std::unordered_set<Node>& funs, |
81 |
|
std::unordered_set<Node>& processed); |
82 |
|
/** |
83 |
|
* Get the connected types. This traverses subfield types of datatypes and |
84 |
|
* adds to connectedTypes everything that is necessary for printing tn. |
85 |
|
* |
86 |
|
* @param tn The type to traverse |
87 |
|
* @param connectedTypes The types that tn depends on |
88 |
|
* @param process The types we have already processed. We update this set |
89 |
|
* with those added to connectedTypes. |
90 |
|
*/ |
91 |
|
void getConnectedSubfieldTypes(TypeNode tn, |
92 |
|
std::vector<TypeNode>& connectedTypes, |
93 |
|
std::unordered_set<TypeNode>& processed); |
94 |
|
/** |
95 |
|
* Get connected definitions for symbol v. |
96 |
|
* |
97 |
|
* @param recDefs The recursive function definitions that v depends on |
98 |
|
* @param ordinaryDefs The non-recursive definitions that v depends on |
99 |
|
* @param syms The declared symbols that v depends on |
100 |
|
* @param defMap Map from symbols to their definitions |
101 |
|
* @param processedDefs The (recursive or non-recursive) definitions we have |
102 |
|
* processed already. We update this with symbols we add to recDefs and |
103 |
|
* ordinaryDefs. |
104 |
|
* @param visited The set of terms we have already visited when searching for |
105 |
|
* free symbols. This set is updated for the bodies of definitions processed |
106 |
|
* in this call. |
107 |
|
*/ |
108 |
|
void getConnectedDefinitions( |
109 |
|
Node v, |
110 |
|
std::vector<Node>& recDefs, |
111 |
|
std::vector<Node>& ordinaryDefs, |
112 |
|
std::unordered_set<Node>& syms, |
113 |
|
const std::unordered_map<Node, std::pair<bool, Node>>& defMap, |
114 |
|
std::unordered_set<Node>& processedDefs, |
115 |
|
std::unordered_set<TNode>& visited); |
116 |
|
/** |
117 |
|
* Decompose definition assertion a. |
118 |
|
* |
119 |
|
* @param a The definition assertion |
120 |
|
* @param isRecDef Updated to true if a is a recursive function definition (a |
121 |
|
* quantified formula) |
122 |
|
* @param sym Updated to the symbol that a defines |
123 |
|
* @param body Update to the term that defines sym |
124 |
|
* @return true if the definition was successfully inferred |
125 |
|
*/ |
126 |
|
bool decomposeDefinition(Node a, bool& isRecDef, Node& sym, Node& body); |
127 |
|
/** |
128 |
|
* Pointer to the printer we are using, which is responsible for printing |
129 |
|
* individual commands. |
130 |
|
*/ |
131 |
|
const Printer* d_printer; |
132 |
|
}; |
133 |
|
|
134 |
|
} // namespace smt |
135 |
|
} // namespace cvc5 |
136 |
|
|
137 |
|
#endif /* CVC5__SMT__PRINT_BENCHMARK_H */ |