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

Handling of from_int and to_int #114

Merged
merged 12 commits into from
Jan 29, 2024
Merged

Handling of from_int and to_int #114

merged 12 commits into from
Jan 29, 2024

Conversation

jurajsic
Copy link
Member

@jurajsic jurajsic commented Jan 18, 2024 •
edited
Loading

Adds a (basic) handling of from_int and to_int.
It should be able to handle cases where they lead to solutions with finite languages in the automata for the string variables used in from_int and to_int.
I had to also rewrite the way to_code/from_code was handled.

@jurajsic jurajsic changed the title from_int and to_int Handling of from_int and to_int Jan 25, 2024
@jurajsic
Copy link
Member Author

jurajsic commented Jan 25, 2024 •
edited
Loading

The results for the three benchmarks that contain to_int/from_int.

Benchmark stringfuzz/to120.csv
# of formulae: 11618
--------------------------------------------------
tool                           ✅    ❌    avg    med      time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -----  -----  --------  -----  -------  ---------  ----  --------  -------
z3-noodler-147a0e0-fb6e2b1  10574  1044   0.02   0.01    264.03   6087     4487       1044     0         0        0
cvc5-1.0.8                  10552  1066   2.61   0.02  27503.53   5777     4775          0  1065         1        0
z3-4.12.2                   11232   386   4.14   0.04  46483.27   6148     5084          0   367        19        0
z3-noodler-8de5f2c-387babd  10051  1567   0.03   0.01    264.13   6071     3980       1567     0         0        0
--------------------------------------------------

Benchmark str_small_rw/to120.csv
# of formulae: 1880
--------------------------------------------------
tool                          ✅    ❌    avg    med    time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ----  ----  -----  -----  ------  -----  -------  ---------  ----  --------  -------
z3-noodler-147a0e0-fb6e2b1  1734   146   0.22   0.01  381.20      4     1730        111    20        15        0
cvc5-1.0.8                  1861    19   0.03   0.01   48.26     22     1839          2    17         0        0
z3-4.12.2                   1817    63   0.06   0.03  112.09     25     1792          0    63         0        0
z3-noodler-8de5f2c-387babd  1721   159   0.18   0.01  312.72      4     1717        126    19        14        0
--------------------------------------------------

Benchmark full_str_int/to120.csv
# of formulae: 16968
--------------------------------------------------
tool                           ✅    ❌    avg    med      time    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  -----  ----  -----  -----  --------  -----  -------  ---------  ----  --------  -------
z3-noodler-147a0e0-fb6e2b1  14504  2464   0.10   0.01   1457.78    757    13747       1620   821        23        0
cvc5-1.0.8                  16968     0   0.31   0.03   5258.46   2526    14442          0     0         0        0
z3-4.12.2                   16734   234   1.45   0.04  24231.84   2478    14256          0   234         0        0
z3-noodler-8de5f2c-387babd  11688  5280   0.02   0.01    266.10    177    11511       5273     7         0        0

image
image
image

There was nearly no impact on the other benchmarks (as was expected):

# of formulae: 69565
| method                     |    max |     mean |   median |   std. dev |   TO+MO+ERR |   unknowns |
|----------------------------|--------|----------|----------|------------|-------------|------------|
| z3-noodler-147a0e0-fb6e2b1 | 113.35 | 0.136684 |     0.02 |    1.86548 |         508 |        410 |
| z3-noodler-8de5f2c-387babd | 110.41 | 0.134954 |     0.02 |    1.80886 |         509 |        410 |

image

@jurajsic jurajsic marked this pull request as ready for review January 25, 2024 17:06
@jurajsic jurajsic requested review from vhavlena and Adda0 January 25, 2024 17:06
vhavlena
vhavlena approved these changes Jan 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.

Good job. I have just a couple of smaller remarks.

README.md Outdated Show resolved Hide resolved
src/smt/theory_str_noodler/decision_procedure.cpp Outdated Show resolved Hide resolved
src/smt/theory_str_noodler/decision_procedure.cpp Outdated Show resolved Hide resolved
src/smt/theory_str_noodler/decision_procedure.cpp Outdated Show resolved Hide resolved
src/smt/theory_str_noodler/decision_procedure.cpp Outdated Show resolved Hide resolved
src/smt/theory_str_noodler/formula.h Outdated Show resolved Hide resolved
@vhavlena vhavlena linked an issue Jan 26, 2024 that may be closed by this pull request
Add a basic support for to_int/from_int #76
Closed
Adda0
Adda0 approved these changes Jan 29, 2024
View reviewed changes
Copy link
Collaborator

@Adda0 Adda0 left a comment

Choose a reason for hiding this comment

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

Seems good to me. I do not anything else to add.

@jurajsic jurajsic merged commit 50d9014 into devel Jan 29, 2024
@jurajsic jurajsic deleted the to-from-int branch January 29, 2024 19: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

@Adda0 Adda0 Adda0 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.

Add a basic support for to_int/from_int
3 participants
@jurajsic @vhavlena @Adda0