mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

seq bug fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-26 07:21:31 -08:00
parent 924f03c6de
commit 345f6e87bd
4 changed files with 329 additions and 162 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -538,34 +538,40 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
}
}
}
if (a1 != b1) {
return BR_FAILED;
}
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) {
all_values &= m().is_value(as[i].get()) && m().is_value(bs[i].get());
if (as[i].get() != bs[i].get()) {
if (all_values) {
result = m().mk_false();
return BR_DONE;
}
break;
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;
}
break;
}
if (i == as.size()) {
result = m().mk_true();
return BR_DONE;
result = mk_and(eqs);
if (m().is_true(result)) {
return BR_DONE;
}
return BR_REWRITE3;
}
SASSERT(i < as.size());
if (i == bs.size()) {
expr_ref_vector es(m());
for (unsigned j = i; j < as.size(); ++j) {
es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
eqs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
}
result = mk_and(es);
result = mk_and(eqs);
return BR_REWRITE3;
}
if (i > 0) {
@ -575,8 +581,9 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
result = m_util.str.mk_prefix(a, b);
return BR_DONE;
}
UNREACHABLE();
return BR_FAILED;
else {
return BR_FAILED;
}
}
br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
@ -1221,19 +1228,19 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
SASSERT(m().get_sort(ch) == m().get_sort(a));
lhs.push_back(ch);
rhs.push_back(a);
ls.pop_back();
++head1;
if (s.length() == 1) {
rs.pop_back();
++head2;
}
else {
expr_ref s2(m_util.str.mk_string(s.extract(1, s.length()-1)), m());
rs[rs.size()-1] = s2;
rs[head2] = s2;
}
}
else {
break;
}
TRACE("seq", tout << "change front\n";);
TRACE("seq", tout << ls << " == " << rs << "\n";);
change = true;
lchange = true;

4
src/ast/seq_decl_plugin.cpp
View file

@ -143,11 +143,15 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
if (eq) {
result.m_buffer.append(dst.m_buffer);
found = true;
i += src.length() - 1;
}
else {
result.m_buffer.push_back(m_buffer[i]);
}
}
for (unsigned i = length() - src.length() + 1; i < length(); ++i) {
result.m_buffer.push_back(m_buffer[i]);
}
return result;
}

414
src/smt/theory_seq.cpp
View file

@ -70,7 +70,6 @@ expr* theory_seq::solution_map::find(expr* e, dependency*& d) {
expr* result = e;
while (m_map.find(result, value)) {
d = m_dm.mk_join(d, value.second);
TRACE("seq", tout << mk_pp(result, m) << " -> " << mk_pp(value.first, m) << "\n";);
SASSERT(result != value.first);
SASSERT(e != value.first);
result = value.first;
@ -195,7 +194,7 @@ theory_seq::~theory_seq() {
final_check_status theory_seq::final_check_eh() {
TRACE("seq", display(tout););
TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n"););
if (simplify_and_solve_eqs()) {
++m_stats.m_solve_eqs;
TRACE("seq", tout << ">>solve_eqs\n";);
@ -422,12 +421,12 @@ bool theory_seq::propagate_length_coherence(expr* e) {
tail = mk_concat(elems.size(), elems.c_ptr());
// len(e) >= low => e = tail;
literal low(mk_literal(m_autil.mk_ge(m_util.str.mk_length(e), m_autil.mk_numeral(lo, true))));
add_axiom(~low, mk_eq(e, tail, false));
add_axiom(~low, mk_seq_eq(e, tail));
if (upper_bound(e, hi)) {
// len(e) <= hi => len(tail) <= hi - lo
expr_ref high1(m_autil.mk_le(m_util.str.mk_length(e), m_autil.mk_numeral(hi, true)), m);
if (hi == lo) {
add_axiom(~mk_literal(high1), mk_eq(seq, emp, false));
add_axiom(~mk_literal(high1), mk_seq_eq(seq, emp));
}
else {
expr_ref high2(m_autil.mk_le(m_util.str.mk_length(seq), m_autil.mk_numeral(hi-lo, true)), m);
@ -501,6 +500,11 @@ bool theory_seq::is_tail(expr* e, expr*& s, unsigned& idx) const {
(idx = r.get_unsigned(), s = to_app(e)->get_arg(0), true);
}
bool theory_seq::is_eq(expr* e, expr*& a, expr*& b) const {
return is_skolem(symbol("seq.eq"), e) &&
(a = to_app(e)->get_arg(0), b = to_app(e)->get_arg(1), true);
}
expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
sort* char_sort = 0;
@ -608,15 +612,23 @@ bool theory_seq::check_extensionality() {
bool theory_seq::is_solved() {
if (!m_eqs.empty()) {
TRACE("seq", tout << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";);
IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";);
return false;
}
for (unsigned i = 0; i < m_automata.size(); ++i) {
if (!m_automata[i]) {
TRACE("seq", tout << "(seq.giveup regular expression did not compile to automaton)\n";);
IF_VERBOSE(10, verbose_stream() << "(seq.giveup regular expression did not compile to automaton)\n";);
return false;
}
}
if (false && !m_nqs.empty()) {
TRACE("seq", display_disequation(tout << "(seq.giveup ", m_nqs[0]); tout << " is unsolved)\n";);
IF_VERBOSE(10, display_disequation(verbose_stream() << "(seq.giveup ", m_nqs[0]); verbose_stream() << " is unsolved)\n";);
return false;
}
return true;
}
@ -737,11 +749,10 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
}
}
TRACE("seq",
tout << ls << " = " << rs << " => \n";
if (!ls.empty() || !rs.empty()) tout << ls << " = " << rs << ";\n";
for (unsigned i = 0; i < lhs.size(); ++i) {
tout << mk_pp(lhs[i].get(), m) << "\n = \n" << mk_pp(rhs[i].get(), m) << "; \n";
}
tout << "\n";);
tout << mk_pp(lhs[i].get(), m) << " = " << mk_pp(rhs[i].get(), m) << ";\n";
});
return true;
@ -1004,12 +1015,12 @@ bool theory_seq::solve_nqs(unsigned i) {
bool theory_seq::solve_ne(unsigned idx) {
context& ctx = get_context();
ne const& n = m_nqs[idx];
TRACE("seq", display_disequation(tout, n););
unsigned num_undef_lits = 0;
for (unsigned i = 0; i < n.lits().size(); ++i) {
switch (ctx.get_assignment(n.lits(i))) {
case l_false:
TRACE("seq", display_disequation(tout << "has false literal\n", n););
return true;
case l_true:
break;
@ -1035,6 +1046,7 @@ bool theory_seq::solve_ne(unsigned idx) {
change = canonize(n.rs(i), rs, deps) || change;
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, change)) {
TRACE("seq", display_disequation(tout << "reduces to false", n););
return true;
}
else if (!change) {
@ -1059,10 +1071,8 @@ bool theory_seq::solve_ne(unsigned idx) {
new_rs.push_back(rs);
}
TRACE("seq",
for (unsigned j = 0; j < lhs.size(); ++j) {
tout << mk_pp(lhs[j].get(), m) << " " << mk_pp(rhs[j].get(), m) << "\n";
}
tout << "\n";
tout << lhs << " != " << rhs << "\n";
for (unsigned j = 0; j < new_ls.size(); ++j) tout << new_ls[j] << " != " << new_rs[j] << "\n";
tout << n.ls(i) << " != " << n.rs(i) << "\n";);
for (unsigned j = 0; j < lhs.size(); ++j) {
@ -1095,6 +1105,9 @@ bool theory_seq::solve_ne(unsigned idx) {
new_deps = m_dm.mk_join(deps, new_deps);
}
}
TRACE("seq", display_disequation(tout, n););
if (!updated && num_undef_lits == 0) {
return false;
}
@ -1331,43 +1344,15 @@ void theory_seq::init_model(model_generator & mg) {
}
}
class unit_wrapper_proc : public model_value_proc {
theory_seq& th;
model_value_dependency m_dep;
public:
unit_wrapper_proc(theory_seq& th, model_value_dependency d, expr* n): th(th), m_dep(d) {}
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values) {
SASSERT(values.size() == 1);
bv_util bv(th.m);
rational val;
unsigned sz;
if (bv.is_numeral(values[0], val, sz) && sz == zstring().num_bits()) {
unsigned v = val.get_unsigned();
svector<bool> val_as_bits;
for (unsigned i = 0; i < sz; ++i) {
val_as_bits.push_back(1 == v % 2);
v = v / 2;
}
return m_util.str.mk_string(zstring(sz, val_as_bits.c_ptr()));
}
else {
return th.m_util.str.mk_unit(values[0]);
}
}
virtual void get_dependencies(buffer<model_value_dependency> & result) {
result.push_back(m_dep);
}
};
class seq_value_proc : public model_value_proc {
theory_seq& th;
app* n;
class theory_seq::seq_value_proc : public model_value_proc {
theory_seq& th;
sort* m_sort;
svector<model_value_dependency> m_dependencies;
ptr_vector<expr> m_strings;
svector<bool> m_source;
public:
seq_value_proc(theory_seq& th, app* n): th(th), n(n) {
seq_value_proc(theory_seq& th, sort* s): th(th), m_sort(s) {
}
virtual ~seq_value_proc() {}
void add_dependency(enode* n) {
@ -1383,49 +1368,68 @@ public:
}
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values) {
SASSERT(values.size() == m_dependencies.size());
ptr_vector<expr> args;
expr_ref_vector args(th.m);
unsigned j = 0, k = 0;
bool is_string = th.m_util.is_string(m_sort);
for (unsigned i = 0; i < m_source.size(); ++i) {
if (m_source[i]) {
args.push_back(values[j++]);
if (m_source[i] && is_string) {
bv_util bv(th.m);
rational val;
unsigned sz;
VERIFY(bv.is_numeral(values[j++], val, sz));
svector<bool> val_as_bits;
unsigned v = val.get_unsigned();
for (unsigned i = 0; i < sz; ++i) {
val_as_bits.push_back(1 == v % 2);
v = v / 2;
}
args.push_back(th.m_util.str.mk_string(zstring(sz, val_as_bits.c_ptr())));
}
else if (m_source[i]) {
args.push_back(th.m_util.str.mk_unit(values[j++]));
}
else {
args.push_back(m_strings[k++]);
}
}
if (args.empty()) {
return th.mk_value(n);
}
return th.mk_value(mg.get_manager().mk_app(n->get_decl(), args.size(), args.c_ptr()));
expr_ref result = th.mk_concat(args, m_sort);
th.m_rewrite(result);
th.m_factory->add_trail(result);
return to_app(result);
}
};
model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
expr_ref e(m);
expr* e1, *e2;
e = m_rep.find(n->get_owner());
if (m_util.str.is_concat(e, e1, e2)) {
if (m_util.is_seq(n->get_owner())) {
ptr_vector<expr> concats;
get_concat(n->get_owner(), concats);
context& ctx = get_context();
seq_value_proc* sv = alloc(seq_value_proc, *this, to_app(e));
sort* srt = m.get_sort(n->get_owner());
seq_value_proc* sv = alloc(seq_value_proc, *this, srt);
// e = e1 .. en
// those that are units, those that are not units.
// e = unit(e1) +
for (unsigned i = 0; i < concats.size(); ++i) {
expr* c = concats[i], *c1;
if (m_util.str.is_unit(c, c1)) {
sv->add_dependency(ctx.get_enode(c1));
}
else if (m_util.str.is_string(c)) {
sv->add_string(c);
}
else {
sv->add_string(mk_value(to_app(c)));
}
}
return sv;
}
else if (m_util.str.is_unit(e, e1)) {
return alloc(unit_wrapper_proc, *this, ctx.get_enode(e1));
}
else {
return alloc(expr_wrapper_proc, mk_value(e));
return alloc(expr_wrapper_proc, mk_value(n->get_owner()));
}
}
app* theory_seq::mk_value(app* e) {
expr_ref result(m);
result = m_rep.find(e);
if (is_var(result)) {
SASSERT(m_factory);
@ -1618,7 +1622,7 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) {
expr_ref c = mk_last(s);
expr_ref s1c = mk_concat(s1, m_util.str.mk_unit(c));
literal s_eq_emp = mk_eq_empty(s);
add_axiom(s_eq_emp, mk_eq(s, s1c, false));
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)));
}
@ -1669,7 +1673,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
add_axiom(cnt, mk_eq(i, minus_one, false));
add_axiom(~s_eq_empty, mk_eq(i, zero, false));
add_axiom(s_eq_empty, ~mk_eq_empty(t), mk_eq(i, minus_one, false));
add_axiom(~cnt, s_eq_empty, mk_eq(t, xsy, false));
add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy));
add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false));
tightest_prefix(s, x, ~cnt);
}
@ -1692,7 +1696,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
// 0 <= offset & offset < len(t) & indexof(y,s,0) >= 0 = -1 =>
// -1 = indexof(y,s,0) + offset = indexof(t, s, offset)
add_axiom(~offset_ge_0, offset_ge_len, mk_eq(t, mk_concat(x, y), false));
add_axiom(~offset_ge_0, offset_ge_len, mk_seq_eq(t, mk_concat(x, y)));
add_axiom(~offset_ge_0, offset_ge_len, mk_eq(m_util.str.mk_length(x), offset, false));
add_axiom(~offset_ge_0, offset_ge_len,
~mk_eq(indexof0, minus_one, false), mk_eq(i, minus_one, false));
@ -1718,9 +1722,9 @@ void theory_seq::add_replace_axiom(expr* r) {
expr_ref xty = mk_concat(x, t, y);
expr_ref xsy = mk_concat(x, s, y);
literal cnt = mk_literal(m_util.str.mk_contains(a ,s));
add_axiom(cnt, mk_eq(r, a, false));
add_axiom(~cnt, mk_eq(a, xsy, false));
add_axiom(~cnt, mk_eq(r, xty, false));
add_axiom(cnt, mk_seq_eq(r, a));
add_axiom(~cnt, mk_seq_eq(a, xsy));
add_axiom(~cnt, mk_seq_eq(r, xty));
tightest_prefix(s, x, ~cnt);
}
@ -1991,7 +1995,7 @@ void theory_seq::add_at_axiom(expr* e) {
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
literal i_ge_len_s = mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(s, xey, false));
add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, xey));
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false));
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, false));
}
@ -2050,10 +2054,10 @@ literal theory_seq::mk_literal(expr* _e) {
return ctx.get_literal(e);
}
literal theory_seq::mk_equals(expr* a, expr* b) {
literal lit = mk_eq(a, b, false);
get_context().force_phase(lit);
return lit;
literal theory_seq::mk_seq_eq(expr* a, expr* b) {
SASSERT(m_util.is_seq(a));
return mk_literal(mk_skolem(symbol("seq.eq"), a, b, 0, m.mk_bool_sort()));
}
literal theory_seq::mk_eq_empty(expr* _e) {
@ -2061,16 +2065,25 @@ literal theory_seq::mk_eq_empty(expr* _e) {
SASSERT(m_util.is_seq(e));
expr_ref emp(m);
zstring s;
if (m_util.str.is_string(e, s)) {
if (s.length() == 0) {
return true_literal;
if (m_util.str.is_empty(e)) {
return true_literal;
}
expr_ref_vector concats(m);
m_util.str.get_concat(e, concats);
for (unsigned i = 0; i < concats.size(); ++i) {
if (m_util.str.is_unit(concats[i].get())) {
return false_literal;
}
else {
if (m_util.str.is_string(concats[i].get(), s) && s.length() > 0) {
return false_literal;
}
}
emp = m_util.str.mk_empty(m.get_sort(e));
return mk_equals(e, emp);
literal lit = mk_eq(e, emp, false);
get_context().force_phase(lit);
return lit;
}
void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, literal l5) {
@ -2138,6 +2151,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
expr* e = ctx.bool_var2expr(v);
expr* e1, *e2;
expr_ref f(m);
bool change = false;
literal lit(v, !is_true);
if (m_util.str.is_prefix(e, e1, e2)) {
@ -2147,11 +2161,14 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
propagate_eq(lit, f, e2, true);
}
else {
// !prefix(e1,e2) => e1 != ""
#if 0
propagate_not_prefix(e);
#else
propagate_non_empty(lit, e1);
if (add_prefix2prefix(e)) {
if (add_prefix2prefix(e, change)) {
add_atom(e);
}
#endif
}
}
else if (m_util.str.is_suffix(e, e1, e2)) {
@ -2161,6 +2178,10 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
propagate_eq(lit, f, e2, true);
}
else {
#if 1
propagate_not_suffix(e);
#else
// lit => e1 != empty
propagate_non_empty(lit, e1);
@ -2170,9 +2191,11 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
f = mk_concat(f1, m_util.str.mk_unit(f2));
propagate_eq(lit, e1, f, true);
if (add_suffix2suffix(e)) {
TRACE("seq", tout << "suffix: " << f << " = " << mk_pp(e1, m) << "\n";);
if (add_suffix2suffix(e, change)) {
add_atom(e);
}
#endif
}
}
else if (m_util.str.is_contains(e, e1, e2)) {
@ -2185,7 +2208,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
else if (!canonizes(false, e)) {
propagate_non_empty(lit, e2);
propagate_lit(0, 1, &lit, ~mk_literal(m_util.str.mk_prefix(e2, e1)));
if (add_contains2contains(e)) {
if (add_contains2contains(e, change)) {
add_atom(e);
}
}
@ -2193,7 +2216,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
else if (is_accept(e)) {
if (is_true) {
propagate_acc_rej_length(lit, e);
if (add_accept2step(e)) {
if (add_accept2step(e, change)) {
add_atom(e);
}
}
@ -2207,11 +2230,16 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
else if (is_step(e)) {
if (is_true) {
propagate_step(lit, e);
if (add_step2accept(e)) {
if (add_step2accept(e, change)) {
add_atom(e);
}
}
}
else if (is_eq(e, e1, e2)) {
if (is_true) {
propagate_eq(lit, e1, e2, true);
}
}
else if (m_util.str.is_in_re(e)) {
propagate_in_re(e, is_true);
}
@ -2253,13 +2281,53 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
m_rewrite(eq);
if (!m.is_false(eq)) {
TRACE("seq", tout << "new disequality: " << eq << "\n";);
literal lit = ~mk_eq(e1, e2, false);
//SASSERT(get_context().get_assignment(lit) == l_true);
dependency* dep = m_dm.mk_leaf(assumption(lit));
m_nqs.push_back(ne(e1, e2, dep));
solve_nqs(m_nqs.size() - 1);
literal lit = mk_eq(e1, e2, false);
// propagate x != "" into x = (++ (unit (nth x 0) (tail x 0)))
if (m_util.str.is_empty(e2)) {
std::swap(e1, e2);
}
if (false && m_util.str.is_empty(e1)) {
expr_ref head(m), tail(m), conc(m);
mk_decompose(e2, head, tail);
conc = mk_concat(head, tail);
propagate_eq(~lit, e2, conc, true);
}
#if 0
// (e1 = "" & e2 = xdz) or (e2 = "" & e1 = xcy) or (e1 = xcy & e2 = xdz & c != d) or (e1 = x & e2 = xdz) or (e2 = x & e1 = xcy)
// e1 = "" or e1 = xcy or e1 = x
// e2 = "" or e2 = xdz or e2 = x
// e1 = xcy or e2 = xdz
// c != d
literal lit = mk_seq_eq(e1, e2);
sort* char_sort = 0;
expr_ref emp(m);
VERIFY(m_util.is_seq(m.get_sort(e1), char_sort));
emp = m_util.str.mk_empty(m.get_sort(e1));
expr_ref x = mk_skolem(symbol("seq.ne.x"), e1, e2);
expr_ref y = mk_skolem(symbol("seq.ne.y"), e1, e2);
expr_ref z = mk_skolem(symbol("seq.ne.z"), e1, e2);
expr_ref c = mk_skolem(symbol("seq.ne.c"), e1, e2, 0, char_sort);
expr_ref d = mk_skolem(symbol("seq.ne.d"), e1, e2, 0, char_sort);
literal e1_is_emp = mk_seq_eq(e1, emp);
literal e2_is_emp = mk_seq_eq(e2, emp);
literal e1_is_xcy = mk_seq_eq(e1, mk_concat(x, m_util.str.mk_unit(c), y));
literal e2_is_xdz = mk_seq_eq(e2, mk_concat(x, m_util.str.mk_unit(d), z));
add_axiom(lit, e1_is_emp, e1_is_xcy, mk_seq_eq(e1, x));
add_axiom(lit, e2_is_emp, e2_is_xdz, mk_seq_eq(e2, x));
add_axiom(lit, e1_is_xcy, e2_is_xdz);
add_axiom(lit, ~mk_eq(c, d, false));
#else
else {
dependency* dep = m_dm.mk_leaf(assumption(~lit));
m_nqs.push_back(ne(e1, e2, dep));
solve_nqs(m_nqs.size() - 1);
}
#endif
}
// add solution for variable that is non-empty?
}
void theory_seq::push_scope_eh() {
@ -2420,7 +2488,7 @@ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) {
acc(s, idx, re, i) -> \/ step(s, idx, re, i, j, t) if i is non-final
acc(s, idx, re, i) -> len(s) <= idx \/ step(s, idx, re, i, j, t) if i is final
*/
bool theory_seq::add_accept2step(expr* acc) {
bool theory_seq::add_accept2step(expr* acc, bool& change) {
context& ctx = get_context();
TRACE("seq", tout << mk_pp(acc, m) << "\n";);
@ -2443,9 +2511,10 @@ bool theory_seq::add_accept2step(expr* acc) {
if (aut->is_final_state(src)) {
lits.push_back(mk_literal(m_autil.mk_le(len, idx)));
switch (ctx.get_assignment(lits.back())) {
case l_true:
case l_true:
return false;
case l_undef:
change = true;
ctx.force_phase(lits.back());
return true;
default:
@ -2473,6 +2542,7 @@ bool theory_seq::add_accept2step(expr* acc) {
break;
}
}
change = true;
if (has_undef && mvs.size() == 1) {
literal lit = lits.back();
lits.pop_back();
@ -2499,7 +2569,7 @@ bool theory_seq::add_accept2step(expr* acc) {
acc(s, idx, re, i) & step(s, idx, re, i, j, t) => acc(s, idx + 1, re, j)
*/
bool theory_seq::add_step2accept(expr* step) {
bool theory_seq::add_step2accept(expr* step, bool& change) {
context& ctx = get_context();
SASSERT(ctx.get_assignment(step) == l_true);
expr* re, *_acc, *s, *idx, *i, *j;
@ -2509,8 +2579,10 @@ bool theory_seq::add_step2accept(expr* step) {
case l_false:
break;
case l_undef:
change = true;
return true;
case l_true: {
change = true;
rational r;
VERIFY(m_autil.is_numeral(idx, r) && r.is_unsigned());
expr_ref idx1(m_autil.mk_int(r.get_unsigned() + 1), m);
@ -2546,7 +2618,7 @@ Recall we also have:
rej(s, idx, re, i) -> len(s) > idx if i is final
*/
bool theory_seq::add_reject2reject(expr* rej) {
bool theory_seq::add_reject2reject(expr* rej, bool& change) {
context& ctx = get_context();
SASSERT(ctx.get_assignment(rej) == l_true);
expr* s, *idx, *re;
@ -2566,7 +2638,7 @@ bool theory_seq::add_reject2reject(expr* rej) {
case l_true:
return false;
case l_undef:
ctx.force_phase(len_le_idx);
ctx.force_phase(len_le_idx);
return true;
default:
break;
@ -2589,6 +2661,7 @@ bool theory_seq::add_reject2reject(expr* rej) {
}
eqs.push_back(eq);
}
change = true;
if (has_undef) {
return true;
}
@ -2603,10 +2676,71 @@ bool theory_seq::add_reject2reject(expr* rej) {
return false;
}
/*
!prefix(e1,e2) => e1 != ""
!prefix(e1,e2) => e2 = "" or e1 = xcy & (e2 = xdz & c != d or x = e2)
*/
void theory_seq::propagate_not_prefix(expr* e) {
context& ctx = get_context();
expr* e1, *e2;
VERIFY(m_util.str.is_prefix(e, e1, e2));
literal lit = ctx.get_literal(e);
SASSERT(ctx.get_assignment(lit) == l_false);
if (canonizes(false, e)) {
return;
}
propagate_non_empty(~lit, e1);
expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m);
literal e2_is_emp = mk_seq_eq(e2, emp);
sort* char_sort = 0;
VERIFY(m_util.is_seq(m.get_sort(e1), char_sort));
expr_ref x = mk_skolem(symbol("seq.prefix.x"), e1, e2);
expr_ref y = mk_skolem(symbol("seq.prefix.y"), e1, e2);
expr_ref z = mk_skolem(symbol("seq.prefix.z"), e1, e2);
expr_ref c = mk_skolem(symbol("seq.prefix.c"), e1, e2, 0, char_sort);
expr_ref d = mk_skolem(symbol("seq.prefix.d"), e1, e2, 0, char_sort);
add_axiom(lit, e2_is_emp, mk_seq_eq(e1, mk_concat(x, m_util.str.mk_unit(c), y)));
add_axiom(lit, e2_is_emp, mk_seq_eq(e2, mk_concat(x, m_util.str.mk_unit(d), z)), mk_seq_eq(e2, x));
add_axiom(lit, e2_is_emp, ~mk_eq(c, d, false), mk_seq_eq(e2, x));
}
/*
!suffix(e1,e2) => e1 != ""
!suffix(e1,e2) => e2 = "" or e1 = ycx & (e2 = zdx & c != d or x = e2)
*/
void theory_seq::propagate_not_suffix(expr* e) {
context& ctx = get_context();
expr* e1, *e2;
VERIFY(m_util.str.is_suffix(e, e1, e2));
literal lit = ctx.get_literal(e);
SASSERT(ctx.get_assignment(lit) == l_false);
if (canonizes(false, e)) {
return;
}
propagate_non_empty(~lit, e1);
expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m);
literal e2_is_emp = mk_seq_eq(e2, emp);
sort* char_sort = 0;
VERIFY(m_util.is_seq(m.get_sort(e1), char_sort));
expr_ref x = mk_skolem(symbol("seq.suffix.x"), e1, e2);
expr_ref y = mk_skolem(symbol("seq.suffix.y"), e1, e2);
expr_ref z = mk_skolem(symbol("seq.suffix.z"), e1, e2);
expr_ref c = mk_skolem(symbol("seq.suffix.c"), e1, e2, 0, char_sort);
expr_ref d = mk_skolem(symbol("seq.suffix.d"), e1, e2, 0, char_sort);
add_axiom(lit, e2_is_emp, mk_seq_eq(e1, mk_concat(y, m_util.str.mk_unit(c), x)));
add_axiom(lit, e2_is_emp, mk_seq_eq(e2, mk_concat(z, m_util.str.mk_unit(d), x)), mk_seq_eq(e2, x));
add_axiom(lit, e2_is_emp, ~mk_eq(c, d, false), mk_seq_eq(e2, x));
}
/*
!prefix -> e2 = emp \/ nth(e1,0) != nth(e2,0) \/ !prefix(tail(e1),tail(e2))
*/
bool theory_seq::add_prefix2prefix(expr* e) {
bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
context& ctx = get_context();
expr* e1, *e2;
VERIFY(m_util.str.is_prefix(e, e1, e2));
@ -2616,26 +2750,16 @@ bool theory_seq::add_prefix2prefix(expr* e) {
}
expr_ref head1(m), tail1(m), head2(m), tail2(m), conc(m);
literal e1_is_emp = mk_eq_empty(e1);
switch (ctx.get_assignment(e1_is_emp)) {
case l_true:
return false; // done
case l_undef:
return true; // retry
default:
break;
}
mk_decompose(e1, head1, tail1);
conc = mk_concat(head1, tail1);
propagate_eq(~e1_is_emp, e1, conc, true);
TRACE("seq", tout << mk_pp(e, m) << "\n";);
literal e2_is_emp = mk_eq_empty(e2);
switch (ctx.get_assignment(e2_is_emp)) {
case l_true:
TRACE("seq", tout << mk_pp(e2, m) << " = empty\n";);
return false; // done
case l_undef:
ctx.force_phase(~e2_is_emp);
// ctx.force_phase(e2_is_emp);
TRACE("seq", tout << mk_pp(e2, m) << " ~ empty\n";);
return true; // retry
default:
break;
@ -2645,28 +2769,49 @@ bool theory_seq::add_prefix2prefix(expr* e) {
conc = mk_concat(head2, tail2);
propagate_eq(~e2_is_emp, e2, conc, true);
literal e1_is_emp = mk_eq_empty(e1);
switch (ctx.get_assignment(e1_is_emp)) {
case l_true:
TRACE("seq", tout << mk_pp(e1, m) << " = empty\n";);
return false; // done
case l_undef:
TRACE("seq", tout << mk_pp(e1, m) << " ~ empty\n";);
return true; // retry
default:
break;
}
mk_decompose(e1, head1, tail1);
conc = mk_concat(head1, tail1);
propagate_eq(~e1_is_emp, e1, conc, true);
literal lit = mk_eq(head1, head2, false);
switch (ctx.get_assignment(lit)) {
case l_true:
break;
case l_false:
TRACE("seq", tout << head1 << " = " << head2 << "\n";);
return false;
case l_undef:
ctx.force_phase(~lit);
TRACE("seq", tout << head1 << " ~ " << head2 << "\n";);
return true;
}
change = true;
literal_vector lits;
lits.push_back(~ctx.get_literal(e));
lits.push_back(~e2_is_emp);
lits.push_back(lit);
propagate_lit(0, lits.size(), lits.c_ptr(), ~mk_literal(m_util.str.mk_prefix(tail1, tail2)));
TRACE("seq", tout << "saturate: " << tail1 << " = " << tail2 << "\n";);
return false;
}
/*
!suffix(e1, e2) -> e2 = emp \/ last(e1) != last(e2) \/ !suffix(first(e1), first(e2))
*/
bool theory_seq::add_suffix2suffix(expr* e) {
bool theory_seq::add_suffix2suffix(expr* e, bool& change) {
context& ctx = get_context();
expr* e1, *e2;
VERIFY(m_util.str.is_suffix(e, e1, e2));
@ -2679,7 +2824,7 @@ bool theory_seq::add_suffix2suffix(expr* e) {
switch (ctx.get_assignment(e2_is_emp)) {
case l_true:
return false; // done
case l_undef:
case l_undef:
ctx.force_phase(e2_is_emp);
return true; // retry
case l_false:
@ -2717,6 +2862,7 @@ bool theory_seq::add_suffix2suffix(expr* e) {
break;
}
change = true;
literal_vector lits;
lits.push_back(~ctx.get_literal(e));
lits.push_back(~e2_is_emp);
@ -2748,7 +2894,7 @@ bool theory_seq::canonizes(bool sign, expr* e) {
!contains(e1, e2) -> e1 = emp \/ !contains(tail(e1), e2)
*/
bool theory_seq::add_contains2contains(expr* e) {
bool theory_seq::add_contains2contains(expr* e, bool& change) {
context& ctx = get_context();
expr* e1, *e2;
VERIFY(m_util.str.is_contains(e, e1, e2));
@ -2756,19 +2902,25 @@ bool theory_seq::add_contains2contains(expr* e) {
if (canonizes(false, e)) {
return false;
}
expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m);
switch (assume_equality(e1, emp)) {
literal e1_is_emp = mk_eq_empty(e1);
switch (ctx.get_assignment(e1_is_emp)) {
case l_true:
return false; // done
case l_undef:
ctx.force_phase(e1_is_emp);
return true; // retry
default:
break;
}
expr_ref head(m), tail(m);
change = true;
expr_ref head(m), tail(m), conc(m);
mk_decompose(e1, head, tail);
literal lits[2] = { ~ctx.get_literal(e), ~mk_eq(e1, emp, false) };
conc = mk_concat(head, tail);
propagate_eq(~e1_is_emp, e1, conc, true);
literal lits[2] = { ~ctx.get_literal(e), ~e1_is_emp };
propagate_lit(0, 2, lits, ~mk_literal(m_util.str.mk_contains(tail, e2)));
return false;
}
@ -2780,38 +2932,39 @@ bool theory_seq::propagate_automata() {
}
m_trail_stack.push(value_trail<theory_seq, unsigned>(m_atoms_qhead));
ptr_vector<expr> re_add;
bool change = false;
while (m_atoms_qhead < m_atoms.size() && !ctx.inconsistent()) {
expr* e = m_atoms[m_atoms_qhead];
TRACE("seq", tout << mk_pp(e, m) << "\n";);
bool reQ = false;
if (is_accept(e)) {
reQ = add_accept2step(e);
reQ = add_accept2step(e, change);
}
else if (is_reject(e)) {
reQ = add_reject2reject(e);
reQ = add_reject2reject(e, change);
}
else if (is_step(e)) {
reQ = add_step2accept(e);
reQ = add_step2accept(e, change);
}
else if (m_util.str.is_prefix(e)) {
reQ = add_prefix2prefix(e);
reQ = add_prefix2prefix(e, change);
}
else if (m_util.str.is_suffix(e)) {
reQ = add_suffix2suffix(e);
reQ = add_suffix2suffix(e, change);
}
else if (m_util.str.is_contains(e)) {
reQ = add_contains2contains(e);
reQ = add_contains2contains(e, change);
}
if (reQ) {
re_add.push_back(e);
change = true;
}
++m_atoms_qhead;
}
m_atoms.append(re_add);
return true;
return change || get_context().inconsistent();
}
#if 0
void theory_seq::get_concat(expr* e, ptr_vector<expr>& concats) {
expr* e1, *e2;
while (true) {
@ -2825,4 +2978,3 @@ void theory_seq::get_concat(expr* e, ptr_vector<expr>& concats) {
return;
}
}
#endif

22
src/smt/theory_seq.h
View file

@ -45,6 +45,8 @@ namespace smt {
typedef std::pair<expr*, dependency*> expr_dep;
typedef obj_map<expr, expr_dep> eqdep_map_t;
class seq_value_proc;
// cache to track evaluations under equalities
class eval_cache {
eqdep_map_t m_map;
@ -138,8 +140,7 @@ namespace smt {
m_util.str.get_concat(l, ls);
m_util.str.get_concat(r, rs);
return eq(m_eq_id++, ls, rs, dep);
}
}
class ne {
vector<expr_ref_vector> m_lhs;
@ -355,6 +356,7 @@ namespace smt {
bool add_solution(expr* l, expr* r, dependency* dep);
bool is_nth(expr* a) const;
bool is_tail(expr* a, expr*& s, unsigned& idx) const;
bool is_eq(expr* e, expr*& a, expr*& b) const;
expr_ref mk_nth(expr* s, expr* idx);
expr_ref mk_last(expr* e);
expr_ref mk_first(expr* e);
@ -385,7 +387,7 @@ namespace smt {
void add_in_re_axiom(expr* n);
literal mk_literal(expr* n);
literal mk_eq_empty(expr* n);
literal mk_equals(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);
expr_ref mk_sub(expr* a, expr* b);
enode* ensure_enode(expr* a);
@ -421,12 +423,14 @@ namespace smt {
bool is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const;
bool is_step(expr* e) const;
void propagate_step(literal lit, expr* n);
bool add_reject2reject(expr* rej);
bool add_accept2step(expr* acc);
bool add_step2accept(expr* step);
bool add_prefix2prefix(expr* e);
bool add_suffix2suffix(expr* e);
bool add_contains2contains(expr* e);
bool add_reject2reject(expr* rej, bool& change);
bool add_accept2step(expr* acc, bool& change);
bool add_step2accept(expr* step, bool& change);
bool add_prefix2prefix(expr* e, bool& change);
bool add_suffix2suffix(expr* e, bool& change);
bool add_contains2contains(expr* e, bool& change);
void propagate_not_prefix(expr* e);
void propagate_not_suffix(expr* e);
void ensure_nth(literal lit, expr* s, expr* idx);
bool canonizes(bool sign, expr* e);
void propagate_non_empty(literal lit, expr* s);