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