Proper type system for Expressions and Registers

[ThomasHaas]

This is an extension of #39.

Context: We currently have 2 types of expressions BExpr and IExpr. IExpr can either represent a mathematical integer or a bit vector expression. However, we only have one type of Register that always holds IExpr values.

Problems: It is easy to mix up operations of incompatible types. Currently, a lot of implicit conversions happen which somewhat circumvent the type mismatch problems. Proper typing can make the code more save, can avoid the implicit conversions and can make the encoding more efficient.

Possible solution:

• Add BVExpr and maybe use a common supertype ValueExpr for BVExpr and IExpr.
• For all Expr types add a corresponding Register type (BRegister, IRegister, BVRegister and possibly ValueRegister as a supertype of IRegister and BVRegister).
• Add toBoolFormula, toIntegerFormula and toBVFormula methods (possibly with a precision parameter for the latter) that allow conversions if necessary and avoid implicit conversions as much as possible (with properly typed registers, conversions should only be necessary when mixing theories).
• Do the same for getLastValueExpr (this one in particular can introduce a lot of implicit conversions right now)

The reason why a ValueExpr as a supertype for IExpr and BVExpr might be reasonable is because our domain of computation is always split into Booleans + the value domain of Integers, BitVectors or both.