SMTStabilizer API
Public API documentation for SMTStabilizer
Loading...
Searching...
No Matches
kind.cpp
Go to the documentation of this file.
1/* -*- Source -*-
2 *
3 * The Kind Enumeration
4 *
5 * Author: Fuqi Jia <jiafq@ios.ac.cn>
6 *
7 * Copyright (C) 2025 Fuqi Jia
8 *
9 * Permission is hereby granted, free of charge, to any person obtaining a
10 * copy of this software and associated documentation files (the "Software"),
11 * to deal in the Software without restriction, including without limitation
12 * the rights to use, copy, modify, merge, publish, distribute, sublicense,
13 * and/or sell copies of the Software, and to permit persons to whom the
14 * Software is furnished to do so, subject to the following conditions:
15 *
16 * The above copyright notice and this permission notice shall be included in
17 * all copies or substantial portions of the Software.
18 *
19 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
20 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
21 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
22 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
23 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
24 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
25 * DEALINGS IN THE SOFTWARE.
26 */
27
28// Modified by Xiang Zhang, 2026
29// Additional changes licensed under the MIT License
30
31#include "kind.h"
32
33namespace stabilizer::parser {
34
35std::string kindToString(const NODE_KIND &nk) {
36 switch (nk) {
37 case NODE_KIND::NT_UNKNOWN:
38 return "UNKNOWN_KIND";
39 case NODE_KIND::NT_ERROR:
40 return "ERROR";
41 case NODE_KIND::NT_NULL:
42 return "NULL";
43 case NODE_KIND::NT_CONST_TRUE:
44 return "true";
45 case NODE_KIND::NT_CONST_FALSE:
46 return "false";
47 case NODE_KIND::NT_CONST_ARRAY:
48 return "const_array";
49 case NODE_KIND::NT_PLACEHOLDER_VAR:
50 return "placeholder_var";
51 // CORE OPERATORS
52 case NODE_KIND::NT_EQ:
53 return "=";
54 case NODE_KIND::NT_DISTINCT:
55 return "distinct";
56 case NODE_KIND::NT_EQ_BOOL:
57 return "=";
58 case NODE_KIND::NT_EQ_OTHER:
59 return "=";
60 case NODE_KIND::NT_DISTINCT_BOOL:
61 return "distinct";
62 case NODE_KIND::NT_DISTINCT_OTHER:
63 return "distinct";
64 // CONSTANT / VARIABLE
65 case NODE_KIND::NT_CONST:
66 return "CONST";
67 case NODE_KIND::NT_VAR:
68 return "VAR";
69 case NODE_KIND::NT_TEMP_VAR:
70 return "TEMP_VAR";
71 // BOOLEAN
72 case NODE_KIND::NT_NOT:
73 return "not";
74 case NODE_KIND::NT_AND:
75 return "and";
76 case NODE_KIND::NT_OR:
77 return "or";
78 case NODE_KIND::NT_IMPLIES:
79 return "=>";
80 case NODE_KIND::NT_XOR:
81 return "xor";
82 // UF
83 case NODE_KIND::NT_UF_APPLY:
84 return "UF_APPLY";
85 case NODE_KIND::NT_DT_FUN_APPLY:
86 return "DT_FUN_APPLY";
87 // ARITHMATIC COMMON OPERATORS
88 case NODE_KIND::NT_ADD:
89 return "+";
90 case NODE_KIND::NT_MUL:
91 return "*";
92 case NODE_KIND::NT_IAND:
93 return "iand";
94 case NODE_KIND::NT_POW2:
95 return "pow2";
96 case NODE_KIND::NT_POW:
97 return "^";
98 case NODE_KIND::NT_SUB:
99 return "-";
100 case NODE_KIND::NT_NEG:
101 return "-";
102 case NODE_KIND::NT_DIV_INT:
103 return "div";
104 case NODE_KIND::NT_DIV_REAL:
105 return "/";
106 case NODE_KIND::NT_MOD:
107 return "mod";
108 case NODE_KIND::NT_ABS:
109 return "abs";
110 case NODE_KIND::NT_SQRT:
111 return "sqrt";
112 case NODE_KIND::NT_SAFESQRT:
113 return "safesqrt";
114 case NODE_KIND::NT_CEIL:
115 return "ceil";
116 case NODE_KIND::NT_FLOOR:
117 return "floor";
118 case NODE_KIND::NT_ROUND:
119 return "round";
120 // TRANSCENDENTAL ARITHMATIC
121 case NODE_KIND::NT_EXP:
122 return "exp";
123 case NODE_KIND::NT_LOG:
124 return "log";
125 case NODE_KIND::NT_LN:
126 return "ln";
127 case NODE_KIND::NT_LG:
128 return "lg";
129 case NODE_KIND::NT_LB:
130 return "lb";
131 case NODE_KIND::NT_SIN:
132 return "sin";
133 case NODE_KIND::NT_COS:
134 return "cos";
135 case NODE_KIND::NT_SEC:
136 return "sec";
137 case NODE_KIND::NT_CSC:
138 return "csc";
139 case NODE_KIND::NT_TAN:
140 return "tan";
141 case NODE_KIND::NT_COT:
142 return "cot";
143 case NODE_KIND::NT_ASIN:
144 return "asin";
145 case NODE_KIND::NT_ACOS:
146 return "acos";
147 case NODE_KIND::NT_ASEC:
148 return "asec";
149 case NODE_KIND::NT_ACSC:
150 return "acsc";
151 case NODE_KIND::NT_ATAN:
152 return "atan";
153 case NODE_KIND::NT_ACOT:
154 return "acot";
155 case NODE_KIND::NT_SINH:
156 return "sinh";
157 case NODE_KIND::NT_COSH:
158 return "cosh";
159 case NODE_KIND::NT_TANH:
160 return "tanh";
161 case NODE_KIND::NT_SECH:
162 return "sech";
163 case NODE_KIND::NT_CSCH:
164 return "csch";
165 case NODE_KIND::NT_COTH:
166 return "coth";
167 case NODE_KIND::NT_ASINH:
168 return "asinh";
169 case NODE_KIND::NT_ACOSH:
170 return "acosh";
171 case NODE_KIND::NT_ATANH:
172 return "atanh";
173 case NODE_KIND::NT_ASECH:
174 return "asech";
175 case NODE_KIND::NT_ACSCH:
176 return "acsch";
177 case NODE_KIND::NT_ACOTH:
178 return "acoth";
179 case NODE_KIND::NT_ATAN2:
180 return "atan2";
181 case NODE_KIND::NT_LE:
182 return "<=";
183 case NODE_KIND::NT_LT:
184 return "<";
185 case NODE_KIND::NT_GE:
186 return ">=";
187 case NODE_KIND::NT_GT:
188 return ">";
189 // ARITHMATIC CONVERSION
190 case NODE_KIND::NT_TO_INT:
191 return "to_int";
192 case NODE_KIND::NT_TO_REAL:
193 return "to_real";
194 // ARITHMATIC PROPERTIES
195 case NODE_KIND::NT_IS_INT:
196 return "is_int";
197 case NODE_KIND::NT_IS_DIVISIBLE:
198 return "is_divisible";
199 case NODE_KIND::NT_IS_PRIME:
200 return "is_prime";
201 case NODE_KIND::NT_IS_EVEN:
202 return "is_even";
203 case NODE_KIND::NT_IS_ODD:
204 return "is_odd";
205 // ARITHMATIC CONSTANTS
206 case NODE_KIND::NT_CONST_PI:
207 return "pi";
208 case NODE_KIND::NT_CONST_E:
209 return "e";
210 case NODE_KIND::NT_INFINITY:
211 return "inf";
212 case NODE_KIND::NT_POS_INFINITY:
213 return "+inf";
214 case NODE_KIND::NT_NEG_INFINITY:
215 return "-inf";
216 case NODE_KIND::NT_NAN:
217 return "NaN";
218 case NODE_KIND::NT_EPSILON:
219 return "epsilon";
220 case NODE_KIND::NT_POS_EPSILON:
221 return "+epsilon";
222 case NODE_KIND::NT_NEG_EPSILON:
223 return "-epsilon";
224 // ARITHMATIC FUNCTIONS
225 // case NODE_KIND::NT_SUM:
226 // return "sum";
227 // case NODE_KIND::NT_PROD:
228 // return "prod";
229 case NODE_KIND::NT_GCD:
230 return "gcd";
231 case NODE_KIND::NT_LCM:
232 return "lcm";
233 case NODE_KIND::NT_FACT:
234 return "factorial";
235 // BITVECTOR COMMON OPERATORS
236 // Bit-wise operations
237 case NODE_KIND::NT_BV_NOT:
238 return "bvnot";
239 case NODE_KIND::NT_BV_AND:
240 return "bvand";
241 case NODE_KIND::NT_BV_OR:
242 return "bvor";
243 case NODE_KIND::NT_BV_XOR:
244 return "bvxor";
245 case NODE_KIND::NT_BV_NAND:
246 return "bvnand";
247 case NODE_KIND::NT_BV_NOR:
248 return "bvnor";
249 case NODE_KIND::NT_BV_XNOR:
250 return "bvxnor";
251 case NODE_KIND::NT_BV_COMP:
252 return "bvcomp";
253 // Arithmetic operations
254 case NODE_KIND::NT_BV_NEG:
255 return "bvneg";
256 case NODE_KIND::NT_BV_ADD:
257 return "bvadd";
258 case NODE_KIND::NT_BV_SUB:
259 return "bvsub";
260 case NODE_KIND::NT_BV_MUL:
261 return "bvmul";
262 case NODE_KIND::NT_BV_UDIV:
263 return "bvudiv";
264 case NODE_KIND::NT_BV_SDIV:
265 return "bvsdiv";
266 case NODE_KIND::NT_BV_UREM:
267 return "bvurem";
268 case NODE_KIND::NT_BV_SREM:
269 return "bvsrem";
270 case NODE_KIND::NT_BV_UMOD:
271 return "bvumod";
272 case NODE_KIND::NT_BV_SMOD:
273 return "bvsmod";
274 // Arithmetic operations with overflow
275 case NODE_KIND::NT_BV_NEGO:
276 return "bvnego";
277 case NODE_KIND::NT_BV_SADDO:
278 return "bvsaddo";
279 case NODE_KIND::NT_BV_UADDO:
280 return "bvuaddo";
281 case NODE_KIND::NT_BV_SMULO:
282 return "bvsmulo";
283 case NODE_KIND::NT_BV_UMULO:
284 return "bvumulo";
285 case NODE_KIND::NT_BV_SDIVO:
286 return "bvsdivo";
287 case NODE_KIND::NT_BV_UDIVO:
288 return "bvudivo";
289 case NODE_KIND::NT_BV_SREMO:
290 return "bvsremo";
291 case NODE_KIND::NT_BV_UREMO:
292 return "bvuremo";
293 case NODE_KIND::NT_BV_SMODO:
294 return "bvsmodo";
295 case NODE_KIND::NT_BV_UMODO:
296 return "bvumodo";
297 // Shift operations
298 case NODE_KIND::NT_BV_SHL:
299 return "bvshl";
300 case NODE_KIND::NT_BV_LSHR:
301 return "bvlshr";
302 case NODE_KIND::NT_BV_ASHR:
303 return "bvashr";
304 // Function
305 case NODE_KIND::NT_BV_CONCAT:
306 return "concat";
307 case NODE_KIND::NT_BV_EXTRACT:
308 return "extract";
309 case NODE_KIND::NT_BV_REPEAT:
310 return "repeat";
311 case NODE_KIND::NT_BV_ZERO_EXT:
312 return "zero_extend";
313 case NODE_KIND::NT_BV_SIGN_EXT:
314 return "sign_extend";
315 case NODE_KIND::NT_BV_ROTATE_LEFT:
316 return "rotate_left";
317 case NODE_KIND::NT_BV_ROTATE_RIGHT:
318 return "rotate_right";
319 // BITVECTOR COMP
320 case NODE_KIND::NT_BV_ULT:
321 return "bvult";
322 case NODE_KIND::NT_BV_ULE:
323 return "bvule";
324 case NODE_KIND::NT_BV_UGT:
325 return "bvugt";
326 case NODE_KIND::NT_BV_UGE:
327 return "bvuge";
328 case NODE_KIND::NT_BV_SLT:
329 return "bvslt";
330 case NODE_KIND::NT_BV_SLE:
331 return "bvsle";
332 case NODE_KIND::NT_BV_SGT:
333 return "bvsgt";
334 case NODE_KIND::NT_BV_SGE:
335 return "bvsge";
336 // BITVECTOR CONVERSION
337 case NODE_KIND::NT_BV_TO_NAT:
338 return "bv2nat";
339 case NODE_KIND::NT_NAT_TO_BV:
340 return "nat2bv";
341 case NODE_KIND::NT_UBV_TO_INT:
342 return "ubv_to_int";
343 case NODE_KIND::NT_SBV_TO_INT:
344 return "sbv_to_int";
345 case NODE_KIND::NT_INT_TO_BV:
346 return "int2bv";
347 case NODE_KIND::NT_BV_TO_INT:
348 return "bv2nat";
349 // FLOATING POINT COMMON OPERATORS
350 case NODE_KIND::NT_FP_ADD:
351 return "fp.add";
352 case NODE_KIND::NT_FP_SUB:
353 return "fp.sub";
354 case NODE_KIND::NT_FP_MUL:
355 return "fp.mul";
356 case NODE_KIND::NT_FP_DIV:
357 return "fp.div";
358 case NODE_KIND::NT_FP_ABS:
359 return "fp.abs";
360 case NODE_KIND::NT_FP_NEG:
361 return "fp.neg";
362 case NODE_KIND::NT_FP_REM:
363 return "fp.rem";
364 case NODE_KIND::NT_FP_FMA:
365 return "fp.fma";
366 case NODE_KIND::NT_FP_SQRT:
367 return "fp.sqrt";
368 case NODE_KIND::NT_FP_ROUND_TO_INTEGRAL:
369 return "fp.roundToIntegral";
370 case NODE_KIND::NT_FP_MIN:
371 return "fp.min";
372 case NODE_KIND::NT_FP_MAX:
373 return "fp.max";
374 // FLOATING POINT COMP
375 case NODE_KIND::NT_FP_LE:
376 return "fp.leq";
377 case NODE_KIND::NT_FP_LT:
378 return "fp.lt";
379 case NODE_KIND::NT_FP_GE:
380 return "fp.geq";
381 case NODE_KIND::NT_FP_GT:
382 return "fp.gt";
383 case NODE_KIND::NT_FP_EQ:
384 return "fp.eq";
385 // FLOATING POINT CONVERSION
386 case NODE_KIND::NT_FP_TO_UBV:
387 return "fp.to_ubv";
388 case NODE_KIND::NT_FP_TO_SBV:
389 return "fp.to_sbv";
390 case NODE_KIND::NT_FP_TO_REAL:
391 return "fp.to_real";
392 case NODE_KIND::NT_FP_TO_FP:
393 return "to_fp";
394 case NODE_KIND::NT_FP_TO_FP_UNSIGNED:
395 return "to_fp_unsigned";
396
397 // FLOATING POINT PROPERTIES
398 case NODE_KIND::NT_FP_IS_NORMAL:
399 return "fp.isNormal";
400 case NODE_KIND::NT_FP_IS_SUBNORMAL:
401 return "fp.isSubnormal";
402 case NODE_KIND::NT_FP_IS_ZERO:
403 return "fp.isZero";
404 case NODE_KIND::NT_FP_IS_INF:
405 return "fp.isInfinite";
406 case NODE_KIND::NT_FP_IS_NAN:
407 return "fp.isNaN";
408 case NODE_KIND::NT_FP_IS_NEG:
409 return "fp.isNegative";
410 case NODE_KIND::NT_FP_IS_POS:
411 return "fp.isPositive";
412 // ARRAY
413 case NODE_KIND::NT_SELECT:
414 return "select";
415 case NODE_KIND::NT_STORE:
416 return "store";
417 // DATATYPES
418 case NODE_KIND::NT_DT_TESTER:
419 return "is";
420 case NODE_KIND::NT_DT_UPDATER:
421 return "update";
422 // TUPLES
423 case NODE_KIND::NT_TUPLE_CONSTRUCTOR:
424 return "tuple";
425 case NODE_KIND::NT_TUPLE_UNIT:
426 return "tuple.unit";
427 case NODE_KIND::NT_TUPLE_SELECT:
428 return "tuple.select";
429 case NODE_KIND::NT_TUPLE_UPDATE:
430 return "tuple.update";
431 case NODE_KIND::NT_TUPLE_PROJECT:
432 return "tuple.project";
433 // STRINGS COMMON OPERATORS
434 case NODE_KIND::NT_STR_LEN:
435 return "str.len";
436 case NODE_KIND::NT_STR_CONCAT:
437 return "str.++";
438 case NODE_KIND::NT_STR_SUBSTR:
439 return "str.substr";
440 case NODE_KIND::NT_STR_PREFIXOF:
441 return "str.prefixof";
442 case NODE_KIND::NT_STR_SUFFIXOF:
443 return "str.suffixof";
444 case NODE_KIND::NT_STR_INDEXOF:
445 return "str.indexof";
446 case NODE_KIND::NT_STR_CHARAT:
447 return "str.at";
448 case NODE_KIND::NT_STR_UPDATE:
449 return "str.update";
450 case NODE_KIND::NT_STR_REPLACE:
451 return "str.replace";
452 case NODE_KIND::NT_STR_REPLACE_ALL:
453 return "str.replace_all";
454 case NODE_KIND::NT_STR_TO_LOWER:
455 return "str.to_lower";
456 case NODE_KIND::NT_STR_TO_UPPER:
457 return "str.to_upper";
458 case NODE_KIND::NT_STR_REV:
459 return "str.rev";
460 case NODE_KIND::NT_STR_SPLIT:
461 return "str.split";
462 case NODE_KIND::NT_STR_SPLIT_AT:
463 return "str.split_at";
464 case NODE_KIND::NT_STR_SPLIT_REST:
465 return "str.split_rest";
466 case NODE_KIND::NT_STR_NUM_SPLITS:
467 return "str.num_splits";
468 case NODE_KIND::NT_STR_SPLIT_AT_RE:
469 return "str.split_at_re";
470 case NODE_KIND::NT_STR_SPLIT_REST_RE:
471 return "str.split_rest_re";
472 case NODE_KIND::NT_STR_NUM_SPLITS_RE:
473 return "str.num_splits_re";
474 // STRINGS COMP
475 case NODE_KIND::NT_STR_LT:
476 return "str.<";
477 case NODE_KIND::NT_STR_LE:
478 return "str.<=";
479 case NODE_KIND::NT_STR_GT:
480 return "str.>";
481 case NODE_KIND::NT_STR_GE:
482 return "str.>=";
483 // STRINGS PROPERTIES
484 case NODE_KIND::NT_STR_IN_REG:
485 return "str.in_re";
486 case NODE_KIND::NT_STR_CONTAINS:
487 return "str.contains";
488 case NODE_KIND::NT_STR_IS_DIGIT:
489 return "str.is_digit";
490 // STRINGS CONVERSION
491 case NODE_KIND::NT_STR_FROM_INT:
492 return "str.from_int";
493 case NODE_KIND::NT_STR_TO_INT:
494 return "str.to_int";
495 case NODE_KIND::NT_STR_TO_REG:
496 return "str.to_re";
497 case NODE_KIND::NT_STR_TO_CODE:
498 return "str.to_code";
499 case NODE_KIND::NT_STR_FROM_CODE:
500 return "str.from_code";
501 case NODE_KIND::NT_REG_NONE:
502 return "re.none";
503 case NODE_KIND::NT_REG_ALL:
504 return "re.all";
505 case NODE_KIND::NT_REG_ALLCHAR:
506 return "re.allchar";
507 case NODE_KIND::NT_REG_CONCAT:
508 return "re.++";
509 case NODE_KIND::NT_REG_UNION:
510 return "re.union";
511 case NODE_KIND::NT_REG_INTER:
512 return "re.inter";
513 case NODE_KIND::NT_REG_DIFF:
514 return "re.diff";
515 case NODE_KIND::NT_REG_STAR:
516 return "re.*";
517 case NODE_KIND::NT_REG_PLUS:
518 return "re.+";
519 case NODE_KIND::NT_REG_OPT:
520 return "re.opt";
521 case NODE_KIND::NT_REG_RANGE:
522 return "re.range";
523 case NODE_KIND::NT_REG_REPEAT:
524 return "re.^";
525 case NODE_KIND::NT_REG_LOOP:
526 return "re.loop";
527 case NODE_KIND::NT_REG_COMPLEMENT:
528 return "re.comp";
529 // STRINGS RE FUNCTIONS
530 case NODE_KIND::NT_STR_REPLACE_REG:
531 return "str.replace_re";
532 case NODE_KIND::NT_STR_REPLACE_REG_ALL:
533 return "str.replace_re_all";
534 case NODE_KIND::NT_STR_INDEXOF_REG:
535 return "str.indexof";
536 // INTERVAL
537 case NODE_KIND::NT_MAX:
538 return "max";
539 case NODE_KIND::NT_MIN:
540 return "min";
541 // LET
542 case NODE_KIND::NT_LET:
543 return "let";
544 case NODE_KIND::NT_LET_CHAIN:
545 return "let_chain";
546 case NODE_KIND::NT_LET_BIND_VAR:
547 return "let_bind_var";
548 case NODE_KIND::NT_LET_BIND_VAR_LIST:
549 return "let_bind_var_list";
550 // ITE
551 case NODE_KIND::NT_ITE:
552 return "ite";
553 // QUANTIFIERS
554 case NODE_KIND::NT_FORALL:
555 return "forall";
556 case NODE_KIND::NT_EXISTS:
557 return "exists";
558 case NODE_KIND::NT_QUANT_VAR:
559 return "quant_var";
560 // FUNC
561 case NODE_KIND::NT_FUNC_DEC:
562 return "func_dec";
563 case NODE_KIND::NT_FUNC_DEF:
564 return "func_def";
565 case NODE_KIND::NT_FUNC_PARAM:
566 return "func_param";
567 case NODE_KIND::NT_FUNC_APPLY:
568 return "func_apply";
569 case NODE_KIND::NT_FUNC_REC:
570 return "func_rec";
571 case NODE_KIND::NT_FUNC_REC_APPLY:
572 return "func_rec_apply";
573 default:
574 return "UNKNOWN_KIND";
575 }
576}
577NODE_KIND getNegatedKind(const NODE_KIND &nk) {
578 switch (nk) {
579 case NODE_KIND::NT_EQ:
580 return NODE_KIND::NT_DISTINCT;
581 case NODE_KIND::NT_DISTINCT:
582 return NODE_KIND::NT_EQ;
583 case NODE_KIND::NT_EQ_BOOL:
584 return NODE_KIND::NT_DISTINCT_BOOL;
585 case NODE_KIND::NT_DISTINCT_BOOL:
586 return NODE_KIND::NT_EQ_BOOL;
587 case NODE_KIND::NT_EQ_OTHER:
588 return NODE_KIND::NT_DISTINCT_OTHER;
589 case NODE_KIND::NT_DISTINCT_OTHER:
590 return NODE_KIND::NT_EQ_OTHER;
591 case NODE_KIND::NT_LE:
592 return NODE_KIND::NT_GT;
593 case NODE_KIND::NT_LT:
594 return NODE_KIND::NT_GE;
595 case NODE_KIND::NT_GE:
596 return NODE_KIND::NT_LT;
597 case NODE_KIND::NT_GT:
598 return NODE_KIND::NT_LE;
599 case NODE_KIND::NT_BV_ULT:
600 return NODE_KIND::NT_BV_UGE;
601 case NODE_KIND::NT_BV_UGT:
602 return NODE_KIND::NT_BV_ULE;
603 case NODE_KIND::NT_BV_ULE:
604 return NODE_KIND::NT_BV_UGT;
605 case NODE_KIND::NT_BV_UGE:
606 return NODE_KIND::NT_BV_ULT;
607 case NODE_KIND::NT_BV_SLT:
608 return NODE_KIND::NT_BV_SGE;
609 case NODE_KIND::NT_BV_SGT:
610 return NODE_KIND::NT_BV_SLE;
611 case NODE_KIND::NT_BV_SLE:
612 return NODE_KIND::NT_BV_SGT;
613 case NODE_KIND::NT_BV_SGE:
614 return NODE_KIND::NT_BV_SLT;
615 case NODE_KIND::NT_FP_LE:
616 return NODE_KIND::NT_FP_GT;
617 case NODE_KIND::NT_FP_LT:
618 return NODE_KIND::NT_FP_GE;
619 case NODE_KIND::NT_FP_GE:
620 return NODE_KIND::NT_FP_LT;
621 case NODE_KIND::NT_FP_GT:
622 return NODE_KIND::NT_FP_LE;
623 case NODE_KIND::NT_STR_LT:
624 return NODE_KIND::NT_STR_GE;
625 case NODE_KIND::NT_STR_GT:
626 return NODE_KIND::NT_STR_LE;
627 case NODE_KIND::NT_STR_LE:
628 return NODE_KIND::NT_STR_GT;
629 case NODE_KIND::NT_STR_GE:
630 return NODE_KIND::NT_STR_LT;
631 default:
632 return NODE_KIND::NT_UNKNOWN;
633 }
634}
635NODE_KIND getFlipKind(const NODE_KIND &nk) {
636 switch (nk) {
637 case NODE_KIND::NT_EQ:
638 return NODE_KIND::NT_EQ;
639 case NODE_KIND::NT_DISTINCT:
640 return NODE_KIND::NT_DISTINCT;
641 case NODE_KIND::NT_EQ_BOOL:
642 return NODE_KIND::NT_EQ_BOOL;
643 case NODE_KIND::NT_DISTINCT_BOOL:
644 return NODE_KIND::NT_DISTINCT_BOOL;
645 case NODE_KIND::NT_EQ_OTHER:
646 return NODE_KIND::NT_EQ_OTHER;
647 case NODE_KIND::NT_DISTINCT_OTHER:
648 return NODE_KIND::NT_DISTINCT_OTHER;
649 case NODE_KIND::NT_LE:
650 return NODE_KIND::NT_GE;
651 case NODE_KIND::NT_LT:
652 return NODE_KIND::NT_GT;
653 case NODE_KIND::NT_GE:
654 return NODE_KIND::NT_LE;
655 case NODE_KIND::NT_GT:
656 return NODE_KIND::NT_LT;
657 case NODE_KIND::NT_ADD:
658 return NODE_KIND::NT_SUB;
659 case NODE_KIND::NT_SUB:
660 return NODE_KIND::NT_ADD;
661 case NODE_KIND::NT_DIV_INT:
662 return NODE_KIND::NT_MUL;
663 case NODE_KIND::NT_DIV_REAL:
664 return NODE_KIND::NT_MUL;
665 case NODE_KIND::NT_BV_SUB:
666 return NODE_KIND::NT_BV_ADD;
667 case NODE_KIND::NT_BV_ADD:
668 return NODE_KIND::NT_BV_SUB;
669 case NODE_KIND::NT_BV_UDIV:
670 return NODE_KIND::NT_BV_MUL;
671 case NODE_KIND::NT_BV_SDIV:
672 return NODE_KIND::NT_BV_MUL;
673 case NODE_KIND::NT_BV_ULT:
674 return NODE_KIND::NT_BV_UGT;
675 case NODE_KIND::NT_BV_UGT:
676 return NODE_KIND::NT_BV_ULT;
677 case NODE_KIND::NT_BV_ULE:
678 return NODE_KIND::NT_BV_UGE;
679 case NODE_KIND::NT_BV_UGE:
680 return NODE_KIND::NT_BV_ULE;
681 case NODE_KIND::NT_BV_SLT:
682 return NODE_KIND::NT_BV_SGE;
683 case NODE_KIND::NT_BV_SGT:
684 return NODE_KIND::NT_BV_SLT;
685 case NODE_KIND::NT_BV_SLE:
686 return NODE_KIND::NT_BV_SGE;
687 case NODE_KIND::NT_BV_SGE:
688 return NODE_KIND::NT_BV_SLE;
689 case NODE_KIND::NT_FP_ADD:
690 return NODE_KIND::NT_FP_SUB;
691 case NODE_KIND::NT_FP_SUB:
692 return NODE_KIND::NT_FP_ADD;
693 case NODE_KIND::NT_FP_MUL:
694 return NODE_KIND::NT_FP_DIV;
695 case NODE_KIND::NT_FP_DIV:
696 return NODE_KIND::NT_FP_MUL;
697 case NODE_KIND::NT_FP_LE:
698 return NODE_KIND::NT_FP_GE;
699 case NODE_KIND::NT_FP_LT:
700 return NODE_KIND::NT_FP_GT;
701 case NODE_KIND::NT_FP_GE:
702 return NODE_KIND::NT_FP_LE;
703 case NODE_KIND::NT_FP_GT:
704 return NODE_KIND::NT_FP_LT;
705 case NODE_KIND::NT_STR_LT:
706 return NODE_KIND::NT_STR_GT;
707 case NODE_KIND::NT_STR_GT:
708 return NODE_KIND::NT_STR_LT;
709 case NODE_KIND::NT_STR_LE:
710 return NODE_KIND::NT_STR_GE;
711 case NODE_KIND::NT_STR_GE:
712 return NODE_KIND::NT_STR_LE;
713 default:
714 return NODE_KIND::NT_UNKNOWN;
715 }
716}
717
718NODE_KIND getOperKind(const std::string &s) {
719 auto it = oper_key_map.find(s);
720 if (it != oper_key_map.end()) {
721 return it->second;
722 }
723 return NODE_KIND::NT_UNKNOWN;
724}
725} // namespace stabilizer::parser
stabilizer::parser::oper_key_map
const std::unordered_map< std::string, NODE_KIND > oper_key_map
Definition kind.h:385
stabilizer::parser::kindToString
std::string kindToString(const NODE_KIND &nk)
Definition kind.cpp:35
stabilizer::parser::getOperKind
NODE_KIND getOperKind(const std::string &s)
Definition kind.cpp:718
stabilizer::parser::getFlipKind
NODE_KIND getFlipKind(const NODE_KIND &nk)
Definition kind.cpp:635
stabilizer::parser::getNegatedKind
NODE_KIND getNegatedKind(const NODE_KIND &nk)
Definition kind.cpp:577