fix(BV): Internalize sign_extend and repeat

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
@@ -1478,7 +1552,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,18 @@ module BV = struct
       (Sy.Op (Sy.Extract (j, i))) [s] (Ty.Tbitv (i - j + 1))
 
   (* Other operations *)
-  let rec repeat i t =
-    assert (i >= 1);
-    if i = 1 then t else concat t (repeat (i - 1) t)
+  let repeat i t =
+    if i < 1 then
+      Fmt.invalid_arg "repeat: count must be positive (got %d)" i;
+    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 5 4) ((_ sign_extend 4) x)) ((_ repeat 2) ((_ extract 3 3) 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)