smt expr: simplify(= (+ a c1) (+ a  c2)) -> false
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -215,6 +215,17 @@ expr expr::mkQuantVar(unsigned i, Z3_sort sort) {
return Z3_mk_bound(ctx(), i, sort);
}
+bool expr::isBinOp(expr &a, expr &b, int z3op) const {
+ if (auto app = isAppOf(z3op)) {
+ if (Z3_get_domain_size(ctx(), decl()) != 2)
+ return false;
+ a = Z3_get_app_arg(ctx(), app, 0);
+ b = Z3_get_app_arg(ctx(), app, 1);
+ return true;
+ }
+ return false;
+}
+
expr expr::mkVar(const char *name, const expr &type) {
C2(type);
return ::mkVar(name, type.sort());
@@ -344,12 +355,7 @@ bool expr::isInt(int64_t &n) const {
}
bool expr::isEq(expr &lhs, expr &rhs) const {
- if (auto app = isAppOf(Z3_OP_EQ)) {
- lhs = Z3_get_app_arg(ctx(), app, 0);
- rhs = Z3_get_app_arg(ctx(), app, 1);
- return true;
- }
- return false;
+ return isBinOp(lhs, rhs, Z3_OP_EQ);
}
bool expr::isIf(expr &cond, expr &then, expr &els) const {
@@ -388,14 +394,7 @@ bool expr::isExtract(expr &e, unsigned &high, unsigned &low) const {
}
bool expr::isAnd(expr &a, expr &b) const {
- if (auto app = isAppOf(Z3_OP_AND)) {
- if (Z3_get_domain_size(ctx(), decl()) != 2)
- return false;
- a = Z3_get_app_arg(ctx(), app, 0);
- b = Z3_get_app_arg(ctx(), app, 1);
- return true;
- }
- return false;
+ return isBinOp(a, b, Z3_OP_AND);
}
bool expr::isNot(expr &neg) const {
@@ -406,6 +405,27 @@ bool expr::isNot(expr &neg) const {
return false;
}
+bool expr::isAdd(expr &a, expr &b) const {
+ return isBinOp(a, b, Z3_OP_BADD);
+}
+
+bool expr::isBasePlusOffset(expr &base, uint64_t &offset) const {
+ expr a, b;
+ if (isAdd(a, b)) {
+ if (a.isUInt(offset)) {
+ base = b;
+ return true;
+ }
+ if (b.isUInt(offset)) {
+ base = a;
+ return true;
+ }
+ }
+ base = *this;
+ offset = 0;
+ return true;
+}
+
bool expr::isConstArray(expr &val) const {
if (auto app = isAppOf(Z3_OP_CONST_ARRAY)) {
val = Z3_get_app_arg(ctx(), app, 0);
@@ -1027,6 +1047,7 @@ expr expr::cmp_eq(const expr &rhs, bool simplify) const {
if (rhs.isFalse())
return !*this;
+ // (= (= a bit) (= b bit)) -> (= a b)
{
expr lhs_a, lhs_b, rhs_a, rhs_b;
if (isEq(lhs_a, lhs_b) && lhs_a.bits() == 1 && rhs.isEq(rhs_a, rhs_b) &&
@@ -1034,6 +1055,17 @@ expr expr::cmp_eq(const expr &rhs, bool simplify) const {
return lhs_b == rhs_b;
}
+ // (= (+ a c1) (+ a c2)) -> false
+ {
+ expr lhs_base, rhs_base;
+ uint64_t lhs_offset, rhs_offset;
+ if (isBasePlusOffset(lhs_base, lhs_offset) &&
+ rhs.isBasePlusOffset(rhs_base, rhs_offset) &&
+ lhs_base.eq(rhs_base) &&
+ lhs_offset != rhs_offset)
+ return false;
+ }
+
if (auto app = isAppOf(Z3_OP_CONCAT)) {
unsigned num_args = Z3_get_app_num_args(ctx(), app);
if (rhs.isConst()) {

MODIFY
smt/expr.h
smt/expr.h
@@ -65,6 +65,8 @@ class expr {
static expr mkConst(Z3_func_decl decl);
static expr mkQuantVar(unsigned i, Z3_sort sort);
+ bool isBinOp(expr &a, expr &b, int z3op) const;
+
public:
expr() : ptr(0) {}
@@ -127,6 +129,8 @@ public:
bool isExtract(expr &e, unsigned &high, unsigned &low) const;
bool isAnd(expr &a, expr &b) const;
bool isNot(expr &neg) const;
+ bool isAdd(expr &a, expr &b) const;
+ bool isBasePlusOffset(expr &base, uint64_t &offset) const;
bool isConstArray(expr &val) const;
bool isStore(expr &array, expr &idx, expr &val) const;

smt expr: simplify(= (+ a c1) (+ a  c2)) -> false