drivers/tptp-tff0.drv

   1 (* Why driver for first-order tptp provers supporting TFF0 *)
   2
   3 printer "tptp-tff0"
   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 transformation "discriminate"
  42 transformation "encoding_smt"
  43
  44 import "discrimination.gen"
  45
  46 theory BuiltIn
  47   syntax predicate (=)  "(%1 = %2)"
  48   syntax type int  "$int"
  49   syntax type real "$real"
  50
  51   meta "encoding:kept" type int
  52   meta "encoding:kept" type real
  53   meta "eliminate_algebraic" "no_index"
  54 end
  55
  56 theory int.Int
  57   syntax function zero "0"
  58   syntax function one  "1"
  59
  60   syntax function (+)  "$sum(%1,%2)"
  61   syntax function (-)  "$difference(%1,%2)"
  62   syntax function (*)  "$product(%1,%2)"
  63   syntax function (-_) "$uminus(%1)"
  64
  65   syntax predicate (<=) "$lesseq(%1,%2)"
  66   syntax predicate (<)  "$less(%1,%2)"
  67   syntax predicate (>=) "$greatereq(%1,%2)"
  68   syntax predicate (>)  "$greater(%1,%2)"
  69
  70   remove prop MulComm.Comm
  71   remove prop MulAssoc.Assoc
  72   remove prop Unit_def_l
  73   remove prop Unit_def_r
  74   remove prop Inv_def_l
  75   remove prop Inv_def_r
  76   remove prop Assoc
  77   remove prop Mul_distr_l
  78   remove prop Mul_distr_r
  79   remove prop Comm
  80   remove prop Unitary
  81   remove prop Refl
  82   remove prop Trans
  83   remove prop Antisymm
  84   remove prop Total
  85   remove prop NonTrivialRing
  86   remove prop CompatOrderAdd
  87   remove prop ZeroLessOne
  88 end
  89
  90 theory real.Real
  91   syntax function zero "0.0"
  92   syntax function one  "1.0"
  93
  94   syntax function (+)  "$sum(%1,%2)"
  95   syntax function (-)  "$difference(%1,%2)"
  96   syntax function (*)  "$product(%1,%2)"
  97   syntax function (-_) "$uminus(%1)"
  98
  99   syntax function (/)  "$quotient(%1,%2)"
 100   syntax function inv  "$quotient(1.0,%1)"
 101
 102   syntax predicate (<=) "$lesseq(%1,%2)"
 103   syntax predicate (<)  "$less(%1,%2)"
 104   syntax predicate (>=) "$greatereq(%1,%2)"
 105   syntax predicate (>)  "$greater(%1,%2)"
 106
 107   remove prop MulComm.Comm
 108   remove prop MulAssoc.Assoc
 109   remove prop Unit_def_l
 110   remove prop Unit_def_r
 111   remove prop Inv_def_l
 112   remove prop Inv_def_r
 113   remove prop Assoc
 114   remove prop Mul_distr_l
 115   remove prop Mul_distr_r
 116   remove prop Comm
 117   remove prop Unitary
 118   remove prop Inverse
 119   remove prop Refl
 120   remove prop Trans
 121   remove prop Antisymm
 122   remove prop Total
 123   remove prop NonTrivialRing
 124   remove prop CompatOrderAdd
 125   remove prop ZeroLessOne
 126 end
 127
 128 theory int.EuclideanDivision
 129   syntax function div "$quotient_e(%1,%2)"
 130   syntax function mod "$remainder_e(%1,%2)"
 131
 132   remove prop Div_mod
 133   remove prop Div_bound
 134   remove prop Mod_bound
 135   remove prop Mod_1
 136   remove prop Div_1
 137   remove prop Div_inf
 138   remove prop Div_inf_neg
 139   remove prop Mod_0
 140   remove prop Div_1_left
 141   remove prop Div_minus1_left
 142   remove prop Mod_1_left
 143   remove prop Mod_minus1_left
 144 end
 145
 146 theory tptp.Univ
 147   syntax type iType "$i"
 148
 149   meta "encoding:kept" type iType
 150 end
 151
 152 theory tptp.IntTrunc
 153   syntax function floor    "$floor(%1)"
 154   syntax function ceiling  "$ceiling(%1)"
 155   syntax function truncate "$truncate(%1)"
 156   syntax function round    "$round(%1)"
 157
 158   syntax function to_int   "$to_int(%1)"
 159
 160   syntax predicate is_int  "$is_int(%1)"
 161   syntax predicate is_rat  "$is_rat(%1)"
 162 end
 163
 164 theory tptp.IntDivT
 165   syntax function div_t "$quotient_t(%1,%2)"
 166   syntax function mod_t "$remainder_t(%1,%2)"
 167 end
 168
 169 theory tptp.IntDivF
 170   syntax function div_f "$quotient_f(%1,%2)"
 171   syntax function mod_f "$remainder_f(%1,%2)"
 172 end
 173
 174 theory tptp.Rat
 175   syntax type rat "$rat"
 176
 177   syntax function zero "0/1"
 178   syntax function one  "1/1"
 179
 180   syntax function (+)  "$sum(%1,%2)"
 181   syntax function (-)  "$difference(%1,%2)"
 182   syntax function (*)  "$product(%1,%2)"
 183   syntax function (-_) "$uminus(%1)"
 184
 185   syntax function (/)  "$quotient(%1,%2)"
 186   syntax function inv  "$quotient(1/1,%1)"
 187
 188   syntax predicate (<=) "$lesseq(%1,%2)"
 189   syntax predicate (<)  "$less(%1,%2)"
 190   syntax predicate (>=) "$greatereq(%1,%2)"
 191   syntax predicate (>)  "$greater(%1,%2)"
 192
 193   syntax function to_rat   "$to_rat(%1)"
 194
 195   syntax predicate is_int  "$is_int(%1)"
 196   syntax predicate is_rat  "$is_rat(%1)"
 197
 198   remove prop MulComm.Comm
 199   remove prop MulAssoc.Assoc
 200   remove prop Unit_def_l
 201   remove prop Unit_def_r
 202   remove prop Inv_def_l
 203   remove prop Inv_def_r
 204   remove prop Assoc
 205   remove prop Mul_distr_l
 206   remove prop Mul_distr_r
 207   remove prop Comm
 208   remove prop Unitary
 209   remove prop Refl
 210   remove prop Trans
 211   remove prop Antisymm
 212   remove prop Total
 213   remove prop NonTrivialRing
 214   remove prop CompatOrderAdd
 215   remove prop ZeroLessOne
 216
 217   meta "encoding:kept" type rat
 218 end
 219
 220 theory tptp.RatTrunc
 221   syntax function floor    "$floor(%1)"
 222   syntax function ceiling  "$ceiling(%1)"
 223   syntax function truncate "$truncate(%1)"
 224   syntax function round    "$round(%1)"
 225
 226   syntax function to_int   "$to_int(%1)"
 227 end
 228
 229 theory tptp.RatDivE
 230   syntax function div "$quotient_e(%1,%2)"
 231   syntax function mod "$remainder_e(%1,%2)"
 232 end
 233
 234 theory tptp.RatDivT
 235   syntax function div_t "$quotient_t(%1,%2)"
 236   syntax function mod_t "$remainder_t(%1,%2)"
 237 end
 238
 239 theory tptp.RatDivF
 240   syntax function div_f "$quotient_f(%1,%2)"
 241   syntax function mod_f "$remainder_f(%1,%2)"
 242 end
 243
 244 theory tptp.Real
 245   syntax function to_real "$to_real(%1)"
 246 end
 247
 248 theory real.FromInt
 249   syntax function from_int "$to_real(%1)"
 250
 251   remove prop Zero
 252   remove prop One
 253   remove prop Add
 254   remove prop Sub
 255   remove prop Mul
 256   remove prop Neg
 257 end
 258
 259 theory real.Truncate
 260   syntax function floor    "$to_int(%1)"
 261   syntax function ceil     "$to_int($ceiling(%1))"
 262   syntax function truncate "$to_int($truncate(%1))"
 263
 264   remove prop Truncate_int
 265   remove prop Truncate_down_pos
 266   remove prop Truncate_up_neg
 267   remove prop Real_of_truncate
 268   remove prop Truncate_monotonic
 269   remove prop Truncate_monotonic_int1
 270   remove prop Truncate_monotonic_int2
 271   remove prop Floor_int
 272   remove prop Ceil_int
 273   remove prop Floor_down
 274   remove prop Ceil_up
 275   remove prop Floor_monotonic
 276   remove prop Ceil_monotonic
 277 end
 278
 279 theory tptp.RealTrunc
 280   syntax function floor    "$floor(%1)"
 281   syntax function ceiling  "$ceiling(%1)"
 282   syntax function truncate "$truncate(%1)"
 283   syntax function round    "$round(%1)"
 284
 285   syntax function to_int   "$to_int(%1)"
 286
 287   syntax predicate is_int  "$is_int(%1)"
 288   syntax predicate is_rat  "$is_rat(%1)"
 289 end
 290
 291 theory tptp.RealDivE
 292   syntax function div "$quotient_e(%1,%2)"
 293   syntax function mod "$remainder_e(%1,%2)"
 294 end
 295
 296 theory tptp.RealDivT
 297   syntax function div_t "$quotient_t(%1,%2)"
 298   syntax function mod_t "$remainder_t(%1,%2)"
 299 end
 300
 301 theory tptp.RealDivF
 302   syntax function div_f "$quotient_f(%1,%2)"
 303   syntax function mod_f "$remainder_f(%1,%2)"
 304 end
 305
 306 theory tptp.IntToRat
 307   syntax function to_rat   "$to_rat(%1)"
 308 end
 309
 310 theory tptp.IntToReal
 311   syntax function to_real "$to_real(%1)"
 312 end
 313
 314 theory tptp.RealToRat
 315   syntax function to_rat   "$to_rat(%1)"
 316 end
 317
 318 theory tptp.RatToReal
 319   syntax function to_real "$to_real(%1)"
 320 end