jurajsic
commented
6 months ago After reenabling the rule a in (str.to_re a') -> (a = a'):
# of formulae: 103318
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
----------------------------------------------- ------ ----- --------- ----- ----- ----- ----- ------- --------- ----- -------- -------
z3-noodler-e58cb97-d95fe13 102120 1198 13149.57 0.13 0.01 1.55 62768 39352 636 509 53 0
z3-noodler-605ccd5-d95fe13 101976 1342 15990.37 0.16 0.01 1.75 62637 39339 638 658 46 0
cvc5-1.1.2 99699 3619 76478.24 0.77 0.00 6.77 60798 38901 2 3608 9 0
z3-4.13.0 97687 5631 132036.99 1.35 0.01 8.11 58874 38813 210 4960 461 0
ostrich-5dd2e10ca 86344 16986 782639.00 9.06 1.75 19.20 47556 38788 0 16962 12 12
z3-4.13.0+cvc5-1.1.2 100756 2562 60604.78 0.60 0.00 6.00 61099 39657 2562 0 0 0
z3-noodler-e58cb97-d95fe13+cvc5-1.1.2 103176 142 9532.31 0.09 0.00 1.43 63261 39915 142 0 0 0
z3-noodler-e58cb97-d95fe13+z3-4.13.0 102785 533 10145.54 0.10 0.01 1.10 62956 39829 533 0 0 0
z3-noodler-e58cb97-d95fe13+z3-4.13.0+cvc5-1.1.2 103190 128 8963.63 0.09 0.00 1.46 63270 39920 128 0 0 0
--------------------------------------------------Interesting benchmarks:
Benchmark automatark
# of formulae: 15995
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
----------------------------------------------- ----- ---- -------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-e58cb97-d95fe13 15970 25 904.53 0.06 0.01 0.67 10466 5504 0 25 0 0
z3-noodler-605ccd5-d95fe13 15963 32 1014.05 0.06 0.01 0.67 10463 5500 0 32 0 0
cvc5-1.1.2 15902 93 2216.97 0.14 0.00 2.83 10460 5442 0 85 8 0
z3-4.13.0 15870 125 6425.06 0.40 0.02 3.90 10469 5401 0 124 1 0
ostrich-5dd2e10ca 15947 48 24332.97 1.53 1.41 1.89 10440 5507 0 48 0 0
z3-4.13.0+cvc5-1.1.2 15969 26 543.82 0.03 0.00 1.22 10481 5488 26 0 0 0
z3-noodler-e58cb97-d95fe13+cvc5-1.1.2 15991 4 177.80 0.01 0.00 0.27 10478 5513 4 0 0 0
z3-noodler-e58cb97-d95fe13+z3-4.13.0 15995 0 389.91 0.02 0.01 0.36 10481 5514 0 0 0 0
z3-noodler-e58cb97-d95fe13+z3-4.13.0+cvc5-1.1.2 15995 0 100.21 0.01 0.00 0.16 10481 5514 0 0 0 0
--------------------------------------------------
Benchmark slent
# of formulae: 1128
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
----------------------------------------------- ---- ---- ------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-e58cb97-d95fe13 1124 4 236.71 0.21 0.01 3.16 626 498 0 4 0 0
z3-noodler-605ccd5-d95fe13 1125 3 25.59 0.02 0.01 0.11 629 496 1 2 0 0
cvc5-1.1.2 1104 24 1079.50 0.98 0.00 6.51 618 486 0 24 0 0
z3-4.13.0 1055 73 385.56 0.37 0.01 4.01 571 484 0 73 0 0
ostrich-5dd2e10ca 1002 126 5154.54 5.14 2.00 13.05 592 410 0 126 0 0
z3-4.13.0+cvc5-1.1.2 1112 16 1044.79 0.94 0.00 6.35 620 492 16 0 0 0
z3-noodler-e58cb97-d95fe13+cvc5-1.1.2 1128 0 10.29 0.01 0.00 0.08 630 498 0 0 0 0
z3-noodler-e58cb97-d95fe13+z3-4.13.0 1128 0 28.62 0.03 0.01 0.39 630 498 0 0 0 0
z3-noodler-e58cb97-d95fe13+z3-4.13.0+cvc5-1.1.2 1128 0 7.56 0.01 0.00 0.05 630 498 0 0 0 0
--------------------------------------------------
Benchmark webapp
# of formulae: 681
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
----------------------------------------------- ---- ---- ------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-e58cb97-d95fe13 361 320 14.47 0.04 0.02 0.09 133 228 316 2 2 0
z3-noodler-605ccd5-d95fe13 355 326 66.63 0.19 0.02 1.99 130 225 316 6 4 0
cvc5-1.1.2 588 93 864.69 1.47 0.01 9.96 165 423 0 93 0 0
z3-4.13.0 450 231 312.63 0.69 0.02 6.78 36 414 120 111 0 0
ostrich-5dd2e10ca 539 142 6434.26 11.94 4.14 24.06 125 414 0 142 0 0
z3-4.13.0+cvc5-1.1.2 590 91 861.65 1.46 0.01 9.95 167 423 91 0 0 0
z3-noodler-e58cb97-d95fe13+cvc5-1.1.2 633 48 444.93 0.70 0.01 6.96 210 423 48 0 0 0
z3-noodler-e58cb97-d95fe13+z3-4.13.0 551 130 70.95 0.13 0.02 2.30 134 417 130 0 0 0
z3-noodler-e58cb97-d95fe13+z3-4.13.0+cvc5-1.1.2 633 48 443.27 0.70 0.01 6.96 210 423 48 0 0 0
--------------------------------------------------
Benchmark kaluza
# of formulae: 19432
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
----------------------------------------------- ----- ---- -------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-e58cb97-d95fe13 19209 223 940.47 0.05 0.01 1.58 16111 3098 0 209 14 0
z3-noodler-605ccd5-d95fe13 19106 326 1063.84 0.06 0.01 1.38 15999 3107 0 320 6 0
cvc5-1.1.2 19431 1 1061.97 0.05 0.00 1.87 16302 3129 0 1 0 0
z3-4.13.0 19148 284 2019.12 0.11 0.01 2.02 16032 3116 0 284 0 0
ostrich-5dd2e10ca 19144 290 37052.30 1.94 1.39 3.45 16015 3129 0 286 2 2
z3-4.13.0+cvc5-1.1.2 19431 1 911.09 0.05 0.00 1.82 16302 3129 1 0 0 0
z3-noodler-e58cb97-d95fe13+cvc5-1.1.2 19431 1 1045.84 0.05 0.00 1.87 16302 3129 1 0 0 0
z3-noodler-e58cb97-d95fe13+z3-4.13.0 19266 166 484.52 0.03 0.01 0.47 16144 3122 166 0 0 0
z3-noodler-e58cb97-d95fe13+z3-4.13.0+cvc5-1.1.2 19431 1 899.28 0.05 0.00 1.82 16302 3129 1 0 0 0
--------------------------------------------------
Benchmark redos
# of formulae: 3287
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
----------------------------------------------- ---- ---- -------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-e58cb97-d95fe13 3284 3 2490.22 0.76 0.03 3.61 2444 840 0 3 0 0
z3-noodler-605ccd5-d95fe13 3256 31 5271.29 1.62 0.91 6.17 2428 828 0 31 0 0
cvc5-1.1.2 1070 2217 27894.06 26.07 0.03 38.26 574 496 0 2217 0 0
z3-4.13.0 888 2399 326.46 0.37 0.01 2.85 48 840 0 2099 300 0
ostrich-5dd2e10ca 1715 1572 55284.56 32.24 33.17 36.98 1053 662 0 1572 0 0
z3-4.13.0+cvc5-1.1.2 1414 1873 27009.57 19.10 0.02 34.70 574 840 1873 0 0 0
z3-noodler-e58cb97-d95fe13+cvc5-1.1.2 3284 3 2349.02 0.72 0.02 3.60 2444 840 3 0 0 0
z3-noodler-e58cb97-d95fe13+z3-4.13.0 3284 3 2221.45 0.68 0.02 3.60 2444 840 3 0 0 0
z3-noodler-e58cb97-d95fe13+z3-4.13.0+cvc5-1.1.2 3284 3 2217.38 0.68 0.02 3.60 2444 840 3 0 0 0
--------------------------------------------------We improved on automatark, redos, kaluza, and webapp (but the last one is probably some randomness), while there is slight degradation on few (4 or so) formulae from slent (which might be the reason this rule was turned off in #39.
This PR reenables the rewriter rule
(str.in A (str.to_re B))->(A = B)which was turned off in #39 (probably because ofslent) and partly reenabled in #126.