mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

change data-structures to concanetation decomposition normal form

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-07 16:03:37 -08:00
parent 0c2334417c
commit ad778f87c7
6 changed files with 235 additions and 401 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/ast/ast_smt2_pp.cpp
View file

@ -1201,14 +1201,18 @@ std::ostream& operator<<(std::ostream& out, app_ref const& e) {
} }
std::ostream& operator<<(std::ostream& out, expr_ref_vector const& e) { std::ostream& operator<<(std::ostream& out, expr_ref_vector const& e) {
for (unsigned i = 0; i < e.size(); ++i) for (unsigned i = 0; i < e.size(); ++i) {
out << mk_ismt2_pp(e[i], e.get_manager()) << "\n"; out << mk_ismt2_pp(e[i], e.get_manager());
if (i + 1 < e.size()) out << "; ";
}
return out; return out;
} }
std::ostream& operator<<(std::ostream& out, app_ref_vector const& e) { std::ostream& operator<<(std::ostream& out, app_ref_vector const& e) {
for (unsigned i = 0; i < e.size(); ++i) for (unsigned i = 0; i < e.size(); ++i) {
out << mk_ismt2_pp(e[i], e.get_manager()) << "\n"; out << mk_ismt2_pp(e[i], e.get_manager());
if (i + 1 < e.size()) out << "; ";
}
return out; return out;
} }

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

@ -830,11 +830,12 @@ br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) { br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
expr_ref_vector lhs(m()), rhs(m()), res(m()); expr_ref_vector lhs(m()), rhs(m()), res(m());
if (!reduce_eq(l, r, lhs, rhs)) { bool changed = false;
if (!reduce_eq(l, r, lhs, rhs, changed)) {
result = m().mk_false(); result = m().mk_false();
return BR_DONE; return BR_DONE;
} }
if (lhs.size() == 1 && lhs[0].get() == l && rhs[0].get() == r) { if (!changed) {
return BR_FAILED; return BR_FAILED;
} }
for (unsigned i = 0; i < lhs.size(); ++i) { for (unsigned i = 0; i < lhs.size(); ++i) {
@ -844,20 +845,19 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
return BR_REWRITE3; return BR_REWRITE3;
} }
bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs) { bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) {
expr* a, *b; expr* a, *b;
zstring s; zstring s;
bool change = false;
bool lchange = false;
SASSERT(lhs.empty());
// solve from back // solve from back
while (true) { while (true) {
while (!rs.empty() && m_util.str.is_empty(rs.back())) { while (!rs.empty() && m_util.str.is_empty(rs.back())) {
rs.pop_back(); rs.pop_back();
change = true;
} }
while (!ls.empty() && m_util.str.is_empty(ls.back())) { while (!ls.empty() && m_util.str.is_empty(ls.back())) {
ls.pop_back(); ls.pop_back();
change = true;
} }
if (ls.empty() || rs.empty()) { if (ls.empty() || rs.empty()) {
break; break;
@ -901,7 +901,9 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
else { else {
break; break;
} }
TRACE("seq", tout << "change back\n";);
change = true; change = true;
lchange = true;
} }
// solve from front // solve from front
@ -956,7 +958,10 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
else { else {
break; break;
} }
TRACE("seq", tout << "change front\n";);
change = true; change = true;
lchange = true;
} }
// reduce strings // reduce strings
zstring s1, s2; zstring s1, s2;
@ -982,7 +987,9 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
else { else {
rs[head2] = m_util.str.mk_string(s2.extract(l, s2.length()-l)); rs[head2] = m_util.str.mk_string(s2.extract(l, s2.length()-l));
} }
TRACE("seq", tout << "change string\n";);
change = true; change = true;
lchange = true;
} }
while (head1 < ls.size() && while (head1 < ls.size() &&
head2 < rs.size() && head2 < rs.size() &&
@ -1002,52 +1009,109 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
if (l < s2.length()) { if (l < s2.length()) {
rs.push_back(m_util.str.mk_string(s2.extract(0, s2.length()-l))); rs.push_back(m_util.str.mk_string(s2.extract(0, s2.length()-l)));
} }
TRACE("seq", tout << "change string back\n";);
change = true; change = true;
lchange = true;
} }
bool is_sat; bool is_sat;
unsigned szl = ls.size() - head1, szr = rs.size() - head2; unsigned szl = ls.size() - head1, szr = rs.size() - head2;
expr* const* _ls = ls.c_ptr() + head1, * const* _rs = rs.c_ptr() + head2; expr* const* _ls = ls.c_ptr() + head1, * const* _rs = rs.c_ptr() + head2;
if (length_constrained(szl, _ls, szr, _rs, lhs, rhs, is_sat)) { if (length_constrained(szl, _ls, szr, _rs, lhs, rhs, is_sat)) {
ls.reset(); rs.reset(); ls.reset(); rs.reset();
return is_sat; change = true;
}
if (is_subsequence(szl, _ls, szr, _rs, lhs, rhs, is_sat)) {
ls.reset(); rs.reset();
return is_sat; return is_sat;
} }
if (szl == 0 && szr == 0) { if (szr == 0 && szl == 0) {
ls.reset(); rs.reset();
return true;
}
else if (!change) {
// skip
SASSERT(lhs.empty());
}
else {
// could solve if either side is fixed size.
SASSERT(szl > 0 && szr > 0);
lhs.push_back(m_util.str.mk_concat(szl, ls.c_ptr() + head1));
rhs.push_back(m_util.str.mk_concat(szr, rs.c_ptr() + head2));
ls.reset(); ls.reset();
rs.reset(); rs.reset();
return true;
} }
SASSERT(lhs.empty() || ls.empty()); if (szr == 0 && szl > 0) {
std::swap(szr, szl);
std::swap(_ls, _rs);
}
if (szl == 0 && szr > 0) {
if (set_empty(szr, _rs, true, lhs, rhs)) {
lchange |= szr > 1;
change |= szr > 1;
TRACE("seq", tout << lchange << " " << szr << "\n";);
if (szr == 1 && !lchange) {
lhs.reset();
rhs.reset();
}
else {
ls.reset();
rs.reset();
}
return true;
}
else {
return false;
}
}
SASSERT(szl > 0 && szr > 0);
if (is_subsequence(szl, _ls, szr, _rs, lhs, rhs, is_sat)) {
ls.reset(); rs.reset();
change = true;
return is_sat;
}
if (lchange) {
if (head1 > 0) {
for (unsigned i = 0; i < szl; ++i) {
ls[i] = ls[i + head1];
}
}
ls.shrink(szl);
if (head2 > 0) {
for (unsigned i = 0; i < szr; ++i) {
rs[i] = rs[i + head2];
}
}
rs.shrink(szr);
}
SASSERT(rs.empty() == ls.empty());
change |= lchange;
return true; return true;
} }
bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs) { void seq_rewriter::add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& lhs, expr_ref_vector& rhs) {
if (ls.empty() && !rs.empty()) {
rhs.push_back(m_util.str.mk_concat(rs));
lhs.push_back(m_util.str.mk_empty(m().get_sort(rhs.back())));
}
else if (rs.empty() && !ls.empty()) {
lhs.push_back(m_util.str.mk_concat(ls));
rhs.push_back(m_util.str.mk_empty(m().get_sort(lhs.back())));
}
else if (!rs.empty() && !ls.empty()) {
lhs.push_back(m_util.str.mk_concat(ls));
rhs.push_back(m_util.str.mk_concat(rs));
}
}
bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& changed) {
m_lhs.reset(); m_lhs.reset();
m_rhs.reset(); m_rhs.reset();
m_util.str.get_concat(l, m_lhs); m_util.str.get_concat(l, m_lhs);
m_util.str.get_concat(r, m_rhs); m_util.str.get_concat(r, m_rhs);
if (reduce_eq(m_lhs, m_rhs, lhs, rhs)) { bool change = false;
if (reduce_eq(m_lhs, m_rhs, lhs, rhs, change)) {
SASSERT(lhs.size() == rhs.size()); SASSERT(lhs.size() == rhs.size());
if (lhs.empty()) { if (!change) {
lhs.push_back(l); lhs.push_back(l);
rhs.push_back(r); rhs.push_back(r);
} }
else {
add_seqs(m_lhs, m_rhs, lhs, rhs);
}
changed |= change;
return true; return true;
} }
else { else {

7
src/ast/rewriter/seq_rewriter.h
View file

@ -90,9 +90,12 @@ public:
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
bool reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs); bool reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change);
bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change);
void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& lhs, expr_ref_vector& rhs);
bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs);
}; };

1
src/ast/seq_decl_plugin.h
View file

@ -223,6 +223,7 @@ public:
app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); } app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
app* mk_concat(expr* a, expr* b, expr* c) { return mk_concat(a, mk_concat(b, c)); } app* mk_concat(expr* a, expr* b, expr* c) { return mk_concat(a, mk_concat(b, c)); }
expr* mk_concat(unsigned n, expr* const* es) { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); } expr* mk_concat(unsigned n, expr* const* es) { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); }
expr* mk_concat(expr_ref_vector const& es) { return mk_concat(es.size(), es.c_ptr()); }
app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); } app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); }
app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); } app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); }
app* mk_contains(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); } app* mk_contains(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); }

343
src/smt/theory_seq.cpp
View file

@ -650,17 +650,22 @@ void theory_seq::enforce_length_coherence(enode* n1, enode* n2) {
bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependency* deps) { bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependency* deps) {
context& ctx = get_context(); context& ctx = get_context();
expr_ref_vector lhs(m), rhs(m); expr_ref_vector lhs(m), rhs(m);
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs)) { bool changed = false;
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, changed)) {
// equality is inconsistent.x2 // equality is inconsistent.x2
TRACE("seq", tout << ls << " != " << rs << "\n";); TRACE("seq", tout << ls << " != " << rs << "\n";);
set_conflict(deps); set_conflict(deps);
return true; return true;
} }
if (lhs.empty()) { if (!changed) {
SASSERT(lhs.empty() && rhs.empty());
return false; return false;
} }
SASSERT(lhs.size() == rhs.size()); SASSERT(lhs.size() == rhs.size());
SASSERT(ls.empty() && rs.empty()); m_seq_rewrite.add_seqs(ls, rs, lhs, rhs);
if (lhs.empty()) {
return true;
}
for (unsigned i = 0; !ctx.inconsistent() && i < lhs.size(); ++i) { for (unsigned i = 0; !ctx.inconsistent() && i < lhs.size(); ++i) {
expr_ref li(lhs[i].get(), m); expr_ref li(lhs[i].get(), m);
expr_ref ri(rhs[i].get(), m); expr_ref ri(rhs[i].get(), m);
@ -686,10 +691,10 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
} }
bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) { bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) {
if (l.size() == 1 && is_var(l[0]) && !occurs(l[0], r) && add_solution(l[0], mk_concat(r), deps)) { if (l.size() == 1 && is_var(l[0]) && !occurs(l[0], r) && add_solution(l[0], mk_concat(r, m.get_sort(l[0])), deps)) {
return true; return true;
} }
if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l), deps)) { if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l, m.get_sort(r[0])), deps)) {
return true; return true;
} }
@ -697,11 +702,9 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const&
} }
bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) { bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) {
SASSERT(l != r);
if (l == r) { if (l == r) {
return true; return true;
} }
if (is_var(l) && !occurs(l, r) && add_solution(l, r, deps)) { if (is_var(l) && !occurs(l, r) && add_solution(l, r, deps)) {
return true; return true;
} }
@ -773,7 +776,8 @@ bool theory_seq::solve_eqs(unsigned i) {
context& ctx = get_context(); context& ctx = get_context();
bool change = false; bool change = false;
for (; !ctx.inconsistent() && i < m_eqs.size(); ++i) { for (; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
eq e = m_eqs[i]; eq const& e = m_eqs[i];
TRACE("seq", tout << i << "\n";);
if (solve_eq(e.ls(), e.rs(), e.dep())) { if (solve_eq(e.ls(), e.rs(), e.dep())) {
if (i + 1 != m_eqs.size()) { if (i + 1 != m_eqs.size()) {
eq e1 = m_eqs[m_eqs.size()-1]; eq e1 = m_eqs[m_eqs.size()-1];
@ -785,6 +789,7 @@ bool theory_seq::solve_eqs(unsigned i) {
change = true; change = true;
} }
} }
TRACE("seq", tout << "solve_eqs\n";);
return change || ctx.inconsistent(); return change || ctx.inconsistent();
} }
@ -796,20 +801,22 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
dependency* dep2 = 0; dependency* dep2 = 0;
bool change = canonize(l, ls, dep2); bool change = canonize(l, ls, dep2);
change = canonize(r, rs, dep2) || change; change = canonize(r, rs, dep2) || change;
TRACE("seq", tout << ls << " = " << rs << "\n";);
deps = m_dm.mk_join(dep2, deps); deps = m_dm.mk_join(dep2, deps);
TRACE("seq", tout << l << " = " << r << " ==> ";
tout << ls << " = " << rs << "\n";);
if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) { if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) {
return true; return true;
} }
TRACE("seq", tout << ls << " = " << rs << "\n";); TRACE("seq", tout << ls << " = " << rs << "\n";);
SASSERT(rs.empty() == ls.empty()); if (ls.empty() && rs.empty()) {
if (ls.empty()) {
return true; return true;
} }
if (!ctx.inconsistent() && solve_unit_eq(ls, rs, deps)) { if (!ctx.inconsistent() && solve_unit_eq(ls, rs, deps)) {
TRACE("seq", tout << "unit\n";);
return true; return true;
} }
if (!ctx.inconsistent() && solve_binary_eq(ls, rs, deps)) { if (!ctx.inconsistent() && solve_binary_eq(ls, rs, deps)) {
TRACE("seq", tout << "binary\n";);
return true; return true;
} }
if (!ctx.inconsistent() && change) { if (!ctx.inconsistent() && change) {
@ -871,6 +878,7 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
return false; return false;
} }
if (xs.size() != ys.size()) { if (xs.size() != ys.size()) {
TRACE("seq", tout << "binary conflict\n";);
set_conflict(dep); set_conflict(dep);
return false; return false;
} }
@ -928,149 +936,24 @@ bool theory_seq::solve_nqs(unsigned i) {
bool change = false; bool change = false;
context & ctx = get_context(); context & ctx = get_context();
for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) { for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) {
if (!m_nqs[i].is_solved()) { if (solve_ne(i)) {
solve_ne(i); if (i + 1 != m_nqs.size()) {
ne n = m_nqs[m_nqs.size()-1];
m_nqs.set(i, n);
--i;
}
m_nqs.pop_back();
} }
} }
return m_new_propagation || ctx.inconsistent(); return m_new_propagation || ctx.inconsistent();
} }
void theory_seq::solve_ne(unsigned idx) {
bool theory_seq::solve_ne(unsigned idx) {
context& ctx = get_context(); context& ctx = get_context();
ne const& n = m_nqs[idx]; ne const& n = m_nqs[idx];
TRACE("seq", display_disequation(tout, n);); TRACE("seq", display_disequation(tout, n););
SASSERT(!n.is_solved());
unsigned num_undef_lits = 0;
for (unsigned i = 0; i < n.m_lits.size(); ++i) {
switch (ctx.get_assignment(n.m_lits[i])) {
case l_false:
// mark as solved in
mark_solved(idx);
return;
case l_true:
break;
case l_undef:
++num_undef_lits;
break;
}
}
for (unsigned i = 0; i < n.m_lhs.size(); ++i) {
expr_ref_vector& ls = m_ls;
expr_ref_vector& rs = m_rs;
expr_ref_vector& lhs = m_lhs;
expr_ref_vector& rhs = m_rhs;
ls.reset(); rs.reset(); lhs.reset(); rhs.reset();
dependency* deps = 0;
expr* l = n.m_lhs[i];
expr* r = n.m_rhs[i];
canonize(l, ls, deps);
canonize(r, rs, deps);
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs)) {
mark_solved(idx);
return;
}
else if (lhs.empty() || (lhs.size() == 1 && lhs[0].get() == l)) {
// continue
}
else {
TRACE("seq",
for (unsigned j = 0; j < lhs.size(); ++j) {
tout << mk_pp(lhs[j].get(), m) << " ";
}
tout << "\n";
tout << mk_pp(l, m) << " != " << mk_pp(r, m) << "\n";);
for (unsigned j = 0; j < lhs.size(); ++j) {
expr_ref nl(lhs[j].get(), m);
expr_ref nr(rhs[j].get(), m);
if (m_util.is_seq(nl) || m_util.is_re(nl)) {
m_trail_stack.push(push_ne(*this, idx, nl, nr));
}
else {
literal lit(mk_eq(nl, nr, false));
m_trail_stack.push(push_lit(*this, idx, lit));
ctx.mark_as_relevant(lit);
switch (ctx.get_assignment(lit)) {
case l_false:
mark_solved(idx);
return;
case l_true:
break;
case l_undef:
++num_undef_lits;
m_new_propagation = true;
break;
}
}
}
m_trail_stack.push(push_dep(*this, idx, deps));
erase_index(idx, i);
--i;
}
}
if (num_undef_lits == 1 && n.m_lhs.empty()) {
literal_vector lits;
literal undef_lit = null_literal;
for (unsigned i = 0; i < n.m_lits.size(); ++i) {
literal lit = n.m_lits[i];
switch (ctx.get_assignment(lit)) {
case l_true:
lits.push_back(lit);
break;
case l_false:
UNREACHABLE();
break;
case l_undef:
SASSERT(undef_lit == null_literal);
undef_lit = lit;
break;
}
}
TRACE("seq", tout << "propagate: " << undef_lit << "\n";);
SASSERT(undef_lit != null_literal);
propagate_lit(n.m_dep, lits.size(), lits.c_ptr(), ~undef_lit);
}
else if (num_undef_lits == 0 && n.m_lhs.empty()) {
literal_vector lits(n.m_lits);
lits.push_back(~mk_eq(n.m_l, n.m_r, false));
set_conflict(n.m_dep, lits);
SASSERT(m_new_propagation);
}
else if (false && num_undef_lits == 0 && n.m_lhs.size() == 1) {
expr* l = n.m_lhs[0];
expr* r = n.m_rhs[0];
if (m_util.str.is_empty(r)) {
std::swap(l, r);
}
if (m_util.str.is_empty(l) && is_var(r)) {
literal lit = ~mk_eq_empty(r);
switch (ctx.get_assignment(lit)) {
case l_true: {
expr_ref head(m), tail(m);
mk_decompose(r, head, tail);
expr_ref conc = mk_concat(head, tail);
propagate_is_conc(r, conc);
m_new_propagation = true;
break;
}
case l_undef:
m_new_propagation = true;
break;
case l_false:
break;
}
}
}
}
#if 0
bool theory_seq::solve_ne2(unsigned idx) {
context& ctx = get_context();
ne2 const& n = m_nqs[idx];
TRACE("seq", display_disequation(tout, n););
unsigned num_undef_lits = 0; unsigned num_undef_lits = 0;
for (unsigned i = 0; i < n.lits().size(); ++i) { for (unsigned i = 0; i < n.lits().size(); ++i) {
switch (ctx.get_assignment(n.lits(i))) { switch (ctx.get_assignment(n.lits(i))) {
@ -1083,10 +966,10 @@ bool theory_seq::solve_ne2(unsigned idx) {
break; break;
} }
} }
unsigned_vector unchanged;
dependency* new_deps = 0; dependency* new_deps = n.dep();
vector<expr_ref_vector> new_ls, new_rs; vector<expr_ref_vector> new_ls, new_rs;
literal_vector new_lits = n.lits(); literal_vector new_lits(n.lits());
bool updated = false; bool updated = false;
for (unsigned i = 0; i < n.ls().size(); ++i) { for (unsigned i = 0; i < n.ls().size(); ++i) {
expr_ref_vector& ls = m_ls; expr_ref_vector& ls = m_ls;
@ -1095,34 +978,49 @@ bool theory_seq::solve_ne2(unsigned idx) {
expr_ref_vector& rhs = m_rhs; expr_ref_vector& rhs = m_rhs;
ls.reset(); rs.reset(); lhs.reset(); rhs.reset(); ls.reset(); rs.reset(); lhs.reset(); rhs.reset();
dependency* deps = 0; dependency* deps = 0;
expr_ref_vector const& l = n.ls(i); bool change = false;
expr_ref_vector const& r = n.rs(i); change = canonize(n.ls(i), ls, deps) || change;
change = canonize(l, ls, deps) || change; change = canonize(n.rs(i), rs, deps) || change;
change = canonize(r, rs, deps) || change;
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs)) { if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, change)) {
return true; return true;
} }
else if (!change && lhs.empty()) { else if (!change) {
unchanged.push_back(i); // std::cout << n.ls(i) << " " << ls << "\n";
} // std::cout << n.rs(i) << " " << rs << "\n";
else if (change && lhs.empty()) { continue;
} }
else { else {
if (!updated) {
for (unsigned j = 0; j < i; ++j) {
new_ls.push_back(n.ls(j));
new_rs.push_back(n.rs(j));
}
}
updated = true; updated = true;
if (!ls.empty() || !rs.empty()) {
new_ls.push_back(ls);
new_rs.push_back(rs);
}
TRACE("seq", TRACE("seq",
for (unsigned j = 0; j < lhs.size(); ++j) { for (unsigned j = 0; j < lhs.size(); ++j) {
tout << mk_pp(lhs[j].get(), m) << " "; tout << mk_pp(lhs[j].get(), m) << " ";
} }
tout << "\n"; tout << "\n";
tout << l << " != " << r << "\n";); tout << n.ls(i) << " != " << n.rs(i) << "\n";);
for (unsigned j = 0; j < lhs.size(); ++j) { for (unsigned j = 0; j < lhs.size(); ++j) {
expr_ref nl(lhs[j].get(), m); expr* nl = lhs[j].get();
expr_ref nr(rhs[j].get(), m); expr* nr = rhs[j].get();
if (m_util.is_seq(nl) || m_util.is_re(nl)) { if (m_util.is_seq(nl) || m_util.is_re(nl)) {
new_ls.push_back(nl); ls.reset();
new_rs.push_back(nr); rs.reset();
SASSERT(!m_util.str.is_concat(nl));
SASSERT(!m_util.str.is_concat(nr));
ls.push_back(nl); rs.push_back(nr);
new_ls.push_back(ls);
new_rs.push_back(rs);
} }
else { else {
literal lit(mk_eq(nl, nr, false)); literal lit(mk_eq(nl, nr, false));
@ -1140,7 +1038,7 @@ bool theory_seq::solve_ne2(unsigned idx) {
} }
} }
} }
new_deps = deps; new_deps = m_dm.mk_join(deps, new_deps);
} }
} }
if (num_undef_lits == 1 && new_ls.empty()) { if (num_undef_lits == 1 && new_ls.empty()) {
@ -1166,31 +1064,19 @@ bool theory_seq::solve_ne2(unsigned idx) {
propagate_lit(new_deps, lits.size(), lits.c_ptr(), ~undef_lit); propagate_lit(new_deps, lits.size(), lits.c_ptr(), ~undef_lit);
return true; return true;
} }
else if (num_undef_lits == 0 && new_ls.empty()) { else if (updated) {
set_conflict(new_deps, new_lits); if (num_undef_lits == 0 && new_ls.empty()) {
SASSERT(m_new_propagation); TRACE("seq", tout << "conflict\n";);
return true; set_conflict(new_deps, new_lits);
SASSERT(m_new_propagation);
}
else {
m_nqs.push_back(ne(new_ls, new_rs, new_lits, new_deps));
}
} }
else if (change) { return updated;
}
return change;
} }
#endif
void theory_seq::mark_solved(unsigned idx) {
m_trail_stack.push(solved_ne(*this, idx));
}
void theory_seq::erase_index(unsigned idx, unsigned i) {
ne const& n = m_nqs[idx];
unsigned sz = n.m_lhs.size();
if (i + 1 != sz) {
m_trail_stack.push(set_ne(*this, idx, i, n.m_lhs[sz-1], n.m_rhs[sz-1]));
}
m_trail_stack.push(pop_ne(*this, idx));
}
bool theory_seq::simplify_and_solve_eqs() { bool theory_seq::simplify_and_solve_eqs() {
context & ctx = get_context(); context & ctx = get_context();
@ -1308,26 +1194,24 @@ void theory_seq::display_equations(std::ostream& out) const {
void theory_seq::display_disequations(std::ostream& out) const { void theory_seq::display_disequations(std::ostream& out) const {
bool first = true; bool first = true;
for (unsigned i = 0; i < m_nqs.size(); ++i) { for (unsigned i = 0; i < m_nqs.size(); ++i) {
if (!m_nqs[i].is_solved()) { if (first) out << "Disequations:\n";
if (first) out << "Disequations:\n"; first = false;
first = false; display_disequation(out, m_nqs[i]);
display_disequation(out, m_nqs[i]); }
}
}
} }
void theory_seq::display_disequation(std::ostream& out, ne const& e) const { void theory_seq::display_disequation(std::ostream& out, ne const& e) const {
for (unsigned j = 0; j < e.m_lits.size(); ++j) { for (unsigned j = 0; j < e.lits().size(); ++j) {
out << e.m_lits[j] << " "; out << e.lits(j) << " ";
} }
if (e.m_lits.size() > 0) { if (e.lits().size() > 0) {
out << "\n"; out << "\n";
} }
for (unsigned j = 0; j < e.m_lhs.size(); ++j) { for (unsigned j = 0; j < e.ls().size(); ++j) {
out << mk_pp(e.m_lhs[j], m) << " != " << mk_pp(e.m_rhs[j], m) << "\n"; out << e.ls(j) << " != " << e.rs(j) << "\n";
} }
if (e.m_dep) { if (e.dep()) {
display_deps(out, e.m_dep); display_deps(out, e.dep());
} }
} }
@ -1529,44 +1413,40 @@ expr_ref theory_seq::canonize(expr* e, dependency*& eqs) {
return result; return result;
} }
bool theory_seq::canonize(expr* e0, expr_ref_vector& es, dependency*& eqs) { bool theory_seq::canonize(expr* e, expr_ref_vector& es, dependency*& eqs) {
dependency* dep = 0;
expr* e = m_rep.find(e0, dep);
bool change = e != e0;
expr* e1, *e2; expr* e1, *e2;
if (m_util.str.is_concat(e, e1, e2)) { expr_ref e3(e, m);
change = canonize(e1, es, eqs) || change; bool change = false;
change = canonize(e2, es, eqs) || change; while (true) {
} if (m_util.str.is_concat(e3, e1, e2)) {
else if (m_util.str.is_empty(e)) { canonize(e1, es, eqs);
// skip e3 = e2;
} change = true;
else { continue;
expr_ref e3 = expand(e, eqs); }
if (m_util.str.is_concat(e3) || m_util.str.is_empty(e3)) { if (m_util.str.is_empty(e3)) {
change = canonize(e3, es, eqs) || change; return true;
}
expr_ref e4 = expand(e3, eqs);
change |= e4 != e3;
if (m_util.str.is_concat(e4) || m_util.str.is_empty(e4)) {
e3 = e4;
continue;
} }
else { else {
change = e3 != e || change; es.push_back(e4);
es.push_back(e3); break;
} }
} }
eqs = m_dm.mk_join(eqs, dep);
return change; return change;
} }
bool theory_seq::canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs) { bool theory_seq::canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs) {
dependency* dep = 0;
bool change = false; bool change = false;
for (unsigned i = 0; i < es.size(); ++i) { for (unsigned i = 0; i < es.size(); ++i) {
expr_ref r = expand(es[i], eqs); change = canonize(es[i], result, eqs) || change;
change |= r != es[i]; SASSERT(!m_util.str.is_concat(es[i]) || change);
if (m_util.str.is_concat(r)) {
canonize(r, result, eqs);
}
else if (!m_util.str.is_empty(r)) {
result.push_back(r);
}
} }
return change; return change;
} }
@ -2093,7 +1973,7 @@ void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) {
s2 = tail; s2 = tail;
} }
elems.push_back(s2); elems.push_back(s2);
conc = mk_concat(elems); conc = mk_concat(elems, m.get_sort(s));
propagate_eq(lit, s, conc, true); propagate_eq(lit, s, conc, true);
} }
@ -2295,7 +2175,10 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
expr_ref eq(m.mk_eq(e1, e2), m); expr_ref eq(m.mk_eq(e1, e2), m);
m_rewrite(eq); m_rewrite(eq);
if (!m.is_false(eq)) { if (!m.is_false(eq)) {
m_nqs.push_back(ne(e1, e2)); 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); solve_nqs(m_nqs.size() - 1);
} }
// add solution for variable that is non-empty? // add solution for variable that is non-empty?

155
src/smt/theory_seq.h
View file

@ -141,22 +141,30 @@ namespace smt {
} }
class ne2 { class ne {
vector<expr_ref_vector> m_lhs; vector<expr_ref_vector> m_lhs;
vector<expr_ref_vector> m_rhs; vector<expr_ref_vector> m_rhs;
literal_vector m_lits; literal_vector m_lits;
dependency* m_dep; dependency* m_dep;
public: public:
ne2(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep): ne(expr_ref const& l, expr_ref const& r, dependency* dep):
m_dep(dep) { m_dep(dep) {
m_lhs.push_back(l); expr_ref_vector ls(l.get_manager()); ls.push_back(l);
m_rhs.push_back(r); expr_ref_vector rs(r.get_manager()); rs.push_back(r);
m_lhs.push_back(ls);
m_rhs.push_back(rs);
} }
ne2(ne2 const& other): ne(vector<expr_ref_vector> const& l, vector<expr_ref_vector> const& r, literal_vector const& lits, dependency* dep):
m_lhs(l),
m_rhs(r),
m_lits(lits),
m_dep(dep) {}
ne(ne const& other):
m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {} m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {}
ne2& operator=(ne2 const& other) { ne& operator=(ne const& other) {
if (this != &other) { if (this != &other) {
m_lhs.reset(); m_lhs.append(other.m_lhs); m_lhs.reset(); m_lhs.append(other.m_lhs);
m_rhs.reset(); m_rhs.append(other.m_rhs); m_rhs.reset(); m_rhs.append(other.m_rhs);
@ -174,136 +182,6 @@ namespace smt {
dependency* dep() const { return m_dep; } dependency* dep() const { return m_dep; }
}; };
// asserted or derived disqequality with dependencies
struct ne {
bool m_solved;
expr_ref m_l, m_r;
expr_ref_vector m_lhs;
expr_ref_vector m_rhs;
literal_vector m_lits;
dependency* m_dep;
ne(expr_ref& l, expr_ref& r):
m_solved(false), m_l(l), m_r(r), m_lhs(l.get_manager()), m_rhs(r.get_manager()), m_dep(0) {
m_lhs.push_back(l);
m_rhs.push_back(r);
}
ne(ne const& other):
m_solved(other.m_solved), m_l(other.m_l), m_r(other.m_r), m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {}
ne& operator=(ne const& other) {
m_solved = other.m_solved;
m_l = other.m_l;
m_r = other.m_r;
m_lhs.reset(); m_lhs.append(other.m_lhs);
m_rhs.reset(); m_rhs.append(other.m_rhs);
m_lits.reset(); m_lits.append(other.m_lits);
m_dep = other.m_dep;
return *this;
}
bool is_solved() const { return m_solved; }
};
class pop_lit : public trail<theory_seq> {
unsigned m_idx;
literal m_lit;
public:
pop_lit(theory_seq& th, unsigned idx): m_idx(idx), m_lit(th.m_nqs[idx].m_lits.back()) {
th.m_nqs.ref(m_idx).m_lits.pop_back();
}
virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits.push_back(m_lit); }
};
class push_lit : public trail<theory_seq> {
unsigned m_idx;
public:
push_lit(theory_seq& th, unsigned idx, literal lit): m_idx(idx) {
th.m_nqs.ref(m_idx).m_lits.push_back(lit);
}
virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits.pop_back(); }
};
class set_lit : public trail<theory_seq> {
unsigned m_idx;
unsigned m_i;
literal m_lit;
public:
set_lit(theory_seq& th, unsigned idx, unsigned i, literal lit):
m_idx(idx), m_i(i), m_lit(th.m_nqs[idx].m_lits[i]) {
th.m_nqs.ref(m_idx).m_lits[i] = lit;
}
virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits[m_i] = m_lit; }
};
class solved_ne : public trail<theory_seq> {
unsigned m_idx;
public:
solved_ne(theory_seq& th, unsigned idx) : m_idx(idx) { th.m_nqs.ref(idx).m_solved = true; }
virtual void undo(theory_seq& th) { th.m_nqs.ref(m_idx).m_solved = false; }
};
void mark_solved(unsigned idx);
class push_ne : public trail<theory_seq> {
unsigned m_idx;
public:
push_ne(theory_seq& th, unsigned idx, expr* l, expr* r) : m_idx(idx) {
th.m_nqs.ref(m_idx).m_lhs.push_back(l);
th.m_nqs.ref(m_idx).m_rhs.push_back(r);
}
virtual void undo(theory_seq& th) { th.m_nqs.ref(m_idx).m_lhs.pop_back(); th.m_nqs.ref(m_idx).m_rhs.pop_back(); }
};
class pop_ne : public trail<theory_seq> {
expr_ref m_lhs;
expr_ref m_rhs;
unsigned m_idx;
public:
pop_ne(theory_seq& th, unsigned idx):
m_lhs(th.m_nqs[idx].m_lhs.back(), th.m),
m_rhs(th.m_nqs[idx].m_rhs.back(), th.m),
m_idx(idx) {
th.m_nqs.ref(idx).m_lhs.pop_back();
th.m_nqs.ref(idx).m_rhs.pop_back();
}
virtual void undo(theory_seq& th) {
th.m_nqs.ref(m_idx).m_lhs.push_back(m_lhs);
th.m_nqs.ref(m_idx).m_rhs.push_back(m_rhs);
m_lhs.reset();
m_rhs.reset();
}
};
class set_ne : public trail<theory_seq> {
expr_ref m_lhs;
expr_ref m_rhs;
unsigned m_idx;
unsigned m_i;
public:
set_ne(theory_seq& th, unsigned idx, unsigned i, expr* l, expr* r):
m_lhs(th.m_nqs[idx].m_lhs[i], th.m),
m_rhs(th.m_nqs[idx].m_rhs[i], th.m),
m_idx(idx),
m_i(i) {
th.m_nqs.ref(idx).m_lhs[i] = l;
th.m_nqs.ref(idx).m_rhs[i] = r;
}
virtual void undo(theory_seq& th) {
th.m_nqs.ref(m_idx).m_lhs[m_i] = m_lhs;
th.m_nqs.ref(m_idx).m_rhs[m_i] = m_rhs;
m_lhs.reset();
m_rhs.reset();
}
};
class push_dep : public trail<theory_seq> {
dependency* m_dep;
unsigned m_idx;
public:
push_dep(theory_seq& th, unsigned idx, dependency* d): m_dep(th.m_nqs[idx].m_dep), m_idx(idx) {
th.m_nqs.ref(idx).m_dep = d;
}
virtual void undo(theory_seq& th) {
th.m_nqs.ref(m_idx).m_dep = m_dep;
}
};
class apply { class apply {
public: public:
virtual ~apply() {} virtual ~apply() {}
@ -441,12 +319,13 @@ namespace smt {
bool solve_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep); bool solve_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
bool propagate_max_length(expr* l, expr* r, dependency* dep); bool propagate_max_length(expr* l, expr* r, dependency* dep);
expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); }
expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); } expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); }
expr_ref mk_concat(expr_ref_vector const& es) { return mk_concat(es.size(), es.c_ptr()); } expr_ref mk_concat(expr_ref_vector const& es, sort* s) { if (es.empty()) return mk_empty(s); return mk_concat(es.size(), es.c_ptr()); }
expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(m_util.str.mk_concat(e1, e2), m); } expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(m_util.str.mk_concat(e1, e2), m); }
expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(m_util.str.mk_concat(e1, e2, e3), m); } expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(m_util.str.mk_concat(e1, e2, e3), m); }
bool solve_nqs(unsigned i); bool solve_nqs(unsigned i);
void solve_ne(unsigned i); bool solve_ne(unsigned i);
// asserting consequences // asserting consequences
void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const; void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;