support for veriT 201410

drivers/verit.drv

-(* Why driver for SMT syntax *)
+(* Why3 driver for veriT solver *)
 
 prelude ";;; this is a prelude for veriT"
 prelude "(set-logic AUFLIRA)"
+(* A  : Array
+   UF : Uninterpreted Function
+   LIRA : Linear Integer Reals Arithmetic
+*)
 
-printer "smtv2"
-filename "%f-%t-%g.smt2"
+import "smt-libv2.drv"
+import "discrimination.gen"
 
-valid "^unsat"
-unknown "^\\(unknown\\|sat\\)" ""
+(* specific message from veriT 201310 *)
 unknown "non-linear reasoning desactivated" ""
 
-time "why3cpulimit time : %s s"
-
-(* À discuter *)
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"
@@ -27,114 +27,10 @@ transformation "simplify_formula"
 transformation "encoding_smt"
 transformation "encoding_sort"
 
-theory BuiltIn
-  syntax type int   "Int"
-  syntax type real  "Real"
-  syntax predicate (=)  "(= %1 %2)"
-
-  meta "encoding : kept" type int
-end
-
-theory int.Int
-
-  prelude ";;; this is a prelude for integer arithmetic"
-
-  syntax function zero "0"
-  syntax function one  "1"
-
-  syntax function (+)  "(+ %1 %2)"
-  syntax function (-)  "(- %1 %2)"
-  syntax function (*)  "(* %1 %2)"
-  syntax function (-_) "(- %1)"
-
-  syntax predicate (<=) "(<= %1 %2)"
-  syntax predicate (<)  "(< %1 %2)"
-  syntax predicate (>=) "(>= %1 %2)"
-  syntax predicate (>)  "(> %1 %2)"
-
-  remove prop CommutativeGroup.Comm.Comm
-  remove prop CommutativeGroup.Assoc
-  remove prop CommutativeGroup.Unit_def_l
-  remove prop CommutativeGroup.Unit_def_r
-  remove prop CommutativeGroup.Inv_def_l
-  remove prop CommutativeGroup.Inv_def_r
-  remove prop Assoc.Assoc
-  remove prop Mul_distr_l
-  remove prop Mul_distr_r
-  remove prop Comm.Comm
-  remove prop Unitary
-  remove prop Refl
-  remove prop Trans
-  remove prop Antisymm
-  remove prop Total
-  remove prop NonTrivialRing
-  remove prop CompatOrderAdd
-  remove prop ZeroLessOne
-
-end
-
-
-theory real.Real
-
-  prelude ";;; this is a prelude for real arithmetic"
-
-  syntax function zero "0.0"
-  syntax function one  "1.0"
-
-  syntax function (+)  "(+ %1 %2)"
-  syntax function (-)  "(- %1 %2)"
-  syntax function (*)  "(* %1 %2)"
-  syntax function (/)  "(/ %1 %2)"
-  syntax function (-_) "(- %1)"
-  syntax function inv  "(/ 1.0 %1)"
-
-  syntax predicate (<=) "(<= %1 %2)"
-  syntax predicate (<)  "(< %1 %2)"
-  syntax predicate (>=) "(>= %1 %2)"
-  syntax predicate (>)  "(> %1 %2)"
-
-  remove prop CommutativeGroup.Comm.Comm
-  remove prop CommutativeGroup.Assoc
-  remove prop CommutativeGroup.Unit_def_l
-  remove prop CommutativeGroup.Unit_def_r
-  remove prop CommutativeGroup.Inv_def_l
-  remove prop CommutativeGroup.Inv_def_r
-  remove prop Assoc.Assoc
-  remove prop Mul_distr_l
-  remove prop Mul_distr_r
-  remove prop Comm.Comm
-  remove prop Unitary
-  remove prop Inverse
-  remove prop Refl
-  remove prop Trans
-  remove prop Antisymm
-  remove prop Total
-  remove prop NonTrivialRing
-  remove prop CompatOrderAdd
-  remove prop ZeroLessOne
-
-  meta "encoding : kept" type real
-
-end
-
-theory Bool
-   syntax type bool      "Bool"
-   syntax function True  "true"
-   syntax function False "false"
-   meta "encoding : kept" type bool
-end
-
-theory bool.Bool
-   syntax function andb  "(and %1 %2)"
-   syntax function orb   "(or %1 %2)"
-   syntax function xorb  "(xor %1 %2)"
-   syntax function notb  "(not %1)"
-end
-
 
 (*
 Local Variables:
-mode: why
+mode: why3
 compile-command: "unset LANG; make -C .. bench"
 End:
 *)

examples/logic/genealogy/why3session.xml

@@ -26,6 +26,7 @@
 <prover id="21" name="CVC4" version="1.3" timelimit="3" memlimit="1000"/>
 <prover id="22" name="Vampire" version="0.6" timelimit="3" memlimit="1000"/>
 <prover id="23" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
+<prover id="24" name="veriT" version="201410" timelimit="5" memlimit="1000"/>
 <file name="../genealogy.why" expanded="true">
 <theory name="Genealogy" sum="35e1439432a79e05534b2c5cf39ad9dc" expanded="true">
  <goal name="Child_is_son_or_daughter" expanded="true">
@@ -53,6 +54,7 @@
  <proof prover="21"><result status="unknown" time="0.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.01" steps="10"/></proof>
+ <proof prover="24"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Sibling_sym" expanded="true">
  <proof prover="1"><result status="valid" time="0.00"/></proof>
@@ -77,6 +79,7 @@
  <proof prover="21"><result status="valid" time="0.00"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.01" steps="2"/></proof>
+ <proof prover="24"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Sibling_is_brother_or_sister" expanded="true">
  <proof prover="1"><result status="unknown" time="0.01"/></proof>
@@ -101,6 +104,7 @@
  <proof prover="21"><result status="unknown" time="0.01"/></proof>
  <proof prover="22"><result status="valid" time="0.00"/></proof>
  <proof prover="23"><result status="valid" time="0.01" steps="9"/></proof>
+ <proof prover="24"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Grandparent_is_grandfather_or_grandmother" expanded="true">
  <proof prover="1"><result status="valid" time="0.01"/></proof>
@@ -124,6 +128,7 @@
  <proof prover="21"><result status="valid" time="0.00"/></proof>
  <proof prover="22"><result status="valid" time="0.01"/></proof>
  <proof prover="23"><result status="valid" time="0.01" steps="32"/></proof>
+ <proof prover="24"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Grandfather_male" expanded="true">
  <proof prover="1"><result status="valid" time="0.00"/></proof>
@@ -147,6 +152,7 @@
  <proof prover="21"><result status="valid" time="0.00"/></proof>
  <proof prover="22"><result status="valid" time="0.03"/></proof>
  <proof prover="23"><result status="valid" time="0.01" steps="5"/></proof>
+ <proof prover="24"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Grandmother_female" expanded="true">
  <proof prover="1"><result status="valid" time="0.01"/></proof>
@@ -170,6 +176,7 @@
  <proof prover="21"><result status="valid" time="0.00"/></proof>
  <proof prover="22"><result status="valid" time="0.01"/></proof>
  <proof prover="23"><result status="valid" time="0.01" steps="5"/></proof>
+ <proof prover="24"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Only_two_grandfathers" expanded="true">
  <proof prover="1"><result status="valid" time="0.01"/></proof>
@@ -193,6 +200,7 @@
  <proof prover="21"><result status="valid" time="0.00"/></proof>
  <proof prover="22"><result status="valid" time="0.01"/></proof>
  <proof prover="23"><result status="valid" time="0.01" steps="10"/></proof>
+ <proof prover="24"><result status="valid" time="0.00"/></proof>
  </goal>
 </theory>
 </file>

share/provers-detection-data.conf

@@ -277,6 +277,16 @@ command = "%l/why3-cpulimit %t 0 -s %e %f"
 driver = "drivers/beagle.drv"
 version_ok = "0.4.1"
 
+[ATP verit]
+name = "veriT"
+exec = "veriT"
+exec = "veriT-201410"
+version_switch = "--version"
+version_regexp = "version \\([^ \n\r]+\\)"
+command = "%l/why3-cpulimit %t %m -s %e --disable-print-success %f"
+driver = "drivers/verit.drv"
+version_ok = "201410"
+
 [ATP verit]
 name = "veriT"
 exec = "veriT"
@@ -286,7 +296,7 @@ version_regexp = "version \\([^ \n\r]+\\)"
 command = "%l/why3-cpulimit %t %m -s %e --disable-print-success --enable-simp \
 --enable-unit-simp --enable-simp-sym --enable-unit-subst-simp --enable-bclause %f"
 driver = "drivers/verit.drv"
-version_ok = "201310"
+version_old = "201310"
 
 # Z3 4.3.2 does not support option global option -rs anymore.
 # use settings given by "z3 -p" instead