jurajsic
commented
2 weeks ago Results (comparing only on benchmarks with conversions, also with model turned on):
# of formulae: 30466
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
--------------------------------- ----- ---- -------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-be33653-9ab1675 30240 226 1559.88 0.05 0.01 0.64 8849 21391 125 90 0 11
z3-noodler-be33653-2756940 30250 216 2283.43 0.08 0.01 1.66 8857 21393 124 66 26 0
z3-noodler-length-ab1b074-2756940 30256 210 2511.72 0.08 0.01 1.87 8863 21393 124 61 25 0
cvc5-1.1.2 29739 727 35755.04 1.20 0.01 7.78 8699 21040 2 724 1 0
z3-4.13.0 29643 823 63461.18 2.14 0.01 10.42 8505 21138 0 698 125 0
--------------------------------------------------
Benchmark stringfuzz
# of formulae: 11618
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
--------------------------------- ----- ---- -------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-be33653-9ab1675 11616 2 362.78 0.03 0.01 0.59 6354 5262 1 1 0 0
z3-noodler-be33653-2756940 11616 2 323.05 0.03 0.01 0.18 6354 5262 1 1 0 0
z3-noodler-length-ab1b074-2756940 11616 2 321.03 0.03 0.01 0.19 6354 5262 1 1 0 0
cvc5-1.1.2 10915 703 30628.85 2.81 0.00 12.55 6158 4757 0 702 1 0
z3-4.13.0 11090 528 44638.05 4.03 0.01 14.89 6004 5086 0 403 125 0
--------------------------------------------------
Benchmark str_small_rw
# of formulae: 1880
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
--------------------------------- ---- ---- ------ ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-be33653-9ab1675 1811 69 211.01 0.12 0.01 1.30 3 1808 7 51 0 11
z3-noodler-be33653-2756940 1814 66 417.22 0.23 0.01 3.20 4 1810 6 34 26 0
z3-noodler-length-ab1b074-2756940 1814 66 384.42 0.21 0.01 2.97 4 1810 6 36 24 0
cvc5-1.1.2 1861 19 31.09 0.02 0.00 0.56 20 1841 2 17 0 0
z3-4.13.0 1821 59 202.53 0.11 0.01 2.66 25 1796 0 59 0 0
--------------------------------------------------
Benchmark full_str_int
# of formulae: 16968
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
--------------------------------- ----- ---- -------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-model-be33653-9ab1675 16813 155 986.09 0.06 0.01 0.57 2492 14321 117 38 0 0
z3-noodler-be33653-2756940 16820 148 1543.16 0.09 0.01 1.95 2499 14321 117 31 0 0
z3-noodler-length-ab1b074-2756940 16826 142 1806.27 0.11 0.01 2.30 2505 14321 117 24 1 0
cvc5-1.1.2 16963 5 5095.10 0.30 0.01 1.42 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
--------------------------------------------------
This PR (probably) fixes #135. There was a problem that conversion could be axiomitized on higher level and after popping, it would not be axiomitized again, as it was saved in
axiomatized_persist_terms.