alt_ergo_common.drv 5.21 KB
Newer Older
1
(* Why drivers for Alt-Ergo: common part *)
2

3
prelude "(* this is the prelude for Alt-Ergo, version >= 0.95.2 *)"
4 5 6 7

printer "alt-ergo"
filename "%f-%t-%g.why"

8 9 10 11 12
valid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Valid"
invalid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Invalid"
unknown "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:I don't know" ""
timeout "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Timeout"
steplimitexceeded "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Steps limit reached"
13
outofmemory "Fatal error: out of memory"
14
outofmemory "Fatal error: exception Stack_overflow"
15
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
16 17 18 19
time "Valid (%s)"
time "Valid (%s)"
steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\))" 2
steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2
20 21 22 23 24 25 26 27
time "why3cpulimit time : %s s"

(* À discuter *)
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
28
transformation "eliminate_algebraic"
29
transformation "eliminate_epsilon"
30 31 32
transformation "eliminate_if"
transformation "eliminate_let"

33
transformation "split_premise_right"
34 35 36 37 38 39 40 41
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)

theory BuiltIn
  syntax type int   "int"
  syntax type real  "real"

  syntax predicate (=)  "(%1 = %2)"
42 43 44 45

  meta "eliminate_algebraic" "keep_enums"
  meta "eliminate_algebraic" "keep_recs"

46 47 48 49 50 51 52 53 54 55 56 57 58 59
end

theory int.Int

  prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"

  syntax function zero "0"
  syntax function one  "1"

  syntax function (+)  "(%1 + %2)"
  syntax function (-)  "(%1 - %2)"
  syntax function (*)  "(%1 * %2)"
  syntax function (-_) "(-%1)"

60 61 62 63 64
  meta "invalid trigger" predicate (<=)
  meta "invalid trigger" predicate (<)
  meta "invalid trigger" predicate (>=)
  meta "invalid trigger" predicate (>)

65 66 67 68 69 70
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"

  remove prop CommutativeGroup.Comm.Comm
71 72 73 74 75
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
76
  remove prop Assoc.Assoc
77 78
  remove prop Mul_distr_l
  remove prop Mul_distr_r
79 80 81 82 83 84 85 86
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
87
  remove prop ZeroLessOne
88 89 90

end

91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
theory int.EuclideanDivision

  syntax function div "(%1 / %2)"
  syntax function mod "(%1 % %2)"

end

theory int.ComputerDivision

  prelude "logic comp_div: int, int -> int"
  prelude "axiom comp_div_def: forall x, y:int. x >= 0 and y > 0 -> comp_div(x,y) = x / y"

  prelude "logic comp_mod: int, int -> int"
  prelude "axiom comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> comp_mod(x,y) = x % y"

  syntax function div "comp_div(%1,%2)"
  syntax function mod "comp_mod(%1,%2)"

end

111 112 113 114 115 116 117 118 119 120 121 122 123 124 125

theory real.Real

  prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"

  syntax function zero "0.0"
  syntax function one  "1.0"

  syntax function (+)  "(%1 + %2)"
  syntax function (-)  "(%1 - %2)"
  syntax function (*)  "(%1 * %2)"
  syntax function (/)  "(%1 / %2)"
  syntax function (-_) "(-%1)"
  syntax function inv  "(1.0 / %1)"

126 127 128 129 130
  meta "invalid trigger" predicate (<=)
  meta "invalid trigger" predicate (<)
  meta "invalid trigger" predicate (>=)
  meta "invalid trigger" predicate (>)

131 132 133 134 135 136
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"

  remove prop CommutativeGroup.Comm.Comm
137 138 139 140 141
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
142
  remove prop Assoc.Assoc
143 144
  remove prop Mul_distr_l
  remove prop Mul_distr_r
145 146 147 148 149 150 151 152 153
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
  remove prop Inverse
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
154
  remove prop ZeroLessOne
155 156 157 158 159 160 161 162 163 164 165

end

theory real.RealInfix

  syntax function (+.)  "(%1 + %2)"
  syntax function (-.)  "(%1 - %2)"
  syntax function ( *.) "(%1 * %2)"
  syntax function (/.)  "(%1 / %2)"
  syntax function (-._) "(-%1)"

166 167 168 169 170
  meta "invalid trigger" predicate (<=.)
  meta "invalid trigger" predicate (<.)
  meta "invalid trigger" predicate (>=.)
  meta "invalid trigger" predicate (>.)

171 172 173 174 175 176 177
  syntax predicate (<=.) "(%1 <= %2)"
  syntax predicate (<.)  "(%1 <  %2)"
  syntax predicate (>=.) "(%1 >= %2)"
  syntax predicate (>.)  "(%1 >  %2)"

end

178
theory Bool
179 180 181 182 183 184 185 186 187 188 189
  syntax type     bool  "bool"
  syntax function True  "true"
  syntax function False "false"
end

theory Tuple0
  syntax type     tuple0 "unit"
  syntax function Tuple0 "void"
end

theory algebra.AC
190 191 192
  meta AC function op
  remove prop Comm.Comm
  remove prop Assoc
193
end
194 195 196 197 198 199 200 201 202 203

theory map.Map
  syntax type  map "(%1,%2) farray"

  syntax function get "(%1[%2])"
  syntax function set "(%1[%2 <- %3])"

  remove prop Select_eq
  remove prop Select_neq
end