Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

gappa.drv 3.13 KB
Newer Older
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
1 2 3 4 5

(* Why driver for Gappa *)

prelude "# this is a prelude for Gappa"

MARCHE Claude's avatar
MARCHE Claude committed
6
printer "gappa"
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
7 8 9
filename "%f-%t-%g.gappa"

valid 0
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
10
unknown "no contradiction was found\\|some enclosures were not satisfied" "Unknown"
11 12
time "why3cpulimit time : %s s"
fail "Error: \\(.*\\)" "\\1"
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
13

MARCHE Claude's avatar
MARCHE Claude committed
14
transformation "simplify_recursive_definition"
15
transformation "inline_trivial"
MARCHE Claude's avatar
MARCHE Claude committed
16
transformation "eliminate_builtin"
MARCHE Claude's avatar
MARCHE Claude committed
17
transformation "inline_all"
18
transformation "eliminate_definition"
MARCHE Claude's avatar
MARCHE Claude committed
19
transformation "eliminate_inductive"
20
transformation "eliminate_algebraic_smt"
MARCHE Claude's avatar
MARCHE Claude committed
21 22 23
transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
24
transformation "simplify_trivial_quantification"
25
transformation "introduce_premises"
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
26 27

theory BuiltIn
28 29 30
  syntax type int   "int"
  syntax type real  "real"
  syntax logic (=)  "(%1 = %2)"
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
31 32 33 34 35 36 37 38 39
end

theory int.Int

  prelude "# this is a prelude for Gappa integer arithmetic"

  syntax logic zero "0"
  syntax logic one  "1"

40 41 42 43
  syntax logic (+)  "(%1 + %2)"
  syntax logic (-)  "(%1 - %2)"
  syntax logic (*)  "(%1 * %2)"
  syntax logic (-_) "(-%1)"
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
44

45 46 47 48
  meta "inline : no" logic (<=)
  meta "inline : no" logic (>=)
  meta "inline : no" logic (>)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm

end

MARCHE Claude's avatar
MARCHE Claude committed
64 65 66 67 68 69
theory int.Abs

  syntax logic abs  "| %1 |"

end

70 71 72 73 74 75 76 77 78 79 80
theory int.EuclideanDivision

  syntax logic div "int<dn>(%1 / %2)"

end

theory int.ComputerDivision

  syntax logic div "int<zr>(%1 / %2)"

end
MARCHE Claude's avatar
MARCHE Claude committed
81

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
82 83 84 85 86 87 88
theory real.Real

  prelude "# this is a prelude for Gappa real arithmetic"

  syntax logic zero "0.0"
  syntax logic one  "1.0"

89 90 91 92 93 94
  syntax logic (+)  "(%1 + %2)"
  syntax logic (-)  "(%1 - %2)"
  syntax logic (*)  "(%1 * %2)"
  syntax logic (/)  "(%1 / %2)"
  syntax logic (-_) "(-%1)"
  syntax logic inv  "(1.0 / %1)"
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
95

96 97 98
  meta "inline : no" logic (<=)
  meta "inline : no" logic (>=)
  meta "inline : no" logic (>)
99
  
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
  remove prop Inverse

end

116 117 118 119 120 121
theory real.Abs

  syntax logic abs  "| %1 |"

end

122 123 124 125 126 127
theory real.Square

  syntax logic sqrt  "sqrt(%1)"

end

128 129 130
theory floating_point.Single

  prelude "@rnd_ieee32_ne=float<ieee_32,ne>;"
131 132 133 134
  prelude "@rnd_ieee32_zr=float<ieee_32,zr>;"
  prelude "@rnd_ieee32_up=float<ieee_32,up>;"
  prelude "@rnd_ieee32_dn=float<ieee_32,dn>;"
  prelude "@rnd_ieee32_na=float<ieee_32,na>;"
135 136 137

end

138 139 140
theory floating_point.Double

  prelude "@rnd_ieee64_ne=float<ieee_64,ne>;"
141 142 143 144
  prelude "@rnd_ieee64_zr=float<ieee_64,zr>;"
  prelude "@rnd_ieee64_up=float<ieee_64,up>;"
  prelude "@rnd_ieee64_dn=float<ieee_64,dn>;"
  prelude "@rnd_ieee64_na=float<ieee_64,na>;"
145 146 147

end

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
148
(*
MARCHE Claude's avatar
MARCHE Claude committed
149
Local Variables:
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
150 151
mode: why
compile-command: "make -C .. bench"
MARCHE Claude's avatar
MARCHE Claude committed
152
End:
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
153
*)