BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_AND) with special const.

[aniemetz]

All experiments on QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s).

x_m & concat(y_my, 0_n, z_mz) rewrites to concat(x[m-1:m-my] & y, 0_n, x[m-my-n-1:0] & z):

          | CVC4-base                              | CVC4-concatpullup-and0                |
BENCHMARK | SLVD   SAT   UNSAT   TO   MO   CPU[s]  | SLVD   SAT   UNSAT   TO  MO   CPU[s]  |
   totals | 38985 13843  25142  1089  28  991222.5 | 38994 13846  25148  1080 28  983990.8 |

Add x_m & concat(y_my, 1_n, z_mz) rewrites to concat(x[m-1:m-my] & y, 0_[n-1], x[m-my-n:m-my-n], x[m-my-n-1:0] & z):

          | CVC4-base                              | CVC4-concatpullup-and01                |
BENCHMARK | SLVD   SAT   UNSAT   TO   MO   CPU[s]  | SLVD   SAT   UNSAT   TO  MO   CPU[s]  |
   totals | 38985 13843  25142  1089  28  991222.5 | 38997 13848  25149  1077 28  984740.3 |

Add x_m & concat(y_my, ~0_n, z_mz) rewrites to concat(x[m-1:m-my] & y, x[m-my-1:m-my-n], x[m-my-n-1:0] & z):

          | CVC4-base                              | CVC4-concatpullup-and01~0                |
BENCHMARK | SLVD   SAT   UNSAT   TO   MO   CPU[s]  | SLVD   SAT   UNSAT   TO  MO   CPU[s]  |
   totals | 38985 13843  25142  1089  28  991222.5 | 38992 13844  25148  1082 28   984887.4|