VeriFIT / z3-noodler

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

Turn on reduction for noodlification #107

Closed jurajsic closed 10 months ago

jurajsic commented 1 year ago

This PR fixes a bug where noodlification did not reduce (nor trim) automata in resulting nooodles.

Needs to be benchmarked, it is possible that simulation might slow it down, or that we should just turn on trimming.

vhavlena commented 1 year ago

Maybe the simulation reduction will be too expensive. We could add option "trim" to do just the trimming. But we will see after the results.

vhavlena commented 11 months ago

I suggest first to finish and merge the PR #104 and then try the effect of the noodle reduction.

vhavlena commented 10 months ago

The results (z3-noodler-feada45-a57f582 is the PR version, z3-noodler-1482571-a57f582 is the pyex-opt version -- NOT devel) image

# of formulae: 82972
###################################################################################
####                                   Table 1                                 ####
###################################################################################
| method                     |    max |     mean |   median |   std. dev |   TO+MO+ERR |   unknowns |
|----------------------------|--------|----------|----------|------------|-------------|------------|
| z3-noodler-feada45-a57f582 | 116.1  | 0.494545 |     0.02 |    3.67665 |        2198 |       2011 |
| cvc5-1.0.8                 | 119.36 | 0.515113 |     0.02 |    5.2351  |        1723 |          2 |
| z3-4.12.2                  | 119.29 | 1.49018  |     0.04 |    8.17615 |        2623 |        123 |
| z3-noodler-1482571-a57f582 | 115.42 | 0.463528 |     0.02 |    3.42857 |        2465 |       2098 |
vhavlena commented 10 months ago

Should I merge the PR?

Adda0 commented 10 months ago

I would merge the PR.