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-08-01/src/theory/rewriter_tables_template.h /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-08-01/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 |
40017191 |
Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) |
65 |
|
{ |
66 |
40017191 |
switch (theoryId) |
67 |
|
{ |
68 |
|
// clang-format off |
69 |
6359627 |
case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::getPreRewriteCache(node); |
70 |
14913931 |
case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::getPreRewriteCache(node); |
71 |
1166159 |
case THEORY_UF: return RewriteAttibute<THEORY_UF>::getPreRewriteCache(node); |
72 |
9782108 |
case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::getPreRewriteCache(node); |
73 |
4807029 |
case THEORY_BV: return RewriteAttibute<THEORY_BV>::getPreRewriteCache(node); |
74 |
20002 |
case THEORY_FP: return RewriteAttibute<THEORY_FP>::getPreRewriteCache(node); |
75 |
100708 |
case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::getPreRewriteCache(node); |
76 |
832863 |
case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::getPreRewriteCache(node); |
77 |
5090 |
case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::getPreRewriteCache(node); |
78 |
143719 |
case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::getPreRewriteCache(node); |
79 |
7493 |
case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::getPreRewriteCache(node); |
80 |
1581317 |
case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::getPreRewriteCache(node); |
81 |
297145 |
case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::getPreRewriteCache(node); |
82 |
|
|
83 |
|
// clang-format on |
84 |
|
default: Unreachable(); |
85 |
|
} |
86 |
|
} |
87 |
|
|
88 |
106970486 |
Node Rewriter::getPostRewriteCache(theory::TheoryId theoryId, TNode node) |
89 |
|
{ |
90 |
106970486 |
switch (theoryId) |
91 |
|
{ |
92 |
|
// clang-format off |
93 |
6434600 |
case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::getPostRewriteCache(node); |
94 |
44818666 |
case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::getPostRewriteCache(node); |
95 |
8584486 |
case THEORY_UF: return RewriteAttibute<THEORY_UF>::getPostRewriteCache(node); |
96 |
27256823 |
case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::getPostRewriteCache(node); |
97 |
9665179 |
case THEORY_BV: return RewriteAttibute<THEORY_BV>::getPostRewriteCache(node); |
98 |
41446 |
case THEORY_FP: return RewriteAttibute<THEORY_FP>::getPostRewriteCache(node); |
99 |
255198 |
case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::getPostRewriteCache(node); |
100 |
3038973 |
case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::getPostRewriteCache(node); |
101 |
14334 |
case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::getPostRewriteCache(node); |
102 |
536854 |
case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::getPostRewriteCache(node); |
103 |
14535 |
case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::getPostRewriteCache(node); |
104 |
5424959 |
case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::getPostRewriteCache(node); |
105 |
884433 |
case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::getPostRewriteCache(node); |
106 |
|
|
107 |
|
// clang-format on |
108 |
|
default: Unreachable(); |
109 |
|
} |
110 |
|
} |
111 |
|
|
112 |
12196935 |
void Rewriter::setPreRewriteCache(theory::TheoryId theoryId, |
113 |
|
TNode node, |
114 |
|
TNode cache) |
115 |
|
{ |
116 |
12196935 |
switch (theoryId) |
117 |
|
{ |
118 |
|
// clang-format off |
119 |
405059 |
case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::setPreRewriteCache(node, cache); |
120 |
6204804 |
case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::setPreRewriteCache(node, cache); |
121 |
420411 |
case THEORY_UF: return RewriteAttibute<THEORY_UF>::setPreRewriteCache(node, cache); |
122 |
3150204 |
case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::setPreRewriteCache(node, cache); |
123 |
1174097 |
case THEORY_BV: return RewriteAttibute<THEORY_BV>::setPreRewriteCache(node, cache); |
124 |
4808 |
case THEORY_FP: return RewriteAttibute<THEORY_FP>::setPreRewriteCache(node, cache); |
125 |
31278 |
case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::setPreRewriteCache(node, cache); |
126 |
298775 |
case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::setPreRewriteCache(node, cache); |
127 |
1757 |
case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::setPreRewriteCache(node, cache); |
128 |
53710 |
case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::setPreRewriteCache(node, cache); |
129 |
1082 |
case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::setPreRewriteCache(node, cache); |
130 |
317726 |
case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::setPreRewriteCache(node, cache); |
131 |
133224 |
case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::setPreRewriteCache(node, cache); |
132 |
|
|
133 |
|
// clang-format on |
134 |
|
default: Unreachable(); |
135 |
|
} |
136 |
|
} |
137 |
|
|
138 |
11422204 |
void Rewriter::setPostRewriteCache(theory::TheoryId theoryId, |
139 |
|
TNode node, |
140 |
|
TNode cache) |
141 |
|
{ |
142 |
11422204 |
switch (theoryId) |
143 |
|
{ |
144 |
|
// clang-format off |
145 |
407269 |
case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::setPostRewriteCache(node, cache); |
146 |
5679284 |
case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::setPostRewriteCache(node, cache); |
147 |
415151 |
case THEORY_UF: return RewriteAttibute<THEORY_UF>::setPostRewriteCache(node, cache); |
148 |
3179358 |
case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::setPostRewriteCache(node, cache); |
149 |
901909 |
case THEORY_BV: return RewriteAttibute<THEORY_BV>::setPostRewriteCache(node, cache); |
150 |
4779 |
case THEORY_FP: return RewriteAttibute<THEORY_FP>::setPostRewriteCache(node, cache); |
151 |
29055 |
case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::setPostRewriteCache(node, cache); |
152 |
298698 |
case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::setPostRewriteCache(node, cache); |
153 |
1757 |
case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::setPostRewriteCache(node, cache); |
154 |
52962 |
case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::setPostRewriteCache(node, cache); |
155 |
1068 |
case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::setPostRewriteCache(node, cache); |
156 |
317726 |
case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::setPostRewriteCache(node, cache); |
157 |
133188 |
case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::setPostRewriteCache(node, cache); |
158 |
|
|
159 |
|
// clang-format on |
160 |
|
default: Unreachable(); |
161 |
|
} |
162 |
|
} |
163 |
|
|
164 |
10481 |
Rewriter::Rewriter() : d_tpg(nullptr) |
165 |
|
{ |
166 |
3427287 |
for (size_t i = 0; i < kind::LAST_KIND; ++i) |
167 |
|
{ |
168 |
3416806 |
d_preRewriters[i] = nullptr; |
169 |
3416806 |
d_postRewriters[i] = nullptr; |
170 |
|
} |
171 |
|
|
172 |
146734 |
for (size_t i = 0; i < theory::THEORY_LAST; ++i) |
173 |
|
{ |
174 |
136253 |
d_preRewritersEqual[i] = nullptr; |
175 |
136253 |
d_postRewritersEqual[i] = nullptr; |
176 |
|
} |
177 |
10481 |
} |
178 |
|
|
179 |
|
void Rewriter::clearCachesInternal() |
180 |
|
{ |
181 |
|
typedef cvc5::expr::attr::AttributeUniqueId AttributeUniqueId; |
182 |
|
std::vector<AttributeUniqueId> preids; |
183 |
|
// clang-format off |
184 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BUILTIN>::pre_rewrite())); |
185 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BOOL>::pre_rewrite())); |
186 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_UF>::pre_rewrite())); |
187 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARITH>::pre_rewrite())); |
188 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BV>::pre_rewrite())); |
189 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_FP>::pre_rewrite())); |
190 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARRAYS>::pre_rewrite())); |
191 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_DATATYPES>::pre_rewrite())); |
192 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SEP>::pre_rewrite())); |
193 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SETS>::pre_rewrite())); |
194 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BAGS>::pre_rewrite())); |
195 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_STRINGS>::pre_rewrite())); |
196 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_QUANTIFIERS>::pre_rewrite())); |
197 |
|
// clang-format on |
198 |
|
|
199 |
|
std::vector<AttributeUniqueId> |
200 |
|
postids; |
201 |
|
// clang-format off |
202 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BUILTIN>::post_rewrite())); |
203 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BOOL>::post_rewrite())); |
204 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_UF>::post_rewrite())); |
205 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARITH>::post_rewrite())); |
206 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BV>::post_rewrite())); |
207 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_FP>::post_rewrite())); |
208 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARRAYS>::post_rewrite())); |
209 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_DATATYPES>::post_rewrite())); |
210 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SEP>::post_rewrite())); |
211 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SETS>::post_rewrite())); |
212 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BAGS>::post_rewrite())); |
213 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_STRINGS>::post_rewrite())); |
214 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_QUANTIFIERS>::post_rewrite())); |
215 |
|
// clang-format on |
216 |
|
|
217 |
|
std::vector<const AttributeUniqueId*> |
218 |
|
allids; |
219 |
|
for (size_t i = 0, size = preids.size(); i < size; ++i) |
220 |
|
{ |
221 |
|
allids.push_back(&preids[i]); |
222 |
|
} |
223 |
|
for (size_t i = 0, size = postids.size(); i < size; ++i) |
224 |
|
{ |
225 |
|
allids.push_back(&postids[i]); |
226 |
|
} |
227 |
|
NodeManager::currentNM()->deleteAttributes(allids); |
228 |
|
} |
229 |
|
|
230 |
|
} // namespace theory |
231 |
|
} // namespace cvc5 |