fix(BV): Internalize sign_extend and repeat

Currently, we convert `sign_extend` and `repeat` to the appropriate
concatenations and extractions at the term level. This has the advantage
that it is simple, but the inconvenient that we create a potentially
large amount of terms that do not appear in the original problem
(proportional to the size of the sign extension or repetition).

In addition to preventing obvious simplifications with extractions, the
creation of many terms clutters the union-find which drastically slows
down the solver in presence of sign extensions to large bit-widths.

src/lib/reasoners/bitv.ml

@@ -302,13 +302,13 @@ let negate_bitv : bitv -> bitv = List.map negate_solver_simple_term
 
 let extract_st i j { bv; sz } =
   if sz = j - i + 1 then
-    [ { bv ; sz } ]
+    { bv ; sz }
   else
     match bv with
-    | Cte b -> [{ bv = Cte (Z.extract b i (j - i + 1)); sz = j - i + 1 }]
-    | Other r -> [{ bv = Ext (r, sz, i, j) ; sz = j - i + 1 }]
+    | Cte b -> { bv = Cte (Z.extract b i (j - i + 1)); sz = j - i + 1 }
+    | Other r -> { bv = Ext (r, sz, i, j) ; sz = j - i + 1 }
     | Ext (r, sz, k, _) ->
-      [{ bv = Ext (r, sz, i + k, j + k) ; sz = j - i + 1 }]
+      { bv = Ext (r, sz, i + k, j + k) ; sz = j - i + 1 }
 
 (* extract [i..j] from a composition of size [size]
 
@@ -320,15 +320,38 @@ let rec extract size i j = function
     assert false
   | [ st ] ->
     assert (st.sz = size);
-    extract_st i j st
+    [ extract_st i j st ]
   | { sz; _ } :: sts when j < size - sz ->
     extract (size - sz) i j sts
   | ({ sz; _ } as st) :: _ when i >= size - sz ->
-    extract_st (i - (size - sz)) (j - (size - sz)) st
+    [ extract_st (i - (size - sz)) (j - (size - sz)) st ]
   | ({ sz; _ } as st) :: sts ->
-    extract_st 0 (j - (size - sz)) st @
+    extract_st 0 (j - (size - sz)) st ::
     extract (size - sz) i (size - sz - 1) sts
 
+(* [repeat n b] concatenates [n] copies of [b] *)
+let repeat n b =
+  assert (n > 0);
+  let rec loop b n acc =
+    if n = 0 then acc
+    else loop b (n - 1) (b @ acc)
+  in
+  loop b (n - 1) b
+
+(* [sign_extend n sts] is [concat (repeat n (sign sts)) sts]. *)
+let sign_extend n sts =
+  match n, sts with
+  | _, [] -> assert false
+  | 0, sts -> sts
+  | n, ({ sz; bv } as st) :: sts ->
+    match bv with
+    | Cte b ->
+      int2bv_const (n + sz) (Z.signed_extract b 0 sz) @ sts
+    | _ ->
+      List.rev_append
+        (repeat n [ extract_st (sz - 1) (sz - 1) st ])
+        (st :: sts)
+
 module type ALIEN = sig
   include Sig.X
   val embed : r abstract -> r
@@ -348,7 +371,8 @@ module Shostak(X : ALIEN) = struct
     match sy with
     | Sy.Bitv _
     | Op (
-        Concat | Extract _ | BV2Nat
+        Concat | Extract _ | Sign_extend _ | Repeat _
+        | BV2Nat
         | BVnot | BVand | BVor | BVxor
         | BVadd | BVsub | BVmul | BVudiv | BVurem
         | BVshl | BVlshr)
@@ -371,6 +395,8 @@ module Shostak(X : ALIEN) = struct
       | Vother of 'a
       | Vextract of 'a * int * int
       | Vconcat of 'a * 'a
+      | Vsign_extend of int * 'a
+      | Vrepeat of int * 'a
       | Vnot of 'a
 
     type 'a view = { descr : 'a view_descr ; size : int }
@@ -381,6 +407,10 @@ module Shostak(X : ALIEN) = struct
         { descr = Vcte s; size }
       | { f = Op Concat; xs = [ t1; t2 ]; ty = Tbitv size; _ } ->
         { descr = Vconcat (t1, t2); size }
+      | { f = Op (Sign_extend n) ; xs = [ t ] ; ty = Tbitv size; _ } ->
+        { descr = Vsign_extend (n, t); size }
+      | { f = Op (Repeat n) ; xs = [ t ] ; ty = Tbitv size; _ } ->
+        { descr = Vrepeat (n, t) ; size }
       | { f = Op Extract (i, j); xs = [ t' ]; ty = Tbitv size; _ } ->
         assert (size = j - i + 1);
         { descr = Vextract (t', i, j); size }
@@ -463,6 +493,40 @@ module Shostak(X : ALIEN) = struct
           let+ u = vextract ~neg 0 (j - vv.size) vu
           and+ v = vextract ~neg i (vv.size - 1) vv
           in u @ v
+      | Vsign_extend (_, u) ->
+        let vu = view u in
+        if j < vu.size then
+          (* extraction from the original vector *)
+          vextract ~neg i j vu
+        else if i >= vu.size then
+          (* extraction from the repeated sign part *)
+          let+ sgn = vextract ~neg (vu.size - 1) (vu.size - 1) vu in
+          repeat size sgn
+        else
+          (* extraction from both repeated sign and original vector *)
+          let+ u = vextract ~neg i (vu.size - 1) vu in
+          sign_extend (j - vu.size + 1) u
+      | Vrepeat (_, u) ->
+        let vu = view u in
+        (* i = ib * vu.size + il
+           j = jb * vu.size + jl *)
+        let ib = i / vu.size and jb = j / vu.size in
+        let il = i mod vu.size and jl = j mod vu.size in
+        if ib = jb then (
+          (* extraction from within a single repetition *)
+          assert (il <= jl);
+          vextract ~neg il jl vu
+        ) else
+          (* extraction across consecutive repetitions *)
+          let+ u = vmake ~neg vu in
+          let suffix =
+            if il = 0 then []
+            else extract vu.size il (vu.size - 1) u
+          and prefix =
+            if jl = 0 then []
+            else extract vu.size 0 jl u
+          in
+          prefix @ repeat (jb - ib - 1) u @ suffix
       | Vnot t ->
         vextract ~neg:(not neg) i j (view t)
     and vmake ~neg tv ctx =
@@ -473,6 +537,16 @@ module Shostak(X : ALIEN) = struct
       | Vother t -> other ~neg t tv.size ctx
       | Vextract (t', i, j) ->
         run ctx @@ vextract ~neg i j (view t')
+      | Vsign_extend (n, t) ->
+        run ctx @@
+        let+ r = make ~neg t in
+        let sz = tv.size - n in
+        let b = extract sz (sz - 1) (sz - 1) r in
+        repeat n b @ r
+      | Vrepeat (n, t) ->
+        run ctx @@
+        let+ r = make ~neg t in
+        repeat n r
       | Vconcat (t1, t2) ->
         run ctx @@
         let+ t1 = make ~neg t1 and+ t2 = make ~neg t2 in
@@ -1477,7 +1551,7 @@ module Shostak(X : ALIEN) = struct
 *)
   let fully_interpreted sb =
     match sb with
-    | Sy.Op (Concat | Extract _ | BVnot) -> true
+    | Sy.Op (Concat | Extract _ | Sign_extend _ | Repeat _ | BVnot) -> true
     | _ -> false
 
   let term_extract _ = None, false

src/lib/structures/expr.ml

@@ -3097,17 +3097,17 @@ module BV = struct
       (Sy.Op (Sy.Extract (j, i))) [s] (Ty.Tbitv (i - j + 1))
 
   (* Other operations *)
-  let rec repeat i t =
+  let repeat i t =
     assert (i >= 1);
-    if i = 1 then t else concat t (repeat (i - 1) t)
+    mk_term (Op (Repeat i)) [t] (Tbitv (i * size t))
 
   let zero_extend i t =
     if i = 0 then t else concat (bvzero i) t
 
   let sign_extend i t =
-    if i = 0 then t else
-      let m = size t in
-      concat (repeat i (extract (m - 1) (m - 1) t)) t
+    if i = 0 then t
+    else
+      mk_term (Op (Sign_extend i)) [t] (Tbitv (i + size t))
 
   let rotate_left i t =
     let m = size t in

src/lib/structures/symbols.ml

@@ -43,6 +43,8 @@ type operator =
   (* BV *)
   | Concat
   | Extract of int * int (* lower bound * upper bound *)
+  | Sign_extend of int
+  | Repeat of int
   | BVnot | BVand | BVor | BVxor
   | BVadd | BVsub | BVmul | BVudiv | BVurem
   | BVshl | BVlshr
@@ -190,9 +192,12 @@ let compare_operators op1 op2 =
       | Extract (i1, j1), Extract (i2, j2) ->
         let r = Int.compare i1 i2 in
         if r = 0 then Int.compare j1 j2 else r
+      | Sign_extend n1, Sign_extend n2
+      | Repeat n1, Repeat n2 ->
+        Int.compare n1 n2
       | Int2BV n1, Int2BV n2 -> Int.compare n1 n2
       | _ , (Plus | Minus | Mult | Div | Modulo | Real_is_int
-            | Concat | Extract _ | Get | Set | Float
+            | Concat | Extract _ | Sign_extend _ | Repeat _ | Get | Set | Float
             | Access _ | Record | Sqrt_real | Abs_int | Abs_real
             | Real_of_int | Int_floor | Int_ceil | Sqrt_real_default
             | Sqrt_real_excess | Min_real | Min_int | Max_real | Max_int
@@ -350,6 +355,8 @@ module AEPrinter = struct
     (* FixedSizedBitVectors theory *)
     | Extract (i, j) -> Fmt.pf ppf "^{%d; %d}" i j
     | Concat -> Fmt.pf ppf "@"
+    | Sign_extend i -> Fmt.pf ppf  "sign_extend[%d]" i
+    | Repeat i -> Fmt.pf ppf "repeat[%d]" i
     | BV2Nat -> Fmt.pf ppf "bv2nat"
     | Int2BV n -> Fmt.pf ppf "int2bv[%d]" n
     | BVnot -> Fmt.pf ppf "bvnot"
@@ -458,6 +465,8 @@ module SmtPrinter = struct
     (* FixedSizedBitVectors theory *)
     | Extract (i, j) -> Fmt.pf ppf "(_ extract %d %d)" j i
     | Concat -> Fmt.pf ppf "concat"
+    | Sign_extend i -> Fmt.pf ppf "(_ sign_extend %d)" i
+    | Repeat i -> Fmt.pf ppf "(_ repeat %d)" i
     | BV2Nat -> Fmt.pf ppf "bv2nat"
     | BVnot -> Fmt.pf ppf "bvnot"
     | BVand -> Fmt.pf ppf "bvand"

src/lib/structures/symbols.mli

@@ -43,6 +43,8 @@ type operator =
   (* BV *)
   | Concat
   | Extract of int * int (* lower bound * upper bound *)
+  | Sign_extend of int
+  | Repeat of int
   | BVnot | BVand | BVor | BVxor
   | BVadd | BVsub | BVmul | BVudiv | BVurem
   | BVshl | BVlshr

tests/bitv/testfile-repeat-001.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-repeat-001.smt2

@@ -0,0 +1,4 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 4))
+(assert (distinct ((_ extract 5 4) ((_ repeat 10) x)) ((_ extract 1 0) x)))
+(check-sat)

tests/bitv/testfile-repeat-002.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-repeat-002.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-option :reproducible-resource-limit 100)
+(declare-const x (_ BitVec 10))
+; Previously, we would be creating a huge amount of terms here and timeout.
+(assert (distinct ((_ extract 124 95) ((_ repeat 1024) x)) (concat (concat ((_ extract 4 0) x) ((_ repeat 2) x)) ((_ extract 9 5) x))))
+(check-sat)

tests/bitv/testfile-sign-extend-001.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-sign-extend-001.smt2

@@ -0,0 +1,4 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 4))
+(assert (distinct ((_ extract 5 2) ((_ sign_extend 4) x)) (concat ((_ extract 3 3) x) (concat ((_ extract 3 3) x) ((_ extract 3 2) x)))))
+(check-sat)

tests/bitv/testfile-sign-extend-002.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-sign-extend-002.smt2

@@ -0,0 +1,4 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 4))
+(assert (distinct ((_ extract 3 2) ((_ sign_extend 4) x)) ((_ extract 3 2) x)))
+(check-sat)

tests/bitv/testfile-sign-extend-003.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-sign-extend-003.smt2

@@ -0,0 +1,4 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 4))
+(assert (distinct ((_ extract 3 2) ((_ sign_extend 4) x)) ((_ extract 3 2) x)))
+(check-sat)

tests/bitv/testfile-sign-extend-004.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-sign-extend-004.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-option :reproducible-resource-limit 100)
+(declare-const x (_ BitVec 1))
+; Previously, we would be creating a huge amount of terms here and timeout.
+(assert (distinct ((_ extract 1023 1023) ((_ sign_extend 1023) x)) x))
+(check-sat)