smt: simplify extract from ashr (#1105)

AliveToolkit · Oct 31, 2024 · 2a95c52 · 2a95c52
1 parent 1665a69
commit 2a95c52
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/smt/expr.cpp b/smt/expr.cpp
@@ -497,6 +497,10 @@ bool expr::isSignExt(expr &val) const {
   return isUnOp(val, Z3_OP_SIGN_EXT);
 }
 
+bool expr::isAShr(expr &a, expr &b) const {
+  return isBinOp(a, b, Z3_OP_BASHR);
+}
+
 bool expr::isAnd(expr &a, expr &b) const {
   return isBinOp(a, b, Z3_OP_AND);
 }
@@ -1851,6 +1855,15 @@ expr expr::extract(unsigned high, unsigned low, unsigned depth) const {
       return val.sext(high - val_bits + 1);
     }
   }
+  {
+    expr a, b;
+    if (isAShr(a, b)) {
+      uint64_t shift;
+      if (b.isUInt(shift) && high + shift < a.bits()) {
+        return a.extract(high + shift, low + shift);
+      }
+    }
+  }
   {
     expr a, b;
     if (isConcat(a, b)) {

diff --git a/smt/expr.h b/smt/expr.h
@@ -135,6 +135,7 @@ class expr {
   bool isConcat(expr &a, expr &b) const;
   bool isExtract(expr &e, unsigned &high, unsigned &low) const;
   bool isSignExt(expr &val) const;
+  bool isAShr(expr &a, expr &b) const;
   bool isAnd(expr &a, expr &b) const;
   bool isNot(expr &neg) const;
   bool isAdd(expr &a, expr &b) const;