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

Seq rewriter integration #4599

Merged

Conversation

cdstanford
Copy link
Contributor

(Redoing pull request)

Integrate the new derivative normalization functionality into the sequence rewriter.

The primary changes are:

  • All conditions formed when creating a derivative now go through the mk_der_cond function, which enforces a desired normal form. Currently, it enforces that conditions are rewritten to the form x <= c where c is a character code.

  • In the BDD form, conditions are order by character code whenever possible; otherwise expression ID only as a fallback. So, we redefine get_id in the context of mk_der_op_rec to be c for conditions of the form x <= c.

  • In the BDD form, conditions are then simplified locally: unreachable branches are removed. (This uses the auxiliary function pred_implies)

The result is that for regexes which only involve ranges and raw characters/strings as predicates, the BDD form is linear and all leaves of the BDD are reachable. Finally:

  • Additional tracing under the seq_verbose tag

calebstanford-msr and others added 30 commits June 9, 2020 16:43
(and revert an experimental change where BDDs aren't sorted by get_id)
…mplement separate functionality for expr* logic
@NikolajBjorner NikolajBjorner merged commit 5664b57 into Z3Prover:master Jul 28, 2020
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.

3 participants