search

VeriFIT / z3-noodler

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

Update to newest Mata #158

Closed jurajsic closed 2 months ago

jurajsic commented 2 months ago

Results:

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129  102335  1070   11607.70   0.11   0.02   1.60  62902    39433        625   389        56        0
z3-noodler-a8ca33a-d95fe13  102338  1067   12090.90   0.12   0.02   1.67  62907    39431        625   389        53        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                    97694  5711  132044.66   1.35   0.01   8.11  58876    38818        210  4968       463       70
--------------------------------------------------

Benchmark sygus_qgen
# of formulae: 343
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129   343     0    4.57   0.01   0.01   0.01    343        0          0     0         0        0
z3-noodler-a8ca33a-d95fe13   343     0    4.17   0.01   0.01   0.01    343        0          0     0         0        0
cvc5-1.1.2                   343     0   79.25   0.23   0.04   0.94    343        0          0     0         0        0
z3-4.13.0                    343     0   10.38   0.03   0.02   0.02    343        0          0     0         0        0
--------------------------------------------------

Benchmark denghang
# of formulae: 999
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129   999     0   42.54   0.04   0.02   0.60    186      813          0     0         0        0
z3-noodler-a8ca33a-d95fe13   999     0   41.52   0.04   0.02   0.58    186      813          0     0         0        0
cvc5-1.1.2                   981    18  292.35   0.30   0.00   3.71    169      812          0    18         0        0
z3-4.13.0                    883   116  342.20   0.39   0.09   2.17    186      697          0   105        11        0
--------------------------------------------------

Benchmark automatark
# of formulae: 15995
--------------------------------------------------
tool                           ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129  15990     5   533.70   0.03   0.01   0.31  10477     5513          0     5         0        0
z3-noodler-a8ca33a-d95fe13  15990     5   523.67   0.03   0.01   0.30  10477     5513          0     5         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
--------------------------------------------------

Benchmark stringfuzz
# of formulae: 11618
--------------------------------------------------
tool                           ✅    ❌      time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  --------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129  11617     1    379.21   0.03   0.01   1.01   6355     5262          1     0         0        0
z3-noodler-a8ca33a-d95fe13  11617     1    375.33   0.03   0.01   1.05   6355     5262          1     0         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                   11081   537  45873.06   4.14   0.01  15.39   5995     5086          0   412       125        0
--------------------------------------------------

Benchmark redos
# of formulae: 3287
--------------------------------------------------
tool                          ✅    ❌      time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  --------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129  3285     2   2632.91   0.80   0.03   3.79   2445      840          0     2         0        0
z3-noodler-a8ca33a-d95fe13  3285     2   2634.90   0.80   0.03   3.78   2445      840          0     2         0        0
cvc5-1.1.2                  1070  2217  27894.06  26.07   0.03  38.26    574      496          0  2217         0        0
z3-4.13.0                    888  2399    326.46   0.37   0.01   2.85     48      840          0  2099       300        0
--------------------------------------------------

Benchmark norn
# of formulae: 1027
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129  1027     0   14.34   0.01   0.01   0.01    712      315          0     0         0        0
z3-noodler-a8ca33a-d95fe13  1027     0   14.21   0.01   0.01   0.01    712      315          0     0         0        0
cvc5-1.1.2                   943    84  279.95   0.30   0.01   2.77    705      238          0    84         0        0
z3-4.13.0                    903   124  174.62   0.19   0.02   3.88    712      191          0   124         0        0
--------------------------------------------------

Benchmark slog
# of formulae: 1976
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129  1976     0   28.15   0.01   0.01   0.02    808     1168          0     0         0        0
z3-noodler-a8ca33a-d95fe13  1976     0   27.18   0.01   0.01   0.02    808     1168          0     0         0        0
cvc5-1.1.2                  1976     0    1.10   0.00   0.00   0.00    808     1168          0     0         0        0
z3-4.13.0                   1945    31  488.71   0.25   0.01   3.22    777     1168          0    31         0        0
--------------------------------------------------

Benchmark slent
# of formulae: 1128
--------------------------------------------------
tool                          ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129  1122     6   168.36   0.15   0.01   2.64    624      498          0     6         0        0
z3-noodler-a8ca33a-d95fe13  1122     6   271.42   0.24   0.01   3.64    625      497          0     6         0        0
cvc5-1.1.2                  1104    24  1079.50   0.98   0.00   6.51    618      486          0    24         0        0
z3-4.13.0                   1055    73   385.56   0.37   0.01   4.01    571      484          0    73         0        0
--------------------------------------------------

Benchmark omark
# of formulae: 17
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129     9     8    0.13   0.01   0.01   0.01      2        7          0     6         2        0
z3-noodler-a8ca33a-d95fe13     9     8    0.12   0.01   0.01   0.01      2        7          0     6         2        0
cvc5-1.1.2                     5    12    0.95   0.19   0.01   0.41      2        3          0    12         0        0
z3-4.13.0                      7    10    7.67   1.10   0.01   2.86      2        5          0     8         2        0
--------------------------------------------------

Benchmark kepler
# of formulae: 587
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129   584     3   15.69   0.03   0.01   0.07    284      300          0     3         0        0
z3-noodler-a8ca33a-d95fe13   584     3   16.02   0.03   0.01   0.07    284      300          0     3         0        0
cvc5-1.1.2                   347   240    0.54   0.00   0.00   0.00     50      297          0   240         0        0
z3-4.13.0                    278   309   24.64   0.09   0.01   0.87    135      143          0   285        24        0
--------------------------------------------------

Benchmark woorpje
# of formulae: 809
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129   774    35  219.53   0.28   0.01   3.33    612      162          0    17        18        0
z3-noodler-a8ca33a-d95fe13   773    36  283.33   0.37   0.01   4.49    611      162          0    18        18        0
cvc5-1.1.2                   755    54   45.21   0.06   0.01   0.23    591      164          0    54         0        0
z3-4.13.0                    782    27  300.36   0.38   0.02   4.80    618      164          0    27         0        0
--------------------------------------------------

Benchmark webapp
# of formulae: 681
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129   363   318   15.15   0.04   0.02   0.08    135      228        316     0         2        0
z3-noodler-a8ca33a-d95fe13   363   318   15.73   0.04   0.02   0.10    135      228        316     0         2        0
cvc5-1.1.2                   588    93  864.69   1.47   0.01   9.96    165      423          0    93         0        0
z3-4.13.0                    450   231  312.63   0.69   0.02   6.78     36      414        120   111         0        0
--------------------------------------------------

Benchmark kaluza
# of formulae: 19432
--------------------------------------------------
tool                           ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129  19214   218  1368.61   0.07   0.01   2.12  16112     3102          0   198        20        0
z3-noodler-a8ca33a-d95fe13  19211   221  1063.08   0.06   0.01   1.44  16112     3099          0   205        16        0
cvc5-1.1.2                  19431     1  1061.97   0.05   0.00   1.87  16302     3129          0     1         0        0
z3-4.13.0                   19148   284  2019.12   0.11   0.01   2.02  16032     3116          0   284         0        0
--------------------------------------------------

Benchmark transducer_plus
# of formulae: 91
--------------------------------------------------
tool                          ✅    ❌    time     avg     med     std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  ------  ------  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129     0    91    0.00  nan     nan     nan         0        0         91     0         0        0
z3-noodler-a8ca33a-d95fe13     0    91    0.00  nan     nan     nan         0        0         91     0         0        0
cvc5-1.1.2                    42    49  490.70   11.68    3.24   22.98     41        1          0    49         0        0
z3-4.13.0                      1    90    0.01    0.01    0.01  nan         0        1         90     0         0        0
--------------------------------------------------

Benchmark leetcode
# of formulae: 2652
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129  2650     2   52.88   0.02   0.01   0.04    866     1784          0     0         2        0
z3-noodler-a8ca33a-d95fe13  2648     4   52.43   0.02   0.01   0.05    864     1784          0     0         4        0
cvc5-1.1.2                  2652     0   32.91   0.01   0.00   0.03    867     1785          0     0         0        0
z3-4.13.0                   2652     0   43.44   0.02   0.01   0.12    867     1785          0     0         0        0
--------------------------------------------------

Benchmark str_small_rw
# of formulae: 1880
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129  1761   119  335.75   0.19   0.01   2.63      4     1757         92    18         9        0
z3-noodler-a8ca33a-d95fe13  1762   118  365.65   0.21   0.01   2.74      4     1758         92    17         9        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
--------------------------------------------------

Benchmark pyex
# of formulae: 23845
--------------------------------------------------
tool                           ✅    ❌      time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  --------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129  23751    94   4180.49   0.18   0.10   1.14  20380     3371          0    92         2        0
z3-noodler-a8ca33a-d95fe13  23754    91   4657.91   0.20   0.10   1.85  20382     3372          0    89         2        0
cvc5-1.1.2                  23826    19   6384.00   0.27   0.07   2.48  20406     3420          0    19         0        0
z3-4.13.0                   22858   987  54817.37   2.40   0.12  10.23  19587     3271          0   987         0        0
--------------------------------------------------

Benchmark full_str_int
# of formulae: 16968
--------------------------------------------------
tool                           ✅    ❌      time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  --------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129  16800   168   1614.88   0.10   0.01   1.80   2487    14313        125    42         1        0
z3-noodler-a8ca33a-d95fe13  16805   163   1743.48   0.10   0.01   1.83   2492    14313        125    38         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                   16729   239  20278.49   1.21   0.01   6.90   2473    14256          0   239         0        0
--------------------------------------------------

Benchmark snia
# of formulae: 70
--------------------------------------------------
tool                          ✅    ❌    time     avg     med     std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  ------  ------  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-1bb282d-8119129    70     0    0.81    0.01    0.01    0.01     70        0          0     0         0        0
z3-noodler-a8ca33a-d95fe13    70     0    0.75    0.01    0.01    0.01     70        0          0     0         0        0
cvc5-1.1.2                    70     0    0.00    0.00    0.00    0.00     70        0          0     0         0        0
z3-4.13.0                      0    70    0.00  nan     nan     nan         0        0          0     0         0       70
--------------------------------------------------

image

jurajsic commented 2 months ago

No incorrect results, everything works, we can merge after merging #150 and #143.

vhavlena commented 2 months ago

Can you change the mata version in README file?