alt_ergo_fp.drv 1.16 KB
Newer Older
1 2 3
import "alt_ergo_common.drv"
import "no-bv.gen"

4 5 6 7 8 9
theory int.Abs
  syntax function abs "abs_int(%1)"
  remove prop Abs_le
  remove prop Abs_pos
end

10 11 12 13
theory real.Abs
  syntax function abs "abs_real(%1)"
end

14 15 16 17 18 19 20 21 22 23
theory real.FromInt
  syntax function from_int "real_of_int(%1)"
  remove prop Zero
  remove prop One
  remove prop Add
  remove prop Sub
  remove prop Mul
  remove prop Neg
end

24
theory real.MinMax
25 26 27 28 29 30 31 32 33 34
  syntax function min "min_real(%1, %2)"
  syntax function max "max_real(%1, %2)"
end

theory real.PowerInt
  syntax function power "pow_real_int(%1, %2)"
end

theory real.PowerReal
  syntax function pow "pow_real_real(%1, %2)"
35 36 37 38 39 40
end

theory real.Square
  syntax function sqrt "sqrt_real(%1)"
end

41 42 43 44 45
theory ieee_float.GenericFloat
  remove prop Round_monotonic
  remove prop Round_idempotent
end

46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
theory ieee_float.RoundingMode
  syntax type mode "fpa_rounding_mode"
  syntax function RNE "NearestTiesToEven"
  syntax function RNA "NearestTiesToAway"
  syntax function RTN "Down"
  syntax function RTP "Up"
  syntax function RTZ "ToZero"
end

theory ieee_float.Float32
  syntax function round "float32(%1,%2)"
end

theory ieee_float.Float64
  syntax function round "float64(%1,%2)"
end