vampire.drv 1.07 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2
(* Why driver for first-order tptp provers *)

3
printer "tptp-fof"
MARCHE Claude's avatar
MARCHE Claude committed
4 5
filename "%f-%t-%g.p"

6
valid   "Refutation found"
7 8
(* timeout "Aborted by signal SIGXCPU on" *)
unknown "Time limit reached" "Time out"
9
unknown "Refutation not found" "Unknown"
MARCHE Claude's avatar
MARCHE Claude committed
10 11 12 13 14 15 16 17 18 19 20 21 22
(* invalid "Completion found" *)
(* invalid "SZS status CounterSatisfiable" *)
(* timeout "Ran out of time" *)
(* timeout "Resource 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 *)

23
(*transformation "simplify_recursive_definition"*)
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26 27 28 29 30 31 32 33 34 35
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
36
  syntax predicate (=)  "(%1 = %2)"
MARCHE Claude's avatar
MARCHE Claude committed
37 38 39 40 41 42 43 44
end

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