drivers/alt_ergo_fp.drv

   1 filename "%f-%t-%g.ae"
   2
   3 (* Performed introductions depending on whether counterexamples are
   4    requested, as said by the meta "get_counterexmp". When this meta
   5    set, this transformation introduces the model variables that are
   6    still embedded in the goal. When it is not set, it removes all
   7    these unused-ce-related variables, even in the context.  *)
   8 transformation "counterexamples_dependent_intros"
   9
  10 transformation "inline_trivial"
  11
  12 transformation "eliminate_builtin"
  13 transformation "eliminate_recursion"
  14 transformation "eliminate_inductive"
  15 transformation "eliminate_epsilon"
  16 transformation "eliminate_algebraic"
  17 transformation "eliminate_literal"
  18
  19 transformation "split_premise_right"
  20 transformation "simplify_formula"
  21
  22 import "alt_ergo_common.drv"
  23 import "no-bv.gen"
  24
  25 theory int.Abs
  26   syntax function abs "abs_int(%1)"
  27   remove prop Abs_le
  28   remove prop Abs_pos
  29 end
  30
  31 theory real.Abs
  32   syntax function abs "abs_real(%1)"
  33 end
  34
  35 theory real.FromInt
  36   syntax function from_int "real_of_int(%1)"
  37   remove prop Zero
  38   remove prop One
  39   remove prop Add
  40   remove prop Sub
  41   remove prop Mul
  42   remove prop Neg
  43 end
  44
  45 theory real.MinMax
  46   syntax function min "min_real(%1, %2)"
  47   syntax function max "max_real(%1, %2)"
  48 end
  49
  50 theory real.PowerInt
  51   syntax function power "(%1 **. %2)"
  52 end
  53
  54 theory real.PowerReal
  55   syntax function pow "(%1 **. %2)"
  56 end
  57
  58 theory real.Square
  59   syntax function sqrt "sqrt_real(%1)"
  60 end
  61
  62 theory ieee_float.GenericFloat
  63   remove prop Round_monotonic
  64   remove prop Round_idempotent
  65 end
  66
  67 theory ieee_float.RoundingMode
  68   syntax type mode "fpa_rounding_mode"
  69   syntax function RNE "NearestTiesToEven"
  70   syntax function RNA "NearestTiesToAway"
  71   syntax function RTN "Down"
  72   syntax function RTP "Up"
  73   syntax function RTZ "ToZero"
  74 end
  75
  76 theory ieee_float.Float32
  77   syntax function round "float32(%1,%2)"
  78 end
  79
  80 theory ieee_float.Float64
  81   syntax function round "float64(%1,%2)"
  82 end