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

Pyex: optimizations #104

Merged
merged 22 commits into from
Dec 20, 2023
Merged

Pyex: optimizations #104

merged 22 commits into from
Dec 20, 2023

Conversation

vhavlena
Copy link
Collaborator

@vhavlena vhavlena commented Oct 28, 2023 •
edited
Loading

This PR introduces several heuristics and optimisations:

  • enlarging not(contains) fragment by checking syntactic subsumption over string terms
  • theory rewrite during mk_literal
  • specialisations of various predicates/function (contains, not(prefix), not(suffix), replace)
  • new preprocessing: alignment inference and leveraging generate equivalent
  • minor changes in seq_rewrite to avoid seq.unit during solving

@vhavlena vhavlena marked this pull request as ready for review December 7, 2023 07:16
@vhavlena
Copy link
Collaborator Author

vhavlena commented Dec 7, 2023

image

Results on all benchmarks (current version is below in the plot). Several notes:

  • quite significant improvement on pyex and str_small_rw
  • on par/slightly better with other benchmarks except kaluza. On kaluza we have now about 250 timeouts more. I have checked the formulae and they are difficult. For instance, a change of order of the noodle processing or some little change in preprocessing might caused the issue. When I played with that reduction of noodles as proposed in another PR might solve some of the cases. So I would take it as it is now.
  • Our results match with the results of cvc5 except str-pred-small-rw/str-pred-small-rw_486.smt2 and str-pred-small-rw/str-pred-small-rw_392.smt2 (we say unsat, cvc5 says sat). I think they are unsat (ostrich returns unsat too, but it is not reliable much)
| method                     |    max |      mean |   median |   std. dev |   TO+MO+ERR |   unknowns |
|----------------------------|--------|-----------|----------|------------|-------------|------------|
| z3-noodler-1482571-a57f582 | 115.42 |  0.463528 |     0.02 |    3.42857 |        2465 |       2098 |
| cvc5-1.0.8                 | 119.36 |  0.515113 |     0.02 |    5.2351  |        1723 |          2 |
| z3-4.12.2                  | 119.29 |  1.49018  |     0.04 |    8.17615 |        2623 |        123 |
| z3str4                     | 118.44 |  0.608656 |     0.02 |    4.12256 |        1285 |        392 |
| ostrich-70d01e2d2          | 912.88 | 13.1827   |     2.45 |   39.3352  |       13797 |          1 |
| z3strRE                    | 119.59 |  0.247021 |     0.01 |    3.03464 |        1177 |      18558 |
| z3-noodler-f211b89-bb85433 | 119.79 |  0.96354  |     0.03 |    6.76557 |        4334 |       2914 |

@vhavlena vhavlena requested review from jurajsic and Adda0 December 7, 2023 14:42
@vhavlena vhavlena mentioned this pull request Dec 7, 2023
Merged
Adda0
Adda0 reviewed Dec 8, 2023
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.

This is a way too large a PR with way too many random heuristics for me to review consistently.

There are multiple smaller and larger heuristics. It may be hard to see the impact of each single heuristic alone, however. According to the results, they seem to work together well enough.

From what I have seen, the PR seems OK. I have not noticed any obvious issues with the PR.

src/ast/rewriter/seq_rewriter.cpp Outdated Show resolved Hide resolved
src/smt/theory_str_noodler/decision_procedure.cpp 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 Show resolved Hide resolved
src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp Show resolved Hide resolved
src/smt/theory_str_noodler/formula_preprocess.cpp Outdated Show resolved Hide resolved
src/smt/theory_str_noodler/formula_preprocess.cpp Outdated Show resolved Hide resolved
jurajsic
jurajsic approved these changes Dec 19, 2023
View reviewed changes
Copy link
Member

@jurajsic jurajsic left a comment

Choose a reason for hiding this comment

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

I only skimmed the new preprocessing functions, otherwise looks good.

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.h Outdated Show resolved Hide resolved
src/smt/theory_str_noodler/decision_procedure.h Show resolved Hide resolved
src/smt/theory_str_noodler/formula.h Outdated Show resolved Hide resolved
@jurajsic
Copy link
Member

We should probably check some formulae from kaluza in more detail, i.e. check the traces of old and this version for some instances and see what is happening.

Adda0
Adda0 approved these changes Dec 20, 2023
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.

The PR looks good to me.

When the remaining unresolved discussions are resolved, I am OK with merging the PR.

@vhavlena
Copy link
Collaborator Author

We should probably check some formulae from kaluza in more detail, i.e. check the traces of old and this version for some instances and see what is happening.

I have checked some instances. It seems that it is caused by (i) a soundness fix of some optimisation, and/or (ii) by a different order of preprocessing rules (we might get slightly different automata and equations than those in devel). If it is indeed (i), I hope I will be able to improve it (have an idea), but I leave it for another PR.

@vhavlena vhavlena merged commit 9911283 into devel Dec 20, 2023
@vhavlena vhavlena deleted the pyex-opt branch December 20, 2023 14:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Adda0 Adda0 Adda0 approved these changes

@jurajsic jurajsic jurajsic 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.
3 participants
@vhavlena @jurajsic @Adda0