search

VeriFIT / z3-noodler

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

`full_str_int`: performance optimizations #164

Closed vhavlena closed 1 month ago

vhavlena commented 1 month ago

This PR strengthen some axioms to avoid redundant checks.

vhavlena commented 1 month ago

Results:

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-837f212-2756940  102446   959   12073.04   0.12   0.02   1.65  62960    39486        530   355        74        0
z3-noodler-7801978-2756940  102424   981   14358.39   0.14   0.02   1.99  62951    39473        530   378        73        0
cvc5-1.1.2                   99774  3631   76479.19   0.77   0.00   6.77  60870    38904          2  3620         9        0
z3-4.13.0                    97745  5660  128712.47   1.32   0.01   7.95  58927    38818        211  4914       465       70
--------------------------------------------------

Biggest impact on full_str_int:

Benchmark full_str_int
# of formulae: 16968
--------------------------------------------------
tool                           ✅    ❌      time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  --------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-837f212-2756940  16821   147   1440.71   0.09   0.01   1.64   2500    14321        117    29         1        0
z3-noodler-7801978-2756940  16801   167   3801.76   0.23   0.01   3.12   2493    14308        117    50         0        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
--------------------------------------------------

image

jurajsic commented 1 month ago

EDIT: wrong PR, the following is for #160

After the fix:

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-7525ba0-2756940  102442   963   11912.81   0.12   0.02   1.61  62954    39488        530   364        69        0
z3-noodler-837f212-2756940  102446   959   12073.04   0.12   0.02   1.65  62960    39486        530   355        74        0
cvc5-1.1.2                   99774  3631   76479.19   0.77   0.00   6.77  60870    38904          2  3620         9        0
z3-4.13.0                    97745  5660  128712.47   1.32   0.01   7.95  58927    38818        211  4914       465       70
z3-noodler-86a65bd-2756940  102303  1102   19077.34   0.19   0.02   2.32  62822    39481        530   412       160        0
--------------------------------------------------

image

vhavlena commented 1 month ago

Wrong thread? 😄

jurajsic commented 1 month ago

Wrong thread? 😄

Yep :D Should be in #160