alt_ergo_common.drv 4.86 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
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"
12
timeout "^Timeout$"
13
steplimitexceeded "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Steps limit reached"
14
outofmemory "Fatal error: out of memory"
15
outofmemory "Fatal error: exception Stack_overflow"
16
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
17 18 19 20
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
21 22 23 24 25 26 27
time "why3cpulimit time : %s s"

transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
28
transformation "eliminate_algebraic"
Clément Fumex's avatar
Clément Fumex committed
29
transformation "eliminate_literal"
30
transformation "eliminate_if"
Quentin Garchery's avatar
Quentin Garchery committed
31
transformation "eliminate_epsilon"
32 33
transformation "eliminate_let"

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

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

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

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

47 48 49 50 51 52 53 54 55 56 57 58 59 60
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)"

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

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

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

end

92 93 94 95 96 97 98 99 100
theory int.EuclideanDivision

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

end

theory int.ComputerDivision

101
  use for_drivers.ComputerOfEuclideanDivision
102 103 104

end

105 106 107 108 109 110 111
theory for_drivers.ComputerOfEuclideanDivision

  remove prop cdiv_cases_0
  remove prop cdiv_cases_1

end

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

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)"

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

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

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

end

theory real.RealInfix

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

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

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

end

179
theory Bool
180 181 182 183 184 185 186 187 188 189 190
  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
191
  meta AC function op
192
  remove prop Comm
193
  remove prop Assoc
194
end
195

Andrei Paskevich's avatar
Andrei Paskevich committed
196 197 198 199
theory HighOrd
  syntax type     (->) "(%1,%2) farray"
  syntax function (@)  "(%1[%2])"
end
200

Andrei Paskevich's avatar
Andrei Paskevich committed
201
theory map.Map
202 203
  syntax function get  "(%1[%2])"
  syntax function set  "(%1[%2 <- %3])"
204
end