Less underapproximating int conversions

[jurajsic]

Added some from_int/to_int axioms that should help reducing the need for underapproximation in LIA encoding of int conversions. Also added command line argument underapprox_length by which we can make underapproximation more precise (if it is larger, it can be more precise). It denotes the maximum length of digit words that are handled (i.e. for 5 this means 99999 is the maximum number that conversions can handle - but only if they are not finite already).

[jurajsic]

On benchmarks with to_int/from_int (and only those formulae):

Benchmark stringfuzz/to120.csv
# of formulae: 1608
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-1a3c655-2cddb2f  1604     4   0.05   0.01   79.53    284     1320          4     0         0        0
cvc5-1.0.8                  1579    29   0.04   0.03   67.37    284     1295          0    29         0        0
z3-4.12.2                   1562    46   0.11   0.03  171.25    285     1277          0    46         0        0
cvc5-1.1.1                  1579    29   0.01   0.01   23.65    284     1295          0    29         0        0
z3-4.12.5                   1565    43   0.20   0.01  307.99    286     1279          0    43         0        0
z3-noodler-bee36a1-2cddb2f  1604     4   0.10   0.01  158.88    284     1320          4     0         0        0
--------------------------------------------------

Benchmark str_small_rw/to120.csv
# of formulae: 80
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-1a3c655-2cddb2f    73     7   0.01   0.01    0.78      0       73          2     5         0        0
cvc5-1.0.8                    78     2   0.01   0.01    0.71      1       77          2     0         0        0
z3-4.12.2                     78     2   0.03   0.03    2.20      1       77          0     2         0        0
cvc5-1.1.1                    78     2   0.00   0.00    0.02      1       77          2     0         0        0
z3-4.12.5                     78     2   0.01   0.01    0.72      1       77          0     2         0        0
z3-noodler-bee36a1-2cddb2f    74     6   0.01   0.01    1.00      1       73          2     4         0        0
--------------------------------------------------

Benchmark full_str_int/to120.csv
# of formulae: 16130
--------------------------------------------------
tool                           ✅    ❌    avg    med      time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -----  -----  --------  -----  -------  ---------  ----  --------  -------
z3-noodler-1a3c655-2cddb2f  15422   708   0.18   0.01   2707.03   1809    13613        582   126         0        0
cvc5-1.0.8                  16130     0   0.32   0.03   5194.88   2342    13788          0     0         0        0
z3-4.12.2                   15900   230   1.51   0.04  24070.16   2298    13602          0   230         0        0
cvc5-1.1.1                  16125     5   0.29   0.01   4614.45   2338    13787          0     5         0        0
z3-4.12.5                   15894   236   1.27   0.01  20225.67   2292    13602          0   236         0        0
z3-noodler-bee36a1-2cddb2f  15213   917   0.20   0.01   2966.71   1776    13437        808   109         0        0
--------------------------------------------------

For str_small_rw, the one SAT that is now TO is weird, on mac it still gives SAT. Other TOs are problems with loop protection, it gets stuck.

[jurajsic]

And graphs for these benchmarks (again, restricted to only formulae containing to_int/from_int):

[jurajsic]

I fixed a small bug (which didn't show up in the results), the current results are then:

Benchmark stringfuzz/to120.csv
# of formulae: 1608
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-005708c-2cddb2f  1603     5   0.04   0.01   58.76    283     1320          5     0         0        0
cvc5-1.0.8                  1579    29   0.04   0.03   67.37    284     1295          0    29         0        0
z3-4.12.2                   1562    46   0.11   0.03  171.25    285     1277          0    46         0        0
cvc5-1.1.1                  1579    29   0.01   0.01   23.65    284     1295          0    29         0        0
z3-4.12.5                   1565    43   0.20   0.01  307.99    286     1279          0    43         0        0
z3-noodler-bee36a1-2cddb2f  1604     4   0.10   0.01  158.88    284     1320          4     0         0        0
--------------------------------------------------

Benchmark str_small_rw/to120.csv
# of formulae: 80
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-005708c-2cddb2f    73     7   0.01   0.01    0.74      0       73          2     4         1        0
cvc5-1.0.8                    78     2   0.01   0.01    0.71      1       77          2     0         0        0
z3-4.12.2                     78     2   0.03   0.03    2.20      1       77          0     2         0        0
cvc5-1.1.1                    78     2   0.00   0.00    0.02      1       77          2     0         0        0
z3-4.12.5                     78     2   0.01   0.01    0.72      1       77          0     2         0        0
z3-noodler-bee36a1-2cddb2f    74     6   0.01   0.01    1.00      1       73          2     4         0        0
--------------------------------------------------

Benchmark full_str_int/to120.csv
# of formulae: 16130
--------------------------------------------------
tool                           ✅    ❌    avg    med      time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -----  -----  --------  -----  -------  ---------  ----  --------  -------
z3-noodler-005708c-2cddb2f  15436   694   0.21   0.01   3287.43   1823    13613        578   116         0        0
cvc5-1.0.8                  16130     0   0.32   0.03   5194.88   2342    13788          0     0         0        0
z3-4.12.2                   15900   230   1.51   0.04  24070.16   2298    13602          0   230         0        0
cvc5-1.1.1                  16125     5   0.29   0.01   4614.45   2338    13787          0     5         0        0
z3-4.12.5                   15894   236   1.27   0.01  20225.67   2292    13602          0   236         0        0
z3-noodler-bee36a1-2cddb2f  15213   917   0.20   0.01   2966.71   1776    13437        808   109         0        0
--------------------------------------------------

[jurajsic]

Nice! Approve. Did you measure impact on the other benchmarks? (I don't expect some improvements outside conversions, just to be sure we don't introduce some regression).

Yes I did, there was minimum impact.