Generic BV cleanup.

BitVector theory:
* Express to_int in terms of to_uint and a new predicate
  is_signed_positive. I can't use sge directly because it has not been
  introduced yet, and it can't be re-ordered as it uses to_int.

* Add new axiom to link the two.

Generic BitVector driver:
* Re-ordering of the BV driver to match the theory.
* Remove to_uint_of_int axiom.
* Remove the new axiom linking is_signed_positive and sge.

Z3:
* Refactor Z3 specific BV driver, similar to what is done with CVC4. Make
  a note that explains Z3's bv2int is actually bv2nat despite
  the name.

CVC4:
* Simplify its BV driver slightly by moving to_uint printer into bv_gen.

Change-Id: I0a00ad1f65219a9e0896f542dd832b6055653dc5

Conflicts:
	drivers/cvc4_bv.gen
	drivers/z3_gnatprove.drv