Support constant rotating in bit-blast

[QinshiWang]

Bit blasting should support functions like rotate_left when the amount of shifting is a constant. The code below is an example.

(declare-fun a () (_ BitVec 32))
(define-fun b () (_ BitVec 32) ((_ rotate_left 7) a))
(assert (= b b))
(apply bit-blast)

[LeventErkok]

This seems to work:

(declare-fun a () (_ BitVec 32))
(define-fun b () (_ BitVec 32) ((_ rotate_left 7) a))
(assert (= b b))
(apply (then simplify bit-blast))

yielding:

(goals
(goal
  :precision precise :depth 1)
)

[NikolajBjorner]

added nested simplification for self-contained use