feat(BV, CP): Propagators for addition and multiplication

This patch adds constraints to represent bit-vector addition and
multiplication, with propagators in the interval domain and a simple
propagator for multiplication that only considers the factors-of-two
multiples in the bit-vector domain (this information cannot be captured
by the interval domain due to imprecise handling of overflow).

No propagator for addition in the bit-vector domain is provided yet,
although the plan is to add a full-adder propagator to provide a limited
form of *local* bit-blasting, as suggested in

  S. Bardin, P. Herrmann, and F. Perroud.
  “An Alternative to SAT-Based Approaches for Bit-Vectors”.
  In: TACAS. 2010.

Author: bclement-ocp

src/lib/reasoners/bitlist.ml

@@ -49,7 +49,7 @@ let explanation { ex; _ } = ex
 
 let exact width value ex =
   { width
-  ; bits_set = value
+  ; bits_set = Z.extract value 0 width
   ; bits_clr = Z.extract (Z.lognot value) 0 width
   ; ex }
 
@@ -264,3 +264,39 @@ let fold_domain f b acc =
         (ofs + 1) { b with bits_set = Z.logor b.bits_set mask } acc
   in
   fold_domain_aux 0 b acc
+
+(* simple propagator: only compute known low bits *)
+let mul a b =
+  let sz = width a in
+  assert (width b = sz);
+
+  let ex = Ex.union (explanation a) (explanation b) in
+
+  (* (a * 2^n) * (b * 2^m) = (a * b) * 2^(n + m) *)
+  let zeroes_a = Z.trailing_zeros @@ Z.lognot a.bits_clr in
+  let zeroes_b = Z.trailing_zeros @@ Z.lognot b.bits_clr in
+  if zeroes_a + zeroes_b >= sz then
+    exact sz Z.zero ex
+  else
+    let low_bits =
+      if zeroes_a + zeroes_b = 0 then empty
+      else exact (zeroes_a + zeroes_b) Z.zero ex
+    in
+    let a = extract a zeroes_a (zeroes_a + sz - width low_bits - 1) in
+    assert (width a + width low_bits = sz);
+    let b = extract b zeroes_b (zeroes_b + sz - width low_bits - 1) in
+    assert (width b + width low_bits = sz);
+    (* ((ah * 2^n) + al) * ((bh * 2^m) + bl) =
+        al * bl  (mod 2^(min n m)) *)
+    let low_a_known = Z.trailing_zeros @@ Z.lognot @@ bits_known a in
+    let low_b_known = Z.trailing_zeros @@ Z.lognot @@ bits_known b in
+    let low_known = min low_a_known low_b_known in
+    let mid_bits =
+      if low_known = 0 then empty
+      else exact
+          low_known
+          Z.(extract (value a) 0 low_known * extract (value b) 0 low_known)
+          ex
+    in
+    concat (unknown (sz - width mid_bits - width low_bits) Ex.empty) @@
+    concat mid_bits low_bits

src/lib/reasoners/bitlist.mli

@@ -118,6 +118,9 @@ val logor : t -> t -> t
 val logxor : t -> t -> t
 (** Bitwise xor. *)
 
+val mul : t -> t -> t
+(** Multiplication. *)
+
 val concat : t -> t -> t
 (** Bit-vector concatenation. *)
 

src/lib/reasoners/bitv.ml

@@ -347,7 +347,10 @@ module Shostak(X : ALIEN) = struct
   let is_mine_symb sy =
     match sy with
     | Sy.Bitv _
-    | Op (Concat | Extract _ | BV2Nat | BVnot | BVand | BVor | BVxor)
+    | Op (
+        Concat | Extract _ | BV2Nat
+        | BVnot | BVand | BVor | BVxor
+        | BVadd | BVsub | BVmul)
       -> true
     | _ -> false
 
@@ -403,7 +406,10 @@ module Shostak(X : ALIEN) = struct
     let other ~neg t _sz ctx =
       let r, ctx' =
         match E.term_view t with
-        | { f = Op (BVand | BVor | BVxor); _ } ->
+        | { f = Op (
+            BVand | BVor | BVxor
+            | BVadd | BVsub | BVmul
+          ); _ } ->
           X.term_embed t, []
         | _ -> X.make t
       in