Not contains via counter automata

vhavlena commented 3 months ago

This PR introduces kind a lot of new stuff

extension of DecisionProcedure to handle disequations and not(contains) after a stable solution is found
Implementation of Tag-based solving of a single diseqation and first step towards handling a single not(contains). This can be turned on by smt.str.ca_constr=true (by default it is off)
extension of FormulaPreprocessor to handle not(contains) predicates as well
quite nice things around Parikh image: at least there is a procedure creating Parikh image formula for an NFA. It might be useful for the future
bug fixes in axiomatization a preprocessing

vhavlena commented 2 months ago

The results before the last rebase were fine. I am running the experiments after rebase now.

vhavlena commented 2 months ago

The results

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-146dbc0-d95fe13  102391  1014   11437.14   0.11   0.02   1.50  62907    39484        537   409        68        0
z3-noodler-a8ca33a-d95fe13  102338  1067   12090.90   0.12   0.02   1.67  62907    39431        625   389        53        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                    97694  5711  132044.66   1.35   0.01   8.11  58876    38818        210  4968       463       70
--------------------------------------------------

vhavlena commented 2 months ago

Main difference to the devel:

Benchmark str_small_rw
# of formulae: 1880
--------------------------------------------------
tool                          ✅    ❌    time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  ------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-146dbc0-d95fe13  1816    64  343.62   0.19   0.01   2.86      4     1812          4    37        23        0
z3-noodler-a8ca33a-d95fe13  1762   118  365.65   0.21   0.01   2.74      4     1758         92    17         9        0
cvc5-1.1.2                  1861    19   31.09   0.02   0.00   0.56     20     1841          2    17         0        0
z3-4.13.0                   1821    59  214.88   0.12   0.01   2.86     25     1796          0    59         0        0
--------------------------------------------------

vhavlena commented 2 months ago

I have checked the notcontains bug and it is indeed solved by handling notcontains inside the preprocessor (there is a rule requiring that a variable has no other occurrences and it did not take into account variables in notcontains).

jurajsic commented 2 months ago

I have checked the notcontains bug and it is indeed solved by handling notcontains inside the preprocessor (there is a rule requiring that a variable has no other occurrences and it did not take into account variables in notcontains).

Should that rule be fixed then? It should check for the variables in not contains. Or at least add a note that it does not check not contains.

vhavlena commented 2 months ago

I have checked the notcontains bug and it is indeed solved by handling notcontains inside the preprocessor (there is a rule requiring that a variable has no other occurrences and it did not take into account variables in notcontains).

Should that rule be fixed then? It should check for the variables in not contains. Or at least add a note that it does not check not contains.

It's ok. The Preprocessor now takes into account all variables in the system including those in notcontains.

jurajsic commented 2 months ago

I have checked the notcontains bug and it is indeed solved by handling notcontains inside the preprocessor (there is a rule requiring that a variable has no other occurrences and it did not take into account variables in notcontains).

Should that rule be fixed then? It should check for the variables in not contains. Or at least add a note that it does not check not contains.

It's ok. The Preprocessor now takes into account all variables in the system including those in notcontains.

Ah ok, I get it now, this PR fixed it.

VeriFIT / z3-noodler

Not contains via counter automata #150