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.

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

Fixing infinite looping #140

Merged
merged 4 commits into from
May 9, 2024
Merged

Fixing infinite looping #140

merged 4 commits into from
May 9, 2024

Conversation

vhavlena
Copy link
Collaborator

@vhavlena vhavlena commented May 3, 2024

This PR introduces small optimizations:

  • better axioms for conversions preventing infinite looping in the loop protection
  • better axiom for replace slightly reducing the number of unknows in str_small_rw

@vhavlena
Copy link
Collaborator Author

vhavlena commented May 3, 2024

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
--------------------------------------------------

@vhavlena vhavlena marked this pull request as ready for review May 3, 2024 18:47
@vhavlena vhavlena requested a review from jurajsic May 3, 2024 18:47
@vhavlena vhavlena merged commit d59547c into devel May 9, 2024
@vhavlena vhavlena deleted the infinite-looping branch May 9, 2024 12:58
This was referenced May 16, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants