search

VeriFIT / z3-noodler

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

Reenable `str.in_re` rewrite rule #126

Closed jurajsic closed 8 months ago

jurajsic commented 8 months ago

In #39, we disabled rewriter rule (str.in_re S1 (str.to_re S2)) -> S1 = S2 because it could create a large amount of disequalities (if there was negation before it). However, if S2 contains variables, noodler fails, because it cannot handle variables in regexes. So for these cases, we reenable it.

jurajsic commented 8 months ago 
Benchmark sygus_qgen/to120.csv
# of formulae: 343
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f   343     0   0.02   0.02    5.25    343        0          0     0         0        0
cvc5-1.0.8                   343     0   0.27   0.10   92.87    343        0          0     0         0        0
z3-4.12.2                    343     0   0.06   0.05   20.06    343        0          0     0         0        0
cvc5-1.1.1                   343     0   0.23   0.04   79.96    343        0          0     0         0        0
z3-4.12.5                    343     0   0.03   0.02   10.59    343        0          0     0         0        0
z3-noodler-005708c-2cddb2f   343     0   0.02   0.02    5.24    343        0          0     0         0        0
--------------------------------------------------

Benchmark denghang/to120.csv
# of formulae: 999
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f   999     0   0.04   0.02   42.38    186      813          0     0         0        0
cvc5-1.0.8                   981    18   0.46   0.02  452.30    169      812          0    18         0        0
z3-4.12.2                    881   118   0.45   0.13  398.98    186      695          0   118         0        0
cvc5-1.1.1                   981    18   0.43   0.00  418.42    169      812          0    18         0        0
z3-4.12.5                    883   116   0.39   0.08  341.13    186      697          0   105        11        0
z3-noodler-005708c-2cddb2f   999     0   0.04   0.02   42.05    186      813          0     0         0        0
--------------------------------------------------

Benchmark automatark/to120.csv
# of formulae: 15995
--------------------------------------------------
tool                           ✅    ❌    avg    med     time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -----  -----  -------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f  15935    60   0.12   0.02  1912.75  10452     5483          0    60         0        0
cvc5-1.0.8                  15901    94   0.17   0.01  2639.32  10459     5442          0    85         9        0
z3-4.12.2                   15882   113   0.31   0.05  4845.79  10471     5411          0   112         1        0
cvc5-1.1.1                  15899    96   0.15   0.00  2418.43  10459     5440          0    88         8        0
z3-4.12.5                   15869   126   0.40   0.02  6343.72  10468     5401          0   125         1        0
z3-noodler-005708c-2cddb2f  15935    60   0.12   0.02  1924.32  10452     5483          0    60         0        0
--------------------------------------------------

Benchmark stringfuzz/to120.csv
# of formulae: 11618
--------------------------------------------------
tool                           ✅    ❌    avg    med      time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -----  -----  --------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f  11614     4   0.03   0.01    337.82   6353     5261          4     0         0        0
cvc5-1.0.8                  10552  1066   2.61   0.02  27503.53   5777     4775          0  1065         1        0
z3-4.12.2                   11232   386   4.14   0.04  46483.27   6148     5084          0   367        19        0
cvc5-1.1.1                  10522  1096   2.65   0.00  27893.23   5756     4766          0  1095         1        0
z3-4.12.5                   11072   546   4.09   0.01  45283.01   5986     5086          0   421       125        0
z3-noodler-005708c-2cddb2f  11613     5   0.03   0.01    339.16   6353     5260          5     0         0        0
--------------------------------------------------

Benchmark norn/to120.csv
# of formulae: 1027
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f  1027     0   0.01   0.01   14.98    712      315          0     0         0        0
cvc5-1.0.8                   942    85   0.25   0.03  236.08    705      237          0    85         0        0
z3-4.12.2                    903   124   0.19   0.05  168.88    712      191          0   124         0        0
cvc5-1.1.1                   943    84   0.29   0.01  274.24    705      238          0    84         0        0
z3-4.12.5                    904   123   0.32   0.02  293.44    712      192          0   123         0        0
z3-noodler-005708c-2cddb2f  1027     0   0.02   0.01   15.56    712      315          0     0         0        0
--------------------------------------------------

Benchmark slog/to120.csv
# of formulae: 1976
--------------------------------------------------
tool                          ✅    ❌    avg    med     time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  -------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f  1976     0   0.02   0.01    30.03    808     1168          0     0         0        0
cvc5-1.0.8                  1976     0   0.01   0.01    18.27    808     1168          0     0         0        0
z3-4.12.2                   1905    71   0.58   0.03  1109.01    737     1168          0    71         0        0
cvc5-1.1.1                  1976     0   0.00   0.00     1.00    808     1168          0     0         0        0
z3-4.12.5                   1943    33   0.12   0.01   224.64    775     1168          0    33         0        0
z3-noodler-005708c-2cddb2f  1976     0   0.02   0.01    30.15    808     1168          0     0         0        0
--------------------------------------------------

Benchmark slent/to120.csv
# of formulae: 1128
--------------------------------------------------
tool                          ✅    ❌    avg    med     time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  -------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f  1127     1   0.05   0.01    52.02    629      498          1     0         0        0
cvc5-1.0.8                  1106    22   0.87   0.01   965.39    618      488          0    22         0        0
z3-4.12.2                   1054    74   0.38   0.03   401.39    573      481          0    74         0        0
cvc5-1.1.1                  1104    24   0.98   0.00  1080.27    618      486          0    24         0        0
z3-4.12.5                   1053    75   0.29   0.01   300.43    569      484          0    75         0        0
z3-noodler-005708c-2cddb2f  1126     2   0.03   0.01    31.27    629      497          1     1         0        0
--------------------------------------------------

Benchmark transducer_plus/to120.csv
# of formulae: 91
--------------------------------------------------
tool                          ✅    ❌     avg     med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  ------  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f     0    91  nan     nan       0.00      0        0         91     0         0        0
cvc5-1.0.8                    42    49   13.34    3.17  560.14     41        1          0    49         0        0
z3-4.12.2                      1    90    0.04    0.04    0.04      0        1         90     0         0        0
cvc5-1.1.1                    41    50   15.49    3.71  635.07     40        1          0    50         0        0
z3-4.12.5                      1    90    0.01    0.01    0.01      0        1         90     0         0        0
z3-noodler-005708c-2cddb2f     0    91  nan     nan       0.00      0        0         91     0         0        0
--------------------------------------------------

Benchmark kepler/to120.csv
# of formulae: 587
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f   584     3   0.03   0.01   16.42    284      300          0     3         0        0
cvc5-1.0.8                   347   240   0.01   0.01    4.86     50      297          0   240         0        0
z3-4.12.2                    274   313   0.06   0.04   17.09    131      143          0   313         0        0
cvc5-1.1.1                   347   240   0.00   0.00    0.65     50      297          0   240         0        0
z3-4.12.5                    278   309   0.09   0.02   25.70    135      143          0   284        25        0
z3-noodler-005708c-2cddb2f   584     3   0.03   0.01   16.62    284      300          0     3         0        0
--------------------------------------------------

Benchmark woorpje/to120.csv
# of formulae: 809
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f   750    59   0.52   0.02  388.10    589      161          0    15        44        0
cvc5-1.0.8                   755    54   0.11   0.03   83.22    591      164          0    54         0        0
z3-4.12.2                    784    25   0.52   0.04  405.28    620      164          0    25         0        0
cvc5-1.1.1                   755    54   0.06   0.01   44.90    591      164          0    54         0        0
z3-4.12.5                    782    27   0.27   0.02  214.78    618      164          0    27         0        0
z3-noodler-005708c-2cddb2f   751    58   0.68   0.02  511.61    590      161          0    14        44        0
--------------------------------------------------

Benchmark webapp/to120.csv
# of formulae: 681
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f   358   323   0.52   0.02  184.97    132      226        316     3         4        0
cvc5-1.0.8                   588    93   1.36   0.05  800.32    165      423          0    93         0        0
z3-4.12.2                    457   224   0.71   0.04  323.64     42      415        123   101         0        0
cvc5-1.1.1                   587    94   1.35   0.01  791.79    164      423          0    94         0        0
z3-4.12.5                    447   234   0.46   0.02  203.56     33      414        119   115         0        0
z3-noodler-005708c-2cddb2f   358   323   0.54   0.02  193.73    132      226        316     3         4        0
--------------------------------------------------

Benchmark kaluza/to120.csv
# of formulae: 19432
--------------------------------------------------
tool                           ✅    ❌    avg    med     time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -----  -----  -------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f  19163   269   0.06   0.01  1174.86  16066     3097          0   261         8        0
cvc5-1.0.8                  19432     0   0.06   0.01  1253.63  16303     3129          0     0         0        0
z3-4.12.2                   19268   164   0.11   0.02  2095.90  16145     3123          0   164         0        0
cvc5-1.1.1                  19432     0   0.06   0.00  1122.86  16303     3129          0     0         0        0
z3-4.12.5                   19147   285   0.10   0.01  1938.97  16031     3116          0   285         0        0
z3-noodler-005708c-2cddb2f  19160   272   0.05   0.01   928.07  16065     3095          0   264         8        0
--------------------------------------------------

Benchmark leetcode/to120.csv
# of formulae: 2652
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f  2648     4   0.02   0.01   54.65    864     1784          0     0         4        0
cvc5-1.0.8                  2652     0   0.03   0.02   87.84    867     1785          0     0         0        0
z3-4.12.2                   2652     0   0.04   0.02   99.66    867     1785          0     0         0        0
cvc5-1.1.1                  2652     0   0.01   0.00   32.58    867     1785          0     0         0        0
z3-4.12.5                   2652     0   0.02   0.01   43.00    867     1785          0     0         0        0
z3-noodler-005708c-2cddb2f  2648     4   0.02   0.01   53.15    864     1784          0     0         4        0
--------------------------------------------------

Benchmark str_small_rw/to120.csv
# of formulae: 1880
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f  1744   136   0.20   0.01  346.11      4     1740        101    21        14        0
cvc5-1.0.8                  1861    19   0.03   0.01   48.26     22     1839          2    17         0        0
z3-4.12.2                   1817    63   0.06   0.03  112.09     25     1792          0    63         0        0
cvc5-1.1.1                  1861    19   0.02   0.00   28.48     20     1841          2    17         0        0
z3-4.12.5                   1819    61   0.07   0.01  132.27     25     1794          0    61         0        0
z3-noodler-005708c-2cddb2f  1745   135   0.19   0.01  331.10      4     1741        101    23        11        0
--------------------------------------------------

Benchmark pyex/to120.csv
# of formulae: 23845
--------------------------------------------------
tool                           ✅    ❌    avg    med      time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -----  -----  --------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f  23751    94   0.21   0.10   5035.65  20380     3371          0    93         1        0
cvc5-1.0.8                  23811    34   0.32   0.13   7665.50  20392     3419          0    33         1        0
z3-4.12.2                   22774  1071   2.77   0.24  63069.90  19503     3271          0  1071         0        0
cvc5-1.1.1                  23802    43   0.21   0.06   5103.25  20383     3419          0    43         0        0
z3-4.12.5                   22839  1006   2.42   0.12  55195.90  19568     3271          0  1006         0        0
z3-noodler-005708c-2cddb2f  23751    94   0.21   0.10   4993.58  20380     3371          0    93         1        0
--------------------------------------------------

Benchmark full_str_int/to120.csv
# of formulae: 16968
--------------------------------------------------
tool                           ✅    ❌    avg    med      time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -----  -----  --------  -----  -------  ---------  ----  --------  -------
z3-noodler-789525b-2cddb2f  16270   698   0.21   0.01   3421.03   2003    14267        577   121         0        0
cvc5-1.0.8                  16968     0   0.31   0.03   5258.46   2526    14442          0     0         0        0
z3-4.12.2                   16734   234   1.45   0.04  24231.84   2478    14256          0   234         0        0
cvc5-1.1.1                  16963     5   0.27   0.01   4657.42   2522    14441          0     5         0        0
z3-4.12.5                   16727   241   1.21   0.01  20316.56   2471    14256          0   241         0        0
z3-noodler-005708c-2cddb2f  16268   700   0.21   0.01   3380.19   2001    14267        578   122         0        0
--------------------------------------------------
jurajsic commented 8 months ago

It solved at least that one unknown in stringfuzz which was the whole reason for this PR, otherwise it probably had no impact, other than the random +-solved few instances in other benchmarks.