Reorganize drivers for Z3 and CVC4

drivers/cvc4.drv

-import "cvc4_bare.drv"
+(** Why3 driver for CVC4 *)
+
+prelude "(set-logic AUFBVDTNIRA)"
+(*
+    A  : Array
+    UF : Uninterpreted Function
+    BV : BitVectors
+    DT : Datatypes
+    NIRA : NonLinear Integer Reals Arithmetic
+*)
+(* prelude "(set-logic ALL_SUPPORTED)"
+   does not seem to include DT
+*)
+
+import "smt-libv2.drv"
 import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+transformation "eliminate_epsilon"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate"
+transformation "encoding_smt"
+
+(** Error messages specific to CVC4 *)
+
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+timeout "interrupted by timeout"
+
+(* regexp for steps should match things like
+
+smt::SmtEngine::resourceUnitsUsed, 1041
+
+but not in the same line as the "valid" answer
+
+*)
+
+(** Extra theories supported by CVC4 *)
+
+(* Disabled:
+   CVC4 division seems to be neither the Euclidean one, nor the Computer one
+
+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 int.ComputerDivision
+   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
+*)

drivers/cvc4_bare.drv → drivers/cvc4_14.drv

+(** Why3 driver for CVC4 *)
 
 prelude "(set-logic AUFBVDTNIRA)"
 (*
-prelude "(set-logic AUFNIRA)"   (* how come bv is supported by cvc4 in this logic ?!? *)
-*)
-(** A  : Array
+    A  : Array
     UF : Uninterpreted Function
     BV : BitVectors
     DT : Datatypes
     NIRA : NonLinear Integer Reals Arithmetic
 *)
-(* prelude "(set-logic ALL_SUPPORTED)" *)
+(* prelude "(set-logic ALL_SUPPORTED)"
+   does not seem to include DT
+*)
 
 import "smt-libv2.drv"
+import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "detect_polymorphism"
+transformation "eliminate_definition_if_poly"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic_if_poly"
+transformation "eliminate_epsilon"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate_if_poly"
+transformation "encoding_smt_if_poly"
+
+(** Error messages specific to CVC4 *)
+
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+timeout "interrupted by timeout"
 
 (* regexp for steps should match things like
 
@@ -21,8 +42,11 @@ but not in the same line as the "valid" answer
 
 *)
 
-(* CVC4 division seems to be neither the Euclidean one, nor the Computer one *)
-(*
+(** Extra theories supported by CVC4 *)
+
+(* Disabled:
+   CVC4 division seems to be neither the Euclidean one, nor the Computer one
+
 theory int.EuclideanDivision
    syntax function div "(div %1 %2)"
    syntax function mod "(mod %1 %2)"

drivers/smt-libv2.drv

-(* Why driver for SMT v2 syntax for bit-vectors *)
+(* Why3 driver for SMT-LIB2 syntax, including bit-vectors *)
 
-prelude ";;; this is a prelude for smt-lib v2"
-(*prelude "(set-logic AUFNIRA)"*)
-(** A  : Array
+prelude ";;; generated by SMT-LIB2 driver"
+
+(*
+
+Note: we do not insert any command "set-logic" because its
+interpretation is specific to provers
+
+prelude "(set-logic AUFNIRA)"
+
+    A  : Array
     UF : Uninterpreted Function
     DT : Datatypes (not needed at the end ...)
     NIRA : NonLinear Integer Reals Arithmetic
+
 *)
 
 printer "smtv2"
@@ -13,25 +21,8 @@ filename "%f-%t-%g.smt2"
 
 valid "^unsat"
 unknown "^\\(unknown\\|sat\\|Fail\\)" ""
-outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
-timeout "interrupted by timeout"
 time "why3cpulimit time : %s s"
 
-(* À discuter *)
-
-transformation "inline_trivial"
-transformation "eliminate_builtin"
-transformation "detect_polymorphism"
-transformation "eliminate_definition_if_poly"
-transformation "eliminate_inductive"
-transformation "eliminate_algebraic_if_poly"
-transformation "eliminate_epsilon"
-
-transformation "simplify_formula"
-(*transformation "simplify_trivial_quantification"*)
-
-transformation "discriminate_if_poly"
-transformation "encoding_smt_if_poly"
 
 theory BuiltIn
   syntax type int   "Int"
@@ -43,7 +34,7 @@ end
 
 theory int.Int
 
-  prelude ";;; this is a prelude for smt-lib v2 integer arithmetic"
+  prelude ";;; SMT-LIB2: integer arithmetic"
 
   syntax function zero "0"
   syntax function one  "1"
@@ -82,7 +73,7 @@ end
 
 theory real.Real
 
-  prelude ";;; this is a prelude for smt-lib v2 real arithmetic"
+  prelude ";;; SMT-LIB2: real arithmetic"
 
   syntax function zero "0.0"
   syntax function one  "1.0"
@@ -143,7 +134,7 @@ theory bool.Ite
   meta "encoding : lskept" function ite
 end
 
-(*
+(* not uniformly interpreted by provers
 theory real.Truncate
   syntax function floor "(to_int %1)"
   remove prop Floor_down

drivers/z3.drv

+(** Why3 driver for Z3 <= 4.3.1 *)
+
 prelude "(set-logic AUFNIRA)"
-(** A  : Array
-    UF : Uninterpreted Function
-    DT : Datatypes (not needed at the end ...)
-    NIRA : NonLinear Integer Reals Arithmetic
+(* A  : Array
+   UF : Uninterpreted Function
+   NIRA : NonLinear Integer Reals Arithmetic
 *)
 
-import "z3_bare.drv"
+import "smt-libv2.drv"
+import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+transformation "eliminate_epsilon"
+
+transformation "simplify_formula"
+(* transformation "simplify_trivial_quantification" *)
+
+transformation "discriminate"
+transformation "encoding_smt"
+
+(** Error messages specific to Z3 *)
+
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+timeout "interrupted by timeout"
 
+(** Extra theories supported by Z3 *)
+
+(* div/mod of Z3 seems to be Euclidean Division *)
+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.FromInt
+  syntax function from_int "(to_real %1)"
+  remove prop Zero
+  remove prop One
+  remove prop Add
+  remove prop Sub
+  remove prop Mul
+  remove prop Neg
+end
+
+(* does not work: Z3 segfaults
+theory real.Trigonometry
+
+  syntax function cos "(cos %1)"
+  syntax function sin "(sin %1)"
+  syntax function pi "pi"
+  syntax function tan "(tan %1)"
+  syntax function atan "(atan %1)"
+
+end
+*)

drivers/z3_bare.drv → drivers/z3_432.drv

+(** Why3 driver for Z3 >= 4.3.2 *)
+
+(* Do not set any logic, let z3 choose by itself
+   prelude "(set-logic AUFNIRA)"
+*)
+
 import "smt-libv2.drv"
+import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "detect_polymorphism"
+transformation "eliminate_definition_if_poly"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic_if_poly"
+transformation "eliminate_epsilon"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate_if_poly"
+transformation "encoding_smt_if_poly"
+
+
+(** Error messages specific to Z3 *)
+
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+timeout "interrupted by timeout"
+
+(** Extra theories supported by Z3 *)
 
 (* div/mod of Z3 seems to be Euclidean Division *)
 theory int.EuclideanDivision
@@ -20,7 +49,7 @@ theory real.FromInt
   remove prop Neg
 end
 
-(* does not work: Z3 segfaults 
+(* does not work: Z3 segfaults
 theory real.Trigonometry
 
   syntax function cos "(cos %1)"
@@ -31,5 +60,3 @@ theory real.Trigonometry
 
 end
 *)
-
-import "discrimination.gen"
\ No newline at end of file

share/provers-detection-data.conf

@@ -96,7 +96,7 @@ version_switch = "--version"
 version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
 version_ok  = "1.5-prerelease"
 version_ok  = "1.4"
-driver = "drivers/cvc4.drv"
+driver = "drivers/cvc4_14.drv"
 # --random-seed=42 is not needed as soon as --random-freq=0.0 by default
 command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"
 
@@ -324,6 +324,7 @@ version_ok = "201310"
 
 # Z3 4.3.2 does not support option global option -rs anymore.
 # use settings given by "z3 -p" instead
+# Z3 4.3.2 supports Datatypes
 [ATP z3]
 name = "Z3"
 exec = "z3"
@@ -333,7 +334,7 @@ version_switch = "-version"
 version_regexp = "Z3 version \\([^ \n\r]+\\)"
 version_ok  = "4.3.3"
 version_ok = "4.3.2"
-driver = "drivers/z3_bare.drv"  # Do not set any logic, let z3 choose by itself
+driver = "drivers/z3_432.drv"
 command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
 
 [ATP z3]