SMTLIB's FP theory might require Reals/Reals_Ints and BV

[Gbury]

It seems to happen that some problems set their logic to QF_FP, and then use the to_fp function to convert a real to a floating point number (it happens in e.g. QF_FP/20170501-Heizmann-UltimateAutomizer/filter2_reinit_true-unreach-call.c_7.smt2).
The problem is that currently dolmen fails when that happens because the real number is not typed since neither the Reals nor the Reals_ints theory is used because QF_FP does not include them. So the question is:

• is the use of a real litteral illegal in QF_FP (and would need e.g. QF_LRAFP ?)
• does QF_FP means also using the Reals theory
• does the Floats theory includes litterals for Reals (which doesn't seem to be the case according to the description of the theory checked in the repo currently).

cc @bobot

[Gbury]

This also applies to the BV theory, as seen in QF_FP/20170501-Heizmann-UltimateAutomizer/water_pid_true-unreach-call.c_372.smt2 : the litteral syntax for binary and hexadecimal vector is specified in the float theory (and thus implemented by the Float theory in dolmen), but not the syntax for decimal bitvector litterals, which is used in the problem mentioned. So:

• is it a mistake in the description of the Float theory, which should include the litteral syntax
• should such uses be considered illegal ?

[bobot]

I believe they should be illegal, but it is very handy. For now I think we should accept whatever is accepted in the benchmarks if not too complicated, but at the same time, opening issues or thread on the ML for answering the question.

[Gbury]

Closed by #79