smt: add (extract (sign_ext x)) simplification
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -426,6 +426,14 @@ bool expr::isExtract(expr &e, unsigned &high, unsigned &low) const {
return false;
}
+bool expr::isSignExt(expr &val) const {
+ if (auto app = isAppOf(Z3_OP_SIGN_EXT)) {
+ val = Z3_get_app_arg(ctx(), app, 0);
+ return true;
+ }
+ return false;
+}
+
bool expr::isAnd(expr &a, expr &b) const {
return isBinOp(a, b, Z3_OP_AND);
}
@@ -1488,6 +1496,15 @@ expr expr::extract(unsigned high, unsigned low) const {
if (isExtract(sub, high_2, low_2))
return sub.extract(high + low_2, low + low_2);
}
+ if (low == 0) {
+ expr val;
+ if (isSignExt(val)) {
+ auto val_bits = val.bits();
+ if (high < val_bits)
+ return val.extract(high, 0);
+ return val.sext(high - val_bits + 1);
+ }
+ }
{
expr a, b;
if (isConcat(a, b)) {

MODIFY
smt/expr.h
smt/expr.h
@@ -137,6 +137,7 @@ public:
bool isIf(expr &cond, expr &then, expr &els) const;
bool isConcat(expr &a, expr &b) const;
bool isExtract(expr &e, unsigned &high, unsigned &low) const;
+ bool isSignExt(expr &val) const;
bool isAnd(expr &a, expr &b) const;
bool isNot(expr &neg) const;
bool isAdd(expr &a, expr &b) const;

smt: add (extract (sign_ext x)) simplification