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-11-07/src/expr/metakind_template.h /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-11-07/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 |
799208398 |
inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const { |
137 |
799208398 |
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 |
|
#ifdef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP |
149 |
|
|
150 |
|
namespace cvc5 { |
151 |
|
|
152 |
|
// clang-format off |
153 |
|
|
154 |
|
class UninterpretedConstant; |
155 |
|
class AbstractValue; |
156 |
|
class CardinalityConstraint; |
157 |
|
class CombinedCardinalityConstraint; |
158 |
|
struct Divisible; |
159 |
|
class Rational; |
160 |
|
struct IndexedRootPredicate; |
161 |
|
struct IntAnd; |
162 |
|
struct BitVectorSize; |
163 |
|
class BitVector; |
164 |
|
struct BitVectorBitOf; |
165 |
|
struct BitVectorExtract; |
166 |
|
struct BitVectorRepeat; |
167 |
|
struct BitVectorRotateLeft; |
168 |
|
struct BitVectorRotateRight; |
169 |
|
struct BitVectorSignExtend; |
170 |
|
struct BitVectorZeroExtend; |
171 |
|
struct IntToBitVector; |
172 |
|
class FloatingPoint; |
173 |
|
enum class RoundingMode; |
174 |
|
class FloatingPointSize; |
175 |
|
class FloatingPointToFPIEEEBitVector; |
176 |
|
class FloatingPointToFPFloatingPoint; |
177 |
|
class FloatingPointToFPReal; |
178 |
|
class FloatingPointToFPSignedBitVector; |
179 |
|
class FloatingPointToFPUnsignedBitVector; |
180 |
|
class FloatingPointToFPGeneric; |
181 |
|
class FloatingPointToUBV; |
182 |
|
class FloatingPointToUBVTotal; |
183 |
|
class FloatingPointToSBV; |
184 |
|
class FloatingPointToSBVTotal; |
185 |
|
class ArrayStoreAll; |
186 |
|
class DatatypeIndexConstant; |
187 |
|
class AscriptionType; |
188 |
|
class TupleProjectOp; |
189 |
|
class CodatatypeBoundVariable; |
190 |
|
class EmptySet; |
191 |
|
class SingletonOp; |
192 |
|
class EmptyBag; |
193 |
|
class MakeBagOp; |
194 |
|
class String; |
195 |
|
class Sequence; |
196 |
|
struct RegExpRepeat; |
197 |
|
struct RegExpLoop; |
198 |
|
// clang-format on |
199 |
|
|
200 |
|
namespace expr { |
201 |
|
// clang-format off |
202 |
|
|
203 |
|
template <> |
204 |
|
UninterpretedConstant const& NodeValue::getConst< UninterpretedConstant >() const; |
205 |
|
|
206 |
|
template <> |
207 |
|
AbstractValue const& NodeValue::getConst< AbstractValue >() const; |
208 |
|
|
209 |
|
template <> |
210 |
|
Kind const& NodeValue::getConst< Kind >() const; |
211 |
|
|
212 |
|
template <> |
213 |
|
TypeConstant const& NodeValue::getConst< TypeConstant >() const; |
214 |
|
|
215 |
|
template <> |
216 |
|
bool const& NodeValue::getConst< bool >() const; |
217 |
|
|
218 |
|
template <> |
219 |
|
CardinalityConstraint const& NodeValue::getConst< CardinalityConstraint >() const; |
220 |
|
|
221 |
|
template <> |
222 |
|
CombinedCardinalityConstraint const& NodeValue::getConst< CombinedCardinalityConstraint >() const; |
223 |
|
|
224 |
|
template <> |
225 |
|
Divisible const& NodeValue::getConst< Divisible >() const; |
226 |
|
|
227 |
|
template <> |
228 |
|
Rational const& NodeValue::getConst< Rational >() const; |
229 |
|
|
230 |
|
template <> |
231 |
|
IndexedRootPredicate const& NodeValue::getConst< IndexedRootPredicate >() const; |
232 |
|
|
233 |
|
template <> |
234 |
|
IntAnd const& NodeValue::getConst< IntAnd >() const; |
235 |
|
|
236 |
|
template <> |
237 |
|
BitVectorSize const& NodeValue::getConst< BitVectorSize >() const; |
238 |
|
|
239 |
|
template <> |
240 |
|
BitVector const& NodeValue::getConst< BitVector >() const; |
241 |
|
|
242 |
|
template <> |
243 |
|
BitVectorBitOf const& NodeValue::getConst< BitVectorBitOf >() const; |
244 |
|
|
245 |
|
template <> |
246 |
|
BitVectorExtract const& NodeValue::getConst< BitVectorExtract >() const; |
247 |
|
|
248 |
|
template <> |
249 |
|
BitVectorRepeat const& NodeValue::getConst< BitVectorRepeat >() const; |
250 |
|
|
251 |
|
template <> |
252 |
|
BitVectorRotateLeft const& NodeValue::getConst< BitVectorRotateLeft >() const; |
253 |
|
|
254 |
|
template <> |
255 |
|
BitVectorRotateRight const& NodeValue::getConst< BitVectorRotateRight >() const; |
256 |
|
|
257 |
|
template <> |
258 |
|
BitVectorSignExtend const& NodeValue::getConst< BitVectorSignExtend >() const; |
259 |
|
|
260 |
|
template <> |
261 |
|
BitVectorZeroExtend const& NodeValue::getConst< BitVectorZeroExtend >() const; |
262 |
|
|
263 |
|
template <> |
264 |
|
IntToBitVector const& NodeValue::getConst< IntToBitVector >() const; |
265 |
|
|
266 |
|
template <> |
267 |
|
FloatingPoint const& NodeValue::getConst< FloatingPoint >() const; |
268 |
|
|
269 |
|
template <> |
270 |
|
RoundingMode const& NodeValue::getConst< RoundingMode >() const; |
271 |
|
|
272 |
|
template <> |
273 |
|
FloatingPointSize const& NodeValue::getConst< FloatingPointSize >() const; |
274 |
|
|
275 |
|
template <> |
276 |
|
FloatingPointToFPIEEEBitVector const& NodeValue::getConst< FloatingPointToFPIEEEBitVector >() const; |
277 |
|
|
278 |
|
template <> |
279 |
|
FloatingPointToFPFloatingPoint const& NodeValue::getConst< FloatingPointToFPFloatingPoint >() const; |
280 |
|
|
281 |
|
template <> |
282 |
|
FloatingPointToFPReal const& NodeValue::getConst< FloatingPointToFPReal >() const; |
283 |
|
|
284 |
|
template <> |
285 |
|
FloatingPointToFPSignedBitVector const& NodeValue::getConst< FloatingPointToFPSignedBitVector >() const; |
286 |
|
|
287 |
|
template <> |
288 |
|
FloatingPointToFPUnsignedBitVector const& NodeValue::getConst< FloatingPointToFPUnsignedBitVector >() const; |
289 |
|
|
290 |
|
template <> |
291 |
|
FloatingPointToFPGeneric const& NodeValue::getConst< FloatingPointToFPGeneric >() const; |
292 |
|
|
293 |
|
template <> |
294 |
|
FloatingPointToUBV const& NodeValue::getConst< FloatingPointToUBV >() const; |
295 |
|
|
296 |
|
template <> |
297 |
|
FloatingPointToUBVTotal const& NodeValue::getConst< FloatingPointToUBVTotal >() const; |
298 |
|
|
299 |
|
template <> |
300 |
|
FloatingPointToSBV const& NodeValue::getConst< FloatingPointToSBV >() const; |
301 |
|
|
302 |
|
template <> |
303 |
|
FloatingPointToSBVTotal const& NodeValue::getConst< FloatingPointToSBVTotal >() const; |
304 |
|
|
305 |
|
template <> |
306 |
|
ArrayStoreAll const& NodeValue::getConst< ArrayStoreAll >() const; |
307 |
|
|
308 |
|
template <> |
309 |
|
DatatypeIndexConstant const& NodeValue::getConst< DatatypeIndexConstant >() const; |
310 |
|
|
311 |
|
template <> |
312 |
|
AscriptionType const& NodeValue::getConst< AscriptionType >() const; |
313 |
|
|
314 |
|
template <> |
315 |
|
TupleProjectOp const& NodeValue::getConst< TupleProjectOp >() const; |
316 |
|
|
317 |
|
template <> |
318 |
|
CodatatypeBoundVariable const& NodeValue::getConst< CodatatypeBoundVariable >() const; |
319 |
|
|
320 |
|
template <> |
321 |
|
EmptySet const& NodeValue::getConst< EmptySet >() const; |
322 |
|
|
323 |
|
template <> |
324 |
|
SingletonOp const& NodeValue::getConst< SingletonOp >() const; |
325 |
|
|
326 |
|
template <> |
327 |
|
EmptyBag const& NodeValue::getConst< EmptyBag >() const; |
328 |
|
|
329 |
|
template <> |
330 |
|
MakeBagOp const& NodeValue::getConst< MakeBagOp >() const; |
331 |
|
|
332 |
|
template <> |
333 |
|
String const& NodeValue::getConst< String >() const; |
334 |
|
|
335 |
|
template <> |
336 |
|
Sequence const& NodeValue::getConst< Sequence >() const; |
337 |
|
|
338 |
|
template <> |
339 |
|
RegExpRepeat const& NodeValue::getConst< RegExpRepeat >() const; |
340 |
|
|
341 |
|
template <> |
342 |
|
RegExpLoop const& NodeValue::getConst< RegExpLoop >() const; |
343 |
|
|
344 |
|
// clang-format on |
345 |
|
} // namespace expr |
346 |
|
|
347 |
|
namespace kind { |
348 |
|
namespace metakind { |
349 |
|
|
350 |
|
template <Kind k, bool pool> |
351 |
564576448 |
inline bool NodeValueConstCompare<k, pool>::compare( |
352 |
|
const ::cvc5::expr::NodeValue* x, const ::cvc5::expr::NodeValue* y) |
353 |
|
{ |
354 |
|
typedef typename ConstantMapReverse<k>::T T; |
355 |
|
if(pool) { |
356 |
564576448 |
if(x->d_nchildren == 1) { |
357 |
277340216 |
Assert(y->d_nchildren == 0); |
358 |
277340216 |
return compare(y, x); |
359 |
287236232 |
} else if(y->d_nchildren == 1) { |
360 |
277340216 |
Assert(x->d_nchildren == 0); |
361 |
277340216 |
return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]); |
362 |
|
} |
363 |
|
} |
364 |
|
|
365 |
9896016 |
Assert(x->d_nchildren == 0); |
366 |
9896016 |
Assert(y->d_nchildren == 0); |
367 |
9896016 |
return x->getConst<T>() == y->getConst<T>(); |
368 |
|
} |
369 |
|
|
370 |
|
template <Kind k, bool pool> |
371 |
|
inline size_t NodeValueConstCompare<k, pool>::constHash( |
372 |
|
const ::cvc5::expr::NodeValue* nv) |
373 |
|
{ |
374 |
|
typedef typename ConstantMapReverse<k>::T T; |
375 |
|
return nv->getConst<T>().hash(); |
376 |
|
} |
377 |
|
|
378 |
|
// clang-format off |
379 |
|
|
380 |
|
template <> |
381 |
|
struct ConstantMap< UninterpretedConstant > { |
382 |
|
// typedef THEORY_BUILTIN OwningTheory; |
383 |
|
enum { kind = ::cvc5::kind::UNINTERPRETED_CONSTANT }; |
384 |
|
};/* ConstantMap< UninterpretedConstant > */ |
385 |
|
|
386 |
|
template <> |
387 |
|
struct ConstantMapReverse< ::cvc5::kind::UNINTERPRETED_CONSTANT > { |
388 |
|
typedef UninterpretedConstant T; |
389 |
|
};/* ConstantMapReverse< ::cvc5::kind::UNINTERPRETED_CONSTANT > */ |
390 |
|
|
391 |
|
template <> |
392 |
|
struct ConstantMap< AbstractValue > { |
393 |
|
// typedef THEORY_BUILTIN OwningTheory; |
394 |
|
enum { kind = ::cvc5::kind::ABSTRACT_VALUE }; |
395 |
|
};/* ConstantMap< AbstractValue > */ |
396 |
|
|
397 |
|
template <> |
398 |
|
struct ConstantMapReverse< ::cvc5::kind::ABSTRACT_VALUE > { |
399 |
|
typedef AbstractValue T; |
400 |
|
};/* ConstantMapReverse< ::cvc5::kind::ABSTRACT_VALUE > */ |
401 |
|
|
402 |
|
template <> |
403 |
|
struct ConstantMap< Kind > { |
404 |
|
// typedef THEORY_BUILTIN OwningTheory; |
405 |
|
enum { kind = ::cvc5::kind::BUILTIN }; |
406 |
|
};/* ConstantMap< Kind > */ |
407 |
|
|
408 |
|
template <> |
409 |
|
struct ConstantMapReverse< ::cvc5::kind::BUILTIN > { |
410 |
|
typedef Kind T; |
411 |
|
};/* ConstantMapReverse< ::cvc5::kind::BUILTIN > */ |
412 |
|
|
413 |
|
template <> |
414 |
|
struct ConstantMap< TypeConstant > { |
415 |
|
// typedef THEORY_BUILTIN OwningTheory; |
416 |
|
enum { kind = ::cvc5::kind::TYPE_CONSTANT }; |
417 |
|
};/* ConstantMap< TypeConstant > */ |
418 |
|
|
419 |
|
template <> |
420 |
|
struct ConstantMapReverse< ::cvc5::kind::TYPE_CONSTANT > { |
421 |
|
typedef TypeConstant T; |
422 |
|
};/* ConstantMapReverse< ::cvc5::kind::TYPE_CONSTANT > */ |
423 |
|
|
424 |
|
template <> |
425 |
|
struct ConstantMap< bool > { |
426 |
|
// typedef THEORY_BOOL OwningTheory; |
427 |
|
enum { kind = ::cvc5::kind::CONST_BOOLEAN }; |
428 |
|
};/* ConstantMap< bool > */ |
429 |
|
|
430 |
|
template <> |
431 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_BOOLEAN > { |
432 |
|
typedef bool T; |
433 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_BOOLEAN > */ |
434 |
|
|
435 |
|
template <> |
436 |
|
struct ConstantMap< CardinalityConstraint > { |
437 |
|
// typedef THEORY_UF OwningTheory; |
438 |
|
enum { kind = ::cvc5::kind::CARDINALITY_CONSTRAINT_OP }; |
439 |
|
};/* ConstantMap< CardinalityConstraint > */ |
440 |
|
|
441 |
|
template <> |
442 |
|
struct ConstantMapReverse< ::cvc5::kind::CARDINALITY_CONSTRAINT_OP > { |
443 |
|
typedef CardinalityConstraint T; |
444 |
|
};/* ConstantMapReverse< ::cvc5::kind::CARDINALITY_CONSTRAINT_OP > */ |
445 |
|
|
446 |
|
template <> |
447 |
|
struct ConstantMap< CombinedCardinalityConstraint > { |
448 |
|
// typedef THEORY_UF OwningTheory; |
449 |
|
enum { kind = ::cvc5::kind::COMBINED_CARDINALITY_CONSTRAINT_OP }; |
450 |
|
};/* ConstantMap< CombinedCardinalityConstraint > */ |
451 |
|
|
452 |
|
template <> |
453 |
|
struct ConstantMapReverse< ::cvc5::kind::COMBINED_CARDINALITY_CONSTRAINT_OP > { |
454 |
|
typedef CombinedCardinalityConstraint T; |
455 |
|
};/* ConstantMapReverse< ::cvc5::kind::COMBINED_CARDINALITY_CONSTRAINT_OP > */ |
456 |
|
|
457 |
|
template <> |
458 |
|
struct ConstantMap< Divisible > { |
459 |
|
// typedef THEORY_ARITH OwningTheory; |
460 |
|
enum { kind = ::cvc5::kind::DIVISIBLE_OP }; |
461 |
|
};/* ConstantMap< Divisible > */ |
462 |
|
|
463 |
|
template <> |
464 |
|
struct ConstantMapReverse< ::cvc5::kind::DIVISIBLE_OP > { |
465 |
|
typedef Divisible T; |
466 |
|
};/* ConstantMapReverse< ::cvc5::kind::DIVISIBLE_OP > */ |
467 |
|
|
468 |
|
template <> |
469 |
|
struct ConstantMap< Rational > { |
470 |
|
// typedef THEORY_ARITH OwningTheory; |
471 |
|
enum { kind = ::cvc5::kind::CONST_RATIONAL }; |
472 |
|
};/* ConstantMap< Rational > */ |
473 |
|
|
474 |
|
template <> |
475 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_RATIONAL > { |
476 |
|
typedef Rational T; |
477 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_RATIONAL > */ |
478 |
|
|
479 |
|
template <> |
480 |
|
struct ConstantMap< IndexedRootPredicate > { |
481 |
|
// typedef THEORY_ARITH OwningTheory; |
482 |
|
enum { kind = ::cvc5::kind::INDEXED_ROOT_PREDICATE_OP }; |
483 |
|
};/* ConstantMap< IndexedRootPredicate > */ |
484 |
|
|
485 |
|
template <> |
486 |
|
struct ConstantMapReverse< ::cvc5::kind::INDEXED_ROOT_PREDICATE_OP > { |
487 |
|
typedef IndexedRootPredicate T; |
488 |
|
};/* ConstantMapReverse< ::cvc5::kind::INDEXED_ROOT_PREDICATE_OP > */ |
489 |
|
|
490 |
|
template <> |
491 |
|
struct ConstantMap< IntAnd > { |
492 |
|
// typedef THEORY_ARITH OwningTheory; |
493 |
|
enum { kind = ::cvc5::kind::IAND_OP }; |
494 |
|
};/* ConstantMap< IntAnd > */ |
495 |
|
|
496 |
|
template <> |
497 |
|
struct ConstantMapReverse< ::cvc5::kind::IAND_OP > { |
498 |
|
typedef IntAnd T; |
499 |
|
};/* ConstantMapReverse< ::cvc5::kind::IAND_OP > */ |
500 |
|
|
501 |
|
template <> |
502 |
|
struct ConstantMap< BitVectorSize > { |
503 |
|
// typedef THEORY_BV OwningTheory; |
504 |
|
enum { kind = ::cvc5::kind::BITVECTOR_TYPE }; |
505 |
|
};/* ConstantMap< BitVectorSize > */ |
506 |
|
|
507 |
|
template <> |
508 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_TYPE > { |
509 |
|
typedef BitVectorSize T; |
510 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_TYPE > */ |
511 |
|
|
512 |
|
template <> |
513 |
|
struct ConstantMap< BitVector > { |
514 |
|
// typedef THEORY_BV OwningTheory; |
515 |
|
enum { kind = ::cvc5::kind::CONST_BITVECTOR }; |
516 |
|
};/* ConstantMap< BitVector > */ |
517 |
|
|
518 |
|
template <> |
519 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_BITVECTOR > { |
520 |
|
typedef BitVector T; |
521 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_BITVECTOR > */ |
522 |
|
|
523 |
|
template <> |
524 |
|
struct ConstantMap< BitVectorBitOf > { |
525 |
|
// typedef THEORY_BV OwningTheory; |
526 |
|
enum { kind = ::cvc5::kind::BITVECTOR_BITOF_OP }; |
527 |
|
};/* ConstantMap< BitVectorBitOf > */ |
528 |
|
|
529 |
|
template <> |
530 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_BITOF_OP > { |
531 |
|
typedef BitVectorBitOf T; |
532 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_BITOF_OP > */ |
533 |
|
|
534 |
|
template <> |
535 |
|
struct ConstantMap< BitVectorExtract > { |
536 |
|
// typedef THEORY_BV OwningTheory; |
537 |
|
enum { kind = ::cvc5::kind::BITVECTOR_EXTRACT_OP }; |
538 |
|
};/* ConstantMap< BitVectorExtract > */ |
539 |
|
|
540 |
|
template <> |
541 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_EXTRACT_OP > { |
542 |
|
typedef BitVectorExtract T; |
543 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_EXTRACT_OP > */ |
544 |
|
|
545 |
|
template <> |
546 |
|
struct ConstantMap< BitVectorRepeat > { |
547 |
|
// typedef THEORY_BV OwningTheory; |
548 |
|
enum { kind = ::cvc5::kind::BITVECTOR_REPEAT_OP }; |
549 |
|
};/* ConstantMap< BitVectorRepeat > */ |
550 |
|
|
551 |
|
template <> |
552 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_REPEAT_OP > { |
553 |
|
typedef BitVectorRepeat T; |
554 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_REPEAT_OP > */ |
555 |
|
|
556 |
|
template <> |
557 |
|
struct ConstantMap< BitVectorRotateLeft > { |
558 |
|
// typedef THEORY_BV OwningTheory; |
559 |
|
enum { kind = ::cvc5::kind::BITVECTOR_ROTATE_LEFT_OP }; |
560 |
|
};/* ConstantMap< BitVectorRotateLeft > */ |
561 |
|
|
562 |
|
template <> |
563 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_ROTATE_LEFT_OP > { |
564 |
|
typedef BitVectorRotateLeft T; |
565 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_ROTATE_LEFT_OP > */ |
566 |
|
|
567 |
|
template <> |
568 |
|
struct ConstantMap< BitVectorRotateRight > { |
569 |
|
// typedef THEORY_BV OwningTheory; |
570 |
|
enum { kind = ::cvc5::kind::BITVECTOR_ROTATE_RIGHT_OP }; |
571 |
|
};/* ConstantMap< BitVectorRotateRight > */ |
572 |
|
|
573 |
|
template <> |
574 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_ROTATE_RIGHT_OP > { |
575 |
|
typedef BitVectorRotateRight T; |
576 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_ROTATE_RIGHT_OP > */ |
577 |
|
|
578 |
|
template <> |
579 |
|
struct ConstantMap< BitVectorSignExtend > { |
580 |
|
// typedef THEORY_BV OwningTheory; |
581 |
|
enum { kind = ::cvc5::kind::BITVECTOR_SIGN_EXTEND_OP }; |
582 |
|
};/* ConstantMap< BitVectorSignExtend > */ |
583 |
|
|
584 |
|
template <> |
585 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_SIGN_EXTEND_OP > { |
586 |
|
typedef BitVectorSignExtend T; |
587 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_SIGN_EXTEND_OP > */ |
588 |
|
|
589 |
|
template <> |
590 |
|
struct ConstantMap< BitVectorZeroExtend > { |
591 |
|
// typedef THEORY_BV OwningTheory; |
592 |
|
enum { kind = ::cvc5::kind::BITVECTOR_ZERO_EXTEND_OP }; |
593 |
|
};/* ConstantMap< BitVectorZeroExtend > */ |
594 |
|
|
595 |
|
template <> |
596 |
|
struct ConstantMapReverse< ::cvc5::kind::BITVECTOR_ZERO_EXTEND_OP > { |
597 |
|
typedef BitVectorZeroExtend T; |
598 |
|
};/* ConstantMapReverse< ::cvc5::kind::BITVECTOR_ZERO_EXTEND_OP > */ |
599 |
|
|
600 |
|
template <> |
601 |
|
struct ConstantMap< IntToBitVector > { |
602 |
|
// typedef THEORY_BV OwningTheory; |
603 |
|
enum { kind = ::cvc5::kind::INT_TO_BITVECTOR_OP }; |
604 |
|
};/* ConstantMap< IntToBitVector > */ |
605 |
|
|
606 |
|
template <> |
607 |
|
struct ConstantMapReverse< ::cvc5::kind::INT_TO_BITVECTOR_OP > { |
608 |
|
typedef IntToBitVector T; |
609 |
|
};/* ConstantMapReverse< ::cvc5::kind::INT_TO_BITVECTOR_OP > */ |
610 |
|
|
611 |
|
template <> |
612 |
|
struct ConstantMap< FloatingPoint > { |
613 |
|
// typedef THEORY_FP OwningTheory; |
614 |
|
enum { kind = ::cvc5::kind::CONST_FLOATINGPOINT }; |
615 |
|
};/* ConstantMap< FloatingPoint > */ |
616 |
|
|
617 |
|
template <> |
618 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_FLOATINGPOINT > { |
619 |
|
typedef FloatingPoint T; |
620 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_FLOATINGPOINT > */ |
621 |
|
|
622 |
|
template <> |
623 |
|
struct ConstantMap< RoundingMode > { |
624 |
|
// typedef THEORY_FP OwningTheory; |
625 |
|
enum { kind = ::cvc5::kind::CONST_ROUNDINGMODE }; |
626 |
|
};/* ConstantMap< RoundingMode > */ |
627 |
|
|
628 |
|
template <> |
629 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_ROUNDINGMODE > { |
630 |
|
typedef RoundingMode T; |
631 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_ROUNDINGMODE > */ |
632 |
|
|
633 |
|
template <> |
634 |
|
struct ConstantMap< FloatingPointSize > { |
635 |
|
// typedef THEORY_FP OwningTheory; |
636 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TYPE }; |
637 |
|
};/* ConstantMap< FloatingPointSize > */ |
638 |
|
|
639 |
|
template <> |
640 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TYPE > { |
641 |
|
typedef FloatingPointSize T; |
642 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TYPE > */ |
643 |
|
|
644 |
|
template <> |
645 |
|
struct ConstantMap< FloatingPointToFPIEEEBitVector > { |
646 |
|
// typedef THEORY_FP OwningTheory; |
647 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP }; |
648 |
|
};/* ConstantMap< FloatingPointToFPIEEEBitVector > */ |
649 |
|
|
650 |
|
template <> |
651 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP > { |
652 |
|
typedef FloatingPointToFPIEEEBitVector T; |
653 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP > */ |
654 |
|
|
655 |
|
template <> |
656 |
|
struct ConstantMap< FloatingPointToFPFloatingPoint > { |
657 |
|
// typedef THEORY_FP OwningTheory; |
658 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP }; |
659 |
|
};/* ConstantMap< FloatingPointToFPFloatingPoint > */ |
660 |
|
|
661 |
|
template <> |
662 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP > { |
663 |
|
typedef FloatingPointToFPFloatingPoint T; |
664 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP > */ |
665 |
|
|
666 |
|
template <> |
667 |
|
struct ConstantMap< FloatingPointToFPReal > { |
668 |
|
// typedef THEORY_FP OwningTheory; |
669 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_FP_REAL_OP }; |
670 |
|
};/* ConstantMap< FloatingPointToFPReal > */ |
671 |
|
|
672 |
|
template <> |
673 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_REAL_OP > { |
674 |
|
typedef FloatingPointToFPReal T; |
675 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_REAL_OP > */ |
676 |
|
|
677 |
|
template <> |
678 |
|
struct ConstantMap< FloatingPointToFPSignedBitVector > { |
679 |
|
// typedef THEORY_FP OwningTheory; |
680 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP }; |
681 |
|
};/* ConstantMap< FloatingPointToFPSignedBitVector > */ |
682 |
|
|
683 |
|
template <> |
684 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP > { |
685 |
|
typedef FloatingPointToFPSignedBitVector T; |
686 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP > */ |
687 |
|
|
688 |
|
template <> |
689 |
|
struct ConstantMap< FloatingPointToFPUnsignedBitVector > { |
690 |
|
// typedef THEORY_FP OwningTheory; |
691 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP }; |
692 |
|
};/* ConstantMap< FloatingPointToFPUnsignedBitVector > */ |
693 |
|
|
694 |
|
template <> |
695 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP > { |
696 |
|
typedef FloatingPointToFPUnsignedBitVector T; |
697 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP > */ |
698 |
|
|
699 |
|
template <> |
700 |
|
struct ConstantMap< FloatingPointToFPGeneric > { |
701 |
|
// typedef THEORY_FP OwningTheory; |
702 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_FP_GENERIC_OP }; |
703 |
|
};/* ConstantMap< FloatingPointToFPGeneric > */ |
704 |
|
|
705 |
|
template <> |
706 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_GENERIC_OP > { |
707 |
|
typedef FloatingPointToFPGeneric T; |
708 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_FP_GENERIC_OP > */ |
709 |
|
|
710 |
|
template <> |
711 |
|
struct ConstantMap< FloatingPointToUBV > { |
712 |
|
// typedef THEORY_FP OwningTheory; |
713 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_UBV_OP }; |
714 |
|
};/* ConstantMap< FloatingPointToUBV > */ |
715 |
|
|
716 |
|
template <> |
717 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_UBV_OP > { |
718 |
|
typedef FloatingPointToUBV T; |
719 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_UBV_OP > */ |
720 |
|
|
721 |
|
template <> |
722 |
|
struct ConstantMap< FloatingPointToUBVTotal > { |
723 |
|
// typedef THEORY_FP OwningTheory; |
724 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_UBV_TOTAL_OP }; |
725 |
|
};/* ConstantMap< FloatingPointToUBVTotal > */ |
726 |
|
|
727 |
|
template <> |
728 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_UBV_TOTAL_OP > { |
729 |
|
typedef FloatingPointToUBVTotal T; |
730 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_UBV_TOTAL_OP > */ |
731 |
|
|
732 |
|
template <> |
733 |
|
struct ConstantMap< FloatingPointToSBV > { |
734 |
|
// typedef THEORY_FP OwningTheory; |
735 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_SBV_OP }; |
736 |
|
};/* ConstantMap< FloatingPointToSBV > */ |
737 |
|
|
738 |
|
template <> |
739 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_SBV_OP > { |
740 |
|
typedef FloatingPointToSBV T; |
741 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_SBV_OP > */ |
742 |
|
|
743 |
|
template <> |
744 |
|
struct ConstantMap< FloatingPointToSBVTotal > { |
745 |
|
// typedef THEORY_FP OwningTheory; |
746 |
|
enum { kind = ::cvc5::kind::FLOATINGPOINT_TO_SBV_TOTAL_OP }; |
747 |
|
};/* ConstantMap< FloatingPointToSBVTotal > */ |
748 |
|
|
749 |
|
template <> |
750 |
|
struct ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_SBV_TOTAL_OP > { |
751 |
|
typedef FloatingPointToSBVTotal T; |
752 |
|
};/* ConstantMapReverse< ::cvc5::kind::FLOATINGPOINT_TO_SBV_TOTAL_OP > */ |
753 |
|
|
754 |
|
template <> |
755 |
|
struct ConstantMap< ArrayStoreAll > { |
756 |
|
// typedef THEORY_ARRAYS OwningTheory; |
757 |
|
enum { kind = ::cvc5::kind::STORE_ALL }; |
758 |
|
};/* ConstantMap< ArrayStoreAll > */ |
759 |
|
|
760 |
|
template <> |
761 |
|
struct ConstantMapReverse< ::cvc5::kind::STORE_ALL > { |
762 |
|
typedef ArrayStoreAll T; |
763 |
|
};/* ConstantMapReverse< ::cvc5::kind::STORE_ALL > */ |
764 |
|
|
765 |
|
template <> |
766 |
|
struct ConstantMap< DatatypeIndexConstant > { |
767 |
|
// typedef THEORY_DATATYPES OwningTheory; |
768 |
|
enum { kind = ::cvc5::kind::DATATYPE_TYPE }; |
769 |
|
};/* ConstantMap< DatatypeIndexConstant > */ |
770 |
|
|
771 |
|
template <> |
772 |
|
struct ConstantMapReverse< ::cvc5::kind::DATATYPE_TYPE > { |
773 |
|
typedef DatatypeIndexConstant T; |
774 |
|
};/* ConstantMapReverse< ::cvc5::kind::DATATYPE_TYPE > */ |
775 |
|
|
776 |
|
template <> |
777 |
|
struct ConstantMap< AscriptionType > { |
778 |
|
// typedef THEORY_DATATYPES OwningTheory; |
779 |
|
enum { kind = ::cvc5::kind::ASCRIPTION_TYPE }; |
780 |
|
};/* ConstantMap< AscriptionType > */ |
781 |
|
|
782 |
|
template <> |
783 |
|
struct ConstantMapReverse< ::cvc5::kind::ASCRIPTION_TYPE > { |
784 |
|
typedef AscriptionType T; |
785 |
|
};/* ConstantMapReverse< ::cvc5::kind::ASCRIPTION_TYPE > */ |
786 |
|
|
787 |
|
template <> |
788 |
|
struct ConstantMap< TupleProjectOp > { |
789 |
|
// typedef THEORY_DATATYPES OwningTheory; |
790 |
|
enum { kind = ::cvc5::kind::TUPLE_PROJECT_OP }; |
791 |
|
};/* ConstantMap< TupleProjectOp > */ |
792 |
|
|
793 |
|
template <> |
794 |
|
struct ConstantMapReverse< ::cvc5::kind::TUPLE_PROJECT_OP > { |
795 |
|
typedef TupleProjectOp T; |
796 |
|
};/* ConstantMapReverse< ::cvc5::kind::TUPLE_PROJECT_OP > */ |
797 |
|
|
798 |
|
template <> |
799 |
|
struct ConstantMap< CodatatypeBoundVariable > { |
800 |
|
// typedef THEORY_DATATYPES OwningTheory; |
801 |
|
enum { kind = ::cvc5::kind::CODATATYPE_BOUND_VARIABLE }; |
802 |
|
};/* ConstantMap< CodatatypeBoundVariable > */ |
803 |
|
|
804 |
|
template <> |
805 |
|
struct ConstantMapReverse< ::cvc5::kind::CODATATYPE_BOUND_VARIABLE > { |
806 |
|
typedef CodatatypeBoundVariable T; |
807 |
|
};/* ConstantMapReverse< ::cvc5::kind::CODATATYPE_BOUND_VARIABLE > */ |
808 |
|
|
809 |
|
template <> |
810 |
|
struct ConstantMap< EmptySet > { |
811 |
|
// typedef THEORY_SETS OwningTheory; |
812 |
|
enum { kind = ::cvc5::kind::EMPTYSET }; |
813 |
|
};/* ConstantMap< EmptySet > */ |
814 |
|
|
815 |
|
template <> |
816 |
|
struct ConstantMapReverse< ::cvc5::kind::EMPTYSET > { |
817 |
|
typedef EmptySet T; |
818 |
|
};/* ConstantMapReverse< ::cvc5::kind::EMPTYSET > */ |
819 |
|
|
820 |
|
template <> |
821 |
|
struct ConstantMap< SingletonOp > { |
822 |
|
// typedef THEORY_SETS OwningTheory; |
823 |
|
enum { kind = ::cvc5::kind::SINGLETON_OP }; |
824 |
|
};/* ConstantMap< SingletonOp > */ |
825 |
|
|
826 |
|
template <> |
827 |
|
struct ConstantMapReverse< ::cvc5::kind::SINGLETON_OP > { |
828 |
|
typedef SingletonOp T; |
829 |
|
};/* ConstantMapReverse< ::cvc5::kind::SINGLETON_OP > */ |
830 |
|
|
831 |
|
template <> |
832 |
|
struct ConstantMap< EmptyBag > { |
833 |
|
// typedef THEORY_BAGS OwningTheory; |
834 |
|
enum { kind = ::cvc5::kind::EMPTYBAG }; |
835 |
|
};/* ConstantMap< EmptyBag > */ |
836 |
|
|
837 |
|
template <> |
838 |
|
struct ConstantMapReverse< ::cvc5::kind::EMPTYBAG > { |
839 |
|
typedef EmptyBag T; |
840 |
|
};/* ConstantMapReverse< ::cvc5::kind::EMPTYBAG > */ |
841 |
|
|
842 |
|
template <> |
843 |
|
struct ConstantMap< MakeBagOp > { |
844 |
|
// typedef THEORY_BAGS OwningTheory; |
845 |
|
enum { kind = ::cvc5::kind::MK_BAG_OP }; |
846 |
|
};/* ConstantMap< MakeBagOp > */ |
847 |
|
|
848 |
|
template <> |
849 |
|
struct ConstantMapReverse< ::cvc5::kind::MK_BAG_OP > { |
850 |
|
typedef MakeBagOp T; |
851 |
|
};/* ConstantMapReverse< ::cvc5::kind::MK_BAG_OP > */ |
852 |
|
|
853 |
|
template <> |
854 |
|
struct ConstantMap< String > { |
855 |
|
// typedef THEORY_STRINGS OwningTheory; |
856 |
|
enum { kind = ::cvc5::kind::CONST_STRING }; |
857 |
|
};/* ConstantMap< String > */ |
858 |
|
|
859 |
|
template <> |
860 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_STRING > { |
861 |
|
typedef String T; |
862 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_STRING > */ |
863 |
|
|
864 |
|
template <> |
865 |
|
struct ConstantMap< Sequence > { |
866 |
|
// typedef THEORY_STRINGS OwningTheory; |
867 |
|
enum { kind = ::cvc5::kind::CONST_SEQUENCE }; |
868 |
|
};/* ConstantMap< Sequence > */ |
869 |
|
|
870 |
|
template <> |
871 |
|
struct ConstantMapReverse< ::cvc5::kind::CONST_SEQUENCE > { |
872 |
|
typedef Sequence T; |
873 |
|
};/* ConstantMapReverse< ::cvc5::kind::CONST_SEQUENCE > */ |
874 |
|
|
875 |
|
template <> |
876 |
|
struct ConstantMap< RegExpRepeat > { |
877 |
|
// typedef THEORY_STRINGS OwningTheory; |
878 |
|
enum { kind = ::cvc5::kind::REGEXP_REPEAT_OP }; |
879 |
|
};/* ConstantMap< RegExpRepeat > */ |
880 |
|
|
881 |
|
template <> |
882 |
|
struct ConstantMapReverse< ::cvc5::kind::REGEXP_REPEAT_OP > { |
883 |
|
typedef RegExpRepeat T; |
884 |
|
};/* ConstantMapReverse< ::cvc5::kind::REGEXP_REPEAT_OP > */ |
885 |
|
|
886 |
|
template <> |
887 |
|
struct ConstantMap< RegExpLoop > { |
888 |
|
// typedef THEORY_STRINGS OwningTheory; |
889 |
|
enum { kind = ::cvc5::kind::REGEXP_LOOP_OP }; |
890 |
|
};/* ConstantMap< RegExpLoop > */ |
891 |
|
|
892 |
|
template <> |
893 |
|
struct ConstantMapReverse< ::cvc5::kind::REGEXP_LOOP_OP > { |
894 |
|
typedef RegExpLoop T; |
895 |
|
};/* ConstantMapReverse< ::cvc5::kind::REGEXP_LOOP_OP > */ |
896 |
|
|
897 |
|
// clang-format on |
898 |
|
|
899 |
|
struct NodeValueConstPrinter |
900 |
|
{ |
901 |
|
static void toStream(std::ostream& out, const ::cvc5::expr::NodeValue* nv); |
902 |
|
static void toStream(std::ostream& out, TNode n); |
903 |
|
}; |
904 |
|
|
905 |
|
/** |
906 |
|
* Cleanup to be performed when a NodeValue zombie is collected, and |
907 |
|
* it has CONSTANT metakind. This calls the destructor for the underlying |
908 |
|
* C++ type representing the constant value. See |
909 |
|
* NodeManager::reclaimZombies() for more information. |
910 |
|
* |
911 |
|
* This doesn't support "non-inlined" NodeValues, which shouldn't need this |
912 |
|
* kind of cleanup. |
913 |
|
*/ |
914 |
|
void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv); |
915 |
|
|
916 |
|
/** Return the minimum arity of the given kind. */ |
917 |
|
uint32_t getMinArityForKind(::cvc5::Kind k); |
918 |
|
/** Return the maximum arity of the given kind. */ |
919 |
|
uint32_t getMaxArityForKind(::cvc5::Kind k); |
920 |
|
|
921 |
|
} // namespace metakind |
922 |
|
|
923 |
|
/** |
924 |
|
* Map a kind of the operator to the kind of the enclosing expression. For |
925 |
|
* example, since the kind of functions is just VARIABLE, it should map |
926 |
|
* VARIABLE to APPLY_UF. |
927 |
|
*/ |
928 |
|
Kind operatorToKind(::cvc5::expr::NodeValue* nv); |
929 |
|
|
930 |
|
} // namespace kind |
931 |
|
|
932 |
|
} // namespace cvc5 |
933 |
|
|
934 |
|
#endif /* CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP */ |