jurajsic
commented
1 week ago # of formulae: 103405
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
-------------------------------- ------ ---- --------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-5249443-17ffaf6 102431 974 12179.01 0.12 0.02 1.67 62942 39489 530 380 64 0
z3-noodler-1cae537-17ffaf6 102432 973 12422.91 0.12 0.02 1.74 62943 39489 530 379 64 0
z3-noodler-model-5249443-17ffaf6 102431 974 14202.24 0.14 0.02 1.93 62942 39489 534 372 0 68
z3-noodler-model-1cae537-17ffaf6 102423 982 14331.05 0.14 0.02 1.97 62934 39489 534 372 0 76
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-5249443-17ffaf6 343 0 4.51 0.01 0.01 0.01 343 0 0 0 0 0
z3-noodler-1cae537-17ffaf6 343 0 4.62 0.01 0.01 0.01 343 0 0 0 0 0
z3-noodler-model-5249443-17ffaf6 343 0 6.24 0.02 0.02 0.01 343 0 0 0 0 0
z3-noodler-model-1cae537-17ffaf6 343 0 5.97 0.02 0.02 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-5249443-17ffaf6 999 0 42.19 0.04 0.02 0.57 186 813 0 0 0 0
z3-noodler-1cae537-17ffaf6 999 0 43.22 0.04 0.02 0.64 186 813 0 0 0 0
z3-noodler-model-5249443-17ffaf6 999 0 48.62 0.05 0.02 0.58 186 813 0 0 0 0
z3-noodler-model-1cae537-17ffaf6 999 0 48.03 0.05 0.02 0.60 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-5249443-17ffaf6 15990 5 735.09 0.05 0.01 0.50 10477 5513 0 5 0 0
z3-noodler-1cae537-17ffaf6 15990 5 747.84 0.05 0.01 0.53 10477 5513 0 5 0 0
z3-noodler-model-5249443-17ffaf6 15990 5 884.39 0.06 0.02 0.54 10477 5513 0 5 0 0
z3-noodler-model-1cae537-17ffaf6 15990 5 881.35 0.06 0.02 0.53 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-5249443-17ffaf6 11616 2 323.67 0.03 0.01 0.19 6354 5262 1 1 0 0
z3-noodler-1cae537-17ffaf6 11616 2 322.55 0.03 0.01 0.20 6354 5262 1 1 0 0
z3-noodler-model-5249443-17ffaf6 11616 2 493.93 0.04 0.02 0.83 6354 5262 1 1 0 0
z3-noodler-model-1cae537-17ffaf6 11616 2 494.65 0.04 0.02 0.84 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-5249443-17ffaf6 3285 2 2625.12 0.80 0.03 3.76 2445 840 0 2 0 0
z3-noodler-1cae537-17ffaf6 3285 2 2633.81 0.80 0.03 3.77 2445 840 0 2 0 0
z3-noodler-model-5249443-17ffaf6 3285 2 2689.12 0.82 0.04 3.78 2445 840 0 2 0 0
z3-noodler-model-1cae537-17ffaf6 3285 2 2701.03 0.82 0.04 3.78 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-5249443-17ffaf6 1027 0 14.51 0.01 0.01 0.01 712 315 0 0 0 0
z3-noodler-1cae537-17ffaf6 1027 0 14.38 0.01 0.01 0.01 712 315 0 0 0 0
z3-noodler-model-5249443-17ffaf6 1027 0 20.00 0.02 0.02 0.01 712 315 0 0 0 0
z3-noodler-model-1cae537-17ffaf6 1027 0 20.10 0.02 0.02 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-5249443-17ffaf6 1976 0 27.92 0.01 0.01 0.02 808 1168 0 0 0 0
z3-noodler-1cae537-17ffaf6 1976 0 27.56 0.01 0.01 0.02 808 1168 0 0 0 0
z3-noodler-model-5249443-17ffaf6 1976 0 38.13 0.02 0.02 0.03 808 1168 0 0 0 0
z3-noodler-model-1cae537-17ffaf6 1976 0 37.86 0.02 0.02 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-5249443-17ffaf6 1125 3 240.94 0.21 0.01 2.97 627 498 0 3 0 0
z3-noodler-1cae537-17ffaf6 1125 3 244.15 0.22 0.01 2.99 627 498 0 3 0 0
z3-noodler-model-5249443-17ffaf6 1125 3 212.85 0.19 0.02 2.96 627 498 0 3 0 0
z3-noodler-model-1cae537-17ffaf6 1125 3 214.59 0.19 0.02 2.98 627 498 0 3 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-5249443-17ffaf6 9 8 0.10 0.01 0.01 0.01 2 7 0 6 2 0
z3-noodler-1cae537-17ffaf6 9 8 0.13 0.01 0.01 0.02 2 7 0 6 2 0
z3-noodler-model-5249443-17ffaf6 8 9 0.18 0.02 0.01 0.03 1 7 1 6 0 2
z3-noodler-model-1cae537-17ffaf6 8 9 0.16 0.02 0.01 0.02 1 7 1 6 0 2
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-5249443-17ffaf6 584 3 15.93 0.03 0.01 0.07 284 300 0 3 0 0
z3-noodler-1cae537-17ffaf6 584 3 15.91 0.03 0.01 0.07 284 300 0 3 0 0
z3-noodler-model-5249443-17ffaf6 584 3 62.34 0.11 0.02 0.21 284 300 0 3 0 0
z3-noodler-model-1cae537-17ffaf6 584 3 56.87 0.10 0.02 0.19 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-5249443-17ffaf6 776 33 296.56 0.38 0.01 4.64 614 162 0 14 19 0
z3-noodler-1cae537-17ffaf6 777 32 411.26 0.53 0.01 6.15 615 162 0 13 19 0
z3-noodler-model-5249443-17ffaf6 768 41 114.69 0.15 0.02 1.52 606 162 2 15 0 24
z3-noodler-model-1cae537-17ffaf6 768 41 114.76 0.15 0.02 1.51 606 162 2 15 0 24
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-5249443-17ffaf6 365 316 207.73 0.57 0.02 4.97 137 228 315 0 1 0
z3-noodler-1cae537-17ffaf6 365 316 221.00 0.61 0.02 5.33 137 228 315 0 1 0
z3-noodler-model-5249443-17ffaf6 364 317 236.37 0.65 0.03 5.26 136 228 316 0 0 1
z3-noodler-model-1cae537-17ffaf6 364 317 252.97 0.69 0.03 5.70 136 228 316 0 0 1
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-5249443-17ffaf6 19233 199 1550.75 0.08 0.01 2.32 16136 3097 0 185 14 0
z3-noodler-1cae537-17ffaf6 19233 199 1590.31 0.08 0.01 2.39 16136 3097 0 185 14 0
z3-noodler-model-5249443-17ffaf6 19244 188 2473.74 0.13 0.02 3.18 16147 3097 0 173 0 15
z3-noodler-model-1cae537-17ffaf6 19244 188 2536.74 0.13 0.02 3.28 16147 3097 0 173 0 15
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-5249443-17ffaf6 0 91 0.00 nan nan nan 0 0 91 0 0 0
z3-noodler-1cae537-17ffaf6 0 91 0.00 nan nan nan 0 0 91 0 0 0
z3-noodler-model-5249443-17ffaf6 0 91 0.00 nan nan nan 0 0 91 0 0 0
z3-noodler-model-1cae537-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-5249443-17ffaf6 2649 3 51.61 0.02 0.01 0.05 865 1784 0 0 3 0
z3-noodler-1cae537-17ffaf6 2649 3 52.31 0.02 0.01 0.06 865 1784 0 0 3 0
z3-noodler-model-5249443-17ffaf6 2650 2 89.47 0.03 0.02 0.38 866 1784 0 0 0 2
z3-noodler-model-1cae537-17ffaf6 2642 10 88.74 0.03 0.02 0.38 858 1784 0 0 0 10
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-5249443-17ffaf6 1814 66 393.52 0.22 0.01 3.07 4 1810 6 35 25 0
z3-noodler-1cae537-17ffaf6 1814 66 400.52 0.22 0.01 3.15 4 1810 6 35 25 0
z3-noodler-model-5249443-17ffaf6 1814 66 415.61 0.23 0.02 3.22 4 1810 6 37 0 23
z3-noodler-model-1cae537-17ffaf6 1814 66 416.73 0.23 0.02 3.17 4 1810 6 37 0 23
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-5249443-17ffaf6 23754 91 4282.66 0.18 0.10 1.23 20383 3371 0 91 0 0
z3-noodler-1cae537-17ffaf6 23754 91 4317.89 0.18 0.10 1.26 20383 3371 0 91 0 0
z3-noodler-model-5249443-17ffaf6 23752 93 4903.95 0.21 0.12 1.40 20381 3371 0 93 0 0
z3-noodler-model-1cae537-17ffaf6 23752 93 4941.75 0.21 0.12 1.44 20381 3371 0 93 0 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-5249443-17ffaf6 16816 152 1365.43 0.08 0.01 1.54 2495 14321 117 35 0 0
z3-noodler-1cae537-17ffaf6 16816 152 1374.70 0.08 0.01 1.56 2495 14321 117 35 0 0
z3-noodler-model-5249443-17ffaf6 16816 152 1511.30 0.09 0.02 1.51 2495 14321 117 34 0 1
z3-noodler-model-1cae537-17ffaf6 16816 152 1517.56 0.09 0.02 1.52 2495 14321 117 34 0 1
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-5249443-17ffaf6 70 0 0.77 0.01 0.01 0.01 70 0 0 0 0 0
z3-noodler-1cae537-17ffaf6 70 0 0.75 0.01 0.01 0.00 70 0 0 0 0 0
z3-noodler-model-5249443-17ffaf6 70 0 1.31 0.02 0.02 0.01 70 0 0 0 0 0
z3-noodler-model-1cae537-17ffaf6 70 0 1.19 0.02 0.02 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
--------------------------------------------------
During model generation, we add the arguments of concatenation as its dependencies to create the model of the concatenation. However, sometimes (in
Leetcode, for example forQF_SLIA/2019-Leetcode/findLadders/40e8819fff4fee9d50e90f6b69865ac6e7c40c0699830176df703c6e.smt2) it could happen that one of its argument belonged to the same equivalence class as the concatenation, which resulted in problems during dependency evaluation. I think the problem is that the equivalence class contains a literal, but it is not the representative. This PR adds a check, which looks at all enodes belonging to the same equivalence class as concatenation, and if one of them is literal, immediately returns this literal as a model instead of adding dependencies.