drivers/smt-libv2-floats.gen

   1 theory ieee_float.RoundingMode
   2    syntax type mode "RoundingMode"
   3    syntax function RNE "RNE"
   4    syntax function RNA "RNA"
   5    syntax function RTP "RTP"
   6    syntax function RTN "RTN"
   7    syntax function RTZ "RTZ"
   8
   9    syntax predicate to_nearest "(or (= %1 RNE) (= %1 RNA))"
  10 end
  11
  12 theory ieee_float.GenericFloat
  13    (* Part I *)
  14    syntax function abs  "(fp.abs %1)"
  15    syntax function neg  "(fp.neg %1)"
  16
  17    syntax function add  "(fp.add %1 %2 %3)"
  18    syntax function sub  "(fp.sub %1 %2 %3)"
  19    syntax function mul  "(fp.mul %1 %2 %3)"
  20    syntax function div  "(fp.div %1 %2 %3)"
  21
  22    syntax function fma  "(fp.fma %1 %2 %3 %4)"
  23
  24    syntax function sqrt "(fp.sqrt %1 %2)"
  25
  26    syntax function roundToIntegral "(fp.roundToIntegral %1 %2)"
  27
  28    syntax function min "(fp.min %1 %2)"
  29    syntax function max "(fp.max %1 %2)"
  30
  31    syntax predicate le  "(fp.leq %1 %2)"
  32    syntax predicate lt  "(fp.lt %1 %2)"
  33    syntax predicate ge  "(fp.geq %1 %2)"
  34    syntax predicate gt  "(fp.gt %1 %2)"
  35
  36    syntax predicate eq  "(fp.eq %1 %2)"
  37
  38    syntax predicate is_normal    "(fp.isNormal %1)"
  39    syntax predicate is_subnormal "(fp.isSubnormal %1)"
  40    syntax predicate is_zero      "(fp.isZero %1)"
  41    syntax predicate is_infinite  "(fp.isInfinite %1)"
  42    syntax predicate is_nan       "(fp.isNaN %1)"
  43    syntax predicate is_positive  "(fp.isPositive %1)"
  44    syntax predicate is_negative  "(fp.isNegative %1)"
  45
  46    (* We could do this here, but we get slightly slimmer VCs and avoid
  47       issues with Z3 if we do specialised versions of this for Float32 and
  48       Float64 *)
  49    (* The proposed fp.isFinite would fix all this. *)
  50    (* syntax predicate is_finite "(not (or (fp.isInfinite %1) (fp.isNaN %1)))" *)
  51    syntax predicate is_not_nan "(not (fp.isNaN %1))"
  52
  53    syntax function to_real  "(fp.to_real %1)"
  54
  55    syntax predicate overflow_value "true"
  56
  57    syntax predicate sign_zero_result "true"
  58
  59    (* Part II *)
  60
  61    remove allprops
  62 end
  63
  64 theory ieee_float.Float32
  65   (* Part I *)
  66   syntax type t "Float32"
  67   meta "literal:keep" type t
  68   syntax literal t "(fp #b%s1b #b%e8b #b%m23b)"
  69
  70   syntax function zeroF     "((_ to_fp 8 24) #x00000000)"
  71
  72   prelude "(define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))"
  73   prelude "(define-fun fp.isIntegral32 ((x Float32)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))"
  74
  75
  76   syntax predicate t'isFinite "(fp.isFinite32 %1)"
  77   syntax predicate is_int "(fp.isIntegral32 %1)"
  78
  79   (* Faithful translations of the axiomatisation, mainly to remove this crud
  80      from the smtlib output of SPARK. *)
  81   syntax function round "(fp.to_real ((_ to_fp 8 24) %1 %2))"
  82
  83  syntax predicate in_range "\
  84    (and (<= (fp.to_real (fp #b1 #b11111110 #b11111111111111111111111)) %1) \
  85         (<= %1 (fp.to_real (fp #b0 #b11111110 #b11111111111111111111111))))"
  86
  87   syntax predicate no_overflow "\
  88    (and (<= (fp.to_real (fp #b1 #b11111110 #b11111111111111111111111)) \
  89             (fp.to_real ((_ to_fp 8 24) %1 %2))) \
  90         (<= (fp.to_real ((_ to_fp 8 24) %1 %2)) \
  91             (fp.to_real (fp #b0 #b11111110 #b11111111111111111111111))))"
  92
  93   remove allprops
  94 end
  95
  96 theory ieee_float.Float64
  97   (* Part I *)
  98   syntax type t "Float64"
  99   meta "literal:keep" type t
 100   syntax literal t "(fp #b%s1b #b%e11b #b%m52b)"
 101
 102   syntax function zeroF     "((_ to_fp 11 53) #x0000000000000000)"
 103
 104   prelude "(define-fun fp.isFinite64 ((x Float64)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))"
 105   prelude "(define-fun fp.isIntegral64 ((x Float64)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))"
 106
 107   syntax predicate t'isFinite "(fp.isFinite64 %1)"
 108   syntax predicate is_int "(fp.isIntegral64 %1)"
 109
 110   (* Faithful translations of the axiomatisation, mainly to remove this crud
 111      from the smtlib output of SPARK. *)
 112   syntax function round "(fp.to_real ((_ to_fp 11 53) %1 %2))"
 113
 114   syntax predicate in_range "\
 115    (and \
 116     (<= \
 117      (fp.to_real (fp #b1 #b11111111110 #b1111111111111111111111111111111111111111111111111111)) \
 118      %1) \
 119     (<= %1 \
 120      (fp.to_real (fp #b0 #b11111111110 #b1111111111111111111111111111111111111111111111111111))))"
 121
 122   syntax predicate no_overflow "\
 123    (and \
 124     (<= \
 125      (fp.to_real (fp #b1 #b11111111110 #b1111111111111111111111111111111111111111111111111111)) \
 126      (fp.to_real ((_ to_fp 11 53) %1 %2))) \
 127     (<= \
 128      (fp.to_real ((_ to_fp 11 53) %1 %2)) \
 129      (fp.to_real (fp #b0 #b11111111110 #b1111111111111111111111111111111111111111111111111111))))"
 130
 131   remove allprops
 132 end
 133
 134 theory ieee_float.FloatConverter
 135   (* Part I *)
 136    syntax function to_float32 "((_ to_fp 8 24) %1 %2)"
 137    syntax function to_float64 "((_ to_fp 11 53) %1 %2)"
 138
 139    remove allprops
 140 end
 141
 142 theory ieee_float.Float_BV_Converter
 143   (* Part I *)
 144    syntax function to_sbv8  "((_ fp.to_sbv 8) %1 %2)"
 145    syntax function to_sbv16 "((_ fp.to_sbv 16) %1 %2)"
 146    syntax function to_sbv32 "((_ fp.to_sbv 32) %1 %2)"
 147    syntax function to_sbv64 "((_ fp.to_sbv 64) %1 %2)"
 148
 149    syntax function to_ubv8  "((_ fp.to_ubv 8) %1 %2)"
 150    syntax function to_ubv16 "((_ fp.to_ubv 16) %1 %2)"
 151    syntax function to_ubv32 "((_ fp.to_ubv 32) %1 %2)"
 152    syntax function to_ubv64 "((_ fp.to_ubv 64) %1 %2)"
 153
 154    remove allprops
 155 end
 156
 157 theory ieee_float.Float32_BV_Converter
 158   (* Part I *)
 159   syntax function of_sbv8  "((_ to_fp 8 24) %1 %2)"
 160   syntax function of_sbv16 "((_ to_fp 8 24) %1 %2)"
 161   syntax function of_sbv32 "((_ to_fp 8 24) %1 %2)"
 162   syntax function of_sbv64 "((_ to_fp 8 24) %1 %2)"
 163
 164   syntax function of_ubv8  "((_ to_fp_unsigned 8 24) %1 %2)"
 165   syntax function of_ubv16 "((_ to_fp_unsigned 8 24) %1 %2)"
 166   syntax function of_ubv32 "((_ to_fp_unsigned 8 24) %1 %2)"
 167   syntax function of_ubv64 "((_ to_fp_unsigned 8 24) %1 %2)"
 168
 169   remove allprops
 170 end
 171
 172 theory ieee_float.Float64_BV_Converter
 173   (* Part I *)
 174   syntax function of_sbv8  "((_ to_fp 11 53) %1 %2)"
 175   syntax function of_sbv16 "((_ to_fp 11 53) %1 %2)"
 176   syntax function of_sbv32 "((_ to_fp 11 53) %1 %2)"
 177   syntax function of_sbv64 "((_ to_fp 11 53) %1 %2)"
 178
 179   syntax function of_ubv8  "((_ to_fp_unsigned 11 53) %1 %2)"
 180   syntax function of_ubv16 "((_ to_fp_unsigned 11 53) %1 %2)"
 181   syntax function of_ubv32 "((_ to_fp_unsigned 11 53) %1 %2)"
 182   syntax function of_ubv64 "((_ to_fp_unsigned 11 53) %1 %2)"
 183
 184   remove allprops
 185 end