From b38abf64d73016385685689a34608758ca0f780d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Jul 2018 19:30:46 -0700 Subject: [PATCH] use expr_ref on mk_concat Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 71 +++++++++++++++++++++--------------------- src/smt/theory_seq.h | 2 +- 2 files changed, 37 insertions(+), 36 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index c2c3b1cfb..ef50cf3b6 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -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 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; diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index f03bdeb60..3bd6baba9 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -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 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); }