drivers/zenon.drv

   1 (* Why driver for first-order tptp provers *)
   2
   3 printer "tptp-fof"
   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 transformation "discriminate"
  33 transformation "encoding_tptp"
  34
  35 theory BuiltIn
  36   syntax predicate (=)  "(%1 = %2)"
  37   meta "eliminate_algebraic" "no_index"
  38 end
  39
  40 import "discrimination.gen"