smt expr: fold a + b == rhs -> false when applicable
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1189,6 +1189,8 @@ expr expr::cmp_eq(const expr &rhs, bool simplify) const {
return false;
return rhs == *this;
}
+ // constants on rhs from now.
+
if (rhs.isTrue())
return *this;
if (rhs.isFalse())
@@ -1215,6 +1217,7 @@ 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);
+ // (concat x y) == const -> x == const[..] /\ y == const[..]
if (rhs.isConst()) {
AndExpr eqs;
unsigned high = bits();
@@ -1227,6 +1230,7 @@ expr expr::cmp_eq(const expr &rhs, bool simplify) const {
return eqs();
}
+ // (concat ..) == (concat ..)
if (auto app_rhs = rhs.isAppOf(Z3_OP_CONCAT);
app_rhs != nullptr &&
num_args == Z3_get_app_num_args(ctx(), app_rhs)) {
@@ -1287,6 +1291,18 @@ expr expr::cmp_eq(const expr &rhs, bool simplify) const {
}
}
+ {
+ expr a, b;
+ if (isAdd(a, b)) {
+ // Pre: a >= 0, b >= 0, rhs u< b
+ // a + b == rhs -> false
+ if (a.isNegative().isFalse() &&
+ b.isNegative().isFalse() &&
+ (rhs.ult(a).isTrue() || rhs.ult(b).isTrue()))
+ return false;
+ }
+ }
+
// (a u% b) == c -> false if c u>= b
{
expr a, b;

smt expr: fold a + b == rhs -> false when applicable