mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-03 22:06:11 +00:00
Code Activity

have it create string ranges

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-25 20:26:35 -07:00
parent f614721a92
commit baeaa84bde
1 changed files with 4 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/ast/rewriter/seq_rewriter.cpp
View file

@ -4132,12 +4132,8 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
if (max_length(hi) == std::make_pair(true, rational(0))) if (max_length(hi) == std::make_pair(true, rational(0)))
is_empty = true; is_empty = true;
if (!is_empty) { if (!is_empty) {
if (str().is_string(lo, slo)) { if (str().is_string(lo, slo) && slo.length() == 1)
if (slo.length() != 1) clo = slo[0];
is_empty = true;
else
clo = slo[0];
}
else if (str().is_unit(lo, lo1) && m_util.is_const_char(lo1, clo)) else if (str().is_unit(lo, lo1) && m_util.is_const_char(lo1, clo))
; ;
else else
@ -4159,8 +4155,9 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
if (clo > chi) if (clo > chi)
is_empty = true; is_empty = true;
// Singleton: re.range "a" "a" → str.to_re "a" // Singleton: re.range "a" "a" → str.to_re "a"
verbose_stream() << "mk_re_range: " << clo << " " << chi << " is_empty: " << is_empty << "\n";
if (clo == chi) { if (clo == chi) {
result = re().mk_to_re(str().mk_string(slo)); result = re().mk_to_re(str().mk_string(zstring(clo)));
return BR_DONE; return BR_DONE;
} }