3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-02 12:13:25 +00:00

add notes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-31 13:59:27 -07:00
parent 80a7504686
commit 568218e1ed

View file

@ -23,6 +23,8 @@ TODOs:
- if perf suffers: use DFS backtracking search instead of DNF expansion (space overhead)
- create a validation harness: expose certificates for correctness that can be checked.
- extend with lower and upper bound constraints
- cache calls to cofactors so they are only computed once per regex.
- consider using expr_ref as alternative to pinned expressions
- encapsulate within general interface:
create: undo_trail x dependency_manager x ast_manager -> regex_membership
add_constraint : expr* x expr* x dependency* -> void