drivers/tptp.gen

   1 (* Why common driver for first-order tptp provers *)
   2
   3 printer "tptp-fof"
   4 filename "%f-%t-%g.p"
   5
   6 valid   "^% SZS status Theorem"
   7 valid   "^% SZS status Unsatisfiable"
   8 unknown "^% SZS status CounterSatisfiable" ""
   9 unknown "^% SZS status Satisfiable" ""
  10 timeout "^% SZS status Timeout"
  11 unknown "^% SZS status GaveUp" ""
  12 fail    "^% SZS status Error" ""
  13
  14 time "why3cpulimit time : %s s"
  15
  16 (* Performed introductions depending on whether counterexamples are
  17    requested, as said by the meta "get_counterexmp". When this meta
  18    set, this transformation introduces the model variables that are
  19    still embedded in the goal. When it is not set, it removes all
  20    these unused-ce-related variables, even in the context.  *)
  21 transformation "counterexamples_dependent_intros"
  22
  23 transformation "inline_trivial"
  24 transformation "eliminate_builtin"
  25 (* transformation "remove_unused_keep_constants" looses too many proofs *)
  26 transformation "eliminate_definition"
  27 transformation "eliminate_inductive"
  28 transformation "eliminate_if"
  29 transformation "eliminate_epsilon"
  30 transformation "eliminate_algebraic"
  31 transformation "eliminate_literal"
  32 transformation "eliminate_negative_constants"
  33 transformation "eliminate_let"
  34
  35 transformation "simplify_formula"
  36
  37 transformation "discriminate"
  38 transformation "encoding_tptp"
  39
  40 theory BuiltIn
  41   syntax predicate (=)  "(%1 = %2)"
  42   meta "eliminate_algebraic" "no_index"
  43 end
  44
  45 theory Ignore
  46   syntax predicate ignore'term  "true"
  47 end