tptp.drv 966 Bytes
Newer Older
1
(* Why driver for first-order tptp provers *)
2

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

6
valid   "Proof found"
7
invalid "Completion found"
8
invalid "SZS status CounterSatisfiable"
9
timeout "Ran out of time"
10
timeout "Resource limit exceeded"
11
timeout "CPU time limit exceeded"
12
unknown "No Proof Found"            "Unknown"
13
fail    "Failure.*"                   "\"\\0\""
14
time "why3cpulimit time : %s s"
15 16
(* time    "%h:%m:%s on the problem" *)
(* time    "Total time[ ]*: %s s" *)
17

18 19 20

(* to be improved *)

21
(*transformation "simplify_recursive_definition"*)
22 23 24 25 26 27 28 29 30
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_let"

31
transformation "encoding_tptp"
32 33

theory BuiltIn
34
  syntax predicate (=)  "(%1 = %2)"
35 36 37 38 39 40 41 42
end

(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)