tptp.gen 876 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
(* Why common driver for first-order tptp provers *)
2

3
printer "tptp-fof"
4 5
filename "%f-%t-%g.p"

MARCHE Claude's avatar
MARCHE Claude committed
6 7 8 9 10 11 12
valid   "^% SZS status Theorem"
valid   "^% SZS status Unsatisfiable"
unknown "^% SZS status CounterSatisfiable" ""
unknown "^% SZS status Satisfiable" ""
timeout "^% SZS status Timeout"
unknown "^% SZS status GaveUp" ""
fail    "^% SZS status Error" ""
13

MARCHE Claude's avatar
MARCHE Claude committed
14
time "why3cpulimit time : %s s"
15 16 17 18 19 20 21 22 23

(* to be improved *)

transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
24
transformation "eliminate_epsilon"
25 26 27
transformation "eliminate_if"
transformation "eliminate_let"

28 29
transformation "simplify_formula"

30
transformation "discriminate"
31
transformation "encoding_tptp"
32 33

theory BuiltIn
34
  syntax predicate (=)  "(%1 = %2)"
35
  meta "eliminate_algebraic" "no_index"
36 37
end