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 was automatically generated by: |
11 |
|
* |
12 |
|
* ../../../src/expr/mkmetakind /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/expr/metakind_template.h /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/quantifiers/kinds |
13 |
|
* |
14 |
|
* for the cvc5 project. |
15 |
|
*/ |
16 |
|
|
17 |
|
/****************************************************************************** |
18 |
|
* Top contributors (to current version): |
19 |
|
* Morgan Deters, Aina Niemetz, Mathias Preiner |
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 |
|
* Template for the metakind header. |
30 |
|
*/ |
31 |
|
|
32 |
|
#include "cvc5_private.h" |
33 |
|
|
34 |
|
#ifndef CVC5__KIND__METAKIND_H |
35 |
|
#define CVC5__KIND__METAKIND_H |
36 |
|
|
37 |
|
#include <iosfwd> |
38 |
|
|
39 |
|
#include "base/check.h" |
40 |
|
#include "expr/kind.h" |
41 |
|
|
42 |
|
namespace cvc5 { |
43 |
|
|
44 |
|
namespace expr { |
45 |
|
class NodeValue; |
46 |
|
} // namespace expr |
47 |
|
|
48 |
|
namespace kind { |
49 |
|
namespace metakind { |
50 |
|
|
51 |
|
/** |
52 |
|
* Static, compile-time information about types T representing cvc5 |
53 |
|
* constants: |
54 |
|
* |
55 |
|
* typename ConstantMap<T>::OwningTheory |
56 |
|
* |
57 |
|
* The theory in charge of constructing T when constructing Nodes |
58 |
|
* with NodeManager::mkConst(T). |
59 |
|
* |
60 |
|
* typename ConstantMap<T>::kind |
61 |
|
* |
62 |
|
* The kind to use when constructing Nodes with |
63 |
|
* NodeManager::mkConst(T). |
64 |
|
*/ |
65 |
|
template <class T> |
66 |
|
struct ConstantMap; |
67 |
|
|
68 |
|
/** |
69 |
|
* Static, compile-time information about kinds k and what type their |
70 |
|
* corresponding cvc5 constants are: |
71 |
|
* |
72 |
|
* typename ConstantMapReverse<k>::T |
73 |
|
* |
74 |
|
* Constant type for kind k. |
75 |
|
*/ |
76 |
|
template <Kind k> |
77 |
|
struct ConstantMapReverse; |
78 |
|
|
79 |
|
/** |
80 |
|
* Static, compile-time mapping from CONSTANT kinds to comparison |
81 |
|
* functors on NodeValue*. The single element of this structure is: |
82 |
|
* |
83 |
|
* static bool NodeValueCompare<K, pool>::compare(NodeValue* x, NodeValue* y) |
84 |
|
* |
85 |
|
* Compares x and y, given that they are both K-kinded (and the |
86 |
|
* meta-kind of K is CONSTANT). If pool == true, one of x and y |
87 |
|
* (but not both) may be a "non-inlined" NodeValue. If pool == |
88 |
|
* false, neither x nor y may be a "non-inlined" NodeValue. |
89 |
|
*/ |
90 |
|
template <Kind k, bool pool> |
91 |
|
struct NodeValueConstCompare { |
92 |
|
inline static bool compare(const ::cvc5::expr::NodeValue* x, |
93 |
|
const ::cvc5::expr::NodeValue* y); |
94 |
|
inline static size_t constHash(const ::cvc5::expr::NodeValue* nv); |
95 |
|
};/* NodeValueConstCompare<k, pool> */ |
96 |
|
|
97 |
|
struct NodeValueCompare { |
98 |
|
template <bool pool> |
99 |
|
static bool compare(const ::cvc5::expr::NodeValue* nv1, |
100 |
|
const ::cvc5::expr::NodeValue* nv2); |
101 |
|
static size_t constHash(const ::cvc5::expr::NodeValue* nv); |
102 |
|
};/* struct NodeValueCompare */ |
103 |
|
|
104 |
|
/** |
105 |
|
* "metakinds" represent the "kinds" of kinds at the meta-level. |
106 |
|
* "metakind" is an ugly name but it's not used by client code, just |
107 |
|
* by the expr package, and the intent here is to keep it from |
108 |
|
* polluting the kind namespace. For more documentation on what these |
109 |
|
* mean, see src/theory/builtin/kinds. |
110 |
|
*/ |
111 |
|
enum MetaKind_t { |
112 |
|
INVALID = -1, /**< special node non-kinds like NULL_EXPR or LAST_KIND */ |
113 |
|
VARIABLE, /**< special node kinds: no operator */ |
114 |
|
OPERATOR, /**< operators that get "inlined" */ |
115 |
|
PARAMETERIZED, /**< parameterized ops (like APPLYs) that carry extra data */ |
116 |
|
CONSTANT, /**< constants */ |
117 |
|
NULLARY_OPERATOR /**< nullary operator */ |
118 |
|
};/* enum MetaKind_t */ |
119 |
|
|
120 |
|
} // namespace metakind |
121 |
|
|
122 |
|
// import MetaKind into the "cvc5::kind" namespace but keep the |
123 |
|
// individual MetaKind constants under kind::metakind:: |
124 |
|
typedef ::cvc5::kind::metakind::MetaKind_t MetaKind; |
125 |
|
|
126 |
|
/** |
127 |
|
* Get the metakind for a particular kind. |
128 |
|
*/ |
129 |
|
MetaKind metaKindOf(Kind k); |
130 |
|
} // namespace kind |
131 |
|
|
132 |
|
namespace expr { |
133 |
|
|
134 |
|
// Comparison predicate |
135 |
|
struct NodeValuePoolEq { |
136 |
688859850 |
inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const { |
137 |
688859850 |
return ::cvc5::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2); |
138 |
|
} |
139 |
|
}; |
140 |
|
|
141 |
|
} // namespace expr |
142 |
|
} // namespace cvc5 |
143 |
|
|
144 |
|
#include "expr/node_value.h" |
145 |
|
|
146 |
|
#endif /* CVC5__KIND__METAKIND_H */ |
147 |
|
|
148 |
|
// clang-format off |
149 |
|
|
150 |
|
// #include "theory/builtin/::cvc5::theory::builtin::TheoryBuiltin" |
151 |
|
#include "expr/uninterpreted_constant.h" |
152 |
|
#include "util/abstract_value.h" |
153 |
|
#include "expr/kind.h" |
154 |
|
// #include "theory/booleans/::cvc5::theory::booleans::TheoryBool" |
155 |
|
#include "util/bool.h" |
156 |
|
// #include "theory/uf/::cvc5::theory::uf::TheoryUF" |
157 |
|
// #include "theory/arith/::cvc5::theory::arith::TheoryArith" |
158 |
|
#include "util/divisible.h" |
159 |
|
#include "util/rational.h" |
160 |
|
#include "util/indexed_root_predicate.h" |
161 |
|
#include "util/iand.h" |
162 |
|
// #include "theory/bv/::cvc5::theory::bv::TheoryBV" |
163 |
|
#include "util/bitvector.h" |
164 |
|
// #include "theory/fp/::cvc5::theory::fp::TheoryFp" |
165 |
|
#include "util/floatingpoint.h" |
166 |
|
// #include "theory/arrays/::cvc5::theory::arrays::TheoryArrays" |
167 |
|
#include "expr/array_store_all.h" |
168 |
|
// #include "theory/datatypes/::cvc5::theory::datatypes::TheoryDatatypes" |
169 |
|
#include "expr/datatype_index.h" |
170 |
|
#include "expr/ascription_type.h" |
171 |
|
#include "theory/datatypes/tuple_project_op.h" |
172 |
|
// #include "theory/sep/::cvc5::theory::sep::TheorySep" |
173 |
|
// #include "theory/sets/::cvc5::theory::sets::TheorySets" |
174 |
|
#include "expr/emptyset.h" |
175 |
|
#include "theory/sets/singleton_op.h" |
176 |
|
// #include "theory/bags/::cvc5::theory::bags::TheoryBags" |
177 |
|
#include "expr/emptybag.h" |
178 |
|
#include "theory/bags/make_bag_op.h" |
179 |
|
// #include "theory/strings/::cvc5::theory::strings::TheoryStrings" |
180 |
|
#include "util/string.h" |
181 |
|
#include "expr/sequence.h" |
182 |
|
#include "util/regexp.h" |
183 |
|
// #include "theory/quantifiers/::cvc5::theory::quantifiers::TheoryQuantifiers" |
184 |
|
// clang-format on |
185 |
|
|
186 |
|
#ifdef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP |
187 |
|
|
188 |
|
namespace cvc5 { |
189 |
|
|
190 |
|
namespace expr { |
191 |
|
// clang-format off |
192 |
|
|
193 |
|
template <> |
194 |
|
::cvc5::UninterpretedConstant const& NodeValue::getConst< ::cvc5::UninterpretedConstant >() const; |
195 |
|
|
196 |
|
template <> |
197 |
|
::cvc5::AbstractValue const& NodeValue::getConst< ::cvc5::AbstractValue >() const; |
198 |
|
|
199 |
|
template <> |
200 |
|
::cvc5::Kind const& NodeValue::getConst< ::cvc5::Kind >() const; |
201 |
|
|
202 |
|
template <> |
203 |
|
::cvc5::TypeConstant const& NodeValue::getConst< ::cvc5::TypeConstant >() const; |
204 |
|
|
205 |
|
template <> |
206 |
|
bool const& NodeValue::getConst< bool >() const; |
207 |
|
|
208 |
|
template <> |
209 |
|
::cvc5::Divisible const& NodeValue::getConst< ::cvc5::Divisible >() const; |
210 |
|
|
211 |
|
template <> |
212 |
|
::cvc5::Rational const& NodeValue::getConst< ::cvc5::Rational >() const; |
213 |
|
|
214 |
|
template <> |
215 |
|
::cvc5::IndexedRootPredicate const& NodeValue::getConst< ::cvc5::IndexedRootPredicate >() const; |
216 |
|
|
217 |
|
template <> |
218 |
|
::cvc5::IntAnd const& NodeValue::getConst< ::cvc5::IntAnd >() const; |
219 |
|
|
220 |
|
template <> |
221 |
|
::cvc5::BitVectorSize const& NodeValue::getConst< ::cvc5::BitVectorSize >() const; |
222 |
|
|
223 |
|
template <> |
224 |
|
::cvc5::BitVector const& NodeValue::getConst< ::cvc5::BitVector >() const; |
225 |
|
|
226 |
|
template <> |
227 |
|
::cvc5::BitVectorBitOf const& NodeValue::getConst< ::cvc5::BitVectorBitOf >() const; |
228 |
|
|
229 |
|
template <> |
230 |
|
::cvc5::BitVectorExtract const& NodeValue::getConst< ::cvc5::BitVectorExtract >() const; |
231 |
|
|
232 |
|
template <> |
233 |
|
::cvc5::BitVectorRepeat const& NodeValue::getConst< ::cvc5::BitVectorRepeat >() const; |
234 |
|
|
235 |
|
template <> |
236 |
|
::cvc5::BitVectorRotateLeft const& NodeValue::getConst< ::cvc5::BitVectorRotateLeft >() const; |
237 |
|
|
238 |
|
template <> |
239 |
|
::cvc5::BitVectorRotateRight const& NodeValue::getConst< ::cvc5::BitVectorRotateRight >() const; |
240 |
|
|
241 |
|
template <> |
242 |
|
::cvc5::BitVectorSignExtend const& NodeValue::getConst< ::cvc5::BitVectorSignExtend >() const; |
243 |
|
|
244 |
|
template <> |
245 |
|
::cvc5::BitVectorZeroExtend const& NodeValue::getConst< ::cvc5::BitVectorZeroExtend >() const; |
246 |
|
|
247 |
|
template <> |
248 |
|
::cvc5::IntToBitVector const& NodeValue::getConst< ::cvc5::IntToBitVector >() const; |
249 |
|
|
250 |
|
template <> |
251 |
|
::cvc5::FloatingPoint const& NodeValue::getConst< ::cvc5::FloatingPoint >() const; |
252 |
|
|
253 |
|
template <> |
254 |
|
::cvc5::RoundingMode const& NodeValue::getConst< ::cvc5::RoundingMode >() const; |
255 |
|
|
256 |
|
template <> |
257 |
|
::cvc5::FloatingPointSize const& NodeValue::getConst< ::cvc5::FloatingPointSize >() const; |
258 |
|
|
259 |
|
template <> |
260 |
|
::cvc5::FloatingPointToFPIEEEBitVector const& NodeValue::getConst< ::cvc5::FloatingPointToFPIEEEBitVector >() const; |
261 |
|
|
262 |
|
template <> |
263 |
|
::cvc5::FloatingPointToFPFloatingPoint const& NodeValue::getConst< ::cvc5::FloatingPointToFPFloatingPoint >() const; |
264 |
|
|
265 |
|
template <> |
266 |
|
::cvc5::FloatingPointToFPReal const& NodeValue::getConst< ::cvc5::FloatingPointToFPReal >() const; |
267 |
|
|
268 |
|
template <> |
269 |
|
::cvc5::FloatingPointToFPSignedBitVector const& NodeValue::getConst< ::cvc5::FloatingPointToFPSignedBitVector >() const; |
270 |
|
|
271 |
|
template <> |
272 |
|
::cvc5::FloatingPointToFPUnsignedBitVector const& NodeValue::getConst< ::cvc5::FloatingPointToFPUnsignedBitVector >() const; |
273 |
|
|
274 |
|
template <> |
275 |
|
::cvc5::FloatingPointToFPGeneric const& NodeValue::getConst< ::cvc5::FloatingPointToFPGeneric >() const; |
276 |
|
|
277 |
|
template <> |
278 |
|
::cvc5::FloatingPointToUBV const& NodeValue::getConst< ::cvc5::FloatingPointToUBV >() const; |
279 |
|
|
280 |
|
template <> |
281 |
|
::cvc5::FloatingPointToUBVTotal const& NodeValue::getConst< ::cvc5::FloatingPointToUBVTotal >() const; |
282 |
|
|
283 |
|
template <> |
284 |
|
::cvc5::FloatingPointToSBV const& NodeValue::getConst< ::cvc5::FloatingPointToSBV >() const; |
285 |
|
|
286 |
|
template <> |
287 |
|
::cvc5::FloatingPointToSBVTotal const& NodeValue::getConst< ::cvc5::FloatingPointToSBVTotal >() const; |
288 |
|
|
289 |
|
template <> |
290 |
|
::cvc5::ArrayStoreAll const& NodeValue::getConst< ::cvc5::ArrayStoreAll >() const; |
291 |
|
|
292 |
|
template <> |
293 |
|
::cvc5::DatatypeIndexConstant const& NodeValue::getConst< ::cvc5::DatatypeIndexConstant >() const; |
294 |
|
|
295 |
|
template <> |
296 |
|
::cvc5::AscriptionType const& NodeValue::getConst< ::cvc5::AscriptionType >() const; |
297 |
|
|
298 |
|
template <> |
299 |
|
::cvc5::TupleProjectOp const& NodeValue::getConst< ::cvc5::TupleProjectOp >() const; |
300 |
|
|
301 |
|
template <> |
302 |
|
::cvc5::EmptySet const& NodeValue::getConst< ::cvc5::EmptySet >() const; |
303 |
|
|
304 |
|
template <> |
305 |
|
::cvc5::SingletonOp const& NodeValue::getConst< ::cvc5::SingletonOp >() const; |
306 |
|
|
307 |
|
template <> |
308 |
|
::cvc5::EmptyBag const& NodeValue::getConst< ::cvc5::EmptyBag >() const; |
309 |
|
|
310 |
|
template <> |
311 |
|
::cvc5::MakeBagOp const& NodeValue::getConst< ::cvc5::MakeBagOp >() const; |
312 |
|
|
313 |
|
template <> |
314 |
|
::cvc5::String const& NodeValue::getConst< ::cvc5::String >() const; |
315 |
|
|
316 |
|
template <> |
317 |
|
::cvc5::Sequence const& NodeValue::getConst< ::cvc5::Sequence >() const; |
318 |
|
|
319 |
|
template <> |
320 |
|
::cvc5::RegExpRepeat const& NodeValue::getConst< ::cvc5::RegExpRepeat >() const; |
321 |
|
|
322 |
|
template <> |
323 |
|
::cvc5::RegExpLoop const& NodeValue::getConst< ::cvc5::RegExpLoop >() const; |
324 |
|
|
325 |
|
// clang-format on |
326 |
|
} // namespace expr |
327 |
|
|
328 |
|
namespace kind { |
329 |
|
namespace metakind { |
330 |
|
|
331 |
|
template <Kind k, bool pool> |
332 |
487977048 |
inline bool NodeValueConstCompare<k, pool>::compare( |
333 |
|
const ::cvc5::expr::NodeValue* x, const ::cvc5::expr::NodeValue* y) |
334 |
|
{ |
335 |
|
typedef typename ConstantMapReverse<k>::T T; |
336 |
|
if(pool) { |
337 |
487977048 |
if(x->d_nchildren == 1) { |
338 |
240251212 |
Assert(y->d_nchildren == 0); |
339 |
240251212 |
return compare(y, x); |
340 |
247725836 |
} else if(y->d_nchildren == 1) { |
341 |
240251212 |
Assert(x->d_nchildren == 0); |
342 |
240251212 |
return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]); |
343 |
|
} |
344 |
|
} |
345 |
|
|
346 |
7474624 |
Assert(x->d_nchildren == 0); |
347 |
7474624 |
Assert(y->d_nchildren == 0); |
348 |
7474624 |
return x->getConst<T>() == y->getConst<T>(); |
349 |
|
} |
350 |
|
|
351 |
|
template <Kind k, bool pool> |
352 |
|
inline size_t NodeValueConstCompare<k, pool>::constHash( |
353 |
|
const ::cvc5::expr::NodeValue* nv) |
354 |
|
{ |
355 |
|
typedef typename ConstantMapReverse<k>::T T; |
356 |
|
return nv->getConst<T>().hash(); |
357 |
|
} |
358 |
|
|
359 |
|
// clang-format off |
360 |
|
|
361 |
|
template <> |
362 |
|
struct ConstantMap< ::cvc5::UninterpretedConstant > { |
363 |
|
// typedef THEORY_BUILTIN OwningTheory; |
364 |
|
enum { kind = ::cvc5::kind::UNINTERPRETED_CONSTANT }; |
365 |
|
};/* ConstantMap< ::cvc5::UninterpretedConstant > */ |
366 |
|
|
367 |
|
template <> |
368 |
|
struct ConstantMapReverse< ::cvc5::kind::UNINTERPRETED_CONSTANT > { |
369 |
|
typedef ::cvc5::UninterpretedConstant T; |
370 |
|
};/* ConstantMapReverse< ::cvc5::kind::UNINTERPRETED_CONSTANT > */ |
371 |
|
|
372 |
|
template <> |
373 |
|
struct ConstantMap< ::cvc5::AbstractValue > { |
374 |
|
// typedef THEORY_BUILTIN OwningTheory; |
375 |
|
enum { kind = ::cvc5::kind::ABSTRACT_VALUE }; |
376 |
|
};/* ConstantMap< ::cvc5::AbstractValue > */ |
377 |
|
|
378 |
|
template <> |
379 |
|
struct ConstantMapReverse< ::cvc5::kind::ABSTRACT_VALUE > { |
380 |
|
typedef ::cvc5::AbstractValue T; |
381 |
|
};/* ConstantMapReverse< ::cvc5::kind::ABSTRACT_VALUE > */ |
382 |
|
|
383 |
|
template <> |
384 |
|
struct ConstantMap< ::cvc5::Kind > { |
385 |
|
// typedef THEORY_BUILTIN OwningTheory; |
386 |
|
enum { kind = ::cvc5::kind::BUILTIN }; |
387 |
|
};/* ConstantMap< ::cvc5::Kind > */ |
388 |
|
|
389 |
|
template <> |
390 |
|
struct ConstantMapReverse< ::cvc5::kind::BUILTIN > { |
391 |
|
typedef ::cvc5::Kind T; |
392 |
|
};/* ConstantMapReverse< ::cvc5::kind::BUILTIN > */ |
393 |
|
|
394 |
|
template <> |
395 |
|
struct ConstantMap< ::cvc5::TypeConstant > { |
396 |
|
// typedef THEORY_BUILTIN OwningTheory; |
397 |
|
enum { kind = ::cvc5::kind::TYPE_CONSTANT }; |
398 |
|
};/* ConstantMap< ::cvc5::TypeConstant > */ |
399 |
|
|
400 |
|
template <> |
401 |
|
struct ConstantMapReverse< ::cvc5::kind::TYPE_CONSTANT > { |
402 |
|
typedef ::cvc5::TypeConstant T; |
403 |
|
};/* ConstantMapReverse< ::cvc5::kind::TYPE_CONSTANT > */ |
404 |
|
|
405 |
|
template <> |
406 |
|
struct ConstantMap< bool > { |
407 |
|
// typedef THEORY_BOOL OwningTheory; |
408 |
|
enum { kind = ::cvc5::kind::CONST_BOOLEAN }; |
409 |
|
};/* ConstantMap< bool > */ |
410 |
|
|
411 |
|
template <> |
412 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_BOOLEAN > { |
413 |
|
typedef bool T; |
414 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_BOOLEAN > */ |
415 |
|
|
416 |
|
template <> |
417 |
|
struct ConstantMap< ::cvc5::Divisible > { |
418 |
|
// typedef THEORY_ARITH OwningTheory; |
419 |
|
enum { kind = ::cvc5::kind::DIVISIBLE_OP }; |
420 |
|
};/* ConstantMap< ::cvc5::Divisible > */ |
421 |
|
|
422 |
|
template <> |
423 |
|
struct ConstantMapReverse< ::cvc5::kind::DIVISIBLE_OP > { |
424 |
|
typedef ::cvc5::Divisible T; |
425 |
|
};/* ConstantMapReverse< ::cvc5::kind::DIVISIBLE_OP > */ |
426 |
|
|
427 |
|
template <> |
428 |
|
struct ConstantMap< ::cvc5::Rational > { |
429 |
|
// typedef THEORY_ARITH OwningTheory; |
430 |
|
enum { kind = ::cvc5::kind::CONST_RATIONAL }; |
431 |
|
};/* ConstantMap< ::cvc5::Rational > */ |
432 |
|
|
433 |
|
template <> |
434 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_RATIONAL > { |
435 |
|
typedef ::cvc5::Rational T; |
436 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_RATIONAL > */ |
437 |
|
|
438 |
|
template <> |
439 |
|
struct ConstantMap< ::cvc5::IndexedRootPredicate > { |
440 |
|
// typedef THEORY_ARITH OwningTheory; |
441 |
|
enum { kind = ::cvc5::kind::INDEXED_ROOT_PREDICATE_OP }; |
442 |
|
};/* ConstantMap< ::cvc5::IndexedRootPredicate > */ |
443 |
|
|
444 |
|
template <> |
445 |
|
struct ConstantMapReverse< ::cvc5::kind::INDEXED_ROOT_PREDICATE_OP > { |
446 |
|
typedef ::cvc5::IndexedRootPredicate T; |
447 |
|
};/* ConstantMapReverse< ::cvc5::kind::INDEXED_ROOT_PREDICATE_OP > */ |
448 |
|
|
449 |
|
template <> |
450 |
|
struct ConstantMap< ::cvc5::IntAnd > { |
451 |
|
// typedef THEORY_ARITH OwningTheory; |
452 |
|
enum { kind = ::cvc5::kind::IAND_OP }; |
453 |
|
};/* ConstantMap< ::cvc5::IntAnd > */ |
454 |
|
|
455 |
|
template <> |
456 |
|
struct ConstantMapReverse< ::cvc5::kind::IAND_OP > { |
457 |
|
typedef ::cvc5::IntAnd T; |
458 |
|
};/* ConstantMapReverse< ::cvc5::kind::IAND_OP > */ |
459 |
|
|
460 |
|
template <> |
461 |
|
struct ConstantMap< ::cvc5::BitVectorSize > { |
462 |
|
// typedef THEORY_BV OwningTheory; |
463 |
|
enum { kind = ::cvc5::kind::BITVECTOR_TYPE }; |
464 |
|
};/* ConstantMap< ::cvc5::BitVectorSize > */ |
465 |
|
|
466 |
|
template <> |
467 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_TYPE > { |
468 |
|
typedef ::cvc5::BitVectorSize T; |
469 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_TYPE > */ |
470 |
|
|
471 |
|
template <> |
472 |
|
struct ConstantMap< ::cvc5::BitVector > { |
473 |
|
// typedef THEORY_BV OwningTheory; |
474 |
|
enum { kind = ::cvc5::kind::CONST_BITVECTOR }; |
475 |
|
};/* ConstantMap< ::cvc5::BitVector > */ |
476 |
|
|
477 |
|
template <> |
478 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_BITVECTOR > { |
479 |
|
typedef ::cvc5::BitVector T; |
480 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_BITVECTOR > */ |
481 |
|
|
482 |
|
template <> |
483 |
|
struct ConstantMap< ::cvc5::BitVectorBitOf > { |
484 |
|
// typedef THEORY_BV OwningTheory; |
485 |
|
enum { kind = ::cvc5::kind::BITVECTOR_BITOF_OP }; |
486 |
|
};/* ConstantMap< ::cvc5::BitVectorBitOf > */ |
487 |
|
|
488 |
|
template <> |
489 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_BITOF_OP > { |
490 |
|
typedef ::cvc5::BitVectorBitOf T; |
491 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_BITOF_OP > */ |
492 |
|
|
493 |
|
template <> |
494 |
|
struct ConstantMap< ::cvc5::BitVectorExtract > { |
495 |
|
// typedef THEORY_BV OwningTheory; |
496 |
|
enum { kind = ::cvc5::kind::BITVECTOR_EXTRACT_OP }; |
497 |
|
};/* ConstantMap< ::cvc5::BitVectorExtract > */ |
498 |
|
|
499 |
|
template <> |
500 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_EXTRACT_OP > { |
501 |
|
typedef ::cvc5::BitVectorExtract T; |
502 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_EXTRACT_OP > */ |
503 |
|
|
504 |
|
template <> |
505 |
|
struct ConstantMap< ::cvc5::BitVectorRepeat > { |
506 |
|
// typedef THEORY_BV OwningTheory; |
507 |
|
enum { kind = ::cvc5::kind::BITVECTOR_REPEAT_OP }; |
508 |
|
};/* ConstantMap< ::cvc5::BitVectorRepeat > */ |
509 |
|
|
510 |
|
template <> |
511 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_REPEAT_OP > { |
512 |
|
typedef ::cvc5::BitVectorRepeat T; |
513 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_REPEAT_OP > */ |
514 |
|
|
515 |
|
template <> |
516 |
|
struct ConstantMap< ::cvc5::BitVectorRotateLeft > { |
517 |
|
// typedef THEORY_BV OwningTheory; |
518 |
|
enum { kind = ::cvc5::kind::BITVECTOR_ROTATE_LEFT_OP }; |
519 |
|
};/* ConstantMap< ::cvc5::BitVectorRotateLeft > */ |
520 |
|
|
521 |
|
template <> |
522 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_ROTATE_LEFT_OP > { |
523 |
|
typedef ::cvc5::BitVectorRotateLeft T; |
524 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_ROTATE_LEFT_OP > */ |
525 |
|
|
526 |
|
template <> |
527 |
|
struct ConstantMap< ::cvc5::BitVectorRotateRight > { |
528 |
|
// typedef THEORY_BV OwningTheory; |
529 |
|
enum { kind = ::cvc5::kind::BITVECTOR_ROTATE_RIGHT_OP }; |
530 |
|
};/* ConstantMap< ::cvc5::BitVectorRotateRight > */ |
531 |
|
|
532 |
|
template <> |
533 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_ROTATE_RIGHT_OP > { |
534 |
|
typedef ::cvc5::BitVectorRotateRight T; |
535 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_ROTATE_RIGHT_OP > */ |
536 |
|
|
537 |
|
template <> |
538 |
|
struct ConstantMap< ::cvc5::BitVectorSignExtend > { |
539 |
|
// typedef THEORY_BV OwningTheory; |
540 |
|
enum { kind = ::cvc5::kind::BITVECTOR_SIGN_EXTEND_OP }; |
541 |
|
};/* ConstantMap< ::cvc5::BitVectorSignExtend > */ |
542 |
|
|
543 |
|
template <> |
544 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_SIGN_EXTEND_OP > { |
545 |
|
typedef ::cvc5::BitVectorSignExtend T; |
546 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_SIGN_EXTEND_OP > */ |
547 |
|
|
548 |
|
template <> |
549 |
|
struct ConstantMap< ::cvc5::BitVectorZeroExtend > { |
550 |
|
// typedef THEORY_BV OwningTheory; |
551 |
|
enum { kind = ::cvc5::kind::BITVECTOR_ZERO_EXTEND_OP }; |
552 |
|
};/* ConstantMap< ::cvc5::BitVectorZeroExtend > */ |
553 |
|
|
554 |
|
template <> |
555 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_ZERO_EXTEND_OP > { |
556 |
|
typedef ::cvc5::BitVectorZeroExtend T; |
557 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_ZERO_EXTEND_OP > */ |
558 |
|
|
559 |
|
template <> |
560 |
|
struct ConstantMap< ::cvc5::IntToBitVector > { |
561 |
|
// typedef THEORY_BV OwningTheory; |
562 |
|
enum { kind = ::cvc5::kind::INT_TO_BITVECTOR_OP }; |
563 |
|
};/* ConstantMap< ::cvc5::IntToBitVector > */ |
564 |
|
|
565 |
|
template <> |
566 |
|
struct ConstantMapReverse< ::cvc5::kind::INT_TO_BITVECTOR_OP > { |
567 |
|
typedef ::cvc5::IntToBitVector T; |
568 |
|
};/* ConstantMapReverse< ::cvc5::kind::INT_TO_BITVECTOR_OP > */ |
569 |
|
|
570 |
|
template <> |
571 |
|
struct ConstantMap< ::cvc5::FloatingPoint > { |
572 |
|
// typedef THEORY_FP OwningTheory; |
573 |
|
enum { kind = ::cvc5::kind::CONST_FLOATINGPOINT }; |
574 |
|
};/* ConstantMap< ::cvc5::FloatingPoint > */ |
575 |
|
|
576 |
|
template <> |
577 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_FLOATINGPOINT > { |
578 |
|
typedef ::cvc5::FloatingPoint T; |
579 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_FLOATINGPOINT > */ |
580 |
|
|
581 |
|
template <> |
582 |
|
struct ConstantMap< ::cvc5::RoundingMode > { |
583 |
|
// typedef THEORY_FP OwningTheory; |
584 |
|
enum { kind = ::cvc5::kind::CONST_ROUNDINGMODE }; |
585 |
|
};/* ConstantMap< ::cvc5::RoundingMode > */ |
586 |
|
|
587 |
|
template <> |
588 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_ROUNDINGMODE > { |
589 |
|
typedef ::cvc5::RoundingMode T; |
590 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_ROUNDINGMODE > */ |
591 |
|
|
592 |
|
template <> |
593 |
|
struct ConstantMap< ::cvc5::FloatingPointSize > { |
594 |
|
// typedef THEORY_FP OwningTheory; |
595 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TYPE }; |
596 |
|
};/* ConstantMap< ::cvc5::FloatingPointSize > */ |
597 |
|
|
598 |
|
template <> |
599 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TYPE > { |
600 |
|
typedef ::cvc5::FloatingPointSize T; |
601 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TYPE > */ |
602 |
|
|
603 |
|
template <> |
604 |
|
struct ConstantMap< ::cvc5::FloatingPointToFPIEEEBitVector > { |
605 |
|
// typedef THEORY_FP OwningTheory; |
606 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP }; |
607 |
|
};/* ConstantMap< ::cvc5::FloatingPointToFPIEEEBitVector > */ |
608 |
|
|
609 |
|
template <> |
610 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP > { |
611 |
|
typedef ::cvc5::FloatingPointToFPIEEEBitVector T; |
612 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP > */ |
613 |
|
|
614 |
|
template <> |
615 |
|
struct ConstantMap< ::cvc5::FloatingPointToFPFloatingPoint > { |
616 |
|
// typedef THEORY_FP OwningTheory; |
617 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP }; |
618 |
|
};/* ConstantMap< ::cvc5::FloatingPointToFPFloatingPoint > */ |
619 |
|
|
620 |
|
template <> |
621 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP > { |
622 |
|
typedef ::cvc5::FloatingPointToFPFloatingPoint T; |
623 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP > */ |
624 |
|
|
625 |
|
template <> |
626 |
|
struct ConstantMap< ::cvc5::FloatingPointToFPReal > { |
627 |
|
// typedef THEORY_FP OwningTheory; |
628 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_FP_REAL_OP }; |
629 |
|
};/* ConstantMap< ::cvc5::FloatingPointToFPReal > */ |
630 |
|
|
631 |
|
template <> |
632 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_REAL_OP > { |
633 |
|
typedef ::cvc5::FloatingPointToFPReal T; |
634 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_REAL_OP > */ |
635 |
|
|
636 |
|
template <> |
637 |
|
struct ConstantMap< ::cvc5::FloatingPointToFPSignedBitVector > { |
638 |
|
// typedef THEORY_FP OwningTheory; |
639 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP }; |
640 |
|
};/* ConstantMap< ::cvc5::FloatingPointToFPSignedBitVector > */ |
641 |
|
|
642 |
|
template <> |
643 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP > { |
644 |
|
typedef ::cvc5::FloatingPointToFPSignedBitVector T; |
645 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP > */ |
646 |
|
|
647 |
|
template <> |
648 |
|
struct ConstantMap< ::cvc5::FloatingPointToFPUnsignedBitVector > { |
649 |
|
// typedef THEORY_FP OwningTheory; |
650 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP }; |
651 |
|
};/* ConstantMap< ::cvc5::FloatingPointToFPUnsignedBitVector > */ |
652 |
|
|
653 |
|
template <> |
654 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP > { |
655 |
|
typedef ::cvc5::FloatingPointToFPUnsignedBitVector T; |
656 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP > */ |
657 |
|
|
658 |
|
template <> |
659 |
|
struct ConstantMap< ::cvc5::FloatingPointToFPGeneric > { |
660 |
|
// typedef THEORY_FP OwningTheory; |
661 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_FP_GENERIC_OP }; |
662 |
|
};/* ConstantMap< ::cvc5::FloatingPointToFPGeneric > */ |
663 |
|
|
664 |
|
template <> |
665 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_GENERIC_OP > { |
666 |
|
typedef ::cvc5::FloatingPointToFPGeneric T; |
667 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_GENERIC_OP > */ |
668 |
|
|
669 |
|
template <> |
670 |
|
struct ConstantMap< ::cvc5::FloatingPointToUBV > { |
671 |
|
// typedef THEORY_FP OwningTheory; |
672 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_UBV_OP }; |
673 |
|
};/* ConstantMap< ::cvc5::FloatingPointToUBV > */ |
674 |
|
|
675 |
|
template <> |
676 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_UBV_OP > { |
677 |
|
typedef ::cvc5::FloatingPointToUBV T; |
678 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_UBV_OP > */ |
679 |
|
|
680 |
|
template <> |
681 |
|
struct ConstantMap< ::cvc5::FloatingPointToUBVTotal > { |
682 |
|
// typedef THEORY_FP OwningTheory; |
683 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_UBV_TOTAL_OP }; |
684 |
|
};/* ConstantMap< ::cvc5::FloatingPointToUBVTotal > */ |
685 |
|
|
686 |
|
template <> |
687 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_UBV_TOTAL_OP > { |
688 |
|
typedef ::cvc5::FloatingPointToUBVTotal T; |
689 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_UBV_TOTAL_OP > */ |
690 |
|
|
691 |
|
template <> |
692 |
|
struct ConstantMap< ::cvc5::FloatingPointToSBV > { |
693 |
|
// typedef THEORY_FP OwningTheory; |
694 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_SBV_OP }; |
695 |
|
};/* ConstantMap< ::cvc5::FloatingPointToSBV > */ |
696 |
|
|
697 |
|
template <> |
698 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_SBV_OP > { |
699 |
|
typedef ::cvc5::FloatingPointToSBV T; |
700 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_SBV_OP > */ |
701 |
|
|
702 |
|
template <> |
703 |
|
struct ConstantMap< ::cvc5::FloatingPointToSBVTotal > { |
704 |
|
// typedef THEORY_FP OwningTheory; |
705 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_SBV_TOTAL_OP }; |
706 |
|
};/* ConstantMap< ::cvc5::FloatingPointToSBVTotal > */ |
707 |
|
|
708 |
|
template <> |
709 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_SBV_TOTAL_OP > { |
710 |
|
typedef ::cvc5::FloatingPointToSBVTotal T; |
711 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_SBV_TOTAL_OP > */ |
712 |
|
|
713 |
|
template <> |
714 |
|
struct ConstantMap< ::cvc5::ArrayStoreAll > { |
715 |
|
// typedef THEORY_ARRAYS OwningTheory; |
716 |
|
enum { kind = ::cvc5::kind::STORE_ALL }; |
717 |
|
};/* ConstantMap< ::cvc5::ArrayStoreAll > */ |
718 |
|
|
719 |
|
template <> |
720 |
|
struct ConstantMapReverse< ::cvc5::kind::STORE_ALL > { |
721 |
|
typedef ::cvc5::ArrayStoreAll T; |
722 |
|
};/* ConstantMapReverse< ::cvc5::kind::STORE_ALL > */ |
723 |
|
|
724 |
|
template <> |
725 |
|
struct ConstantMap< ::cvc5::DatatypeIndexConstant > { |
726 |
|
// typedef THEORY_DATATYPES OwningTheory; |
727 |
|
enum { kind = ::cvc5::kind::DATATYPE_TYPE }; |
728 |
|
};/* ConstantMap< ::cvc5::DatatypeIndexConstant > */ |
729 |
|
|
730 |
|
template <> |
731 |
|
struct ConstantMapReverse< ::cvc5::kind::DATATYPE_TYPE > { |
732 |
|
typedef ::cvc5::DatatypeIndexConstant T; |
733 |
|
};/* ConstantMapReverse< ::cvc5::kind::DATATYPE_TYPE > */ |
734 |
|
|
735 |
|
template <> |
736 |
|
struct ConstantMap< ::cvc5::AscriptionType > { |
737 |
|
// typedef THEORY_DATATYPES OwningTheory; |
738 |
|
enum { kind = ::cvc5::kind::ASCRIPTION_TYPE }; |
739 |
|
};/* ConstantMap< ::cvc5::AscriptionType > */ |
740 |
|
|
741 |
|
template <> |
742 |
|
struct ConstantMapReverse< ::cvc5::kind::ASCRIPTION_TYPE > { |
743 |
|
typedef ::cvc5::AscriptionType T; |
744 |
|
};/* ConstantMapReverse< ::cvc5::kind::ASCRIPTION_TYPE > */ |
745 |
|
|
746 |
|
template <> |
747 |
|
struct ConstantMap< ::cvc5::TupleProjectOp > { |
748 |
|
// typedef THEORY_DATATYPES OwningTheory; |
749 |
|
enum { kind = ::cvc5::kind::TUPLE_PROJECT_OP }; |
750 |
|
};/* ConstantMap< ::cvc5::TupleProjectOp > */ |
751 |
|
|
752 |
|
template <> |
753 |
|
struct ConstantMapReverse< ::cvc5::kind::TUPLE_PROJECT_OP > { |
754 |
|
typedef ::cvc5::TupleProjectOp T; |
755 |
|
};/* ConstantMapReverse< ::cvc5::kind::TUPLE_PROJECT_OP > */ |
756 |
|
|
757 |
|
template <> |
758 |
|
struct ConstantMap< ::cvc5::EmptySet > { |
759 |
|
// typedef THEORY_SETS OwningTheory; |
760 |
|
enum { kind = ::cvc5::kind::EMPTYSET }; |
761 |
|
};/* ConstantMap< ::cvc5::EmptySet > */ |
762 |
|
|
763 |
|
template <> |
764 |
|
struct ConstantMapReverse< ::cvc5::kind::EMPTYSET > { |
765 |
|
typedef ::cvc5::EmptySet T; |
766 |
|
};/* ConstantMapReverse< ::cvc5::kind::EMPTYSET > */ |
767 |
|
|
768 |
|
template <> |
769 |
|
struct ConstantMap< ::cvc5::SingletonOp > { |
770 |
|
// typedef THEORY_SETS OwningTheory; |
771 |
|
enum { kind = ::cvc5::kind::SINGLETON_OP }; |
772 |
|
};/* ConstantMap< ::cvc5::SingletonOp > */ |
773 |
|
|
774 |
|
template <> |
775 |
|
struct ConstantMapReverse< ::cvc5::kind::SINGLETON_OP > { |
776 |
|
typedef ::cvc5::SingletonOp T; |
777 |
|
};/* ConstantMapReverse< ::cvc5::kind::SINGLETON_OP > */ |
778 |
|
|
779 |
|
template <> |
780 |
|
struct ConstantMap< ::cvc5::EmptyBag > { |
781 |
|
// typedef THEORY_BAGS OwningTheory; |
782 |
|
enum { kind = ::cvc5::kind::EMPTYBAG }; |
783 |
|
};/* ConstantMap< ::cvc5::EmptyBag > */ |
784 |
|
|
785 |
|
template <> |
786 |
|
struct ConstantMapReverse< ::cvc5::kind::EMPTYBAG > { |
787 |
|
typedef ::cvc5::EmptyBag T; |
788 |
|
};/* ConstantMapReverse< ::cvc5::kind::EMPTYBAG > */ |
789 |
|
|
790 |
|
template <> |
791 |
|
struct ConstantMap< ::cvc5::MakeBagOp > { |
792 |
|
// typedef THEORY_BAGS OwningTheory; |
793 |
|
enum { kind = ::cvc5::kind::MK_BAG_OP }; |
794 |
|
};/* ConstantMap< ::cvc5::MakeBagOp > */ |
795 |
|
|
796 |
|
template <> |
797 |
|
struct ConstantMapReverse< ::cvc5::kind::MK_BAG_OP > { |
798 |
|
typedef ::cvc5::MakeBagOp T; |
799 |
|
};/* ConstantMapReverse< ::cvc5::kind::MK_BAG_OP > */ |
800 |
|
|
801 |
|
template <> |
802 |
|
struct ConstantMap< ::cvc5::String > { |
803 |
|
// typedef THEORY_STRINGS OwningTheory; |
804 |
|
enum { kind = ::cvc5::kind::CONST_STRING }; |
805 |
|
};/* ConstantMap< ::cvc5::String > */ |
806 |
|
|
807 |
|
template <> |
808 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_STRING > { |
809 |
|
typedef ::cvc5::String T; |
810 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_STRING > */ |
811 |
|
|
812 |
|
template <> |
813 |
|
struct ConstantMap< ::cvc5::Sequence > { |
814 |
|
// typedef THEORY_STRINGS OwningTheory; |
815 |
|
enum { kind = ::cvc5::kind::CONST_SEQUENCE }; |
816 |
|
};/* ConstantMap< ::cvc5::Sequence > */ |
817 |
|
|
818 |
|
template <> |
819 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_SEQUENCE > { |
820 |
|
typedef ::cvc5::Sequence T; |
821 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_SEQUENCE > */ |
822 |
|
|
823 |
|
template <> |
824 |
|
struct ConstantMap< ::cvc5::RegExpRepeat > { |
825 |
|
// typedef THEORY_STRINGS OwningTheory; |
826 |
|
enum { kind = ::cvc5::kind::REGEXP_REPEAT_OP }; |
827 |
|
};/* ConstantMap< ::cvc5::RegExpRepeat > */ |
828 |
|
|
829 |
|
template <> |
830 |
|
struct ConstantMapReverse< ::cvc5::kind::REGEXP_REPEAT_OP > { |
831 |
|
typedef ::cvc5::RegExpRepeat T; |
832 |
|
};/* ConstantMapReverse< ::cvc5::kind::REGEXP_REPEAT_OP > */ |
833 |
|
|
834 |
|
template <> |
835 |
|
struct ConstantMap< ::cvc5::RegExpLoop > { |
836 |
|
// typedef THEORY_STRINGS OwningTheory; |
837 |
|
enum { kind = ::cvc5::kind::REGEXP_LOOP_OP }; |
838 |
|
};/* ConstantMap< ::cvc5::RegExpLoop > */ |
839 |
|
|
840 |
|
template <> |
841 |
|
struct ConstantMapReverse< ::cvc5::kind::REGEXP_LOOP_OP > { |
842 |
|
typedef ::cvc5::RegExpLoop T; |
843 |
|
};/* ConstantMapReverse< ::cvc5::kind::REGEXP_LOOP_OP > */ |
844 |
|
|
845 |
|
// clang-format on |
846 |
|
|
847 |
|
struct NodeValueConstPrinter |
848 |
|
{ |
849 |
|
static void toStream(std::ostream& out, const ::cvc5::expr::NodeValue* nv); |
850 |
|
static void toStream(std::ostream& out, TNode n); |
851 |
|
}; |
852 |
|
|
853 |
|
/** |
854 |
|
* Cleanup to be performed when a NodeValue zombie is collected, and |
855 |
|
* it has CONSTANT metakind. This calls the destructor for the underlying |
856 |
|
* C++ type representing the constant value. See |
857 |
|
* NodeManager::reclaimZombies() for more information. |
858 |
|
* |
859 |
|
* This doesn't support "non-inlined" NodeValues, which shouldn't need this |
860 |
|
* kind of cleanup. |
861 |
|
*/ |
862 |
|
void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv); |
863 |
|
|
864 |
|
/** Return the minimum arity of the given kind. */ |
865 |
|
uint32_t getMinArityForKind(::cvc5::Kind k); |
866 |
|
/** Return the maximum arity of the given kind. */ |
867 |
|
uint32_t getMaxArityForKind(::cvc5::Kind k); |
868 |
|
|
869 |
|
} // namespace metakind |
870 |
|
|
871 |
|
/** |
872 |
|
* Map a kind of the operator to the kind of the enclosing expression. For |
873 |
|
* example, since the kind of functions is just VARIABLE, it should map |
874 |
|
* VARIABLE to APPLY_UF. |
875 |
|
*/ |
876 |
|
Kind operatorToKind(::cvc5::expr::NodeValue* nv); |
877 |
|
|
878 |
|
} // namespace kind |
879 |
|
|
880 |
|
} // namespace cvc5 |
881 |
|
|
882 |
|
#endif /* CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP */ |