Commit eb4c08b3 authored by MARCHE Claude's avatar MARCHE Claude

factorize tptp driver

parent c1ef48a2
(* Why driver for Eprover *)
valid "Proof found"
invalid "Completion found"
timeout "Ran out of time"
timeout "CPU time limit exceeded"
outofmemory "Out of Memory"
unknown "No Proof Found" ""
fail "Failure.*" "\"\\0\""
time "why3cpulimit time : %s s"
import "tptp.gen"
(* Why driver for first-order tptp provers *)
printer "tptp-fof"
filename "%f-%t-%g.p"
timeout "Time Out Virtual"
valid "PROOF-FOUND"
(* timeout "Aborted by signal SIGXCPU on" *)
unknown "Time limit reached" "Time out"
unknown "Refutation not found" ""
outofmemory "Memory limit exceeded"
(* invalid "Completion found" *)
(* invalid "SZS status CounterSatisfiable" *)
(* timeout "Ran out of time" *)
(* timeout "Resource limit exceeded" *)
(* unknown "No Proof Found" "" *)
(* fail "Failure.*" "\"\\0\"" *)
time "why3cpulimit time : %s s"
(* time "%h:%m:%s on the problem" *)
(* time "Total time[ ]*: %s s" *)
(* to be improved *)
(*transformation "simplify_recursive_definition"*)
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
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
import "tptp.gen"
(* Why driver for SPASS *)
valid "Proof found"
invalid "Completion found"
timeout "Ran out of time"
timeout "CPU time limit exceeded"
outofmemory "Out of Memory"
unknown "No Proof Found" ""
fail "Failure.*" "\"\\0\""
import "tptp.gen"
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
......@@ -5,16 +5,19 @@ filename "%f-%t-%g.p"
valid "Proof found"
invalid "Completion found"
invalid "SZS status CounterSatisfiable"
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" ""
timeout "Ran out of time"
(* timeout "Resource limit exceeded" *)
timeout "CPU time limit exceeded"
outofmemory "Out of Memory"
unknown "No Proof Found" ""
fail "Failure.*" "\"\\0\""
time "why3cpulimit time : %s s"
(* time "%h:%m:%s on the problem" *)
(* time "Total time[ ]*: %s s" *)
(* to be improved *)
......
(* Why driver for first-order tptp provers *)
(* Why common driver for first-order tptp provers *)
printer "tptp-fof"
filename "%f-%t-%g.p"
valid "Proof found"
invalid "Completion found"
invalid "SZS status CounterSatisfiable"
timeout "Ran out of time"
(* timeout "Resource limit exceeded" *)
timeout "CPU time limit exceeded"
outofmemory "Out of Memory"
unknown "No Proof Found" ""
fail "Failure.*" "\"\\0\""
time "why3cpulimit time : %s s"
(* time "%h:%m:%s on the problem" *)
(* time "Total time[ ]*: %s s" *)
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" ""
time "why3cpulimit time : %s s"
(* to be improved *)
......@@ -36,9 +32,3 @@ theory BuiltIn
meta "eliminate_algebraic" "no_index"
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
(* Why driver for first-order tptp provers *)
printer "tptp-fof"
filename "%f-%t-%g.p"
(* Why driver for Vampire *)
valid "Refutation found"
(* timeout "Aborted by signal SIGXCPU on" *)
unknown "Time limit reached" "Time out"
unknown "Refutation not found" ""
outofmemory "Memory limit exceeded"
(* invalid "Completion found" *)
(* invalid "SZS status CounterSatisfiable" *)
(* timeout "Ran out of time" *)
(* timeout "Resource limit exceeded" *)
(* unknown "No Proof Found" "" *)
(* fail "Failure.*" "\"\\0\"" *)
time "why3cpulimit time : %s s"
(* time "%h:%m:%s on the problem" *)
(* time "Total time[ ]*: %s s" *)
(* to be improved *)
(*transformation "simplify_recursive_definition"*)
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
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
import "tptp.gen"
......@@ -109,7 +109,7 @@ version_regexp = "E \\([-0-9.]+\\) [^\n]+"
version_ok = "1.4"
# we pass time 0 to why3-cpulimit to avoid race
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
driver = "drivers/tptp.drv"
driver = "drivers/eprover.drv"
[ATP gappa]
name = "Gappa"
......@@ -170,7 +170,7 @@ version_regexp = "SPASS V \\([^ \n\t]+\\)"
version_ok = "3.7"
# we pass time 0 to why3-cpulimit to avoid race
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
driver = "drivers/tptp.drv"
driver = "drivers/spass.drv"
[ATP vampire]
name = "Vampire"
......@@ -278,7 +278,7 @@ exec = "iprover"
version_switch = " | grep iProver"
version_regexp = "iProver v\\([^ \n\t]+\\)"
version_ok = "0.8.1"
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e --clausifier eprover --clausifier_options \"--tstp-format \" %f"
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e --fof true --out_options none --time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \"eprover --cnf --tstp-format \" %f"
driver = "drivers/iprover.drv"
[ITP coq]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment