mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

add missing return

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-07 21:02:02 -08:00
parent 1cb126f3dd
commit c1a62d346c
2 changed files with 10 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/converters/expr_inverter.cpp
View file

@ -882,15 +882,7 @@ public:
return false; return false;
case OP_SEQ_IN_RE: case OP_SEQ_IN_RE:
if (uncnstr(args[0]) && seq.re.is_ground(args[1]) && seq.is_string(args[0]->get_sort())) { if (uncnstr(args[0]) && seq.re.is_ground(args[1]) && seq.is_string(args[0]->get_sort())) {
#if 0 #if 1
//
// requires auxiliary functions
// some_string_in_re.
// A preliminary implementation exists in sls_seq_plugin.cpp
// it should be moved to seq_rewriter and made agnostic to m_chars.
// maybe use backtracking for better covereage: when some_string_in_re
// fails it doesn't necessarily mean that the regex is empty.
//
zstring s1, s2; zstring s1, s2;
expr* re = args[1]; expr* re = args[1];
expr_ref not_re(seq.re.mk_complement(re), m); expr_ref not_re(seq.re.mk_complement(re), m);

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

@ -6153,6 +6153,7 @@ bool seq_rewriter::some_string_in_re(expr* r, zstring& s) {
expr_mark visited; expr_mark visited;
unsigned_vector str; unsigned_vector str;
expr_ref_vector pinned(m()); expr_ref_vector pinned(m());
if (!some_string_in_re(pinned, visited, r, str)) if (!some_string_in_re(pinned, visited, r, str))
return false; return false;
s = zstring(str.size(), str.data()); s = zstring(str.size(), str.data());
@ -6198,29 +6199,29 @@ bool seq_rewriter::append_char(expr_ref_vector& pinned, expr_mark& visited, buff
if (append_char(pinned, visited, exclude, el, str)) if (append_char(pinned, visited, exclude, el, str))
return true; return true;
exclude.pop_back(); exclude.pop_back();
return false;
} }
if (is_ground(r)) { if (is_ground(r)) {
// ensure selected character is not in exclude // ensure selected character is not in exclude
unsigned ch = 'a'; unsigned ch = 'a';
bool at_base = false; bool wrapped = false;
while (true) { while (true) {
bool found = false; bool found = false;
for (auto [l, h] : exclude) { for (auto [l, h] : exclude) {
if (l <= ch && ch <= h) { if (l <= ch && ch <= h) {
found = true; found = true;
ch = h + 1; ch = h + 1;
break;
} }
} }
if (!found) if (!found)
break; break;
if (ch == zstring::unicode_max_char() + 1) { if (ch != zstring::unicode_max_char() + 1)
if (at_base) continue;
if (wrapped)
return false; return false;
ch = 0; ch = 0;
at_base = true; wrapped = true;
}
} }
str.push_back(ch); str.push_back(ch);
if (some_string_in_re(pinned, visited, r, str)) if (some_string_in_re(pinned, visited, r, str))