drivers/beagle.drv

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