Adding mathematical functions (+ - / *...) and comparison predicates to the...

Adding mathematical functions (+ - / *...) and comparison predicates to the theory of bit-vector and cvc4 driver (based on smt2-lib theory of bit-vector).

drivers/cvc4_bare.drv

@@ -193,24 +193,56 @@ theory bv.BV32
   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 sdiv "(bvsdiv %1 %2)"
+  syntax function srem "(bvsrem %1 %2)"
+  syntax function smod "(bvsmod %1 %2)"
+
+  syntax function rotate_left "((_ rotate_left 1) %1)"
+  syntax function rotate_right "((_ rotate_right 1) %1)"
+
   syntax function lsr "(bvlshr %1 ((_ int2bv 32) %2))"
   syntax function lsl "(bvshl %1 ((_ int2bv 32) %2))"
   syntax function asr "(bvashr %1 ((_ int2bv 32) %2))"
+  syntax function lsr_bv "(bvlshr %1 %2)"
+  syntax function lsl_bv "(bvshl %1 %2)"
+  syntax function asr_bv "(bvashr %1 %2)"
   syntax function to_uint "(bv2nat %1)"
   syntax function to_int "(ite (= ((_ extract 31 31) %1) #b0)
   	 	  	       (bv2nat %1)
 			       (- (bv2nat %1) 4294967296))"
   syntax function of_int "((_ int2bv 32) %1)"
-  syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2)))
-  	 	      	  #b1)"
+  syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)"
+  syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)"
   syntax predicate eq "(= %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)"
+  syntax predicate ult "(bvult %1 %2)"
+  syntax predicate ule "(bvule %1 %2)"
+  syntax predicate ugt "(bvugt %1 %2)"
+  syntax predicate uge "(bvuge %1 %2)"
+
   remove prop Nth_zero
   remove prop Nth_ones
   remove prop Nth_bw_and
   remove prop Nth_bw_or
   remove prop Nth_bw_xor
   remove prop Nth_bw_not
+
+  (* remove prop Add_is_add *)
+  (* remove prop Min_is_min *)
+  (* remove prop Neg_is_neg *)
+  (* remove prop Mul_is_mul *)
+  (* remove prop Udiv_is_udiv *)
+
   remove prop Lsr_nth_low
   remove prop Lsr_nth_high
   remove prop Lsl_nth_low

theories/bv.why

@@ -19,6 +19,8 @@ theory BitVector
   (** [nth b n] is the n-th bit of x (0 <= n < size). bit 0 is
       the least significant bit *)
 
+  function nth_bv t t : bool
+
   predicate eq (v1 v2 : t) =
     forall n:int. 0 <= n < size -> nth v1 n = nth v2 n
 
@@ -52,6 +54,9 @@ theory BitVector
     forall v:t, n:int. 0 <= n < size ->
       nth (bw_not v) n = notb (nth v n)
 
+  function rotate_left (v : t) : t
+
+  function rotate_right (v : t) : t
 
   (** logical shift right *)
   function lsr t int : t
@@ -64,6 +69,8 @@ theory BitVector
     forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s >= size -> 
       nth (lsr b s) n = False
 
+  function lsr_bv t t : t
+
   (** arithmetic shift right *)
   function asr t int : t
 
@@ -73,6 +80,8 @@ theory BitVector
   axiom Asr_nth_high:
     forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n+s >= size -> nth (asr b s) n = nth b (size-1)
 
+  function asr_bv t t : t
+
   (** logical shift left *)
   function lsl t int : t
 
@@ -82,6 +91,8 @@ theory BitVector
   axiom Lsl_nth_low:
     forall b:t,n s:int. 0 <= s < size -> 0 <= n < size -> n-s < 0 -> nth (lsl b s) n = False
 
+  function lsl_bv t t : t
+
   (** conversion to unsigned integers *)
   function to_uint t: int
 
@@ -96,8 +107,82 @@ theory BitVector
   representation of the argument is truncated to [size] bits *)
   function of_int int: t
 
+  constant one : t = of_int 1
+
   (* TODO? axioms related to_int/to_unit and of_int *)
 
+  use import int.Power
+  use import int.EuclideanDivision
+
+  (** addition modulo 2^m *) 
+  function add (v1 v2 : t) : t
+  (* axiom Add_is_add: *)
+  (*   forall v1 v2:t. add v1 v2 = of_int( mod (to_int (v1) + to_int (v2)) (power 2 32)) *)
+  
+  (** 2's complement subtraction modulo 2^m *)
+  function sub (v1 v2 : t) : t
+  (* axiom Min_is_min: *)
+  (*   forall v1 v2:t. sub v1 v2 = of_int( mod (to_int (v1) - to_int (v2)) (power 2 32)) *)
+      
+  (** 2's complement unary minus *)
+  function neg (v1 : t) : t
+  (* axiom Neg_is_neg: *)
+  (*   forall v:t. neg v = of_int( mod (-to_int (v)) (power 2 32)) *)
+  
+  (** multiplication modulo 2^m *)	
+  function mul (v1 v2 : t) : t
+  (* axiom Mul_is_mul: *)
+  (*   forall v1 v2:t. mul v1 v2 = of_int( mod (to_int (v1) * to_int (v2)) (power 2 32)) *)
+
+  (** unsigned division, truncating towards 0 (undefined if divisor is 0) *)  
+  function udiv (v1 v2 : t) : t
+  (* axiom Udiv_is_udiv: *)
+  (*   forall v1 v2:t. udiv v1 v2 = of_int (to_uint (v1) / to_uint (v2)) *)
+
+  (** unsigned remainder from truncating division (undefined if divisor is 0) *)
+  function urem (v1 v2 : t) : t
+
+  (** 2's complement signed division *)
+  function sdiv (v1 v2 : t) : t
+
+  (** 2's complement signed remainder (sign follows dividend) *)
+  function srem (v1 v2 : t) : t
+
+  (** 2's complement signed remainder (sign follows divisor) *)
+  function smod (v1 v2 : t) : t
+
+  (** binary predicate for signed less than *)
+  predicate slt (v1 v2 : t) =
+    (to_int v1) < (to_int v2)
+
+  (** binary predicate for signed less than or equal *)
+  predicate sle (v1 v2 : t) =
+    (to_int v1) <= (to_int v2)
+
+  (**  binary predicate for signed greater than *)
+  predicate sgt (v1 v2 : t) =
+    (to_int v1) > (to_int v2)
+
+  (**  binary predicate for signed greater than or equal *)
+  predicate sge (v1 v2 : t) =
+    (to_int v1) >= (to_int v2)
+
+  (** binary predicate for unsigned less than *)
+  predicate ult (v1 v2 : t) =
+    (to_uint v1) < (to_uint v2)
+
+  (** binary predicate for unsigned less than or equal *)
+  predicate ule (v1 v2 : t) =
+    (to_uint v1) <= (to_uint v2)
+
+  (**  binary predicate for unsigned greater than *)
+  predicate ugt (v1 v2 : t) =
+    (to_uint v1) > (to_uint v2)
+
+  (**  binary predicate for unsigned greater than or equal *)
+  predicate uge (v1 v2 : t) =
+    (to_uint v1) >= (to_uint v2)
+
 end
 
 (** {2 31-bits Bitvectors} *)