mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix bug in definition of rewrite rule for replace, tighten constraints for tightest-prefix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-02-23 18:41:56 -08:00
parent 12458b1a84
commit d5383e2387
3 changed files with 15 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -444,11 +444,12 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
bool found = false; bool found = false;
for (unsigned i = 0; !found && i < as.size(); ++i) { for (unsigned i = 0; !found && i < as.size(); ++i) {
if (bs.size() > as.size() - i) break;
all_values &= m().is_value(as[i].get()); all_values &= m().is_value(as[i].get());
unsigned j = 0; if (bs.size() <= as.size() - i) {
for (; j < bs.size() && as[j+i].get() == bs[j].get(); ++j) {}; unsigned j = 0;
found = j == bs.size(); for (; j < bs.size() && as[j+i].get() == bs[j].get(); ++j) {};
found = j == bs.size();
}
} }
if (found) { if (found) {
result = m().mk_true(); result = m().mk_true();

15
src/smt/theory_seq.cpp
View file

@ -2135,13 +2135,13 @@ void theory_seq::deque_axiom(expr* n) {
lit or s = "" or s = s1*(unit c) lit or s = "" or s = s1*(unit c)
lit or s = "" or !contains(x*s1, s) lit or s = "" or !contains(x*s1, s)
*/ */
void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) { void theory_seq::tightest_prefix(expr* s, expr* x) {
expr_ref s1 = mk_first(s); expr_ref s1 = mk_first(s);
expr_ref c = mk_last(s); expr_ref c = mk_last(s);
expr_ref s1c = mk_concat(s1, m_util.str.mk_unit(c)); expr_ref s1c = mk_concat(s1, m_util.str.mk_unit(c));
literal s_eq_emp = mk_eq_empty(s); literal s_eq_emp = mk_eq_empty(s);
add_axiom(s_eq_emp, mk_seq_eq(s, s1c)); add_axiom(s_eq_emp, mk_seq_eq(s, s1c));
add_axiom(lit1, lit2, s_eq_emp, ~mk_literal(m_util.str.mk_contains(mk_concat(x, s1), s))); add_axiom(s_eq_emp, ~mk_literal(m_util.str.mk_contains(mk_concat(x, s1), s)));
} }
/* /*
@ -2155,7 +2155,7 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) {
len(t) != 0 & !contains(t, s) => i = -1 len(t) != 0 & !contains(t, s) => i = -1
len(t) != 0 & contains(t, s) => t = xsy & i = len(x) len(t) != 0 & contains(t, s) => t = xsy & i = len(x)
len(t) != 0 & contains(t, s) & s != emp => tightest_prefix(x, s) tightest_prefix(x, s)
offset not fixed: offset not fixed:
@ -2193,7 +2193,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
add_axiom(s_eq_empty, ~mk_eq_empty(t), mk_eq(i, minus_one, false)); add_axiom(s_eq_empty, ~mk_eq_empty(t), mk_eq(i, minus_one, false));
add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy)); add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy));
add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false)); add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false));
tightest_prefix(s, x, ~cnt); tightest_prefix(s, x);
} }
else { else {
// offset >= len(t) => indexof(s, t, offset) = -1 // offset >= len(t) => indexof(s, t, offset) = -1
@ -2227,7 +2227,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
/* /*
let r = replace(a, s, t) let r = replace(a, s, t)
(contains(a, s) -> tightest_prefix(s,xs)) tightest_prefix(s, x)
(contains(a, s) -> r = xty & a = xsy) & (contains(a, s) -> r = xty & a = xsy) &
(!contains(a, s) -> r = a) (!contains(a, s) -> r = a)
@ -2243,7 +2243,7 @@ void theory_seq::add_replace_axiom(expr* r) {
add_axiom(cnt, mk_seq_eq(r, a)); add_axiom(cnt, mk_seq_eq(r, a));
add_axiom(~cnt, mk_seq_eq(a, xsy)); add_axiom(~cnt, mk_seq_eq(a, xsy));
add_axiom(~cnt, mk_seq_eq(r, xty)); add_axiom(~cnt, mk_seq_eq(r, xty));
tightest_prefix(s, x, ~cnt); tightest_prefix(s, x);
} }
void theory_seq::add_elim_string_axiom(expr* n) { void theory_seq::add_elim_string_axiom(expr* n) {
@ -3382,6 +3382,7 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
VERIFY(m_util.str.is_prefix(e, e1, e2)); VERIFY(m_util.str.is_prefix(e, e1, e2));
SASSERT(ctx.get_assignment(e) == l_false); SASSERT(ctx.get_assignment(e) == l_false);
if (canonizes(false, e)) { if (canonizes(false, e)) {
TRACE("seq", tout << mk_pp(e, m) << " is false\n";);
return false; return false;
} }
expr_ref head1(m), tail1(m), head2(m), tail2(m), conc(m); expr_ref head1(m), tail1(m), head2(m), tail2(m), conc(m);
@ -3515,11 +3516,13 @@ bool theory_seq::canonizes(bool sign, expr* e) {
TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";); TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";);
if ((m.is_true(cont) && !sign) || if ((m.is_true(cont) && !sign) ||
(m.is_false(cont) && sign)) { (m.is_false(cont) && sign)) {
TRACE("seq", display(tout););
propagate_lit(deps, 0, 0, ctx.get_literal(e)); propagate_lit(deps, 0, 0, ctx.get_literal(e));
return true; return true;
} }
if ((m.is_false(cont) && !sign) || if ((m.is_false(cont) && !sign) ||
(m.is_true(cont) && sign)) { (m.is_true(cont) && sign)) {
TRACE("seq", display(tout););
return true; return true;
} }
return false; return false;

2
src/smt/theory_seq.h
View file

@ -443,7 +443,7 @@ namespace smt {
literal mk_literal(expr* n); literal mk_literal(expr* n);
literal mk_eq_empty(expr* n); literal mk_eq_empty(expr* n);
literal mk_seq_eq(expr* a, expr* b); literal mk_seq_eq(expr* a, expr* b);
void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal); void tightest_prefix(expr* s, expr* x);
expr_ref mk_sub(expr* a, expr* b); expr_ref mk_sub(expr* a, expr* b);
enode* ensure_enode(expr* a); enode* ensure_enode(expr* a);