mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-14 09:45:36 +00:00
Code Activity

Merge remote-tracking branch 'origin/master' into seq-dnf-opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-08-03 10:20:20 -07:00
commit efd168a54f
8 changed files with 201 additions and 68 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.