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-18/src/theory/rewriter_tables_template.h /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-18/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 |
39865592 |
Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) |
65 |
|
{ |
66 |
39865592 |
switch (theoryId) |
67 |
|
{ |
68 |
|
// clang-format off |
69 |
6398910 |
case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::getPreRewriteCache(node); |
70 |
14585623 |
case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::getPreRewriteCache(node); |
71 |
1186090 |
case THEORY_UF: return RewriteAttibute<THEORY_UF>::getPreRewriteCache(node); |
72 |
10235495 |
case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::getPreRewriteCache(node); |
73 |
4668429 |
case THEORY_BV: return RewriteAttibute<THEORY_BV>::getPreRewriteCache(node); |
74 |
20405 |
case THEORY_FP: return RewriteAttibute<THEORY_FP>::getPreRewriteCache(node); |
75 |
106024 |
case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::getPreRewriteCache(node); |
76 |
710778 |
case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::getPreRewriteCache(node); |
77 |
5076 |
case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::getPreRewriteCache(node); |
78 |
142881 |
case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::getPreRewriteCache(node); |
79 |
7763 |
case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::getPreRewriteCache(node); |
80 |
1489916 |
case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::getPreRewriteCache(node); |
81 |
308202 |
case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::getPreRewriteCache(node); |
82 |
|
|
83 |
|
// clang-format on |
84 |
|
default: Unreachable(); |
85 |
|
} |
86 |
|
} |
87 |
|
|
88 |
108784227 |
Node Rewriter::getPostRewriteCache(theory::TheoryId theoryId, TNode node) |
89 |
|
{ |
90 |
108784227 |
switch (theoryId) |
91 |
|
{ |
92 |
|
// clang-format off |
93 |
6472687 |
case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::getPostRewriteCache(node); |
94 |
45316425 |
case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::getPostRewriteCache(node); |
95 |
8615548 |
case THEORY_UF: return RewriteAttibute<THEORY_UF>::getPostRewriteCache(node); |
96 |
28470605 |
case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::getPostRewriteCache(node); |
97 |
9647307 |
case THEORY_BV: return RewriteAttibute<THEORY_BV>::getPostRewriteCache(node); |
98 |
42123 |
case THEORY_FP: return RewriteAttibute<THEORY_FP>::getPostRewriteCache(node); |
99 |
264720 |
case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::getPostRewriteCache(node); |
100 |
2269688 |
case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::getPostRewriteCache(node); |
101 |
14316 |
case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::getPostRewriteCache(node); |
102 |
538293 |
case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::getPostRewriteCache(node); |
103 |
14921 |
case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::getPostRewriteCache(node); |
104 |
6218482 |
case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::getPostRewriteCache(node); |
105 |
899112 |
case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::getPostRewriteCache(node); |
106 |
|
|
107 |
|
// clang-format on |
108 |
|
default: Unreachable(); |
109 |
|
} |
110 |
|
} |
111 |
|
|
112 |
12123139 |
void Rewriter::setPreRewriteCache(theory::TheoryId theoryId, |
113 |
|
TNode node, |
114 |
|
TNode cache) |
115 |
|
{ |
116 |
12123139 |
switch (theoryId) |
117 |
|
{ |
118 |
|
// clang-format off |
119 |
417327 |
case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::setPreRewriteCache(node, cache); |
120 |
6106503 |
case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::setPreRewriteCache(node, cache); |
121 |
423973 |
case THEORY_UF: return RewriteAttibute<THEORY_UF>::setPreRewriteCache(node, cache); |
122 |
3188422 |
case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::setPreRewriteCache(node, cache); |
123 |
1136285 |
case THEORY_BV: return RewriteAttibute<THEORY_BV>::setPreRewriteCache(node, cache); |
124 |
4867 |
case THEORY_FP: return RewriteAttibute<THEORY_FP>::setPreRewriteCache(node, cache); |
125 |
32994 |
case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::setPreRewriteCache(node, cache); |
126 |
259690 |
case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::setPreRewriteCache(node, cache); |
127 |
1754 |
case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::setPreRewriteCache(node, cache); |
128 |
53293 |
case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::setPreRewriteCache(node, cache); |
129 |
1098 |
case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::setPreRewriteCache(node, cache); |
130 |
361894 |
case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::setPreRewriteCache(node, cache); |
131 |
135039 |
case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::setPreRewriteCache(node, cache); |
132 |
|
|
133 |
|
// clang-format on |
134 |
|
default: Unreachable(); |
135 |
|
} |
136 |
|
} |
137 |
|
|
138 |
11464712 |
void Rewriter::setPostRewriteCache(theory::TheoryId theoryId, |
139 |
|
TNode node, |
140 |
|
TNode cache) |
141 |
|
{ |
142 |
11464712 |
switch (theoryId) |
143 |
|
{ |
144 |
|
// clang-format off |
145 |
419512 |
case THEORY_BUILTIN: return RewriteAttibute<THEORY_BUILTIN>::setPostRewriteCache(node, cache); |
146 |
5695264 |
case THEORY_BOOL: return RewriteAttibute<THEORY_BOOL>::setPostRewriteCache(node, cache); |
147 |
418761 |
case THEORY_UF: return RewriteAttibute<THEORY_UF>::setPostRewriteCache(node, cache); |
148 |
3220828 |
case THEORY_ARITH: return RewriteAttibute<THEORY_ARITH>::setPostRewriteCache(node, cache); |
149 |
862801 |
case THEORY_BV: return RewriteAttibute<THEORY_BV>::setPostRewriteCache(node, cache); |
150 |
4837 |
case THEORY_FP: return RewriteAttibute<THEORY_FP>::setPostRewriteCache(node, cache); |
151 |
30600 |
case THEORY_ARRAYS: return RewriteAttibute<THEORY_ARRAYS>::setPostRewriteCache(node, cache); |
152 |
259672 |
case THEORY_DATATYPES: return RewriteAttibute<THEORY_DATATYPES>::setPostRewriteCache(node, cache); |
153 |
1754 |
case THEORY_SEP: return RewriteAttibute<THEORY_SEP>::setPostRewriteCache(node, cache); |
154 |
52702 |
case THEORY_SETS: return RewriteAttibute<THEORY_SETS>::setPostRewriteCache(node, cache); |
155 |
1084 |
case THEORY_BAGS: return RewriteAttibute<THEORY_BAGS>::setPostRewriteCache(node, cache); |
156 |
361894 |
case THEORY_STRINGS: return RewriteAttibute<THEORY_STRINGS>::setPostRewriteCache(node, cache); |
157 |
135003 |
case THEORY_QUANTIFIERS: return RewriteAttibute<THEORY_QUANTIFIERS>::setPostRewriteCache(node, cache); |
158 |
|
|
159 |
|
// clang-format on |
160 |
|
default: Unreachable(); |
161 |
|
} |
162 |
|
} |
163 |
|
|
164 |
13221 |
Rewriter::Rewriter() : d_tpg(nullptr) |
165 |
|
{ |
166 |
|
|
167 |
13221 |
} |
168 |
|
|
169 |
|
void Rewriter::clearCachesInternal() |
170 |
|
{ |
171 |
|
typedef cvc5::expr::attr::AttributeUniqueId AttributeUniqueId; |
172 |
|
std::vector<AttributeUniqueId> preids; |
173 |
|
// clang-format off |
174 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BUILTIN>::pre_rewrite())); |
175 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BOOL>::pre_rewrite())); |
176 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_UF>::pre_rewrite())); |
177 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARITH>::pre_rewrite())); |
178 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BV>::pre_rewrite())); |
179 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_FP>::pre_rewrite())); |
180 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARRAYS>::pre_rewrite())); |
181 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_DATATYPES>::pre_rewrite())); |
182 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SEP>::pre_rewrite())); |
183 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SETS>::pre_rewrite())); |
184 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BAGS>::pre_rewrite())); |
185 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_STRINGS>::pre_rewrite())); |
186 |
|
preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_QUANTIFIERS>::pre_rewrite())); |
187 |
|
// clang-format on |
188 |
|
|
189 |
|
std::vector<AttributeUniqueId> |
190 |
|
postids; |
191 |
|
// clang-format off |
192 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BUILTIN>::post_rewrite())); |
193 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BOOL>::post_rewrite())); |
194 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_UF>::post_rewrite())); |
195 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARITH>::post_rewrite())); |
196 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BV>::post_rewrite())); |
197 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_FP>::post_rewrite())); |
198 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_ARRAYS>::post_rewrite())); |
199 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_DATATYPES>::post_rewrite())); |
200 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SEP>::post_rewrite())); |
201 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_SETS>::post_rewrite())); |
202 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_BAGS>::post_rewrite())); |
203 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_STRINGS>::post_rewrite())); |
204 |
|
postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<THEORY_QUANTIFIERS>::post_rewrite())); |
205 |
|
// clang-format on |
206 |
|
|
207 |
|
std::vector<const AttributeUniqueId*> |
208 |
|
allids; |
209 |
|
for (size_t i = 0, size = preids.size(); i < size; ++i) |
210 |
|
{ |
211 |
|
allids.push_back(&preids[i]); |
212 |
|
} |
213 |
|
for (size_t i = 0, size = postids.size(); i < size; ++i) |
214 |
|
{ |
215 |
|
allids.push_back(&postids[i]); |
216 |
|
} |
217 |
|
NodeManager::currentNM()->deleteAttributes(allids); |
218 |
|
} |
219 |
|
|
220 |
|
} // namespace theory |
221 |
|
} // namespace cvc5 |