mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

fix #5134

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-29 14:11:49 -07:00
parent 6bdf377e11
commit 6d28b1a858
3 changed files with 40 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4136,6 +4136,30 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
* (re.range c_1 c_n) * (re.range c_1 c_n)
*/ */
br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
zstring s;
unsigned len = 0;
rational rlen;
bool is_empty = false;
if (str().is_string(lo, s) && s.length() != 1)
is_empty = true;
if (str().is_string(hi, s) && s.length() != 1)
is_empty = true;
min_length(lo, len);
if (len > 1)
is_empty = true;
min_length(hi, len);
if (len > 1)
is_empty = true;
if (max_length(lo, rlen) && rlen == 0)
is_empty = true;
if (max_length(hi, rlen) && rlen == 0)
is_empty = true;
if (is_empty) {
sort* srt = re().mk_re(lo->get_sort());
result = re().mk_empty(srt);
return BR_DONE;
}
return BR_FAILED; return BR_FAILED;
} }

2
src/smt/seq_eq_solver.cpp
View file

@ -1067,6 +1067,8 @@ bool theory_seq::check_length_coherence() {
if (check_length_coherence(e)) { if (check_length_coherence(e)) {
return true; return true;
} }
if (!ctx.e_internalized(e))
change = true;
enode* n = ensure_enode(e); enode* n = ensure_enode(e);
enode* r = n->get_root(); enode* r = n->get_root();
if (r != n && has_length(r->get_expr())) { if (r != n && has_length(r->get_expr())) {

22
src/smt/theory_seq.cpp
View file

@ -403,7 +403,10 @@ final_check_status theory_seq::final_check_eh() {
TRACEFIN("branch_ne"); TRACEFIN("branch_ne");
return FC_CONTINUE; return FC_CONTINUE;
} }
if (m_unhandled_expr) { if (m_unhandled_expr) {
TRACEFIN("give_up");
TRACE("seq", tout << "unhandled: " << mk_pp(m_unhandled_expr, m) << "\n";);
return FC_GIVEUP; return FC_GIVEUP;
} }
if (is_solved()) { if (is_solved()) {
@ -1412,26 +1415,29 @@ bool theory_seq::internalize_atom(app* a, bool) {
bool theory_seq::internalize_term(app* term) { bool theory_seq::internalize_term(app* term) {
m_has_seq = true; m_has_seq = true;
if (m_util.str.is_in_re(term))
mk_var(ensure_enode(term->get_arg(0)));
if (m_util.str.is_length(term))
mk_var(ensure_enode(term->get_arg(0)));
if (ctx.e_internalized(term)) { if (ctx.e_internalized(term)) {
enode* e = ctx.get_enode(term); mk_var(ctx.get_enode(term));
mk_var(e);
return true; return true;
} }
if (m.is_bool(term) && if (m.is_bool(term) &&
(m_util.str.is_in_re(term) || m_sk.is_skolem(term))) { (m_util.str.is_in_re(term) || m_sk.is_skolem(term))) {
if (m_util.str.is_in_re(term)) {
mk_var(ensure_enode(term->get_arg(0)));
}
bool_var bv = ctx.mk_bool_var(term); bool_var bv = ctx.mk_bool_var(term);
ctx.set_var_theory(bv, get_id()); ctx.set_var_theory(bv, get_id());
ctx.mark_as_relevant(bv); ctx.mark_as_relevant(bv);
return true; return true;
} }
for (auto arg : *term) { for (auto arg : *term)
mk_var(ensure_enode(arg)); mk_var(ensure_enode(arg));
}
if (m.is_bool(term)) { if (m.is_bool(term)) {
bool_var bv = ctx.mk_bool_var(term); bool_var bv = ctx.mk_bool_var(term);
ctx.set_var_theory(bv, get_id()); ctx.set_var_theory(bv, get_id());