mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
55ebf69648
commit
c3b27903f8
|
@ -1206,8 +1206,7 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
|
|||
e = todo.back();
|
||||
todo.pop_back();
|
||||
if (m_util.str.is_string(e, s)) {
|
||||
for (unsigned i = s.length(); i > 0; ) {
|
||||
--i;
|
||||
for (unsigned i = 0; i < s.length(); ++i) {
|
||||
seq.push_back(m_util.str.mk_char(s, i));
|
||||
}
|
||||
}
|
||||
|
@ -1218,14 +1217,13 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
|
|||
seq.push_back(e1);
|
||||
}
|
||||
else if (m_util.str.is_concat(e, e1, e2)) {
|
||||
todo.push_back(e1);
|
||||
todo.push_back(e2);
|
||||
todo.push_back(e1);
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
seq.reverse();
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
|
@ -2251,7 +2251,9 @@ bool theory_seq::internalize_term(app* term) {
|
|||
e = ctx.mk_enode(term, false, m.is_bool(term), true);
|
||||
}
|
||||
mk_var(e);
|
||||
|
||||
if (m_util.str.is_string(term)) {
|
||||
add_elim_string_axiom(term);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
@ -3086,6 +3088,7 @@ void theory_seq::propagate() {
|
|||
|
||||
void theory_seq::enque_axiom(expr* e) {
|
||||
if (!m_axiom_set.contains(e)) {
|
||||
TRACE("seq", tout << "add axiom " << mk_pp(e, m) << "\n";);
|
||||
m_axioms.push_back(e);
|
||||
m_axiom_set.insert(e);
|
||||
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_axioms));
|
||||
|
@ -3285,13 +3288,13 @@ void theory_seq::add_replace_axiom(expr* r) {
|
|||
|
||||
void theory_seq::add_elim_string_axiom(expr* n) {
|
||||
zstring s;
|
||||
TRACE("seq", tout << mk_pp(n, m) << "\n";);
|
||||
VERIFY(m_util.str.is_string(n, s));
|
||||
if (s.length() == 0) {
|
||||
return;
|
||||
}
|
||||
expr_ref result(m_util.str.mk_unit(m_util.str.mk_char(s, s.length()-1)), m);
|
||||
for (unsigned i = s.length()-1; i > 0; ) {
|
||||
--i;
|
||||
for (unsigned i = s.length()-1; i-- > 0; ) {
|
||||
result = mk_concat(m_util.str.mk_unit(m_util.str.mk_char(s, i)), result);
|
||||
}
|
||||
add_axiom(mk_eq(n, result, false));
|
||||
|
|
|
@ -8388,13 +8388,12 @@ namespace smt {
|
|||
lbool theory_str::validate_unsat_core(expr_ref_vector & unsat_core) {
|
||||
app * target_term = to_app(get_manager().mk_not(m_theoryStrOverlapAssumption_term));
|
||||
get_context().internalize(target_term, false);
|
||||
enode* e1 = get_context().get_enode(target_term);
|
||||
for (unsigned i = 0; i < unsat_core.size(); ++i) {
|
||||
app * core_term = to_app(unsat_core.get(i));
|
||||
// not sure if this is the correct way to compare terms in this context
|
||||
enode * e1;
|
||||
enode * e2;
|
||||
e1 = get_context().get_enode(target_term);
|
||||
e2 = get_context().get_enode(core_term);
|
||||
if (!get_context().e_internalized(core_term)) continue;
|
||||
enode *e2 = get_context().get_enode(core_term);
|
||||
if (e1 == e2) {
|
||||
TRACE("str", tout << "overlap detected in unsat core, changing UNSAT to UNKNOWN" << std::endl;);
|
||||
return l_undef;
|
||||
|
|
Loading…
Reference in a new issue