mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-01-07 15:58:34 +00:00
parent e53b580cb4 0c2334417c
commit 66604fa621
5 changed files with 368 additions and 159 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2010,8 +2010,8 @@ bool bv_rewriter::is_add_mul_const(expr* e) const {
bool bv_rewriter::is_concat_target(expr* lhs, expr* rhs) const {
return
m_util.is_concat(lhs) && (is_concat_split_target(rhs) || has_numeral(to_app(lhs))) ||
m_util.is_concat(rhs) && (is_concat_split_target(lhs) || has_numeral(to_app(rhs)));
(m_util.is_concat(lhs) && (is_concat_split_target(rhs) || has_numeral(to_app(lhs)))) ||
(m_util.is_concat(rhs) && (is_concat_split_target(lhs) || has_numeral(to_app(rhs))));
}
bool bv_rewriter::has_numeral(app* a) const {

3
src/smt/smt_context.cpp
View file

@ -4072,8 +4072,7 @@ namespace smt {
// the theories of (array int int) and (array (array int int) int).
// Remark: The inconsistency is not going to be detected if they are
// not marked as shared.
bool result = get_theory(th_id)->is_shared(l->get_th_var());
return result;
return get_theory(th_id)->is_shared(l->get_th_var());
}
default:
return true;

2
src/smt/smt_enode.h
View file

@ -113,6 +113,7 @@ namespace smt {
friend class context;
friend class euf_manager;
friend class conflict_resolution;
theory_var_list * get_th_var_list() {
return m_th_var_list.get_th_var() == null_theory_var ? 0 : &m_th_var_list;
@ -170,6 +171,7 @@ namespace smt {
m_interpreted = true;
}
void del_eh(ast_manager & m, bool update_children_parent = true);
app * get_owner() const {

405
src/smt/theory_seq.cpp
View file

@ -23,7 +23,6 @@ Revision History:
#include "smt_context.h"
#include "smt_model_generator.h"
#include "theory_seq.h"
#include "seq_rewriter.h"
#include "ast_trail.h"
#include "theory_arith.h"
@ -155,12 +154,14 @@ theory_seq::theory_seq(ast_manager& m):
theory(m.mk_family_id("seq")),
m(m),
m_rep(m, m_dm),
m_eq_id(0),
m_factory(0),
m_exclude(m),
m_axioms(m),
m_axioms_head(0),
m_mg(0),
m_rewrite(m),
m_rewrite(m),
m_seq_rewrite(m),
m_util(m),
m_autil(m),
m_trail_stack(*this),
@ -232,50 +233,47 @@ final_check_status theory_seq::final_check_eh() {
bool theory_seq::branch_variable() {
context& ctx = get_context();
unsigned sz = m_eqs.size();
expr_ref_vector ls(m), rs(m);
int start = ctx.get_random_value();
unsigned s = 0;
for (unsigned i = 0; i < sz; ++i) {
unsigned k = (i + start) % sz;
eq e = m_eqs[k];
TRACE("seq", tout << e.m_lhs << " = " << e.m_rhs << "\n";);
ls.reset(); rs.reset();
m_util.str.get_concat(e.m_lhs, ls);
m_util.str.get_concat(e.m_rhs, rs);
eq const& e = m_eqs[k];
unsigned id = e.id();
TRACE("seq", tout << e.ls() << " = " << e.rs() << "\n";);
s = find_branch_start(e.m_lhs, e.m_rhs);
bool found = find_branch_candidate(s, e.m_dep, ls, rs);
insert_branch_start(e.m_lhs, e.m_rhs, s);
s = find_branch_start(2*id);
bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs());
insert_branch_start(2*id, s);
if (found) {
return true;
}
s = find_branch_start(e.m_lhs, e.m_rhs);
found = find_branch_candidate(s, e.m_dep, rs, ls);
insert_branch_start(e.m_rhs, e.m_lhs, s);
s = find_branch_start(2*id + 1);
found = find_branch_candidate(s, e.dep(), e.rs(), e.ls());
insert_branch_start(2*id + 1, s);
if (found) {
return true;
}
#if 0
if (!has_length(e.m_lhs)) {
enforce_length(ensure_enode(e.m_lhs));
if (!has_length(e.ls())) {
enforce_length(ensure_enode(e.ls()));
}
if (!has_length(e.m_rhs)) {
enforce_length(ensure_enode(e.m_rhs));
if (!has_length(e.rs())) {
enforce_length(ensure_enode(e.rs()));
}
#endif
}
return ctx.inconsistent();
}
void theory_seq::insert_branch_start(expr* l, expr* r, unsigned s) {
m_branch_start.insert(l, r, s);
m_trail_stack.push(pop_branch(m, l, r));
void theory_seq::insert_branch_start(unsigned k, unsigned s) {
m_branch_start.insert(k, s);
m_trail_stack.push(pop_branch(k));
}
unsigned theory_seq::find_branch_start(expr* l, expr* r) {
unsigned theory_seq::find_branch_start(unsigned k) {
unsigned s = 0;
if (m_branch_start.find(l, r, s)) {
if (m_branch_start.find(k, s)) {
return s;
}
return 0;
@ -301,14 +299,15 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
// start = 0;
for (; start < rs.size(); ++start) {
unsigned j = start;
if (occurs(l, rs[j])) {
SASSERT(!m_util.str.is_concat(rs[j]));
SASSERT(!m_util.str.is_string(rs[j]));
if (l == rs[j]) {
return false;
}
SASSERT(!m_util.str.is_string(rs[j]));
if (!can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size() - j - 1, rs.c_ptr() + j + 1)) {
continue;
}
v0 = m_util.str.mk_concat(j + 1, rs.c_ptr());
v0 = mk_concat(j + 1, rs.c_ptr());
if (l_false != assume_equality(l, v0)) {
TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
++start;
@ -324,7 +323,7 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
literal_vector lits;
lits.push_back(~mk_eq_empty(l));
for (unsigned i = 0; i < rs.size(); ++i) {
v0 = m_util.str.mk_concat(i + 1, rs.c_ptr());
v0 = mk_concat(i + 1, rs.c_ptr());
lits.push_back(~mk_eq(l, v0, false));
}
set_conflict(dep, lits);
@ -412,7 +411,7 @@ bool theory_seq::propagate_length_coherence(expr* e) {
}
expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
elems.push_back(seq);
tail = m_util.str.mk_concat(elems.size(), elems.c_ptr());
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));
@ -441,7 +440,7 @@ bool theory_seq::check_length_coherence(expr* e) {
l_false == assume_equality(e, emp)) {
// e = emp \/ e = unit(head.elem(e))*tail(e)
mk_decompose(e, head, tail);
expr_ref conc(m_util.str.mk_concat(head, tail), m);
expr_ref conc = mk_concat(head, tail);
propagate_is_conc(e, conc);
assume_equality(tail, emp);
}
@ -549,7 +548,7 @@ void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
bool theory_seq::is_solved() {
if (!m_eqs.empty()) {
IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].m_lhs << " = " << m_eqs[0].m_rhs << " 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) {
@ -632,54 +631,76 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
void theory_seq::enforce_length_coherence(enode* n1, enode* n2) {
expr* o1 = n1->get_owner();
expr* o2 = n2->get_owner();
if (m_util.str.is_concat(o1) && m_util.str.is_concat(o2)) {
//std::cout << "concats:\n" << mk_pp(o1,m) << "\n" << mk_pp(o2,m) << "\n";
return;
}
if (has_length(o1) && !has_length(o2)) {
//std::cout << "enforce length: " << mk_pp(o1,m) << " -> " << mk_pp(o2,m) << "\n";
enforce_length(n2);
}
else if (has_length(o2) && !has_length(o1)) {
//std::cout << "enforce length: " << mk_pp(o2,m) << " -> " << mk_pp(o1,m) << "\n";
enforce_length(n1);
}
}
bool theory_seq::simplify_eq(expr* l, expr* r, dependency* deps) {
bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependency* deps) {
context& ctx = get_context();
seq_rewriter rw(m);
expr_ref_vector lhs(m), rhs(m);
if (!rw.reduce_eq(l, r, lhs, rhs)) {
// equality is inconsistent.
TRACE("seq", tout << mk_pp(l, m) << " != " << mk_pp(r, m) << "\n";);
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs)) {
// equality is inconsistent.x2
TRACE("seq", tout << ls << " != " << rs << "\n";);
set_conflict(deps);
return true;
}
if (unchanged(l, lhs, r, rhs)) {
if (lhs.empty()) {
return false;
}
SASSERT(lhs.size() == rhs.size());
for (unsigned i = 0; i < lhs.size(); ++i) {
SASSERT(ls.empty() && rs.empty());
for (unsigned i = 0; !ctx.inconsistent() && i < lhs.size(); ++i) {
expr_ref li(lhs[i].get(), m);
expr_ref ri(rhs[i].get(), m);
if (m_util.is_seq(li) || m_util.is_re(li)) {
m_eqs.push_back(eq(li, ri, deps));
if (solve_unit_eq(li, ri, deps)) {
// skip
}
else if (m_util.is_seq(li) || m_util.is_re(li)) {
m_eqs.push_back(mk_eqdep(li, ri, deps));
}
else {
propagate_eq(deps, ensure_enode(li), ensure_enode(ri));
}
}
TRACE("seq",
tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " => \n";
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";);
return true;
}
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)) {
return true;
}
if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l), deps)) {
return true;
}
return false;
}
bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) {
SASSERT(l != r);
if (l == r) {
return true;
}
//propagate_max_length(l, r, deps);
if (is_var(l) && !occurs(l, r) && add_solution(l, r, deps)) {
return true;
@ -691,8 +712,16 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) {
return false;
}
bool theory_seq::occurs(expr* a, expr_ref_vector const& b) {
for (unsigned i = 0; i < b.size(); ++i) {
if (a == b[i]) return true;
}
return false;
}
bool theory_seq::occurs(expr* a, expr* b) {
// true if a occurs under an interpreted function or under left/right selector.
// true if a occurs under an interpreted function or under left/right selector.
SASSERT(is_var(a));
SASSERT(m_todo.empty());
expr* e1, *e2;
@ -709,9 +738,10 @@ bool theory_seq::occurs(expr* a, expr* b) {
m_todo.push_back(e2);
}
}
return false;
return false;
}
bool theory_seq::is_var(expr* a) {
return
m_util.is_seq(a) &&
@ -744,7 +774,7 @@ bool theory_seq::solve_eqs(unsigned i) {
bool change = false;
for (; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
eq e = m_eqs[i];
if (solve_eq(e.m_lhs, e.m_rhs, e.m_dep)) {
if (solve_eq(e.ls(), e.rs(), e.dep())) {
if (i + 1 != m_eqs.size()) {
eq e1 = m_eqs[m_eqs.size()-1];
m_eqs.set(i, e1);
@ -758,22 +788,32 @@ bool theory_seq::solve_eqs(unsigned i) {
return change || ctx.inconsistent();
}
bool theory_seq::solve_eq(expr* _l, expr* _r, dependency* deps) {
bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) {
context& ctx = get_context();
expr_ref l = canonize(_l, deps);
expr_ref r = canonize(_r, deps);
TRACE("seq", tout << l << " = " << r << "\n";);
if (!ctx.inconsistent() && simplify_eq(l, r, deps)) {
expr_ref_vector& ls = m_ls;
expr_ref_vector& rs = m_rs;
rs.reset(); ls.reset();
dependency* dep2 = 0;
bool change = canonize(l, ls, dep2);
change = canonize(r, rs, dep2) || change;
TRACE("seq", tout << ls << " = " << rs << "\n";);
deps = m_dm.mk_join(dep2, deps);
if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) {
return true;
}
if (!ctx.inconsistent() && solve_unit_eq(l, r, deps)) {
TRACE("seq", tout << ls << " = " << rs << "\n";);
SASSERT(rs.empty() == ls.empty());
if (ls.empty()) {
return true;
}
if (!ctx.inconsistent() && solve_unit_eq(ls, rs, deps)) {
return true;
}
if (!ctx.inconsistent() && solve_binary_eq(l, r, deps)) {
if (!ctx.inconsistent() && solve_binary_eq(ls, rs, deps)) {
return true;
}
if (!ctx.inconsistent() && (_l != l || _r != r)) {
m_eqs.push_back(eq(l, r, deps));
if (!ctx.inconsistent() && change) {
m_eqs.push_back(eq(m_eq_id++, ls, rs, deps));
return true;
}
return false;
@ -787,45 +827,40 @@ bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) {
}
rational hi;
if (is_tail(l, s, idx) && has_length(s) && m_util.str.is_empty(r) && !upper_bound(s, hi)) {
std::cout << "max length " << mk_pp(s, m) << " " << idx << "\n";
//std::cout << "max length " << mk_pp(s, m) << " " << idx << "\n";
propagate_lit(deps, 0, 0, mk_literal(m_autil.mk_le(m_util.str.mk_length(s), m_autil.mk_int(idx+1))));
return true;
}
return false;
}
bool theory_seq::is_binary_eq(expr* l, expr* r, expr*& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr*& y) {
xs.reset();
ys.reset();
get_concat(l, xs);
if (xs.size() > 1 && is_var(xs[0])) {
get_concat(r, ys);
if (ys.size() > 1 && is_var(ys.back())) {
x = xs[0];
y = ys.back();
for (unsigned i = 1; i < xs.size(); ++i) {
if (!m_util.str.is_unit(xs[i])) return false;
xs[i-1] = xs[i];
}
xs.pop_back();
for (unsigned i = 0; i < ys.size()-1; ++i) {
if (!m_util.str.is_unit(ys[i])) return false;
}
ys.pop_back();
return true;
bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr*& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr*& y) {
if (ls.size() > 1 && is_var(ls[0]) &&
rs.size() > 1 && is_var(rs.back())) {
xs.reset();
ys.reset();
x = ls[0];
y = rs.back();
for (unsigned i = 1; i < ls.size(); ++i) {
if (!m_util.str.is_unit(ls[i])) return false;
}
for (unsigned i = 0; i < rs.size()-1; ++i) {
if (!m_util.str.is_unit(rs[i])) return false;
}
xs.append(ls.size()-1, ls.c_ptr() + 1);
ys.append(rs.size()-1, rs.c_ptr());
return true;
}
return false;
}
bool theory_seq::solve_binary_eq(expr* l, expr* r, dependency* dep) {
bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
context& ctx = get_context();
ptr_vector<expr> xs, ys;
expr* x, *y;
bool is_binary = is_binary_eq(l, r, x, xs, ys, y);
bool is_binary = is_binary_eq(ls, rs, x, xs, ys, y);
if (!is_binary) {
std::swap(l, r);
is_binary = is_binary_eq(l, r, x, xs, ys, y);
is_binary = is_binary_eq(rs, ls, x, xs, ys, y);
}
if (!is_binary) {
return false;
@ -902,7 +937,6 @@ bool theory_seq::solve_nqs(unsigned i) {
void theory_seq::solve_ne(unsigned idx) {
context& ctx = get_context();
seq_rewriter rw(m);
ne const& n = m_nqs[idx];
TRACE("seq", display_disequation(tout, n););
@ -932,7 +966,7 @@ void theory_seq::solve_ne(unsigned idx) {
expr* r = n.m_rhs[i];
canonize(l, ls, deps);
canonize(r, rs, deps);
if (!rw.reduce_eq(ls, rs, lhs, rhs)) {
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs)) {
mark_solved(idx);
return;
}
@ -1015,7 +1049,7 @@ void theory_seq::solve_ne(unsigned idx) {
case l_true: {
expr_ref head(m), tail(m);
mk_decompose(r, head, tail);
expr_ref conc(m_util.str.mk_concat(head, tail), m);
expr_ref conc = mk_concat(head, tail);
propagate_is_conc(r, conc);
m_new_propagation = true;
break;
@ -1031,6 +1065,120 @@ void theory_seq::solve_ne(unsigned idx) {
}
#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;
for (unsigned i = 0; i < n.lits().size(); ++i) {
switch (ctx.get_assignment(n.lits(i))) {
case l_false:
return true;
case l_true:
break;
case l_undef:
++num_undef_lits;
break;
}
}
unsigned_vector unchanged;
dependency* new_deps = 0;
vector<expr_ref_vector> new_ls, new_rs;
literal_vector new_lits = n.lits();
bool updated = false;
for (unsigned i = 0; i < n.ls().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_ref_vector const& l = n.ls(i);
expr_ref_vector const& r = n.rs(i);
change = canonize(l, ls, deps) || change;
change = canonize(r, rs, deps) || change;
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs)) {
return true;
}
else if (!change && lhs.empty()) {
unchanged.push_back(i);
}
else if (change && lhs.empty()) {
}
else {
updated = true;
TRACE("seq",
for (unsigned j = 0; j < lhs.size(); ++j) {
tout << mk_pp(lhs[j].get(), m) << " ";
}
tout << "\n";
tout << l << " != " << r << "\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)) {
new_ls.push_back(nl);
new_rs.push_back(nr);
}
else {
literal lit(mk_eq(nl, nr, false));
ctx.mark_as_relevant(lit);
new_lits.push_back(lit);
switch (ctx.get_assignment(lit)) {
case l_false:
return true;
case l_true:
break;
case l_undef:
++num_undef_lits;
m_new_propagation = true;
break;
}
}
}
new_deps = deps;
}
}
if (num_undef_lits == 1 && new_ls.empty()) {
literal_vector lits;
literal undef_lit = null_literal;
for (unsigned i = 0; i < new_lits.size(); ++i) {
literal lit = new_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(new_deps, lits.size(), lits.c_ptr(), ~undef_lit);
return true;
}
else if (num_undef_lits == 0 && new_ls.empty()) {
set_conflict(new_deps, new_lits);
SASSERT(m_new_propagation);
return true;
}
else if (change) {
}
return change;
}
#endif
void theory_seq::mark_solved(unsigned idx) {
m_trail_stack.push(solved_ne(*this, idx));
}
@ -1152,8 +1300,8 @@ void theory_seq::display(std::ostream & out) const {
void theory_seq::display_equations(std::ostream& out) const {
for (unsigned i = 0; i < m_eqs.size(); ++i) {
eq const& e = m_eqs[i];
out << e.m_lhs << " = " << e.m_rhs << " <- ";
display_deps(out, e.m_dep);
out << e.ls() << " = " << e.rs() << " <- ";
display_deps(out, e.dep());
}
}
@ -1381,13 +1529,14 @@ expr_ref theory_seq::canonize(expr* e, dependency*& eqs) {
return result;
}
void theory_seq::canonize(expr* e0, expr_ref_vector& es, dependency*& eqs) {
bool theory_seq::canonize(expr* e0, expr_ref_vector& es, dependency*& eqs) {
dependency* dep = 0;
expr* e = m_rep.find(e0, dep);
bool change = e != e0;
expr* e1, *e2;
if (m_util.str.is_concat(e, e1, e2)) {
canonize(e1, es, eqs);
canonize(e2, es, eqs);
change = canonize(e1, es, eqs) || change;
change = canonize(e2, es, eqs) || change;
}
else if (m_util.str.is_empty(e)) {
// skip
@ -1395,15 +1544,34 @@ void theory_seq::canonize(expr* e0, expr_ref_vector& es, dependency*& eqs) {
else {
expr_ref e3 = expand(e, eqs);
if (m_util.str.is_concat(e3) || m_util.str.is_empty(e3)) {
canonize(e3, es, eqs);
change = canonize(e3, es, eqs) || change;
}
else {
change = e3 != e || change;
es.push_back(e3);
}
}
eqs = m_dm.mk_join(eqs, dep);
return change;
}
bool theory_seq::canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs) {
dependency* dep = 0;
bool change = false;
for (unsigned i = 0; i < es.size(); ++i) {
expr_ref r = expand(es[i], eqs);
change |= r != es[i];
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;
}
expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
expr_ref result(m);
dependency* deps = 0;
@ -1416,7 +1584,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
expr* e = m_rep.find(e0, deps);
expr* e1, *e2;
if (m_util.str.is_concat(e, e1, e2)) {
result = m_util.str.mk_concat(expand(e1, deps), expand(e2, deps));
result = mk_concat(expand(e1, deps), expand(e2, deps));
}
else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) {
result = e;
@ -1515,10 +1683,10 @@ void theory_seq::deque_axiom(expr* n) {
void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) {
expr_ref s1 = mk_skolem(m_seq_first, s);
expr_ref c = mk_last(s);
expr_ref s1c(m_util.str.mk_concat(s1, m_util.str.mk_unit(c)), m);
expr_ref s1c = mk_concat(s1, m_util.str.mk_unit(c));
literal s_eq_emp = mk_eq_empty(s);
add_axiom(lit1, lit2, s_eq_emp, mk_eq(s, s1c, false));
add_axiom(lit1, lit2, s_eq_emp, ~mk_literal(m_util.str.mk_prefix(s, m_util.str.mk_concat(x, s1))));
add_axiom(lit1, lit2, s_eq_emp, ~mk_literal(m_util.str.mk_prefix(s, mk_concat(x, s1))));
}
/*
@ -1564,7 +1732,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
if (m_autil.is_numeral(offset, r) && r.is_zero()) {
expr_ref x = mk_skolem(m_contains_left, t, s);
expr_ref y = mk_skolem(m_contains_right, t, s);
xsy = m_util.str.mk_concat(x,s,y);
xsy = mk_concat(x,s,y);
literal cnt = mk_literal(m_util.str.mk_contains(t, s));
literal eq_empty = mk_eq_empty(s);
add_axiom(cnt, mk_eq(i, minus_one, false));
@ -1585,7 +1753,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, m_util.str.mk_concat(x, y), false));
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_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));
@ -1608,8 +1776,8 @@ void theory_seq::add_replace_axiom(expr* r) {
VERIFY(m_util.str.is_replace(r, a, s, t));
expr_ref x = mk_skolem(m_contains_left, a, s);
expr_ref y = mk_skolem(m_contains_right, a, s);
expr_ref xty(m_util.str.mk_concat(x, t, y), m);
expr_ref xsy(m_util.str.mk_concat(x, s, y), m);
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));
@ -1626,7 +1794,7 @@ void theory_seq::add_elim_string_axiom(expr* n) {
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;
result = m_util.str.mk_concat(m_util.str.mk_unit(m_util.str.mk_char(s, i)), result);
result = mk_concat(m_util.str.mk_unit(m_util.str.mk_char(s, i)), result);
}
add_axiom(mk_eq(n, result, false));
m_rep.update(n, result, 0);
@ -1654,11 +1822,6 @@ void theory_seq::add_length_axiom(expr* n) {
SASSERT(n != len);
add_axiom(mk_eq(len, n, false));
//std::cout << len << "\n";
//len = m_autil.mk_add(len, m_autil.mk_mul(m_autil.mk_int(-1), n));
//TRACE("seq", tout << "Add length coherence for " << mk_pp(n, m) << "\n";);
//add_axiom(mk_literal(m_autil.mk_le(len, m_autil.mk_int(0))));
//add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(0))));
m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
}
else {
@ -1846,7 +2009,7 @@ void theory_seq::add_extract_axiom(expr* e) {
expr_ref lx(m_util.str.mk_length(x), m);
expr_ref le(m_util.str.mk_length(e), m);
expr_ref ls_minus_i(mk_sub(ls, i), m);
expr_ref xe(m_util.str.mk_concat(x, e), m);
expr_ref xe = mk_concat(x, e);
expr_ref zero(m_autil.mk_int(0), m);
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
@ -1872,7 +2035,7 @@ void theory_seq::add_at_axiom(expr* e) {
expr_ref x(m), y(m), lx(m), le(m), xey(m), zero(m), one(m), len_e(m), len_x(m);
x = mk_skolem(m_at_left, s);
y = mk_skolem(m_at_right, s);
xey = m_util.str.mk_concat(x, e, y);
xey = mk_concat(x, e, y);
zero = m_autil.mk_int(0);
one = m_autil.mk_int(1);
len_e = m_util.str.mk_length(e);
@ -1914,38 +2077,24 @@ void theory_seq::propagate_step(literal lit, expr* step) {
void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) {
context& ctx = get_context();
rational r;
SASSERT(ctx.get_assignment(lit) == l_true);
VERIFY(m_autil.is_numeral(idx, r) && r.is_unsigned());
unsigned _idx = r.get_unsigned();
dependency* dep = 0;
expr_ref s1 = canonize(s, dep);
ptr_vector<expr> es;
expr* e1;
expr_ref nth = mk_nth(s, idx);
expr_ref head(m), tail(m), conc(m);
expr_ref head(m), tail(m), conc(m), len1(m), len2(m);
expr_ref_vector elems(m);
get_concat(s1, es);
unsigned i = 0;
for (; i <= _idx && i < es.size() && m_util.str.is_unit(es[i]); ++i) {};
if (i == _idx && i < es.size() && m_util.str.is_unit(es[i], e1)) {
dep = m_dm.mk_join(dep, m_dm.mk_leaf(assumption(lit)));
propagate_eq(dep, ensure_enode(nth), ensure_enode(e1));
return;
}
// TBD could tune this aggregate quadratic overhead
expr* s2 = s;
for (unsigned j = 0; j <= _idx; ++j) {
mk_decompose(s2, head, tail);
elems.push_back(head);
len1 = m_util.str.mk_length(s2);
len2 = m_autil.mk_add(m_autil.mk_int(1), m_util.str.mk_length(tail));
propagate_eq(lit, len1, len2, false);
s2 = tail;
}
elems.push_back(s2);
conc = m_util.str.mk_concat(elems.size(), elems.c_ptr());
conc = mk_concat(elems);
propagate_eq(lit, s, conc, true);
// TBD: examine other places for enforcing constraints on tail
conc = m_autil.mk_add(m_autil.mk_int(_idx+1), m_util.str.mk_length(s2));
add_axiom(~lit, mk_eq(m_util.str.mk_length(s), conc, false));
//add_axiom(~lit, mk_literal(m_autil.mk_ge(m_util.str.mk_length(s), m_autil.mk_int(_idx + 1))));
}
literal theory_seq::mk_literal(expr* _e) {
@ -2037,7 +2186,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
if (m_util.str.is_prefix(e, e1, e2)) {
if (is_true) {
f = mk_skolem(m_prefix, e1, e2);
f = m_util.str.mk_concat(e1, f);
f = mk_concat(e1, f);
propagate_eq(lit, f, e2, true);
}
else {
@ -2051,7 +2200,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
else if (m_util.str.is_suffix(e, e1, e2)) {
if (is_true) {
f = mk_skolem(m_suffix, e1, e2);
f = m_util.str.mk_concat(f, e1);
f = mk_concat(f, e1);
propagate_eq(lit, f, e2, true);
}
else {
@ -2061,7 +2210,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
// lit => e1 = first ++ (unit last)
expr_ref f1 = mk_skolem(m_seq_first, e1);
expr_ref f2 = mk_last(e1);
f = m_util.str.mk_concat(f1, m_util.str.mk_unit(f2));
f = mk_concat(f1, m_util.str.mk_unit(f2));
propagate_eq(lit, e1, f, true);
if (add_suffix2suffix(e)) {
@ -2073,7 +2222,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
if (is_true) {
expr_ref f1 = mk_skolem(m_contains_left, e1, e2);
expr_ref f2 = mk_skolem(m_contains_right, e1, e2);
f = m_util.str.mk_concat(f1, e2, f2);
f = mk_concat(f1, e2, f2);
propagate_eq(lit, f, e1, true);
}
else if (!canonizes(false, e)) {
@ -2131,7 +2280,7 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
expr_ref o1(n1->get_owner(), m);
expr_ref o2(n2->get_owner(), m);
TRACE("seq", tout << o1 << " = " << o2 << "\n";);
m_eqs.push_back(eq(o1, o2, deps));
m_eqs.push_back(mk_eqdep(o1, o2, deps));
solve_eqs(m_eqs.size()-1);
enforce_length_coherence(n1, n2);
}
@ -2555,7 +2704,7 @@ bool theory_seq::add_suffix2suffix(expr* e) {
expr_ref last2 = mk_last(e2);
expr_ref first1 = mk_skolem(m_seq_first, e1);
expr_ref last1 = mk_last(e1);
expr_ref conc(m_util.str.mk_concat(first2, m_util.str.mk_unit(last2)), m);
expr_ref conc = mk_concat(first2, m_util.str.mk_unit(last2));
propagate_eq(~mk_eq(e2, emp, false), e2, conc);
literal last_eq = mk_eq(last1, last2, false);

113
src/smt/theory_seq.h
View file

@ -106,14 +106,72 @@ namespace smt {
};
// Asserted or derived equality with dependencies
struct eq {
expr_ref m_lhs;
expr_ref m_rhs;
dependency* m_dep;
eq(expr_ref& l, expr_ref& r, dependency* d):
m_lhs(l), m_rhs(r), m_dep(d) {}
eq(eq const& other): m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_dep(other.m_dep) {}
eq& operator=(eq const& other) { m_lhs = other.m_lhs; m_rhs = other.m_rhs; m_dep = other.m_dep; return *this; }
class eq {
unsigned m_id;
expr_ref_vector m_lhs;
expr_ref_vector m_rhs;
dependency* m_dep;
public:
eq(unsigned id, expr_ref_vector& l, expr_ref_vector& r, dependency* d):
m_id(id), m_lhs(l), m_rhs(r), m_dep(d) {}
eq(eq const& other): m_id(other.m_id), m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_dep(other.m_dep) {}
eq& operator=(eq const& other) {
if (this != &other) {
m_lhs.reset();
m_rhs.reset();
m_lhs.append(other.m_lhs);
m_rhs.append(other.m_rhs);
m_dep = other.m_dep;
m_id = other.m_id;
}
return *this;
}
expr_ref_vector const& ls() const { return m_lhs; }
expr_ref_vector const& rs() const { return m_rhs; }
dependency* dep() const { return m_dep; }
unsigned id() const { return m_id; }
};
eq mk_eqdep(expr* l, expr* r, dependency* dep) {
expr_ref_vector ls(m), rs(m);
m_util.str.get_concat(l, ls);
m_util.str.get_concat(r, rs);
return eq(m_eq_id++, ls, rs, dep);
}
class ne2 {
vector<expr_ref_vector> m_lhs;
vector<expr_ref_vector> m_rhs;
literal_vector m_lits;
dependency* m_dep;
public:
ne2(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep):
m_dep(dep) {
m_lhs.push_back(l);
m_rhs.push_back(r);
}
ne2(ne2 const& other):
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) {
if (this != &other) {
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;
}
vector<expr_ref_vector> const& ls() const { return m_lhs; }
vector<expr_ref_vector> const& rs() const { return m_rhs; }
expr_ref_vector const& ls(unsigned i) const { return m_lhs[i]; }
expr_ref_vector const& rs(unsigned i) const { return m_rhs[i]; }
literal_vector const& lits() const { return m_lits; }
literal lits(unsigned i) const { return m_lits[i]; }
dependency* dep() const { return m_dep; }
};
@ -282,13 +340,11 @@ namespace smt {
};
class pop_branch : public trail<theory_seq> {
expr_ref m_l, m_r;
unsigned k;
public:
pop_branch(ast_manager& m, expr* l, expr* r): m_l(l, m), m_r(r, m) {}
pop_branch(unsigned k): k(k) {}
virtual void undo(theory_seq& th) {
th.m_branch_start.erase(m_l, m_r);
m_l.reset();
m_r.reset();
th.m_branch_start.erase(k);
}
};
@ -311,6 +367,7 @@ namespace smt {
solution_map m_rep; // unification representative.
scoped_vector<eq> m_eqs; // set of current equations.
scoped_vector<ne> m_nqs; // set of current disequalities.
unsigned m_eq_id;
seq_factory* m_factory; // value factory
exclusion_table m_exclude; // set of asserted disequalities.
@ -322,6 +379,7 @@ namespace smt {
scoped_ptr_vector<apply> m_replay; // set of actions to replay
model_generator* m_mg;
th_rewriter m_rewrite;
seq_rewriter m_seq_rewrite;
seq_util m_util;
arith_util m_autil;
th_trail_stack m_trail_stack;
@ -375,21 +433,20 @@ namespace smt {
bool propagate_length_coherence(expr* e);
bool solve_eqs(unsigned start);
bool solve_eq(expr* l, expr* r, dependency* dep);
bool simplify_eq(expr* l, expr* r, dependency* dep);
bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
bool solve_unit_eq(expr* l, expr* r, dependency* dep);
bool is_binary_eq(expr* l, expr* r, expr*& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr*& y);
bool solve_binary_eq(expr* l, expr* r, dependency* dep);
bool solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
bool is_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, expr*& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr*& y);
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);
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* 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); }
bool solve_nqs(unsigned i);
void solve_ne(unsigned i);
bool unchanged(expr* e, expr_ref_vector& es) const { return es.size() == 1 && es[0] == e; }
bool unchanged(expr* e, expr_ref_vector& es, expr* f, expr_ref_vector& fs) const {
return
(unchanged(e, es) && unchanged(f, fs)) ||
(unchanged(e, fs) && unchanged(e, fs));
}
// asserting consequences
void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;
@ -399,15 +456,16 @@ namespace smt {
void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs = false);
void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
obj_pair_map<expr, expr, unsigned> m_branch_start;
void insert_branch_start(expr* l, expr* r, unsigned s);
unsigned find_branch_start(expr* l, expr* r);
u_map<unsigned> m_branch_start;
void insert_branch_start(unsigned k, unsigned s);
unsigned find_branch_start(unsigned k);
bool find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs);
bool can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs) const;
lbool assume_equality(expr* l, expr* r);
// variable solving utilities
bool occurs(expr* a, expr* b);
bool occurs(expr* a, expr_ref_vector const& b);
bool is_var(expr* b);
bool add_solution(expr* l, expr* r, dependency* dep);
bool is_nth(expr* a) const;
@ -415,7 +473,8 @@ namespace smt {
expr_ref mk_nth(expr* s, expr* idx);
expr_ref mk_last(expr* e);
expr_ref canonize(expr* e, dependency*& eqs);
void canonize(expr* e, expr_ref_vector& es, dependency*& eqs);
bool canonize(expr* e, expr_ref_vector& es, dependency*& eqs);
bool canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs);
expr_ref expand(expr* e, dependency*& eqs);
void add_dependency(dependency*& dep, enode* a, enode* b);