vampire.drv 1010 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
(* Why driver for first-order tptp provers *)

printer "tptp"
filename "%f-%t-%g.p"

valid   "Refutation.*found"
(* invalid "Completion found" *)
(* invalid "SZS status CounterSatisfiable" *)
(* timeout "Ran out of time" *)
(* timeout "Resource limit exceeded" *)
(* timeout "CPU time limit exceeded" *)
(* unknown "No Proof Found"            "Unknown" *)
(* fail    "Failure.*"                   "\"\\0\"" *)
time "why3cpulimit time : %s s"
(* time    "%h:%m:%s on the problem" *)
(* time    "Total time[ ]*: %s s" *)


(* to be improved *)

21
(*transformation "simplify_recursive_definition"*)
MARCHE Claude's avatar
MARCHE Claude committed
22 23 24 25 26 27 28 29 30 31 32 33
transformation "inline_trivial"

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

transformation "encoding_tptp"

theory BuiltIn
34
  syntax predicate (=)  "(%1 = %2)"
MARCHE Claude's avatar
MARCHE Claude committed
35 36 37 38 39 40 41 42
end

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