mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-17 18:43:45 +00:00
Code Activity

Add comments for regex enhancements in seq_model

Browse source 
Added comments regarding future improvements for regex handling.
This commit is contained in:
Nikolaj Bjorner 2026-03-14 10:26:50 -07:00 • committed by GitHub
parent 1437ec25ce
commit ba7b0392fe
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/seq/seq_model.cpp
View file

@ -272,6 +272,9 @@ namespace smt {
return e ? expr_ref(e, m) : expr_ref(m);
}
// NSB review: replace this by seq_rewriter::some_string_in_re when it is a regex over strings.
// add a routine that works for regular expressions over types other than strings to seq_rewriter
// use this for regexes over non-strings.
expr_ref seq_model::generate_regex_witness(euf::snode* regex, unsigned depth) {
if (!regex)
return expr_ref(m_seq.str.mk_empty(m_seq.str.mk_string_sort()), m);