1 |
|
/****************************************************************************** |
2 |
|
* This file is part of the cvc5 project. |
3 |
|
* |
4 |
|
* Copyright (c) 2010-2021 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 |
|
* This header file automatically generated by: |
11 |
|
* |
12 |
|
* ../../../src/theory/mkrewriter /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/rewriter_tables_template.h /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-29/src/theory/quantifiers/kinds |
13 |
|
* |
14 |
|
* for the cvc5 project. |
15 |
|
*/ |
16 |
|
|
17 |
|
/****************************************************************************** |
18 |
|
* Top contributors (to current version): |
19 |
|
* Dejan Jovanovic, Tim King, Andres Noetzli |
20 |
|
* |
21 |
|
* This file is part of the cvc5 project. |
22 |
|
* |
23 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
24 |
|
* in the top-level source directory and their institutional affiliations. |
25 |
|
* All rights reserved. See the file COPYING in the top-level source |
26 |
|
* directory for licensing information. |
27 |
|
* **************************************************************************** |
28 |
|
* |
29 |
|
* Rewriter tables for various theories. |
30 |
|
* |
31 |
|
* This file contains template code for the rewriter tables that are generated |
32 |
|
* from the Theory kinds files. |
33 |
|
*/ |
34 |
|
|
35 |
|
#include "cvc5_private.h" |
36 |
|
|
37 |
|
#pragma once |
38 |
|
|
39 |
|
#include "expr/attribute.h" |
40 |
|
#include "expr/attribute_unique_id.h" |
41 |
|
#include "theory/rewriter.h" |
42 |
|
#include "theory/rewriter_attributes.h" |
43 |
|
|
44 |
|
// clang-format off |
45 |
|
#include "theory/builtin/theory_builtin_rewriter.h" |
46 |
|
#include "theory/booleans/theory_bool_rewriter.h" |
47 |
|
#include "theory/uf/theory_uf_rewriter.h" |
48 |
|
#include "theory/arith/arith_rewriter.h" |
49 |
|
#include "theory/bv/theory_bv_rewriter.h" |
50 |
|
#include "theory/fp/theory_fp_rewriter.h" |
51 |
|
#include "theory/arrays/theory_arrays_rewriter.h" |
52 |
|
#include "theory/datatypes/datatypes_rewriter.h" |
53 |
|
#include "theory/sep/theory_sep_rewriter.h" |
54 |
|
#include "theory/sets/theory_sets_rewriter.h" |
55 |
|
#include "theory/bags/bags_rewriter.h" |
56 |
|
#include "theory/strings/sequences_rewriter.h" |
57 |
|
#include "theory/quantifiers/quantifiers_rewriter.h" |
58 |
|
|
59 |
|
// clang-format on |
60 |
|
|
61 |
|
namespace cvc5 { |
62 |
|
namespace theory { |
63 |
|
|
64 |
27819922 |
Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) |
65 |
|
{ |
66 |
27819922 |
switch (theoryId) |
67 |
|
{ |
68 |
|
// clang-format off |
69 |
5082464 |
case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::getPreRewriteCache(node); |
70 |
10674802 |
case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::getPreRewriteCache(node); |
71 |
669086 |
case THEORY_UF: return RewriteAttibute<THEORY_UF>::getPreRewriteCache(node); |
72 |
5912375 |
case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::getPreRewriteCache(node); |
73 |
3621512 |
case THEORY_BV: return RewriteAttibute<THEORY_BV>::getPreRewriteCache(node); |
74 |
17614 |
case THEORY_FP: return RewriteAttibute<THEORY_FP>::getPreRewriteCache(node); |
75 |
75484 |
case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::getPreRewriteCache(node); |
76 |
496953 |
case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::getPreRewriteCache(node); |
77 |
2022 |
case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::getPreRewriteCache(node); |
78 |
70583 |
case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::getPreRewriteCache(node); |
79 |
5484 |
case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::getPreRewriteCache(node); |
80 |
1047550 |
case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::getPreRewriteCache(node); |
81 |
143993 |
case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::getPreRewriteCache(node); |
82 |
|
|
83 |
|
// clang-format on |
84 |
|
default: Unreachable(); |
85 |
|
} |
86 |
|
} |
87 |
|
|
88 |
73837093 |
Node Rewriter::getPostRewriteCache(theory::TheoryId theoryId, TNode node) |
89 |
|
{ |
90 |
73837093 |
switch (theoryId) |
91 |
|
{ |
92 |
|
// clang-format off |
93 |
5131848 |
case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::getPostRewriteCache(node); |
94 |
30783701 |
case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::getPostRewriteCache(node); |
95 |
7085527 |
case THEORY_UF: return RewriteAttibute<THEORY_UF>::getPostRewriteCache(node); |
96 |
16546332 |
case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::getPostRewriteCache(node); |
97 |
7238621 |
case THEORY_BV: return RewriteAttibute<THEORY_BV>::getPostRewriteCache(node); |
98 |
36822 |
case THEORY_FP: return RewriteAttibute<THEORY_FP>::getPostRewriteCache(node); |
99 |
179270 |
case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::getPostRewriteCache(node); |
100 |
1441131 |
case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::getPostRewriteCache(node); |
101 |
5822 |
case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::getPostRewriteCache(node); |
102 |
261051 |
case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::getPostRewriteCache(node); |
103 |
10198 |
case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::getPostRewriteCache(node); |
104 |
4695230 |
case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::getPostRewriteCache(node); |
105 |
421540 |
case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::getPostRewriteCache(node); |
106 |
|
|
107 |
|
// clang-format on |
108 |
|
default: Unreachable(); |
109 |
|
} |
110 |
|
} |
111 |
|
|
112 |
7799434 |
void Rewriter::setPreRewriteCache(theory::TheoryId theoryId, |
113 |
|
TNode node, |
114 |
|
TNode cache) |
115 |
|
{ |
116 |
7799434 |
switch (theoryId) |
117 |
|
{ |
118 |
|
// clang-format off |
119 |
274566 |
case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::setPreRewriteCache(node, cache); |
120 |
4191286 |
case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::setPreRewriteCache(node, cache); |
121 |
213600 |
case THEORY_UF: return RewriteAttibute<THEORY_UF>::setPreRewriteCache(node, cache); |
122 |
1766595 |
case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::setPreRewriteCache(node, cache); |
123 |
813965 |
case THEORY_BV: return RewriteAttibute<THEORY_BV>::setPreRewriteCache(node, cache); |
124 |
4090 |
case THEORY_FP: return RewriteAttibute<THEORY_FP>::setPreRewriteCache(node, cache); |
125 |
20385 |
case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::setPreRewriteCache(node, cache); |
126 |
169546 |
case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::setPreRewriteCache(node, cache); |
127 |
665 |
case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::setPreRewriteCache(node, cache); |
128 |
27528 |
case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::setPreRewriteCache(node, cache); |
129 |
761 |
case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::setPreRewriteCache(node, cache); |
130 |
253098 |
case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::setPreRewriteCache(node, cache); |
131 |
63349 |
case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::setPreRewriteCache(node, cache); |
132 |
|
|
133 |
|
// clang-format on |
134 |
|
default: Unreachable(); |
135 |
|
} |
136 |
|
} |
137 |
|
|
138 |
7385186 |
void Rewriter::setPostRewriteCache(theory::TheoryId theoryId, |
139 |
|
TNode node, |
140 |
|
TNode cache) |
141 |
|
{ |
142 |
7385186 |
switch (theoryId) |
143 |
|
{ |
144 |
|
// clang-format off |
145 |
275451 |
case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::setPostRewriteCache(node, cache); |
146 |
3922692 |
case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::setPostRewriteCache(node, cache); |
147 |
209210 |
case THEORY_UF: return RewriteAttibute<THEORY_UF>::setPostRewriteCache(node, cache); |
148 |
1783187 |
case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::setPostRewriteCache(node, cache); |
149 |
657226 |
case THEORY_BV: return RewriteAttibute<THEORY_BV>::setPostRewriteCache(node, cache); |
150 |
4008 |
case THEORY_FP: return RewriteAttibute<THEORY_FP>::setPostRewriteCache(node, cache); |
151 |
18783 |
case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::setPostRewriteCache(node, cache); |
152 |
169534 |
case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::setPostRewriteCache(node, cache); |
153 |
665 |
case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::setPostRewriteCache(node, cache); |
154 |
27238 |
case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::setPostRewriteCache(node, cache); |
155 |
758 |
case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::setPostRewriteCache(node, cache); |
156 |
253098 |
case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::setPostRewriteCache(node, cache); |
157 |
63336 |
case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::setPostRewriteCache(node, cache); |
158 |
|
|
159 |
|
// clang-format on |
160 |
|
default: Unreachable(); |
161 |
|
} |
162 |
|
} |
163 |
|
|
164 |
9528 |
Rewriter::Rewriter() : d_tpg(nullptr) {} |
165 |
|
|
166 |
|
void Rewriter::clearCachesInternal() |
167 |
|
{ |
168 |
|
typedef cvc5::expr::attr::AttributeUniqueId AttributeUniqueId; |
169 |
|
std::vector<AttributeUniqueId> preids; |
170 |
|
// clang-format off |
171 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BUILTIN>::pre_rewrite())); |
172 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BOOL>::pre_rewrite())); |
173 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_UF>::pre_rewrite())); |
174 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARITH>::pre_rewrite())); |
175 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BV>::pre_rewrite())); |
176 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_FP>::pre_rewrite())); |
177 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARRAYS>::pre_rewrite())); |
178 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_DATATYPES>::pre_rewrite())); |
179 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SEP>::pre_rewrite())); |
180 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SETS>::pre_rewrite())); |
181 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BAGS>::pre_rewrite())); |
182 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_STRINGS>::pre_rewrite())); |
183 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_QUANTIFIERS>::pre_rewrite())); |
184 |
|
// clang-format on |
185 |
|
|
186 |
|
std::vector<AttributeUniqueId> |
187 |
|
postids; |
188 |
|
// clang-format off |
189 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BUILTIN>::post_rewrite())); |
190 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BOOL>::post_rewrite())); |
191 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_UF>::post_rewrite())); |
192 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARITH>::post_rewrite())); |
193 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BV>::post_rewrite())); |
194 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_FP>::post_rewrite())); |
195 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARRAYS>::post_rewrite())); |
196 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_DATATYPES>::post_rewrite())); |
197 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SEP>::post_rewrite())); |
198 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SETS>::post_rewrite())); |
199 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BAGS>::post_rewrite())); |
200 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_STRINGS>::post_rewrite())); |
201 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_QUANTIFIERS>::post_rewrite())); |
202 |
|
// clang-format on |
203 |
|
|
204 |
|
std::vector<const AttributeUniqueId*> |
205 |
|
allids; |
206 |
|
for (size_t i = 0, size = preids.size(); i < size; ++i) |
207 |
|
{ |
208 |
|
allids.push_back(&preids[i]); |
209 |
|
} |
210 |
|
for (size_t i = 0, size = postids.size(); i < size; ++i) |
211 |
|
{ |
212 |
|
allids.push_back(&postids[i]); |
213 |
|
} |
214 |
|
NodeManager::currentNM()->deleteAttributes(allids); |
215 |
|
} |
216 |
|
|
217 |
|
} // namespace theory |
218 |
|
} // namespace cvc5 |