jurajsic
commented
3 hours ago I am not sure which version is previous, I compare with #176 (0122b33-17ffaf6) and #174 (193f136-17ffaf6):
# of formulae: 103405
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ------ ---- --------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 102444 961 14328.80 0.14 0.02 1.90 62953 39491 530 359 0 72
z3-noodler-cd34a4a-17ffaf6 102442 963 12208.15 0.12 0.02 1.65 62951 39491 528 374 61 0
z3-noodler-193f136-17ffaf6 102442 963 12345.08 0.12 0.02 1.72 62953 39489 530 372 61 0
z3-noodler-model-193f136-17ffaf6 102439 966 14252.71 0.14 0.02 1.95 62950 39489 534 364 0 68
z3-noodler-0122b33-17ffaf6 102443 962 12100.47 0.12 0.02 1.66 62952 39491 528 372 62 0
cvc5-1.2.0 99841 3564 73861.19 0.74 0.01 6.42 60931 38910 2 3553 9 0
z3-4.13.0 97745 5660 128712.47 1.32 0.01 7.95 58927 38818 211 4914 465 70
--------------------------------------------------
Benchmark sygus_qgen
# of formulae: 343
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------ ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 343 0 5.83 0.02 0.02 0.01 343 0 0 0 0 0
z3-noodler-cd34a4a-17ffaf6 343 0 4.45 0.01 0.01 0.01 343 0 0 0 0 0
z3-noodler-193f136-17ffaf6 343 0 4.65 0.01 0.01 0.01 343 0 0 0 0 0
z3-noodler-model-193f136-17ffaf6 343 0 6.39 0.02 0.02 0.01 343 0 0 0 0 0
z3-noodler-0122b33-17ffaf6 343 0 4.46 0.01 0.01 0.01 343 0 0 0 0 0
cvc5-1.2.0 343 0 80.99 0.24 0.04 0.93 343 0 0 0 0 0
z3-4.13.0 343 0 10.35 0.03 0.02 0.02 343 0 0 0 0 0
--------------------------------------------------
Benchmark denghang
# of formulae: 999
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------ ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 999 0 49.08 0.05 0.02 0.59 186 813 0 0 0 0
z3-noodler-cd34a4a-17ffaf6 999 0 41.88 0.04 0.02 0.59 186 813 0 0 0 0
z3-noodler-193f136-17ffaf6 999 0 43.22 0.04 0.02 0.61 186 813 0 0 0 0
z3-noodler-model-193f136-17ffaf6 999 0 48.75 0.05 0.02 0.59 186 813 0 0 0 0
z3-noodler-0122b33-17ffaf6 999 0 42.03 0.04 0.02 0.58 186 813 0 0 0 0
cvc5-1.2.0 982 17 371.55 0.38 0.00 4.64 170 812 0 17 0 0
z3-4.13.0 883 116 326.28 0.37 0.08 2.10 186 697 0 105 11 0
--------------------------------------------------
Benchmark automatark
# of formulae: 15995
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ----- ---- ------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 15990 5 892.63 0.06 0.02 0.54 10477 5513 0 5 0 0
z3-noodler-cd34a4a-17ffaf6 15990 5 733.44 0.05 0.01 0.51 10477 5513 0 5 0 0
z3-noodler-193f136-17ffaf6 15990 5 737.85 0.05 0.01 0.51 10477 5513 0 5 0 0
z3-noodler-model-193f136-17ffaf6 15990 5 894.39 0.06 0.02 0.55 10477 5513 0 5 0 0
z3-noodler-0122b33-17ffaf6 15990 5 741.71 0.05 0.01 0.52 10477 5513 0 5 0 0
cvc5-1.2.0 15903 92 2196.84 0.14 0.00 2.77 10460 5443 0 84 8 0
z3-4.13.0 15871 124 6107.03 0.38 0.02 3.72 10469 5402 0 123 1 0
--------------------------------------------------
Benchmark stringfuzz
# of formulae: 11618
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ----- ---- -------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 11616 2 505.60 0.04 0.02 0.96 6354 5262 1 1 0 0
z3-noodler-cd34a4a-17ffaf6 11616 2 312.34 0.03 0.01 0.17 6354 5262 1 1 0 0
z3-noodler-193f136-17ffaf6 11616 2 323.48 0.03 0.01 0.18 6354 5262 1 1 0 0
z3-noodler-model-193f136-17ffaf6 11616 2 497.35 0.04 0.02 0.91 6354 5262 1 1 0 0
z3-noodler-0122b33-17ffaf6 11616 2 321.25 0.03 0.01 0.18 6354 5262 1 1 0 0
cvc5-1.2.0 10946 672 30049.07 2.75 0.00 12.34 6184 4762 0 671 1 0
z3-4.13.0 11090 528 44638.05 4.03 0.01 14.89 6004 5086 0 403 125 0
--------------------------------------------------
Benchmark redos
# of formulae: 3287
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- -------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 3283 4 2673.46 0.81 0.05 2.85 2443 840 0 4 0 0
z3-noodler-cd34a4a-17ffaf6 3283 4 2548.21 0.78 0.03 2.82 2443 840 0 4 0 0
z3-noodler-193f136-17ffaf6 3285 2 2631.41 0.80 0.03 3.80 2445 840 0 2 0 0
z3-noodler-model-193f136-17ffaf6 3285 2 2709.66 0.82 0.04 3.83 2445 840 0 2 0 0
z3-noodler-0122b33-17ffaf6 3285 2 2620.25 0.80 0.03 3.77 2445 840 0 2 0 0
cvc5-1.2.0 1116 2171 27007.04 24.20 0.14 34.28 620 496 0 2171 0 0
z3-4.13.0 888 2399 297.55 0.34 0.01 2.60 48 840 0 2099 300 0
--------------------------------------------------
Benchmark norn
# of formulae: 1027
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------ ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 1027 0 20.49 0.02 0.02 0.01 712 315 0 0 0 0
z3-noodler-cd34a4a-17ffaf6 1027 0 14.70 0.01 0.01 0.01 712 315 0 0 0 0
z3-noodler-193f136-17ffaf6 1027 0 14.31 0.01 0.01 0.01 712 315 0 0 0 0
z3-noodler-model-193f136-17ffaf6 1027 0 20.04 0.02 0.02 0.01 712 315 0 0 0 0
z3-noodler-0122b33-17ffaf6 1027 0 14.60 0.01 0.01 0.01 712 315 0 0 0 0
cvc5-1.2.0 943 84 247.71 0.26 0.01 2.41 705 238 0 84 0 0
z3-4.13.0 904 123 278.96 0.31 0.02 5.21 712 192 0 123 0 0
--------------------------------------------------
Benchmark slog
# of formulae: 1976
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------ ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 1976 0 37.79 0.02 0.02 0.02 808 1168 0 0 0 0
z3-noodler-cd34a4a-17ffaf6 1976 0 28.59 0.01 0.01 0.02 808 1168 0 0 0 0
z3-noodler-193f136-17ffaf6 1976 0 27.91 0.01 0.01 0.02 808 1168 0 0 0 0
z3-noodler-model-193f136-17ffaf6 1976 0 37.81 0.02 0.02 0.02 808 1168 0 0 0 0
z3-noodler-0122b33-17ffaf6 1976 0 27.83 0.01 0.01 0.02 808 1168 0 0 0 0
cvc5-1.2.0 1976 0 1.85 0.00 0.00 0.00 808 1168 0 0 0 0
z3-4.13.0 1956 20 539.58 0.28 0.01 3.81 788 1168 0 20 0 0
--------------------------------------------------
Benchmark slent
# of formulae: 1128
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 1124 4 220.31 0.20 0.02 3.06 626 498 0 4 0 0
z3-noodler-cd34a4a-17ffaf6 1124 4 243.12 0.22 0.01 2.99 626 498 0 4 0 0
z3-noodler-193f136-17ffaf6 1125 3 242.43 0.22 0.01 2.98 627 498 0 3 0 0
z3-noodler-model-193f136-17ffaf6 1125 3 220.51 0.20 0.02 3.07 627 498 0 3 0 0
z3-noodler-0122b33-17ffaf6 1124 4 239.77 0.21 0.01 2.94 626 498 0 4 0 0
cvc5-1.2.0 1104 24 1002.26 0.91 0.00 6.12 618 486 0 24 0 0
z3-4.13.0 1052 76 345.30 0.33 0.01 4.17 571 481 0 76 0 0
--------------------------------------------------
Benchmark omark
# of formulae: 17
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------ ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 9 8 0.19 0.02 0.01 0.02 2 7 0 6 0 2
z3-noodler-cd34a4a-17ffaf6 9 8 0.12 0.01 0.01 0.01 2 7 0 6 2 0
z3-noodler-193f136-17ffaf6 9 8 0.13 0.01 0.01 0.01 2 7 0 6 2 0
z3-noodler-model-193f136-17ffaf6 8 9 0.20 0.03 0.02 0.03 1 7 1 6 0 2
z3-noodler-0122b33-17ffaf6 9 8 0.11 0.01 0.01 0.01 2 7 0 6 2 0
cvc5-1.2.0 5 12 1.03 0.21 0.00 0.46 2 3 0 12 0 0
z3-4.13.0 7 10 8.06 1.15 0.01 3.01 2 5 0 8 2 0
--------------------------------------------------
Benchmark kepler
# of formulae: 587
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------ ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 584 3 61.33 0.11 0.02 0.21 284 300 0 3 0 0
z3-noodler-cd34a4a-17ffaf6 584 3 16.21 0.03 0.01 0.07 284 300 0 3 0 0
z3-noodler-193f136-17ffaf6 584 3 16.39 0.03 0.01 0.07 284 300 0 3 0 0
z3-noodler-model-193f136-17ffaf6 584 3 62.36 0.11 0.02 0.21 284 300 0 3 0 0
z3-noodler-0122b33-17ffaf6 584 3 15.45 0.03 0.01 0.07 284 300 0 3 0 0
cvc5-1.2.0 347 240 0.86 0.00 0.00 0.00 50 297 0 240 0 0
z3-4.13.0 278 309 25.95 0.09 0.02 0.90 135 143 0 283 26 0
--------------------------------------------------
Benchmark woorpje
# of formulae: 809
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------ ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 769 40 115.50 0.15 0.02 1.50 607 162 1 16 0 23
z3-noodler-cd34a4a-17ffaf6 777 32 415.11 0.53 0.01 6.28 615 162 0 13 19 0
z3-noodler-193f136-17ffaf6 776 33 298.61 0.38 0.01 4.63 614 162 0 14 19 0
z3-noodler-model-193f136-17ffaf6 768 41 114.76 0.15 0.02 1.50 606 162 2 15 0 24
z3-noodler-0122b33-17ffaf6 776 33 295.27 0.38 0.01 4.62 614 162 0 14 19 0
cvc5-1.2.0 755 54 47.07 0.06 0.01 0.25 591 164 0 54 0 0
z3-4.13.0 782 27 295.18 0.38 0.02 4.74 618 164 0 27 0 0
--------------------------------------------------
Benchmark webapp
# of formulae: 681
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------ ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 364 317 244.65 0.67 0.03 5.73 136 228 316 0 0 1
z3-noodler-cd34a4a-17ffaf6 365 316 197.66 0.54 0.02 4.81 137 228 315 0 1 0
z3-noodler-193f136-17ffaf6 365 316 200.77 0.55 0.02 4.79 137 228 315 0 1 0
z3-noodler-model-193f136-17ffaf6 364 317 249.13 0.68 0.03 5.58 136 228 316 0 0 1
z3-noodler-0122b33-17ffaf6 365 316 193.41 0.53 0.02 4.71 137 228 315 0 1 0
cvc5-1.2.0 588 93 767.89 1.31 0.02 8.73 165 423 0 93 0 0
z3-4.13.0 451 230 317.75 0.70 0.02 6.71 37 414 121 109 0 0
--------------------------------------------------
Benchmark kaluza
# of formulae: 19432
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ----- ---- ------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 19254 178 2395.76 0.12 0.02 3.15 16157 3097 0 163 0 15
z3-noodler-cd34a4a-17ffaf6 19245 187 1526.94 0.08 0.01 2.35 16148 3097 0 176 11 0
z3-noodler-193f136-17ffaf6 19245 187 1542.89 0.08 0.01 2.38 16148 3097 0 176 11 0
z3-noodler-model-193f136-17ffaf6 19254 178 2425.80 0.13 0.02 3.21 16157 3097 0 163 0 15
z3-noodler-0122b33-17ffaf6 19245 187 1518.68 0.08 0.01 2.33 16148 3097 0 176 11 0
cvc5-1.2.0 19426 6 459.94 0.02 0.00 0.42 16297 3129 0 6 0 0
z3-4.13.0 19139 293 1428.86 0.07 0.01 1.71 16022 3117 0 293 0 0
--------------------------------------------------
Benchmark transducer_plus
# of formulae: 91
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------ ------ ------ ------ ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 0 91 0.00 nan nan nan 0 0 91 0 0 0
z3-noodler-cd34a4a-17ffaf6 0 91 0.00 nan nan nan 0 0 91 0 0 0
z3-noodler-193f136-17ffaf6 0 91 0.00 nan nan nan 0 0 91 0 0 0
z3-noodler-model-193f136-17ffaf6 0 91 0.00 nan nan nan 0 0 91 0 0 0
z3-noodler-0122b33-17ffaf6 0 91 0.00 nan nan nan 0 0 91 0 0 0
cvc5-1.2.0 42 49 482.14 11.48 3.11 22.06 41 1 0 49 0 0
z3-4.13.0 1 90 0.01 0.01 0.01 nan 0 1 90 0 0 0
--------------------------------------------------
Benchmark leetcode
# of formulae: 2652
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------ ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 2649 3 70.84 0.03 0.02 0.06 865 1784 0 0 0 3
z3-noodler-cd34a4a-17ffaf6 2650 2 53.12 0.02 0.01 0.05 866 1784 0 0 2 0
z3-noodler-193f136-17ffaf6 2649 3 52.13 0.02 0.01 0.06 865 1784 0 0 3 0
z3-noodler-model-193f136-17ffaf6 2650 2 90.61 0.03 0.02 0.38 866 1784 0 0 0 2
z3-noodler-0122b33-17ffaf6 2650 2 52.10 0.02 0.01 0.05 866 1784 0 0 2 0
cvc5-1.2.0 2652 0 36.00 0.01 0.00 0.03 867 1785 0 0 0 0
z3-4.13.0 2652 0 41.89 0.02 0.01 0.11 867 1785 0 0 0 0
--------------------------------------------------
Benchmark str_small_rw
# of formulae: 1880
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------ ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 1815 65 365.25 0.20 0.02 2.97 3 1812 4 36 0 25
z3-noodler-cd34a4a-17ffaf6 1815 65 321.88 0.18 0.01 2.57 3 1812 4 37 24 0
z3-noodler-193f136-17ffaf6 1814 66 402.83 0.22 0.01 3.20 4 1810 6 35 25 0
z3-noodler-model-193f136-17ffaf6 1814 66 412.04 0.23 0.02 3.10 4 1810 6 37 0 23
z3-noodler-0122b33-17ffaf6 1815 65 330.24 0.18 0.01 2.67 3 1812 4 36 25 0
cvc5-1.2.0 1860 20 34.43 0.02 0.00 0.62 19 1841 2 18 0 0
z3-4.13.0 1821 59 202.53 0.11 0.01 2.66 25 1796 0 59 0 0
--------------------------------------------------
Benchmark pyex
# of formulae: 23845
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ----- ---- -------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 23757 88 5108.15 0.22 0.12 1.55 20386 3371 0 86 0 2
z3-noodler-cd34a4a-17ffaf6 23752 93 4341.90 0.18 0.10 1.36 20381 3371 0 91 2 0
z3-noodler-193f136-17ffaf6 23753 92 4432.06 0.19 0.10 1.39 20382 3371 0 92 0 0
z3-noodler-model-193f136-17ffaf6 23750 95 4934.37 0.21 0.12 1.40 20379 3371 0 95 0 0
z3-noodler-0122b33-17ffaf6 23752 93 4288.73 0.18 0.10 1.35 20381 3371 0 91 2 0
cvc5-1.2.0 23820 25 6002.12 0.25 0.07 2.51 20400 3420 0 25 0 0
z3-4.13.0 22895 950 55228.54 2.41 0.12 10.38 19624 3271 0 950 0 0
--------------------------------------------------
Benchmark full_str_int
# of formulae: 16968
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ----- ---- -------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 16815 153 1560.69 0.09 0.02 1.48 2494 14321 117 35 0 1
z3-noodler-cd34a4a-17ffaf6 16817 151 1407.62 0.08 0.01 1.46 2496 14321 117 34 0 0
z3-noodler-193f136-17ffaf6 16816 152 1373.22 0.08 0.01 1.53 2495 14321 117 35 0 0
z3-noodler-model-193f136-17ffaf6 16816 152 1527.30 0.09 0.02 1.52 2495 14321 117 34 0 1
z3-noodler-0122b33-17ffaf6 16817 151 1393.70 0.08 0.01 1.44 2496 14321 117 34 0 0
cvc5-1.2.0 16963 5 5072.37 0.30 0.01 1.39 2521 14442 0 5 0 0
z3-4.13.0 16732 236 18620.60 1.11 0.01 6.38 2476 14256 0 236 0 0
--------------------------------------------------
Benchmark snia
# of formulae: 70
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ---- ---- ------ ------ ------ ------ ----- ------- --------- ---- -------- -------
z3-noodler-model-cd34a4a-17ffaf6 70 0 1.25 0.02 0.02 0.01 70 0 0 0 0 0
z3-noodler-cd34a4a-17ffaf6 70 0 0.86 0.01 0.01 0.01 70 0 0 0 0 0
z3-noodler-193f136-17ffaf6 70 0 0.79 0.01 0.01 0.00 70 0 0 0 0 0
z3-noodler-model-193f136-17ffaf6 70 0 1.24 0.02 0.02 0.01 70 0 0 0 0 0
z3-noodler-0122b33-17ffaf6 70 0 0.88 0.01 0.01 0.01 70 0 0 0 0 0
cvc5-1.2.0 70 0 0.03 0.00 0.00 0.00 70 0 0 0 0 0
z3-4.13.0 0 70 0.00 nan nan nan 0 0 0 0 0 70
--------------------------------------------------
If the language of an automaton for a variable contains only one word, we return it immediately instead of looking trough incusions. This can help for cyclic inclusions, we can now generate model for two of the three mentioned formulas in #179 (it cannot generate model for
QF_SLIA/20230329-woorpje-lu/track05/05_track_169.smt2).