New remove_epsilon() for nfa

[jurajsic]

This PR rewrites the code for remove_epsilon() by using simpler epsilon closure computation and using synchronized iterator for adding new transitions.

There are still possible optimizations, by

1. adding a version that works in-place instead of the current one,
2. assuming that epsilon is always at the end (we could have something like first epsilon as argument instead of specific symbol).

[jurajsic]

I benchmarked this version by running Z3-Noodler benchmarks, these are the results (compared to devel):

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74  102884   521  8469.59   0.08   0.01   1.28  63193    39691        186   227       108        0
z3-noodler-67f7ce2-71f80d7  102884   521  8614.87   0.08   0.01   1.30  63193    39691        186   228       107        0
--------------------------------------------------


Benchmark sygus_qgen
# of formulae: 343
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74   343     0    1.61   0.00   0.00   0.01    343        0          0     0         0        0
z3-noodler-67f7ce2-71f80d7   343     0    1.96   0.01   0.01   0.01    343        0          0     0         0        0
--------------------------------------------------

Benchmark denghang
# of formulae: 999
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74   999     0   38.21   0.04   0.01   0.71    186      813          0     0         0        0
z3-noodler-67f7ce2-71f80d7   999     0   37.62   0.04   0.01   0.68    186      813          0     0         0        0
--------------------------------------------------

Benchmark automatark
# of formulae: 15995
--------------------------------------------------
tool                           ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74  15990     5  541.30   0.03   0.01   0.46  10477     5513          0     5         0        0
z3-noodler-67f7ce2-71f80d7  15990     5  541.65   0.03   0.01   0.45  10477     5513          0     5         0        0
--------------------------------------------------

Benchmark stringfuzz
# of formulae: 11618
--------------------------------------------------
tool                           ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74  11617     1  205.19   0.02   0.00   0.17   6355     5262          1     0         0        0
z3-noodler-67f7ce2-71f80d7  11617     1  209.57   0.02   0.01   0.17   6355     5262          1     0         0        0
--------------------------------------------------

Benchmark redos
# of formulae: 3287
--------------------------------------------------
tool                          ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74  3285     2  2126.36   0.65   0.02   3.39   2445      840          0     2         0        0
z3-noodler-67f7ce2-71f80d7  3285     2  2067.73   0.63   0.02   3.17   2445      840          0     2         0        0
--------------------------------------------------

Benchmark norn
# of formulae: 1027
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74  1027     0    5.28   0.01   0.00   0.01    712      315          0     0         0        0
z3-noodler-67f7ce2-71f80d7  1027     0    5.73   0.01   0.01   0.01    712      315          0     0         0        0
--------------------------------------------------

Benchmark slog
# of formulae: 1976
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74  1976     0    9.93   0.01   0.00   0.02    808     1168          0     0         0        0
z3-noodler-67f7ce2-71f80d7  1976     0   11.34   0.01   0.00   0.02    808     1168          0     0         0        0
--------------------------------------------------

Benchmark slent
# of formulae: 1128
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74  1128     0   23.79   0.02   0.00   0.26    630      498          0     0         0        0
z3-noodler-67f7ce2-71f80d7  1128     0   24.29   0.02   0.01   0.26    630      498          0     0         0        0
--------------------------------------------------

Benchmark omark
# of formulae: 17
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74     9     8    0.08   0.01   0.00   0.02      2        7          0     6         2        0
z3-noodler-67f7ce2-71f80d7     9     8    0.09   0.01   0.01   0.02      2        7          0     6         2        0
--------------------------------------------------

Benchmark kepler
# of formulae: 587
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74   584     3   10.59   0.02   0.01   0.07    284      300          0     1         2        0
z3-noodler-67f7ce2-71f80d7   584     3   10.54   0.02   0.01   0.07    284      300          0     2         1        0
--------------------------------------------------

Benchmark woorpje
# of formulae: 809
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74   774    35  282.26   0.36   0.01   4.17    614      160          0    17        18        0
z3-noodler-67f7ce2-71f80d7   774    35  298.67   0.39   0.01   4.50    614      160          0    17        18        0
--------------------------------------------------

Benchmark webapp
# of formulae: 681
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74   641    40  170.56   0.27   0.01   3.11    215      426         38     0         2        0
z3-noodler-67f7ce2-71f80d7   641    40  169.43   0.26   0.01   3.09    215      426         38     0         2        0
--------------------------------------------------

Benchmark kaluza
# of formulae: 19432
--------------------------------------------------
tool                           ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74  19369    63  119.08   0.01   0.00   0.05  16277     3092         20    34         9        0
z3-noodler-67f7ce2-71f80d7  19369    63  133.45   0.01   0.00   0.05  16277     3092         20    34         9        0
--------------------------------------------------

Benchmark transducer_plus
# of formulae: 91
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74     1    90    0.01   0.01   0.01    nan      0        1          6    37        47        0
z3-noodler-67f7ce2-71f80d7     1    90    0.01   0.01   0.01    nan      0        1          6    37        47        0
--------------------------------------------------

Benchmark leetcode
# of formulae: 2652
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74  2651     1   25.29   0.01   0.00   0.05    867     1784          0     0         1        0
z3-noodler-67f7ce2-71f80d7  2651     1   28.22   0.01   0.01   0.05    867     1784          0     0         1        0
--------------------------------------------------

Benchmark str_small_rw
# of formulae: 1880
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74  1823    57  203.17   0.11   0.00   1.16      4     1819          4    28        25        0
z3-noodler-67f7ce2-71f80d7  1823    57  208.24   0.11   0.00   1.19      4     1819          4    28        25        0
--------------------------------------------------

Benchmark pyex
# of formulae: 23845
--------------------------------------------------
tool                           ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74  23778    67  3624.29   0.15   0.08   1.71  20406     3372          0    65         2        0
z3-noodler-67f7ce2-71f80d7  23778    67  3796.66   0.16   0.08   1.80  20406     3372          0    65         2        0
--------------------------------------------------

Benchmark full_str_int
# of formulae: 16968
--------------------------------------------------
tool                           ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74  16819   149  1082.40   0.06   0.01   1.41   2498    14321        117    32         0        0
z3-noodler-67f7ce2-71f80d7  16819   149  1069.50   0.06   0.01   1.41   2498    14321        117    32         0        0
--------------------------------------------------

Benchmark snia
# of formulae: 70
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-67f7ce2-5f2fe74    70     0    0.19   0.00   0.00   0.00     70        0          0     0         0        0
z3-noodler-67f7ce2-71f80d7    70     0    0.17   0.00   0.00   0.00     70        0          0     0         0        0
--------------------------------------------------

[Adda0]

Since the changes actually do not improve the overall performance, we need to run a proper benchmarking of the changes, perf-test some examples where the performance in worse, and fix the algorithm for such examples. Until this is done, we will convert the PR into a draft.

[jurajsic]

Just a note for myself: if I add the in-place remove_epsilon() method, change its return value to Nfa& similarly as in in-place trim(). Also, I should change it for NFTs too.