Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Less underapproximating int conversions #125

Merged
merged 6 commits into from
Feb 27, 2024
Merged

Less underapproximating int conversions #125

merged 6 commits into from
Feb 27, 2024

Conversation

jurajsic
Copy link
Member

@jurajsic jurajsic commented Feb 26, 2024 •
edited
Loading

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
Copy link
Member Author

jurajsic commented Feb 26, 2024 •
edited
Loading

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
Copy link
Member Author

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

@jurajsic jurajsic force-pushed the to-from-int-more-precise branch from 1a3c655 to 2111591 Compare February 26, 2024 22:27
@jurajsic jurajsic changed the title To from int more precise Less underapporximating int conversions Feb 26, 2024
@jurajsic jurajsic changed the title Less underapporximating int conversions Less underapproximating int conversions Feb 26, 2024
@jurajsic jurajsic marked this pull request as ready for review February 26, 2024 22:38
@jurajsic jurajsic requested a review from vhavlena February 26, 2024 22:38
@jurajsic
Copy link
Member Author

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
--------------------------------------------------

vhavlena
vhavlena approved these changes Feb 27, 2024
View reviewed changes
Copy link
Collaborator

@vhavlena vhavlena left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

@jurajsic
Copy link
Member Author

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.

@jurajsic jurajsic merged commit a764634 into devel Feb 27, 2024
@jurajsic jurajsic deleted the to-from-int-more-precise branch February 27, 2024 19:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@vhavlena vhavlena vhavlena approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@jurajsic @vhavlena