Skip to content

GitLab

why3
why3
Commit 933c5de2 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Support for veriT 201310

parent 15ca0f50
Hide whitespace changes
Inline Side-by-side
Showing with 191 additions and 3 deletions
drivers/verit.drv
View file @ 933c5de2
(* Why driver for SMT syntax *)
prelude ";;; this is a prelude for veriT"
prelude "(set-logic AUFLIRA)"
printer "smtv2"
filename "%f-%t-%g.smt2"
valid "^unsat"
unknown "^\\(unknown\\|sat\\)" ""
unknown "non-linear reasoning desactivated" ""
time "why3cpulimit time : %s s"
(* À discuter *)
......@@ -114,7 +117,7 @@ theory real.Real
end
theory Bool
syntax type bool "bool"
syntax type bool "Bool"
syntax function True "true"
syntax function False "false"
meta "encoding : kept" type bool
......
examples/logic/agatha/why3session.xml
View file @ 933c5de2
......@@ -25,6 +25,10 @@
id="5"
name="Z3"
version="4.3.1"/>
<prover
id="6"
name="veriT"
version="201310"/>
<file
name="../agatha.why"
verified="true"
......@@ -91,6 +95,14 @@
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Diff2"
......@@ -148,6 +160,14 @@
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Diff3"
......@@ -205,6 +225,14 @@
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Enigma"
......@@ -246,6 +274,14 @@
archived="false">
<result status="valid" time="0.06"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
</file>
......
examples/logic/einstein/why3session.xml
View file @ 933c5de2
......@@ -45,6 +45,10 @@
id="10"
name="Z3"
version="4.3.1"/>
<prover
id="11"
name="veriT"
version="201310"/>
<file
name="../einstein.why"
verified="false"
......@@ -178,6 +182,14 @@
archived="false">
<result status="valid" time="1.87"/>
</proof>
<proof
prover="11"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="Wrong"
......@@ -275,6 +287,14 @@
archived="false">
<result status="timeout" time="4.97"/>
</proof>
<proof
prover="11"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="4.97"/>
</proof>
</goal>
<goal
name="G2"
......@@ -372,6 +392,14 @@
archived="false">
<result status="valid" time="2.15"/>
</proof>
<proof
prover="11"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
</file>
......
examples/logic/genealogy/why3session.xml
View file @ 933c5de2
......@@ -49,6 +49,10 @@
id="11"
name="Zenon"
version="0.7.1"/>
<prover
id="12"
name="veriT"
version="201310"/>
<file
name="../genealogy.why"
verified="true"
......@@ -163,6 +167,15 @@
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="12"
timelimit="5"
memlimit="4000"
edited="genealogy-Genealogy-Child_is_son_or_daughter_1.smt2"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Sibling_sym"
......@@ -268,6 +281,14 @@
archived="false">
<result status="timeout" time="5.23"/>
</proof>
<proof
prover="12"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Sibling_is_brother_or_sister"
......@@ -373,6 +394,14 @@
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="12"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Grandparent_is_grandfather_or_grandmother"
......@@ -462,6 +491,14 @@
archived="false">
<result status="timeout" time="5.26"/>
</proof>
<proof
prover="12"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Grandfather_male"
......@@ -567,6 +604,14 @@
archived="false">
<result status="timeout" time="5.10"/>
</proof>
<proof
prover="12"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Grandmother_female"
......@@ -672,6 +717,14 @@
archived="false">
<result status="timeout" time="5.27"/>
</proof>
<proof
prover="12"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Only_two_grandfathers"
......@@ -769,6 +822,14 @@
archived="false">
<result status="timeout" time="5.27"/>
</proof>
<proof
prover="12"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
</file>
......
examples/mccarthy/why3session.xml
View file @ 933c5de2
......@@ -13,10 +13,14 @@
id="2"
name="Z3"
version="2.19"/>
<prover
id="3"
name="veriT"
version="201310"/>
<file
name="../mccarthy.mlw"
verified="true"
expanded="false">
expanded="true">
<theory
name="McCarthy91"
locfile="../mccarthy.mlw"
......@@ -58,6 +62,14 @@
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter f91_nonrec"
......@@ -109,6 +121,14 @@
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter f91_nonrec.2"
......@@ -145,6 +165,14 @@
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter f91_nonrec.3"
......@@ -181,6 +209,14 @@
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter f91_nonrec.4"
......@@ -217,6 +253,14 @@
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter f91_nonrec.5"
......@@ -253,6 +297,14 @@
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter f91_nonrec.6"
......@@ -289,6 +341,14 @@
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</transf>
</goal>
......
share/provers-detection-data.conf
View file @ 933c5de2
......@@ -270,7 +270,7 @@ name = "veriT"
exec = "veriT"
exec = "veriT-201310"
version_switch = "--version"
version_regexp = "Version: \\([^ \n\r]+\\)"
version_regexp = "version \\([^ \n\r]+\\)"
command = "%l/why3-cpulimit %t %m -s %e --enable-simp --enable-unit-simp --enable-simp-sym --enable-unit-subst-simp --enable-bclause %f"
driver = "drivers/verit.drv"
version_ok = "201310"
......
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