Add mkZero, mkOne and mkUmulo to bv utils. (#1200)

Add mkZero, mkOne and mkUmulo to bv utils. (#1200)

This adds several utility functions for the theory BV. Function mkUmulo encodes an unsigned multiplication overflow detection operation, which we need for CBQI BV. In the future, we will introduce a Umulo node kind (and a corresponding bit-blasting strategy based on the encoding implemented in mkUmulo).