Added support for CVC5.

config/caisar-detection-data.conf

@@ -32,6 +32,17 @@ driver = "alt_ergo"
 editor = "altgr-ergo"
 use_at_auto_level = 1
 
+[ATP cvc5]
+name = "CVC5"
+exec = "cvc5"
+version_switch = "--version 2>&1 | head -1"
+version_regexp = "This is cvc5 version \\([0-9.]+\\)"
+version_ok  = "1.0.2"
+command = "%e --stats-internal --tlimit=%t000 %f"
+command_steps = "%e --stats-internal --steps-bound %S %f"
+driver = "caisar_drivers/cvc5.drv"
+use_at_auto_level = 1
+
 [ATP marabou]
 name = "Marabou"
 exec = "Marabou"

config/drivers/cvc4_16.gen

+(** Why3 driver for CVC4 >= 1.6 (with floating point support) *)
+
+prelude "(set-info :smt-lib-version 2.6)"
+
+import "smt-libv2.gen"
+printer "smtv2.6"
+import "smt-libv2-bv.gen"
+import "cvc4_bv.gen"
+import "smt-libv2-floats.gen"
+import "discrimination.gen"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "detect_polymorphism"
+transformation "eliminate_definition_conditionally"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic_if_poly"
+transformation "eliminate_literal"
+transformation "eliminate_epsilon"
+transformation "simplify_formula"
+
+(* Prepare for counter-example query: get rid of some quantifiers
+   (makes it possible to query model values of the variables in
+   premises) and introduce counter-example projections.  Note: does
+   nothing if meta get_counterexmp is not set *)
+transformation "prepare_for_counterexmp"
+
+transformation "discriminate_if_poly"
+transformation "encoding_smt_if_poly"
+
+(** Error messages specific to CVC4 *)
+
+outofmemory "(error \".*out of memory\")"
+outofmemory "CVC4 suffered a segfault"
+outofmemory "CVC4::BVMinisat::OutOfMemoryException"
+outofmemory "std::bad_alloc"
+outofmemory "Cannot allocate memory"
+timeout "interrupted by timeout"
+steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
+(*
+specific output message when CVC4 reaches its resource limit
+*)
+steplimitexceeded "unknown (RESOURCEOUT)"
+
+
+(** Extra theories supported by CVC4 *)
+
+(* CVC4 division seems to be the Euclidean one, not 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
+*)

config/drivers/cvc4_bv.gen

+(* bitvector modules, is not in smt-libv2.gen since cvc4 and z3 don't
+   have the same name for the function to_int *)
+
+theory bv.BV_Gen
+  syntax function to_uint "(bv2nat %1)"
+end
+
+theory bv.BV256
+  (* mapping of_int to int2bv is disabled because it breaks proofs
+     in examples/bitcount, examples/esterel,
+     examples/isqrt_von_neumann, examples/rightmostbittrick,
+     examples/bitwalker *)
+
+  (* syntax function of_int "((_ int2bv 256) %1)" *)
+  syntax function t'int "(bv2nat %1)"
+end
+
+theory bv.BV128
+  (* syntax function of_int "((_ int2bv 128) %1)" *)
+  syntax function t'int "(bv2nat %1)"
+end
+
+theory bv.BV64
+  (* syntax function of_int "((_ int2bv 64) %1)" *)
+  syntax function t'int "(bv2nat %1)"
+end
+
+theory bv.BV32
+  (* syntax function of_int "((_ int2bv 32) %1)" *)
+  syntax function t'int "(bv2nat %1)"
+end
+
+theory bv.BV16
+  (* syntax function of_int "((_ int2bv 16) %1)" *)
+  syntax function t'int "(bv2nat %1)"
+end
+
+theory bv.BV8
+  (* syntax function of_int "((_ int2bv 8) %1)" *)
+  syntax function t'int "(bv2nat %1)"
+end

config/drivers/cvc5.drv

+(** Why3 driver for CVC5 1.0.0 *)
+
+prelude ";; produced by cvc5.drv ;;"
+
+transformation "actual_net_apply"
+
+prelude "(set-logic ALL)"
+
+unknown "^(error \"Can't get-info :reason-unknown when the last result wasn't unknown!\")$" "(not unknown!)"
+
+outofmemory "cvc5 suffered a segfault"
+outofmemory "cvc5::internal::Minisat::OutOfMemoryException"
+
+steps "resource::resourceUnitsUsed = \\([0-9]+\\)" 1
+
+import "cvc4_16.gen"
+
+theory BuiltIn
+
+  meta "supports_smt_get_info_unknown_reason" ""
+
+end

config/drivers/discrimination.gen

+theory BuiltIn
+  meta "select_inst_default" "local"
+  meta "select_lskept_default" "local"
+  meta "select_lsinst_default" "local"
+  meta "select_kept_default" "all"
+end
+

config/drivers/smt-libv2-bv.gen

+(* Why3 driver for SMT-LIB2, common part of bit-vector theories *)
+
+prelude ";;; SMT-LIB2 driver: bit-vectors, common part"
+
+theory bv.BV_Gen
+  remove prop size_pos
+  remove prop nth_out_of_bound
+  remove prop Nth_zeros
+  remove prop Nth_ones
+
+  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)"
+
+  (* Warning: we should NOT remove all the axioms using "allprops" *)
+
+  remove prop Nth_bw_and
+  remove prop Nth_bw_or
+  remove prop Nth_bw_xor
+  remove prop Nth_bw_not
+
+  (** Shift operators *)
+
+  remove prop Lsr_nth_low
+  remove prop Lsr_nth_high
+  remove prop lsr_zeros
+  remove prop Asr_nth_low
+  remove prop Asr_nth_high
+  remove prop asr_zeros
+  remove prop Lsl_nth_low
+  remove prop Lsl_nth_high
+  remove prop lsl_zeros
+  remove prop Nth_rotate_left
+  remove prop Nth_rotate_right
+
+  (* Conversions from/to integers *)
+
+  remove prop two_power_size_val
+  remove prop max_int_val
+
+  (* function to_int  - solver specific *)
+  (* function to_uint - solver specific *)
+  (* function of_int  - solver specific *)
+
+  remove prop to_uint_extensionality
+  remove prop to_int_extensionality
+
+  remove prop to_uint_bounds
+  (*remove prop to_uint_of_int*)
+  remove prop to_uint_size_bv
+  remove prop to_uint_zeros
+  remove prop to_uint_ones
+  remove prop to_uint_one
+
+  (* comparison operators *)
+
+  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 predicate slt "(bvslt %1 %2)"
+  syntax predicate sle "(bvsle %1 %2)"
+  syntax predicate sgt "(bvsgt %1 %2)"
+  syntax predicate sge "(bvsge %1 %2)"
+
+  (** Arithmetic operators *)
+
+  syntax function add "(bvadd %1 %2)"
+  remove prop to_uint_add
+  remove prop to_uint_add_bounded
+
+  syntax function sub "(bvsub %1 %2)"
+  remove prop to_uint_sub
+  remove prop to_uint_sub_bounded
+
+  syntax function neg "(bvneg %1)"
+  remove prop to_uint_neg
+
+  syntax function mul "(bvmul %1 %2)"
+  remove prop to_uint_mul
+  remove prop to_uint_mul_bounded
+
+  syntax function udiv "(bvudiv %1 %2)"
+  remove prop to_uint_udiv
+
+  syntax function urem "(bvurem %1 %2)"
+  remove prop to_uint_urem
+
+  syntax function sdiv "(bvsdiv %1 %2)"
+  (*remove prop to_int_sdiv*)
+
+  syntax function srem "(bvsrem %1 %2)"
+  (*remove prop to_int_srem*)
+
+  (** Bitvector alternatives for shifts, rotations and nth *)
+
+  syntax function lsr_bv "(bvlshr %1 %2)"
+  (* remove prop lsr_bv_is_lsr *)
+  remove prop to_uint_lsr
+
+  syntax function asr_bv "(bvashr %1 %2)"
+  (* remove prop asr_bv_is_asr *)
+
+  syntax function lsl_bv "(bvshl %1 %2)"
+  (* remove prop lsl_bv_is_lsl *)
+
+  remove prop to_uint_lsl
+
+  (** rotations *)
+  (* remove prop rotate_left_bv_is_rotate_left *)
+  (* remove prop rotate_right_bv_is_rotate_right *)
+
+  (** nth_bv *)
+
+  (* remove prop nth_bv_def *)
+  (* remove prop Nth_bv_is_nth *)
+  (* remove prop Nth_bv_is_nth2 *)
+
+  remove prop Extensionality
+end
+
+theory bv.BV256
+  meta "literal:keep" type t
+
+  syntax literal t "#x%64x"
+  syntax type t "(_ BitVec 256)"
+
+  syntax function zeros "#x0000000000000000000000000000000000000000000000000000000000000000"
+  syntax function one   "#x0000000000000000000000000000000000000000000000000000000000000001"
+  syntax function ones  "#xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"
+  syntax function size_bv "(_ bv256 256)"
+
+  syntax predicate is_signed_positive "(bvsge %1 (_ bv0 256))"
+
+  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv256 256))) (bvlshr %1 (bvsub (_ bv256 256) (bvurem %2 (_ bv256 256)))))"
+  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv256 256))) (bvshl %1 (bvsub (_ bv256 256) (bvurem %2 (_ bv256 256)))))"
+end
+
+theory bv.BV128
+  meta "literal:keep" type t
+
+  syntax literal t "#x%32x"
+  syntax type t "(_ BitVec 128)"
+
+  syntax function zeros "#x00000000000000000000000000000000"
+  syntax function one   "#x00000000000000000000000000000001"
+  syntax function ones  "#xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"
+  syntax function size_bv "(_ bv128 128)"
+
+  syntax predicate is_signed_positive "(bvsge %1 (_ bv0 128))"
+
+  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv128 128))) (bvlshr %1 (bvsub (_ bv128 128) (bvurem %2 (_ bv128 128)))))"
+  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv128 128))) (bvshl %1 (bvsub (_ bv128 128) (bvurem %2 (_ bv128 128)))))"
+end
+
+theory bv.BV64
+  meta "literal:keep" type t
+
+  syntax literal t "#x%16x"
+  syntax type t "(_ BitVec 64)"
+
+  syntax function zeros "#x0000000000000000"
+  syntax function one   "#x0000000000000001"
+  syntax function ones  "#xFFFFFFFFFFFFFFFF"
+  syntax function size_bv "(_ bv64 64)"
+
+  syntax predicate is_signed_positive "(bvsge %1 (_ bv0 64))"
+
+  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
+  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
+end
+
+theory bv.BV32
+  meta "literal:keep" type t
+
+  syntax literal t "#x%8x"
+  syntax type t "(_ BitVec 32)"
+
+  syntax function zeros "#x00000000"
+  syntax function one   "#x00000001"
+  syntax function ones  "#xFFFFFFFF"
+  syntax function size_bv "(_ bv32 32)"
+
+  syntax predicate is_signed_positive "(bvsge %1 (_ bv0 32))"
+
+  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
+  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
+end
+
+theory bv.BV16
+  meta "literal:keep" type t
+
+  syntax literal t "#x%4x"
+  syntax type t "(_ BitVec 16)"
+
+  syntax function zeros "#x0000"
+  syntax function one   "#x0001"
+  syntax function ones  "#xFFFF"
+  syntax function size_bv "(_ bv16 16)"
+
+  syntax predicate is_signed_positive "(bvsge %1 (_ bv0 16))"
+
+  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
+  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
+end
+
+theory bv.BV8
+  meta "literal:keep" type t
+
+  syntax literal t (* "#b%8b"  *) "#x%2x"
+  syntax type t "(_ BitVec 8)"
+
+  syntax function zeros "#x00"
+  syntax function one   "#x01"
+  syntax function ones  "#xFF"
+  syntax function size_bv "(_ bv8 8)"
+
+  syntax predicate is_signed_positive "(bvsge %1 (_ bv0 8))"
+
+  syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
+  syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
+end
+
+theory bv.BVConverter_Gen
+  remove allprops
+end
+
+theory bv.BVConverter_128_256
+  syntax function toBig "((_ zero_extend 128) %1)"
+  syntax function stoBig "((_ sign_extend 128) %1)"
+  syntax function toSmall "((_ extract 127 0) %1)"
+end
+
+theory bv.BVConverter_64_128
+  syntax function toBig "((_ zero_extend 64) %1)"
+  syntax function stoBig "((_ sign_extend 64) %1)"
+  syntax function toSmall "((_ extract 63 0) %1)"
+end
+
+theory bv.BVConverter_32_128
+  syntax function toBig "((_ zero_extend 96) %1)"
+  syntax function stoBig "((_ sign_extend 96) %1)"
+  syntax function toSmall "((_ extract 31 0) %1)"
+end
+
+theory bv.BVConverter_16_128
+  syntax function toBig "((_ zero_extend 112) %1)"
+  syntax function stoBig "((_ sign_extend 112) %1)"
+  syntax function toSmall "((_ extract 15 0) %1)"
+end
+
+theory bv.BVConverter_8_128
+  syntax function toBig "((_ zero_extend 120) %1)"
+  syntax function stoBig "((_ sign_extend 120) %1)"
+  syntax function toSmall "((_ extract 7 0) %1)"
+end
+
+theory bv.BVConverter_32_64
+  syntax function toBig "((_ zero_extend 32) %1)"
+  syntax function stoBig "((_ sign_extend 32) %1)"
+  syntax function toSmall "((_ extract 31 0) %1)"
+end
+
+theory bv.BVConverter_16_64
+  syntax function toBig "((_ zero_extend 48) %1)"
+  syntax function stoBig "((_ sign_extend 48) %1)"
+  syntax function toSmall "((_ extract 15 0) %1)"
+end
+
+theory bv.BVConverter_8_64
+  syntax function toBig "((_ zero_extend 56) %1)"
+  syntax function stoBig "((_ sign_extend 56) %1)"
+  syntax function toSmall "((_ extract 7 0) %1)"
+end
+
+theory bv.BVConverter_16_32
+  syntax function toBig "((_ zero_extend 16) %1)"
+  syntax function stoBig "((_ sign_extend 16) %1)"
+  syntax function toSmall "((_ extract 15 0) %1)"
+end
+
+theory bv.BVConverter_8_32
+  syntax function toBig "((_ zero_extend 24) %1)"
+  syntax function stoBig "((_ sign_extend 24) %1)"
+  syntax function toSmall "((_ extract 7 0) %1)"
+end
+
+theory bv.BVConverter_8_16
+  syntax function toBig "((_ zero_extend 8) %1)"
+  syntax function stoBig "((_ sign_extend 8) %1)"
+  syntax function toSmall "((_ extract 7 0) %1)"
+end
+
+theory bv.Pow2int
+  remove allprops
+end

config/drivers/smt-libv2-floats.gen

+theory ieee_float.RoundingMode
+   syntax type mode "RoundingMode"
+   syntax function RNE "RNE"
+   syntax function RNA "RNA"
+   syntax function RTP "RTP"
+   syntax function RTN "RTN"
+   syntax function RTZ "RTZ"
+
+   syntax predicate to_nearest "(or (= %1 RNE) (= %1 RNA))"
+end
+
+theory ieee_float.GenericFloat
+   (* Part I *)
+   syntax function abs  "(fp.abs %1)"
+   syntax function neg  "(fp.neg %1)"
+
+   syntax function add  "(fp.add %1 %2 %3)"
+   syntax function sub  "(fp.sub %1 %2 %3)"
+   syntax function mul  "(fp.mul %1 %2 %3)"
+   syntax function div  "(fp.div %1 %2 %3)"
+
+   syntax function fma  "(fp.fma %1 %2 %3 %4)"
+
+   syntax function sqrt "(fp.sqrt %1 %2)"
+
+   syntax function roundToIntegral "(fp.roundToIntegral %1 %2)"
+
+   syntax function min "(fp.min %1 %2)"
+   syntax function max "(fp.max %1 %2)"
+
+   syntax predicate le  "(fp.leq %1 %2)"
+   syntax predicate lt  "(fp.lt %1 %2)"
+   syntax predicate ge  "(fp.geq %1 %2)"
+   syntax predicate gt  "(fp.gt %1 %2)"
+
+   syntax predicate eq  "(fp.eq %1 %2)"
+
+   syntax predicate is_normal    "(fp.isNormal %1)"
+   syntax predicate is_subnormal "(fp.isSubnormal %1)"
+   syntax predicate is_zero      "(fp.isZero %1)"
+   syntax predicate is_infinite  "(fp.isInfinite %1)"
+   syntax predicate is_nan       "(fp.isNaN %1)"
+   syntax predicate is_positive  "(fp.isPositive %1)"
+   syntax predicate is_negative  "(fp.isNegative %1)"
+
+   (* We could do this here, but we get slightly slimmer VCs and avoid
+      issues with Z3 if we do specialised versions of this for Float32 and
+      Float64 *)
+   (* The proposed fp.isFinite would fix all this. *)
+   (* syntax predicate is_finite "(not (or (fp.isInfinite %1) (fp.isNaN %1)))" *)
+   syntax predicate is_not_nan "(not (fp.isNaN %1))"
+
+   syntax function to_real  "(fp.to_real %1)"
+
+   syntax predicate overflow_value "true"
+
+   syntax predicate sign_zero_result "true"
+
+   (* Part II *)
+
+   remove allprops
+end
+
+theory ieee_float.Float32
+  (* Part I *)
+  syntax type t "Float32"
+  meta "literal:keep" type t
+  syntax literal t "(fp #b%s1b #b%e8b #b%m23b)"
+
+  syntax function zeroF     "((_ to_fp 8 24) #x00000000)"
+
+  prelude "(define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))"
+  prelude "(define-fun fp.isIntegral32 ((x Float32)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))"
+
+
+  syntax predicate t'isFinite "(fp.isFinite32 %1)"
+  syntax predicate is_int "(fp.isIntegral32 %1)"
+
+  (* Faithful translations of the axiomatisation, mainly to remove this crud
+     from the smtlib output of SPARK. *)
+  syntax function round "(fp.to_real ((_ to_fp 8 24) %1 %2))"
+
+ syntax predicate in_range "\
+   (and (<= (fp.to_real (fp #b1 #b11111110 #b11111111111111111111111)) %1) \
+        (<= %1 (fp.to_real (fp #b0 #b11111110 #b11111111111111111111111))))"
+
+  syntax predicate no_overflow "\
+   (and (<= (fp.to_real (fp #b1 #b11111110 #b11111111111111111111111)) \
+            (fp.to_real ((_ to_fp 8 24) %1 %2))) \
+        (<= (fp.to_real ((_ to_fp 8 24) %1 %2)) \
+            (fp.to_real (fp #b0 #b11111110 #b11111111111111111111111))))"
+
+  remove allprops
+end
+
+theory ieee_float.Float64
+  (* Part I *)
+  syntax type t "Float64"
+  meta "literal:keep" type t
+  syntax literal t "(fp #b%s1b #b%e11b #b%m52b)"
+
+  syntax function zeroF     "((_ to_fp 11 53) #x0000000000000000)"
+
+  prelude "(define-fun fp.isFinite64 ((x Float64)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))"
+  prelude "(define-fun fp.isIntegral64 ((x Float64)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))"
+
+  syntax predicate t'isFinite "(fp.isFinite64 %1)"
+  syntax predicate is_int "(fp.isIntegral64 %1)"
+
+  (* Faithful translations of the axiomatisation, mainly to remove this crud
+     from the smtlib output of SPARK. *)
+  syntax function round "(fp.to_real ((_ to_fp 11 53) %1 %2))"
+
+  syntax predicate in_range "\
+   (and \
+    (<= \
+     (fp.to_real (fp #b1 #b11111111110 #b1111111111111111111111111111111111111111111111111111)) \
+     %1) \
+    (<= %1 \
+     (fp.to_real (fp #b0 #b11111111110 #b1111111111111111111111111111111111111111111111111111))))"
+
+  syntax predicate no_overflow "\
+   (and \
+    (<= \
+     (fp.to_real (fp #b1 #b11111111110 #b1111111111111111111111111111111111111111111111111111)) \
+     (fp.to_real ((_ to_fp 11 53) %1 %2))) \
+    (<= \
+     (fp.to_real ((_ to_fp 11 53) %1 %2)) \
+     (fp.to_real (fp #b0 #b11111111110 #b1111111111111111111111111111111111111111111111111111))))"
+
+  remove allprops
+end
+
+theory ieee_float.FloatConverter
+  (* Part I *)
+   syntax function to_float32 "((_ to_fp 8 24) %1 %2)"
+   syntax function to_float64 "((_ to_fp 11 53) %1 %2)"
+
+   remove allprops
+end
+
+theory ieee_float.Float_BV_Converter
+  (* Part I *)
+   syntax function to_ubv8  "((_ fp.to_ubv 8) %1 %2)"
+   syntax function to_ubv16 "((_ fp.to_ubv 16) %1 %2)"
+   syntax function to_ubv32 "((_ fp.to_ubv 32) %1 %2)"
+   syntax function to_ubv64 "((_ fp.to_ubv 64) %1 %2)"
+
+   remove allprops
+end
+
+theory ieee_float.Float32_BV_Converter
+  (* Part I *)
+  syntax function of_ubv8  "((_ to_fp_unsigned 8 24) %1 %2)"
+  syntax function of_ubv16 "((_ to_fp_unsigned 8 24) %1 %2)"
+  syntax function of_ubv32 "((_ to_fp_unsigned 8 24) %1 %2)"
+  syntax function of_ubv64 "((_ to_fp_unsigned 8 24) %1 %2)"
+
+  remove allprops
+end
+
+theory ieee_float.Float64_BV_Converter
+  (* Part I *)
+  syntax function of_ubv8  "((_ to_fp_unsigned 11 53) %1 %2)"
+  syntax function of_ubv16 "((_ to_fp_unsigned 11 53) %1 %2)"
+  syntax function of_ubv32 "((_ to_fp_unsigned 11 53) %1 %2)"
+  syntax function of_ubv64 "((_ to_fp_unsigned 11 53) %1 %2)"
+
+  remove allprops
+end

config/drivers/smt-libv2.gen

+(* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
+
+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
+
+*)
+
+filename "%f-%t-%g.smt2"
+unknown "^\\(unknown\\|sat\\|Fail\\)$" "\\1"
+unknown "^(:reason-unknown \\([^)]*\\))$" "\\1"
+time "why3cpulimit time : %s s"
+valid "^unsat$"
+
+theory BuiltIn
+  syntax type int   "Int"
+  syntax type real  "Real"
+  syntax predicate (=)  "(= %1 %2)"
+
+  meta "encoding:kept" type int
+  meta "encoding:ignore_polymorphism_ls" predicate (=)
+end
+
+theory int.Int
+
+  prelude ";;; SMT-LIB2: 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 MulComm.Comm
+  remove prop MulAssoc.Assoc
+  remove prop Unit_def_l
+  remove prop Unit_def_r
+  remove prop Inv_def_l
+  remove prop Inv_def_r
+  remove prop Assoc
+  remove prop Mul_distr_l
+  remove prop Mul_distr_r
+  remove prop 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 ";;; SMT-LIB2: 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 MulComm.Comm
+  remove prop MulAssoc.Assoc
+  remove prop Unit_def_l
+  remove prop Unit_def_r
+  remove prop Inv_def_l
+  remove prop Inv_def_r
+  remove prop Assoc
+  remove prop Mul_distr_l
+  remove prop Mul_distr_r
+  remove prop 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 real.Abs
+  syntax function abs "(ite (>= %1 0.0) %1 (- %1))"
+
+  remove allprops
+end
+
+theory real.MinMax
+
+  remove allprops
+end
+
+theory real.FromInt
+  syntax function from_int "(to_real %1)"
+
+  remove allprops
+end
+
+theory real.Truncate
+  syntax function truncate "(ite (>= %1 0.0) \
+                                 (to_int %1) \
+                                 (- (to_int (- %1))))"
+  syntax function floor "(to_int %1)"
+  syntax function ceil "(- (to_int (- %1)))"
+
+  remove allprops
+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)"
+  syntax function implb "(=> %1 %2)"
+end
+
+theory bool.Ite
+  syntax function ite "(ite %1 %2 %3)"
+  meta "encoding:lskept" function ite
+  meta "encoding:ignore_polymorphism_ls" function ite
+end
+
+(* not uniformly interpreted by provers
+theory real.Truncate
+  syntax function floor "(to_int %1)"
+  remove prop Floor_down
+  remove prop Floor_monotonic
+end
+*)
+
+theory HighOrd
+  syntax type     (->) "(Array %1 %2)"
+  syntax function (@)  "(select %1 %2)"
+
+  meta "encoding:lskept" function (@)
+  meta "encoding:ignore_polymorphism_ts" type (->)
+  meta "encoding:ignore_polymorphism_ls" function (@)
+end
+
+theory map.Map
+  syntax function get "(select %1 %2)"
+  syntax function set "(store %1 %2 %3)"
+
+  meta "encoding:lskept" function get
+  meta "encoding:lskept" function set
+  meta "encoding:ignore_polymorphism_ls" function get
+  meta "encoding:ignore_polymorphism_ls" function ([])
+  meta "encoding:ignore_polymorphism_ls" function set
+  meta "encoding:ignore_polymorphism_ls" function ([<-])
+end
+
+theory map.Const
+  meta "encoding:lskept" function const
+(*  syntax function const "(const[%t0] %1)" *)
+end

config/dune

@@ -6,5 +6,13 @@
   caisar-detection-data.conf
   (drivers/pyrat.drv as drivers/pyrat.drv)
   (drivers/marabou.drv as drivers/marabou.drv)
-  (drivers/saver.drv as drivers/saver.drv))
+  (drivers/saver.drv as drivers/saver.drv)
+  (drivers/cvc5.drv as drivers/cvc5.drv)
+  (drivers/cvc4_16.gen as drivers/cvc4_16.gen)
+  (drivers/cvc4_bv.gen as drivers/cvc4_bv.gen)
+  (drivers/smt-libv2-bv.gen as drivers/smt-libv2-bv.gen)
+  (drivers/smt-libv2-floats.gen as drivers/smt-libv2-floats.gen)
+  (drivers/smt-libv2.gen as drivers/smt-libv2.gen)
+  (drivers/discrimination.gen as drivers/discrimination.gen)
+  )
  (package caisar))

src/main.ml

@@ -27,9 +27,8 @@ let caisar = "caisar"
 
 let () =
   Native_nn_prover.init ();
-  Vars_on_lhs.init ();
-  Actual_net_apply.init ()
-  
+  Actual_net_apply.init ();
+  Vars_on_lhs.init ()
 
 let () =
   Pyrat.init ();
@@ -231,3 +230,4 @@ let () =
     |> Cmd.eval ~catch:false |> Caml.exit
   with exn when not (log_level_is_debug ()) ->
     Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)
+

src/prover.ml

@@ -20,9 +20,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type t = Marabou | Pyrat | Saver
+type t = Marabou | Pyrat | Saver | CVC5
 
-let list_available () = [ Marabou; Pyrat; Saver ]
+let list_available () = [ Marabou; Pyrat; Saver ; CVC5]
 
 let of_string prover =
   let prover = String.lowercase_ascii prover in
@@ -30,9 +30,11 @@ let of_string prover =
   | "marabou" -> Some Marabou
   | "pyrat" -> Some Pyrat
   | "saver" -> Some Saver
+  | "cvc5" -> Some CVC5
   | _ -> None
 
 let to_string = function
   | Marabou -> "Marabou"
   | Pyrat -> "PyRAT"
   | Saver -> "SAVer"
+  | CVC5 -> "CVC5"

tests/autodetect.t

@@ -4,7 +4,7 @@ Test autodetect
   > echo "2.4.0"
   > EOF
 
-  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver
+  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver bin/cvc5
 
   $ bin/alt-ergo
   2.4.0
@@ -18,11 +18,15 @@ Test autodetect
   $ bin/saver --version
   v1.0
 
+  $ bin/cvc5 --version
+  This is cvc5 version 1.0.2 [git tag 1.0.2 branch HEAD]
+
   $ PATH=$(pwd)/bin:$PATH
 
   $ caisar config -d -vv 2>&1 | ./filter_tmpdir.sh
   [caisar][DEBUG] Command `config'
   [caisar][DEBUG] Automatic detection
+  <autodetect>Run: ($TESTCASE_ROOT/bin/cvc5 --version 2>&1 | head -1) > $TMPFILE 2>&1
   <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
   <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
   <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
@@ -30,11 +34,13 @@ Test autodetect
   <autodetect>0 prover(s) added
   <autodetect>Generating strategies:
   <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
+  <autodetect>Found prover CVC5 version 1.0.2, OK.
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.1, OK.
   <autodetect>Found prover SAVer version v1.0, OK.
-  <autodetect>4 prover(s) added
+  <autodetect>5 prover(s) added
   [caisar] Alt-Ergo 2.4.0
+           CVC5 1.0.2
            Marabou 1.0.+
            PyRAT 1.1
            SAVer v1.0

tests/bin/cvc5

+#!/bin/sh -e
+
+
+case $1 in
+    --version)
+        echo "This is cvc5 version 1.0.2 [git tag 1.0.2 branch HEAD]"
+        ;;
+    *)
+        echo "PWD: $(pwd)"
+        echo "NN: $1"
+        test -e $1 || (echo "Cannot find the NN file" && exit 1)
+        echo "Goal:"
+        cat $2
+        echo "Unknown"
+esac

tests/dune

@@ -7,5 +7,6 @@
   bin/pyrat.py
   bin/Marabou
   bin/saver
+  bin/cvc5
   filter_tmpdir.sh)
  (package caisar))

tests/simple_cvc5.t

+Test verify
+  $ cat - > bin/alt-ergo << EOF
+  > #!/bin/sh
+  > echo "2.4.0"
+  > EOF
+
+  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver bin/cvc5
+
+  $ bin/alt-ergo
+  2.4.0
+
+  $ bin/pyrat.py --version
+  PyRAT 1.1
+
+  $ bin/Marabou --version
+  1.0.+
+
+  $ bin/saver --version
+  v1.0
+
+  $ PATH=$(pwd)/bin:$PATH
+
+  $ caisar verify -L . --format whyml --prover=CVC5 - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9_./]*/$TMPFILE/'
+  > theory T
+  >   use TestNetworkONNX.NNasTuple
+  >   use ieee_float.Float64
+  >   use caisar.NN
+  > 
+  >   goal G: forall x1 x2 x3.
+  >      (0.0:t) .< x1 .< (0.5:t) ->
+  >      let (y1,y2) = net_apply x1 x2 x3 in
+  >      (0.0:t) .< y1 .< (0.5:t) /\ (0.0:t) .< y2 .< (1.0:t)
+  > end
+  > EOF
+  [caisar] Goal G: High failure