search

VeriFIT / z3-noodler

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

Fix axioms for replace_re #162

Closed jurajsic closed 3 months ago

jurajsic commented 3 months ago

This PR fixes axioms for replace_re, they now look a bit similar to replace, with handling the tightest prefix.

jurajsic commented 3 months ago 
# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-d3ad231-2756940  102380  1025    7817.79   0.08   0.01   0.69  62887    39493        528   468        29        0
z3-noodler-756c48c-2756940  102407   998   12292.07   0.12   0.02   1.73  62917    39490        528   396        74        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                    97745  5660  128712.47   1.32   0.01   7.95  58927    38818        211  4914       465       70
--------------------------------------------------

image

jurajsic commented 3 months ago

I just realised it is not correct, I need to handle the case when empty string is in R.

jurajsic commented 3 months ago

With the fix for epsilon:

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-334dc52-2756940  102404  1001   12243.71   0.12   0.02   1.70  62914    39490        528   396        77        0
z3-noodler-756c48c-2756940  102407   998   12292.07   0.12   0.02   1.73  62917    39490        528   396        74        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                    97745  5660  128712.47   1.32   0.01   7.95  58927    38818        211  4914       465       70
--------------------------------------------------

image