Commit f374ae6a authored by Claude Marche's avatar Claude Marche

miserably failed attempts to support zenon and iprover

parent 47b6786a
(* Why driver for first-order tptp provers *)
printer "tptp-fof"
filename "%f-%t-%g.p"
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:
*)
(* Why driver for first-order tptp provers *)
printer "tptp-fof"
filename "%f-%t-%g.p"
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:
*)
......@@ -11,16 +11,10 @@ Lemma predicate_extensionality:
Admitted.
(* "it is folklore that the two are consistent" *)
(*
Hypothesis eq_dec:
forall {a:Type} {a_WT:WhyType a} (x y:a),
x=y \/ x<>y.
*)
(* Why3 goal *)
Definition set : forall (a:Type) {a_WT:WhyType a}, Type.
intros.
exact (a -> Prop).
intros.
exact (a -> Prop).
Defined.
Global Instance set_WhyType : forall a {a_WT:WhyType a}, WhyType (set a).
......@@ -98,7 +92,7 @@ Defined.
Lemma add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
intros a a_WT x y s.
unfold add, mem; intuition.
unfold add, mem; intuition.
Qed.
(* Why3 goal *)
......@@ -111,7 +105,7 @@ Defined.
Lemma remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
intros a a_WT x y s.
unfold remove, mem; intuition.
unfold remove, mem; intuition.
Qed.
(* Why3 goal *)
......
......@@ -262,6 +262,25 @@ version_old = "1.3"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt %f"
driver = "drivers/z3_smtv1.drv"
[ATP zenon]
name = "Zenon"
exec = "zenon"
exec = "zenon-0.7.1"
version_switch = "-v"
version_regexp = "zenon version \\([^ \n\t]+\\)"
version_ok = "0.7.1"
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -itptp -max-size %mM -max-time %ts %f"
driver = "drivers/zenon.drv"
[ATP iprover]
name = "iProver"
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"
driver = "drivers/iprover.drv"
[ITP coq]
name = "Coq"
exec = "coqtop -batch"
......
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