Commit c1ef48a2 authored by MARCHE Claude's avatar MARCHE Claude

Support for Zenon, seems to work now

parent e544432d
......@@ -4,20 +4,10 @@ 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\"" *)
timeout "Zenon error: could not find a proof within the time limit"
outofmemory "Zenon error: could not find a proof within the memory size limit"
unknown "NO-PROOF" "no proof found"
time "why3cpulimit time : %s s"
(* time "%h:%m:%s on the problem" *)
(* time "Total time[ ]*: %s s" *)
(* to be improved *)
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="./genealogy/why3session.xml" shape_version="2">
name="examples/genealogy/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
......@@ -38,19 +38,23 @@
id="8"
name="Z3"
version="3.2"/>
<prover
id="9"
name="Zenon"
version="0.7.1"/>
<file
name="../genealogy.why"
verified="true"
expanded="false">
expanded="true">
<theory
name="Genealogy"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="2" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
<goal
name="Child_is_son_or_daughter"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="23" loccnumb="7" loccnume="31"
sum="0fde3c4f7583ff6e9fdaf0ce7b4f3389"
proved="true"
......@@ -96,6 +100,15 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="120"
memlimit="1000"
edited="genealogy-Genealogy-Child_is_son_or_daughter_1.p"
obsolete="false"
archived="false">
<result status="valid" time="0.36"/>
</proof>
<proof
prover="8"
timelimit="5"
......@@ -131,7 +144,7 @@
</goal>
<goal
name="Sibling_sym"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="29" loccnumb="7" loccnume="18"
sum="9a92a8e0fe47bbd3fabeaf95bdb6478a"
proved="true"
......@@ -177,6 +190,14 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="120"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.34"/>
</proof>
<proof
prover="8"
timelimit="5"
......@@ -212,7 +233,7 @@
</goal>
<goal
name="Sibling_is_brother_or_sister"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="34" loccnumb="7" loccnume="35"
sum="54165903233e74eef52a31f1d35b8b51"
proved="true"
......@@ -258,6 +279,14 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="120"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.32"/>
</proof>
<proof
prover="8"
timelimit="5"
......@@ -293,7 +322,7 @@
</goal>
<goal
name="Grandparent_is_grandfather_or_grandmother"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="45" loccnumb="7" loccnume="48"
sum="c61ec3544cb1baa038f6db3e31109756"
proved="true"
......@@ -331,6 +360,15 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="120"
memlimit="1000"
edited="genealogy-Genealogy-Grandparent_is_grandfather_or_grandmother_1.p"
obsolete="false"
archived="false">
<result status="timeout" time="120.60"/>
</proof>
<proof
prover="8"
timelimit="5"
......@@ -358,7 +396,7 @@
</goal>
<goal
name="Grandfather_male"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="48" loccnumb="7" loccnume="23"
sum="f21f5bc53305ec525334fbfe7d8ee21b"
proved="true"
......@@ -404,6 +442,14 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="120"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="125.11"/>
</proof>
<proof
prover="8"
timelimit="5"
......@@ -439,7 +485,7 @@
</goal>
<goal
name="Grandmother_female"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="50" loccnumb="7" loccnume="25"
sum="6046a0d8dba383c5e7e8a8521140862d"
proved="true"
......@@ -485,6 +531,14 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="120"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="121.38"/>
</proof>
<proof
prover="8"
timelimit="5"
......@@ -520,7 +574,7 @@
</goal>
<goal
name="Only_two_grandfathers"
locfile="./genealogy/../genealogy.why"
locfile="examples/genealogy/../genealogy.why"
loclnum="53" loccnumb="7" loccnume="28"
sum="2644ef6a6d637a753381302d35a2bf73"
proved="true"
......@@ -566,6 +620,14 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="120"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="121.51"/>
</proof>
<proof
prover="8"
timelimit="5"
......
......@@ -269,7 +269,7 @@ 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"
command = "'@LOCALBIN@why3-cpulimit' %T 0 -s %e -p0 -itptp -max-size %mM -max-time %ts %f"
driver = "drivers/zenon.drv"
[ATP iprover]
......
......@@ -865,7 +865,10 @@ let editors_page c (notebook:GPack.notebook) =
let preferences (c : t) =
let dialog = GWindow.dialog ~title:"Why3: preferences" () in
let dialog = GWindow.dialog
~modal:true
~title:"Why3: preferences" ()
in
let vbox = dialog#vbox in
let notebook = GPack.notebook ~packing:vbox#add () in
(** page "general settings" **)
......
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