Add option to select reduction algorithm by jurajsic · Pull Request #218 · VeriFIT/z3-noodler

jurajsic · 2025-04-15T13:54:20Z

Comparison of NFA reduction methods. It just replaces all reduce() simulation calls (also in noodlification inside mata) by residual ones.

Depends on VeriFIT/mata#520

jurajsic · 2025-04-16T06:22:39Z

Results where

618ac8b is simulation,
7c5ae10 is simulation+trimming (as simulation can return untrimmed automaton),
7d9721a is residual_with, and
7d59741 is residual_after.
Everything was run using forward direction.

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌      time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  --------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a  102927   478   8342.49   0.08   0.01   1.42  63232    39695        143   260        75        0
z3-noodler-7c5ae10-277599a  102927   478   8565.17   0.08   0.01   1.48  63232    39695        143   259        76        0
z3-noodler-7d9721a-277599a  102596   809  11304.82   0.11   0.01   1.78  62918    39678        143   348       318        0
z3-noodler-7d59741-277599a  102584   821  10953.88   0.11   0.01   1.59  62909    39675        143   360       318        0
--------------------------------------------------


Benchmark sygus_qgen
# of formulae: 343
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a   343     0    1.31   0.00   0.00   0.00    343        0          0     0         0        0
z3-noodler-7c5ae10-277599a   343     0    1.27   0.00   0.00   0.00    343        0          0     0         0        0
z3-noodler-7d9721a-277599a   343     0    1.21   0.00   0.00   0.00    343        0          0     0         0        0
z3-noodler-7d59741-277599a   343     0    1.29   0.00   0.00   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-618ac8b-277599a   999     0   29.75   0.03   0.01   0.66    186      813          0     0         0        0
z3-noodler-7c5ae10-277599a   998     1   28.68   0.03   0.01   0.63    185      813          0     0         1        0
z3-noodler-7d9721a-277599a   997     2  106.35   0.11   0.01   2.65    186      811          0     0         2        0
z3-noodler-7d59741-277599a   995     4   93.50   0.09   0.01   2.65    185      810          0     1         3        0
--------------------------------------------------

Benchmark automatark
# of formulae: 15995
--------------------------------------------------
tool                           ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a  15990     5   401.26   0.03   0.00   0.33  10477     5513          0     5         0        0
z3-noodler-7c5ae10-277599a  15990     5   397.00   0.02   0.00   0.33  10477     5513          0     5         0        0
z3-noodler-7d9721a-277599a  15977    18  1126.48   0.07   0.00   2.17  10469     5508          0    18         0        0
z3-noodler-7d59741-277599a  15970    25   592.80   0.04   0.00   0.95  10463     5507          0    25         0        0
--------------------------------------------------

Benchmark stringfuzz
# of formulae: 11618
--------------------------------------------------
tool                           ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a  11617     1   98.39   0.01   0.00   0.16   6355     5262          1     0         0        0
z3-noodler-7c5ae10-277599a  11617     1   99.96   0.01   0.00   0.16   6355     5262          1     0         0        0
z3-noodler-7d9721a-277599a  11617     1   91.24   0.01   0.00   0.15   6355     5262          1     0         0        0
z3-noodler-7d59741-277599a  11617     1   87.99   0.01   0.00   0.16   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-618ac8b-277599a  3285     2  1904.50   0.58   0.01   3.23   2445      840          0     2         0        0
z3-noodler-7c5ae10-277599a  3285     2  1896.31   0.58   0.01   3.16   2445      840          0     2         0        0
z3-noodler-7d9721a-277599a  3285     2  3336.82   1.02   0.01   4.08   2445      840          0     2         0        0
z3-noodler-7d59741-277599a  3284     3  3475.10   1.06   0.02   4.46   2444      840          0     3         0        0
--------------------------------------------------

Benchmark norn
# of formulae: 1027
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a  1027     0    4.45   0.00   0.00   0.01    712      315          0     0         0        0
z3-noodler-7c5ae10-277599a  1027     0    4.90   0.00   0.00   0.01    712      315          0     0         0        0
z3-noodler-7d9721a-277599a  1027     0    4.58   0.00   0.00   0.01    717      310          0     0         0        0
z3-noodler-7d59741-277599a  1027     0    4.21   0.00   0.00   0.01    717      310          0     0         0        0
--------------------------------------------------

Benchmark slog
# of formulae: 1976
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a  1976     0    8.77   0.00   0.00   0.02    808     1168          0     0         0        0
z3-noodler-7c5ae10-277599a  1976     0    9.04   0.00   0.00   0.02    808     1168          0     0         0        0
z3-noodler-7d9721a-277599a  1974     2   63.38   0.03   0.00   0.51    806     1168          0     0         2        0
z3-noodler-7d59741-277599a  1974     2   92.65   0.05   0.00   0.63    806     1168          0     0         2        0
--------------------------------------------------

Benchmark slent
# of formulae: 1128
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a  1128     0   21.61   0.02   0.00   0.24    630      498          0     0         0        0
z3-noodler-7c5ae10-277599a  1128     0   21.84   0.02   0.00   0.25    630      498          0     0         0        0
z3-noodler-7d9721a-277599a  1126     2   64.14   0.06   0.00   1.09    631      495          0     2         0        0
z3-noodler-7d59741-277599a  1125     3   32.55   0.03   0.00   0.36    630      495          0     3         0        0
--------------------------------------------------

Benchmark omark
# of formulae: 17
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a     9     8    0.07   0.01   0.00   0.01      2        7          0     6         2        0
z3-noodler-7c5ae10-277599a     9     8    0.07   0.01   0.00   0.01      2        7          0     6         2        0
z3-noodler-7d9721a-277599a     9     8    0.11   0.01   0.01   0.02      2        7          0     6         2        0
z3-noodler-7d59741-277599a     9     8    0.09   0.01   0.01   0.02      2        7          0     7         1        0
--------------------------------------------------

Benchmark kepler
# of formulae: 587
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a   584     3   10.13   0.02   0.01   0.06    284      300          0     1         2        0
z3-noodler-7c5ae10-277599a   584     3    9.69   0.02   0.00   0.06    284      300          0     1         2        0
z3-noodler-7d9721a-277599a   584     3    9.72   0.02   0.00   0.06    284      300          0     1         2        0
z3-noodler-7d59741-277599a   584     3    9.80   0.02   0.01   0.06    284      300          0     1         2        0
--------------------------------------------------

Benchmark woorpje
# of formulae: 809
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a   774    35  245.00   0.32   0.01   3.34    614      160          0    14        21        0
z3-noodler-7c5ae10-277599a   774    35  244.28   0.32   0.01   3.34    614      160          0    15        20        0
z3-noodler-7d9721a-277599a   771    38  287.57   0.37   0.01   3.66    611      160          0    13        25        0
z3-noodler-7d59741-277599a   771    38  329.38   0.43   0.01   4.08    611      160          0    12        26        0
--------------------------------------------------

Benchmark webapp
# of formulae: 681
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a   663    18  420.04   0.63   0.01   6.12    234      429          1    16         1        0
z3-noodler-7c5ae10-277599a   663    18  417.76   0.63   0.01   6.19    234      429          1    16         1        0
z3-noodler-7d9721a-277599a   648    33  532.51   0.82   0.01   7.33    221      427          1    22        10        0
z3-noodler-7d59741-277599a   647    34  441.26   0.68   0.01   5.32    221      426          1    23        10        0
--------------------------------------------------

Benchmark kaluza
# of formulae: 19432
--------------------------------------------------
tool                           ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a  19369    63  112.46   0.01   0.00   0.05  16277     3092         20    34         9        0
z3-noodler-7c5ae10-277599a  19369    63  114.53   0.01   0.00   0.05  16277     3092         20    34         9        0
z3-noodler-7d9721a-277599a  19307   125   88.99   0.00   0.00   0.02  16215     3092         20    50        55        0
z3-noodler-7d59741-277599a  19307   125   87.77   0.00   0.00   0.04  16215     3092         20    50        55        0
--------------------------------------------------

Benchmark transducer_plus
# of formulae: 91
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a    22    69  359.56  16.34   1.08  34.47     20        2          0    63         6        0
z3-noodler-7c5ae10-277599a    22    69  357.36  16.24   1.10  34.85     20        2          0    62         7        0
z3-noodler-7d9721a-277599a    20    71  111.79   5.59   0.35  15.18     18        2          0    63         8        0
z3-noodler-7d59741-277599a    20    71  112.04   5.60   0.36  15.33     18        2          0    63         8        0
--------------------------------------------------

Benchmark leetcode
# of formulae: 2652
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a  2651     1   24.59   0.01   0.00   0.05    867     1784          0     0         1        0
z3-noodler-7c5ae10-277599a  2651     1   25.03   0.01   0.00   0.05    867     1784          0     0         1        0
z3-noodler-7d9721a-277599a  2651     1   21.37   0.01   0.00   0.01    867     1784          0     0         1        0
z3-noodler-7d59741-277599a  2651     1   20.64   0.01   0.00   0.01    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-618ac8b-277599a  1823    57  190.90   0.10   0.00   1.10      4     1819          4    22        31        0
z3-noodler-7c5ae10-277599a  1823    57  195.94   0.11   0.00   1.12      4     1819          4    22        31        0
z3-noodler-7d9721a-277599a  1823    57  219.25   0.12   0.00   1.15      4     1819          4    22        31        0
z3-noodler-7d59741-277599a  1823    57  223.68   0.12   0.00   1.19      4     1819          4    23        30        0
--------------------------------------------------

Benchmark pyex
# of formulae: 23845
--------------------------------------------------
tool                           ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a  23779    66  3505.75   0.15   0.07   1.78  20407     3372          0    64         2        0
z3-noodler-7c5ae10-277599a  23780    65  3731.31   0.16   0.07   1.99  20408     3372          0    63         2        0
z3-noodler-7d9721a-277599a  23551   294  4452.57   0.19   0.06   2.19  20179     3372          0   115       179        0
z3-noodler-7d59741-277599a  23551   294  4556.43   0.19   0.06   2.17  20179     3372          0   115       179        0
--------------------------------------------------

Benchmark full_str_int
# of formulae: 16968
--------------------------------------------------
tool                           ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a  16818   150  1003.77   0.06   0.00   1.26   2497    14321        117    33         0        0
z3-noodler-7c5ae10-277599a  16818   150  1010.03   0.06   0.01   1.25   2497    14321        117    33         0        0
z3-noodler-7d9721a-277599a  16816   152   786.56   0.05   0.00   1.04   2495    14321        117    34         1        0
z3-noodler-7d59741-277599a  16816   152   792.54   0.05   0.00   1.05   2495    14321        117    34         1        0
--------------------------------------------------

Benchmark snia
# of formulae: 70
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-618ac8b-277599a    70     0    0.18   0.00   0.00   0.00     70        0          0     0         0        0
z3-noodler-7c5ae10-277599a    70     0    0.17   0.00   0.00   0.00     70        0          0     0         0        0
z3-noodler-7d9721a-277599a    70     0    0.18   0.00   0.00   0.00     70        0          0     0         0        0
z3-noodler-7d59741-277599a    70     0    0.16   0.00   0.00   0.00     70        0          0     0         0        0
--------------------------------------------------

Simulation vs other three:

Residual_with vs residual_after:

Also, both residual versions give incorrect results (i.e. both simulation versions and both cvc5 an z3 gives different result than residual versions) for:

  | benchmark | benchmark-group | name | z3-noodler-618ac8b-277599a-result | z3-noodler-618ac8b-277599a-runtime | z3-noodler-7c5ae10-277599a-result | z3-noodler-7c5ae10-277599a-runtime | z3-noodler-7d9721a-277599a-result | z3-noodler-7d9721a-277599a-runtime | z3-noodler-7d59741-277599a-result | z3-noodler-7d59741-277599a-runtime | cvc5-1.2.0-result | cvc5-1.2.0-runtime | z3-4.13.4-result | z3-4.13.4-runtime | benchmark_group
-- | -- | -- | -- | -- | -- | -- | -- | -- | -- | -- | -- | -- | -- | -- | -- | --
32618 | norn | equations | ../formulae/QF_SLIA/2015-Norn/HammingDistance/norn-benchmark-710.smt2 | unsat | 0.01 | unsat | 0.01 | sat | 0.01 | sat | 0 | unsat | 0.03 | unsat | 0.01 | equations
32733 | norn | equations | ../formulae/QF_SLIA/2015-Norn/HammingDistance/norn-benchmark-876.smt2 | unsat | 0.01 | unsat | 0.01 | sat | 0 | sat | 0.01 | unsat | 0.05 | unsat | 0.02 | equations
33176 | norn | equations | ../formulae/QF_SLIA/2015-Norn/StringReplace/norn-benchmark-49.smt2 | unsat | 0.01 | unsat | 0 | sat | 0 | sat | 0 | unsat | 0 | unsat | 0 | equations
33215 | norn | equations | ../formulae/QF_SLIA/2015-Norn/StringReplace/norn-benchmark-54.smt2 | unsat | 0 | unsat | 0.01 | sat | 0 | sat | 0.01 | unsat | 0 | unsat | 0 | equations
33255 | norn | equations | ../formulae/QF_SLIA/2015-Norn/ChunkSplit/norn-benchmark-12.smt2 | unsat | 0 | unsat | 0 | sat | 0 | sat | 0.01 | unsat | 0 | unsat | 0 | equations
36010 | slent | equations | ../formulae/QF_SLIA/2019-Jiang/slent/slent_stranger_str_rep_3049_sink.smt2 | unsat | 0.02 | unsat | 0.02 | sat | 0.01 | sat | 0.01 | unsat | 0.01 | unsat | 0.26 | equations
36060 | slent | equations | ../formulae/QF_SLIA/2019-Jiang/slent/slent_stranger_str_rep_2992_sink.smt2 | unsat | 0.02 | unsat | 0.02 | sat | 0.01 | sat | 0.01 | unsat | 0.01 | unsat | 0.36 | equations
38254 | webapp | equations | ../formulae/QF_SLIA/20230403-webapp/str-rep/str_replace205.smt2 | unsat | 0.02 | unsat | 0.03 | sat | 0.01 | sat | 0.01 | unsat | 0.01 | unsat | 0.24 | equations
38410 | webapp | equations | ../formulae/QF_SLIA/20230403-webapp/str-rep/str_replace188.smt2 | unsat | 0.02 | unsat | 0.02 | sat | 0.01 | sat | 0.01 | unsat | 0.02 | unsat | 0.34 | equations

jurajsic · 2025-04-16T18:33:29Z

The incorrect results were fixed by #219

jurajsic added 5 commits April 15, 2025 15:53

add option to select reduction algorithm

973d607

add constant to select reduction algorithm

7c5ae10

change to residual_with reduction

7d9721a

change to residual_after reduction

7d59741

remove trimming after simulation

618ac8b

add traces

0012542

jurajsic force-pushed the try_residual_reduction branch from 7ea880b to 0012542 Compare April 16, 2025 17:52

jurajsic force-pushed the try_residual_reduction branch from c6c57ea to 0012542 Compare April 18, 2025 08:18

jurajsic force-pushed the try_residual_reduction branch from c05fbde to 0012542 Compare April 30, 2025 08:40

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add option to select reduction algorithm#218

Add option to select reduction algorithm#218
jurajsic wants to merge 6 commits intodevelfrom
try_residual_reduction

jurajsic commented Apr 15, 2025 •

edited

Loading

Uh oh!

jurajsic commented Apr 16, 2025 •

edited

Loading

Uh oh!

jurajsic commented Apr 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

jurajsic commented Apr 15, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jurajsic commented Apr 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jurajsic commented Apr 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

jurajsic commented Apr 15, 2025 •

edited

Loading

jurajsic commented Apr 16, 2025 •

edited

Loading