mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
9b4cf1559d
commit
52910fa465
|
@ -561,6 +561,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
|
|||
zstring s;
|
||||
rational pos, len;
|
||||
|
||||
TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << " " << mk_pp(c, m()) << "\n";);
|
||||
bool constantBase = m_util.str.is_string(a, s);
|
||||
bool constantPos = m_autil.is_numeral(b, pos);
|
||||
bool constantLen = m_autil.is_numeral(c, len);
|
||||
|
@ -599,6 +600,10 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
|
|||
SASSERT(_len > 0);
|
||||
expr_ref_vector as(m()), bs(m());
|
||||
m_util.str.get_concat(a, as);
|
||||
if (as.empty()) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
for (unsigned i = 0; i < as.size() && _len > 0; ++i) {
|
||||
if (m_util.str.is_unit(as[i].get())) {
|
||||
if (_pos == 0) {
|
||||
|
@ -613,7 +618,12 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
|
|||
return BR_FAILED;
|
||||
}
|
||||
}
|
||||
result = m_util.str.mk_concat(bs);
|
||||
if (bs.empty()) {
|
||||
result = m_util.str.mk_empty(m().get_sort(a));
|
||||
}
|
||||
else {
|
||||
result = m_util.str.mk_concat(bs);
|
||||
}
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
|
|
@ -346,7 +346,8 @@ namespace smt2 {
|
|||
// consume garbage
|
||||
// return true if managed to recover from the error...
|
||||
bool sync_after_error() {
|
||||
while (true) {
|
||||
unsigned num_errors = 0;
|
||||
while (num_errors < 100) {
|
||||
try {
|
||||
while (curr_is_rparen())
|
||||
next();
|
||||
|
@ -374,8 +375,10 @@ namespace smt2 {
|
|||
catch (scanner_exception & ex) {
|
||||
SASSERT(ex.has_pos());
|
||||
error(ex.line(), ex.pos(), ex.msg());
|
||||
++num_errors;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void check_next(scanner::token t, char const * msg) {
|
||||
|
@ -3117,7 +3120,7 @@ namespace smt2 {
|
|||
|
||||
bool operator()() {
|
||||
m_num_bindings = 0;
|
||||
bool found_errors = false;
|
||||
unsigned found_errors = 0;
|
||||
|
||||
try {
|
||||
scan_core();
|
||||
|
@ -3126,7 +3129,7 @@ namespace smt2 {
|
|||
error(ex.msg());
|
||||
if (!sync_after_error())
|
||||
return false;
|
||||
found_errors = true;
|
||||
found_errors++;
|
||||
}
|
||||
|
||||
while (true) {
|
||||
|
@ -3138,7 +3141,7 @@ namespace smt2 {
|
|||
parse_cmd();
|
||||
break;
|
||||
case scanner::EOF_TOKEN:
|
||||
return !found_errors;
|
||||
return found_errors == 0;
|
||||
default:
|
||||
throw parser_exception("invalid command, '(' expected");
|
||||
break;
|
||||
|
|
Loading…
Reference in a new issue