add the prover cvc4

drivers/cvc4.drv

+import "cvc4_bare.drv"
+import "discrimination.gen"
+
+(*
+Local Variables:
+mode: why
+compile-command: "unset LANG; make -C .. bench"
+End:
+*)

drivers/cvc4_bare.drv

+(* Why driver for SMT syntax *)
+
+prelude ";;; this is a prelude for CVC4"
+prelude "(set-logic AUFNIRA)"
+(** A  : Array
+    UF : Uninterpreted Function
+    DT : Datatypes (not needed at the end ...)
+    NIRA : NonLinear Integer Reals Arithmetic
+*)
+
+printer "smtv2"
+filename "%f-%t-%g.smt2"
+
+valid "^unsat"
+unknown "^\\(unknown\\|sat\\|Fail\\)" ""
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+time "why3cpulimit time : %s s"
+
+
+(* À discuter *)
+(*transformation "simplify_recursive_definition"*)
+transformation "inline_trivial"
+
+
+transformation "eliminate_builtin"
+transformation "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate"
+transformation "encoding_smt"
+
+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 CVC4 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 CVC4 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
+
+ (* Not supported currently *)
+(*
+theory Bool
+   syntax type     bool  "Bool"
+   syntax function True  "true"
+   syntax function False "false"
+   meta "encoding : kept" type bool
+end
+*)
+(** so use datatype *)
+(*
+theory Bool
+   prelude "(declare-datatypes () ((why3_bool  (why3_true) (why3_false) )))"
+   syntax type     bool  "why3_bool"
+   syntax function True  "why3_true"
+   syntax function False "why3_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)"
+   syntax function implb "(=> %1 %2)"
+end
+*)
+
+theory int.EuclideanDivision
+   syntax function div "(div %1 %2)"
+   syntax function mod "(mod %1 %2)"
+   remove prop Mod_bound
+   remove prop Div_mod
+   remove prop Mod_1
+   remove prop Div_1
+end
+
+(*
+theory real.Truncate
+  syntax function floor "(to_int %1)"
+  remove prop Floor_down
+  remove prop Floor_monotonic
+end
+*)
+
+theory map.Map
+  syntax type map "(Array %1 %2)"
+  meta "encoding : lskept" function get
+  meta "encoding : lskept" function set
+  meta "encoding : lskept" function const
+
+  syntax function get   "(select %1 %2)"
+  syntax function set   "(store %1 %2 %3)"
+(*  syntax function const "(const[%t0] %1)" *)
+end
+
+
+(*
+Local Variables:
+mode: why
+compile-command: "unset LANG; make -C .. bench"
+End:
+*)

share/provers-detection-data.conf.in

@@ -302,6 +302,15 @@ version_old = "1.3"
 command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt %f"
 driver = "drivers/z3_smtv1.drv"
 
+[ATP cvc4]
+name = "CVC4"
+exec = "cvc4"
+version_switch = "--version"
+version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
+version_ok  = "0.0prerelease"
+driver = "drivers/cvc4.drv"
+command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e --lang=smt2 %f"
+
 [ATP zenon]
 name = "Zenon"
 exec = "zenon"