drivers/zenon_modulo.drv

   1 (* Why driver for first-order tptp provers *)
   2
   3 printer "tptp-tff1"
   4 filename "%f-%t-%g.p"
   5
   6 valid   "PROOF-FOUND"
   7 timeout "Zenon error: could not find a proof within the time limit"
   8 outofmemory "Zenon error: could not find a proof within the memory size limit"
   9 unknown "NO-PROOF" "no proof found"
  10 time "why3cpulimit time : %s s"
  11
  12 (* to be improved *)
  13
  14 (* Performed introductions depending on whether counterexamples are
  15    requested, as said by the meta "get_counterexmp". When this meta
  16    set, this transformation introduces the model variables that are
  17    still embedded in the goal. When it is not set, it removes all
  18    these unused-ce-related variables, even in the context.  *)
  19 transformation "counterexamples_dependent_intros"
  20
  21 transformation "inline_trivial"
  22
  23 transformation "eliminate_builtin"
  24 transformation "eliminate_definition"
  25 transformation "eliminate_inductive"
  26 transformation "eliminate_if"
  27 transformation "eliminate_epsilon"
  28 transformation "eliminate_algebraic"
  29 transformation "eliminate_literal"
  30 transformation "eliminate_let"
  31
  32 theory BuiltIn
  33   syntax predicate (=)  "(%1 = %2)"
  34   syntax type int  "$int"
  35   syntax type real "$real"
  36   meta "eliminate_algebraic" "no_index"
  37 end
  38
  39
  40 theory int.Int
  41   syntax function zero "0"
  42   syntax function one  "1"
  43
  44   syntax function (+)  "$sum(%1,%2)"
  45   syntax function (-)  "$difference(%1,%2)"
  46   syntax function (*)  "$product(%1,%2)"
  47   syntax function (-_) "$uminus(%1)"
  48
  49   syntax predicate (<=) "$lesseq(%1,%2)"
  50   syntax predicate (<)  "$less(%1,%2)"
  51   syntax predicate (>=) "$greatereq(%1,%2)"
  52   syntax predicate (>)  "$greater(%1,%2)"
  53
  54   remove prop MulComm.Comm
  55   remove prop MulAssoc.Assoc
  56   remove prop Unit_def_l
  57   remove prop Unit_def_r
  58   remove prop Inv_def_l
  59   remove prop Inv_def_r
  60   remove prop Assoc
  61   remove prop Mul_distr_l
  62   remove prop Mul_distr_r
  63   remove prop Comm
  64   remove prop Unitary
  65   remove prop Refl
  66   remove prop Trans
  67   remove prop Antisymm
  68   remove prop Total
  69   remove prop NonTrivialRing
  70   remove prop CompatOrderAdd
  71   remove prop ZeroLessOne
  72 end
  73
  74 theory real.Real
  75   syntax function zero "0.0"
  76   syntax function one  "1.0"
  77
  78   syntax function (+)  "$sum(%1,%2)"
  79   syntax function (-)  "$difference(%1,%2)"
  80   syntax function (*)  "$product(%1,%2)"
  81   syntax function (-_) "$uminus(%1)"
  82
  83   syntax function (/)  "$quotient(%1,%2)"
  84   syntax function inv  "$quotient(1.0,%1)"
  85
  86   syntax predicate (<=) "$lesseq(%1,%2)"
  87   syntax predicate (<)  "$less(%1,%2)"
  88   syntax predicate (>=) "$greatereq(%1,%2)"
  89   syntax predicate (>)  "$greater(%1,%2)"
  90
  91   remove prop MulComm.Comm
  92   remove prop MulAssoc.Assoc
  93   remove prop Unit_def_l
  94   remove prop Unit_def_r
  95   remove prop Inv_def_l
  96   remove prop Inv_def_r
  97   remove prop Assoc
  98   remove prop Mul_distr_l
  99   remove prop Mul_distr_r
 100   remove prop Comm
 101   remove prop Unitary
 102   remove prop Inverse
 103   remove prop Refl
 104   remove prop Trans
 105   remove prop Antisymm
 106   remove prop Total
 107   remove prop NonTrivialRing
 108   remove prop CompatOrderAdd
 109   remove prop ZeroLessOne
 110 end
 111
 112 theory int.EuclideanDivision
 113   syntax function div "$quotient_e(%1,%2)"
 114   syntax function mod "$remainder_e(%1,%2)"
 115
 116   remove prop Div_mod
 117   remove prop Div_bound
 118   remove prop Mod_bound
 119   remove prop Mod_1
 120   remove prop Div_1
 121   remove prop Div_inf
 122   remove prop Div_inf_neg
 123   remove prop Mod_0
 124   remove prop Div_1_left
 125   remove prop Div_minus1_left
 126   remove prop Mod_1_left
 127   remove prop Mod_minus1_left
 128 end
 129
 130 theory tptp.Univ
 131   syntax type iType "$i"
 132 end
 133
 134 theory tptp.IntTrunc
 135   syntax function floor    "$floor(%1)"
 136   syntax function ceiling  "$ceiling(%1)"
 137   syntax function truncate "$truncate(%1)"
 138   syntax function round    "$round(%1)"
 139
 140   syntax function to_int   "$to_int(%1)"
 141
 142   syntax predicate is_int  "$is_int(%1)"
 143   syntax predicate is_rat  "$is_rat(%1)"
 144 end
 145
 146 theory tptp.IntDivT
 147   syntax function div_t "$quotient_t(%1,%2)"
 148   syntax function mod_t "$remainder_t(%1,%2)"
 149 end
 150
 151 theory tptp.IntDivF
 152   syntax function div_f "$quotient_f(%1,%2)"
 153   syntax function mod_f "$remainder_f(%1,%2)"
 154 end
 155
 156 theory tptp.Rat
 157   syntax type rat "$rat"
 158
 159   syntax function zero "0/1"
 160   syntax function one  "1/1"
 161
 162   syntax function (+)  "$sum(%1,%2)"
 163   syntax function (-)  "$difference(%1,%2)"
 164   syntax function (*)  "$product(%1,%2)"
 165   syntax function (-_) "$uminus(%1)"
 166
 167   syntax function (/)  "$quotient(%1,%2)"
 168   syntax function inv  "$quotient(1/1,%1)"
 169
 170   syntax predicate (<=) "$lesseq(%1,%2)"
 171   syntax predicate (<)  "$less(%1,%2)"
 172   syntax predicate (>=) "$greatereq(%1,%2)"
 173   syntax predicate (>)  "$greater(%1,%2)"
 174
 175   syntax function to_rat   "$to_rat(%1)"
 176
 177   syntax predicate is_int  "$is_int(%1)"
 178   syntax predicate is_rat  "$is_rat(%1)"
 179
 180   remove prop MulComm.Comm
 181   remove prop MulAssoc.Assoc
 182   remove prop Unit_def_l
 183   remove prop Unit_def_r
 184   remove prop Inv_def_l
 185   remove prop Inv_def_r
 186   remove prop Assoc
 187   remove prop Mul_distr_l
 188   remove prop Mul_distr_r
 189   remove prop Comm
 190   remove prop Unitary
 191   remove prop Refl
 192   remove prop Trans
 193   remove prop Antisymm
 194   remove prop Total
 195   remove prop NonTrivialRing
 196   remove prop CompatOrderAdd
 197   remove prop ZeroLessOne
 198 end
 199
 200 theory tptp.RatTrunc
 201   syntax function floor    "$floor(%1)"
 202   syntax function ceiling  "$ceiling(%1)"
 203   syntax function truncate "$truncate(%1)"
 204   syntax function round    "$round(%1)"
 205
 206   syntax function to_int   "$to_int(%1)"
 207 end
 208
 209 theory tptp.RatDivE
 210   syntax function div "$quotient_e(%1,%2)"
 211   syntax function mod "$remainder_e(%1,%2)"
 212 end
 213
 214 theory tptp.RatDivT
 215   syntax function div_t "$quotient_t(%1,%2)"
 216   syntax function mod_t "$remainder_t(%1,%2)"
 217 end
 218
 219 theory tptp.RatDivF
 220   syntax function div_f "$quotient_f(%1,%2)"
 221   syntax function mod_f "$remainder_f(%1,%2)"
 222 end
 223
 224 theory tptp.Real
 225   syntax function to_real "$to_real(%1)"
 226 end
 227
 228 theory real.FromInt
 229   syntax function from_int "$to_real(%1)"
 230
 231   remove prop Zero
 232   remove prop One
 233   remove prop Add
 234   remove prop Sub
 235   remove prop Mul
 236   remove prop Neg
 237 end
 238
 239 theory real.Truncate
 240   syntax function floor    "$to_int(%1)"
 241   syntax function ceil     "$to_int($ceiling(%1))"
 242   syntax function truncate "$to_int($truncate(%1))"
 243
 244   remove prop Truncate_int
 245   remove prop Truncate_down_pos
 246   remove prop Truncate_up_neg
 247   remove prop Real_of_truncate
 248   remove prop Truncate_monotonic
 249   remove prop Truncate_monotonic_int1
 250   remove prop Truncate_monotonic_int2
 251   remove prop Floor_int
 252   remove prop Ceil_int
 253   remove prop Floor_down
 254   remove prop Ceil_up
 255   remove prop Floor_monotonic
 256   remove prop Ceil_monotonic
 257 end
 258
 259 theory tptp.RealTrunc
 260   syntax function floor    "$floor(%1)"
 261   syntax function ceiling  "$ceiling(%1)"
 262   syntax function truncate "$truncate(%1)"
 263   syntax function round    "$round(%1)"
 264
 265   syntax function to_int   "$to_int(%1)"
 266
 267   syntax predicate is_int  "$is_int(%1)"
 268   syntax predicate is_rat  "$is_rat(%1)"
 269 end
 270
 271 theory tptp.RealDivE
 272   syntax function div "$quotient_e(%1,%2)"
 273   syntax function mod "$remainder_e(%1,%2)"
 274 end
 275
 276 theory tptp.RealDivT
 277   syntax function div_t "$quotient_t(%1,%2)"
 278   syntax function mod_t "$remainder_t(%1,%2)"
 279 end
 280
 281 theory tptp.RealDivF
 282   syntax function div_f "$quotient_f(%1,%2)"
 283   syntax function mod_f "$remainder_f(%1,%2)"
 284 end
 285
 286 theory tptp.IntToRat
 287   syntax function to_rat   "$to_rat(%1)"
 288 end
 289
 290 theory tptp.IntToReal
 291   syntax function to_real "$to_real(%1)"
 292 end
 293
 294 theory tptp.RealToRat
 295   syntax function to_rat   "$to_rat(%1)"
 296 end
 297
 298 theory tptp.RatToReal
 299   syntax function to_real "$to_real(%1)"
 300 end