Always rewrite boolean ITEs with constant then/else-branches (#4619)
Also adds better tracing and rewrites for binary AND/OR to account for reductions from constant ITEs.
An evaluation of master vs this commit, with 600s, no options, shows the impact of this commit to be negligible and mostly restricted to QF_LIA. Below there is a summary and a list of the unique solves.
```
Benchmark | Stat Slvd Tot To Mo Err Cpu[s] Mem[MB] Uniq | Stat Slvd Tot To Mo Err Cpu[s] Mem[MB] Uniq |
QF_ALIA | ok 125 126 1 0 0 2382.6 5410.8 0 | ok 125 126 1 0 0 2322.1 5211.8 0 |
QF_AX | ok 549 551 2 0 0 2381.4 2533.1 0 | ok 549 551 2 0 0 2400.8 2676.4 0 |
QF_IDL | ok 1682 2193 511 0 0 399395.4 491490.3 3 | ok 1682 2193 511 0 0 400813.9 491129.9 3 |
QF_LIA | ok 4419 6947 2521 7 0
1774140.9
2782838.1 27 | ok 4409 6947 2531 7 0
1775886.7
2785165.7 17 |
QF_LIRA | ok 5 7 2 0 0 1209.9 3626.9 0 | ok 5 7 2 0 0 1209.5 3707.2 0 |
QF_LRA | ok 1517 1648 131 0 0 134215.1 170443.1 3 | ok 1516 1648 132 0 0 134819.6 169942.7 2 |
QF_RDL | ok 210 255 45 0 0 32896.0 23261.0 0 | ok 210 255 45 0 0 32902.7 23312.5 0 |
QF_UF | ok 7444 7457 13 0 0 16156.4 74432.9 0 | ok 7444 7457 13 0 0 16043.8 75067.6 0 |
__totals | ok 15951 19184 3226 7 0
2362777.7
3554036.2 33 | ok 15940 19184 3237 7 0
2366399.2
3556213.8 22 |```
```
DIRECTORY | master | branch |
Benchmark | Stat RES Exit Cpu[s] Mem[MB] | Stat RES Exit Cpu[s] Mem[MB] |
non_incremental_QF_IDL/asp-GraphPartitioning-rand_21_150_1235870252_0_k=3_v=10_e=20_unsat.gph.smt2 | to - 2 600.1 246.4 | ok 20 0 596.71 245.9 |
non_incremental_QF_IDL/asp-SchurNumbers-15.13.schur.lp.smt2 | ok 10 0 533.64 243.8 | to - 2 600.07 246.8 |
non_incremental_QF_IDL/job_shop-jobshop38-2-19-19-4-4-12.smt2 | ok 10 0 586.13 221.5 | to - 2 600.09 216.8 |
non_incremental_QF_IDL/queens_bench-n_queen-queen82-1.smt2 | to - 2 600.01 197.8 | ok 10 0 570.36 198.9 |
non_incremental_QF_IDL/schedulingIDL-tai_15x15_3_mkspan871.smt2 | to - 2 600.1 128.0 | ok 10 0 586.8 127.8 |
non_incremental_QF_IDL/schedulingIDL-tai_15x15_9_mkspan930.smt2 | ok 10 0 575.55 124.4 | to - 2 600.07 122.6 |
non_incremental_QF_LIA/arctic-matrix-constraint-
1007795.smt2 | ok 10 0 334.96 386.7 | to - 2 600.02 335.5 |
non_incremental_QF_LIA/arctic-matrix-constraint-
1008025.smt2 | ok 10 0 180.57 384.6 | to - 2 600.02 338.6 |
non_incremental_QF_LIA/arctic-matrix-constraint-
1107622.smt2 | ok 10 0 310.68 349.2 | to - 2 600.01 341.3 |
non_incremental_QF_LIA/arctic-matrix-constraint-
1275621.smt2 | ok 10 0 5.59 232.0 | to - 2 600.04 407.4 |
non_incremental_QF_LIA/arctic-matrix-constraint-
1360077.smt2 | ok 10 0 422.4 667.7 | to - 11 591.94 663.2 |
non_incremental_QF_LIA/arctic-matrix-constraint-
1765766.smt2 | to - 11 598.02 656.8 | ok 10 0 62.5 669.8 |
non_incremental_QF_LIA/arctic-matrix-constraint-391798.smt2 | ok 10 0 9.0 119.3 | to - 2 600.08 131.8 |
non_incremental_QF_LIA/arctic-matrix-constraint-481231.smt2 | ok 10 0 402.37 220.9 | to - 2 600.09 199.6 |
non_incremental_QF_LIA/arctic-matrix-constraint-689472.smt2 | ok 10 0 28.51 155.9 | to - 2 600.06 215.1 |
non_incremental_QF_LIA/arctic-matrix-constraint-864173.smt2 | ok 10 0 125.59 326.3 | to - 11 597.87 348.8 |
non_incremental_QF_LIA/arctic-matrix-constraint-901628.smt2 | to - 2 600.04 225.5 | ok 10 0 391.31 228.3 |
non_incremental_QF_LIA/arctic-matrix-constraint-916576.smt2 | to - 2 600.01 244.4 | ok 10 0 432.4 246.9 |
non_incremental_QF_LIA/arctic-matrix-constraint-928134.smt2 | ok 10 0 447.55 222.7 | to - 2 600.06 264.7 |
non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-27-42.smt2 | ok 10 0 579.39 414.9 | to - 2 600.07 417.4 |
non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-27-47.smt2 | to - 2 600.02 604.2 | ok 10 0 594.54 603.6 |
non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-45-43.smt2 | to - 2 600.05 628.1 | ok 10 0 588.25 627.6 |
non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-46-47.smt2 | ok 10 0 589.88 570.0 | to - 2 600.09 566.9 |
non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-54-47.smt2 | ok 20 0 590.89 599.9 | to - 2 600.01 598.4 |
non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-54-50.smt2 | ok 10 0 594.72 804.7 | to - 11 593.13 843.5 |
non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-17-47.smt2 | ok 20 0 593.29 524.2 | to - 2 600.08 522.8 |
non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-20-48.smt2 | to - 2 600.02 562.5 | ok 10 0 594.33 560.3 |
non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-5-46.smt2 | to - 2 600.09 492.9 | ok 10 0 576.02 491.9 |
non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-52-47.smt2 | to - 2 600.02 532.2 | ok 20 0 592.3 533.4 |
non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-53-48.smt2 | ok 20 0 599.82 729.4 | to - 2 600.02 742.1 |
non_incremental_QF_LIA/nec-smt-large-getoption_user-prp-41-47.smt2 | to - 11 589.46 1377.2 | ok 20 0 580.82 1380.1 |
non_incremental_QF_LIA/nec-smt-large-user_is_in_group-prp-23-46.smt2 | to - 2 600.08 633.5 | ok 10 0 576.07 634.0 |
non_incremental_QF_LIA/tropical-matrix-constraint-
1015084.smt2 | ok 10 0 408.08 374.5 | to - 2 600.01 336.4 |
non_incremental_QF_LIA/tropical-matrix-constraint-
1206577.smt2 | ok 10 0 361.82 375.4 | to - 11 593.45 288.4 |
non_incremental_QF_LIA/tropical-matrix-constraint-
1268455.smt2 | ok 10 0 270.87 654.3 | to - 2 600.08 670.5 |
non_incremental_QF_LIA/tropical-matrix-constraint-
1270163.smt2 | to - 2 600.02 410.4 | ok 10 0 425.02 420.6 |
non_incremental_QF_LIA/tropical-matrix-constraint-
1270998.smt2 | ok 10 0 349.91 384.6 | to - 2 600.01 417.5 |
non_incremental_QF_LIA/tropical-matrix-constraint-
1290859.smt2 | to - 2 600.1 365.9 | ok 10 0 117.77 270.0 |
non_incremental_QF_LIA/tropical-matrix-constraint-
1361831.smt2 | to - 2 600.07 431.0 | ok 10 0 421.55 686.9 |
non_incremental_QF_LIA/tropical-matrix-constraint-
1452366.smt2 | to - 2 600.04 439.4 | ok 10 0 87.42 451.9 |
non_incremental_QF_LIA/tropical-matrix-constraint-
1791895.smt2 | to - 2 600.1 480.3 | ok 10 0 102.16 459.7 |
non_incremental_QF_LIA/tropical-matrix-constraint-
1908553.smt2 | to - 2 600.01 713.8 | ok 10 0 22.22 394.9 |
non_incremental_QF_LIA/tropical-matrix-constraint-
2061672.smt2 | ok 10 0 51.6 521.2 | to - 2 600.04 545.8 |
non_incremental_QF_LIA/tropical-matrix-constraint-244431.smt2 | ok 10 0 292.95 88.2 | to - 2 600.01 97.7 |
non_incremental_QF_LIA/tropical-matrix-constraint-368069.smt2 | to - 2 600.05 135.3 | ok 10 0 445.93 134.2 |
non_incremental_QF_LIA/tropical-matrix-constraint-369883.smt2 | ok 10 0 510.59 134.2 | to - 2 600.01 127.7 |
non_incremental_QF_LIA/tropical-matrix-constraint-527358.smt2 | ok 10 0 243.33 135.0 | to - 2 600.05 140.7 |
non_incremental_QF_LIA/tropical-matrix-constraint-614657.smt2 | ok 10 0 515.89 209.6 | to - 2 600.07 166.6 |
non_incremental_QF_LIA/tropical-matrix-constraint-645054.smt2 | ok 10 0 41.34 185.3 | to - 2 600.08 205.1 |
non_incremental_QF_LIA/tropical-matrix-constraint-794687.smt2 | ok 10 0 502.03 235.3 | to - 2 600.07 242.0 |
non_incremental_QF_LRA/LassoRanker-CooperatingT2-sas2.t2.c_Iteration7_Loop_7-phaseTemplate.smt2 | ok 20 0 593.7 591.3 | to - 2 600.03 614.7 |
non_incremental_QF_LRA/LassoRanker-SV-COMP-aviad_true-termination.c_Iteration1_Loop_4-phaseTemplate.smt2 | ok 10 0 594.16 738.5 | to - 2 600.03 701.6 |
non_incremental_QF_LRA/LassoRanker-Ultimate-Collatz.bpl_Iteration1_Loop_2-pieceTemplate.smt2 | to - 2 600.09 711.5 | ok 20 0 593.46 711.2 |
non_incremental_QF_LRA/tropical-matrix-constraint-199552.smt2 | ok 10 0 268.04 71.2 | to - 2 600.05 81.6 |
non_incremental_QF_LRA/tropical-matrix-constraint-223827.smt2 | to - 2 600.06 91.9 | ok 10 0 505.07 95.9 |```
projects / cvc5.git / commit