Fix Z3 Legacy Floating-Point Theory

[baierd]

The old Z3 version does not support FPs currently. Some problems are solved by #513, all remaining problems are found in the retranslation of SMT model values to Java values. There are 3 main problems that are solved, 2 of wich are not optimally solved for now (1 & 2) below:

1. NaN could not be detected, but crashed the normal evaluation. This is now detected based on the unique String representation of NaN.
2. +/-Infinity could not be detected, but crashed the normal evaluation. This is now detected based on the unique String representation of +/- inifity.
3. Normal FP values need to be built by their exponent and significand String representations pulled from the AST string. None other representation seems to be accurate somehow. Zeros need to be detected before this however, but thats easy.

This branch is based on #513 and should only be merged after #513.

[baierd]

Examples for calling the FP managers makeNumber() with single precisions and output of the model value of the constant based on multiple API calls. The exponents string representation is called: exp string, while the mantissas string representation is: mant string.

astToString() seems to only return the type with the names of special values or the bit values of sign, exponent, and mantissa.

getNumeralString() seems to be only the names of special values or the bit values of sign, exponent, and mantissa.

fpmgr.makeNumber(0.0, singlePrecType)
astToString:      (_ +zero 8 24)
getNumeralString: +zero
exp string:       0   mant string:  1

fpmgr.makeNumber(1.0, singlePrecType)
astToString:      (fp #b0 #x7f #b00000000000000000000000)
getNumeralString: 1.0 0
exp string:       0   mant string:  1

fpmgr.makeNumber(2.0, singlePrecType)
astToString:      (fp #b0 #x80 #b00000000000000000000000)
getNumeralString: 1.0 1
exp string:       1   mant string:  1

fpmgr.makeNumber(3.0, singlePrecType)
astToString:      (fp #b0 #x80 #b10000000000000000000000)
getNumeralString: 1.5 1
exp string:       1   mant string:  1.5

We might be able to detect zero based on the string representation.

Edit: just using the hex/binary representation of the AST after filtering out zeros works fine.

[kfriedberger]

looks good to me.