Document Builder expression simplifications

[andreistefanescu]

This is now a common pattern: optimizing an operation by checking if one of the arguments is ite c then a else b, where a and b are concrete, and pushing the operation down through the ite. One thing that's not as clear is what metrics we use to determine which operations should receive these optimizations—for instance, we apply this optimization to bvAndBits, but not bvXorBits. Was the set of operations to optimize chosen based on an assessment of which operations occurred most commonly in a large SAW proof? Something else?

Either way, it might be helpful to record this information in a Note somewhere. I'm thinking of something like this:

  bvZext sym w x
    ...

    -- See Note [ExprBuilder muxing optimizations]
    | Just (BaseIte _ _ c a b) <- asApp x
    , Just a_bv <- asBV a
    , Just b_bv <- asBV b = do
      Just LeqProof <- return $ isPosNat w
      a' <- bvLit sym w $ BV.zext w a_bv
      b' <- bvLit sym w $ BV.zext w b_bv
      bvIte sym c a' b'

  bvSext sym w x
    ...

    -- See Note [ExprBuilder muxing optimizations]
    | Just (BaseIte _ _ c a b) <- asApp x
    , Just a_bv <- asBV a
    , Just b_bv <- asBV b = do
      Just LeqProof <- return $ isPosNat w
      a' <- bvLit sym w $ BV.sext (bvWidth x) w a_bv
      b' <- bvLit sym w $ BV.sext (bvWidth x) w b_bv
      bvIte sym c a' b'

...

{-
Note [ExprBuilder muxing optimizations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Whenever we see certain operations of the form op (ite c then a else b), where a and b are concrete,
then we optimize it by ...

We do this because ...

We chose which optimizations receive this optimization by ...
-}

And then reference the Note in each place where we apply this optimization.

Originally posted by @RyanGlScott in #252 (comment)