improve transformation used by dreal driver
The driver for dreal uses a dedicated transformation keep_only_arithmetic
. The code for this transformation could be made more elegant, more compact, and could support more cases.
For example, this transformation would completely remove an hypothesis of the form
H: not (arith_fact \/ non_arith_fact)
whereas it could keep
H: not arith_fact