Counterexample support for cvc4 moved to cvc4-1.5

drivers/cvc4_14.drv

@@ -12,19 +12,6 @@ prelude "(set-logic AUFBVDTNIRA)"
    does not seem to include DT
 *)
 
-(* Counterexamples: enable model construction *)
-prelude ";; Enable model construction"
-prelude "(set-option :produce-models true)"
-
-(* Counterexamples: makes it possible to get rid of more quantifiers while introducing premises *) 
-(* transformation "split_intro" *)
-
-(* Counterexamples: get rid of some quantifiers - makes it possible to query model values of the variables in premises *)
-transformation "introduce_premises"
-
-(* Counterexamples: set model parser *)
-model_parser "cvc4_z3"
-
 import "smt-libv2.drv"
 import "discrimination.gen"
 

drivers/cvc4_15.drv

+(** Why3 driver for CVC4 >= 1.5 *)
+
+prelude "(set-logic AUFBVDTLIRA)"
+(*
+    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
+*)
+
+(* Counterexamples: enable model construction *)
+prelude ";; Enable model construction"
+prelude "(set-option :produce-models true)"
+
+(* Counterexamples: makes it possible to get rid of more quantifiers while introducing premises *) 
+(* transformation "split_intro" *)
+
+(* Counterexamples: get rid of some quantifiers - makes it possible to query model values of the variables in premises *)
+transformation "introduce_premises"
+transformation "intro_projections_counterexmp"
+
+(* Counterexamples: set model parser *)
+model_parser "cvc4_z3"
+
+import "smt-libv2.drv"
+import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+(* temporarily disabled: too much experimental
+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"
+steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
+stepslimitexceeded "??"
+
+
+(** 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
+*)
+
+(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
+   have the same name for the function to_int *)
+theory bitvec.BitVector64
+  syntax type t "(_ BitVec 64)"
+
+  syntax function zero "#x00000000"
+  syntax function ones "#xFFFFFFFF"
+  syntax function bw_and "(bvand %1 %2)"
+  syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
+
+  syntax function add "(bvadd %1 %2)"
+  syntax function sub "(bvsub %1 %2)"
+  syntax function neg "(bvneg %1)"
+  syntax function mul "(bvmul %1 %2)"
+  syntax function udiv "(bvudiv %1 %2)"
+  syntax function urem "(bvurem %1 %2)"
+
+  syntax function lsr "(bvlshr %1 %2)"
+  syntax function lsl "(bvshl %1 %2)"
+  syntax function asr "(bvashr %1 %2)"
+  syntax converter of_int "(_ bv%1 64)"
+  syntax function to_int "(bv2nat %1)"
+  remove prop to_int_of_int
+  remove prop to_int_extensionality
+  remove prop to_int_bounds
+  syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
+
+  remove prop to_int_add
+  remove prop to_int_sub
+  remove prop to_int_neg
+  remove prop to_int_mul
+  remove prop to_int_udiv
+  remove prop to_int_urem
+  remove prop to_int_lsr
+  remove prop to_int_lsl
+
+  remove prop nth_ext
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_or
+  remove prop Nth_bw_and
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+
+  syntax predicate ult "(bvult %1 %2)"
+  syntax predicate ule "(bvule %1 %2)"
+  syntax predicate ugt "(bvugt %1 %2)"
+  syntax predicate uge "(bvuge %1 %2)"
+
+  syntax function nth
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 64)) (_ bv0 64)))"
+
+  syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
+  syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
+end
+
+theory bitvec.BitVector32
+  syntax type t "(_ BitVec 32)"
+
+  syntax function zero "#x00000000"
+  syntax function ones "#xFFFFFFFF"
+  syntax function bw_and "(bvand %1 %2)"
+  syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
+
+  syntax function add "(bvadd %1 %2)"
+  syntax function sub "(bvsub %1 %2)"
+  syntax function neg "(bvneg %1)"
+  syntax function mul "(bvmul %1 %2)"
+  syntax function udiv "(bvudiv %1 %2)"
+  syntax function urem "(bvurem %1 %2)"
+
+  syntax function lsr "(bvlshr %1 %2)"
+  syntax function lsl "(bvshl %1 %2)"
+  syntax function asr "(bvashr %1 %2)"
+  syntax converter of_int "(_ bv%1 32)"
+  syntax function to_int "(bv2nat %1)"
+  remove prop to_int_of_int
+  remove prop to_int_extensionality
+  remove prop to_int_bounds
+  syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
+
+  remove prop to_int_add
+  remove prop to_int_sub
+  remove prop to_int_neg
+  remove prop to_int_mul
+  remove prop to_int_udiv
+  remove prop to_int_urem
+  remove prop to_int_lsr
+  remove prop to_int_lsl
+
+  remove prop nth_ext
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_or
+  remove prop Nth_bw_and
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+
+  syntax predicate ult "(bvult %1 %2)"
+  syntax predicate ule "(bvule %1 %2)"
+  syntax predicate ugt "(bvugt %1 %2)"
+  syntax predicate uge "(bvuge %1 %2)"
+
+  syntax function nth
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 32)) (_ bv0 32)))"
+
+  syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
+  syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
+end
+
+theory bitvec.BitVector16
+  syntax type t "(_ BitVec 16)"
+
+  syntax function zero "#x0000"
+  syntax function ones "#xFFFF"
+  syntax function bw_and "(bvand %1 %2)"
+  syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
+
+  syntax function add "(bvadd %1 %2)"
+  syntax function sub "(bvsub %1 %2)"
+  syntax function neg "(bvneg %1)"
+  syntax function mul "(bvmul %1 %2)"
+  syntax function udiv "(bvudiv %1 %2)"
+  syntax function urem "(bvurem %1 %2)"
+
+  syntax function lsr "(bvlshr %1 %2)"
+  syntax function lsl "(bvshl %1 %2)"
+  syntax function asr "(bvashr %1 %2)"
+  syntax converter of_int "(_ bv%1 16)"
+  syntax function to_int "(bv2nat %1)"
+  remove prop to_int_of_int
+  remove prop to_int_extensionality
+  remove prop to_int_bounds
+  syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
+
+  remove prop to_int_add
+  remove prop to_int_sub
+  remove prop to_int_neg
+  remove prop to_int_mul
+  remove prop to_int_udiv
+  remove prop to_int_urem
+  remove prop to_int_lsr
+  remove prop to_int_lsl
+
+  remove prop nth_ext
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_or
+  remove prop Nth_bw_and
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+
+  syntax predicate ult "(bvult %1 %2)"
+  syntax predicate ule "(bvule %1 %2)"
+  syntax predicate ugt "(bvugt %1 %2)"
+  syntax predicate uge "(bvuge %1 %2)"
+
+  syntax function nth
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 16)) (_ bv0 16)))"
+
+  syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
+  syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
+end
+
+theory bitvec.BitVector8
+  syntax type t "(_ BitVec 8)"
+
+  syntax function zero "#x00"
+  syntax function ones "#xFF"
+  syntax function bw_and "(bvand %1 %2)"
+  syntax function bw_or "(bvor %1 %2)"
+  syntax function bw_xor "(bvxor %1 %2)"
+  syntax function bw_not "(bvnot %1)"
+
+  syntax function add "(bvadd %1 %2)"
+  syntax function sub "(bvsub %1 %2)"
+  syntax function neg "(bvneg %1)"
+  syntax function mul "(bvmul %1 %2)"
+  syntax function udiv "(bvudiv %1 %2)"
+  syntax function urem "(bvurem %1 %2)"
+
+  syntax function lsr "(bvlshr %1 %2)"
+  syntax function lsl "(bvshl %1 %2)"
+  syntax function asr "(bvashr %1 %2)"
+  syntax converter of_int "(_ bv%1 8)"
+  syntax function to_int "(bv2nat %1)"
+  remove prop to_int_of_int
+  remove prop to_int_extensionality
+  remove prop to_int_bounds
+  syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
+
+  remove prop to_int_add
+  remove prop to_int_sub
+  remove prop to_int_neg
+  remove prop to_int_mul
+  remove prop to_int_udiv
+  remove prop to_int_urem
+  remove prop to_int_lsr
+  remove prop to_int_lsl
+
+  remove prop nth_ext
+  remove prop Nth_zero
+  remove prop Nth_ones
+  remove prop Nth_bw_or
+  remove prop Nth_bw_and
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+
+  syntax predicate ult "(bvult %1 %2)"
+  syntax predicate ule "(bvule %1 %2)"
+  syntax predicate ugt "(bvugt %1 %2)"
+  syntax predicate uge "(bvuge %1 %2)"
+
+  syntax function nth
+    "(not (= (bvand (bvlshr %1 %2) (_ bv1 8)) (_ bv0 8)))"
+
+  syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
+  syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
+end

share/provers-detection-data.conf

@@ -87,7 +87,7 @@ version_switch = "--version"
 version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
 version_ok  = "1.5-prerelease"
 version_ok  = "1.5"
-driver = "drivers/cvc4_14.drv"
+driver = "drivers/cvc4_15.drv"
 # --random-seed=42 is not needed as soon as --random-freq=0.0 by default
 # to try: --inst-when=full-last-call
 command = "%l/why3-cpulimit %T %m -s %e --stats --tlimit-per=%t000 --lang=smt2 %f"