mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-08 06:52:26 +00:00
Code Activity

Update seq_monadic.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-08-03 10:11:15 -07:00 • committed by GitHub
parent 9e7363bd27
commit 2441ae2f30
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/rewriter/seq_monadic.cpp
View file

@ -40,6 +40,11 @@ TODOs:
explored and we can check the variable intersection membership constraints if the new
expansion is feasible. Constant characters are consumed at the same time to also prune
the choice.
- separate out "live-state" and enumerator over reachable live states:
- make it share live states between callers.
- make it expose an iterator instead of using vectors of live states to allow on-demand expansion of live states.
- make use of DFS exploration of derivatives to extract live states without visiting all states up front.
- use it in seq_regex legacy mode that also has this notion.