update sessions

drivers/c.drv

@@ -25,7 +25,7 @@ module mach.int.Int32
   syntax type int32  "int32_t"
   syntax literal int32 "0x%8x"
 
-(*  syntax val of_int "(int32_t)%1" *)
+  syntax val of_int "(int32_t)(%1)"
   syntax val (+)     "%1 + %2"
   syntax val (-)     "%1 - %2"
   syntax val (-_)    "-%1"
@@ -51,8 +51,6 @@ end
 module mach.int.UInt32
 
   syntax literal uint32 "0x%8xU"
-  (* syntax converter of_int "%1U" *)
-
 
   syntax val (+)     "%1 + %2"
   syntax val (-)     "%1 - %2"
@@ -184,7 +182,6 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt);
 "
 
   syntax literal uint32 "0x%8xU"
-  (* syntax converter of_int "%1U" *)
 
   syntax val (+)     "%1 + %2"
   syntax val (-)     "%1 - %2"
@@ -226,7 +223,7 @@ module mach.int.Int64
   syntax type int64  "int64_t"
   syntax literal int64 "0x%16xLL"
 
-(*  syntax val of_int "(int64_t)%1" *)
+  syntax val of_int "(int64_t)(%1)"
   syntax val (+)     "%1 + %2"
   syntax val (-)     "%1 - %2"
   syntax val (-_)    "-%1"
@@ -252,7 +249,6 @@ end
 module mach.int.UInt64
 
   syntax literal uint64 "0x%16xULL"
-  (* syntax converter of_int "%1ULL" *)
 
   syntax val (+)     "%1 + %2"
   syntax val (-)     "%1 - %2"
@@ -508,7 +504,6 @@ static struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
 }
 "
   syntax literal uint64 "0x%16xULL"
-  (* syntax converter of_int "%1ULL" *)
 
   syntax val uint64_max "0xffffffffffffffffULL"
 

drivers/cvc4_bv.gen

@@ -6,21 +6,26 @@ theory bv.BV_Gen
 end
 
 theory bv.BV64
-  (*syntax converter of_int "((_ int2bv 64) %1)"*)
+  (* 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 64) %1)" *)
   syntax function t'int "(bv2nat %1)"
 end
 
 theory bv.BV32
-  (*syntax converter of_int "((_ int2bv 32) %1)"*)
+  (* syntax function of_int "((_ int2bv 32) %1)" *)
   syntax function t'int "(bv2nat %1)"
 end
 
 theory bv.BV16
-  (*syntax converter of_int "((_ int2bv 16) %1)"*)
+  (* syntax function of_int "((_ int2bv 16) %1)" *)
   syntax function t'int "(bv2nat %1)"
 end
 
 theory bv.BV8
-  (*syntax converter of_int "((_ int2bv 8) %1)"*)
+  (* syntax function of_int "((_ int2bv 8) %1)" *)
   syntax function t'int "(bv2nat %1)"
 end

drivers/z3_bv.gen

@@ -6,7 +6,10 @@ theory bv.BV_Gen
 end
 
 theory bv.BV64
-  (* syntax converter of_int "((_ int2bv 64) %1)" *)
+  (* mapping of_int to int2bv is disabled because it breaks proofs
+     in examples/queens_bv, examples/bitwalker *)
+
+  (* syntax function of_int "((_ int2bv 64) %1)" *)
   syntax function t'int "(bv2int %1)"
 
   remove prop Nth_bv_is_nth
@@ -14,7 +17,7 @@ theory bv.BV64
 end
 
 theory bv.BV32
-  (* syntax converter of_int "((_ int2bv 32) %1)" *)
+  (* syntax function of_int "((_ int2bv 32) %1)" *)
   syntax function t'int "(bv2int %1)"
 
   remove prop Nth_bv_is_nth
@@ -22,7 +25,7 @@ theory bv.BV32
 end
 
 theory bv.BV16
-  (* syntax converter of_int "((_ int2bv 16) %1)" *)
+  (* syntax function of_int "((_ int2bv 16) %1)" *)
   syntax function t'int "(bv2int %1)"
 
   remove prop Nth_bv_is_nth
@@ -30,7 +33,7 @@ theory bv.BV16
 end
 
 theory bv.BV8
-  (* syntax converter of_int "((_ int2bv 8) %1)" *)
+  (* syntax function of_int "((_ int2bv 8) %1)" *)
   syntax function t'int "(bv2int %1)"
 
   remove prop Nth_bv_is_nth

examples/logic/bitvectors.why

@@ -3,18 +3,18 @@ theory TestBV
   use int.Int
   use bv.BV32
 
-  constant b0000  : t = of_int 0b0000
-  constant b0001  : t = of_int 0b0001
-  constant b0010  : t = of_int 0b0010
-  constant b0011  : t = of_int 0b0011
-  constant b0110  : t = of_int 0b0110
-  constant b0101  : t = of_int 0b0101
-  constant b0111  : t = of_int 0b0111
-  constant b1100  : t = of_int 0b1100
-  constant b11100 : t = of_int 0b11100
-
-  constant bv2    : t = of_int 2
-  constant bv31   : t = of_int 31
+  constant b0000  : t = (0b0000:t)
+  constant b0001  : t = (0b0001:t)
+  constant b0010  : t = (0b0010:t)
+  constant b0011  : t = (0b0011:t)
+  constant b0110  : t = (0b0110:t)
+  constant b0101  : t = (0b0101:t)
+  constant b0111  : t = (0b0111:t)
+  constant b1100  : t = (0b1100:t)
+  constant b11100 : t = (0b11100:t)
+
+  constant bv2    : t = (2:t)
+  constant bv31   : t = (31:t)
 
   goal g1 : bw_and b0011 b0110 = b0010
   goal f1 : bw_and b0011 b0110 = b0011
@@ -23,21 +23,21 @@ theory TestBV
   goal f2 :  bw_or b0011 b0110 = b0110
 
   goal g3 :  bw_xor b0011 b0110 = b0101
-  goal g4 :  bw_not b0011 = (of_int 0xFFFFFFFC)
+  goal g4 :  bw_not b0011 = (0xFFFFFFFC:t)
 
   goal g3a : lsr_bv b0111 bv2 = b0001
   goal g3b : lsr_bv ones bv31 = b0001
-  goal f3c : lsr_bv ones (of_int 0x10000001) = (of_int 0x7FFFFFFF) (* should be false: we don't take the modulo of the second argument. *)
+  goal f3c : lsr_bv ones (0x10000001:t) = (0x7FFFFFFF:t) (* should be false: we don't take the modulo of the second argument. *)
 
   goal g3aa : lsr b0111 2 = b0001
   goal g3bb : lsr ones 31 = b0001
-  goal f3cc : lsr ones 0x10000001 = (of_int 0x7FFFFFFF) (* should be false: we don't take the modulo of the second argument. *)
+  goal f3cc : lsr ones 0x10000001 = (0x7FFFFFFF:t) (* should be false: we don't take the modulo of the second argument. *)
 
   goal g4a : lsl_bv b0111 bv2 = b11100
-  goal g4b : lsl_bv b0001 bv31 = (of_int 0x80000000)
+  goal g4b : lsl_bv b0001 bv31 = (0x80000000:t)
 
   goal g4aa : lsl b0111 2 = b11100
-  goal g4bb : lsl b0001 31 = (of_int 0x80000000)
+  goal g4bb : lsl b0001 31 = (0x80000000:t)
 
   goal g5a : asr_bv b0111 bv2 = b0001
   goal g5b : asr_bv ones bv31 = ones
@@ -52,13 +52,13 @@ theory TestBV
   goal g7b : to_int ones = -1
 
   goal g8a : nth_bv b0110 bv2 = True
-  goal g8b : nth_bv b0110 (of_int 3) = False
+  goal g8b : nth_bv b0110 (3:t) = False
 
   goal g8aa : nth b0110 2 = True
   goal g8bb : nth b0110 3 = False
 
-  goal gtt : t'int (lsl_bv (of_int 3) (of_int 30)) > 0 (* = 0xC0000000 *)
-  goal gttt : t'int (lsl (of_int 3) 30) > 0 (* = 0xC0000000 *)
+  goal gtt : t'int (lsl_bv (3:t) (30:t)) > 0 (* = 0xC0000000 *)
+  goal gttt : t'int (lsl (3:t) 30) > 0 (* = 0xC0000000 *)
 
   goal not_not : forall v:t. bw_not (bw_not v) = v
 

examples/logic/bitvectors/why3session.xml

@@ -62,12 +62,12 @@
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
  <goal name="g4a" proved="true">
- <proof prover="1" timelimit="5"><result status="valid" time="0.02" steps="106"/></proof>
+ <proof prover="1" timelimit="5"><result status="valid" time="0.02" steps="100"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="g4b" proved="true">
- <proof prover="1" timelimit="5"><result status="valid" time="0.06" steps="106"/></proof>
+ <proof prover="1" timelimit="5"><result status="valid" time="0.06" steps="100"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
  </goal>
@@ -100,7 +100,7 @@
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
  <goal name="g6a" proved="true">
- <proof prover="1" timelimit="5"><result status="valid" time="0.03" steps="74"/></proof>
+ <proof prover="1" timelimit="5"><result status="valid" time="0.03" steps="71"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
  </goal>
@@ -127,16 +127,16 @@
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
  </goal>
- <goal name="g8aa">
+ <goal name="g8aa" proved="true">
  <proof prover="1"><result status="timeout" time="1.00"/></proof>
- <proof prover="2" timelimit="1"><result status="timeout" time="1.00"/></proof>
+ <proof prover="2" timelimit="1"><result status="valid" time="0.02"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
  <goal name="g8bb" proved="true">
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="gtt" proved="true">
- <proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="78"/></proof>
+ <proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="73"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
  </goal>