[fix, bitwuzla] Returned API calls to construct Shl, Shr and AShr exp…

…ressions.
S1eGa · Nov 20, 2023 · f2304ff · f2304ff
1 parent a9ae83d
commit f2304ff
Showing 1 changed file with 3 additions and 30 deletions.
diff --git a/lib/Solver/BitwuzlaBuilder.cpp b/lib/Solver/BitwuzlaBuilder.cpp
@@ -187,14 +187,7 @@ Term BitwuzlaBuilder::bvVarLeftShift(Term expr, Term shift) {
   Term shiftAsBv = castToBitVector(shift);
 
   unsigned width = getBVLength(exprAsBv);
-  Term res = bvZero(width);
-
-  // construct a big if-then-elif-elif-... with one case per possible shift
-  // amount
-  for (int i = width - 1; i >= 0; i--) {
-    res = iteExpr(eqExpr(shiftAsBv, bvConst32(width, i)),
-                  bvLeftShift(exprAsBv, i), res);
-  }
+  Term res = mk_term(Kind::BV_SHL, {exprAsBv, shiftAsBv});
 
   // If overshifting, shift to zero
   Term ex = bvLtExpr(shiftAsBv, bvConst32(getBVLength(shiftAsBv), width));
@@ -209,14 +202,7 @@ Term BitwuzlaBuilder::bvVarRightShift(Term expr, Term shift) {
   Term shiftAsBv = castToBitVector(shift);
 
   unsigned width = getBVLength(exprAsBv);
-  Term res = bvZero(width);
-
-  // construct a big if-then-elif-elif-... with one case per possible shift
-  // amount
-  for (int i = width - 1; i >= 0; i--) {
-    res = iteExpr(eqExpr(shiftAsBv, bvConst32(width, i)),
-                  bvRightShift(exprAsBv, i), res);
-  }
+  Term res = mk_term(Kind::BV_SHR, {exprAsBv, shiftAsBv});
 
   // If overshifting, shift to zero
   Term ex = bvLtExpr(shiftAsBv, bvConst32(getBVLength(shiftAsBv), width));
@@ -232,20 +218,7 @@ Term BitwuzlaBuilder::bvVarArithRightShift(Term expr, Term shift) {
 
   unsigned width = getBVLength(exprAsBv);
 
-  // get the sign bit to fill with
-  Term signedBool = bvBoolExtract(exprAsBv, width - 1);
-
-  // start with the result if shifting by width-1
-  Term res = constructAShrByConstant(exprAsBv, width - 1, signedBool);
-
-  // construct a big if-then-elif-elif-... with one case per possible shift
-  // amount
-  // XXX more efficient to move the ite on the sign outside all exprs?
-  // XXX more efficient to sign extend, right shift, then extract lower bits?
-  for (int i = width - 2; i >= 0; i--) {
-    res = iteExpr(eqExpr(shiftAsBv, bvConst32(width, i)),
-                  constructAShrByConstant(exprAsBv, i, signedBool), res);
-  }
+  Term res = mk_term(Kind::BV_ASHR, {exprAsBv, shiftAsBv});
 
   // If overshifting, shift to zero
   Term ex = bvLtExpr(shiftAsBv, bvConst32(getBVLength(shiftAsBv), width));