search

VeriFIT / z3-noodler

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

Relevancy fixing #163

Closed vhavlena closed 3 months ago

vhavlena commented 3 months ago

This PR fixes relevancy propagation of prefix and friends during the initial search.

vhavlena commented 3 months ago

Results:

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-38dbe37-2756940  102424   981   14375.28   0.14   0.01   1.99  62951    39473        530   378        73        0
z3-noodler-334dc52-2756940  102404  1001   12243.71   0.12   0.02   1.70  62914    39490        528   396        77        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
--------------------------------------------------
vhavlena commented 3 months ago

Is suffix and preffix enough? Aren't there other functions whose negations should be also marked as relevant?

I added also contains. The problem affects predicates only.

vhavlena commented 3 months ago

There is some degradation on full_str_int

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-7801978-2756940  102424   981   14358.39   0.14   0.02   1.99  62951    39473        530   378        73        0
z3-noodler-334dc52-2756940  102404  1001   12243.71   0.12   0.02   1.70  62914    39490        528   396        77        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
--------------------------------------------------

Benchmark full_str_int
# of formulae: 16968
--------------------------------------------------
tool                           ✅    ❌      time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  --------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-7801978-2756940  16801   167   3801.76   0.23   0.01   3.12   2493    14308        117    50         0        0
z3-noodler-334dc52-2756940  16810   158   1496.75   0.09   0.01   1.34   2489    14321        117    40         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                   16732   236  18620.60   1.11   0.01   6.38   2476    14256          0   236         0        0
--------------------------------------------------

image

jurajsic commented 3 months ago

I think the degradation is ok, it is better to be correct. You can merge.