mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
use expr_ref on mk_concat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
13413d0529
commit
b38abf64d7
|
@ -415,9 +415,9 @@ bool theory_seq::branch_binary_variable(eq const& e) {
|
|||
expr_ref Y1(mk_skolem(symbol("seq.left"), x, y), m);
|
||||
expr_ref Y2(mk_skolem(symbol("seq.right"), x, y), m);
|
||||
ys.push_back(Y1);
|
||||
expr_ref ysY1(mk_concat(ys));
|
||||
expr_ref xsE(mk_concat(xs));
|
||||
expr_ref Y1Y2(mk_concat(Y1, Y2));
|
||||
expr_ref ysY1 = mk_concat(ys);
|
||||
expr_ref xsE = mk_concat(xs);
|
||||
expr_ref Y1Y2 = mk_concat(Y1, Y2);
|
||||
dependency* dep = e.dep();
|
||||
propagate_eq(dep, ~lit, x, ysY1);
|
||||
propagate_eq(dep, ~lit, y, Y1Y2);
|
||||
|
@ -524,9 +524,9 @@ bool theory_seq::eq_unit(expr* const& l, expr* const &r) const {
|
|||
unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector const& rs) {
|
||||
SASSERT(!ls.empty() && !rs.empty());
|
||||
unsigned_vector res;
|
||||
expr* l = mk_concat(ls);
|
||||
expr* r = mk_concat(rs);
|
||||
expr* pair = m.mk_eq(l,r);
|
||||
expr_ref l = mk_concat(ls);
|
||||
expr_ref r = mk_concat(rs);
|
||||
expr_ref pair(m.mk_eq(l,r), m);
|
||||
if (m_overlap.find(pair, res)) {
|
||||
return res;
|
||||
}
|
||||
|
@ -535,7 +535,7 @@ unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector c
|
|||
if (eq_unit(ls[i], rs.back())) {
|
||||
bool same = true;
|
||||
if (i >= 1) {
|
||||
for (unsigned j = i-1; j>=0 && rs.size()+j-i>=1; --j) {
|
||||
for (unsigned j = i - 1; rs.size() + j >= 1 + i; --j) {
|
||||
if (!eq_unit(ls[j], rs[rs.size()+j-i-1])) {
|
||||
same = false;
|
||||
break;
|
||||
|
@ -556,9 +556,9 @@ unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector c
|
|||
unsigned_vector theory_seq::overlap2(expr_ref_vector const& ls, expr_ref_vector const& rs) {
|
||||
SASSERT(!ls.empty() && !rs.empty());
|
||||
unsigned_vector res;
|
||||
expr* l = mk_concat(ls);
|
||||
expr* r = mk_concat(rs);
|
||||
expr* pair = m.mk_eq(l,r);
|
||||
expr_ref l = mk_concat(ls);
|
||||
expr_ref r = mk_concat(rs);
|
||||
expr_ref pair(m.mk_eq(l,r), m);
|
||||
if (m_overlap2.find(pair, res)) {
|
||||
return res;
|
||||
}
|
||||
|
@ -567,7 +567,7 @@ unsigned_vector theory_seq::overlap2(expr_ref_vector const& ls, expr_ref_vector
|
|||
if (eq_unit(ls[i],rs[0])) {
|
||||
bool same = true;
|
||||
unsigned j = i+1;
|
||||
while (j<ls.size() && j-i<rs.size()) {
|
||||
while (j < ls.size() && j-i < rs.size()) {
|
||||
if (!eq_unit(ls[j], rs[j-i])) {
|
||||
same = false;
|
||||
break;
|
||||
|
@ -582,8 +582,9 @@ unsigned_vector theory_seq::overlap2(expr_ref_vector const& ls, expr_ref_vector
|
|||
return result;
|
||||
}
|
||||
|
||||
bool theory_seq::branch_ternary_variable_base(dependency* dep, unsigned_vector indexes,
|
||||
expr* const& x, expr_ref_vector const& xs, expr* const& y1, expr_ref_vector const& ys, expr* const& y2) {
|
||||
bool theory_seq::branch_ternary_variable_base(
|
||||
dependency* dep, unsigned_vector indexes,
|
||||
expr* const& x, expr_ref_vector const& xs, expr* const& y1, expr_ref_vector const& ys, expr* const& y2) {
|
||||
context& ctx = get_context();
|
||||
bool change = false;
|
||||
for (auto ind : indexes) {
|
||||
|
@ -610,7 +611,7 @@ bool theory_seq::branch_ternary_variable_base(dependency* dep, unsigned_vector i
|
|||
propagate_eq(dep, lits, y2, xs2E, true);
|
||||
if (ind > ys.size()) {
|
||||
expr_ref xs1E(m_util.str.mk_concat(ind-ys.size(), xs.c_ptr()), m);
|
||||
expr_ref xxs1E(mk_concat(x, xs1E), m);
|
||||
expr_ref xxs1E = mk_concat(x, xs1E);
|
||||
propagate_eq(dep, lits, xxs1E, y1, true);
|
||||
}
|
||||
else if (ind == ys.size()) {
|
||||
|
@ -618,7 +619,7 @@ bool theory_seq::branch_ternary_variable_base(dependency* dep, unsigned_vector i
|
|||
}
|
||||
else {
|
||||
expr_ref ys1E(m_util.str.mk_concat(ys.size()-ind, ys.c_ptr()), m);
|
||||
expr_ref y1ys1E(mk_concat(y1, ys1E), m);
|
||||
expr_ref y1ys1E = mk_concat(y1, ys1E);
|
||||
propagate_eq(dep, lits, x, y1ys1E, true);
|
||||
}
|
||||
return true;
|
||||
|
@ -661,12 +662,12 @@ bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) {
|
|||
return true;
|
||||
|
||||
// x ++ xs = y1 ++ ys ++ y2 => x = y1 ++ ys ++ z, z ++ xs = y2
|
||||
expr_ref xsE(mk_concat(xs), m);
|
||||
expr_ref ysE(mk_concat(ys), m);
|
||||
expr_ref y1ys(mk_concat(y1, ysE));
|
||||
expr_ref xsE = mk_concat(xs);
|
||||
expr_ref ysE = mk_concat(ys);
|
||||
expr_ref y1ys = mk_concat(y1, ysE);
|
||||
expr_ref Z(mk_skolem(m_seq_align, y2, xsE, x, y1ys), m);
|
||||
expr_ref ZxsE(mk_concat(Z, xsE), m);
|
||||
expr_ref y1ysZ(mk_concat(y1ys, Z), m);
|
||||
expr_ref ZxsE = mk_concat(Z, xsE);
|
||||
expr_ref y1ysZ = mk_concat(y1ys, Z);
|
||||
if (indexes.empty()) {
|
||||
TRACE("seq", tout << "one case\n";);
|
||||
TRACE("seq", display_equation(tout, e););
|
||||
|
@ -726,7 +727,7 @@ bool theory_seq::branch_ternary_variable_base2(dependency* dep, unsigned_vector
|
|||
propagate_eq(dep, lits, 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 xs2x(mk_concat(xs2E, x), m);
|
||||
expr_ref xs2x = mk_concat(xs2E, x);
|
||||
propagate_eq(dep, lits, xs2x, y2, true);
|
||||
}
|
||||
else if (xs.size() - ind == ys.size()) {
|
||||
|
@ -734,7 +735,7 @@ bool theory_seq::branch_ternary_variable_base2(dependency* dep, unsigned_vector
|
|||
}
|
||||
else {
|
||||
expr_ref ys1E(m_util.str.mk_concat(ys.size()-xs.size()+ind, ys.c_ptr()+xs.size()-ind), m);
|
||||
expr_ref ys1y2(mk_concat(ys1E, y2), m);
|
||||
expr_ref ys1y2 = mk_concat(ys1E, y2);
|
||||
propagate_eq(dep, lits, x, ys1y2, true);
|
||||
}
|
||||
return true;
|
||||
|
@ -776,12 +777,12 @@ bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
|
|||
return true;
|
||||
|
||||
// xs ++ x = y1 ++ ys ++ y2 => xs ++ z = y1, x = z ++ ys ++ y2
|
||||
expr_ref xsE(mk_concat(xs), m);
|
||||
expr_ref ysE(mk_concat(ys), m);
|
||||
expr_ref ysy2(mk_concat(ysE, y2), m);
|
||||
expr_ref xsE = mk_concat(xs);
|
||||
expr_ref ysE = mk_concat(ys);
|
||||
expr_ref ysy2 = mk_concat(ysE, y2);
|
||||
expr_ref Z(mk_skolem(m_seq_align, x, ysy2, y1, xsE), m);
|
||||
expr_ref xsZ(mk_concat(xsE, Z), m);
|
||||
expr_ref Zysy2(mk_concat(Z, ysy2), m);
|
||||
expr_ref xsZ = mk_concat(xsE, Z);
|
||||
expr_ref Zysy2 = mk_concat(Z, ysy2);
|
||||
if (indexes.empty()) {
|
||||
TRACE("seq", tout << "one case\n";);
|
||||
TRACE("seq", display_equation(tout, e););
|
||||
|
@ -850,9 +851,9 @@ bool theory_seq::branch_quat_variable(eq const& e) {
|
|||
SASSERT(!xs.empty() && !ys.empty());
|
||||
|
||||
xs.push_back(x2);
|
||||
expr_ref xsx2(mk_concat(xs), m);
|
||||
expr_ref xsx2 = mk_concat(xs);
|
||||
ys.push_back(y2);
|
||||
expr_ref ysy2(mk_concat(ys), m);
|
||||
expr_ref ysy2 = mk_concat(ys);
|
||||
expr_ref x1(x1_l, m);
|
||||
expr_ref y1(y1_l, m);
|
||||
expr_ref sub(mk_sub(m_util.str.mk_length(x1_l), m_util.str.mk_length(y1_l)), m);
|
||||
|
@ -869,8 +870,8 @@ bool theory_seq::branch_quat_variable(eq const& e) {
|
|||
TRACE("seq", tout << "false branch\n";);
|
||||
TRACE("seq", display_equation(tout, e););
|
||||
expr_ref Z1(mk_skolem(m_seq_align, ysy2, xsx2, x1, y1), m);
|
||||
expr_ref y1Z1(mk_concat(y1, Z1), m);
|
||||
expr_ref Z1xsx2(mk_concat(Z1, xsx2), m);
|
||||
expr_ref y1Z1 = mk_concat(y1, Z1);
|
||||
expr_ref Z1xsx2 = mk_concat(Z1, xsx2);
|
||||
literal_vector lits;
|
||||
lits.push_back(~lit2);
|
||||
dependency* dep = e.dep();
|
||||
|
@ -882,8 +883,8 @@ bool theory_seq::branch_quat_variable(eq const& e) {
|
|||
TRACE("seq", tout << "true branch\n";);
|
||||
TRACE("seq", display_equation(tout, e););
|
||||
expr_ref Z2(mk_skolem(m_seq_align, xsx2, ysy2, y1, x1), m);
|
||||
expr_ref x1Z2(mk_concat(x1, Z2), m);
|
||||
expr_ref Z2ysy2(mk_concat(Z2, ysy2), m);
|
||||
expr_ref x1Z2 = mk_concat(x1, Z2);
|
||||
expr_ref Z2ysy2 = mk_concat(Z2, ysy2);
|
||||
literal_vector lits;
|
||||
lits.push_back(lit2);
|
||||
dependency* dep = e.dep();
|
||||
|
@ -1384,8 +1385,8 @@ bool theory_seq::branch_variable_mb() {
|
|||
for (auto elem : len2) l2 += elem;
|
||||
if (l1 != l2) {
|
||||
TRACE("seq", tout << "lengths are not compatible\n";);
|
||||
expr_ref l(mk_concat(e.ls()), m);
|
||||
expr_ref r(mk_concat(e.rs()), m);
|
||||
expr_ref l = mk_concat(e.ls());
|
||||
expr_ref r = mk_concat(e.rs());
|
||||
expr_ref lnl(m_util.str.mk_length(l), m), lnr(m_util.str.mk_length(r), m);
|
||||
propagate_eq(e.dep(), lnl, lnr, false);
|
||||
change = true;
|
||||
|
|
|
@ -443,7 +443,7 @@ namespace smt {
|
|||
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* mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty()); return m_util.str.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(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); }
|
||||
|
|
Loading…
Reference in a new issue