feat(BV, CP): Add propagators for bvudiv and bvurem

These are interval propagators only and respect the SMT-LIB semantics
for division by 0. This requires custom operators in the `Intervals`
module that update the bounds appropriately, sincethe existing `div`
operator is undefined on `0`.

src/lib/reasoners/bitv.ml

@@ -353,7 +353,7 @@ module Shostak(X : ALIEN) = struct
     | Op (
         Concat | Extract _ | BV2Nat
         | BVnot | BVand | BVor | BVxor
-        | BVadd | BVsub | BVmul)
+        | BVadd | BVsub | BVmul | BVudiv | BVurem)
       -> true
     | _ -> false
 
@@ -411,7 +411,7 @@ module Shostak(X : ALIEN) = struct
         match E.term_view t with
         | { f = Op (
             BVand | BVor | BVxor
-            | BVadd | BVsub | BVmul
+            | BVadd | BVsub | BVmul | BVudiv | BVurem
           ); _ } ->
           X.term_embed t, []
         | _ -> X.make t

src/lib/reasoners/bitv_rel.ml

@@ -246,6 +246,17 @@ module Constraint : sig
   val bvmul : X.r -> X.r -> X.r -> t
   (** [bvmul r x y] is the constraint [r = x * y] *)
 
+  val bvudiv : X.r -> X.r -> X.r -> t
+  (** [bvudir r x y] is the constraint [r = x / y]
+
+      This uses the convention that [x / 0] is [-1]. *)
+
+  val bvurem : X.r -> X.r -> X.r -> t
+  (** [bvurem r x y] is the constraint [r = x % y], where [x % y] is the
+      remainder of euclidean division.
+
+      This uses the convention that [x % 0] is [x]. *)
+
   val bvule : X.r -> X.r -> t
 
   val bvugt : X.r -> X.r -> t
@@ -262,21 +273,24 @@ end = struct
     (* Bitwise operations *)
     | Band | Bor | Bxor
     (* Arithmetic operations *)
-    | Badd | Bmul
+    | Badd | Bmul | Budiv | Burem
 
   let pp_binop ppf = function
     | Band -> Fmt.pf ppf "bvand"
     | Bor -> Fmt.pf ppf "bvor"
     | Bxor -> Fmt.pf ppf "bvxor"
     | Badd -> Fmt.pf ppf "bvadd"
     | Bmul -> Fmt.pf ppf "bvmul"
+    | Budiv -> Fmt.pf ppf "bvudiv"
+    | Burem -> Fmt.pf ppf "bvurem"
 
   let equal_binop : binop -> binop -> bool = Stdlib.(=)
 
   let hash_binop : binop -> int = Hashtbl.hash
 
   let is_commutative = function
     | Band | Bor | Bxor | Badd | Bmul -> true
+    | Budiv | Burem -> false
 
   let propagate_binop ~ex dx op dy dz =
     let open Domains.Ephemeral in
@@ -313,6 +327,12 @@ end = struct
     | Bmul -> (* Only forward propagation for now *)
       update ~ex dx (Bitlist.mul !!dy !!dz)
 
+    | Budiv -> (* No bitlist propagation for now *)
+      ()
+
+    | Burem -> (* No bitlist propagation for now *)
+      ()
+
   let propagate_interval_binop ~ex sz dr op dx dy =
     let open Interval_domains.Ephemeral in
     let norm i = Intervals.extract i 0 (sz - 1) in
@@ -325,6 +345,12 @@ end = struct
     | Bmul -> (* Only forward propagation for now *)
       update ~ex dr @@ norm @@ Intervals.mult !!dx !!dy
 
+    | Budiv -> (* Only forward propagation for now *)
+      update ~ex dr @@ Intervals.bvudiv sz !!dx !!dy
+
+    | Burem -> (* Only forward propagation for now *)
+      update ~ex dr @@ Intervals.bvurem !!dx !!dy
+
     | Band | Bor | Bxor ->
       (* No interval propagation for bitwise operators yet *)
       ()
@@ -529,6 +555,8 @@ end = struct
     (* r = x - y <-> x = r + y *)
     bvadd x r y
   let bvmul = cbinop Bmul
+  let bvudiv = cbinop Budiv
+  let bvurem = cbinop Burem
 
   let crel r = hcons @@ Crel r
 
@@ -692,6 +720,16 @@ end = struct
     | Bxor -> cast ty @@ Z.logxor x y
     | Badd -> cast ty @@ Z.add x y
     | Bmul -> cast ty @@ Z.mul x y
+    | Budiv ->
+      if Z.equal y Z.zero then
+        cast ty Z.minus_one
+      else
+        cast ty @@ Z.div x y
+    | Burem ->
+      if Z.equal y Z.zero then
+        cast ty x
+      else
+        cast ty @@ Z.rem x y
 
   (* Constant simplification rules for binary operators.
 
@@ -736,6 +774,8 @@ end = struct
       add_mul_const acts r x (value y)
     | Bmul -> false
 
+    | Budiv | Burem -> false
+
   (* Algebraic rewrite rules for binary operators.
 
      Rules based on constant simplifications are in [rw_binop_const]. *)
@@ -805,6 +845,8 @@ let extract_binop =
     | BVadd -> Some bvadd
     | BVsub -> Some bvsub
     | BVmul -> Some bvmul
+    | BVudiv -> Some bvudiv
+    | BVurem -> Some bvurem
     | _ -> None
 
 let extract_constraints bcs uf r t =

src/lib/reasoners/intervals.ml

@@ -1204,6 +1204,146 @@ let pick ~is_max { ints; is_int; _ } =
 (*   Bit-vector  *)
 (*****************)
 
+type 'a star = Neg_infinite | Finite of 'a | Pos_infinite
+
+let compare_star compare n1 n2 =
+  match n1, n2 with
+  | Neg_infinite, Neg_infinite -> 0
+  | Neg_infinite, (Finite _ | Pos_infinite) -> -1
+  | (Finite _ | Pos_infinite), Neg_infinite -> 1
+
+  | Finite n1, Finite n2 -> compare n1 n2
+  | Finite _, Pos_infinite -> -1
+  | Pos_infinite, Finite _ -> 1
+
+  | Pos_infinite, Pos_infinite -> 0
+
+let compare_zstar = compare_star Z.compare
+
+let is_zero_zstar = function
+  | Finite z when Z.equal z Z.zero -> true
+  | _ -> false
+
+let map_star f = function
+  | Neg_infinite -> Neg_infinite
+  | Finite n -> Finite (f n)
+  | Pos_infinite -> Pos_infinite
+
+let zstar_of_borne_inf lb =
+  match int_of_borne_inf lb with
+  | Large (lb, ex) -> Finite (Q.to_bigint lb), ex
+  | Minfty -> Neg_infinite, Ex.empty
+  | Strict _ | Pinfty -> assert false
+
+let zstar_of_borne_sup ub =
+  match int_of_borne_sup ub with
+  | Large (ub, ex) -> Finite (Q.to_bigint ub), ex
+  | Pinfty -> Pos_infinite, Ex.empty
+  | Strict _ | Minfty -> assert false
+
+let borne_of_zstar ~ex = function
+  | Neg_infinite -> Minfty
+  | Finite z -> Large (Q.of_bigint z, ex)
+  | Pos_infinite -> Pinfty
+
+let bvudiv_b a b =
+  match a, b with
+  | Large (a, ex_a), Large (b, ex_b) ->
+    assert (Q.compare b Q.zero > 0);
+    let a = Q.to_bigint a and b = Q.to_bigint b in
+    Large (Q.of_bigint @@ Z.div a b, Ex.union ex_a ex_b)
+  | _ -> assert false
+
+let bvudiv sz x y =
+  assert (x.is_int && y.is_int);
+  let mone = Q.of_bigint @@ Z.extract Z.minus_one 0 sz in
+  (* |-1| is always a valid upper bound *)
+  let mone_ub = Large (mone, Ex.empty) in
+  let ints =
+    List.fold_left (fun acc (lb2, ub2) ->
+        let ub2 = int_of_borne_sup ub2 in
+        if zero_endpoint ub2 then
+          (* if ub2 is zero then y is zero and the result is always -1 *)
+          let mone_lb = Large (mone, explain_borne ub2) in
+          (mone_lb, mone_ub) :: acc
+        else
+          let lb2 = int_of_borne_inf lb2 in
+          List.fold_left (fun acc (lb1, ub1) ->
+              let lb1 = int_of_borne_inf lb1 in
+              let ub1 = int_of_borne_sup ub1 in
+              let lb = bvudiv_b lb1 ub2 in
+              if zero_endpoint lb2 then
+                (* if lb2 is zero y can be zero and the result can be -1 *)
+                match ub1 with
+                | Pinfty -> (lb, mone_ub) :: acc
+                | Large (ub1, _) when Q.compare ub1 mone >= 0 ->
+                  (lb, mone_ub) :: acc
+                | _ ->
+                  (* the gap between ub1 and -1 is explained by ub1 *)
+                  let mone_lb = Large (mone, explain_borne ub1) in
+                  (mone_lb, mone_ub):: (lb, ub1) :: acc
+              else
+                (lb, bvudiv_b ub1 lb2) :: acc
+            ) acc x.ints
+      ) [] y.ints
+  in
+  let res =
+    union_intervals
+      { ints
+      ; is_int = true
+      ; expl = Ex.union x.expl y.expl
+      }
+  in
+  assert (res.ints != []);
+  res
+
+let bvurem x y =
+  assert (x.is_int && y.is_int);
+  let zero_lb = Large (Q.zero, Ex.empty) in
+  let ints =
+    List.fold_left (fun acc (lb2, ub2) ->
+        let lb2, ex_lb2 = zstar_of_borne_inf lb2 in
+        let ub2, ex_ub2 = zstar_of_borne_sup ub2 in
+        List.fold_left (fun acc (lb1, ub1) ->
+            let lb1, ex_lb1 = zstar_of_borne_inf lb1 in
+            let ub1, ex_ub1 = zstar_of_borne_sup ub1 in
+            if is_zero_zstar ub2 then
+              (* y is always zero -> identity *)
+              let lb = borne_of_zstar ~ex:(Ex.union ex_lb1 ex_ub2) lb1 in
+              let ub = borne_of_zstar ~ex:(Ex.union ex_ub1 ex_ub2) ub1 in
+              (lb, ub) :: acc
+            else if compare_zstar ub1 lb2 < 0 then
+              (* if x < y bvurem is the identity; need to add the justification
+                 for the x < y inequality to the bounds *)
+              let ex = Ex.union ex_ub1 ex_lb2 in
+              let lb = borne_of_zstar ~ex:(Ex.union ex_lb1 ex) lb1 in
+              let ub = borne_of_zstar ~ex:(Ex.union ex_ub1 ex) ub1 in
+              (lb, ub) :: acc
+            else if is_zero_zstar lb2 || compare_zstar ub1 ub2 < 0 then
+              (* the range [0, ub1] is always valid
+                 it is also the best we can do if y can be zero or can be bigger
+                 than x *)
+              let ub = borne_of_zstar ~ex:ex_ub1 ub1 in
+              (zero_lb, ub) :: acc
+            else
+              (* y is non-zero (by ex_lb2) ; [0, ub2 - 1[ is valid *)
+              let ub =
+                borne_of_zstar ~ex:(Ex.union ex_lb2 ex_ub2)
+                  (map_star Z.pred ub2)
+              in
+              (zero_lb, ub) :: acc
+          ) acc x.ints
+      ) [] y.ints
+  in
+  let res =
+    union_intervals
+      { ints
+      ; is_int = x.is_int
+      ; expl = Ex.union x.expl y.expl }
+  in
+  assert (res.ints != []);
+  res
+
 (** Apply function [f] to the interval.
 
     [f] *MUST* be monotone (either increasing or decreasing depending on the

src/lib/reasoners/intervals.mli

@@ -164,6 +164,20 @@ val extract : t -> int -> int -> t
     unbounded (in which case [extract s i j] returns the full interval
     [[0, 2^(j - i + 1) - 1]]). *)
 
+val bvudiv : int -> t -> t -> t
+(** [bvudiv sz s t] computes an overapproximation of integer division for
+    bit-vectors of width [sz] as defined in the FixedSizeBitVectors SMT-LIB
+    theory, i.e. where [bvudiv n 0] is [2^sz - 1].
+
+    [s] and [t] must be within the [0, 2^sz - 1] range. *)
+
+val bvurem : t -> t -> t
+(** [bvurem sz s t] computes an overapproximation of integer remainder for
+    bit-vectors of width [sz] as defined in the FixedSizeBitVectors SMT-LIB
+    theory, i.e. where [bvurem n 0] is [n].
+
+    [s] and [t] must be within the [0, 2^sz - 1] range. *)
+
 type interval_matching =
   ((Numbers.Q.t * bool) option * (Numbers.Q.t * bool) option * Ty.t)
     Var.Map.t

src/lib/structures/expr.ml

@@ -3067,16 +3067,8 @@ module BV = struct
   let bvsub s t = mk_term (Op BVsub) [s; t] (type_info s)
   let bvneg s = bvsub (of_bigint_like s Z.zero) s
   let bvmul s t = mk_term (Op BVmul) [s; t] (type_info s)
-  let bvudiv s t =
-    let m = size2 s t in
-    ite (eq (bv2nat t) Ints.(~$0))
-      (bvones m)
-      (int2bv m Ints.(bv2nat s / bv2nat t))
-  let bvurem s t =
-    let m = size2 s t in
-    ite (eq (bv2nat t) Ints.(~$0))
-      s
-      (int2bv m Ints.(bv2nat s mod bv2nat t))
+  let bvudiv s t = mk_term (Op BVudiv) [s; t] (type_info s)
+  let bvurem s t = mk_term (Op BVurem) [s; t] (type_info s)
   let bvsdiv s t =
     let m = size2 s t in
     let msb_s = extract (m - 1) (m - 1) s in

src/lib/structures/symbols.ml

@@ -47,7 +47,7 @@ type operator =
   | Concat
   | Extract of int * int (* lower bound * upper bound *)
   | BVnot | BVand | BVor | BVxor
-  | BVadd | BVsub | BVmul
+  | BVadd | BVsub | BVmul | BVudiv | BVurem
   | Int2BV of int | BV2Nat
   (* FP *)
   | Float
@@ -199,7 +199,7 @@ let compare_operators op1 op2 =
             | Sqrt_real_excess | Min_real | Min_int | Max_real | Max_int
             | Integer_log2 | Pow | Integer_round
             | BVnot | BVand | BVor | BVxor
-            | BVadd | BVsub | BVmul
+            | BVadd | BVsub | BVmul | BVudiv | BVurem
             | Int2BV _ | BV2Nat
             | Not_theory_constant | Is_theory_constant | Linear_dependency
             | Constr _ | Destruct _ | Tite) -> assert false
@@ -362,6 +362,8 @@ module AEPrinter = struct
     | BVadd -> Fmt.pf ppf "bvadd"
     | BVsub -> Fmt.pf ppf "bvsub"
     | BVmul -> Fmt.pf ppf "bvmul"
+    | BVudiv -> Fmt.pf ppf "bvudiv"
+    | BVurem -> Fmt.pf ppf "bvurem"
 
     (* ArraysEx theory *)
     | Get -> Fmt.pf ppf "get"
@@ -467,6 +469,8 @@ module SmtPrinter = struct
     | BVadd -> Fmt.pf ppf "bvadd"
     | BVsub -> Fmt.pf ppf "bvsub"
     | BVmul -> Fmt.pf ppf "bvmul"
+    | BVudiv -> Fmt.pf ppf "bvudiv"
+    | BVurem -> Fmt.pf ppf "bvurem"
 
     (* ArraysEx theory *)
     | Get -> Fmt.pf ppf "select"

src/lib/structures/symbols.mli

@@ -47,7 +47,7 @@ type operator =
   | Concat
   | Extract of int * int (* lower bound * upper bound *)
   | BVnot | BVand | BVor | BVxor
-  | BVadd | BVsub | BVmul
+  | BVadd | BVsub | BVmul | BVudiv | BVurem
   | Int2BV of int | BV2Nat
   (* FP *)
   | Float