mathematica.drv 5.22 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12

(* Why driver for Mathematica *)

prelude "(* this is a prelude for Mathematica *)"

printer "mathematica"
filename "%f-%t-%g.m"

valid "\\bTrue\\b"
unknown "\\bFalse\\b" "\\bFalse\\b"
time "why3cpulimit time : %s s"

13 14
transformation "inline_trivial"
transformation "inline_all"
15 16 17 18 19 20 21

transformation "eliminate_builtin"
(*transformation "eliminate_definition"*)
(*transformation "eliminate_recursion"*)
(*transformation "eliminate_inductive"*)
(*transformation "eliminate_algebraic"*)
(*transformation "eliminate_algebraic_math"*)
22
transformation "eliminate_epsilon"
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
(*transformation "eliminate_if"*)
transformation "eliminate_let"

(*transformation "split_premise"*)
transformation "simplify_formula"
(*transformation "simplify_unknown_lsymbols"*)
transformation "simplify_trivial_quantification"
(*transformation "introduce_premises"*)
(*transformation "instantiate_predicate"*)
(*transformation "abstract_unknown_lsymbols"*)

theory BuiltIn
  syntax type int   "Integers"
  syntax type real  "Reals"
  syntax predicate (=)  "(%1 == %2)"

39
  meta "encoding:kept" type int
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
end

(* int *)

theory int.Int

  prelude "(* this is a prelude for Mathematica 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)"

  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 < %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 > %2)"

61 62 63
  meta "inline:no" predicate (<=)
  meta "inline:no" predicate (>=)
  meta "inline:no" predicate (>)
64

Andrei Paskevich's avatar
Andrei Paskevich committed
65 66 67 68 69 70 71
  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
72 73
  remove prop Mul_distr_l
  remove prop Mul_distr_r
Andrei Paskevich's avatar
Andrei Paskevich committed
74
  remove prop Comm
75 76 77 78 79 80 81
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
82
  remove prop CompatOrderMult
83 84
  remove prop ZeroLessOne

85
  meta "encoding:kept" type int
86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
end

theory int.Abs

  syntax function abs  "Abs[%1]"

end

theory int.EuclideanDivision

  syntax function div "Quotient[%1, %2]"
  syntax function mod "Mod[%1, %2]"

  remove prop Mod_bound
  remove prop Div_bound
  remove prop Div_mod
  remove prop Mod_1
  remove prop Div_1

105
  meta "encoding:kept" type int
106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
end

(* real *)

theory real.Real

  prelude "(* this is a prelude for Mathematica real arithmetic *)"

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

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

  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 < %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 > %2)"

129 130 131
  meta "inline:no" predicate (<=)
  meta "inline:no" predicate (>=)
  meta "inline:no" predicate (>)
132

Andrei Paskevich's avatar
Andrei Paskevich committed
133 134 135 136 137 138 139
  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
140 141
  remove prop Mul_distr_l
  remove prop Mul_distr_r
Andrei Paskevich's avatar
Andrei Paskevich committed
142
  remove prop Comm
143 144 145 146 147 148 149 150 151 152
  remove prop Unitary
  remove prop Inverse
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop ZeroLessOne

153 154 155 156 157 158 159 160
  remove prop add_div
  remove prop sub_div
  remove prop neg_div
  remove prop assoc_mul_div
  remove prop assoc_div_mul
  remove prop assoc_div_div
  remove prop CompatOrderMult

161
  (*meta "encoding:kept" type real*)
162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246
end

theory real.Abs

  syntax function abs "Abs[%1]"

end

theory real.MinMax

  syntax function min "Min[%1, %2]"
  syntax function max "Max[%1, %2]"

end

theory real.Square

  syntax function sqr  "Power[%1,2]"
  syntax function sqrt "Sqrt[%1]"

end

theory real.ExpLog

  syntax function exp "Exp[%1]"
  syntax function e   "E"
  syntax function log "Log[%1]"
  syntax function log2 "Log[2, %1]"
  syntax function log10 "Log[10, %1]"

  remove prop Exp_zero
  remove prop Exp_sum
  remove prop Log_one
  remove prop Log_mul
  remove prop Log_exp
  remove prop Exp_log

end

theory real.PowerInt

  syntax function power "Power[%1, %2]"

end

theory real.PowerReal

  syntax function pow "Power[%1, %2]"

end

theory real.Trigonometry

  syntax function cos "Cos[%1]"
  syntax function sin "Sin[%1]"
  syntax function tan "Tan[%1]"
  syntax function atan "ArcTan[%1]"

  syntax function pi "Pi"

end

theory real.Hyperbolic

  syntax function sinh "Sinh[%1]"
  syntax function cosh "Cosh[%1]"
  syntax function tanh "Tanh[%1]"
  syntax function asinh "ArcSinh[%1]"
  syntax function acosh "ArcCosh[%1]"
  syntax function atanh "ArcTanh[%1]"

end

theory real.FromInt

  remove prop Zero
  remove prop One
  remove prop Add
  remove prop Sub
  remove prop Mul
  remove prop Neg

end


247
theory Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
248 249 250 251 252
  syntax type     bool  "Bool"
  syntax function True  "True"
  syntax function False "False"

  meta "encoding:kept" type bool
253 254 255
end

theory bool.Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
256 257 258 259 260
  syntax function andb  "(%1 && %2)"
  syntax function orb   "(%1 || %2)"
  syntax function xorb  "Xor[%1, %2]"
  syntax function notb  "(! %1)"
  syntax function implb "Implies[%1, %2]"
261
end