Changing the handled operators in bv2int preprocessing pass (#4970)

Some of the bit-vector operators are directly translated to integers, while others are eliminated before the translation.
This PR changes the set of operators that we eliminate (and as a consequence, also the set of operators that we handle directly):

The only bit-wise operator that is translated is bvand. The rest are now eliminated.
bvneg is now eliminated.
The various division operators are still eliminated, but using different rewrite rules.
zero-extend and sign-extend are now handled directly.
shifting is changed to favor ITEs over non-linear multiplication.

1 files changed, 7 insertions, 6 deletions

diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2
index 998234a17..d213b0c3d 100644
--- a/test/regress/regress2/bv_to_int_shifts.smt2
+++ b/test/regress/regress2/bv_to_int_shifts.smt2
@@ -1,17 +1,18 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_BV)
-(declare-fun s () (_ BitVec 64))
-(declare-fun t () (_ BitVec 64))
-(declare-fun splust () (_ BitVec 64))
-(declare-fun shift1 () (_ BitVec 64))
-(declare-fun shift2 () (_ BitVec 64))
-(declare-fun negshift1 () (_ BitVec 64))
+(declare-fun s () (_ BitVec 4))
+(declare-fun t () (_ BitVec 4))
+(declare-fun splust () (_ BitVec 4))
+(declare-fun shift1 () (_ BitVec 4))
+(declare-fun shift2 () (_ BitVec 4))
+(declare-fun negshift1 () (_ BitVec 4))
 
 (assert (= shift1 (bvlshr s splust)))
 (assert (= shift2 (bvlshr t splust)))
 (assert (= negshift1 (bvneg shift1)))
 (assert (= splust (bvadd s t)))
 (assert (distinct negshift1 shift2))
+(assert (distinct s (bvshl s (_ bv4 4))))
 
 (check-sat)