mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 13:40:52 +00:00
Code Activity

updates to seq and bug fixes (#4056)

Browse source 
* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4037

* nicer output for skolem functions

* more overhaul of seq, some bug fixes

* na

* added offset_eq file

* na

* fix #4044

* fix #4040

* fix #4045

* updated ignore

* new rewrites for indexof based on #4036

* add shortcuts

* updated ne solver for seq, fix #4025

* use pair vectors for equalities that are reduced by seq_rewriter

* use erase_and_swap

* remove unit-walk

* na

* add check for #3200

* nits

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* name a type

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove fp check

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove unsound axiom instantiation for non-contains

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix rewrites

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4053

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4052

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-22 13:18:55 -07:00 • committed by GitHub
parent 53c14bd554
commit 95a78b2450
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
39 changed files with 1516 additions and 1654 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/CMakeLists.txt
View file

@ -15,6 +15,8 @@ z3_add_component(smt
seq_axioms.cpp
seq_skolem.cpp
seq_eq_solver.cpp
seq_ne_solver.cpp
seq_offset_eq.cpp
smt_almost_cg_table.cpp
smt_arith_value.cpp
smt_case_split_queue.cpp

112
src/smt/seq_axioms.cpp
View file

@ -88,8 +88,12 @@ this translates to:
void seq_axioms::add_extract_axiom(expr* e) {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
expr* s = nullptr, *i = nullptr, *l = nullptr;
VERIFY(seq.str.is_extract(e, s, i, l));
expr* _s = nullptr, *_i = nullptr, *_l = nullptr;
VERIFY(seq.str.is_extract(e, _s, _i, _l));
expr_ref s(_s, m), i(_i, m), l(_l, m);
m_rewrite(s);
m_rewrite(i);
if (l) m_rewrite(l);
if (is_tail(s, i, l)) {
add_tail_axiom(e, s);
return;
@ -294,14 +298,16 @@ void seq_axioms::tightest_prefix(expr* s, expr* x) {
(len(s) <= len(t) -> i <= len(t)-len(s))
*/
void seq_axioms::add_indexof_axiom(expr* i) {
expr* s = nullptr, *t = nullptr, *offset = nullptr;
expr* _s = nullptr, *_t = nullptr, *_offset = nullptr;
rational r;
VERIFY(seq.str.is_index(i, t, s) ||
seq.str.is_index(i, t, s, offset));
VERIFY(seq.str.is_index(i, _t, _s) ||
seq.str.is_index(i, _t, _s, _offset));
expr_ref minus_one(a.mk_int(-1), m);
expr_ref zero(a.mk_int(0), m);
expr_ref xsy(m);
expr_ref xsy(m), t(_t, m), s(_s, m), offset(_offset, m);
m_rewrite(t);
m_rewrite(s);
if (offset) m_rewrite(offset);
literal cnt = mk_literal(seq.str.mk_contains(t, s));
literal i_eq_m1 = mk_eq(i, minus_one);
literal i_eq_0 = mk_eq(i, zero);
@ -375,8 +381,11 @@ void seq_axioms::add_indexof_axiom(expr* i) {
*/
void seq_axioms::add_last_indexof_axiom(expr* i) {
expr* s = nullptr, *t = nullptr;
VERIFY(seq.str.is_last_index(i, t, s));
expr* _s = nullptr, *_t = nullptr;
VERIFY(seq.str.is_last_index(i, _t, _s));
expr_ref s(_s, m), t(_t, m);
m_rewrite(s);
m_rewrite(t);
expr_ref minus_one(a.mk_int(-1), m);
expr_ref zero(a.mk_int(0), m);
expr_ref s_head(m), s_tail(m);
@ -417,8 +426,12 @@ void seq_axioms::add_last_indexof_axiom(expr* i) {
*/
void seq_axioms::add_replace_axiom(expr* r) {
expr* u = nullptr, *s = nullptr, *t = nullptr;
VERIFY(seq.str.is_replace(r, u, s, t));
expr* _u = nullptr, *_s = nullptr, *_t = nullptr;
VERIFY(seq.str.is_replace(r, _u, _s, _t));
expr_ref u(_u, m), s(_s, m), t(_t, m);
m_rewrite(u);
m_rewrite(s);
m_rewrite(t);
expr_ref x = m_sk.mk_indexof_left(u, s);
expr_ref y = m_sk.mk_indexof_right(u, s);
expr_ref xty = mk_concat(x, t, y);
@ -445,8 +458,11 @@ void seq_axioms::add_replace_axiom(expr* r) {
*/
void seq_axioms::add_at_axiom(expr* e) {
TRACE("seq", tout << "at-axiom: " << ctx().get_scope_level() << " " << mk_bounded_pp(e, m) << "\n";);
expr* s = nullptr, *i = nullptr;
VERIFY(seq.str.is_at(e, s, i));
expr* _s = nullptr, *_i = nullptr;
VERIFY(seq.str.is_at(e, _s, _i));
expr_ref s(_s, m), i(_i, m);
m_rewrite(s);
m_rewrite(i);
expr_ref zero(a.mk_int(0), m);
expr_ref one(a.mk_int(1), m);
expr_ref emp(seq.str.mk_empty(m.get_sort(e)), m);
@ -465,7 +481,7 @@ void seq_axioms::add_at_axiom(expr* e) {
}
nth = es.back();
es.push_back(m_sk.mk_tail(s, i));
add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, seq.str.mk_concat(es)));
add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, seq.str.mk_concat(es, m.get_sort(e))));
add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(nth, e));
}
else {
@ -513,9 +529,11 @@ void seq_axioms::add_nth_axiom(expr* e) {
void seq_axioms::add_itos_axiom(expr* e) {
expr* n = nullptr;
expr* _n = nullptr;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(seq.str.is_itos(e, n));
VERIFY(seq.str.is_itos(e, _n));
expr_ref n(_n, m);
m_rewrite(n);
// itos(n) = "" <=> n < 0
expr_ref zero(a.mk_int(0), m);
@ -575,8 +593,10 @@ Define auxiliary function with the property:
*/
void seq_axioms::add_stoi_axiom(expr* e, unsigned k) {
SASSERT(k > 0);
expr* s = nullptr;
VERIFY (seq.str.is_stoi(e, s));
expr* _s = nullptr;
VERIFY (seq.str.is_stoi(e, _s));
expr_ref s(_s, m);
m_rewrite(s);
auto stoi2 = [&](unsigned j) { return m_sk.mk("seq.stoi", s, a.mk_int(j), a.mk_int()); };
auto digit = [&](unsigned j) { return m_sk.mk_digit2int(mk_nth(s, j)); };
expr_ref len = mk_len(s);
@ -682,17 +702,20 @@ void seq_axioms::ensure_digit_axiom() {
!(e1 < e2) or !(e2 < e1)
*/
void seq_axioms::add_lt_axiom(expr* n) {
expr* e1 = nullptr, *e2 = nullptr;
VERIFY(seq.str.is_lt(n, e1, e2));
expr* _e1 = nullptr, *_e2 = nullptr;
VERIFY(seq.str.is_lt(n, _e1, _e2));
expr_ref e1(_e1, m), e2(_e2, m);
m_rewrite(e1);
m_rewrite(e2);
sort* s = m.get_sort(e1);
sort* char_sort = nullptr;
VERIFY(seq.is_seq(s, char_sort));
literal lt = mk_literal(n);
expr_ref x = m_sk.mk(symbol("str.lt.x"), e1, e2);
expr_ref y = m_sk.mk(symbol("str.lt.y"), e1, e2);
expr_ref z = m_sk.mk(symbol("str.lt.z"), e1, e2);
expr_ref c = m_sk.mk(symbol("str.lt.c"), e1, e2, char_sort);
expr_ref d = m_sk.mk(symbol("str.lt.d"), e1, e2, char_sort);
expr_ref x = m_sk.mk("str.<.x", e1, e2);
expr_ref y = m_sk.mk("str.<.y", e1, e2);
expr_ref z = m_sk.mk("str.<.z", e1, e2);
expr_ref c = m_sk.mk("str.<.c", e1, e2, char_sort);
expr_ref d = m_sk.mk("str.<.d", e1, e2, char_sort);
expr_ref xcy = mk_concat(x, seq.str.mk_unit(c), y);
expr_ref xdz = mk_concat(x, seq.str.mk_unit(d), z);
literal eq = mk_eq(e1, e2);
@ -747,8 +770,11 @@ void seq_axioms::add_unit_axiom(expr* n) {
*/
void seq_axioms::add_suffix_axiom(expr* e) {
expr* s = nullptr, *t = nullptr;
VERIFY(seq.str.is_suffix(e, s, t));
expr* _s = nullptr, *_t = nullptr;
VERIFY(seq.str.is_suffix(e, _s, _t));
expr_ref s(_s, m), t(_t, m);
m_rewrite(s);
m_rewrite(t);
literal lit = mk_literal(e);
literal s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1);
sort* char_sort = nullptr;
@ -764,8 +790,11 @@ void seq_axioms::add_suffix_axiom(expr* e) {
}
void seq_axioms::add_prefix_axiom(expr* e) {
expr* s = nullptr, *t = nullptr;
VERIFY(seq.str.is_prefix(e, s, t));
expr* _s = nullptr, *_t = nullptr;
VERIFY(seq.str.is_prefix(e, _s, _t));
expr_ref s(_s, m), t(_t, m);
m_rewrite(s);
m_rewrite(t);
literal lit = mk_literal(e);
literal s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1);
sort* char_sort = nullptr;
@ -806,6 +835,31 @@ void seq_axioms::add_length_axiom(expr* n) {
}
}
/**
~contains(a, b) => ~prefix(b, a)
~contains(a, b) => ~contains(tail(a), b) or a = empty
~contains(a, b) & a = empty => b != empty
~(a = empty) => a = head + tail
*/
void seq_axioms::unroll_not_contains(expr* e) {
expr_ref head(m), tail(m);
expr* a = nullptr, *b = nullptr;
VERIFY(seq.str.is_contains(e, a, b));
m_sk.decompose(a, head, tail);
expr_ref pref(seq.str.mk_prefix(b, a), m);
expr_ref postf(seq.str.mk_contains(tail, b), m);
m_rewrite(pref);
m_rewrite(postf);
literal pre = mk_literal(pref);
literal cnt = mk_literal(e);
literal ctail = mk_literal(postf);
literal emp = mk_eq_empty(a, true);
add_axiom(cnt, ~pre);
add_axiom(cnt, ~ctail);
add_axiom(~emp, mk_eq_empty(tail));
add_axiom(emp, mk_eq(a, seq.str.mk_concat(head, tail)));
}
expr_ref seq_axioms::add_length_limit(expr* s, unsigned k) {
expr_ref bound_tracker = m_sk.mk_length_limit(s, k);

1
src/smt/seq_axioms.h
View file

@ -86,6 +86,7 @@ namespace smt {
void add_le_axiom(expr* n);
void add_unit_axiom(expr* n);
void add_length_axiom(expr* n);
void unroll_not_contains(expr* n);
literal is_digit(expr* ch);
literal mk_ge(expr* e, int k) { return mk_ge_e(e, a.mk_int(k)); }

522
src/smt/seq_eq_solver.cpp
View file

@ -31,15 +31,9 @@ bool theory_seq::solve_eqs(unsigned i) {
context& ctx = get_context();
bool change = false;
for (; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
eq const& e = m_eqs[i];
if (solve_eq(e.ls(), e.rs(), e.dep(), i)) {
if (i + 1 != m_eqs.size()) {
eq e1 = m_eqs[m_eqs.size()-1];
m_eqs.set(i, e1);
--i;
}
if (solve_eq(i)) {
m_eqs.erase_and_swap(i--);
++m_stats.m_num_reductions;
m_eqs.pop_back();
change = true;
}
TRACE("seq_verbose", display_equations(tout););
@ -47,20 +41,23 @@ bool theory_seq::solve_eqs(unsigned i) {
return change || m_new_propagation || ctx.inconsistent();
}
bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps, unsigned idx) {
bool theory_seq::solve_eq(unsigned idx) {
const eq& e = m_eqs[idx];
context& ctx = get_context();
expr_ref_vector& ls = m_ls;
expr_ref_vector& rs = m_rs;
rs.reset(); ls.reset();
m_ls.reset();
m_rs.reset();
dependency* dep2 = nullptr;
bool change = false;
if (!canonize(l, ls, dep2, change)) return false;
if (!canonize(r, rs, dep2, change)) return false;
deps = m_dm.mk_join(dep2, deps);
TRACE("seq_verbose", tout << l << " = " << r << " ==> ";
if (!canonize(e.ls(), ls, dep2, change)) return false;
if (!canonize(e.rs(), rs, dep2, change)) return false;
dependency* deps = m_dm.mk_join(dep2, e.dep());
TRACE("seq_verbose",
tout << e.ls() << " = " << e.rs() << " ==> ";
tout << ls << " = " << rs << "\n";
display_deps(tout, deps);
);
display_deps(tout, deps););
if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) {
TRACE("seq", tout << "simplified\n";);
return true;
@ -91,22 +88,16 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
}
if (!ctx.inconsistent() && change) {
// The propagation step from arithmetic state (e.g. length offset) to length constraints
if (get_context().get_scope_level() == 0) {
prop_arith_to_len_offset();
}
TRACE("seq", tout << "inserting equality\n";);
bool updated = false;
expr_ref_vector new_ls(m);
if (!m_len_offset.empty() &&
find_better_rep(ls, rs, idx, deps, new_ls)) {
if (!m_offset_eq.empty() && find_better_rep(ls, rs, idx, deps, new_ls)) {
// Find a better equivalent term for lhs of an equation based on length constraints
m_eqs.push_back(eq(m_eq_id++, new_ls, rs, deps));
return true;
}
else {
m_eqs.push_back(eq(m_eq_id++, ls, rs, deps));
m_eqs.set(idx, eq(m_eq_id++, ls, rs, deps));
}
TRACE("seq", tout << "simplified\n";);
return true;
}
return false;
}
@ -138,10 +129,8 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
context& ctx = get_context();
ptr_vector<expr> xs, ys;
expr_ref x(m), y(m);
bool is_binary =
is_binary_eq(ls, rs, x, xs, ys, y) ||
is_binary_eq(rs, ls, x, xs, ys, y);
if (!is_binary) {
if (!is_binary_eq(ls, rs, x, xs, ys, y) &&
!is_binary_eq(rs, ls, x, xs, ys, y)) {
return false;
}
// Equation is of the form x ++ xs = ys ++ y
@ -227,9 +216,44 @@ bool theory_seq::occurs(expr* a, expr* b) {
return false;
}
// TODO: propagate length offsets for last vars
/**
\brief
This step performs destructive superposition
Based on the implementation it would do the following:
e: l1 + l2 + l3 + l = r1 + r2 + r
G |- len(l1) = len(l2) = len(r1) = 0
e': l1 + l2 + l3 + l = r3 + r' occurs prior to e among equations
G |- len(r3) = len(r2)
r2, r3 are not identical
----------------------------------
e'' : l1 + l2 + l3 + l = r3 + r'
e: l1 + l2 + l3 + l = r1 + r2 + r
G |- len(l1) = len(l2) = len(r1) = 0
e': l1 + l2 + l3 + l = r3 + r' occurs prior to e among equations
G |- len(r3) = len(r2) + offset
r2, r3 are not identical
----------------------------------
e'' : l1 + l2 + l3 + l = r3 + r'
NB, this doesn't make sense because e'' is just e', which already occurs.
It doesn't inherit the constraints from e either, which would get lost.
NB, if len(r3) = len(r2) would be used, then the justification for the equality
needs to be tracked in dependencies.
TODO: propagate length offsets for last vars
*/
bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned idx,
dependency*& deps, expr_ref_vector & res) {
// disabled until functionality is clarified
return false;
context& ctx = get_context();
if (ls.empty() || rs.empty())
@ -251,7 +275,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
// Offset = 0, No change
if (l_fst && get_root(len_l_fst) == root2) {
TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst, m) << ")\n";);
return false;
}
@ -265,7 +289,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
nl_fst = e.rs().get(0);
if (nl_fst && nl_fst != r_fst && root2 == get_root(mk_len(nl_fst))) {
res.reset();
res.append(e.rs().size(), e.rs().c_ptr());
res.append(e.rs());
deps = m_dm.mk_join(e.dep(), deps);
return true;
}
@ -273,38 +297,27 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
// Offset != 0, No change
if (l_fst && ctx.e_internalized(len_l_fst)) {
enode * root1 = get_root(len_l_fst);
obj_map<enode, int> tmp;
int offset;
if (!m_autil.is_numeral(root1->get_owner()) && !m_autil.is_numeral(root2->get_owner())) {
if (m_len_offset.find(root1, tmp) && tmp.find(root2, offset)) {
TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
find_max_eq_len(ls, rs);
return false;
}
else if (m_len_offset.find(root2, tmp) && tmp.find(root1, offset)) {
TRACE("seq", tout << "(" << mk_pp(r_fst, m) << ", " << mk_pp(l_fst,m) << ")\n";);
find_max_eq_len(ls ,rs);
return false;
}
if (m_offset_eq.contains(root1, root2)) {
TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
find_max_eq_len(ls, rs);
return false;
}
}
// Offset != 0, Changed
obj_map<enode, int> tmp;
if (!m_autil.is_numeral(root2->get_owner()) && m_len_offset.find(root2, tmp)) {
if (m_offset_eq.contains(root2)) {
for (unsigned i = 0; i < idx; ++i) {
eq const& e = m_eqs[i];
if (e.ls() != ls) continue;
expr* nl_fst = nullptr;
if (e.rs().size()>1 && is_var(e.rs().get(0)))
if (e.rs().size() > 1 && is_var(e.rs().get(0)))
nl_fst = e.rs().get(0);
if (nl_fst && nl_fst != r_fst) {
int offset;
expr_ref len_nl_fst = mk_len(nl_fst);
if (ctx.e_internalized(len_nl_fst)) {
enode * root1 = ctx.get_enode(len_nl_fst)->get_root();
if (!m_autil.is_numeral(root1->get_owner()) && tmp.find(root1, offset)) {
enode * root1 = get_root(len_nl_fst);
if (m_offset_eq.contains(root2, root1)) {
res.reset();
res.append(e.rs().size(), e.rs().c_ptr());
res.append(e.rs());
deps = m_dm.mk_join(e.dep(), deps);
find_max_eq_len(res, rs);
return true;
@ -329,12 +342,12 @@ bool theory_seq::has_len_offset(expr_ref_vector const& ls, expr_ref_vector const
expr_ref len_l_fst = mk_len(l_fst);
if (!ctx.e_internalized(len_l_fst))
return false;
enode * root1 = ctx.get_enode(len_l_fst)->get_root();
enode * root1 = get_root(len_l_fst);
expr_ref len_r_fst = mk_len(r_fst);
if (!ctx.e_internalized(len_r_fst))
return false;
enode* root2 = ctx.get_enode(len_r_fst)->get_root();
enode* root2 = get_root(len_r_fst);
if (root1 == root2) {
TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
@ -342,43 +355,30 @@ bool theory_seq::has_len_offset(expr_ref_vector const& ls, expr_ref_vector const
return true;
}
if (m_autil.is_numeral(root1->get_owner()) || m_autil.is_numeral(root2->get_owner()))
return false;
obj_map<enode, int> tmp;
if (m_len_offset.find(root1, tmp) && tmp.find(root2, offset)) {
TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << ")\n";);
return true;
}
if (m_len_offset.find(root2, tmp) && tmp.find(root1, offset)) {
offset = -offset;
TRACE("seq", tout << "(" << mk_pp(r_fst, m) << ", " << mk_pp(l_fst,m) << ")\n";);
if (m_offset_eq.find(root1, root2, offset)) {
TRACE("seq", tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << " " << offset << ")\n";);
return true;
}
return false;
}
bool theory_seq::len_based_split() {
unsigned sz = m_eqs.size();
if (sz == 0)
return false;
if ((int) get_context().get_scope_level() > m_len_prop_lvl) {
m_len_prop_lvl = get_context().get_scope_level();
prop_arith_to_len_offset();
if (!m_len_offset.empty()) {
for (unsigned i = sz-1; i > 0; --i) {
eq const& e = m_eqs[i];
expr_ref_vector new_ls(m);
dependency *deps = e.dep();
if (find_better_rep(e.ls(), e.rs(), i, deps, new_ls)) {
expr_ref_vector rs(m);
rs.append(e.rs().size(), e.rs().c_ptr());
m_eqs.set(i, eq(m_eq_id++, new_ls, rs, deps));
TRACE("seq", display_equation(tout, m_eqs[i]););
}
if (false && m_offset_eq.propagate() && !m_offset_eq.empty()) {
// NB: disabled until find_better_rep is handled.
#if 0
for (unsigned i = m_eqs.size(); i-- > 0; ) {
eq const& e = m_eqs[i];
expr_ref_vector new_ls(m);
dependency *deps = e.dep();
if (find_better_rep(e.ls(), e.rs(), i, deps, new_ls)) {
expr_ref_vector rs(m);
rs.append(e.rs());
m_eqs.set(i, eq(m_eq_id++, new_ls, rs, deps));
TRACE("seq", display_equation(tout, m_eqs[i]););
}
}
#endif
}
for (auto const& e : m_eqs) {
@ -389,44 +389,60 @@ bool theory_seq::len_based_split() {
return false;
}
/*
ls = x11 + x12 for len(x11) = len(y11)
rs = y11 + y12
ls = x11 + Z + x12 for len(x11) = len(y11) + offset
rs = y11 + Z + y12
ls = x11 + Z + x12 for len(x11) = len(y11) - offset
rs = y11 + Z + y12
Use last case as sample:
propagate ls = rs & len(x12 + Z) == len(y11) => x11 + Z == y11
propagate ls = rs & len(x11 + Z) == len(y11) => x12 == Z + y12
propagate ls = rs & len(x12 + Z) == len(y11) => len(Z) = offset
propagate ls = rs & len(ls[2:]) == len(rs[2:]) => ls[2:] == rs[2:]
*/
bool theory_seq::len_based_split(eq const& e) {
context& ctx = get_context();
expr_ref_vector const& ls = e.ls();
expr_ref_vector const& rs = e.rs();
int offset_orig = 0;
if (!has_len_offset(ls, rs, offset_orig))
int offset = 0;
if (!has_len_offset(ls, rs, offset))
return false;
TRACE("seq", tout << "split based on length\n";);
TRACE("seq", display_equation(tout, e););
expr_ref x11(m_util.str.mk_concat(1, ls.c_ptr()), m);
expr_ref x12(m_util.str.mk_concat(ls.size()-1, ls.c_ptr()+1), m);
expr_ref y11(m_util.str.mk_concat(1, rs.c_ptr()), m);
expr_ref y12(m_util.str.mk_concat(rs.size()-1, rs.c_ptr()+1), m);
sort* srt = m.get_sort(ls[0]);
expr_ref x11 = expr_ref(ls[0], m);
expr_ref x12 = mk_concat(ls.size()-1, ls.c_ptr()+1, srt);
expr_ref y11 = expr_ref(rs[0], m);
expr_ref y12 = mk_concat(rs.size()-1, rs.c_ptr()+1, srt);
expr_ref lenX11 = mk_len(x11);
expr_ref lenY11(m);
expr_ref lenY11 = mk_len(y11);
expr_ref Z(m);
int offset = 0;
if (offset_orig != 0) {
lenY11 = m_autil.mk_add(mk_len(y11), m_autil.mk_int(offset_orig));
if (offset_orig > 0) {
offset = offset_orig;
if (offset != 0) {
lenY11 = m_autil.mk_add(lenY11, m_autil.mk_int(offset));
if (offset > 0) {
Z = m_sk.mk_align(y12, x12, x11, y11);
y11 = mk_concat(y11, Z);
x12 = mk_concat(Z, x12);
}
else {
offset = -offset_orig;
offset = -offset;
Z = m_sk.mk_align(x12, y12, y11, x11);
x11 = mk_concat(x11, Z);
y12 = mk_concat(Z, y12);
}
}
else {
lenY11 = mk_len(y11);
}
dependency* dep = e.dep();
literal_vector lits;
@ -444,27 +460,13 @@ bool theory_seq::len_based_split(eq const& e) {
for (unsigned i = 2; i < rs.size(); ++i) {
len2 = mk_add(len2, mk_len(rs[i]));
}
literal lit2;
if (!m_autil.is_numeral(len1) && !m_autil.is_numeral(len2)) {
lit2 = mk_eq(len1, len2, false);
}
else {
expr_ref eq_len(m.mk_eq(len1, len2), m);
lit2 = mk_literal(eq_len);
}
literal lit2 = mk_eq(len1, len2, false);
if (ctx.get_assignment(lit2) == l_true) {
lits.push_back(lit2);
TRACE("seq", tout << mk_pp(len1, m) << " = " << mk_pp(len2, m) << "\n";);
expr_ref lhs(m), rhs(m);
if (ls.size() > 2)
lhs = m_util.str.mk_concat(ls.size()-2, ls.c_ptr()+2);
else
lhs = m_util.str.mk_empty(m.get_sort(x11));
if (rs.size() > 2)
rhs = m_util.str.mk_concat(rs.size()-2, rs.c_ptr()+2);
else
rhs = m_util.str.mk_empty(m.get_sort(x11));
TRACE("seq", tout << len1 << " = " << len2 << "\n";);
expr_ref lhs = mk_concat(ls.size()-2, ls.c_ptr()+2, srt);
expr_ref rhs = mk_concat(rs.size()-2, rs.c_ptr()+2, srt);
propagate_eq(dep, lits, lhs, rhs, true);
lits.pop_back();
}
@ -622,7 +624,7 @@ bool theory_seq::split_lengths(dependency* dep,
else if (m_util.str.is_unit(Y)) {
SASSERT(lenB == lenX);
bs.push_back(Y);
expr_ref bY(m_util.str.mk_concat(bs), m);
expr_ref bY = mk_concat(bs, m.get_sort(Y));
propagate_eq(dep, lits, X, bY, true);
}
else {
@ -655,13 +657,9 @@ bool theory_seq::branch_binary_variable(eq const& e) {
}
ptr_vector<expr> xs, ys;
expr_ref x(m), y(m);
bool is_binary = is_binary_eq(e.ls(), e.rs(), x, xs, ys, y);
if (!is_binary) {
is_binary = is_binary_eq(e.rs(), e.ls(), x, xs, ys, y);
}
if (!is_binary) {
if (!is_binary_eq(e.ls(), e.rs(), x, xs, ys, y) &&
!is_binary_eq(e.rs(), e.ls(), x, xs, ys, y))
return false;
}
if (x == y) {
return false;
}
@ -760,7 +758,7 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector
else {
literal lit = mk_eq(m_autil.mk_int(lX), mk_len(X), false);
if (l_true == ctx.get_assignment(lit)) {
expr_ref R(m_util.str.mk_concat(lX, units.c_ptr()), m);
expr_ref R = mk_concat(lX, units.c_ptr(), m.get_sort(X));
propagate_eq(dep, lit, X, R);
TRACE("seq", tout << "propagate " << mk_pp(X, m) << " " << R << "\n";);
}
@ -794,7 +792,7 @@ bool theory_seq::branch_ternary_variable2() {
return false;
}
bool theory_seq::eq_unit(expr* const& l, expr* const &r) const {
bool theory_seq::eq_unit(expr* l, expr* r) const {
return l == r || is_unit_nth(l) || is_unit_nth(r);
}
@ -866,49 +864,42 @@ unsigned_vector theory_seq::overlap2(expr_ref_vector const& ls, expr_ref_vector
bool theory_seq::branch_ternary_variable_base(
dependency* dep, unsigned_vector const& indexes,
expr* const& x, expr_ref_vector const& xs, expr* const& y1, expr_ref_vector const& ys, expr* const& y2) {
expr* x, expr_ref_vector const& xs, expr* y1, expr_ref_vector const& ys, expr* y2) {
context& ctx = get_context();
bool change = false;
for (auto ind : indexes) {
TRACE("seq", tout << "ind = " << ind << "\n";);
expr_ref xs2E(m);
if (xs.size() > ind) {
xs2E = m_util.str.mk_concat(xs.size()-ind, xs.c_ptr()+ind);
}
else {
xs2E = m_util.str.mk_empty(m.get_sort(x));
}
xs2E = mk_concat(xs.size()-ind, xs.c_ptr()+ind, m.get_sort(x));
literal lit1 = mk_literal(m_autil.mk_le(mk_len(y2), m_autil.mk_int(xs.size()-ind)));
if (ctx.get_assignment(lit1) == l_undef) {
switch (ctx.get_assignment(lit1)) {
case l_undef:
TRACE("seq", tout << "base case init\n";);
ctx.mark_as_relevant(lit1);
ctx.force_phase(lit1);
change = true;
continue;
}
else if (ctx.get_assignment(lit1) == l_true) {
break;
case l_true:
TRACE("seq", tout << "base case: true branch\n";);
literal_vector lits;
lits.push_back(lit1);
propagate_eq(dep, lits, y2, xs2E, true);
propagate_eq(dep, lit1, y2, xs2E, true);
if (ind > ys.size()) {
expr_ref xs1E(m_util.str.mk_concat(ind-ys.size(), xs.c_ptr()), m);
expr_ref xs1E = mk_concat(ind-ys.size(), xs.c_ptr(), m.get_sort(x));
expr_ref xxs1E = mk_concat(x, xs1E);
propagate_eq(dep, lits, xxs1E, y1, true);
propagate_eq(dep, lit1, xxs1E, y1, true);
}
else if (ind == ys.size()) {
propagate_eq(dep, lits, x, y1, true);
propagate_eq(dep, lit1, x, y1, true);
}
else {
expr_ref ys1E(m_util.str.mk_concat(ys.size()-ind, ys.c_ptr()), m);
expr_ref ys1E = mk_concat(ys.size()-ind, ys.c_ptr(), m.get_sort(x));
expr_ref y1ys1E = mk_concat(y1, ys1E);
propagate_eq(dep, lits, x, y1ys1E, true);
propagate_eq(dep, lit1, x, y1ys1E, true);
}
return true;
}
else {
default:
TRACE("seq", tout << "base case: false branch\n";);
continue;
break;
}
}
return change;
@ -918,11 +909,8 @@ bool theory_seq::branch_ternary_variable_base(
bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) {
expr_ref_vector xs(m), ys(m);
expr_ref x(m), y1(m), y2(m);
bool is_ternary = is_ternary_eq(e.ls(), e.rs(), x, xs, y1, ys, y2, flag1);
if (!is_ternary) {
is_ternary = is_ternary_eq(e.rs(), e.ls(), x, xs, y1, ys, y2, flag1);
}
if (!is_ternary) {
if (!is_ternary_eq(e.ls(), e.rs(), x, xs, y1, ys, y2, flag1) &&
!is_ternary_eq(e.rs(), e.ls(), x, xs, y1, ys, y2, flag1)) {
return false;
}
@ -985,49 +973,42 @@ bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) {
return true;
}
bool theory_seq::branch_ternary_variable_base2(dependency* dep, unsigned_vector const& indexes,
expr_ref_vector const& xs, expr* const& x, expr* const& y1, expr_ref_vector const& ys, expr* const& y2) {
bool theory_seq::branch_ternary_variable_base2(
dependency* dep, unsigned_vector const& indexes,
expr_ref_vector const& xs, expr* x, expr* y1, expr_ref_vector const& ys, expr* y2) {
context& ctx = get_context();
sort* srt = m.get_sort(x);
bool change = false;
for (auto ind : indexes) {
expr_ref xs1E(m);
if (ind > 0) {
xs1E = m_util.str.mk_concat(ind, xs.c_ptr());
}
else {
xs1E = m_util.str.mk_empty(m.get_sort(x));
}
literal lit1 = mk_literal(m_autil.mk_le(mk_len(y1), m_autil.mk_int(ind)));
if (ctx.get_assignment(lit1) == l_undef) {
expr_ref xs1E = mk_concat(ind, xs.c_ptr(), m.get_sort(x));
literal le = m_ax.mk_le(mk_len(y1), ind);
switch (ctx.get_assignment(le)) {
case l_undef:
TRACE("seq", tout << "base case init\n";);
ctx.mark_as_relevant(lit1);
ctx.force_phase(lit1);
ctx.mark_as_relevant(le);
ctx.force_phase(le);
change = true;
continue;
}
else if (ctx.get_assignment(lit1) == l_true) {
break;
case l_true:
TRACE("seq", tout << "base case: true branch\n";);
literal_vector lits;
lits.push_back(lit1);
propagate_eq(dep, lits, y1, xs1E, true);
propagate_eq(dep, le, y1, xs1E, true);
if (xs.size() - ind > ys.size()) {
expr_ref xs2E(m_util.str.mk_concat(xs.size()-ind-ys.size(), xs.c_ptr()+ind+ys.size()), m);
expr_ref xs2E = mk_concat(xs.size()-ind-ys.size(), xs.c_ptr()+ind+ys.size(), srt);
expr_ref xs2x = mk_concat(xs2E, x);
propagate_eq(dep, lits, xs2x, y2, true);
propagate_eq(dep, le, xs2x, y2, true);
}
else if (xs.size() - ind == ys.size()) {
propagate_eq(dep, lits, x, y2, true);
propagate_eq(dep, le, x, y2, true);
}
else {
expr_ref ys1E(m_util.str.mk_concat(ys.size()-xs.size()+ind, ys.c_ptr()+xs.size()-ind), m);
expr_ref ys1E = mk_concat(ys.size()-xs.size()+ind, ys.c_ptr()+xs.size()-ind, srt);
expr_ref ys1y2 = mk_concat(ys1E, y2);
propagate_eq(dep, lits, x, ys1y2, true);
propagate_eq(dep, le, x, ys1y2, true);
}
return true;
}
else {
default:
TRACE("seq", tout << "base case: false branch\n";);
continue;
break;
}
}
return change;
@ -1037,13 +1018,9 @@ bool theory_seq::branch_ternary_variable_base2(dependency* dep, unsigned_vector
bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
expr_ref_vector xs(m), ys(m);
expr_ref x(m), y1(m), y2(m);
bool is_ternary = is_ternary_eq2(e.ls(), e.rs(), xs, x, y1, ys, y2, flag1);
if (!is_ternary) {
is_ternary = is_ternary_eq2(e.rs(), e.ls(), xs, x, y1, ys, y2, flag1);
}
if (!is_ternary) {
if (!is_ternary_eq2(e.ls(), e.rs(), xs, x, y1, ys, y2, flag1) &&
!is_ternary_eq2(e.rs(), e.ls(), xs, x, y1, ys, y2, flag1))
return false;
}
rational lenX, lenY1, lenY2;
context& ctx = get_context();
@ -1078,21 +1055,18 @@ bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
}
else {
literal ge = m_ax.mk_ge(mk_len(y1), xs.size());
if (ctx.get_assignment(ge) == l_undef) {
switch (ctx.get_assignment(ge)) {
case l_undef:
TRACE("seq", tout << "rec case init\n";);
ctx.mark_as_relevant(ge);
ctx.force_phase(ge);
}
else if (ctx.get_assignment(ge) == l_true) {
TRACE("seq", tout << "true branch\n";);
TRACE("seq", display_equation(tout, e););
literal_vector lits;
lits.push_back(ge);
dependency* dep = e.dep();
propagate_eq(dep, lits, x, Zysy2, true);
propagate_eq(dep, lits, y1, xsZ, true);
}
else {
break;
case l_true:
TRACE("seq", display_equation(tout << "true branch\n", e););
propagate_eq(e.dep(), ge, x, Zysy2, true);
propagate_eq(e.dep(), ge, y1, xsZ, true);
break;
default:
return branch_ternary_variable_base2(e.dep(), indexes, xs, x, y1, ys, y2);
}
}
@ -1112,19 +1086,17 @@ bool theory_seq::branch_quat_variable() {
// Equation is of the form x1 ++ xs ++ x2 = y1 ++ ys ++ y2 where xs, ys are units.
bool theory_seq::branch_quat_variable(eq const& e) {
expr_ref_vector xs(m), ys(m);
expr_ref x1_l(m), x2(m), y1_l(m), y2(m);
bool is_quat = is_quat_eq(e.ls(), e.rs(), x1_l, xs, x2, y1_l, ys, y2);
if (!is_quat) {
expr_ref x1(m), x2(m), y1(m), y2(m);
if (!is_quat_eq(e.ls(), e.rs(), x1, xs, x2, y1, ys, y2))
return false;
}
rational lenX1, lenX2, lenY1, lenY2;
context& ctx = get_context();
if (!get_length(x1_l, lenX1)) {
add_length_to_eqc(x1_l);
if (!get_length(x1, lenX1)) {
add_length_to_eqc(x1);
}
if (!get_length(y1_l, lenY1)) {
add_length_to_eqc(y1_l);
if (!get_length(y1, lenY1)) {
add_length_to_eqc(y1);
}
if (!get_length(x2, lenX2)) {
add_length_to_eqc(x2);
@ -1138,101 +1110,44 @@ bool theory_seq::branch_quat_variable(eq const& e) {
expr_ref xsx2 = mk_concat(xs);
ys.push_back(y2);
expr_ref ysy2 = mk_concat(ys);
expr_ref x1(x1_l, m);
expr_ref y1(y1_l, m);
expr_ref sub(mk_sub(mk_len(x1_l), mk_len(y1_l)), m);
expr_ref sub(mk_sub(mk_len(x1), mk_len(y1)), m);
literal le = m_ax.mk_le(sub, 0);
literal_vector lits;
if (ctx.get_assignment(le) == l_undef) {
switch (ctx.get_assignment(le)) {
case l_undef:
TRACE("seq", tout << "init branch\n";);
TRACE("seq", display_equation(tout, e););
ctx.mark_as_relevant(le);
ctx.force_phase(le);
}
else if (ctx.get_assignment(le) == l_false) {
break;
case l_false: {
// |x1| > |y1| => x1 = y1 ++ z1, z1 ++ xs ++ x2 = ys ++ y2
TRACE("seq", tout << "false branch\n";);
TRACE("seq", display_equation(tout, e););
expr_ref Z1 = m_sk.mk_align(ysy2, xsx2, x1, y1);
expr_ref y1Z1 = mk_concat(y1, Z1);
expr_ref Z1xsx2 = mk_concat(Z1, xsx2);
lits.push_back(~le);
dependency* dep = e.dep();
propagate_eq(dep, lits, x1, y1Z1, true);
propagate_eq(dep, lits, Z1xsx2, ysy2, true);
propagate_eq(dep, ~le, x1, y1Z1, true);
propagate_eq(dep, ~le, Z1xsx2, ysy2, true);
break;
}
else if (ctx.get_assignment(le) == l_true) {
case l_true: {
// |x1| <= |y1| => x1 ++ z2 = y1, xs ++ x2 = z2 ++ ys ++ y2
TRACE("seq", tout << "true branch\n";);
TRACE("seq", display_equation(tout, e););
expr_ref Z2 = m_sk.mk_align(xsx2, ysy2, y1, x1);
expr_ref x1Z2 = mk_concat(x1, Z2);
expr_ref Z2ysy2 = mk_concat(Z2, ysy2);
lits.push_back(le);
dependency* dep = e.dep();
propagate_eq(dep, lits, x1Z2, y1, true);
propagate_eq(dep, lits, xsx2, Z2ysy2, true);
propagate_eq(dep, le, x1Z2, y1, true);
propagate_eq(dep, le, xsx2, Z2ysy2, true);
break;
}
}
return true;
}
void theory_seq::len_offset(expr* e, rational val) {
context & ctx = get_context();
expr *l1 = nullptr, *l2 = nullptr, *l21 = nullptr, *l22 = nullptr;
rational fact;
if (m_autil.is_add(e, l1, l2) && m_autil.is_mul(l2, l21, l22) &&
m_autil.is_numeral(l21, fact) && fact.is_minus_one()) {
if (ctx.e_internalized(l1) && ctx.e_internalized(l22)) {
enode* r1 = get_root(l1), *n1 = r1;
enode* r2 = get_root(l22), *n2 = r2;
expr *e1 = nullptr, *e2 = nullptr;
do {
if (m_util.str.is_length(n1->get_owner(), e1))
break;
n1 = n1->get_next();
}
while (n1 != r1);
do {
if (m_util.str.is_length(n2->get_owner(), e2))
break;
n2 = n2->get_next();
}
while (n2 != r2);
obj_map<enode, int> tmp;
if (m_util.str.is_length(n1->get_owner(), e1)
&& m_util.str.is_length(n2->get_owner(), e2) &&
m_len_offset.find(r1, tmp)) {
tmp.insert(r2, val.get_int32());
m_len_offset.insert(r1, tmp);
TRACE("seq", tout << "a length pair: " << mk_pp(e1, m) << ", " << mk_pp(e2, m) << "\n";);
return;
}
}
}
}
// Find the length offset from the congruence closure core
void theory_seq::prop_arith_to_len_offset() {
context & ctx = get_context();
obj_hashtable<enode> const_set;
ptr_vector<enode>::const_iterator it = ctx.begin_enodes();
ptr_vector<enode>::const_iterator end = ctx.end_enodes();
for (; it != end; ++it) {
enode * root = (*it)->get_root();
rational val;
if (m_autil.is_numeral(root->get_owner(), val) && val.is_neg()) {
if (const_set.contains(root)) continue;
const_set.insert(root);
TRACE("seq", tout << "offset: " << mk_pp(root->get_owner(), m) << "\n";);
enode *next = root->get_next();
while (next != root) {
TRACE("seq", tout << "eqc: " << mk_pp(next->get_owner(), m) << "\n";);
len_offset(next->get_owner(), val);
next = next->get_next();
}
}
}
}
int theory_seq::find_fst_non_empty_idx(expr_ref_vector const& xs) {
context & ctx = get_context();
@ -1415,26 +1330,7 @@ unsigned theory_seq::find_branch_start(unsigned k) {
return 0;
}
expr_ref_vector theory_seq::expand_strings(expr_ref_vector const& es) {
expr_ref_vector ls(m);
for (expr* e : es) {
zstring s;
if (m_util.str.is_string(e, s)) {
for (unsigned i = 0; i < s.length(); ++i) {
ls.push_back(m_util.str.mk_unit(m_util.str.mk_char(s, i)));
}
}
else {
ls.push_back(e);
}
}
return ls;
}
bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& _ls, expr_ref_vector const& _rs) {
expr_ref_vector ls = expand_strings(_ls);
expr_ref_vector rs = expand_strings(_rs);
bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs) {
if (ls.empty()) {
return false;
}
@ -1474,10 +1370,7 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
bool all_units = true;
for (expr* r : rs) {
if (!m_util.str.is_unit(r)) {
all_units = false;
break;
}
all_units &= m_util.str.is_unit(r);
}
if (all_units) {
context& ctx = get_context();
@ -1593,7 +1486,7 @@ bool theory_seq::propagate_length_coherence(expr* e) {
expr_ref_vector elems(m);
unsigned _lo = lo.get_unsigned();
for (unsigned j = 0; j < _lo; ++j) {
mk_decompose(seq, head, tail);
m_sk.decompose(seq, head, tail);
elems.push_back(head);
seq = tail;
}
@ -1630,7 +1523,7 @@ bool theory_seq::check_length_coherence(expr* e) {
expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
expr_ref head(m), tail(m);
// e = emp \/ e = unit(head.elem(e))*tail(e)
mk_decompose(e, head, tail);
m_sk.decompose(e, head, tail);
expr_ref conc = mk_concat(head, tail);
if (propagate_is_conc(e, conc)) {
assume_equality(tail, emp);
@ -1756,6 +1649,7 @@ bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) &&
rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
unsigned l_start = 1;
sort* srt = m.get_sort(ls[0]);
for (; l_start < ls.size()-1; ++l_start) {
if (m_util.str.is_unit(ls[l_start])) break;
}
@ -1783,12 +1677,12 @@ bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
}
xs.reset();
xs.append(l_end-l_start+1, ls.c_ptr()+l_start);
x1 = m_util.str.mk_concat(l_start, ls.c_ptr());
x2 = m_util.str.mk_concat(ls.size()-l_end-1, ls.c_ptr()+l_end+1);
x1 = mk_concat(l_start, ls.c_ptr(), srt);
x2 = mk_concat(ls.size()-l_end-1, ls.c_ptr()+l_end+1, srt);
ys.reset();
ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
y1 = mk_concat(r_start, rs.c_ptr(), srt);
y2 = mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1, srt);
return true;
}
return false;
@ -1802,6 +1696,7 @@ bool theory_seq::is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const&
expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1) {
if (ls.size() > 1 && (is_var(ls[0]) || flag1) &&
rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
sort* srt = m.get_sort(ls[0]);
unsigned l_start = ls.size()-1;
for (; l_start > 0; --l_start) {
if (!m_util.str.is_unit(ls[l_start])) break;
@ -1826,11 +1721,11 @@ bool theory_seq::is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const&
}
xs.reset();
xs.append(ls.size()-l_start, ls.c_ptr()+l_start);
x = m_util.str.mk_concat(l_start, ls.c_ptr());
x = mk_concat(l_start, ls.c_ptr(), srt);
ys.reset();
ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
y1 = mk_concat(r_start, rs.c_ptr(), srt);
y2 = mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1, srt);
return true;
}
return false;
@ -1844,6 +1739,7 @@ bool theory_seq::is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const
expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1) {
if (ls.size() > 1 && (is_var(ls.back()) || flag1) &&
rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
sort* srt = m.get_sort(ls[0]);
unsigned l_start = 0;
for (; l_start < ls.size()-1; ++l_start) {
if (!m_util.str.is_unit(ls[l_start])) break;
@ -1867,11 +1763,11 @@ bool theory_seq::is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const
}
xs.reset();
xs.append(l_start, ls.c_ptr());
x = m_util.str.mk_concat(ls.size()-l_start, ls.c_ptr()+l_start);
x = mk_concat(ls.size()-l_start, ls.c_ptr()+l_start, srt);
ys.reset();
ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
y1 = mk_concat(r_start, rs.c_ptr(), srt);
y2 = mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1, srt);
return true;
}
return false;
@ -1890,7 +1786,7 @@ bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const&
expr_ref_vector ls1(m), rs1(m);
expr_ref idx1(m_autil.mk_add(idx, m_autil.mk_int(1)), m);
m_rewrite(idx1);
expr_ref rhs(m_util.str.mk_concat(rs.size(), rs.c_ptr()), m);
expr_ref rhs = mk_concat(rs.size(), rs.c_ptr(), m.get_sort(ls[0]));
ls1.push_back(s);
if (!idx_is_zero) rs1.push_back(m_sk.mk_pre(s, idx));
rs1.push_back(m_util.str.mk_unit(rhs));

303
src/smt/seq_ne_solver.cpp Normal file
View file

@ -0,0 +1,303 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
seq_ne_solver.cpp
Abstract:
Features from theory_seq that are specific to solving dis-equations.
Author:
Nikolaj Bjorner (nbjorner) 2015-6-12
*/
#include <typeinfo>
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_trail.h"
#include "ast/for_each_expr.h"
#include "smt/smt_context.h"
#include "smt/theory_seq.h"
#include "smt/theory_arith.h"
using namespace smt;
bool theory_seq::solve_nqs(unsigned i) {
context & ctx = get_context();
for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) {
if (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();
}
bool theory_seq::solve_ne(unsigned idx) {
TRACE("seq", display_disequation(tout << "solve: ", m_nqs[idx]););
unsigned num_undef_lits = 0;
return
(!check_ne_literals(idx, num_undef_lits))
|| (num_undef_lits <= 1 && propagate_ne2lit(idx))
|| (num_undef_lits == 0 && propagate_ne2eq(idx))
|| reduce_ne(idx);
}
bool theory_seq::check_ne_literals(unsigned idx, unsigned& num_undef_lits) {
ne const& n = m_nqs[idx];
context& ctx = get_context();
for (literal lit : n.lits()) {
switch (ctx.get_assignment(lit)) {
case l_false:
TRACE("seq", display_disequation(tout << "has false literal\n", n);
ctx.display_literal_verbose(tout, lit);
tout << "\n" << lit << " " << ctx.is_relevant(lit) << "\n";
);
return false;
case l_true:
break;
case l_undef:
++num_undef_lits;
break;
}
}
return true;
}
/*
\brief propagate if there is a single undefined literal, others are true.
*/
bool theory_seq::propagate_ne2lit(unsigned idx) {
ne const& n = m_nqs[idx];
context& ctx = get_context();
if (!n.eqs().empty()) {
return false;
}
literal_vector lits;
literal undef_lit = null_literal;
for (literal lit : n.lits()) {
switch (ctx.get_assignment(lit)) {
case l_true:
lits.push_back(lit);
break;
case l_false:
return true;
break;
case l_undef:
if (undef_lit != null_literal)
return false;
undef_lit = lit;
break;
}
}
if (undef_lit == null_literal) {
dependency* dep = n.dep();
dependency* dep1 = nullptr;
if (explain_eq(n.l(), n.r(), dep1)) {
literal diseq = mk_eq(n.l(), n.r(), false);
if (ctx.get_assignment(diseq) == l_false) {
lits.reset();
lits.push_back(~diseq);
dep = dep1;
TRACE("seq", tout << "conflict explained\n";);
}
}
set_conflict(dep, lits);
}
else {
TRACE("seq", tout << "propagate: " << undef_lit << "\n";);
propagate_lit(n.dep(), lits.size(), lits.c_ptr(), ~undef_lit);
}
return true;
}
/*
\brief propagate "" != s into s = head(s) + tail(s)
Assumes all literals are assigned to true.
*/
bool theory_seq::propagate_ne2eq(unsigned idx) {
ne const& n = m_nqs[idx];
if (n.eqs().size() != 1)
return false;
auto const& l = n[0].first;
auto const& r = n[0].second;
if (l.empty())
return propagate_ne2eq(idx, r);
if (r.empty())
return propagate_ne2eq(idx, l);
return false;
}
bool theory_seq::propagate_ne2eq(unsigned idx, expr_ref_vector const& es) {
if (es.empty())
return false;
ne const& n = m_nqs[idx];
expr_ref e(m), head(m), tail(m);
e = mk_concat(es, m.get_sort(es[0]));
m_sk.decompose(e, head, tail);
propagate_eq(n.dep(), n.lits(), e, mk_concat(head, tail), false);
return true;
}
bool theory_seq::reduce_ne(unsigned idx) {
ne const& n = m_nqs[idx];
context& ctx = get_context();
bool updated = false;
dependency* new_deps = n.dep();
vector<decomposed_eq> new_eqs;
literal_vector new_lits(n.lits());
for (unsigned i = 0; i < n.eqs().size(); ++i) {
auto const& p = n[i];
expr_ref_vector& ls = m_ls;
expr_ref_vector& rs = m_rs;
expr_ref_pair_vector& eqs = m_new_eqs;
ls.reset(); rs.reset(); eqs.reset();
dependency* deps = nullptr;
bool change = false;
if (!canonize(p.first, ls, deps, change)) return false;
if (!canonize(p.second, rs, deps, change)) return false;
new_deps = m_dm.mk_join(deps, new_deps);
if (!m_seq_rewrite.reduce_eq(ls, rs, eqs, change)) {
TRACE("seq", display_disequation(tout << "reduces to false: ", n);
tout << p.first << " -> " << ls << "\n";
tout << p.second << " -> " << rs << "\n";);
return true;
}
if (!change) {
TRACE("seq", tout << "no change " << p.first << " " << p.second << "\n";);
if (updated) {
new_eqs.push_back(p);
}
continue;
}
if (!updated) {
for (unsigned j = 0; j < i; ++j) {
new_eqs.push_back(n[j]);
}
updated = true;
}
if (!ls.empty() || !rs.empty()) {
new_eqs.push_back(decomposed_eq(ls, rs));
}
TRACE("seq",
for (auto const& p : eqs) tout << mk_pp(p.first, m) << " != " << mk_pp(p.second, m) << "\n";
for (auto const& p : new_eqs) tout << p.first << " != " << p.second << "\n";
tout << p.first << " != " << p.second << "\n";);
for (auto const& p : eqs) {
expr* nl = p.first;
expr* nr = p.second;
if (m_util.is_seq(nl) || m_util.is_re(nl)) {
ls.reset();
rs.reset();
m_util.str.get_concat_units(nl, ls);
m_util.str.get_concat_units(nr, rs);
new_eqs.push_back(decomposed_eq(ls, rs));
}
else if (nl != nr) {
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:
m_new_propagation = true;
break;
}
}
}
}
TRACE("seq", display_disequation(tout << "updated: " << updated << "\n", n););
if (updated) {
m_nqs.set(idx, ne(n.l(), n.r(), new_eqs, new_lits, new_deps));
TRACE("seq", display_disequation(tout << "updated: ", m_nqs[idx]););
}
return false;
}
bool theory_seq::branch_nqs() {
for (unsigned i = 0; i < m_nqs.size(); ++i) {
ne n = m_nqs[i];
lbool r = branch_nq(n);
switch (r) {
case l_undef: // needs assignment to a literal.
return true;
case l_true: // disequality is satisfied.
m_nqs.erase_and_swap(i);
break;
case l_false: // needs to be expanded.
m_nqs.erase_and_swap(i);
return true;
}
}
return false;
}
lbool theory_seq::branch_nq(ne const& n) {
context& ctx = get_context();
literal eq_len = mk_eq(mk_len(n.l()), mk_len(n.r()), false);
ctx.mark_as_relevant(eq_len);
switch (ctx.get_assignment(eq_len)) {
case l_false:
TRACE("seq", ctx.display_literal_smt2(tout << "lengths are different: ", eq_len) << "\n";);
return l_true;
case l_undef:
return l_undef;
default:
break;
}
literal eq = mk_eq(n.l(), n.r(), false);
literal len_gt = mk_literal(m_autil.mk_ge(mk_len(n.l()), m_autil.mk_int(1)));
ctx.mark_as_relevant(len_gt);
switch (ctx.get_assignment(len_gt)) {
case l_false:
add_axiom(eq, ~eq_len, len_gt);
return l_false;
case l_undef:
return l_undef;
default:
break;
}
expr_ref h1(m), t1(m), h2(m), t2(m);
mk_decompose(n.l(), h1, t1);
mk_decompose(n.r(), h2, t2);
literal eq_head = mk_eq(h1, h2, false);
ctx.mark_as_relevant(eq_head);
switch (ctx.get_assignment(eq_head)) {
case l_false:
TRACE("seq", ctx.display_literal_smt2(tout << "heads are different: ", eq_head) << "\n";);
return l_true;
case l_undef:
return l_undef;
default:
break;
}
// l = r or |l| != |r| or |l| > 0
// l = r or |l| != |r| or h1 != h2 or t1 != t2
add_axiom(eq, ~eq_len, len_gt);
add_axiom(eq, ~eq_len, ~eq_head, ~mk_eq(t1, t2, false));
return l_false;
}

133
src/smt/seq_offset_eq.cpp Normal file
View file

@ -0,0 +1,133 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
seq_offset_eq.h
Abstract:
Container for maintaining equalities between lengths of sequences.
Author:
Thai Minh Trinh 2017
Nikolaj Bjorner (nbjorner) 2020-4-16
--*/
#include "ast/ast_pp.h"
#include "smt/seq_offset_eq.h"
#include "smt/smt_context.h"
using namespace smt;
/**
Match:
e == val where val is an integer
e == r1 - r2
r1 == len(e1)
r2 == len(e2)
update m_offset_equalities to contain.
r1 |-> [r2 |-> val]
*/
seq_offset_eq::seq_offset_eq(theory& th, ast_manager& m):
th(th), m(m), seq(m), a(m), m_propagation_level(-1) {
}
bool seq_offset_eq::match_x_minus_y(expr* e, expr*& x, expr*& y) const {
expr* z = nullptr, *u = nullptr;
rational fact;
return
a.is_add(e, x, z) &&
a.is_mul(z, u, y) &&
a.is_numeral(u, fact) &&
fact.is_minus_one();
}
void seq_offset_eq::len_offset(expr* e, int val) {
context & ctx = th.get_context();
expr *x = nullptr, *y = nullptr;
expr *e1 = nullptr, *e2 = nullptr;
if (match_x_minus_y(e, x, y) &&
ctx.e_internalized(x) &&
ctx.e_internalized(y)) {
TRACE("seq", tout << "eqc: " << mk_pp(e, m) << "\n";);
enode* r1 = th.get_root(x);
enode* r2 = th.get_root(y);
for (enode* n1 : *r1) {
if (!seq.str.is_length(n1->get_owner(), e1))
continue;
for (enode* n2 : *r2) {
if (!seq.str.is_length(n2->get_owner(), e2))
continue;
if (r1->get_owner_id() > r2->get_owner_id()) {
std::swap(r1, r2);
val = -val;
}
m_offset_equalities.insert(r1, r2, val);
m_has_offset_equality.insert(r1);
m_has_offset_equality.insert(r2);
TRACE("seq", tout << "a length pair: " << mk_pp(e1, m) << ", " << mk_pp(e2, m) << "\n";);
return;
}
return;
}
}
}
// Find the length offset from the congruence closure core
void seq_offset_eq::prop_arith_to_len_offset() {
rational val;
for (enode* n : th.get_context().enodes()) {
if (a.is_numeral(n->get_owner(), val) && val.is_int32() && INT_MIN < val.get_int32()) {
TRACE("seq", tout << "offset: " << mk_pp(n->get_owner(), m) << "\n";);
enode *next = n->get_next();
while (next != n) {
len_offset(next->get_owner(), val.get_int32());
next = next->get_next();
}
}
}
}
bool seq_offset_eq::find(enode* n1, enode* n2, int& offset) const {
n1 = n1->get_root();
n2 = n2->get_root();
if (n1->get_owner_id() > n2->get_owner_id())
std::swap(n1, n2);
return
!a.is_numeral(n2->get_owner()) &&
!a.is_numeral(n2->get_owner()) &&
m_offset_equalities.find(n1, n2, offset);
}
bool seq_offset_eq::contains(enode* r) {
r = r->get_root();
return !a.is_numeral(r->get_owner()) && m_has_offset_equality.contains(r);
}
bool seq_offset_eq::propagate() {
context& ctx = th.get_context();
int lvl = (int) ctx.get_scope_level();
if (lvl > m_propagation_level) {
m_propagation_level = lvl;
prop_arith_to_len_offset();
return true;
}
else {
return false;
}
}
void seq_offset_eq::pop_scope_eh(unsigned num_scopes) {
context& ctx = th.get_context();
int new_lvl = (int) (ctx.get_scope_level() - num_scopes);
if (m_propagation_level > new_lvl) {
m_propagation_level = -1;
m_offset_equalities.reset();
m_has_offset_equality.reset();
}
}

55
src/smt/seq_offset_eq.h Normal file
View file

@ -0,0 +1,55 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
seq_offset_eq.h
Abstract:
Container for maintaining equalities between lengths of sequences.
Author:
Thai Minh Trinh 2017
Nikolaj Bjorner (nbjorner) 2020-4-16
--*/
#pragma once
#include "util/obj_pair_hashtable.h"
#include "ast/seq_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "smt/smt_theory.h"
namespace smt {
class seq_offset_eq {
theory& th;
ast_manager& m;
seq_util seq;
arith_util a;
obj_hashtable<enode> m_has_offset_equality;
obj_pair_map<enode, enode, int> m_offset_equalities;
int m_propagation_level;
bool match_x_minus_y(expr* e, expr*& x, expr*& y) const;
void len_offset(expr* e, int val);
void prop_arith_to_len_offset();
public:
seq_offset_eq(theory& th, ast_manager& m);
bool empty() const { return m_offset_equalities.empty(); }
/**
\breif determine if r1 = r2 + offset
*/
bool find(enode* r1, enode* r2, int& offset) const;
bool contains(enode* r1, enode* r2) const { int offset = 0; return find(r1, r2, offset); }
bool contains(enode* r);
bool propagate();
void pop_scope_eh(unsigned num_scopes);
};
};

1
src/smt/seq_skolem.cpp
View file

@ -112,6 +112,7 @@ decompose_main:
head = seq.str.mk_unit(seq.str.mk_nth_i(s, idx));
tail = mk(m_tail, s, idx);
m_rewrite(head);
m_rewrite(tail);
}
else {
head = seq.str.mk_unit(seq.str.mk_nth_i(e, a.mk_int(0)));

5
src/smt/seq_skolem.h
View file

@ -92,6 +92,11 @@ namespace smt {
bool is_step(expr* e) const { return is_skolem(m_aut_step, e); }
bool is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, expr*& j, expr*& t) const;
bool is_accept(expr* acc) const { return is_skolem(m_accept, acc); }
bool is_accept(expr* a, expr*& s, expr*& i, expr*& r, expr*& n) const {
return is_accept(a) && (s = to_app(a)->get_arg(0), i = to_app(a)->get_arg(1),
r = to_app(a)->get_arg(2), n = to_app(a)->get_arg(3),
true);
}
bool is_post(expr* e, expr*& s, expr*& start);
bool is_pre(expr* e, expr*& s, expr*& i);
bool is_eq(expr* e, expr*& a, expr*& b) const;

7
src/smt/smt_conflict_resolution.cpp
View file

@ -767,7 +767,6 @@ namespace smt {
if it already exists. Otherwise, return 0 and add p to the todo-list.
*/
proof * conflict_resolution::get_proof(enode * n1, enode * n2) {
SASSERT(n1 != n2);
proof * pr;
if (m_eq2proof.find(n1, n2, pr)) {
TRACE("proof_gen_bug", tout << "eq2_pr_cached: #" << n1->get_owner_id() << " #" << n2->get_owner_id() << "\n";);
@ -1204,6 +1203,12 @@ namespace smt {
void conflict_resolution::mk_proof(enode * lhs, enode * rhs) {
SASSERT(!m_eq2proof.contains(lhs, rhs));
if (lhs == rhs) {
proof* pr = m.mk_reflexivity(lhs->get_owner());
m_new_proofs.push_back(pr);
m_eq2proof.insert(lhs, rhs, pr);
return;
}
enode * c = find_common_ancestor(lhs, rhs);
ptr_buffer<proof> prs1;
mk_proof(lhs, c, prs1);

15
src/smt/smt_enode.h
View file

@ -354,6 +354,21 @@ namespace smt {
enode_vector::const_iterator end_parents() const {
return m_parents.end();
}
class iterator {
enode* m_first;
enode* m_last;
public:
iterator(enode* n, enode* m): m_first(n), m_last(m) {}
enode* operator*() { return m_first; }
iterator& operator++() { if (!m_last) m_last = m_first; m_first = m_first->m_next; return *this; }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const& other) const { return m_last == other.m_last && m_first == other.m_first; }
bool operator!=(iterator const& other) const { return !(*this == other); }
};
iterator begin() { return iterator(this, nullptr); }
iterator end() { return iterator(this, this); }
theory_var_list const * get_th_var_list() const {
return m_th_var_list.get_th_var() == null_theory_var ? nullptr : &m_th_var_list;

8
src/smt/smt_justification.cpp
View file

@ -177,7 +177,8 @@ namespace smt {
void mp_iff_justification::get_antecedents(conflict_resolution & cr) {
SASSERT(m_node1 != m_node2);
if (m_node1 == m_node2)
return;
cr.mark_eq(m_node1, m_node2);
context & ctx = cr.get_context();
bool_var v = ctx.enode2bool_var(m_node1);
@ -187,6 +188,9 @@ namespace smt {
}
proof * mp_iff_justification::mk_proof(conflict_resolution & cr) {
ast_manager& m = cr.get_manager();
if (m_node1 == m_node2)
return m.mk_reflexivity(m_node1->get_owner());
proof * pr1 = cr.get_proof(m_node1, m_node2);
context & ctx = cr.get_context();
bool_var v = ctx.enode2bool_var(m_node1);
@ -194,7 +198,7 @@ namespace smt {
literal l(v, val == l_false);
proof * pr2 = cr.get_proof(l);
if (pr1 && pr2) {
ast_manager & m = cr.get_manager();
proof * pr;
SASSERT(m.has_fact(pr1));
SASSERT(m.has_fact(pr2));

1
src/smt/smt_setup.cpp
View file

@ -682,6 +682,7 @@ namespace smt {
//
setup_mi_arith();
setup_arrays();
setup_card();
}
void setup::setup_UFNIA() {

2
src/smt/smt_theory.h
View file

@ -513,6 +513,8 @@ namespace smt {
enode* ensure_enode(expr* e);
enode* get_root(expr* e) { return ensure_enode(e)->get_root(); }
// -----------------------------------
//
// Model generation

26
src/smt/theory_arith_nl.h
View file

@ -182,14 +182,23 @@ template<typename Ext>
rational theory_arith<Ext>::decompose_monomial(expr* m, buffer<var_power_pair>& vp) const {
rational coeff(1);
vp.reset();
expr_fast_mark1 mark;
auto insert = [&](expr* arg) {
rational r;
if (m_util.is_numeral(arg, r))
coeff *= r;
else if (!vp.empty() && vp.back().first == arg)
vp.back().second += 1;
else
else if (mark.is_marked(arg)) {
for (unsigned i = vp.size(); i-- > 0; ) {
if (vp[i].first == arg) {
vp[i].second++;
break;
}
}
}
else {
mark.mark(arg);
vp.push_back(var_power_pair(arg, 1));
}
};
while (m_util.is_mul(m)) {
unsigned sz = to_app(m)->get_num_args();
@ -394,7 +403,8 @@ bool theory_arith<Ext>::update_bounds_using_interval(theory_var v, interval cons
}
bound * old_lower = lower(v);
if (old_lower == nullptr || new_lower > old_lower->get_value()) {
TRACE("non_linear", tout << "NEW lower bound for v" << v << " " << new_lower << "\n";
TRACE("non_linear", tout << "NEW lower bound for v" << v << " " << mk_pp(var2expr(v), get_manager())
<< " " << new_lower << "\n";
display_interval(tout, i); tout << "\n";);
mk_derived_nl_bound(v, new_lower, B_LOWER, i.get_lower_dependencies());
r = true;
@ -722,19 +732,19 @@ bool theory_arith<Ext>::branch_nl_int_var(theory_var v) {
*/
template<typename Ext>
bool theory_arith<Ext>::is_monomial_linear(expr * m) const {
SASSERT(is_pure_monomial(m));
unsigned num_nl_vars = 0;
for (expr* arg : *to_app(m)) {
if (!get_context().e_internalized(arg))
return false;
theory_var _var = expr2var(arg);
CTRACE("non_linear", is_fixed(_var),
tout << mk_pp(arg, get_manager()) << " is fixed: " << lower_bound(_var) << "\n";);
if (!is_fixed(_var)) {
num_nl_vars++;
}
else {
if (lower_bound(_var).is_zero())
return true;
else if (lower_bound(_var).is_zero()) {
return true;
}
}
return num_nl_vars <= 1;

2
src/smt/theory_recfun.cpp
View file

@ -487,7 +487,7 @@ namespace smt {
m_disabled_guards.erase(to_delete);
m_enabled_guards.push_back(to_delete);
m_q_guards.push_back(to_delete);
IF_VERBOSE(1, verbose_stream() << "(smt.recfun :enable-guard)\n");
IF_VERBOSE(1, verbose_stream() << "(smt.recfun :enable-guard " << mk_pp(to_delete, m) << ")\n");
}
else {
IF_VERBOSE(1, verbose_stream() << "(smt.recfun :increment-round)\n");

390
src/smt/theory_seq.cpp
View file

@ -282,9 +282,9 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
m_lts_checked(false),
m_eq_id(0),
m_find(*this),
m_offset_eq(*this, m),
m_overlap(m),
m_overlap2(m),
m_len_prop_lvl(-1),
m_factory(nullptr),
m_exclude(m),
m_axioms(m),
@ -304,6 +304,7 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
m_trail_stack(*this),
m_ls(m), m_rs(m),
m_lhs(m), m_rhs(m),
m_new_eqs(m),
m_has_seq(m_util.has_seq()),
m_res(m),
m_max_unfolding_depth(1),
@ -513,7 +514,7 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
expr_ref_vector elems(m);
for (unsigned j = 0; j < _lo; ++j) {
mk_decompose(seq, head, tail);
m_sk.decompose(seq, head, tail);
elems.push_back(head);
seq = tail;
}
@ -563,9 +564,10 @@ expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
return result;
}
void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
m_sk.decompose(e, head, tail);
add_axiom(~mk_eq_empty(e), mk_eq_empty(tail));;
add_axiom(mk_eq_empty(e), mk_eq(e, mk_concat(head, tail), false));
}
/*
@ -600,24 +602,24 @@ bool theory_seq::check_extensionality() {
if (!canonize(n2->get_owner(), dep, e2)) {
return false;
}
m_lhs.reset(); m_rhs.reset();
m_new_eqs.reset();
bool change = false;
if (!m_seq_rewrite.reduce_eq(e1, e2, m_lhs, m_rhs, change)) {
if (!m_seq_rewrite.reduce_eq(e1, e2, m_new_eqs, change)) {
TRACE("seq", tout << "exclude " << mk_pp(o1, m) << " " << mk_pp(o2, m) << "\n";);
m_exclude.update(o1, o2);
continue;
}
bool excluded = false;
for (unsigned j = 0; !excluded && j < m_lhs.size(); ++j) {
if (m_exclude.contains(m_lhs.get(j), m_rhs.get(j))) {
TRACE("seq", tout << "excluded " << j << " " << m_lhs << " " << m_rhs << "\n";);
for (auto const& p : m_new_eqs) {
if (m_exclude.contains(p.first, p.second)) {
TRACE("seq", tout << "excluded " << mk_pp(p.first, m) << " " << mk_pp(p.second, m) << "\n";);
excluded = true;
break;
}
}
if (excluded) {
continue;
}
TRACE("seq", tout << m_lhs << " = " << m_rhs << "\n";);
ctx.assume_eq(n1, n2);
return false;
}
@ -634,12 +636,7 @@ bool theory_seq::check_contains() {
context & ctx = get_context();
for (unsigned i = 0; !ctx.inconsistent() && i < m_ncs.size(); ++i) {
if (solve_nc(i)) {
if (i + 1 != m_ncs.size()) {
nc n = m_ncs[m_ncs.size()-1];
m_ncs.set(i, n);
--i;
}
m_ncs.pop_back();
m_ncs.erase_and_swap(i--);
}
}
return m_new_propagation || ctx.inconsistent();
@ -907,14 +904,15 @@ bool theory_seq::lift_ite(expr_ref_vector const& ls, expr_ref_vector const& rs,
bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependency* deps) {
context& ctx = get_context();
expr_ref_vector lhs(m), rhs(m);
expr_ref_pair_vector& new_eqs = m_new_eqs;
new_eqs.reset();
bool changed = false;
TRACE("seq",
for (expr* l : ls) tout << "s#" << l->get_id() << " " << mk_bounded_pp(l, m, 2) << "\n";
tout << " = \n";
for (expr* r : rs) tout << "s#" << r->get_id() << " " << mk_bounded_pp(r, m, 2) << "\n";);
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, changed)) {
if (!m_seq_rewrite.reduce_eq(ls, rs, new_eqs, changed)) {
// equality is inconsistent.
TRACE("seq_verbose", tout << ls << " != " << rs << "\n";);
set_conflict(deps);
@ -922,27 +920,29 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
}
if (!changed) {
SASSERT(lhs.empty() && rhs.empty());
SASSERT(new_eqs.empty());
return false;
}
TRACE("seq",
tout << "reduced to\n";
for (expr* l : lhs) tout << mk_bounded_pp(l, m, 2) << "\n";
tout << " = \n";
for (expr* r : rhs) tout << mk_bounded_pp(r, m, 2) << "\n";
for (auto p : new_eqs) {
tout << mk_bounded_pp(p.first, m, 2) << "\n";
tout << " = \n";
tout << mk_bounded_pp(p.second, m, 2) << "\n";
}
);
SASSERT(lhs.size() == rhs.size());
m_seq_rewrite.add_seqs(ls, rs, lhs, rhs);
if (lhs.empty()) {
m_seq_rewrite.add_seqs(ls, rs, new_eqs);
if (new_eqs.empty()) {
TRACE("seq", tout << "solved\n";);
return true;
}
TRACE("seq_verbose",
tout << ls << " = " << rs << "\n";
tout << lhs << " = " << rhs << "\n";);
for (unsigned i = 0; !ctx.inconsistent() && i < lhs.size(); ++i) {
expr_ref li(lhs.get(i), m);
expr_ref ri(rhs.get(i), m);
tout << ls << " = " << rs << "\n";);
for (auto const& p : new_eqs) {
if (ctx.inconsistent())
break;
expr_ref li(p.first, m);
expr_ref ri(p.second, m);
if (solve_unit_eq(li, ri, deps)) {
// no-op
}
@ -956,8 +956,8 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
}
TRACE("seq_verbose",
if (!ls.empty() || !rs.empty()) tout << ls << " = " << rs << ";\n";
for (unsigned i = 0; i < lhs.size(); ++i) {
tout << mk_pp(lhs.get(i), m) << " = " << mk_pp(rhs.get(i), m) << ";\n";
for (auto const& p : new_eqs) {
tout << mk_pp(p.first, m) << " = " << mk_pp(p.second, m) << ";\n";
});
@ -976,7 +976,7 @@ bool theory_seq::solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs
bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep) {
if (rs.empty()) {
literal lit = mk_simplified_literal(m_autil.mk_le(n, m_autil.mk_int(-1)));
literal lit = m_ax.mk_le(n, -1);
propagate_lit(dep, 0, nullptr, lit);
return true;
}
@ -1003,7 +1003,7 @@ bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep)
if (rs.size() > 1) {
VERIFY (m_util.str.is_unit(rs[0], u));
digit = m_sk.mk_digit2int(u);
propagate_lit(dep, 0, nullptr, mk_simplified_literal(m_autil.mk_ge(digit, m_autil.mk_int(1))));
propagate_lit(dep, 0, nullptr, m_ax.mk_ge(digit, 1));
}
return true;
}
@ -1060,7 +1060,7 @@ bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) {
}
rational hi;
if (m_sk.is_tail_u(l, s, idx) && has_length(s) && m_util.str.is_empty(r) && !upper_bound(s, hi)) {
propagate_lit(deps, 0, nullptr, mk_literal(m_autil.mk_le(mk_len(s), m_autil.mk_int(idx+1))));
propagate_lit(deps, 0, nullptr, m_ax.mk_le(mk_len(s), idx+1));
return true;
}
return false;
@ -1196,15 +1196,14 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
expr* s, *i, *l;
rational r;
if (m_util.str.is_extract(e, s, i, l)) {
// 0 <= i <= len(s), 0 <= l, i + l <= len(s)
expr_ref zero(m_autil.mk_int(0), m);
// 0 <= i <= len(s), 0 <= l, i + l <= len(s)
expr_ref ls = mk_len(s);
expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i),l), m);
bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
literal i_ge_0 = i_is_zero?true_literal:mk_simplified_literal(m_autil.mk_ge(i, zero));
literal i_lt_len_s = ~mk_simplified_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
literal li_ge_ls = mk_simplified_literal(m_autil.mk_ge(ls_minus_i_l, zero));
literal l_ge_zero = mk_simplified_literal(m_autil.mk_ge(l, zero));
literal i_ge_0 = i_is_zero?true_literal:m_ax.mk_ge(i, 0);
literal i_lt_len_s = ~m_ax.mk_ge(mk_sub(i, ls), 0);
literal li_ge_ls = m_ax.mk_ge(ls_minus_i_l, 0);
literal l_ge_zero = m_ax.mk_ge(l, 0);
literal _lits[4] = { i_ge_0, i_lt_len_s, li_ge_ls, l_ge_zero };
if (ctx.get_assignment(i_ge_0) == l_true &&
ctx.get_assignment(i_lt_len_s) == l_true &&
@ -1219,10 +1218,9 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
}
else if (m_util.str.is_at(e, s, i)) {
// has length 1 if 0 <= i < len(s)
expr_ref zero(m_autil.mk_int(0), m);
bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
literal i_ge_0 = i_is_zero?true_literal:mk_simplified_literal(m_autil.mk_ge(i, zero));
literal i_lt_len_s = ~mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero));
literal i_ge_0 = i_is_zero?true_literal:m_ax.mk_ge(i, 0);
literal i_lt_len_s = ~m_ax.mk_ge(mk_sub(i, mk_len(s)), 0);
literal _lits[2] = { i_ge_0, i_lt_len_s};
if (ctx.get_assignment(i_ge_0) == l_true &&
ctx.get_assignment(i_lt_len_s) == l_true) {
@ -1233,10 +1231,9 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
}
}
else if (m_sk.is_pre(e, s, i)) {
expr_ref zero(m_autil.mk_int(0), m);
bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
literal i_ge_0 = i_is_zero?true_literal:mk_simplified_literal(m_autil.mk_ge(i, zero));
literal i_lt_len_s = ~mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero));
literal i_ge_0 = i_is_zero?true_literal:m_ax.mk_ge(i, 0);
literal i_lt_len_s = ~m_ax.mk_ge(mk_sub(i, mk_len(s)), 0);
literal _lits[2] = { i_ge_0, i_lt_len_s };
if (ctx.get_assignment(i_ge_0) == l_true &&
ctx.get_assignment(i_lt_len_s) == l_true) {
@ -1247,9 +1244,8 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
}
}
else if (m_sk.is_post(e, s, i)) {
expr_ref zero(m_autil.mk_int(0), m);
literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
literal len_s_ge_i = mk_simplified_literal(m_autil.mk_ge(mk_sub(mk_len(s), i), zero));
literal i_ge_0 = m_ax.mk_ge(i, 0);
literal len_s_ge_i = m_ax.mk_ge(mk_sub(mk_len(s), i), 0);
literal _lits[2] = { i_ge_0, len_s_ge_i };
if (ctx.get_assignment(i_ge_0) == l_true &&
ctx.get_assignment(len_s_ge_i) == l_true) {
@ -1264,7 +1260,7 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
// e = tail(s, l), len(s) <= l => len(tail(s, l)) = 0
expr_ref len_s = mk_len(s);
literal len_s_gt_l = mk_simplified_literal(m_autil.mk_ge(mk_sub(len_s, l), m_autil.mk_int(1)));
literal len_s_gt_l = m_ax.mk_ge(mk_sub(len_s, l), 1);
switch (ctx.get_assignment(len_s_gt_l)) {
case l_true:
len = mk_sub(mk_sub(len_s, l), m_autil.mk_int(1));
@ -1288,248 +1284,6 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
}
bool theory_seq::branch_nqs() {
for (unsigned i = 0; i < m_nqs.size(); ++i) {
ne n = m_nqs[i];
lbool r = branch_nq(n);
switch (r) {
case l_undef: // needs assignment to a literal.
return true;
case l_true: // disequality is satisfied.
break;
case l_false: // needs to be expanded.
if (m_nqs.size() > 1) {
ne n2 = m_nqs[m_nqs.size() - 1];
m_nqs.set(0, n2);
}
m_nqs.pop_back();
return true;
}
}
return false;
}
lbool theory_seq::branch_nq(ne const& n) {
context& ctx = get_context();
literal eq_len = mk_eq(mk_len(n.l()), mk_len(n.r()), false);
ctx.mark_as_relevant(eq_len);
switch (ctx.get_assignment(eq_len)) {
case l_false:
TRACE("seq", ctx.display_literal_smt2(tout << "lengths are different: ", eq_len) << "\n";);
return l_true;
case l_undef:
return l_undef;
default:
break;
}
literal eq = mk_eq(n.l(), n.r(), false);
literal len_gt = mk_literal(m_autil.mk_ge(mk_len(n.l()), m_autil.mk_int(1)));
ctx.mark_as_relevant(len_gt);
switch (ctx.get_assignment(len_gt)) {
case l_false:
add_axiom(eq, ~eq_len, len_gt);
return l_false;
case l_undef:
return l_undef;
default:
break;
}
expr_ref h1(m), t1(m), h2(m), t2(m);
mk_decompose(n.l(), h1, t1);
mk_decompose(n.r(), h2, t2);
literal eq_head = mk_eq(h1, h2, false);
ctx.mark_as_relevant(eq_head);
switch (ctx.get_assignment(eq_head)) {
case l_false:
TRACE("seq", ctx.display_literal_smt2(tout << "heads are different: ", eq_head) << "\n";);
return l_true;
case l_undef:
return l_undef;
default:
break;
}
// l = r or |l| != |r| or |l| > 0
// l = r or |l| != |r| or h1 != h2 or t1 != t2
add_axiom(eq, ~eq_len, len_gt);
add_axiom(eq, ~eq_len, ~eq_head, ~mk_eq(t1, t2, false));
return l_false;
}
bool theory_seq::solve_nqs(unsigned i) {
context & ctx = get_context();
for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) {
if (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();
}
bool theory_seq::solve_ne(unsigned idx) {
context& ctx = get_context();
ne const& n = m_nqs[idx];
TRACE("seq", display_disequation(tout << "solve: ", n););
unsigned num_undef_lits = 0;
for (literal lit : n.lits()) {
switch (ctx.get_assignment(lit)) {
case l_false:
TRACE("seq", display_disequation(tout << "has false literal\n", n);
ctx.display_literal_verbose(tout, lit);
tout << "\n" << lit << " " << ctx.is_relevant(lit) << "\n";
);
return true;
case l_true:
break;
case l_undef:
++num_undef_lits;
break;
}
}
bool updated = false;
dependency* new_deps = n.dep();
vector<expr_ref_vector> new_ls, new_rs;
literal_vector new_lits(n.lits());
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 = nullptr;
bool change = false;
if (!canonize(n.ls(i), ls, deps, change)) return false;
if (!canonize(n.rs(i), rs, deps, change)) return false;
if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, change)) {
TRACE("seq", display_disequation(tout << "reduces to false: ", n);
tout << n.ls(i) << " -> " << ls << "\n";
tout << n.rs(i) << " -> " << rs << "\n";);
return true;
}
else if (!change) {
TRACE("seq", tout << "no change " << n.ls(i) << " " << n.rs(i) << "\n";);
if (updated) {
new_ls.push_back(n.ls(i));
new_rs.push_back(n.rs(i));
}
continue;
}
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;
if (!ls.empty() || !rs.empty()) {
new_ls.push_back(ls);
new_rs.push_back(rs);
}
TRACE("seq",
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) {
expr* nl = lhs[j].get();
expr* nr = rhs[j].get();
if (m_util.is_seq(nl) || m_util.is_re(nl)) {
ls.reset();
rs.reset();
m_util.str.get_concat_units(nl, ls);
m_util.str.get_concat_units(nr, rs);
new_ls.push_back(ls);
new_rs.push_back(rs);
}
else if (nl != nr) {
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 = m_dm.mk_join(deps, new_deps);
}
}
TRACE("seq", display_disequation(tout << "updated: " << updated << " undef lits: " << num_undef_lits << "\n", n););
if (!updated && num_undef_lits == 0) {
return false;
}
if (!updated) {
for (unsigned j = 0; j < n.ls().size(); ++j) {
new_ls.push_back(n.ls(j));
new_rs.push_back(n.rs(j));
}
}
if (num_undef_lits == 1 && new_ls.empty()) {
literal_vector lits;
literal undef_lit = null_literal;
for (literal lit : new_lits) {
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;
}
if (updated) {
if (num_undef_lits == 0 && new_ls.empty()) {
TRACE("seq", tout << "conflict\n";);
dependency* deps1 = nullptr;
if (explain_eq(n.l(), n.r(), deps1)) {
literal diseq = mk_eq(n.l(), n.r(), false);
if (ctx.get_assignment(diseq) == l_false) {
new_lits.reset();
new_lits.push_back(~diseq);
new_deps = deps1;
TRACE("seq", tout << "conflict explained\n";);
}
}
set_conflict(new_deps, new_lits);
SASSERT(m_new_propagation);
}
else {
m_nqs.push_back(ne(n.l(), n.r(), new_ls, new_rs, new_lits, new_deps));
TRACE("seq", display_disequation(tout << "updated: ", m_nqs[m_nqs.size()-1]););
}
}
return updated;
}
bool theory_seq::solve_nc(unsigned idx) {
@ -1540,7 +1294,6 @@ bool theory_seq::solve_nc(unsigned idx) {
#if 1
expr* a = nullptr, *b = nullptr;
VERIFY(m_util.str.is_contains(n.contains(), a, b));
expr_ref head(m), tail(m);
literal pre, cnt, ctail, emp;
lbool is_gt = ctx.get_assignment(len_gt);
TRACE("seq", ctx.display_literal_smt2(tout << len_gt << " := " << is_gt << "\n", len_gt) << "\n";);
@ -1582,18 +1335,7 @@ bool theory_seq::solve_nc(unsigned idx) {
}
IF_VERBOSE(0, verbose_stream() << n.contains() << "\n");
#endif
mk_decompose(a, head, tail);
expr_ref pref(m_util.str.mk_prefix(b, a), m);
expr_ref postf(m_util.str.mk_contains(tail, b), m);
m_rewrite(pref);
m_rewrite(postf);
pre = mk_literal(pref);
cnt = mk_literal(n.contains());
ctail = mk_literal(postf);
emp = mk_literal(m_util.str.mk_is_empty(a));
add_axiom(cnt, ~pre);
add_axiom(cnt, ~ctail);
add_axiom(emp, mk_eq(a, m_util.str.mk_concat(head, tail), false));
m_ax.unroll_not_contains(n.contains());
return true;
#endif
@ -1983,12 +1725,12 @@ std::ostream& theory_seq::display_disequation(std::ostream& out, ne const& e) co
if (!e.lits().empty()) {
out << "\n";
}
for (unsigned j = 0; j < e.ls().size(); ++j) {
for (expr* t : e.ls(j)) {
for (unsigned j = 0; j < e.eqs().size(); ++j) {
for (expr* t : e[j].first) {
out << mk_bounded_pp(t, m, 2) << " ";
}
out << " != ";
for (expr* t : e.rs(j)) {
for (expr* t : e[j].second) {
out << mk_bounded_pp(t, m, 2) << " ";
}
out << "\n";
@ -2088,9 +1830,9 @@ void theory_seq::init_model(model_generator & mg) {
m_factory->register_value(n.r());
}
for (ne const& n : m_nqs) {
for (unsigned i = 0; i < n.ls().size(); ++i) {
init_model(n.ls(i));
init_model(n.rs(i));
for (unsigned i = 0; i < n.eqs().size(); ++i) {
init_model(n[i].first);
init_model(n[i].second);
}
}
}
@ -2308,8 +2050,9 @@ void theory_seq::validate_model(model& mdl) {
for (auto const& eq : m_eqs) {
expr_ref_vector ls = eq.ls();
expr_ref_vector rs = eq.rs();
expr_ref l(m_util.str.mk_concat(ls), m);
expr_ref r(m_util.str.mk_concat(rs), m);
sort* srt = m.get_sort(ls.get(0));
expr_ref l(m_util.str.mk_concat(ls, srt), m);
expr_ref r(m_util.str.mk_concat(rs, srt), m);
if (!mdl.are_equal(l, r)) {
IF_VERBOSE(0, verbose_stream() << "equality failed: " << l << " = " << r << "\nbut\n" << mdl(l) << " != " << mdl(r) << "\n");
}
@ -3071,7 +2814,7 @@ void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) {
expr* s2 = s;
for (unsigned j = 0; j <= _idx; ++j) {
mk_decompose(s2, head, tail);
m_sk.decompose(s2, head, tail);
elems.push_back(head);
len1 = mk_len(s2);
len2 = m_autil.mk_add(m_autil.mk_int(1), mk_len(tail));
@ -3257,8 +3000,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
propagate_non_empty(lit, e2);
dependency* dep = m_dm.mk_leaf(assumption(lit));
// |e1| - |e2| <= -1
literal len_gt = mk_simplified_literal(m_autil.mk_le(mk_sub(mk_len(e1), mk_len(e2)),
m_autil.mk_int(-1)));
literal len_gt = m_ax.mk_le(mk_sub(mk_len(e1), mk_len(e2)), -1);
ctx.force_phase(len_gt);
m_ncs.push_back(nc(expr_ref(e, m), len_gt, dep));
}
@ -3330,7 +3072,6 @@ lbool theory_seq::regex_are_equal(expr* _r1, expr* _r2) {
m_rewrite(diff);
eautomaton* aut = get_automaton(diff);
if (!aut) {
std::cout << diff << "\n";
return l_undef;
}
else if (aut->is_empty()) {
@ -3449,10 +3190,7 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) {
if (ctx.get_base_level() > ctx.get_scope_level() - num_scopes) {
m_replay.reset();
}
if (m_len_prop_lvl > (int) ctx.get_scope_level()) {
m_len_prop_lvl = ctx.get_scope_level();
m_len_offset.reset();
}
m_offset_eq.pop_scope_eh(num_scopes);
}
void theory_seq::restart_eh() {
@ -3513,13 +3251,11 @@ literal theory_seq::mk_accept(expr* s, expr* idx, expr* re, expr* state) {
}
bool theory_seq::is_accept(expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut) {
if (is_accept(e)) {
expr* n = nullptr;
if (m_sk.is_accept(e, s, idx, re, n)) {
rational r;
s = to_app(e)->get_arg(0);
idx = to_app(e)->get_arg(1);
re = to_app(e)->get_arg(2);
TRACE("seq", tout << mk_pp(re, m) << "\n";);
VERIFY(m_autil.is_numeral(to_app(e)->get_arg(3), r));
VERIFY(m_autil.is_numeral(n, r));
SASSERT(r.is_unsigned());
i = r.get_unsigned();
aut = get_automaton(re);
@ -3550,7 +3286,7 @@ void theory_seq::propagate_step(literal lit, expr* step) {
// skip
}
else {
propagate_lit(nullptr, 1, &lit, ~mk_literal(m_autil.mk_le(len_s, idx)));
propagate_lit(nullptr, 1, &lit, ~m_ax.mk_le(len_s, _idx));
}
ensure_nth(lit, s, idx);

63
src/smt/theory_seq.h
View file

@ -33,6 +33,7 @@ Revision History:
#include "smt/theory_seq_empty.h"
#include "smt/seq_skolem.h"
#include "smt/seq_axioms.h"
#include "smt/seq_offset_eq.h"
namespace smt {
@ -178,9 +179,12 @@ namespace smt {
return eq(m_eq_id++, ls, rs, dep);
}
// equalities that are decomposed by conacatenations
typedef std::pair<expr_ref_vector, expr_ref_vector> decomposed_eq;
class ne {
expr_ref m_l, m_r;
vector<expr_ref_vector> m_lhs, m_rhs;
vector<decomposed_eq> m_eqs;
literal_vector m_lits;
dependency* m_dep;
public:
@ -188,36 +192,34 @@ namespace smt {
m_l(l), m_r(r), m_dep(dep) {
expr_ref_vector ls(l.get_manager()); ls.push_back(l);
expr_ref_vector rs(r.get_manager()); rs.push_back(r);
m_lhs.push_back(ls);
m_rhs.push_back(rs);
m_eqs.push_back(std::make_pair(ls, rs));
}
ne(expr_ref const& _l, expr_ref const& _r, vector<expr_ref_vector> const& l, vector<expr_ref_vector> const& r, literal_vector const& lits, dependency* dep):
ne(expr_ref const& _l, expr_ref const& _r, vector<decomposed_eq> const& eqs, literal_vector const& lits, dependency* dep):
m_l(_l), m_r(_r),
m_lhs(l),
m_rhs(r),
m_eqs(eqs),
m_lits(lits),
m_dep(dep) {}
m_dep(dep) {
}
ne(ne const& other):
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) {}
m_eqs(other.m_eqs),
m_lits(other.m_lits), m_dep(other.m_dep) {}
ne& operator=(ne const& other) {
if (this != &other) {
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_eqs.reset(); m_eqs.append(other.m_eqs);
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]; }
vector<decomposed_eq> const& eqs() const { return m_eqs; }
decomposed_eq const& operator[](unsigned i) const { return m_eqs[i]; }
literal_vector const& lits() const { return m_lits; }
literal lits(unsigned i) const { return m_lits[i]; }
dependency* dep() const { return m_dep; }
@ -334,7 +336,6 @@ namespace smt {
}
};
struct s_in_re {
literal m_lit;
expr* m_s;
@ -377,11 +378,11 @@ namespace smt {
bool m_lts_checked;
unsigned m_eq_id;
th_union_find m_find;
seq_offset_eq m_offset_eq;
obj_ref_map<ast_manager, expr, unsigned_vector> m_overlap;
obj_ref_map<ast_manager, expr, unsigned_vector> m_overlap2;
obj_map<enode, obj_map<enode, int>> m_len_offset;
int m_len_prop_lvl;
seq_factory* m_factory; // value factory
exclusion_table m_exclude; // set of asserted disequalities.
@ -408,6 +409,7 @@ namespace smt {
stats m_stats;
ptr_vector<expr> m_todo, m_concat;
expr_ref_vector m_ls, m_rs, m_lhs, m_rhs;
expr_ref_pair_vector m_new_eqs;
bool m_has_seq;
// maintain automata with regular expressions.
@ -457,8 +459,6 @@ namespace smt {
app* get_ite_value(expr* a);
void get_ite_concat(ptr_vector<expr>& head, ptr_vector<expr>& tail);
void len_offset(expr* e, rational val);
void prop_arith_to_len_offset();
int find_fst_non_empty_idx(expr_ref_vector const& x);
expr* find_fst_non_empty_var(expr_ref_vector const& x);
void find_max_eq_len(expr_ref_vector const& ls, expr_ref_vector const& rs);
@ -486,11 +486,13 @@ namespace smt {
void branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units);
bool branch_variable_eq(eq const& e);
bool branch_binary_variable(eq const& e);
bool eq_unit(expr* const& l, expr* const &r) const;
bool eq_unit(expr* l, expr* r) const;
unsigned_vector overlap(expr_ref_vector const& ls, expr_ref_vector const& rs);
unsigned_vector overlap2(expr_ref_vector const& ls, expr_ref_vector const& rs);
bool branch_ternary_variable_base(dependency* dep, unsigned_vector const & indexes, expr* const& x, expr_ref_vector const& xs, expr* const& y1, expr_ref_vector const& ys, expr* const& y2);
bool branch_ternary_variable_base2(dependency* dep, unsigned_vector const& indexes, expr_ref_vector const& xs, expr* const& x, expr* const& y1, expr_ref_vector const& ys, expr* const& y2);
bool branch_ternary_variable_base(dependency* dep, unsigned_vector const & indexes, expr * x,
expr_ref_vector const& xs, expr * y1, expr_ref_vector const& ys, expr * y2);
bool branch_ternary_variable_base2(dependency* dep, unsigned_vector const& indexes, expr_ref_vector const& xs,
expr * x, expr * y1, expr_ref_vector const& ys, expr * y2);
bool branch_ternary_variable(eq const& e, bool flag1 = false);
bool branch_ternary_variable2(eq const& e, bool flag1 = false);
bool branch_quat_variable(eq const& e);
@ -508,7 +510,7 @@ namespace smt {
bool check_contains();
bool check_lts();
bool solve_eqs(unsigned start);
bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep, unsigned idx);
bool solve_eq(unsigned idx);
bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
bool lift_ite(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
bool solve_unit_eq(expr* l, expr* r, dependency* dep);
@ -530,15 +532,21 @@ namespace smt {
bool reduce_length(unsigned i, unsigned j, bool front, expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps);
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(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_ref_vector const& es) { SASSERT(!es.empty()); return expr_ref(m_util.str.mk_concat(es.size(), es.c_ptr()), m); }
expr_ref mk_concat(ptr_vector<expr> const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.c_ptr()); }
expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es, m.get_sort(es[0])), m); }
expr_ref mk_concat(unsigned n, expr*const* es, sort* s) { return expr_ref(m_util.str.mk_concat(n, es, s), m); }
expr_ref mk_concat(expr_ref_vector const& es, sort* s) { return mk_concat(es.size(), es.c_ptr(), s); }
expr_ref mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty()); return expr_ref(m_util.str.mk_concat(es.size(), es.c_ptr(), m.get_sort(es[0])), m); }
expr_ref mk_concat(ptr_vector<expr> const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.c_ptr(), m.get_sort(es[0])); }
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);
bool solve_ne(unsigned i);
bool solve_nc(unsigned i);
bool check_ne_literals(unsigned idx, unsigned& num_undef_lits);
bool propagate_ne2lit(unsigned idx);
bool propagate_ne2eq(unsigned idx);
bool propagate_ne2eq(unsigned idx, expr_ref_vector const& es);
bool reduce_ne(unsigned idx);
bool branch_nqs();
lbool branch_nq(ne const& n);
@ -628,7 +636,6 @@ namespace smt {
expr_ref mk_sub(expr* a, expr* b);
expr_ref mk_add(expr* a, expr* b);
expr_ref mk_len(expr* s);
enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }
dependency* mk_join(dependency* deps, literal lit);
dependency* mk_join(dependency* deps, literal_vector const& lits);