search

VeriFIT / z3-noodler

The Z3-Noodler String Solver
Other
6 stars 5 forks source link

Bug fixing: length unsat formula in preprocessing #153

Closed vhavlena closed 2 months ago

vhavlena commented 3 months ago

This PR fixes bug in preprocessing. The preprocessing rule skip_len_sat requires to be the initial formula length satisfiable. Therefore, I moved the initial length check before the preprocessing itself to ensure that the formula meets the preprocessing requirements.

vhavlena commented 3 months ago

The results seem ok:

# of formulae: 103318
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-ad39615-d95fe13  102228  1090   12781.90   0.13   0.02   1.69  62798    39430        625   406        59        0
z3-noodler-69644b5-d95fe13  102231  1087   11660.24   0.11   0.01   1.57  62805    39426        625   411        51        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
--------------------------------------------------

image

jurajsic commented 2 months ago

I think we can merge this. I would run the experiments again after merging, because #152 is not merged here.

vhavlena commented 2 months ago

I am reverting the last commit, as it unexpectedly caused some performance degradation (not sure why and there is no manpower to find it out).