Support for (limited) model generation - Githubissues

VeriFIT / z3-noodler

The Z3-Noodler String Solver

Other

6 stars 5 forks source link

Support for (limited) model generation #149

Closed jurajsic closed 2 months ago

jurajsic commented 3 months ago

This PR adds suppport for (limited) model generation. More specifically, I added some limited support for model generation

in multiple membership heuristic (limited to cases when we do not have complement)
in main decision procedure (limited to only acyclic cases)

What still is needed to do

handle one membership heuristic, where we need to implement getting a word from regex (with possible complement) and also getting a word from complement of an automaton without constructing the automaton
in multiple membership heuristic, we need to implement getting a word from language difference of two automata without computing the full difference
Nielsen is completely missing

I did not try any proper experiments with models yet, just some random formulae, and it seems it works correctly (when it finishes). I would still merge it for now, and do experiments later, we need to build an infrastructure for them.

I also moved some ad-hoc code related with membership heuristics into their own decision procedures.

jurajsic commented 2 months ago

The impact of changes with model generation turned off:

# of formulae: 103318
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-aa883d5-d95fe13  102260  1058   10436.98   0.10   0.01   1.36  62836    39424        625   376        57        0
z3-noodler-af1b8c8-d95fe13  102270  1048   10940.20   0.11   0.02   1.54  62844    39426        625   373        50        0
cvc5-1.1.2                   99699  3619   76478.24   0.77   0.00   6.77  60798    38901          2  3608         9        0
z3-4.13.0                    97687  5631  132036.99   1.35   0.01   8.11  58874    38813        210  4960       461        0
--------------------------------------------------

jurajsic commented 2 months ago

After mergin with current devel (#153 was missing from here)

# of formulae: 103388
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-88a35a2-d95fe13  102313  1075   11499.55   0.11   0.02   1.54  63045    39268        620   337       118        0

jurajsic commented 2 months ago

Hmm, there are some incorrect results, I have to fix it.

jurajsic commented 2 months ago

It works correctly now, the final results (comparing with devel):

# of formulae: 103388
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-07ed037-d95fe13  102334  1054   12165.82   0.12   0.02   1.67  62911    39423        625   373        56        0
z3-noodler-dad2133-d95fe13  102336  1052   12124.70   0.12   0.02   1.67  62906    39430        625   369        58        0
cvc5-1.1.2                   99769  3619   76478.24   0.77   0.00   6.77  60868    38901          2  3608         9        0
z3-4.13.0                    97687  5701  132036.99   1.35   0.01   8.11  58874    38813        210  4960       461       70
--------------------------------------------------

jurajsic commented 2 months ago

I will have to run it again, I made some significant changes.

jurajsic commented 2 months ago

Results:

# of formulae: 103388
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-a8ca33a-d95fe13  102329  1059   12090.78   0.12   0.02   1.67  62905    39424        625   383        51        0
z3-noodler-dad2133-d95fe13  102336  1052   12124.70   0.12   0.02   1.67  62906    39430        625   369        58        0
cvc5-1.1.2                   99769  3619   76478.24   0.77   0.00   6.77  60868    38901          2  3608         9        0
z3-4.13.0                    97687  5701  132036.99   1.35   0.01   8.11  58874    38813        210  4960       461       70
--------------------------------------------------

Seems it is fine, so I will merge.