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.

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

z3str3: remove legacy code #4215

Merged

Conversation

mtrberzi
Copy link
Collaborator

@mtrberzi mtrberzi commented May 5, 2020

This patch removes a large amount of legacy code from theory_str, including:

  • length/value testing (replaced by fixed length model construction)
  • binary search heuristic for length/value testing
  • regex unroll (replaced by automata-based regex reasoning)
  • fixed-length overlap testing (this was never even implemented completely)

This code has been superseded by newer modules with better performance and is prone to errors. It also won't be maintained going forward. All of the associated code has been disabled by default for a very long time and enabling it isn't the recommended way to invoke Z3str3.

parameter smt.str.fixed_length_overlap_models has been deprecated
…h heuristic

the following parameters are deprecated:
smt.str.use_binary_search
smt.str.binary_search_start
smt.str.fixed_length_models (the fixed-length model construction is now always used)
@mtrberzi
Copy link
Collaborator Author

mtrberzi commented May 5, 2020

As a result of this patch, the following parameters are deprecated:

  • smt.str.use_binary_search and smt.str.binary_search_start (the associated methods have been removed)
  • smt.str.finite_overlap_models (the associated methods have been removed)
  • smt.str.regex_automata (automata-based regex reasoning is now always used)
  • smt.str.fixed_length_models (fixed-length model construction is now always used)

@NikolajBjorner NikolajBjorner merged commit 1f15033 into Z3Prover:master May 6, 2020
@mtrberzi mtrberzi deleted the remove-legacy-len-val-testing branch May 6, 2020 21:03
hgvk94 pushed a commit to hgvk94/z3 that referenced this pull request May 7, 2020
* z3str3: remove legacy fixed-length overlap testing

parameter smt.str.fixed_length_overlap_models has been deprecated

* z3str3: remove legacy length/value testing algorithm and binary search heuristic

the following parameters are deprecated:
smt.str.use_binary_search
smt.str.binary_search_start
smt.str.fixed_length_models (the fixed-length model construction is now always used)

* z3str3: remove legacy regex unroll methods

* z3str3: remove unused methods and member variables
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants