Closed jurajsic closed 4 months ago
On automatark
:
Benchmark automatark
# of formulae: 15995
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
----------------------------------------------- ----- ---- -------- ----- ----- ----- ----- ------- --------- ---- -------- -------
z3-noodler-da892c5-d95fe13 15979 16 553.24 0.03 0.01 0.37 10466 5513 0 16 0 0
z3-noodler-e58cb97-d95fe13 15970 25 904.53 0.06 0.01 0.67 10466 5504 0 25 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-noodler-914a49e-d95fe13 15973 22 790.39 0.05 0.01 0.51 10466 5507 0 22 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-da892c5-d95fe13+cvc5-1.1.2 15992 3 116.10 0.01 0.00 0.16 10478 5514 3 0 0 0
z3-noodler-da892c5-d95fe13+z3-4.13.0 15995 0 296.15 0.02 0.01 0.16 10481 5514 0 0 0 0
z3-noodler-da892c5-d95fe13+z3-4.13.0+cvc5-1.1.2 15995 0 76.14 0.00 0.00 0.04 10481 5514 0 0 0 0
--------------------------------------------------
We can handle all (except one) UNSAT cases, there are still 15 SAT cases for which this heuristic will not help.
Final results:
# of formulae: 103318
--------------------------------------------------
tool ✅ ❌ time avg med std sat unsat unknown TO MO+ERR other
----------------------------------------------- ------ ----- --------- ----- ----- ----- ----- ------- --------- ----- -------- -------
z3-noodler-7380a2a-d95fe13 102134 1184 12821.32 0.13 0.01 1.63 62771 39363 636 495 53 0
z3-noodler-e58cb97-d95fe13 102120 1198 13149.57 0.13 0.01 1.55 62768 39352 636 509 53 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 16974 782639.00 9.06 1.75 19.20 47556 38788 0 16962 0 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-7380a2a-d95fe13+cvc5-1.1.2 103177 141 9307.48 0.09 0.00 1.42 63261 39916 141 0 0 0
z3-noodler-7380a2a-d95fe13+z3-4.13.0 102785 533 9756.39 0.09 0.01 1.04 62956 39829 533 0 0 0
z3-noodler-7380a2a-d95fe13+z3-4.13.0+cvc5-1.1.2 103190 128 8811.23 0.09 0.00 1.45 63270 39920 128 0 0 0
--------------------------------------------------
No impact on other benchmarks, as expected.
This PR adds heuristic for formulae where we only have regex membership predicates (or formulae that are easily tranformed to this form). For each var
x
, it takes allx in RE
orx not in RE
and sorts the regexes by the sum of loops occurring in the regexes, with the regexes that need to be complemented being at the end. Then it lazily computes the intersection of all these regexes, so that if we get an empty language, we can immediately say UNSAT without continuing building the more complex regexes.