VeriFIT / z3-noodler

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

Fixing infinite looping #140

Closed vhavlena closed 6 months ago

vhavlena commented 6 months ago

This PR introduces small optimizations:

vhavlena commented 6 months ago

Results on all

# of formulae: 103318
--------------------------------------------------
tool                                                 ✅     ❌       time    avg    med    std    sat    unsat    unknown     TO    MO+ERR    other
-----------------------------------------------  ------  -----  ---------  -----  -----  -----  -----  -------  ---------  -----  --------  -------
z3-noodler-82db97c-d95fe13                       102200   1118   12913.53   0.13   0.01   1.64  62783    39417        632    434        52        0
z3-noodler-7380a2a-d95fe13                       102134   1184   12821.32   0.13   0.01   1.63  62771    39363        636    495        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
z3-alpha-4.12.2                                   97446   5872  105306.72   1.08   0.01   7.19  59153    38293        414   2113        58     3287
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
--------------------------------------------------

Interesting benchmarks:

Benchmark str_small_rw
# of formulae: 1880
--------------------------------------------------
tool                                               ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
-----------------------------------------------  ----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-82db97c-d95fe13                       1760   120   392.37   0.22   0.01   3.31      5     1755         96    12        12        0
z3-noodler-7380a2a-d95fe13                       1747   133   290.37   0.17   0.01   2.33      4     1743        102    18        13        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   214.88   0.12   0.01   2.86     25     1796          0    59         0        0
z3-alpha-4.12.2                                  1824    56   577.34   0.32   0.00   3.16     25     1799          2    54         0        0
ostrich-5dd2e10ca                                1709   171  7631.12   4.47   1.67   6.61     19     1690          0   171         0        0
z3-4.13.0+cvc5-1.1.2                             1870    10   208.98   0.11   0.00   2.86     25     1845         10     0         0        0
z3-noodler-82db97c-d95fe13+cvc5-1.1.2            1861    19    29.28   0.02   0.00   0.56     20     1841         19     0         0        0
z3-noodler-82db97c-d95fe13+z3-4.13.0             1841    39   369.35   0.20   0.01   3.52     25     1816         39     0         0        0
z3-noodler-82db97c-d95fe13+z3-4.13.0+cvc5-1.1.2  1870    10   207.36   0.11   0.00   2.86     25     1845         10     0         0        0
--------------------------------------------------
Benchmark full_str_int
# of formulae: 16968
--------------------------------------------------
tool                                                ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
-----------------------------------------------  -----  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-82db97c-d95fe13                       16760   208    2644.88   0.16   0.01   1.24   2452    14308        128    80         0        0
z3-noodler-7380a2a-d95fe13                       16706   262    2542.58   0.15   0.01   1.17   2440    14266        126   135         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                                        16729   239   20278.49   1.21   0.01   6.90   2473    14256          0   239         0        0
z3-alpha-4.12.2                                  16699   269   24273.69   1.45   0.00   8.85   2447    14252          0   265         4        0
ostrich-5dd2e10ca                                15909  1059  188731.70  11.86   6.07  14.85   1781    14128          0  1059         0        0
z3-4.13.0+cvc5-1.1.2                             16967     1    3604.97   0.21   0.01   0.94   2525    14442          1     0         0        0
z3-noodler-82db97c-d95fe13+cvc5-1.1.2            16966     2    2007.89   0.12   0.01   0.69   2524    14442          2     0         0        0
z3-noodler-82db97c-d95fe13+z3-4.13.0             16950    18    2153.55   0.13   0.01   0.87   2511    14439         18     0         0        0
z3-noodler-82db97c-d95fe13+z3-4.13.0+cvc5-1.1.2  16967     1    1715.33   0.10   0.01   0.64   2525    14442          1     0         0        0
--------------------------------------------------