Merge pull request #6305 from diffblue/smt2_float_sorts

SMT-LIB2: parse FloatX sorts

Author: kroening

regression/smt2_solver/fp/basic-fp3.desc

@@ -0,0 +1,10 @@
+CORE
+basic-fp3.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+\(define-fun a \(\) \(_ FloatingPoint 5 11\) .*\)
+\(define-fun b \(\) \(_ FloatingPoint 8 24\) .*\)
+\(define-fun c \(\) \(_ FloatingPoint 11 53\) .*\)
+\(define-fun d \(\) \(_ FloatingPoint 15 113\) .*\)
+--

regression/smt2_solver/fp/basic-fp3.smt2

@@ -0,0 +1,9 @@
+(set-logic FP)
+
+(declare-fun a () Float16)
+(declare-fun b () Float32)
+(declare-fun c () Float64)
+(declare-fun d () Float128)
+
+(check-sat)
+(get-model)

src/solvers/smt2/smt2_parser.cpp

@@ -1405,6 +1405,19 @@ void smt2_parsert::setup_sorts()
   sorts["Int"] = [] { return integer_typet(); };
   sorts["Real"] = [] { return real_typet(); };
 
+  sorts["Float16"] = [] {
+    return ieee_float_spect::half_precision().to_type();
+  };
+  sorts["Float32"] = [] {
+    return ieee_float_spect::single_precision().to_type();
+  };
+  sorts["Float64"] = [] {
+    return ieee_float_spect::double_precision().to_type();
+  };
+  sorts["Float128"] = [] {
+    return ieee_float_spect::quadruple_precision().to_type();
+  };
+
   sorts["BitVec"] = [this] {
     if(next_token() != smt2_tokenizert::NUMERAL)
       throw error("expected numeral as bit-width");