smt expr: fold comparison between unaligned concats with at least one constant
MODIFY
smt/expr.cpp
smt/expr.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "smt/expr.h"
+#include "smt/exprs.h"
#include "smt/ctx.h"
#include "util/compiler.h"
#include <algorithm>
@@ -1215,33 +1216,55 @@ expr expr::cmp_eq(const expr &rhs, bool simplify) const {
if (auto app = isAppOf(Z3_OP_CONCAT)) {
unsigned num_args = Z3_get_app_num_args(ctx(), app);
if (rhs.isConst()) {
- set<expr> eqs;
+ AndExpr eqs;
unsigned high = bits();
for (unsigned i = 0; i < num_args; ++i) {
expr arg = Z3_get_app_arg(ctx(), app, i);
unsigned low = high - arg.bits();
- eqs.emplace(arg == rhs.extract(high - 1, low));
+ eqs.add(arg == rhs.extract(high - 1, low));
high = low;
}
- return mk_and(eqs);
+ return eqs();
}
if (auto app_rhs = rhs.isAppOf(Z3_OP_CONCAT);
app_rhs != nullptr &&
num_args == Z3_get_app_num_args(ctx(), app_rhs)) {
- set<expr> eqs;
- bool ok = true;
+ AndExpr eqs;
+ bool all_aligned = true;
+ unsigned l_idx = 0, r_idx = 0;
for (unsigned i = 0; i < num_args; ++i) {
expr lhs = Z3_get_app_arg(ctx(), app, i);
expr rhs = Z3_get_app_arg(ctx(), app_rhs, i);
- if (lhs.bits() != rhs.bits()) {
- ok = false;
- break;
+ unsigned l_bits = lhs.bits();
+ unsigned r_bits = rhs.bits();
+ all_aligned &= l_bits == r_bits;
+
+ if (l_idx == r_idx && l_bits == r_bits) {
+ eqs.add(lhs == rhs);
+ }
+ // even if the concats aren't aligned, we still compare the constant
+ // bits in an attempt to prove the comparison false
+ else if (lhs.isConst() && rhs.isConst()) {
+ // r .. l .. r+sz
+ if (l_idx >= r_idx && l_idx < (r_idx + r_bits)) {
+ unsigned overlap = min(r_bits - (l_idx - r_idx), l_bits);
+ eqs.add(lhs.extract(l_bits-1, l_bits - overlap) ==
+ rhs.extract(overlap-1, 0));
}
- eqs.emplace(lhs == rhs);
+ else if (r_idx >= l_idx && r_idx < (l_idx + l_bits)) {
+ unsigned overlap = min(l_bits - (r_idx - l_idx), r_bits);
+ eqs.add(lhs.extract(overlap-1, 0) ==
+ rhs.extract(r_bits-1, r_bits - overlap));
}
- if (ok)
- return mk_and(eqs);
+ }
+ l_idx += l_bits;
+ r_idx += r_bits;
+ }
+ assert(l_idx == r_idx);
+
+ if (all_aligned || !eqs)
+ return eqs();
}
}

smt expr: fold comparison between unaligned concats with at least one constant