SMTStabilizer API
Public API documentation for SMTStabilizer
Loading...
Searching...
No Matches
rewrite_parser.cpp
Go to the documentation of this file.
1// Copyright (c) 2026 XiangZhang
2//
3// Permission is hereby granted, free of charge, to any person obtaining a copy
4// of this software and associated documentation files (the "Software"), to deal
5// in the Software without restriction, including without limitation the rights
6// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
7// copies of the Software, and to permit persons to whom the Software is
8// furnished to do so, subject to the following conditions:
9//
10// The above copyright notice and this permission notice shall be included in
11// all copies or substantial portions of the Software.
12//
13// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
14// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
15// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
16// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
17// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
18// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
19// SOFTWARE.
20
21#include <algorithm>
22#include <cassert>
23#include <cstddef>
24#include <memory>
25#include <stdexcept>
26#include <string>
27#include <vector>
28
29#include "parser.h"
30#include "parser/dag.h"
31#include "parser/kind.h"
32#include "parser/number.h"
33#include "parser/util.h"
34namespace stabilizer::parser {
35void echo_error(const std::string &msg) {
36 throw std::runtime_error(msg);
37}
38// unary
39std::shared_ptr<DAGNode> Parser::rewrite(NODE_KIND &t, std::shared_ptr<DAGNode> &p) {
40 // return nullptr;
41 switch (t) {
42 case NODE_KIND::NT_CONST_ARRAY:
43 return nullptr;
44 case NODE_KIND::NT_NOT:
45 if (p->isTrue())
46 return mkFalse();
47 else if (p->isFalse())
48 return mkTrue();
49 else if (p->isNot())
50 return p->getChild(0);
51 else
52 return nullptr;
53 case NODE_KIND::NT_NEG:
54 if (p->isCInt())
55 return mkConstInt(-toInt(p));
56 else if (p->isCReal())
57 return mkConstReal(-toReal(p));
58 else if (p->isNeg())
59 return p->getChild(0);
60 else
61 return nullptr;
62 case NODE_KIND::NT_ABS:
63 if (p->isCInt()) {
64 Integer i = toInt(p);
65 if (i < 0)
66 return mkConstInt(-i);
67 else
68 return p;
69 }
70 else if (p->isCReal()) {
71 Real r = toReal(p);
72 if (r < 0)
73 return mkConstReal(-r);
74 else
75 return p;
76 }
77 else if (p->isAbs())
78 return p->getChild(0);
79 else if (p->isNeg())
80 p = p->getChild(0);
81 return nullptr;
82 case NODE_KIND::NT_SQRT:
83 if (p->isCInt() || p->isCReal()) {
84 if (getEvaluateUseFloating())
85 return mkConstReal(toReal(p).sqrt());
86 }
87 else
88 return nullptr;
89
90 case NODE_KIND::NT_SAFESQRT:
91 if (p->isCInt() || p->isCReal()) {
92 if (getEvaluateUseFloating())
93 return mkConstReal(toReal(p).safeSqrt());
94 }
95 else
96 return nullptr;
97 case NODE_KIND::NT_CEIL:
98 if (p->getSort()->isInt() || p->isCInt())
99 return p;
100 else if (p->isCReal())
101 return mkConstReal(toReal(p).ceil());
102 else
103 return nullptr;
104 case NODE_KIND::NT_FLOOR:
105 if (p->getSort()->isInt() || p->isCInt())
106 return p;
107 else if (p->isCReal())
108 return mkConstReal(toReal(p).floor());
109 else
110 return nullptr;
111 case NODE_KIND::NT_ROUND:
112 if (p->getSort()->isInt() || p->isCInt())
113 return p;
114 else if (p->isCReal())
115 return mkConstReal(toReal(p).round());
116 else
117 return nullptr;
118 case NODE_KIND::NT_EXP:
119 if (p->isCInt() || p->isCReal()) {
120 if (getEvaluateUseFloating())
121 return mkConstReal(toReal(p).exp());
122 }
123 else if (p->isLn())
124 return p->getChild(0);
125 else
126 return nullptr;
127 case NODE_KIND::NT_LN:
128 if (p->isCInt() || p->isCReal()) {
129 if (getEvaluateUseFloating())
130 return mkConstReal(toReal(p).ln());
131 }
132 else if (p->isExp())
133 return p->getChild(0);
134 else
135 return nullptr;
136 case NODE_KIND::NT_LG:
137 if (p->isCInt() || p->isCReal()) {
138 if (getEvaluateUseFloating())
139 return mkConstReal(toReal(p).lg());
140 }
141 else
142 return nullptr;
143 case NODE_KIND::NT_LB:
144 if (p->isCInt() || p->isCReal()) {
145 if (getEvaluateUseFloating())
146 return mkConstReal(toReal(p).lb());
147 }
148 else if (p->isPow2())
149 return p->getChild(0);
150 else
151 return nullptr;
152 case NODE_KIND::NT_SIN:
153 if (p->isCInt() || p->isCReal()) {
154 if (getEvaluateUseFloating())
155 return mkConstReal(toReal(p).sin());
156 }
157 else
158 return nullptr;
159 case NODE_KIND::NT_COS:
160 if (p->isCInt() || p->isCReal()) {
161 if (getEvaluateUseFloating())
162 return mkConstReal(toReal(p).cos());
163 }
164 else
165 return nullptr;
166 case NODE_KIND::NT_SEC:
167 if (p->isCInt() || p->isCReal()) {
168 if (getEvaluateUseFloating())
169 return mkConstReal(toReal(p).sec());
170 }
171 else
172 return nullptr;
173 case NODE_KIND::NT_CSC:
174 if (p->isCInt() || p->isCReal()) {
175 if (getEvaluateUseFloating())
176 return mkConstReal(toReal(p).csc());
177 }
178 else
179 return nullptr;
180 case NODE_KIND::NT_TAN:
181 if (p->isCInt() || p->isCReal()) {
182 if (getEvaluateUseFloating())
183 return mkConstReal(toReal(p).tan());
184 }
185 else
186 return nullptr;
187 case NODE_KIND::NT_COT:
188 if (p->isCInt() || p->isCReal()) {
189 if (getEvaluateUseFloating())
190 return mkConstReal(toReal(p).cot());
191 }
192 else
193 return nullptr;
194 case NODE_KIND::NT_ASIN:
195 if (p->isCInt() || p->isCReal()) {
196 if (getEvaluateUseFloating())
197 return mkConstReal(toReal(p).asin());
198 }
199 else
200 return nullptr;
201 case NODE_KIND::NT_ACOS:
202 if (p->isCInt() || p->isCReal()) {
203 if (getEvaluateUseFloating())
204 return mkConstReal(toReal(p).acos());
205 }
206 else
207 return nullptr;
208 case NODE_KIND::NT_ASEC:
209 if (p->isCInt() || p->isCReal()) {
210 if (getEvaluateUseFloating())
211 return mkConstReal(toReal(p).asec());
212 }
213 else
214 return nullptr;
215 case NODE_KIND::NT_ACSC:
216 if (p->isCInt() || p->isCReal()) {
217 if (getEvaluateUseFloating())
218 return mkConstReal(toReal(p).acsc());
219 }
220 else
221 return nullptr;
222 case NODE_KIND::NT_ATAN:
223 if (p->isCInt() || p->isCReal()) {
224 if (getEvaluateUseFloating())
225 return mkConstReal(toReal(p).atan());
226 }
227 else
228 return nullptr;
229 case NODE_KIND::NT_ACOT:
230 if (p->isCInt() || p->isCReal()) {
231 if (getEvaluateUseFloating())
232 return mkConstReal(toReal(p).acot());
233 }
234 else
235 return nullptr;
236 case NODE_KIND::NT_SINH:
237 if (p->isCInt() || p->isCReal()) {
238 if (getEvaluateUseFloating())
239 return mkConstReal(toReal(p).sinh());
240 }
241 else
242 return nullptr;
243 case NODE_KIND::NT_COSH:
244 if (p->isCInt() || p->isCReal()) {
245 if (getEvaluateUseFloating())
246 return mkConstReal(toReal(p).cosh());
247 }
248 else
249 return nullptr;
250 case NODE_KIND::NT_TANH:
251 if (p->isCInt() || p->isCReal()) {
252 if (getEvaluateUseFloating())
253 return mkConstReal(toReal(p).tanh());
254 }
255 else
256 return nullptr;
257 case NODE_KIND::NT_SECH:
258 if (p->isCInt() || p->isCReal()) {
259 if (getEvaluateUseFloating())
260 return mkConstReal(toReal(p).sech());
261 }
262 else
263 return nullptr;
264 case NODE_KIND::NT_CSCH:
265 if (p->isCInt() || p->isCReal()) {
266 if (getEvaluateUseFloating())
267 return mkConstReal(toReal(p).csch());
268 }
269 else
270 return nullptr;
271 case NODE_KIND::NT_COTH:
272 if (p->isCInt() || p->isCReal()) {
273 if (getEvaluateUseFloating())
274 return mkConstReal(toReal(p).coth());
275 }
276 else
277 return nullptr;
278 case NODE_KIND::NT_ASINH:
279 if (p->isCInt() || p->isCReal()) {
280 if (getEvaluateUseFloating())
281 return mkConstReal(toReal(p).asinh());
282 }
283 else
284 return nullptr;
285 case NODE_KIND::NT_ACOSH:
286 if (p->isCInt() || p->isCReal()) {
287 if (getEvaluateUseFloating())
288 return mkConstReal(toReal(p).acosh());
289 }
290 else
291 return nullptr;
292 case NODE_KIND::NT_ATANH:
293 if (p->isCInt() || p->isCReal()) {
294 if (getEvaluateUseFloating())
295 return mkConstReal(toReal(p).atanh());
296 }
297 else
298 return nullptr;
299 case NODE_KIND::NT_ASECH:
300 if (p->isCInt() || p->isCReal()) {
301 if (getEvaluateUseFloating())
302 return mkConstReal(toReal(p).asech());
303 }
304 else
305 return nullptr;
306 case NODE_KIND::NT_ACSCH:
307 if (p->isCInt() || p->isCReal()) {
308 if (getEvaluateUseFloating())
309 return mkConstReal(toReal(p).acsch());
310 }
311 else
312 return nullptr;
313 case NODE_KIND::NT_ACOTH:
314 if (p->isCInt() || p->isCReal()) {
315 if (getEvaluateUseFloating())
316 return mkConstReal(toReal(p).acoth());
317 }
318 else
319 return nullptr;
320 case NODE_KIND::NT_TO_INT:
321 if (p->isCInt())
322 return p;
323 else if (p->isCReal())
324 return mkConstInt(toReal(p).toInteger());
325 else
326 return nullptr;
327 case NODE_KIND::NT_TO_REAL:
328 if (p->isCInt())
329 return mkConstReal(toReal(p));
330 else if (p->getSort()->isReal() || p->isCReal())
331 return p;
332 else
333 return nullptr;
334 case NODE_KIND::NT_IS_INT:
335 if (p->isCInt())
336 return mkTrue();
337 else if (p->isCReal())
338 return mkFalse();
339 else
340 return nullptr;
341 case NODE_KIND::NT_IS_PRIME:
342 if (p->isCInt()) {
343 Integer i = toInt(p);
344 if (MathUtils::isPrime(i))
345 return mkTrue();
346 else
347 return mkFalse();
348 }
349 else {
350 err_all(p, "Prime check on non-integer", line_number);
351 return nullptr;
352 }
353 case NODE_KIND::NT_IS_EVEN:
354 if (p->isCInt()) {
355 Integer i = toInt(p);
356 if (MathUtils::isEven(i))
357 return mkTrue();
358 else
359 return mkFalse();
360 }
361 else {
362 err_all(p, "Even check on non-integer", line_number);
363 return nullptr;
364 }
365 case NODE_KIND::NT_IS_ODD:
366 if (p->isCInt()) {
367 Integer i = toInt(p);
368 if (MathUtils::isOdd(i))
369 return mkTrue();
370 else
371 return mkFalse();
372 }
373 else {
374 err_all(p, "Odd check on non-integer", line_number);
375 return nullptr;
376 }
377 case NODE_KIND::NT_FACT:
378 if (p->isCInt()) {
379 Integer i = toInt(p);
380 if (i < 0) {
381 err_all(p, "Factorial of negative integer", line_number);
382 return nullptr;
383 }
384 else if (i == 0)
385 return mkConstInt(1);
386 else
387 return mkConstInt(MathUtils::factorial(i));
388 }
389 else {
390 err_all(p, "Factorial on non-integer", line_number);
391 return nullptr;
392 }
393 case NODE_KIND::NT_BV_NOT:
394 if (p->isCBV())
395 return mkConstBv(BitVectorUtils::bvNot(p->toString()), p->getSort()->getBitWidth());
396 else if (p->isBVNot())
397 return p->getChild(0);
398 else
399 return nullptr;
400 case NODE_KIND::NT_BV_NEG:
401 if (p->isCBV())
402 return mkConstBv(BitVectorUtils::bvNeg(p->toString()), p->getSort()->getBitWidth());
403 else if (p->isBVNeg())
404 return p->getChild(0);
405 else
406 return nullptr;
407 case NODE_KIND::NT_BV_NEGO:
408 return nullptr;
409 case NODE_KIND::NT_FP_ABS:
410 case NODE_KIND::NT_FP_NEG:
411 case NODE_KIND::NT_FP_IS_NORMAL:
412 case NODE_KIND::NT_FP_IS_SUBNORMAL:
413 case NODE_KIND::NT_FP_IS_ZERO:
414 case NODE_KIND::NT_FP_IS_INF:
415 case NODE_KIND::NT_FP_IS_NAN:
416 case NODE_KIND::NT_FP_IS_NEG:
417 case NODE_KIND::NT_FP_IS_POS:
418 case NODE_KIND::NT_FP_TO_REAL:
419 return nullptr;
420 case NODE_KIND::NT_STR_LEN:
421 if (p->isCStr())
422 return mkConstInt(StringUtils::strUnquate(p->toString()).size());
423 else
424 return nullptr;
425 case NODE_KIND::NT_STR_TO_LOWER:
426 if (p->isCStr())
427 return mkConstStr(StringUtils::strToLower(p->toString()));
428 else if (p->isStrToLower() || p->isStrToUpper())
429 p = p->getChild(0);
430 return nullptr;
431 case NODE_KIND::NT_STR_TO_UPPER:
432 if (p->isCStr())
433 return mkConstStr(StringUtils::strToUpper(p->toString()));
434 else if (p->isStrToUpper() || p->isStrToLower())
435 p = p->getChild(0);
436 return nullptr;
437 case NODE_KIND::NT_STR_REV:
438 if (p->isCStr())
439 return mkConstStr(StringUtils::strRev(p->toString()));
440 else if (p->isStrRev())
441 return p->getChild(0);
442 else
443 return nullptr;
444 case NODE_KIND::NT_STR_IS_DIGIT:
445 if (p->isCStr())
446 return TypeChecker::isInt(StringUtils::strUnquate(p->toString())) ? mkTrue() : mkFalse();
447 else
448 return nullptr;
449 case NODE_KIND::NT_STR_FROM_INT:
450 if (p->isCInt())
451 return mkConstStr(p->toString());
452 else
453 return nullptr;
454 case NODE_KIND::NT_STR_TO_INT:
455 // return nullptr;
456 // std::cout << p->getPureName() << std::endl;
457 if (p->isCStr()) {
458 std::string str = StringUtils::strUnquate(p->toString());
459 if (TypeChecker::isInt(str)) {
460 return mkConstInt(Integer(str));
461 }
462 else {
463 return NodeManager::NAN_NODE;
464 }
465 // else {
466 // // std::cout << p->toString() << std::endl;
467 // err_all(p, "String to int on non-integer", line_number);
468 // }
469 }
470 return nullptr;
471 case NODE_KIND::NT_STR_TO_REG:
472 return nullptr;
473 case NODE_KIND::NT_STR_TO_CODE:
474 if (p->isCStr()) {
475 std::string str = StringUtils::strUnquate(p->toString());
476 if (str.size() == 1) {
477 return mkConstInt(static_cast<int>(str[0]));
478 }
479 else
480 err_all(p, "String to code on non-single character string", line_number);
481 }
482 return nullptr;
483 case NODE_KIND::NT_STR_FROM_CODE:
484 if (p->isCInt()) {
485 if (toInt(p) >= 0 && toInt(p) <= 127) {
486 return mkConstStr(std::string(1, static_cast<char>(toInt(p).toULong())));
487 }
488 else
489 err_all(p, "String from code on non-ASCII character", line_number);
490 }
491 return nullptr;
492 case NODE_KIND::NT_REG_STAR:
493 case NODE_KIND::NT_REG_PLUS:
494 case NODE_KIND::NT_REG_OPT:
495 case NODE_KIND::NT_REG_COMPLEMENT:
496 return nullptr;
497 case NODE_KIND::NT_BV_TO_NAT:
498 if (p->isCBV())
499 return mkConstInt(BitVectorUtils::bvToNat(p->toString()));
500 else
501 return nullptr;
502 case NODE_KIND::NT_BV_TO_INT:
503 if (p->isCBV())
504 return mkConstInt(BitVectorUtils::bvToInt(p->toString()));
505 else
506 return nullptr;
507 case NODE_KIND::NT_UBV_TO_INT:
508 if (p->isCBV())
509 return mkConstInt(BitVectorUtils::bvToNat(p->toString()));
510 else
511 return nullptr;
512 case NODE_KIND::NT_SBV_TO_INT:
513 if (p->isCBV())
514 return mkConstInt(BitVectorUtils::bvToInt(p->toString()));
515 else
516 return nullptr;
517 case NODE_KIND::NT_POW2:
518 if (p->isCInt())
519 return mkConstInt(MathUtils::pow(2, toInt(p)));
520 else if (p->isLb())
521 return p->getChild(0);
522 else
523 return nullptr;
524 default:
525 echo_error("unexpect NODE_KIND in rewrite unary !!!");
526 return nullptr;
527 }
528}
529
530// binary
531std::shared_ptr<DAGNode> Parser::rewrite(NODE_KIND &t, std::shared_ptr<DAGNode> &l, std::shared_ptr<DAGNode> &r) {
532 switch (t) {
533 case NODE_KIND::NT_POW:
534 if ((l->isCReal() || l->isCInt()) && (r->isCReal() || r->isCInt())) {
535 if (getEvaluateUseFloating())
536 return mkConstReal(toReal(l).pow(toReal(r)));
537 }
538 else if (isZero(r) || isOne(l))
539 return mkConstReal(1);
540 else if (isOne(r))
541 return l;
542 else
543 return nullptr;
544 case NODE_KIND::NT_MOD:
545 if (l->isCInt() && r->isCInt())
546 return mkConstInt(toInt(l) % toInt(r));
547 else if (isOne(r) || isZero(l) || l == r)
548 return mkConstInt(0);
549 else
550 return nullptr;
551 case NODE_KIND::NT_LOG:
552 if ((l->isCInt() || l->isCReal()) && (r->isCInt() || r->isCReal())) {
553 if (getEvaluateUseFloating())
554 return mkConstReal(toReal(l).log(toReal(r)));
555 }
556 else if (isOne(l))
557 return mkConstReal(0);
558 else if (l == r)
559 return mkConstReal(1);
560 else
561 return nullptr;
562
563 case NODE_KIND::NT_ATAN2:
564 if ((l->isCInt() || l->isCReal()) && r->isCReal()) {
565 if (getEvaluateUseFloating())
566 return mkConstReal(Real::atan2(toReal(l), toReal(r)));
567 }
568 else
569 return nullptr;
570 case NODE_KIND::NT_IS_DIVISIBLE:
571 if (l->isCInt() && r->isCInt())
572 return toInt(l) % toInt(r) == 0 ? mkTrue() : mkFalse();
573 else {
574 err_all(l, "Is divisible on non-integer", line_number);
575 err_all(r, "Is divisible on non-integer", line_number);
576 return nullptr;
577 }
578 case NODE_KIND::NT_GCD:
579 if (l->isCInt() && r->isCInt())
580 return mkConstInt(MathUtils::gcd(toInt(l), toInt(r)));
581 else {
582 err_all(l, "GCD on non-integer", line_number);
583 err_all(r, "GCD on non-integer", line_number);
584 return nullptr;
585 }
586 case NODE_KIND::NT_LCM:
587 if (l->isCInt() && r->isCInt())
588 return mkConstInt(MathUtils::lcm(toInt(l), toInt(r)));
589 else {
590 err_all(l, "LCM on non-integer", line_number);
591 err_all(r, "LCM on non-integer", line_number);
592 return nullptr;
593 }
594 case NODE_KIND::NT_BV_UDIV:
595 if (l->isCBV() && r->isCBV())
596 return mkConstBv(BitVectorUtils::bvUdiv(l->toString(), r->toString()), l->getSort()->getBitWidth());
597 else if (isZero(r))
598 return mkConstBv("#b" + std::string(l->getSort()->getBitWidth(), '1'), l->getSort()->getBitWidth());
599 else if (isOne(r))
600 return l;
601 else
602 return nullptr;
603 case NODE_KIND::NT_BV_SDIV:
604 if (l->isCBV() && r->isCBV())
605 return mkConstBv(BitVectorUtils::bvSdiv(l->toString(), r->toString()), l->getSort()->getBitWidth());
606 else if (isOne(r))
607 return l;
608 else if (r->isCBV() && BitVectorUtils::bvIsNegOne(r->toString())) {
609 return mkBvNeg(l);
610 }
611 else
612 return nullptr;
613 case NODE_KIND::NT_BV_UREM:
614 if (l->isCBV() && r->isCBV())
615 return mkConstBv(BitVectorUtils::bvUrem(l->toString(), r->toString()), l->getSort()->getBitWidth());
616 else if (isZero(r))
617 return l;
618 else if (isOne(r) || l == r)
619 return mkConstBv(BitVectorUtils::intToBv(0, l->getSort()->getBitWidth()), l->getSort()->getBitWidth());
620 else
621 return nullptr;
622 case NODE_KIND::NT_BV_SREM:
623 if (l->isCBV() && r->isCBV())
624 return mkConstBv(BitVectorUtils::bvSrem(l->toString(), r->toString()), l->getSort()->getBitWidth());
625 else if (isOne(r) || l == r)
626 return mkConstBv(BitVectorUtils::intToBv(0, l->getSort()->getBitWidth()), l->getSort()->getBitWidth());
627 else
628 return nullptr;
629 case NODE_KIND::NT_BV_UMOD:
630 t = NODE_KIND::NT_BV_UREM;
631 return rewrite(t, l, r);
632 case NODE_KIND::NT_BV_SMOD:
633 if (l->isCBV() && r->isCBV())
634 return mkConstBv(BitVectorUtils::bvSmod(l->toString(), r->toString()), l->getSort()->getBitWidth());
635 else if (isZero(r))
636 return l;
637 else if (isOne(r) || l == r)
638 return mkConstBv(BitVectorUtils::intToBv(0, l->getSort()->getBitWidth()), l->getSort()->getBitWidth());
639 else
640 return nullptr;
641 case NODE_KIND::NT_BV_SDIVO:
642 case NODE_KIND::NT_BV_UDIVO:
643 case NODE_KIND::NT_BV_SREMO:
644 case NODE_KIND::NT_BV_UREMO:
645 case NODE_KIND::NT_BV_SMODO:
646 case NODE_KIND::NT_BV_UMODO:
647 return nullptr;
648 case NODE_KIND::NT_BV_SHL:
649 if (l->isCBV() && r->isCBV())
650 return mkConstBv(BitVectorUtils::bvShl(l->toString(), r->toString()), l->getSort()->getBitWidth());
651 else if (isZero(r))
652 return l;
653 else if (r->isCBV() && BitVectorUtils::bvCompareToUint(r->toString(), l->getSort()->getBitWidth()) >= 0)
654 return mkConstBv(BitVectorUtils::intToBv(0, l->getSort()->getBitWidth()), l->getSort()->getBitWidth());
655 else
656 return nullptr;
657 case NODE_KIND::NT_BV_LSHR:
658 if (l->isCBV() && r->isCBV())
659 return mkConstBv(BitVectorUtils::bvLshr(l->toString(), r->toString()), l->getSort()->getBitWidth());
660 else if (isZero(r))
661 return l;
662 else if (r->isCBV() && BitVectorUtils::bvCompareToUint(r->toString(), l->getSort()->getBitWidth()) >= 0)
663 return mkConstBv(BitVectorUtils::intToBv(0, l->getSort()->getBitWidth()), l->getSort()->getBitWidth());
664 else
665 return nullptr;
666 case NODE_KIND::NT_BV_ASHR:
667 if (l->isCBV() && r->isCBV())
668 return mkConstBv(BitVectorUtils::bvAshr(l->toString(), r->toString()), l->getSort()->getBitWidth());
669 else if (isZero(r))
670 return l;
671 else
672 return nullptr;
673 case NODE_KIND::NT_BV_ULT:
674 if (l->isCBV() && r->isCBV())
675 return BitVectorUtils::bvComp(l->toString(), r->toString(), t) ? mkTrue() : mkFalse();
676 else if (isZero(r))
677 return mkFalse();
678 else if (l->isCBV() && BitVectorUtils::bvIsMaxUnsigned(l->toString()))
679 return mkFalse();
680 else if (l == r)
681 return mkFalse();
682 else
683 return nullptr;
684 case NODE_KIND::NT_BV_ULE:
685 if (l->isCBV() && r->isCBV())
686 return BitVectorUtils::bvComp(l->toString(), r->toString(), t) ? mkTrue() : mkFalse();
687 else if (l == r)
688 return mkTrue();
689 else
690 return nullptr;
691 case NODE_KIND::NT_BV_SLT:
692 if (l->isCBV() && r->isCBV())
693 return BitVectorUtils::bvComp(l->toString(), r->toString(), t) ? mkTrue() : mkFalse();
694 else if (l->isCBV() && BitVectorUtils::bvIsMaxSigned(l->toString()))
695 return mkFalse();
696 else if (r->isCBV() && BitVectorUtils::bvIsMinSigned(r->toString()))
697 return mkFalse();
698 else if (l == r)
699 return mkFalse();
700 else
701 return nullptr;
702 case NODE_KIND::NT_BV_SLE:
703 if (l->isCBV() && r->isCBV())
704 return BitVectorUtils::bvComp(l->toString(), r->toString(), t) ? mkTrue() : mkFalse();
705 else if (l == r)
706 return mkTrue();
707 else if (l->isCBV() && BitVectorUtils::bvIsMaxSigned(l->toString()))
708 return mkEq({l, r});
709 else if (r->isCBV() && BitVectorUtils::bvIsMinSigned(r->toString()))
710 return mkEq({l, r});
711 else
712 return nullptr;
713 case NODE_KIND::NT_BV_UGT:
714 t = NODE_KIND::NT_BV_ULT;
715 std::swap(l, r);
716 return rewrite(t, l, r);
717 case NODE_KIND::NT_BV_UGE:
718 t = NODE_KIND::NT_BV_ULE;
719 std::swap(l, r);
720 return rewrite(t, l, r);
721 case NODE_KIND::NT_BV_SGT:
722 t = NODE_KIND::NT_BV_SLT;
723 std::swap(l, r);
724 return rewrite(t, l, r);
725 case NODE_KIND::NT_BV_SGE:
726 t = NODE_KIND::NT_BV_SLE;
727 std::swap(l, r);
728 return rewrite(t, l, r);
729 case NODE_KIND::NT_NAT_TO_BV:
730 if (l->isCInt() && r->isCInt())
731 return mkConstBv(BitVectorUtils::natToBv(toInt(l), toInt(r)), toInt(r).toULong());
732 else
733 return nullptr;
734 case NODE_KIND::NT_INT_TO_BV:
735 if (l->isCInt() && r->isCInt())
736 return mkConstBv(BitVectorUtils::intToBv(toInt(l), toInt(r)), toInt(r).toULong());
737 else
738 return nullptr;
739 case NODE_KIND::NT_FP_REM:
740 case NODE_KIND::NT_FP_SQRT:
741 case NODE_KIND::NT_FP_ROUND_TO_INTEGRAL:
742 return nullptr;
743 case NODE_KIND::NT_SELECT:
744 return nullptr;
745 case NODE_KIND::NT_STR_PREFIXOF:
746 if (l->isCStr() && r->isCStr())
747 return StringUtils::strPrefixof(l->toString(), r->toString()) ? mkTrue() : mkFalse();
748 else
749 return nullptr;
750 case NODE_KIND::NT_STR_SUFFIXOF:
751 if (l->isCStr() && r->isCStr())
752 return StringUtils::strSuffixof(l->toString(), r->toString()) ? mkTrue() : mkFalse();
753 else
754 return nullptr;
755 case NODE_KIND::NT_STR_CHARAT:
756 if (l->isCStr() && r->isCInt())
757 return mkConstStr(StringUtils::strCharAt(l->toString(), toInt(r)));
758 else
759 return nullptr;
760 case NODE_KIND::NT_STR_SPLIT:
761 return nullptr;
762 case NODE_KIND::NT_STR_IN_REG:
763 case NODE_KIND::NT_REG_RANGE:
764 case NODE_KIND::NT_REG_REPEAT:
765 return nullptr;
766 case NODE_KIND::NT_STR_CONTAINS:
767 if (l->isCStr() && r->isCStr())
768 return StringUtils::strContains(l->toString(), r->toString()) ? mkTrue() : mkFalse();
769 else
770 return nullptr;
771 case NODE_KIND::NT_STR_NUM_SPLITS_RE:
772 return nullptr;
773 case NODE_KIND::NT_BV_REPEAT:
774 if (l->isCBV() && r->isCInt())
775 return mkConstBv(BitVectorUtils::bvRepeat(l->toString(), toInt(r)), l->getSort()->getBitWidth() * toInt(r).toULong());
776 else if (isOne(r))
777 return l;
778 else
779 return nullptr;
780 case NODE_KIND::NT_BV_ZERO_EXT:
781 if (l->isCBV() && r->isCInt())
782 return mkConstBv(BitVectorUtils::bvZeroExtend(l->toString(), toInt(r)), l->getSort()->getBitWidth() + toInt(r).toULong());
783 else if (isZero(r))
784 return l;
785 else if (l->isBVZeroExt() && l->getChild(1)->isCInt()) {
786 r = mkConstInt(toInt(l->getChild(1)) + toInt(r));
787 l = l->getChild(0);
788 return rewrite(t, l, r);
789 }
790 else
791 return nullptr;
792 case NODE_KIND::NT_BV_SIGN_EXT:
793 if (l->isCBV() && r->isCInt())
794 return mkConstBv(BitVectorUtils::bvSignExtend(l->toString(), toInt(r)), l->getSort()->getBitWidth() + toInt(r).toULong());
795 else if (isZero(r))
796 return l;
797 else if (l->isBVSignExt() && l->getChild(1)->isCInt()) {
798 r = mkConstInt(toInt(l->getChild(1)) + toInt(r));
799 l = l->getChild(0);
800 return rewrite(t, l, r);
801 }
802 else
803 return nullptr;
804 case NODE_KIND::NT_BV_ROTATE_LEFT:
805 if (l->isCBV() && r->isCInt())
806 return mkConstBv(BitVectorUtils::bvRotateLeft(l->toString(), toInt(r)), l->getSort()->getBitWidth());
807 else if (r->isCInt() && toInt(r).toULong() % l->getSort()->getBitWidth() == 0)
808 return l;
809 else if (l->isBVRotLeft() && r->isCInt()) {
810 Integer total_rotate = toInt(r) + toInt(l->getChild(1));
811 Integer bitwidth = Integer(l->getSort()->getBitWidth());
812 total_rotate = total_rotate % bitwidth;
813 r = mkConstInt(total_rotate);
814 l = l->getChild(0);
815 return rewrite(t, l, r);
816 }
817 else if (l->isBVRotRight() && r->isCInt()) {
818 if (toInt(r) == toInt(l->getChild(1))) {
819 return l->getChild(0);
820 }
821 else if (toInt(r) > toInt(l->getChild(1))) {
822 Integer total_rotate = toInt(r) - toInt(l->getChild(1));
823 Integer bitwidth = Integer(l->getSort()->getBitWidth());
824 total_rotate = total_rotate % bitwidth;
825 r = mkConstInt(total_rotate);
826 l = l->getChild(0);
827 return rewrite(t, l, r);
828 }
829 else {
830 Integer total_rotate = toInt(l->getChild(1)) - toInt(r);
831 Integer bitwidth = Integer(l->getSort()->getBitWidth());
832 total_rotate = total_rotate % bitwidth;
833 t = NODE_KIND::NT_BV_ROTATE_RIGHT;
834 r = mkConstInt(total_rotate);
835 l = l->getChild(0);
836 return rewrite(t, l, r);
837 }
838 }
839 else
840 return nullptr;
841 case NODE_KIND::NT_BV_ROTATE_RIGHT:
842 if (l->isCBV() && r->isCInt())
843 return mkConstBv(BitVectorUtils::bvRotateRight(l->toString(), toInt(r)), l->getSort()->getBitWidth());
844 else if (r->isCInt() && toInt(r).toULong() % l->getSort()->getBitWidth() == 0)
845 return l;
846 else if (l->isBVRotRight() && r->isCInt()) {
847 Integer total_rotate = toInt(r) + toInt(l->getChild(1));
848 Integer bitwidth = Integer(l->getSort()->getBitWidth());
849 total_rotate = total_rotate % bitwidth;
850 r = mkConstInt(total_rotate);
851 l = l->getChild(0);
852 return rewrite(t, l, r);
853 }
854 else if (l->isBVRotLeft() && r->isCInt()) {
855 if (toInt(r) == toInt(l->getChild(1))) {
856 return l->getChild(0);
857 }
858 else if (toInt(r) > toInt(l->getChild(1))) {
859 Integer total_rotate = toInt(r) - toInt(l->getChild(1));
860 Integer bitwidth = Integer(l->getSort()->getBitWidth());
861 total_rotate = total_rotate % bitwidth;
862 r = mkConstInt(total_rotate);
863 l = l->getChild(0);
864 return rewrite(t, l, r);
865 }
866 else {
867 Integer total_rotate = toInt(l->getChild(1)) - toInt(r);
868 Integer bitwidth = Integer(l->getSort()->getBitWidth());
869 total_rotate = total_rotate % bitwidth;
870 t = NODE_KIND::NT_BV_ROTATE_LEFT;
871 r = mkConstInt(total_rotate);
872 l = l->getChild(0);
873 return rewrite(t, l, r);
874 }
875 }
876 else
877 return nullptr;
878 case NODE_KIND::NT_FP_MIN:
879 case NODE_KIND::NT_FP_MAX:
880 return nullptr;
881 case NODE_KIND::NT_BV_XNOR:
882 if (l->isCBV() && r->isCBV())
883 return mkConstBv(BitVectorUtils::bvXnor(l->toString(), r->toString()), l->getSort()->getBitWidth());
884 else if (l == r)
885 return mkConstBv(BitVectorUtils::mkOnes(l->getSort()->getBitWidth()), l->getSort()->getBitWidth());
886 else
887 return nullptr;
888 case NODE_KIND::NT_BV_NAND:
889 if (l->isCBV() && r->isCBV())
890 return mkConstBv(BitVectorUtils::bvNand(l->toString(), r->toString()), l->getSort()->getBitWidth());
891 else if (l == r)
892 return mkBvNot(l);
893 else if (isZero(l) || isZero(r))
894 return mkConstBv(BitVectorUtils::mkOnes(l->getSort()->getBitWidth()), l->getSort()->getBitWidth());
895 else if (isOnes(l))
896 return mkBvNot(r);
897 else if (isOnes(r))
898 return mkBvNot(l);
899 else
900 return nullptr;
901 case NODE_KIND::NT_BV_NOR:
902 if (l->isCBV() && r->isCBV())
903 return mkConstBv(BitVectorUtils::bvNor(l->toString(), r->toString()), l->getSort()->getBitWidth());
904 else if (l == r)
905 return mkBvNot(l);
906 else if (isOnes(l) || isOnes(r))
907 return mkConstBv(BitVectorUtils::intToBv(0, l->getSort()->getBitWidth()), l->getSort()->getBitWidth());
908 else if (isZero(l))
909 return mkBvNot(r);
910 else if (isZero(r))
911 return mkBvNot(l);
912 else
913 return nullptr;
914 case NODE_KIND::NT_BV_SUB:
915 if (l->isCBV() && r->isCBV())
916 return mkConstBv(BitVectorUtils::bvSub(l->toString(), r->toString()), l->getSort()->getBitWidth());
917 else if (isZero(r))
918 return l;
919 else if (isZero(l))
920 return mkBvNeg(r);
921 else if (l == r)
922 return mkConstBv(BitVectorUtils::intToBv(0, l->getSort()->getBitWidth()), l->getSort()->getBitWidth());
923 else
924 return nullptr;
925 default:
926 // echo_error("unexpect NODE_KIND in rewrite binary !!!");
927 return nullptr;
928 }
929}
930
931// ternary
932std::shared_ptr<DAGNode> Parser::rewrite(NODE_KIND &t, std::shared_ptr<DAGNode> &l, std::shared_ptr<DAGNode> &m, std::shared_ptr<DAGNode> &r) {
933 switch (t) {
934 case NODE_KIND::NT_ITE:
935 if (l->isTrue())
936 return m;
937 else if (l->isFalse())
938 return r;
939 else if (m == r)
940 return m;
941 else
942 return nullptr;
943 case NODE_KIND::NT_FP_ADD:
944 case NODE_KIND::NT_FP_SUB:
945 case NODE_KIND::NT_FP_MUL:
946 case NODE_KIND::NT_FP_DIV:
947 case NODE_KIND::NT_FP_TO_UBV:
948 case NODE_KIND::NT_FP_TO_SBV:
949 return nullptr;
950 case NODE_KIND::NT_STORE:
951 return nullptr;
952 case NODE_KIND::NT_STR_SUBSTR:
953 if (l->isCStr() && m->isCInt() && r->isCInt())
954 return mkConstStr(StringUtils::strSubstr(l->toString(), toInt(m), toInt(r)));
955 else
956 return nullptr;
957 case NODE_KIND::NT_STR_INDEXOF:
958 if (l->isCStr() && m->isCStr() && r->isCInt())
959 return mkConstInt(StringUtils::strIndexof(l->toString(), m->toString(), toInt(r)));
960 else
961 return nullptr;
962 case NODE_KIND::NT_STR_UPDATE:
963 if (l->isCStr() && m->isCInt() && r->isCStr())
964 return mkConstStr(StringUtils::strUpdate(l->toString(), toInt(m), r->toString()));
965 else
966 return nullptr;
967 case NODE_KIND::NT_STR_REPLACE:
968 if (l->isCStr() && m->isCStr() && r->isCStr())
969 return mkConstStr(StringUtils::strReplace(l->toString(), m->toString(), r->toString()));
970 else
971 return nullptr;
972 case NODE_KIND::NT_STR_REPLACE_ALL:
973 if (l->isCStr() && m->isCStr() && r->isCStr())
974 return mkConstStr(StringUtils::strReplaceAll(l->toString(), m->toString(), r->toString()));
975 else
976 return nullptr;
977 case NODE_KIND::NT_STR_SPLIT_AT:
978 case NODE_KIND::NT_STR_SPLIT_REST:
979 case NODE_KIND::NT_STR_SPLIT_AT_RE:
980 case NODE_KIND::NT_STR_SPLIT_REST_RE:
981 case NODE_KIND::NT_STR_REPLACE_REG:
982 case NODE_KIND::NT_STR_REPLACE_REG_ALL:
983 case NODE_KIND::NT_STR_INDEXOF_REG:
984 case NODE_KIND::NT_REG_LOOP:
985 return nullptr;
986 case NODE_KIND::NT_BV_EXTRACT:
987 if (l->isCBV() && m->isCInt() && r->isCInt()) {
988 return mkConstBv(BitVectorUtils::bvExtract(l->toString(), toInt(m), toInt(r)), toInt(m).toULong() - toInt(r).toULong() + 1);
989 }
990 else if (m->isCInt() && toInt(m) == l->getSort()->getBitWidth() - 1 && isZero(r))
991 return l;
992 else if (m->isInt() && r->isCInt() && l->isBVExtract() && l->getChild(1)->isCInt() && l->getChild(2)->isCInt()) {
993 m = mkConstInt(toInt(m) + toInt(l->getChild(2)));
994 r = mkConstInt(toInt(r) + toInt(l->getChild(2)));
995 l = l->getChild(0);
996 return rewrite(t, l, m, r);
997 }
998 else
999 return nullptr;
1000 default:
1001 echo_error("unexpect NODE_KIND in rewrite ternary !!!");
1002 return nullptr;
1003 }
1004}
1005
1006// 4-ary
1007std::shared_ptr<DAGNode> Parser::rewrite(NODE_KIND &t, std::shared_ptr<DAGNode> &l, std::shared_ptr<DAGNode> &ml, std::shared_ptr<DAGNode> &mr, std::shared_ptr<DAGNode> &r) {
1008 switch (t) {
1009 case NODE_KIND::NT_FP_FMA:
1010 // case NODE_KIND::NT_FP_TO_FP:
1011 return nullptr;
1012 default:
1013 echo_error("unexpect NODE_KIND in rewrite 4-ary !!!");
1014 return nullptr;
1015 }
1016}
1017
1018// n-ary
1019std::shared_ptr<DAGNode> Parser::rewrite(NODE_KIND &t, std::vector<std::shared_ptr<DAGNode>> &p) {
1020 // return nullptr;
1021 switch (t) {
1022 case NODE_KIND::NT_LE: {
1023 std::vector<std::shared_ptr<DAGNode>> np{p.front()};
1024 np.reserve(p.size());
1025 size_t suf_count = (np.front()->isCInt() || np.front()->isCReal());
1026 std::shared_ptr<DAGNode> last_const = suf_count ? np.front() : nullptr;
1027 for (size_t i = 1, isz = p.size(); i < isz; ++i) {
1028 if (p.at(i) == np.back())
1029 continue;
1030 else if (p.at(i)->isCInt() || p.at(i)->isCReal()) {
1031 if (last_const != nullptr) {
1032 if (p.at(i)->isCInt() && last_const->isCInt()) {
1033 auto lvalue = toInt(last_const), rvalue = toInt(p.at(i));
1034 if (lvalue > rvalue)
1035 return mkFalse();
1036 else if (last_const == np.back() && lvalue == rvalue)
1037 continue;
1038 }
1039 else {
1040 auto lvalue = toReal(last_const), rvalue = toReal(p.at(i));
1041 if (lvalue > rvalue)
1042 return mkFalse();
1043 else if (last_const == np.back() && lvalue == rvalue)
1044 continue;
1045 }
1046 }
1047
1048 last_const = p.at(i);
1049 ++suf_count;
1050 }
1051 else
1052 suf_count = 0;
1053 if (suf_count > 2) {
1054 np.pop_back();
1055 suf_count = 2;
1056 }
1057 np.emplace_back(p.at(i));
1058 }
1059
1060 size_t lidx = 0, ridx = np.size() - 1;
1061 if (np.front()->isConst())
1062 while (lidx + 1 < np.size()) {
1063 if (!np.at(lidx + 1)->isConst())
1064 break;
1065 ++lidx;
1066 }
1067 if (np.back()->isConst())
1068 while (ridx > 0) {
1069 if (!np.at(ridx - 1)->isConst())
1070 break;
1071 --ridx;
1072 }
1073 if (lidx >= ridx)
1074 return mkTrue();
1075 np = std::vector<std::shared_ptr<DAGNode>>(np.begin() + lidx, np.begin() + ridx + 1);
1076
1077 if (np.size() <= 1)
1078 return mkTrue();
1079 else if (np.front()->isConst() && np.back()->isConst()) {
1080 if (toReal(np.front()) == toReal(np.back())) {
1081 np.pop_back();
1082 t = NODE_KIND::NT_EQ;
1083 return rewrite(t, np);
1084 }
1085 }
1086 p.swap(np);
1087 return nullptr;
1088 }
1089 case NODE_KIND::NT_LT: {
1090 std::vector<std::shared_ptr<DAGNode>> np{p.front()};
1091 np.reserve(p.size());
1092 size_t suf_count = (np.front()->isCInt() || np.front()->isCReal());
1093 std::shared_ptr<DAGNode> last_const = suf_count ? np.front() : nullptr;
1094 for (size_t i = 1, isz = p.size(); i < isz; ++i) {
1095 if (p.at(i) == np.back())
1096 return mkFalse();
1097 else if (p.at(i)->isCInt() || p.at(i)->isCReal()) {
1098 if (last_const != nullptr) {
1099 if (p.at(i)->isCInt() && last_const->isCInt()) {
1100 auto lvalue = toInt(last_const), rvalue = toInt(p.at(i));
1101 if (lvalue >= rvalue)
1102 return mkFalse();
1103 }
1104 else {
1105 auto lvalue = toReal(last_const), rvalue = toReal(p.at(i));
1106 if (lvalue >= rvalue)
1107 return mkFalse();
1108 }
1109 }
1110
1111 last_const = p.at(i);
1112 ++suf_count;
1113 }
1114 else
1115 suf_count = 0;
1116 if (suf_count > 2) {
1117 np.pop_back();
1118 suf_count = 2;
1119 }
1120 np.emplace_back(p.at(i));
1121 }
1122 size_t lidx = 0, ridx = np.size() - 1;
1123 if (np.front()->isConst())
1124 while (lidx + 1 < np.size()) {
1125 if (!np.at(lidx + 1)->isConst())
1126 break;
1127 ++lidx;
1128 }
1129 if (np.back()->isConst())
1130 while (ridx > 0) {
1131 if (!np.at(ridx - 1)->isConst())
1132 break;
1133 --ridx;
1134 }
1135 if (lidx >= ridx)
1136 return mkTrue();
1137 np = std::vector<std::shared_ptr<DAGNode>>(np.begin() + lidx, np.begin() + ridx + 1);
1138
1139 if (np.size() <= 1)
1140 return mkTrue();
1141 // if (np.size() == suf_count || np.size() == 1)
1142 // return mkTrue();
1143 p.swap(np);
1144 return nullptr;
1145 }
1146 case NODE_KIND::NT_GE:
1147 t = NODE_KIND::NT_LE;
1148 std::reverse(p.begin(), p.end());
1149 return rewrite(t, p);
1150 case NODE_KIND::NT_GT:
1151 t = NODE_KIND::NT_LT;
1152 std::reverse(p.begin(), p.end());
1153 return rewrite(t, p);
1154 case NODE_KIND::NT_EQ:
1155 case NODE_KIND::NT_EQ_BOOL:
1156 case NODE_KIND::NT_EQ_OTHER:
1157 std::sort(p.begin(), p.end(), [](const std::shared_ptr<DAGNode> &a, const std::shared_ptr<DAGNode> &b) {
1158 if (a->isConst() && !b->isConst())
1159 return false;
1160 else if (!a->isConst() && b->isConst())
1161 return true;
1162 else
1163 return a < b;
1164 });
1165 p.erase(std::unique(p.begin(), p.end()), p.end());
1166 while (p.size() >= 2 && p.rbegin()[0]->isConst() && p.rbegin()[1]->isConst()) {
1167 if (p.rbegin()[0]->isCInt() && p.rbegin()[1]->isCInt())
1168 return mkFalse();
1169 else if (p.rbegin()[0]->isNumeral() && p.rbegin()[1]->isNumeral()) {
1170 if (toReal(p.rbegin()[0]) != toReal(p.rbegin()[1]))
1171 return mkFalse();
1172 p.pop_back();
1173 }
1174 else if (p.rbegin()[0]->getName() == "(fp_bit_representation)" || p.rbegin()[1]->getName() == "(fp_bit_representation)") {
1175 break;
1176 }
1177 else
1178 return mkFalse();
1179 }
1180 if (p.size() <= 1)
1181 return mkTrue();
1182 return nullptr;
1183 case NODE_KIND::NT_DIV_INT: {
1184 if (p.front()->isCInt() || p.front()->isCReal()) {
1185 std::vector<std::shared_ptr<DAGNode>> np;
1186 np.reserve(p.size());
1187 std::shared_ptr<DAGNode> last_const = p.front();
1188 for (size_t i = 1, isz = p.size(); i < isz; ++i) {
1189 if (p.at(i)->isCInt() || p.at(i)->isCReal()) {
1190 if (last_const->isCInt() && p.at(i)->isCInt())
1191 last_const = mkConstInt(toInt(last_const) / toInt(p.at(i)));
1192 else if (getEvaluateUseFloating())
1193 last_const = mkConstInt((toReal(last_const) / toReal(p.at(i))).floor().toInt());
1194 else
1195 echo_error("unexpected divide int rewrite !!!");
1196 }
1197 else {
1198 for (size_t j = i; j < isz; ++j)
1199 np.emplace_back(p.at(j));
1200 break;
1201 }
1202 }
1203 if (np.empty())
1204 return last_const;
1205 np.insert(np.begin(), last_const);
1206 p.swap(np);
1207 }
1208 return nullptr;
1209 }
1210 case NODE_KIND::NT_DIV_REAL:
1211 return nullptr;
1212 case NODE_KIND::NT_STR_LT: {
1213 std::vector<std::shared_ptr<DAGNode>> np{p.front()};
1214 np.reserve(p.size());
1215 size_t suf_count = np.front()->isCStr();
1216 std::shared_ptr<DAGNode> last_const = suf_count ? np.front() : nullptr;
1217 for (size_t i = 1, isz = p.size(); i < isz; ++i) {
1218 if (p.at(i) == np.back())
1219 return mkFalse();
1220 else if (p.at(i)->isCStr()) {
1221 if (last_const != nullptr) {
1222 auto lvalue = last_const->toString(), rvalue = p.at(i)->toString();
1223 if (lvalue >= rvalue)
1224 return mkFalse();
1225 }
1226
1227 last_const = p.at(i);
1228 ++suf_count;
1229 }
1230 else
1231 suf_count = 0;
1232 if (suf_count > 2) {
1233 np.pop_back();
1234 suf_count = 2;
1235 }
1236 np.emplace_back(p.at(i));
1237 }
1238 size_t lidx = 0, ridx = np.size() - 1;
1239 if (np.front()->isConst())
1240 while (lidx + 1 < np.size()) {
1241 if (!np.at(lidx + 1)->isConst())
1242 break;
1243 ++lidx;
1244 }
1245 if (np.back()->isConst())
1246 while (ridx > 0) {
1247 if (!np.at(ridx - 1)->isConst())
1248 break;
1249 --ridx;
1250 }
1251 if (lidx >= ridx)
1252 return mkTrue();
1253 np = std::vector<std::shared_ptr<DAGNode>>(np.begin() + lidx, np.begin() + ridx + 1);
1254
1255 if (np.size() <= 1)
1256 return mkTrue();
1257 p.swap(np);
1258 return nullptr;
1259 }
1260 case NODE_KIND::NT_STR_LE: {
1261 std::vector<std::shared_ptr<DAGNode>> np{p.front()};
1262 np.reserve(p.size());
1263 size_t suf_count = np.front()->isCStr();
1264 std::shared_ptr<DAGNode> last_const = suf_count ? np.front() : nullptr;
1265 for (size_t i = 1, isz = p.size(); i < isz; ++i) {
1266 if (p.at(i) == np.back())
1267 continue;
1268 else if (p.at(i)->isCStr()) {
1269 if (last_const != nullptr) {
1270 auto lvalue = last_const->toString(), rvalue = p.at(i)->toString();
1271 if (lvalue > rvalue)
1272 return mkFalse();
1273 else if (last_const == np.back() && lvalue == rvalue)
1274 continue;
1275 }
1276
1277 last_const = p.at(i);
1278 ++suf_count;
1279 }
1280 else
1281 suf_count = 0;
1282 if (suf_count > 2) {
1283 np.pop_back();
1284 suf_count = 2;
1285 }
1286 np.emplace_back(p.at(i));
1287 }
1288
1289 size_t lidx = 0, ridx = np.size() - 1;
1290 if (np.front()->isConst())
1291 while (lidx + 1 < np.size()) {
1292 if (!np.at(lidx + 1)->isConst())
1293 break;
1294 ++lidx;
1295 }
1296 if (np.back()->isConst())
1297 while (ridx > 0) {
1298 if (!np.at(ridx - 1)->isConst())
1299 break;
1300 --ridx;
1301 }
1302 if (lidx >= ridx)
1303 return mkTrue();
1304 np = std::vector<std::shared_ptr<DAGNode>>(np.begin() + lidx, np.begin() + ridx + 1);
1305
1306 if (np.size() <= 1)
1307 return mkTrue();
1308 else if (np.front()->isConst() && np.back()->isConst()) {
1309 if (np.front()->toString() == np.back()->toString()) {
1310 np.pop_back();
1311 t = NODE_KIND::NT_EQ;
1312 return rewrite(t, np);
1313 }
1314 }
1315 p.swap(np);
1316 return nullptr;
1317 }
1318 case NODE_KIND::NT_STR_GT:
1319 t = NODE_KIND::NT_STR_LT;
1320 std::reverse(p.begin(), p.end());
1321 return rewrite(t, p);
1322 case NODE_KIND::NT_STR_GE:
1323 t = NODE_KIND::NT_STR_LE;
1324 std::reverse(p.begin(), p.end());
1325 return rewrite(t, p);
1326 case NODE_KIND::NT_DISTINCT:
1327 case NODE_KIND::NT_DISTINCT_BOOL:
1328 case NODE_KIND::NT_DISTINCT_OTHER:
1329 std::sort(p.begin(), p.end());
1330 for (size_t i = 1, isz = p.size(); i < isz; ++i) {
1331 if (p.at(i) == p.at(i - 1))
1332 return mkFalse();
1333 }
1334 return nullptr;
1335 case NODE_KIND::NT_AND: {
1336 std::sort(p.begin(), p.end());
1337 std::vector<std::shared_ptr<DAGNode>> np;
1338 np.reserve(p.size());
1339 for (const auto &pc : p) {
1340 if (pc->isFalse())
1341 return mkFalse();
1342 else if (pc->isTrue())
1343 continue;
1344 else if (!np.empty() && pc == np.back())
1345 continue;
1346 else
1347 np.emplace_back(pc);
1348 }
1349 if (np.empty())
1350 return mkTrue();
1351 else if (np.size() == 1)
1352 return np.front();
1353 p.swap(np);
1354 return nullptr;
1355 }
1356 case NODE_KIND::NT_OR: {
1357 std::sort(p.begin(), p.end());
1358 std::vector<std::shared_ptr<DAGNode>> np;
1359 np.reserve(p.size());
1360 for (const auto &pc : p) {
1361 if (pc->isTrue())
1362 return mkTrue();
1363 else if (pc->isFalse())
1364 continue;
1365 else if (!np.empty() && pc == np.back())
1366 continue;
1367 else
1368 np.emplace_back(pc);
1369 }
1370 if (np.empty())
1371 return mkFalse();
1372 else if (np.size() == 1)
1373 return np.front();
1374 p.swap(np);
1375 return nullptr;
1376 }
1377 case NODE_KIND::NT_IMPLIES: {
1378 if (p.back()->isTrue())
1379 return mkTrue();
1380 std::vector<std::shared_ptr<DAGNode>> np;
1381 np.reserve(p.size());
1382 for (size_t i = 0, isz = p.size() - 1; i < isz; ++i) {
1383 if (p.at(i)->isFalse())
1384 return mkTrue();
1385 else if (p.at(i)->isTrue())
1386 continue;
1387 else if (!np.empty() && p.at(i) == np.back())
1388 continue;
1389 else if (p.at(i) == p.back())
1390 return mkTrue();
1391 else
1392 np.emplace_back(p.at(i));
1393 }
1394 np.emplace_back(p.back());
1395 if (np.size() == 1)
1396 return np.front();
1397 p.swap(np);
1398 return nullptr;
1399 }
1400 case NODE_KIND::NT_XOR: {
1401 std::sort(p.begin(), p.end());
1402 std::vector<std::shared_ptr<DAGNode>> np;
1403 np.reserve(p.size());
1404 for (const auto &pc : p) {
1405 if (pc->isFalse())
1406 continue;
1407 else if (!np.empty() && pc == np.back())
1408 np.pop_back();
1409 else
1410 np.emplace_back(pc);
1411 }
1412 if (np.empty())
1413 return mkFalse();
1414 else if (np.size() == 1)
1415 return np.front();
1416 p.swap(np);
1417 return nullptr;
1418 }
1419 case NODE_KIND::NT_ADD: {
1420 std::shared_ptr<DAGNode> cst = nullptr;
1421 std::vector<std::shared_ptr<DAGNode>> np;
1422 np.reserve(p.size());
1423 for (const auto &pc : p) {
1424 if (pc->isCInt()) {
1425 if (cst == nullptr)
1426 cst = pc;
1427 else
1428 cst = mkConstInt(toInt(cst) + toInt(pc));
1429 }
1430 else if (pc->isCReal()) {
1431 if (cst == nullptr)
1432 cst = pc;
1433 else
1434 cst = mkConstReal(toReal(cst) + toReal(pc));
1435 }
1436 else
1437 np.emplace_back(pc);
1438 }
1439
1440 if (cst != nullptr) {
1441 if (!isZero(cst))
1442 np.emplace_back(cst);
1443 }
1444 if (np.empty())
1445 return mkConstInt(0);
1446 else if (np.size() == 1)
1447 return np.front();
1448 p.swap(np);
1449 return nullptr;
1450 }
1451 case NODE_KIND::NT_MUL: {
1452 std::shared_ptr<DAGNode> cst = nullptr;
1453 std::vector<std::shared_ptr<DAGNode>> np;
1454 np.reserve(p.size());
1455 for (const auto &pc : p) {
1456 if (pc->isCInt()) {
1457 if (cst == nullptr)
1458 cst = pc;
1459 else
1460 cst = mkConstInt(toInt(cst) * toInt(pc));
1461 }
1462 else if (pc->isCReal()) {
1463 if (cst == nullptr)
1464 cst = pc;
1465 else
1466 cst = mkConstReal(toReal(cst) * toReal(pc));
1467 }
1468 else
1469 np.emplace_back(pc);
1470 }
1471
1472 if (cst != nullptr) {
1473 if (isZero(cst))
1474 return cst->isCInt() ? mkConstInt(0) : mkConstReal(0.0);
1475 else if (!isOne(cst))
1476 np.emplace_back(cst);
1477 }
1478 if (np.size() == 1)
1479 return np.front();
1480 else if (np.empty())
1481 return mkConstInt(1);
1482 p.swap(np);
1483 return nullptr;
1484 }
1485 case NODE_KIND::NT_IAND: {
1486 std::shared_ptr<DAGNode> cst = nullptr;
1487 std::vector<std::shared_ptr<DAGNode>> np;
1488 np.reserve(p.size());
1489 for (const auto &pc : p) {
1490 if (pc->isCInt()) {
1491 if (cst == nullptr)
1492 cst = pc;
1493 else
1494 cst = mkConstInt(toInt(cst) & toInt(pc));
1495 }
1496 else
1497 np.emplace_back(pc);
1498 }
1499
1500 if (cst != nullptr) {
1501 if (isZero(cst))
1502 return cst;
1503 else
1504 np.emplace_back(cst);
1505 }
1506 if (np.size() == 1)
1507 return np.front();
1508 p.swap(np);
1509 return nullptr;
1510 }
1511 case NODE_KIND::NT_SUB: {
1512 std::vector<std::shared_ptr<DAGNode>> np{p.front()};
1513 np.reserve(p.size());
1514 for (size_t i = 1, isz = p.size(); i < isz; ++i) {
1515 const auto &pc = p.at(i);
1516 if (pc == np.back()) {
1517 np.pop_back();
1518 if (pc->getSort()->isInt())
1519 np.emplace_back(mkConstInt(0));
1520 else
1521 np.emplace_back(mkConstReal(0.0));
1522 }
1523 else if (pc->isNumeral() && np.back()->isNumeral()) {
1524 if (pc->isCInt() && np.back()->isCInt())
1525 np.back() = mkConstInt(toInt(np.back()) - toInt(pc));
1526 else
1527 np.back() = mkConstReal(toReal(np.back()) - toReal(pc));
1528 }
1529 else {
1530 for (size_t j = i; j < isz; ++j)
1531 np.emplace_back(p.at(j));
1532 break;
1533 }
1534 }
1535
1536 if (np.size() == 1)
1537 return np.front();
1538 p.swap(np);
1539 return nullptr;
1540 }
1541 case NODE_KIND::NT_BV_AND: {
1542 std::sort(p.begin(), p.end());
1543 std::vector<std::shared_ptr<DAGNode>> np;
1544 np.reserve(p.size());
1545 std::shared_ptr<DAGNode> cst = nullptr;
1546 for (const auto &pc : p) {
1547 if (pc->isCBV()) {
1548 if (cst == nullptr)
1549 cst = pc;
1550 else
1551 cst = mkConstBv(BitVectorUtils::bvAnd(cst->toString(), pc->toString()), cst->getSort()->getBitWidth());
1552 }
1553 else if (!np.empty() && pc == np.back())
1554 continue;
1555 else
1556 np.emplace_back(pc);
1557 }
1558
1559 if (cst != nullptr) {
1560 if (isZero(cst))
1561 return cst;
1562 else if (!isOnes(cst))
1563 np.emplace_back(cst);
1564 }
1565
1566 if (np.empty())
1567 return mkConstBv(BitVectorUtils::mkOnes(p.front()->getSort()->getBitWidth()), p.front()->getSort()->getBitWidth());
1568 else if (np.size() == 1)
1569 return np.front();
1570 p.swap(np);
1571 return nullptr;
1572 }
1573 case NODE_KIND::NT_BV_OR: {
1574 std::sort(p.begin(), p.end());
1575 std::vector<std::shared_ptr<DAGNode>> np;
1576 np.reserve(p.size());
1577 std::shared_ptr<DAGNode> cst = nullptr;
1578 for (const auto &pc : p) {
1579 if (pc->isCBV()) {
1580 if (cst == nullptr)
1581 cst = pc;
1582 else
1583 cst = mkConstBv(BitVectorUtils::bvOr(cst->toString(), pc->toString()), cst->getSort()->getBitWidth());
1584 }
1585 else if (!np.empty() && pc == np.back())
1586 continue;
1587 else
1588 np.emplace_back(pc);
1589 }
1590
1591 if (cst != nullptr) {
1592 if (isOnes(cst))
1593 return cst;
1594 else if (!isZero(cst))
1595 np.emplace_back(cst);
1596 }
1597
1598 if (np.empty())
1599 return mkConstBv(BitVectorUtils::intToBv(0, p.front()->getSort()->getBitWidth()), p.front()->getSort()->getBitWidth());
1600 else if (np.size() == 1)
1601 return np.front();
1602 p.swap(np);
1603 return nullptr;
1604 }
1605 case NODE_KIND::NT_BV_XOR: {
1606 std::sort(p.begin(), p.end());
1607 std::vector<std::shared_ptr<DAGNode>> np;
1608 np.reserve(p.size());
1609 std::shared_ptr<DAGNode> cst = nullptr;
1610 for (const auto &pc : p) {
1611 if (pc->isCBV()) {
1612 if (cst == nullptr)
1613 cst = pc;
1614 else
1615 cst = mkConstBv(BitVectorUtils::bvXor(cst->toString(), pc->toString()), cst->getSort()->getBitWidth());
1616 }
1617 else if (!np.empty() && pc == np.back())
1618 np.pop_back();
1619 else
1620 np.emplace_back(pc);
1621 }
1622
1623 if (cst != nullptr) {
1624 if (!isZero(cst))
1625 np.emplace_back(cst);
1626 }
1627
1628 if (np.empty())
1629 return mkConstBv(BitVectorUtils::intToBv(0, p.front()->getSort()->getBitWidth()), p.front()->getSort()->getBitWidth());
1630 else if (np.size() == 1)
1631 return np.front();
1632 p.swap(np);
1633 return nullptr;
1634 }
1635
1636 case NODE_KIND::NT_BV_COMP: {
1637 std::sort(p.begin(), p.end());
1638 p.erase(std::unique(p.begin(), p.end()), p.end());
1639 bool has_const = false;
1640 for (const auto &pc : p) {
1641 if (pc->isCBV()) {
1642 if (has_const)
1643 return mkFalse();
1644 else
1645 has_const = true;
1646 }
1647 }
1648 if (p.size() <= 1)
1649 return mkConstBv("#b1", 1);
1650 return nullptr;
1651 }
1652 case NODE_KIND::NT_BV_ADD: {
1653 std::shared_ptr<DAGNode> cst = nullptr;
1654 std::vector<std::shared_ptr<DAGNode>> np;
1655 np.reserve(p.size());
1656 for (const auto &pc : p) {
1657 if (pc->isCBV()) {
1658 if (cst == nullptr)
1659 cst = pc;
1660 else
1661 cst = mkConstBv(BitVectorUtils::bvAdd(cst->toString(), pc->toString()), cst->getSort()->getBitWidth());
1662 }
1663 else
1664 np.emplace_back(pc);
1665 }
1666
1667 if (cst != nullptr) {
1668 if (!isZero(cst))
1669 np.emplace_back(cst);
1670 }
1671 if (np.empty())
1672 return mkConstBv(BitVectorUtils::intToBv(0, p.front()->getSort()->getBitWidth()), p.front()->getSort()->getBitWidth());
1673 else if (np.size() == 1)
1674 return np.front();
1675 p.swap(np);
1676 return nullptr;
1677 }
1678 case NODE_KIND::NT_BV_MUL: {
1679 std::shared_ptr<DAGNode> cst = nullptr;
1680 std::vector<std::shared_ptr<DAGNode>> np;
1681 np.reserve(p.size());
1682 for (const auto &pc : p) {
1683 if (pc->isCBV()) {
1684 if (cst == nullptr)
1685 cst = pc;
1686 else
1687 cst = mkConstBv(BitVectorUtils::bvMul(cst->toString(), pc->toString()), cst->getSort()->getBitWidth());
1688 }
1689 else
1690 np.emplace_back(pc);
1691 }
1692
1693 if (cst != nullptr) {
1694 if (isZero(cst))
1695 return cst;
1696 else if (!isOne(cst))
1697 np.emplace_back(cst);
1698 }
1699 if (np.size() == 1)
1700 return np.front();
1701 else if (np.empty())
1702 return mkConstBv(BitVectorUtils::intToBv(1, p.front()->getSort()->getBitWidth()), p.front()->getSort()->getBitWidth());
1703 p.swap(np);
1704 return nullptr;
1705 }
1706
1707 case NODE_KIND::NT_BV_SADDO:
1708 case NODE_KIND::NT_BV_UADDO:
1709 case NODE_KIND::NT_BV_SMULO:
1710 case NODE_KIND::NT_BV_UMULO:
1711 return nullptr;
1712 case NODE_KIND::NT_BV_CONCAT: {
1713 // return nullptr;
1714 std::vector<std::shared_ptr<DAGNode>> np{p.front()};
1715 for (size_t i = 1, isz = p.size(); i < isz; ++i) {
1716 if (p.at(i)->isCBV() && np.back()->isCBV()) {
1717 // std::cout << np.back()->getSort()->getBitWidth() << ' ' << p.at(i)->getSort()->getBitWidth() << std::endl;
1718
1719 np.back() = (mkConstBv(BitVectorUtils::bvConcat(np.back()->toString(), p.at(i)->toString()),
1720 np.back()->getSort()->getBitWidth() + p.at(i)->getSort()->getBitWidth()));
1721 }
1722 else
1723 np.emplace_back(p.at(i));
1724 }
1725 if (np.size() == 1)
1726 return np.front();
1727 else if (np.size() == 2) {
1728 if (isZero(np.front())) {
1729 return mkBvZeroExt(np.back(), mkConstInt(np.front()->getSort()->getBitWidth()));
1730 }
1731 }
1732 p.swap(np);
1733 return nullptr;
1734 }
1735
1736 case NODE_KIND::NT_FP_LE:
1737 case NODE_KIND::NT_FP_LT:
1738 return nullptr;
1739 case NODE_KIND::NT_FP_GE:
1740 t = NODE_KIND::NT_FP_LE;
1741 std::reverse(p.begin(), p.end());
1742 return rewrite(t, p);
1743 case NODE_KIND::NT_FP_GT:
1744 t = NODE_KIND::NT_FP_LT;
1745 std::reverse(p.begin(), p.end());
1746 return rewrite(t, p);
1747 case NODE_KIND::NT_FP_EQ:
1748 return nullptr;
1749 case NODE_KIND::NT_STR_CONCAT: {
1750 // return nullptr;
1751 std::vector<std::shared_ptr<DAGNode>> np{p.front()};
1752 for (size_t i = 1, isz = p.size(); i < isz; ++i) {
1753 if (p.at(i)->isCStr() && np.back()->isCStr()) {
1754 std::string l_str = np.back()->toString();
1755 std::string r_str = p.at(i)->toString();
1756 if (l_str.back() == '\"' && r_str.front() == '\"')
1757 np.back() = mkConstStr(l_str.substr(0, l_str.size() - 1) + r_str.substr(1));
1758 else
1759 np.back() = mkConstStr(l_str + r_str);
1760 }
1761 else if (p.at(i)->isCStr() && (p.at(i)->toString() == "\"\""))
1762 continue;
1763 else
1764 np.emplace_back(p.at(i));
1765 }
1766 // return nullptr;
1767 if (np.size() > 1 && np.front()->isCStr() && (np.front()->toString() == "\"\"")) {
1768 np.erase(np.begin());
1769 }
1770 if (np.size() == 1)
1771 return np.front();
1772 p.swap(np);
1773 return nullptr;
1774 }
1775 case NODE_KIND::NT_REG_CONCAT:
1776 case NODE_KIND::NT_REG_UNION:
1777 case NODE_KIND::NT_REG_INTER:
1778 case NODE_KIND::NT_REG_DIFF:
1779 return nullptr;
1780 case NODE_KIND::NT_FORALL:
1781 case NODE_KIND::NT_EXISTS:
1782 return nullptr;
1783 case NODE_KIND::NT_MAX: {
1784 std::shared_ptr<DAGNode> cst = nullptr;
1785 std::sort(p.begin(), p.end());
1786 p.erase(std::unique(p.begin(), p.end()), p.end());
1787 std::vector<std::shared_ptr<DAGNode>> np;
1788 for (const auto &pc : p) {
1789 if (pc->isCInt()) {
1790 if (cst == nullptr)
1791 cst = pc;
1792 else if (cst->isCInt()) {
1793 if (toInt(pc) > toInt(cst))
1794 cst = pc;
1795 }
1796 else if (cst->isCReal()) {
1797 if (toReal(pc) > toReal(cst))
1798 cst = pc;
1799 }
1800 }
1801 else if (pc->isCReal()) {
1802 if (cst == nullptr)
1803 cst = pc;
1804 else if (toReal(pc) > toReal(cst))
1805 cst = pc;
1806 }
1807 else {
1808 if (pc->isConst())
1809 echo_error("unexpected constant type in MIN operation!");
1810 np.emplace_back(pc);
1811 }
1812 }
1813 if (cst != nullptr)
1814 np.emplace_back(cst);
1815 if (np.size() == 1)
1816 return np.front();
1817 p.swap(np);
1818 return nullptr;
1819 }
1820 case NODE_KIND::NT_MIN: {
1821 std::shared_ptr<DAGNode> cst = nullptr;
1822 std::vector<std::shared_ptr<DAGNode>> np;
1823 std::sort(p.begin(), p.end());
1824 p.erase(std::unique(p.begin(), p.end()), p.end());
1825 for (const auto &pc : p) {
1826 if (pc->isCInt()) {
1827 if (cst == nullptr)
1828 cst = pc;
1829 else if (cst->isCInt()) {
1830 if (toInt(pc) < toInt(cst))
1831 cst = pc;
1832 }
1833 else if (cst->isCReal()) {
1834 if (toReal(pc) < toReal(cst))
1835 cst = pc;
1836 }
1837 }
1838 else if (pc->isCReal()) {
1839 if (cst == nullptr)
1840 cst = pc;
1841 else if (toReal(pc) < toReal(cst))
1842 cst = pc;
1843 }
1844 else {
1845 if (pc->isConst())
1846 echo_error("unexpected constant type in MIN operation!");
1847 np.emplace_back(pc);
1848 }
1849 }
1850 if (cst != nullptr)
1851 np.emplace_back(cst);
1852 if (np.size() == 1)
1853 return np.front();
1854 p.swap(np);
1855 return nullptr;
1856 }
1857 default: {
1858 std::cout << "NODEKIND: " << kindToString(t) << std::endl;
1859 echo_error("unexpect NODE_KIND in rewrite n-ary !!!");
1860 return nullptr;
1861 }
1862 }
1863}
1864
1865std::shared_ptr<DAGNode> Parser::rewrite_oper(NODE_KIND &t, std::vector<std::shared_ptr<DAGNode>> &p) {
1866 // return nullptr;
1867 if (!options->getRewrite())
1868 return nullptr;
1869 if (getArity(t) > 0 && p.size() != getArity(t)) {
1870 throw std::runtime_error("error: params number not equal to arity !!!");
1871 }
1872 switch (t) {
1873 // zero-ary
1874 case NODE_KIND::NT_NULL:
1875 case NODE_KIND::NT_CONST:
1876 case NODE_KIND::NT_VAR:
1877 case NODE_KIND::NT_TEMP_VAR:
1878 case NODE_KIND::NT_CONST_TRUE:
1879 case NODE_KIND::NT_CONST_FALSE:
1880 case NODE_KIND::NT_CONST_PI:
1881 case NODE_KIND::NT_CONST_E:
1882 case NODE_KIND::NT_INFINITY:
1883 case NODE_KIND::NT_POS_INFINITY:
1884 case NODE_KIND::NT_NEG_INFINITY:
1885 case NODE_KIND::NT_NAN:
1886 case NODE_KIND::NT_EPSILON:
1887 case NODE_KIND::NT_POS_EPSILON:
1888 case NODE_KIND::NT_NEG_EPSILON:
1889 case NODE_KIND::NT_REG_NONE:
1890 case NODE_KIND::NT_REG_ALL:
1891 case NODE_KIND::NT_REG_ALLCHAR:
1892 case NODE_KIND::NT_QUANT_VAR:
1893 return nullptr;
1894
1895 // unary
1896 case NODE_KIND::NT_CONST_ARRAY:
1897 case NODE_KIND::NT_NOT:
1898 case NODE_KIND::NT_NEG:
1899 case NODE_KIND::NT_ABS:
1900 case NODE_KIND::NT_SQRT:
1901 case NODE_KIND::NT_SAFESQRT:
1902 case NODE_KIND::NT_CEIL:
1903 case NODE_KIND::NT_FLOOR:
1904 case NODE_KIND::NT_ROUND:
1905 case NODE_KIND::NT_EXP:
1906 case NODE_KIND::NT_LN:
1907 case NODE_KIND::NT_LG:
1908 case NODE_KIND::NT_LB:
1909 case NODE_KIND::NT_SIN:
1910 case NODE_KIND::NT_COS:
1911 case NODE_KIND::NT_SEC:
1912 case NODE_KIND::NT_CSC:
1913 case NODE_KIND::NT_TAN:
1914 case NODE_KIND::NT_COT:
1915 case NODE_KIND::NT_ASIN:
1916 case NODE_KIND::NT_ACOS:
1917 case NODE_KIND::NT_ASEC:
1918 case NODE_KIND::NT_ACSC:
1919 case NODE_KIND::NT_ATAN:
1920 case NODE_KIND::NT_ACOT:
1921 case NODE_KIND::NT_SINH:
1922 case NODE_KIND::NT_COSH:
1923 case NODE_KIND::NT_TANH:
1924 case NODE_KIND::NT_SECH:
1925 case NODE_KIND::NT_CSCH:
1926 case NODE_KIND::NT_COTH:
1927 case NODE_KIND::NT_ASINH:
1928 case NODE_KIND::NT_ACOSH:
1929 case NODE_KIND::NT_ATANH:
1930 case NODE_KIND::NT_ASECH:
1931 case NODE_KIND::NT_ACSCH:
1932 case NODE_KIND::NT_ACOTH:
1933 case NODE_KIND::NT_TO_INT:
1934 case NODE_KIND::NT_TO_REAL:
1935 case NODE_KIND::NT_IS_INT:
1936 case NODE_KIND::NT_IS_PRIME:
1937 case NODE_KIND::NT_IS_EVEN:
1938 case NODE_KIND::NT_IS_ODD:
1939 case NODE_KIND::NT_FACT:
1940 case NODE_KIND::NT_BV_NOT:
1941 case NODE_KIND::NT_BV_NEG:
1942 case NODE_KIND::NT_BV_NEGO:
1943 case NODE_KIND::NT_FP_ABS:
1944 case NODE_KIND::NT_FP_NEG:
1945 case NODE_KIND::NT_FP_IS_NORMAL:
1946 case NODE_KIND::NT_FP_IS_SUBNORMAL:
1947 case NODE_KIND::NT_FP_IS_ZERO:
1948 case NODE_KIND::NT_FP_IS_INF:
1949 case NODE_KIND::NT_FP_IS_NAN:
1950 case NODE_KIND::NT_FP_IS_NEG:
1951 case NODE_KIND::NT_FP_IS_POS:
1952 case NODE_KIND::NT_FP_TO_REAL:
1953 case NODE_KIND::NT_STR_LEN:
1954 case NODE_KIND::NT_STR_TO_LOWER:
1955 case NODE_KIND::NT_STR_TO_UPPER:
1956 case NODE_KIND::NT_STR_REV:
1957 case NODE_KIND::NT_STR_IS_DIGIT:
1958 case NODE_KIND::NT_STR_FROM_INT:
1959 case NODE_KIND::NT_STR_TO_INT:
1960 case NODE_KIND::NT_STR_TO_REG:
1961 case NODE_KIND::NT_STR_TO_CODE:
1962 case NODE_KIND::NT_STR_FROM_CODE:
1963 case NODE_KIND::NT_REG_STAR:
1964 case NODE_KIND::NT_REG_PLUS:
1965 case NODE_KIND::NT_REG_OPT:
1966 case NODE_KIND::NT_REG_COMPLEMENT:
1967 case NODE_KIND::NT_BV_TO_NAT:
1968 case NODE_KIND::NT_BV_TO_INT:
1969 case NODE_KIND::NT_UBV_TO_INT:
1970 case NODE_KIND::NT_SBV_TO_INT:
1971 case NODE_KIND::NT_POW2:
1972 return rewrite(t, p.front());
1973
1974 // binary
1975 case NODE_KIND::NT_POW:
1976 case NODE_KIND::NT_MOD:
1977 case NODE_KIND::NT_LOG:
1978 case NODE_KIND::NT_ATAN2:
1979 case NODE_KIND::NT_IS_DIVISIBLE:
1980 case NODE_KIND::NT_GCD:
1981 case NODE_KIND::NT_LCM:
1982 case NODE_KIND::NT_BV_UDIV:
1983 case NODE_KIND::NT_BV_SDIV:
1984 case NODE_KIND::NT_BV_UREM:
1985 case NODE_KIND::NT_BV_SREM:
1986 case NODE_KIND::NT_BV_UMOD:
1987 case NODE_KIND::NT_BV_SMOD:
1988 case NODE_KIND::NT_BV_SDIVO:
1989 case NODE_KIND::NT_BV_UDIVO:
1990 case NODE_KIND::NT_BV_SREMO:
1991 case NODE_KIND::NT_BV_UREMO:
1992 case NODE_KIND::NT_BV_SMODO:
1993 case NODE_KIND::NT_BV_UMODO:
1994 case NODE_KIND::NT_BV_SHL:
1995 case NODE_KIND::NT_BV_LSHR:
1996 case NODE_KIND::NT_BV_ASHR:
1997 case NODE_KIND::NT_BV_ULT:
1998 case NODE_KIND::NT_BV_ULE:
1999 case NODE_KIND::NT_BV_UGT:
2000 case NODE_KIND::NT_BV_UGE:
2001 case NODE_KIND::NT_BV_SLT:
2002 case NODE_KIND::NT_BV_SLE:
2003 case NODE_KIND::NT_BV_SGT:
2004 case NODE_KIND::NT_BV_SGE:
2005 case NODE_KIND::NT_NAT_TO_BV:
2006 case NODE_KIND::NT_INT_TO_BV:
2007 case NODE_KIND::NT_FP_REM:
2008 case NODE_KIND::NT_FP_SQRT:
2009 case NODE_KIND::NT_FP_ROUND_TO_INTEGRAL:
2010 case NODE_KIND::NT_SELECT:
2011 case NODE_KIND::NT_STR_PREFIXOF:
2012 case NODE_KIND::NT_STR_SUFFIXOF:
2013 case NODE_KIND::NT_STR_CHARAT:
2014 case NODE_KIND::NT_STR_SPLIT:
2015 case NODE_KIND::NT_STR_IN_REG:
2016 case NODE_KIND::NT_STR_CONTAINS:
2017 case NODE_KIND::NT_STR_NUM_SPLITS_RE:
2018 case NODE_KIND::NT_REG_RANGE:
2019 case NODE_KIND::NT_REG_REPEAT:
2020 case NODE_KIND::NT_BV_REPEAT:
2021 case NODE_KIND::NT_BV_ZERO_EXT:
2022 case NODE_KIND::NT_BV_SIGN_EXT:
2023 case NODE_KIND::NT_BV_ROTATE_LEFT:
2024 case NODE_KIND::NT_BV_ROTATE_RIGHT:
2025 case NODE_KIND::NT_FP_MIN:
2026 case NODE_KIND::NT_FP_MAX:
2027 case NODE_KIND::NT_BV_XNOR:
2028 case NODE_KIND::NT_BV_NAND:
2029 case NODE_KIND::NT_BV_NOR:
2030 case NODE_KIND::NT_BV_SUB:
2031 return rewrite(t, p.at(0), p.at(1));
2032
2033 // ternary
2034 case NODE_KIND::NT_ITE:
2035 case NODE_KIND::NT_FP_ADD:
2036 case NODE_KIND::NT_FP_SUB:
2037 case NODE_KIND::NT_FP_MUL:
2038 case NODE_KIND::NT_FP_DIV:
2039 case NODE_KIND::NT_FP_TO_UBV:
2040 case NODE_KIND::NT_FP_TO_SBV:
2041 case NODE_KIND::NT_STORE:
2042 case NODE_KIND::NT_STR_SUBSTR:
2043 case NODE_KIND::NT_STR_INDEXOF:
2044 case NODE_KIND::NT_STR_UPDATE:
2045 case NODE_KIND::NT_STR_REPLACE:
2046 case NODE_KIND::NT_STR_REPLACE_ALL:
2047 case NODE_KIND::NT_STR_SPLIT_AT:
2048 case NODE_KIND::NT_STR_SPLIT_REST:
2049 case NODE_KIND::NT_STR_SPLIT_AT_RE:
2050 case NODE_KIND::NT_STR_SPLIT_REST_RE:
2051 case NODE_KIND::NT_STR_REPLACE_REG:
2052 case NODE_KIND::NT_STR_REPLACE_REG_ALL:
2053 case NODE_KIND::NT_STR_INDEXOF_REG:
2054 case NODE_KIND::NT_REG_LOOP:
2055 case NODE_KIND::NT_BV_EXTRACT:
2056 return rewrite(t, p.at(0), p.at(1), p.at(2));
2057
2058 // 4-ary
2059 case NODE_KIND::NT_FP_FMA:
2060 // case NODE_KIND::NT_FP_TO_FP:
2061 return rewrite(t, p.at(0), p.at(1), p.at(2), p.at(3));
2062
2063 // n-ary
2064 case NODE_KIND::NT_LE:
2065 case NODE_KIND::NT_LT:
2066 case NODE_KIND::NT_GE:
2067 case NODE_KIND::NT_GT:
2068 case NODE_KIND::NT_EQ:
2069 case NODE_KIND::NT_EQ_BOOL:
2070 case NODE_KIND::NT_EQ_OTHER:
2071 case NODE_KIND::NT_DIV_INT:
2072 case NODE_KIND::NT_DIV_REAL:
2073 case NODE_KIND::NT_STR_LT:
2074 case NODE_KIND::NT_STR_LE:
2075 case NODE_KIND::NT_STR_GT:
2076 case NODE_KIND::NT_STR_GE:
2077 case NODE_KIND::NT_DISTINCT:
2078 case NODE_KIND::NT_DISTINCT_BOOL:
2079 case NODE_KIND::NT_DISTINCT_OTHER:
2080 case NODE_KIND::NT_AND:
2081 case NODE_KIND::NT_OR:
2082 case NODE_KIND::NT_IMPLIES:
2083 case NODE_KIND::NT_XOR:
2084 case NODE_KIND::NT_ADD:
2085 case NODE_KIND::NT_MUL:
2086 case NODE_KIND::NT_IAND:
2087 case NODE_KIND::NT_SUB:
2088 case NODE_KIND::NT_BV_AND:
2089 case NODE_KIND::NT_BV_OR:
2090 case NODE_KIND::NT_BV_XOR:
2091 case NODE_KIND::NT_BV_COMP:
2092 case NODE_KIND::NT_BV_ADD:
2093 case NODE_KIND::NT_BV_MUL:
2094 case NODE_KIND::NT_BV_SADDO:
2095 case NODE_KIND::NT_BV_UADDO:
2096 case NODE_KIND::NT_BV_SMULO:
2097 case NODE_KIND::NT_BV_UMULO:
2098 case NODE_KIND::NT_BV_CONCAT:
2099
2100 case NODE_KIND::NT_FP_LE:
2101 case NODE_KIND::NT_FP_LT:
2102 case NODE_KIND::NT_FP_GE:
2103 case NODE_KIND::NT_FP_GT:
2104 case NODE_KIND::NT_FP_EQ:
2105 case NODE_KIND::NT_STR_CONCAT:
2106 case NODE_KIND::NT_REG_CONCAT:
2107 case NODE_KIND::NT_REG_UNION:
2108 case NODE_KIND::NT_REG_INTER:
2109 case NODE_KIND::NT_REG_DIFF:
2110 case NODE_KIND::NT_FORALL:
2111 case NODE_KIND::NT_EXISTS:
2112 case NODE_KIND::NT_MAX:
2113 case NODE_KIND::NT_MIN:
2114 return rewrite(t, p);
2115
2116 case NODE_KIND::NT_FP_TO_FP: // 3 or 4
2117 return nullptr;
2118
2119 default:
2120 return nullptr;
2121 }
2122}
2123} // namespace stabilizer::parser
stabilizer::parser::BitVectorUtils::bvNand
static std::string bvNand(const std::string &bv1, const std::string &bv2)
Definition util.cpp:390
stabilizer::parser::BitVectorUtils::bvComp
static bool bvComp(const std::string &bv1, const std::string &bv2, const NODE_KIND &kind)
Definition util.cpp:637
stabilizer::parser::BitVectorUtils::bvUdiv
static std::string bvUdiv(const std::string &bv1, const std::string &bv2)
Definition util.cpp:472
stabilizer::parser::BitVectorUtils::bvExtract
static std::string bvExtract(const std::string &bv, const Integer &i, const Integer &j)
Definition util.cpp:585
stabilizer::parser::BitVectorUtils::bvSub
static std::string bvSub(const std::string &bv1, const std::string &bv2)
Definition util.cpp:447
stabilizer::parser::BitVectorUtils::bvZeroExtend
static std::string bvZeroExtend(const std::string &bv, const Integer &n)
Definition util.cpp:608
stabilizer::parser::BitVectorUtils::bvSdiv
static std::string bvSdiv(const std::string &bv1, const std::string &bv2)
Definition util.cpp:504
stabilizer::parser::BitVectorUtils::bvCompareToUint
static int bvCompareToUint(const std::string &bv, const uint64_t &u)
Definition util.cpp:704
stabilizer::parser::BitVectorUtils::bvShl
static std::string bvShl(const std::string &bv, const std::string &n)
Definition util.cpp:541
stabilizer::parser::BitVectorUtils::bvLshr
static std::string bvLshr(const std::string &bv, const std::string &n)
Definition util.cpp:552
stabilizer::parser::BitVectorUtils::bvIsMaxUnsigned
static bool bvIsMaxUnsigned(const std::string &bv)
Definition util.cpp:692
stabilizer::parser::BitVectorUtils::bvConcat
static std::string bvConcat(const std::string &bv1, const std::string &bv2)
Definition util.cpp:577
stabilizer::parser::BitVectorUtils::bvXor
static std::string bvXor(const std::string &bv1, const std::string &bv2)
Definition util.cpp:378
stabilizer::parser::BitVectorUtils::bvRotateLeft
static std::string bvRotateLeft(const std::string &bv, const Integer &n)
Definition util.cpp:621
stabilizer::parser::BitVectorUtils::bvNot
static std::string bvNot(const std::string &bv)
Definition util.cpp:345
stabilizer::parser::BitVectorUtils::bvIsMaxSigned
static bool bvIsMaxSigned(const std::string &bv)
Definition util.cpp:676
stabilizer::parser::BitVectorUtils::bvToNat
static Integer bvToNat(const std::string &bv)
Definition util.cpp:724
stabilizer::parser::BitVectorUtils::natToBv
static std::string natToBv(const Integer &i, const Integer &n)
Definition util.cpp:733
stabilizer::parser::BitVectorUtils::bvSignExtend
static std::string bvSignExtend(const std::string &bv, const Integer &n)
Definition util.cpp:614
stabilizer::parser::BitVectorUtils::bvSrem
static std::string bvSrem(const std::string &bv1, const std::string &bv2)
Definition util.cpp:516
stabilizer::parser::BitVectorUtils::bvToInt
static Integer bvToInt(const std::string &bv)
Definition util.cpp:852
stabilizer::parser::BitVectorUtils::bvRotateRight
static std::string bvRotateRight(const std::string &bv, const Integer &n)
Definition util.cpp:628
stabilizer::parser::BitVectorUtils::bvIsNegOne
static bool bvIsNegOne(const std::string &bv)
Definition util.cpp:698
stabilizer::parser::BitVectorUtils::bvXnor
static std::string bvXnor(const std::string &bv1, const std::string &bv2)
Definition util.cpp:414
stabilizer::parser::BitVectorUtils::bvOr
static std::string bvOr(const std::string &bv1, const std::string &bv2)
Definition util.cpp:366
stabilizer::parser::BitVectorUtils::bvUrem
static std::string bvUrem(const std::string &bv1, const std::string &bv2)
Definition util.cpp:484
stabilizer::parser::BitVectorUtils::mkOnes
static std::string mkOnes(const Integer &n)
Definition util.cpp:720
stabilizer::parser::BitVectorUtils::bvNeg
static std::string bvNeg(const std::string &bv)
Definition util.cpp:427
stabilizer::parser::BitVectorUtils::bvSmod
static std::string bvSmod(const std::string &bv1, const std::string &bv2)
Definition util.cpp:528
stabilizer::parser::BitVectorUtils::bvAshr
static std::string bvAshr(const std::string &bv, const std::string &n)
Definition util.cpp:564
stabilizer::parser::BitVectorUtils::bvNor
static std::string bvNor(const std::string &bv1, const std::string &bv2)
Definition util.cpp:402
stabilizer::parser::BitVectorUtils::bvIsMinSigned
static bool bvIsMinSigned(const std::string &bv)
Definition util.cpp:684
stabilizer::parser::BitVectorUtils::bvAnd
static std::string bvAnd(const std::string &bv1, const std::string &bv2)
Definition util.cpp:354
stabilizer::parser::BitVectorUtils::bvRepeat
static std::string bvRepeat(const std::string &bv, const Integer &n)
Definition util.cpp:599
stabilizer::parser::BitVectorUtils::intToBv
static std::string intToBv(const Integer &i, const Integer &n)
Definition util.cpp:870
stabilizer::parser::BitVectorUtils::bvAdd
static std::string bvAdd(const std::string &bv1, const std::string &bv2)
Definition util.cpp:435
stabilizer::parser::BitVectorUtils::bvMul
static std::string bvMul(const std::string &bv1, const std::string &bv2)
Definition util.cpp:459
stabilizer::parser::HighPrecisionInteger::toString
std::string toString(int base=10) const
Definition number.cpp:1026
stabilizer::parser::HighPrecisionReal::atan2
static HighPrecisionReal atan2(const HighPrecisionReal &y, const HighPrecisionReal &x)
Definition number.cpp:471
stabilizer::parser::MathUtils::isEven
static bool isEven(const Integer &n)
Definition util.cpp:333
stabilizer::parser::MathUtils::lcm
static Integer lcm(const Integer &a, const Integer &b)
Definition util.cpp:284
stabilizer::parser::MathUtils::pow
static Integer pow(const Integer &base, const Integer &exp)
Definition util.cpp:267
stabilizer::parser::MathUtils::factorial
static Integer factorial(const Integer &n)
Definition util.cpp:337
stabilizer::parser::MathUtils::isPrime
static bool isPrime(const Integer &n)
Definition util.cpp:319
stabilizer::parser::MathUtils::gcd
static Integer gcd(const Integer &a, const Integer &b)
Definition util.cpp:278
stabilizer::parser::MathUtils::isOdd
static bool isOdd(const Integer &n)
Definition util.cpp:335
stabilizer::parser::NodeManager::NAN_NODE
static const std::shared_ptr< DAGNode > NAN_NODE
Definition dag.h:1291
stabilizer::parser::Parser::err_all
void err_all(const ERROR_TYPE e, const std::string s="", const size_t ln=0) const
Definition base_parser.cpp:2516
stabilizer::parser::Parser::options
std::shared_ptr< GlobalOptions > options
Definition parser.h:242
stabilizer::parser::Parser::isOne
bool isOne(std::shared_ptr< DAGNode > expr)
Check if an expression is one.
Definition base_parser.cpp:317
stabilizer::parser::Parser::rewrite
std::shared_ptr< DAGNode > rewrite(NODE_KIND &t, std::shared_ptr< DAGNode > &p)
Rewrite unary operation node when simplification rule applies.
Definition rewrite_parser.cpp:39
stabilizer::parser::Parser::mkFalse
std::shared_ptr< DAGNode > mkFalse()
Create a false node.
Definition op_parser.cpp:79
stabilizer::parser::Parser::mkBvZeroExt
std::shared_ptr< DAGNode > mkBvZeroExt(std::shared_ptr< DAGNode > l, std::shared_ptr< DAGNode > r)
Create a bitvector zero extension node.
Definition op_parser.cpp:2300
stabilizer::parser::Parser::toInt
Integer toInt(std::shared_ptr< DAGNode > expr)
Convert an expression to an integer.
Definition base_parser.cpp:300
stabilizer::parser::Parser::mkTrue
std::shared_ptr< DAGNode > mkTrue()
Create a true node.
Definition op_parser.cpp:78
stabilizer::parser::Parser::getEvaluateUseFloating
bool getEvaluateUseFloating() const
Get the use floating for evaluation.
Definition base_parser.cpp:287
stabilizer::parser::Parser::mkBvNot
std::shared_ptr< DAGNode > mkBvNot(std::shared_ptr< DAGNode > param)
Create a bitvector not node.
Definition op_parser.cpp:1925
stabilizer::parser::Parser::mkConstBv
std::shared_ptr< DAGNode > mkConstBv(const std::string &v, const size_t &width)
Create a bit-vector constant.
Definition op_parser.cpp:727
stabilizer::parser::Parser::mkBvNeg
std::shared_ptr< DAGNode > mkBvNeg(std::shared_ptr< DAGNode > param)
Create a bitvector negation node.
Definition op_parser.cpp:2066
stabilizer::parser::Parser::mkConstReal
std::shared_ptr< DAGNode > mkConstReal(const std::string &v)
Create a real constant from string.
Definition op_parser.cpp:689
stabilizer::parser::Parser::mkConstInt
std::shared_ptr< DAGNode > mkConstInt(const std::string &v)
Create an integer constant from string.
Definition op_parser.cpp:680
stabilizer::parser::Parser::isZero
bool isZero(std::shared_ptr< DAGNode > expr)
Check if an expression is zero.
Definition base_parser.cpp:306
stabilizer::parser::Parser::rewrite_oper
std::shared_ptr< DAGNode > rewrite_oper(NODE_KIND &t, std::vector< std::shared_ptr< DAGNode > > &p)
Core operation rewrite helper used before node-manager creation.
Definition rewrite_parser.cpp:1865
stabilizer::parser::Parser::toReal
Real toReal(std::shared_ptr< DAGNode > expr)
Convert an expression to a real.
Definition base_parser.cpp:290
stabilizer::parser::Parser::mkEq
std::shared_ptr< DAGNode > mkEq(const std::vector< std::shared_ptr< DAGNode > > &params)
Create an equality node.
Definition op_parser.cpp:513
stabilizer::parser::Parser::getArity
int getArity(NODE_KIND k) const
Get the arity of a node kind.
Definition op_parser.cpp:4043
stabilizer::parser::Parser::mkConstStr
std::shared_ptr< DAGNode > mkConstStr(const std::string &v)
Create a string constant.
Definition op_parser.cpp:713
stabilizer::parser::Parser::isOnes
bool isOnes(std::shared_ptr< DAGNode > expr)
Definition base_parser.cpp:328
stabilizer::parser::StringUtils::strToUpper
static std::string strToUpper(const std::string &s)
Definition util.cpp:1094
stabilizer::parser::StringUtils::strUnquate
static std::string strUnquate(const std::string &s)
Definition util.h:164
stabilizer::parser::StringUtils::strCharAt
static std::string strCharAt(const std::string &s, const Integer &i)
Definition util.cpp:1024
stabilizer::parser::StringUtils::strSuffixof
static bool strSuffixof(const std::string &s, const std::string &t)
Definition util.cpp:984
stabilizer::parser::StringUtils::strReplaceAll
static std::string strReplaceAll(const std::string &s, const std::string &t, const std::string &u)
Definition util.cpp:1062
stabilizer::parser::StringUtils::strIndexof
static Integer strIndexof(const std::string &s, const std::string &t, const Integer &i)
Definition util.cpp:1007
stabilizer::parser::StringUtils::strSubstr
static std::string strSubstr(const std::string &s, const Integer &i, const Integer &j)
Definition util.cpp:950
stabilizer::parser::StringUtils::strReplace
static std::string strReplace(const std::string &s, const std::string &t, const std::string &u)
Definition util.cpp:1042
stabilizer::parser::StringUtils::strContains
static bool strContains(const std::string &s, const std::string &t)
Definition util.cpp:998
stabilizer::parser::StringUtils::strToLower
static std::string strToLower(const std::string &s)
Definition util.cpp:1085
stabilizer::parser::StringUtils::strUpdate
static std::string strUpdate(const std::string &s, const Integer &i, const std::string &t)
Definition util.cpp:1030
stabilizer::parser::StringUtils::strPrefixof
static bool strPrefixof(const std::string &s, const std::string &t)
Definition util.cpp:971
stabilizer::parser::StringUtils::strRev
static std::string strRev(const std::string &s)
Definition util.cpp:1103
stabilizer::parser::TypeChecker::isInt
static bool isInt(const std::string &str)
Definition util.cpp:47
stabilizer::parser::kindToString
std::string kindToString(const NODE_KIND &nk)
Definition kind.cpp:35
stabilizer::parser::Integer
HighPrecisionInteger Integer
Definition number.h:136
stabilizer::parser::echo_error
void echo_error(const std::string &msg)
Definition rewrite_parser.cpp:35