drivers/tptp-tff1.drv

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