Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Reenable rewriter rule (str.in A (str.to_re B)) -> (A = B) #137

Merged
merged 1 commit into from
Apr 29, 2024
Merged

Reenable rewriter rule (str.in A (str.to_re B)) -> (A = B) #137

merged 1 commit into from
Apr 29, 2024

Conversation

jurajsic
Copy link
Member

@jurajsic jurajsic commented Apr 26, 2024 •
edited
Loading

This PR reenables the rewriter rule (str.in A (str.to_re B)) -> (A = B) which was turned off in #39 (probably because of slent) and partly reenabled in #126.

@jurajsic
Copy link
Member Author

jurajsic commented Apr 27, 2024 •
edited
Loading

After reenabling the rule a in (str.to_re a') -> (a = a'):

# of formulae: 103318
--------------------------------------------------
tool                                                 ✅     ❌       time    avg    med    std    sat    unsat    unknown     TO    MO+ERR    other
-----------------------------------------------  ------  -----  ---------  -----  -----  -----  -----  -------  ---------  -----  --------  -------
z3-noodler-e58cb97-d95fe13                       102120   1198   13149.57   0.13   0.01   1.55  62768    39352        636    509        53        0
z3-noodler-605ccd5-d95fe13                       101976   1342   15990.37   0.16   0.01   1.75  62637    39339        638    658        46        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
ostrich-5dd2e10ca                                 86344  16986  782639.00   9.06   1.75  19.20  47556    38788          0  16962        12       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
z3-noodler-e58cb97-d95fe13+cvc5-1.1.2            103176    142    9532.31   0.09   0.00   1.43  63261    39915        142      0         0        0
z3-noodler-e58cb97-d95fe13+z3-4.13.0             102785    533   10145.54   0.10   0.01   1.10  62956    39829        533      0         0        0
z3-noodler-e58cb97-d95fe13+z3-4.13.0+cvc5-1.1.2  103190    128    8963.63   0.09   0.00   1.46  63270    39920        128      0         0        0
--------------------------------------------------

Interesting benchmarks:

Benchmark automatark
# of formulae: 15995
--------------------------------------------------
tool                                                ✅    ❌      time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
-----------------------------------------------  -----  ----  --------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-e58cb97-d95fe13                       15970    25    904.53   0.06   0.01   0.67  10466     5504          0    25         0        0
z3-noodler-605ccd5-d95fe13                       15963    32   1014.05   0.06   0.01   0.67  10463     5500          0    32         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
ostrich-5dd2e10ca                                15947    48  24332.97   1.53   1.41   1.89  10440     5507          0    48         0        0
z3-4.13.0+cvc5-1.1.2                             15969    26    543.82   0.03   0.00   1.22  10481     5488         26     0         0        0
z3-noodler-e58cb97-d95fe13+cvc5-1.1.2            15991     4    177.80   0.01   0.00   0.27  10478     5513          4     0         0        0
z3-noodler-e58cb97-d95fe13+z3-4.13.0             15995     0    389.91   0.02   0.01   0.36  10481     5514          0     0         0        0
z3-noodler-e58cb97-d95fe13+z3-4.13.0+cvc5-1.1.2  15995     0    100.21   0.01   0.00   0.16  10481     5514          0     0         0        0
--------------------------------------------------

Benchmark slent
# of formulae: 1128
--------------------------------------------------
tool                                               ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
-----------------------------------------------  ----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-e58cb97-d95fe13                       1124     4   236.71   0.21   0.01   3.16    626      498          0     4         0        0
z3-noodler-605ccd5-d95fe13                       1125     3    25.59   0.02   0.01   0.11    629      496          1     2         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
ostrich-5dd2e10ca                                1002   126  5154.54   5.14   2.00  13.05    592      410          0   126         0        0
z3-4.13.0+cvc5-1.1.2                             1112    16  1044.79   0.94   0.00   6.35    620      492         16     0         0        0
z3-noodler-e58cb97-d95fe13+cvc5-1.1.2            1128     0    10.29   0.01   0.00   0.08    630      498          0     0         0        0
z3-noodler-e58cb97-d95fe13+z3-4.13.0             1128     0    28.62   0.03   0.01   0.39    630      498          0     0         0        0
z3-noodler-e58cb97-d95fe13+z3-4.13.0+cvc5-1.1.2  1128     0     7.56   0.01   0.00   0.05    630      498          0     0         0        0
--------------------------------------------------

Benchmark webapp
# of formulae: 681
--------------------------------------------------
tool                                               ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
-----------------------------------------------  ----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-e58cb97-d95fe13                        361   320    14.47   0.04   0.02   0.09    133      228        316     2         2        0
z3-noodler-605ccd5-d95fe13                        355   326    66.63   0.19   0.02   1.99    130      225        316     6         4        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
ostrich-5dd2e10ca                                 539   142  6434.26  11.94   4.14  24.06    125      414          0   142         0        0
z3-4.13.0+cvc5-1.1.2                              590    91   861.65   1.46   0.01   9.95    167      423         91     0         0        0
z3-noodler-e58cb97-d95fe13+cvc5-1.1.2             633    48   444.93   0.70   0.01   6.96    210      423         48     0         0        0
z3-noodler-e58cb97-d95fe13+z3-4.13.0              551   130    70.95   0.13   0.02   2.30    134      417        130     0         0        0
z3-noodler-e58cb97-d95fe13+z3-4.13.0+cvc5-1.1.2   633    48   443.27   0.70   0.01   6.96    210      423         48     0         0        0
--------------------------------------------------

Benchmark kaluza
# of formulae: 19432
--------------------------------------------------
tool                                                ✅    ❌      time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
-----------------------------------------------  -----  ----  --------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-e58cb97-d95fe13                       19209   223    940.47   0.05   0.01   1.58  16111     3098          0   209        14        0
z3-noodler-605ccd5-d95fe13                       19106   326   1063.84   0.06   0.01   1.38  15999     3107          0   320         6        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
ostrich-5dd2e10ca                                19144   290  37052.30   1.94   1.39   3.45  16015     3129          0   286         2        2
z3-4.13.0+cvc5-1.1.2                             19431     1    911.09   0.05   0.00   1.82  16302     3129          1     0         0        0
z3-noodler-e58cb97-d95fe13+cvc5-1.1.2            19431     1   1045.84   0.05   0.00   1.87  16302     3129          1     0         0        0
z3-noodler-e58cb97-d95fe13+z3-4.13.0             19266   166    484.52   0.03   0.01   0.47  16144     3122        166     0         0        0
z3-noodler-e58cb97-d95fe13+z3-4.13.0+cvc5-1.1.2  19431     1    899.28   0.05   0.00   1.82  16302     3129          1     0         0        0
--------------------------------------------------

Benchmark redos
# of formulae: 3287
--------------------------------------------------
tool                                               ✅    ❌      time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
-----------------------------------------------  ----  ----  --------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-e58cb97-d95fe13                       3284     3   2490.22   0.76   0.03   3.61   2444      840          0     3         0        0
z3-noodler-605ccd5-d95fe13                       3256    31   5271.29   1.62   0.91   6.17   2428      828          0    31         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
ostrich-5dd2e10ca                                1715  1572  55284.56  32.24  33.17  36.98   1053      662          0  1572         0        0
z3-4.13.0+cvc5-1.1.2                             1414  1873  27009.57  19.10   0.02  34.70    574      840       1873     0         0        0
z3-noodler-e58cb97-d95fe13+cvc5-1.1.2            3284     3   2349.02   0.72   0.02   3.60   2444      840          3     0         0        0
z3-noodler-e58cb97-d95fe13+z3-4.13.0             3284     3   2221.45   0.68   0.02   3.60   2444      840          3     0         0        0
z3-noodler-e58cb97-d95fe13+z3-4.13.0+cvc5-1.1.2  3284     3   2217.38   0.68   0.02   3.60   2444      840          3     0         0        0
--------------------------------------------------

We improved on automatark, redos, kaluza, and webapp (but the last one is probably some randomness), while there is slight degradation on few (4 or so) formulae from slent (which might be the reason this rule was turned off in #39.

@jurajsic jurajsic force-pushed the fix_rewriter branch 2 times, most recently from 43f4868 to 5e0e87f Compare April 29, 2024 07:50
@jurajsic jurajsic changed the title Rewriter stuff Reenable rewriter rule (str.in A (str.to_re B)) -> (A = B) Apr 29, 2024
@jurajsic jurajsic marked this pull request as ready for review April 29, 2024 07:54
@jurajsic jurajsic requested a review from vhavlena April 29, 2024 07:55
@jurajsic jurajsic merged commit 703d15c into devel Apr 29, 2024
@jurajsic jurajsic deleted the fix_rewriter branch April 29, 2024 18:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@vhavlena vhavlena vhavlena approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@jurajsic @vhavlena