Implement SMT-Lib SFloat/SDouble literals

Not quite done yet; but we can get some basic proofs going as is..