mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

remove unsound simplification in prefix #949

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-21 07:40:35 -06:00
parent d58018841e
commit ca4ae171ea
2 changed files with 16 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -676,6 +676,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
bool isc2 = m_util.str.is_string(b, s2);
if (isc1 && isc2) {
result = m().mk_bool_val(s1.prefixof(s2));
TRACE("seq", tout << result << "\n";);
return BR_DONE;
}
if (m_util.str.is_empty(a)) {
@ -689,6 +690,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
expr_ref_vector as(m()), bs(m());
if (a1 != b1 && isc1 && isc2) {
TRACE("seq", tout << s1 << " " << s2 << "\n";);
if (s1.length() <= s2.length()) {
if (s1.prefixof(s2)) {
if (a == a1) {
@ -733,26 +735,27 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
unsigned i = 0;
bool all_values = true;
expr_ref_vector eqs(m());
for (; i < as.size() && i < bs.size(); ++i) {
expr* a = as[i].get(), *b = bs[i].get();
if (a == b) {
continue;
}
all_values &= m().is_value(a) && m().is_value(b);
if (all_values) {
result = m().mk_false();
return BR_DONE;
}
if (m_util.str.is_unit(a) && m_util.str.is_unit(b)) {
eqs.push_back(m().mk_eq(a, b));
continue;
}
if (m().is_value(a) && m().is_value(b) && m_util.str.is_string(a) && m_util.str.is_string(b)) {
TRACE("seq", tout << mk_pp(a, m()) << " != " << mk_pp(b, m()) << "\n";);
result = m().mk_false();
return BR_DONE;
}
break;
}
if (i == as.size()) {
result = mk_and(eqs);
TRACE("seq", tout << result << "\n";);
if (m().is_true(result)) {
return BR_DONE;
}
@ -764,6 +767,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
eqs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
}
result = mk_and(eqs);
TRACE("seq", tout << result << "\n";);
return BR_REWRITE3;
}
if (i > 0) {
@ -771,6 +775,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
a = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i);
b = m_util.str.mk_concat(bs.size() - i, bs.c_ptr() + i);
result = m_util.str.mk_prefix(a, b);
TRACE("seq", tout << result << "\n";);
return BR_DONE;
}
else {

7
src/smt/theory_seq.cpp
View file

@ -2719,7 +2719,9 @@ bool theory_seq::can_propagate() {
expr_ref theory_seq::canonize(expr* e, dependency*& eqs) {
expr_ref result = expand(e, eqs);
TRACE("seq", tout << mk_pp(e, m) << " expands to " << result << "\n";);
m_rewrite(result);
TRACE("seq", tout << mk_pp(e, m) << " rewrites to " << result << "\n";);
return result;
}
@ -4469,10 +4471,11 @@ bool theory_seq::canonizes(bool sign, expr* e) {
context& ctx = get_context();
dependency* deps = 0;
expr_ref cont = canonize(e, deps);
TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";);
TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";
if (deps) display_deps(tout, deps););
if ((m.is_true(cont) && !sign) ||
(m.is_false(cont) && sign)) {
TRACE("seq", display(tout););
TRACE("seq", display(tout); tout << ctx.get_assignment(ctx.get_literal(e)) << "\n";);
propagate_lit(deps, 0, 0, ctx.get_literal(e));
return true;
}