drivers/mathematica.drv

   1
   2 (* Why driver for Mathematica *)
   3
   4 prelude "(* this is a prelude for Mathematica *)"
   5
   6 printer "mathematica"
   7 filename "%f-%t-%g.m"
   8
   9 valid "\\bTrue\\b"
  10 unknown "\\bFalse\\b" "\\bFalse\\b"
  11 time "why3cpulimit time : %s s"
  12
  13 (* Performed introductions depending on whether counterexamples are
  14    requested, as said by the meta "get_counterexmp". When this meta
  15    set, this transformation introduces the model variables that are
  16    still embedded in the goal. When it is not set, it removes all
  17    these unused-ce-related variables, even in the context.  *)
  18 transformation "counterexamples_dependent_intros"
  19
  20 transformation "inline_trivial"
  21 transformation "inline_all"
  22
  23 transformation "eliminate_builtin"
  24 (*transformation "eliminate_definition"*)
  25 (*transformation "eliminate_recursion"*)
  26 (*transformation "eliminate_inductive"*)
  27 (*transformation "eliminate_if"*)
  28 transformation "eliminate_epsilon"
  29 (*transformation "eliminate_algebraic"*)
  30 (*transformation "eliminate_algebraic_math"*)
  31 transformation "eliminate_literal"
  32 transformation "eliminate_let"
  33
  34 (*transformation "split_premise"*)
  35 transformation "simplify_formula"
  36 (*transformation "simplify_unknown_lsymbols"*)
  37 transformation "simplify_trivial_quantification"
  38 (*transformation "introduce_premises"*)
  39 (*transformation "instantiate_predicate"*)
  40 (*transformation "abstract_unknown_lsymbols"*)
  41
  42 theory BuiltIn
  43   syntax type int   "Integers"
  44   syntax type real  "Reals"
  45   syntax predicate (=)  "(%1 == %2)"
  46
  47   meta "encoding:kept" type int
  48 end
  49
  50 (* int *)
  51
  52 theory int.Int
  53
  54   prelude "(* this is a prelude for Mathematica integer arithmetic *)"
  55
  56   syntax function zero "0"
  57   syntax function one  "1"
  58
  59   syntax function (+)  "(%1 + %2)"
  60   syntax function (-)  "(%1 - %2)"
  61   syntax function (*)  "(%1 %2)"
  62   syntax function (-_) "(-%1)"
  63
  64   syntax predicate (<=) "(%1 <= %2)"
  65   syntax predicate (<)  "(%1 < %2)"
  66   syntax predicate (>=) "(%1 >= %2)"
  67   syntax predicate (>)  "(%1 > %2)"
  68
  69   meta "inline:no" predicate (<=)
  70   meta "inline:no" predicate (>=)
  71   meta "inline:no" predicate (>)
  72
  73   remove prop MulComm.Comm
  74   remove prop MulAssoc.Assoc
  75   remove prop Unit_def_l
  76   remove prop Unit_def_r
  77   remove prop Inv_def_l
  78   remove prop Inv_def_r
  79   remove prop Assoc
  80   remove prop Mul_distr_l
  81   remove prop Mul_distr_r
  82   remove prop Comm
  83   remove prop Unitary
  84   remove prop Refl
  85   remove prop Trans
  86   remove prop Antisymm
  87   remove prop Total
  88   remove prop NonTrivialRing
  89   remove prop CompatOrderAdd
  90   remove prop CompatOrderMult
  91   remove prop ZeroLessOne
  92
  93   meta "encoding:kept" type int
  94 end
  95
  96 theory int.Abs
  97
  98   syntax function abs  "Abs[%1]"
  99
 100 end
 101
 102 theory int.EuclideanDivision
 103
 104   syntax function div "Quotient[%1, %2]"
 105   syntax function mod "Mod[%1, %2]"
 106
 107   remove prop Mod_bound
 108   remove prop Div_bound
 109   remove prop Div_mod
 110   remove prop Mod_1
 111   remove prop Div_1
 112
 113   meta "encoding:kept" type int
 114 end
 115
 116 (* real *)
 117
 118 theory real.Real
 119
 120   prelude "(* this is a prelude for Mathematica real arithmetic *)"
 121
 122   syntax function zero "0"
 123   syntax function one  "1"
 124
 125   syntax function (+)  "(%1 + %2)"
 126   syntax function (-)  "(%1 - %2)"
 127   syntax function (*)  "(%1 * %2)"
 128   syntax function (/)  "(%1 / %2)"
 129   syntax function (-_) "(-%1)"
 130   syntax function inv  "(1 / %1)"
 131
 132   syntax predicate (<=) "(%1 <= %2)"
 133   syntax predicate (<)  "(%1 < %2)"
 134   syntax predicate (>=) "(%1 >= %2)"
 135   syntax predicate (>)  "(%1 > %2)"
 136
 137   meta "inline:no" predicate (<=)
 138   meta "inline:no" predicate (>=)
 139   meta "inline:no" predicate (>)
 140
 141   remove prop MulComm.Comm
 142   remove prop MulAssoc.Assoc
 143   remove prop Unit_def_l
 144   remove prop Unit_def_r
 145   remove prop Inv_def_l
 146   remove prop Inv_def_r
 147   remove prop Assoc
 148   remove prop Mul_distr_l
 149   remove prop Mul_distr_r
 150   remove prop Comm
 151   remove prop Unitary
 152   remove prop Inverse
 153   remove prop Refl
 154   remove prop Trans
 155   remove prop Antisymm
 156   remove prop Total
 157   remove prop NonTrivialRing
 158   remove prop CompatOrderAdd
 159   remove prop ZeroLessOne
 160
 161   remove prop add_div
 162   remove prop sub_div
 163   remove prop neg_div
 164   remove prop assoc_mul_div
 165   remove prop assoc_div_mul
 166   remove prop assoc_div_div
 167   remove prop CompatOrderMult
 168
 169   (*meta "encoding:kept" type real*)
 170 end
 171
 172 theory real.Abs
 173
 174   syntax function abs "Abs[%1]"
 175
 176 end
 177
 178 theory real.MinMax
 179
 180   syntax function min "Min[%1, %2]"
 181   syntax function max "Max[%1, %2]"
 182
 183 end
 184
 185 theory real.Square
 186
 187   syntax function sqr  "Power[%1,2]"
 188   syntax function sqrt "Sqrt[%1]"
 189
 190 end
 191
 192 theory real.ExpLog
 193
 194   syntax function exp "Exp[%1]"
 195   syntax function e   "E"
 196   syntax function log "Log[%1]"
 197   syntax function log2 "Log[2, %1]"
 198   syntax function log10 "Log[10, %1]"
 199
 200   remove prop Exp_zero
 201   remove prop Exp_sum
 202   remove prop Log_one
 203   remove prop Log_mul
 204   remove prop Log_exp
 205   remove prop Exp_log
 206
 207 end
 208
 209 theory real.PowerInt
 210
 211   syntax function power "Power[%1, %2]"
 212
 213 end
 214
 215 theory real.PowerReal
 216
 217   syntax function pow "Power[%1, %2]"
 218
 219 end
 220
 221 theory real.Trigonometry
 222
 223   syntax function cos "Cos[%1]"
 224   syntax function sin "Sin[%1]"
 225   syntax function tan "Tan[%1]"
 226   syntax function atan "ArcTan[%1]"
 227
 228   syntax function pi "Pi"
 229
 230 end
 231
 232 theory real.Hyperbolic
 233
 234   syntax function sinh "Sinh[%1]"
 235   syntax function cosh "Cosh[%1]"
 236   syntax function tanh "Tanh[%1]"
 237   syntax function asinh "ArcSinh[%1]"
 238   syntax function acosh "ArcCosh[%1]"
 239   syntax function atanh "ArcTanh[%1]"
 240
 241 end
 242
 243 theory real.FromInt
 244
 245   remove prop Zero
 246   remove prop One
 247   remove prop Add
 248   remove prop Sub
 249   remove prop Mul
 250   remove prop Neg
 251
 252 end
 253
 254
 255 theory Bool
 256   syntax type     bool  "Bool"
 257   syntax function True  "True"
 258   syntax function False "False"
 259
 260   meta "encoding:kept" type bool
 261 end
 262
 263 theory bool.Bool
 264   syntax function andb  "(%1 && %2)"
 265   syntax function orb   "(%1 || %2)"
 266   syntax function xorb  "Xor[%1, %2]"
 267   syntax function notb  "(! %1)"
 268   syntax function implb "Implies[%1, %2]"
 269 end