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

Length based conversion encoding of int conversions #121

Merged
merged 10 commits into from
Feb 26, 2024
Merged

Length based conversion encoding of int conversions #121

merged 10 commits into from
Feb 26, 2024

Conversation

jurajsic
Copy link
Member

@jurajsic jurajsic commented Feb 20, 2024 •
edited
Loading

Instead of creating each case while creating LIA formula encoding int conversions, we now handle them by legnths, so for example if we have
i = to_int(s_1 s_2) with s_1 \in [4-8][0-9][0-9] and s_2 \in [2-3][5-9]
instead of putting i = 40025 || i = 40026 || .... we now create 400 <= s_1^i <= 899, 25 <= s_2^i <= 29 || 35 <= s_2^i <= 39 and i = s_1^i*100 + s_2^i.

@jurajsic jurajsic force-pushed the to-from-int-length-based branch from a73ee4d to 517657f Compare February 21, 2024 14:04
@jurajsic jurajsic force-pushed the to-from-int-length-based branch from f0202c4 to bdc5b2c Compare February 25, 2024 17:37
@jurajsic jurajsic changed the title int conversions are handled in more concise way Length based conversion encoding of int conversions Feb 25, 2024
@jurajsic jurajsic marked this pull request as ready for review February 25, 2024 17:47
@jurajsic
Copy link
Member Author

Preliminary results (without to-int-eq PR) on only the benchmarks containing conversions:

Benchmark stringfuzz/to120.csv
# of formulae: 1608
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-9d9fdac-2cddb2f  1566    42   0.12   0.01  183.21    283     1283         42     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-bdb7f83-2cddb2f  1562    46   0.05   0.01   71.00    279     1283         42     4         0        0
--------------------------------------------------

Benchmark str_small_rw/to120.csv
# of formulae: 80
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-9d9fdac-2cddb2f    74     6   0.01   0.01    1.04      1       73          2     4         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-bdb7f83-2cddb2f    73     7   0.01   0.01    0.74      0       73          2     5         0        0
--------------------------------------------------

Benchmark full_str_int/to120.csv
# of formulae: 16130
--------------------------------------------------
tool                           ✅    ❌    avg    med      time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -----  -----  --------  -----  -------  ---------  ----  --------  -------
z3-noodler-9d9fdac-2cddb2f  14598  1532   0.15   0.01   2209.77   1374    13224       1432   100         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-bdb7f83-2cddb2f  14527  1603   0.23   0.01   3363.23   1303    13224        895   415       293        0
--------------------------------------------------

@jurajsic jurajsic requested a review from vhavlena February 25, 2024 17:51
@jurajsic
Copy link
Member Author

Comparison with current devel on benchmarks with to_int/from_int:

Benchmark stringfuzz/to120.csv
# of formulae: 1608
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-bee36a1-2cddb2f  1604     4   0.10   0.01  158.88    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-bdb7f83-2cddb2f  1562    46   0.05   0.01   71.00    279     1283         42     4         0        0
z3-noodler-a0d4232-2cddb2f  1595    13   0.02   0.01   34.31    275     1320          4     8         1        0
--------------------------------------------------

Benchmark str_small_rw/to120.csv
# of formulae: 80
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-bee36a1-2cddb2f    74     6   0.01   0.01    1.00      1       73          2     4         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-bdb7f83-2cddb2f    73     7   0.01   0.01    0.74      0       73          2     5         0        0
z3-noodler-a0d4232-2cddb2f    73     7   0.01   0.01    0.77      0       73          2     5         0        0
--------------------------------------------------

Benchmark full_str_int/to120.csv
# of formulae: 16130
--------------------------------------------------
tool                           ✅    ❌    avg    med      time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -----  -----  --------  -----  -------  ---------  ----  --------  -------
z3-noodler-bee36a1-2cddb2f  15213   917   0.20   0.01   2966.71   1776    13437        808   109         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-bdb7f83-2cddb2f  14527  1603   0.23   0.01   3363.23   1303    13224        895   415       293        0
z3-noodler-a0d4232-2cddb2f  15104  1026   0.80   0.01  12018.65   1698    13406        266   469       291        0
--------------------------------------------------

@jurajsic
Copy link
Member Author

Comparison with devel but graphs (again, only int conversion benchmarks):

  • first noodler vs noodler:
    image
    image
  • vs cvc5 and z3 (only full_str_int):
    image
    image

vhavlena
vhavlena approved these changes Feb 26, 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 work! I am happy with the optimizations. Just a few comments.

src/smt/theory_str_noodler/aut_assignment.cpp Outdated Show resolved Hide resolved
src/smt/theory_str_noodler/aut_assignment.cpp Outdated Show resolved Hide resolved
src/smt/theory_str_noodler/decision_procedure.cpp Show resolved Hide resolved
@jurajsic
Copy link
Member Author

@vhavlena can I merge it?

@vhavlena
Copy link
Collaborator

Yes, sure

@jurajsic jurajsic merged commit d24016e into devel Feb 26, 2024
@jurajsic jurajsic deleted the to-from-int-length-based branch February 26, 2024 22:04
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