Use ZArith-based representations for numbers and bitvectors

src/lib/frontend/d_cnf.ml

@@ -950,11 +950,7 @@ let rec mk_expr
           | B.True -> E.vrai
           | B.False -> E.faux
           | B.Integer s -> E.int s
-          | B.Decimal s ->
-            (* We do a roundtrip through [Q.t] to ensure that multiple
-               representations of the same real (e.g. [2] and [0x1.0p1]) get
-               normalized to the same expression.  *)
-            E.real (s |> Q.of_string |> Q.to_string)
+          | B.Decimal s -> E.real s
           | B.Bitvec s ->
             let ty = dty_to_ty term_ty in
             E.bitv s ty

src/lib/reasoners/arith.ml

@@ -227,8 +227,11 @@ module Shostak
   let rec mke coef p t ctx =
     let { E.f = sb ; xs; ty; _ } = E.term_view t in
     match sb, xs with
-    | (Sy.Int n | Sy.Real n) , _  ->
-      let c = Q.mult coef (Q.from_string (Hstring.view n)) in
+    | Sy.Int n, _ ->
+      let c = Q.mult coef (Q.from_z n) in
+      P.add_const c p, ctx
+    | Sy.Real q, _  ->
+      let c = Q.mult coef q in
       P.add_const c p, ctx
 
     | Sy.Op Sy.Mult, [t1;t2] ->
@@ -394,12 +397,7 @@ module Shostak
         | [], c ->
           let c = Q.to_z c in
           let c = ZA.(erem c @@ ~$1 lsl n) in
-          let biv =
-            String.init n (fun i ->
-                let i = n - i - 1 in
-                if ZA.(extract c i 1 |> to_int) = 0 then '0' else '1')
-          in
-          let r, ctx' = E.mk_term (Bitv biv) [] (Tbitv n) |> X.make in
+          let r, ctx' = E.mk_term (Sy.Bitv (n, c)) [] (Tbitv n) |> X.make in
           r, List.rev_append ctx' ctx
         | [ coef, x ], const when Q.is_zero const && Q.is_one coef ->
           begin match X.term_extract x with

src/lib/reasoners/bitv.ml

@@ -194,7 +194,7 @@ module Shostak(X : ALIEN) = struct
 
   module Canon = struct
     type 'a view_descr =
-      | Vcte of string
+      | Vcte of Z.t
       | Vother of 'a
       | Vextract of 'a * int * int
       | Vconcat of 'a * 'a
@@ -204,7 +204,7 @@ module Shostak(X : ALIEN) = struct
 
     let view t =
       match E.term_view t with
-      | { f = Bitv s; ty = Tbitv size; _ } -> { descr = Vcte s; size }
+      | { f = Bitv (_, s); ty = Tbitv size; _ } -> { descr = Vcte s; size }
       | { f = Op Concat; xs = [ t1; t2 ]; ty = Tbitv size; _ } ->
         { descr = Vconcat (t1, t2); size }
       | { f = Op Extract (i, j); xs = [ t' ]; ty = Tbitv size; _ } ->
@@ -311,7 +311,7 @@ module Shostak(X : ALIEN) = struct
       let size = j - i + 1 in
       match tv.descr with
       | Vcte z ->
-        vmake ~neg { descr = Vcte (String.sub z (tv.size - j - 1) size); size }
+        vmake ~neg { descr = Vcte (Z.extract z i size); size }
       | Vother t ->
         let+ o = other ~neg t tv.size in
         extract tv.size i j o
@@ -333,12 +333,11 @@ module Shostak(X : ALIEN) = struct
       match tv.descr with
       | Vcte z ->
         let acc = ref [] in
-        for i = String.length z - 1 downto 0 do
-          let c = z.[i] in
-          match c, !acc with
-          | '0', { bv = Cte b; sz } :: rst when Bool.equal b neg ->
+        for i = 0 to tv.size - 1 do
+          match Z.testbit z i, !acc with
+          | false, { bv = Cte b; sz } :: rst when Bool.equal b neg ->
             acc := { bv = Cte b; sz = sz + 1 } :: rst
-          | '0', rst ->
+          | false, rst ->
             acc := { bv = Cte neg; sz = 1 } :: rst
           | _, { bv = Cte b; sz } :: rst when Bool.equal b (not neg) ->
             acc := { bv = Cte b; sz = sz + 1 } :: rst

src/lib/structures/expr.ml

@@ -964,7 +964,7 @@ let real r =
     mk_term (Sy.Op Sy.Minus) [ positive_real "0"; positive_real pi ] Ty.Treal
   | _ -> positive_real r
 
-let bitv bt ty = mk_term (Sy.Bitv bt) [] ty
+let bitv bt ty = mk_term (Sy.bitv bt) [] ty
 
 let pred t = mk_term (Sy.Op Sy.Minus) [t;int "1"] Ty.Tint
 
@@ -2813,11 +2813,10 @@ type const =
 let const_view t =
   match term_view t with
   | { f = Int n; _ } ->
-    let n = Hstring.view n in
-    begin match int_of_string n with
+    begin match Z.to_int n with
       | n -> Int n
-      | exception Failure _ ->
-        Fmt.failwith "error when trying to convert %s to an int" n
+      | exception Z.Overflow ->
+        Fmt.failwith "error when trying to convert %a to an int" Z.pp_print n
     end
   | { f = Op (Constr c); ty; _ }
     when Ty.equal ty Fpa_rounding.fpa_rounding_mode ->

src/lib/structures/symbols.ml

@@ -86,9 +86,9 @@ type t =
   | False
   | Void
   | Name of Hstring.t * name_kind * bool
-  | Int of Hstring.t
-  | Real of Hstring.t
-  | Bitv of string
+  | Int of Z.t
+  | Real of Q.t
+  | Bitv of int * Z.t
   | Op of operator
   | Lit of lit
   | Form of form
@@ -103,8 +103,16 @@ let name ?(kind=Other) ?(defined=false) s =
   Name (Hstring.make s, kind, defined)
 
 let var s = Var s
-let int i = Int (Hstring.make i)
-let real r = Real (Hstring.make r)
+let int i = Int (Z.of_string i)
+let bitv s =
+  let biv =
+    Compat.String.fold_left (fun n c ->
+        match c with
+        | '0' -> Z.(n lsl 1)
+        | '1' -> Z.((n lsl 1) lor ~$1)
+        | _ -> assert false) Z.zero s
+  in Bitv (String.length s, biv)
+let real r = Real (Q.of_string r)
 let constr s = Op (Constr (Hstring.make s))
 let destruct ~guarded s = Op (Destruct (Hstring.make s, guarded))
 
@@ -210,13 +218,15 @@ let compare_bounds a b =
 let compare s1 s2 =
   Util.compare_algebraic s1 s2
     (function
-      | Int h1, Int h2
-      | Real h1, Real h2 -> Hstring.compare h1 h2
+      | Int z1, Int z2 -> Z.compare z1 z2
+      | Real h1, Real h2 -> Q.compare h1 h2
       | Var v1, Var v2 | MapsTo v1, MapsTo v2 -> Var.compare v1 v2
       | Name (h1, k1, _), Name (h2, k2, _) ->
         let c = Hstring.compare h1 h2 in
         if c <> 0 then c else compare_kinds k1 k2
-      | Bitv s1, Bitv s2 -> String.compare s1 s2
+      | Bitv (n1, s1), Bitv (n2, s2) ->
+        let c = Int.compare n1 n2 in
+        if c <> 0 then c else Z.compare s1 s2
       | Op op1, Op op2 -> compare_operators op1 op2
       | Lit lit1, Lit lit2 -> compare_lits lit1 lit2
       | Form f1, Form f2 -> compare_forms f1 f2
@@ -238,11 +248,12 @@ let hash x =
   | True -> 1
   | False -> 2
   | Let -> 3
-  | Bitv s -> 19 * Hashtbl.hash s + 3
+  | Bitv (n, s) -> 19 * (Hashtbl.hash n + Hashtbl.hash s) + 3
   | In (b1, b2) -> 19 * (Hashtbl.hash b1 + Hashtbl.hash b2) + 4
   | Name (n, Ac, _) -> 19 * Hstring.hash n + 5
   | Name (n, Other, _) -> 19 * Hstring.hash n + 6
-  | Int n | Real n -> 19 * Hstring.hash n + 7
+  | Int z -> 19 * Z.hash z + 7
+  | Real n -> 19 * Hashtbl.hash n + 7
   | Var v -> 19 * Var.hash v + 8
   | MapsTo v -> 19 * Var.hash v + 9
   | Op op -> 19 * Hashtbl.hash op + 10
@@ -287,9 +298,9 @@ let to_string ?(show_vars=true) x = match x with
   | Name (n, _, _) -> Hstring.view n
   | Var v when show_vars -> Format.sprintf "'%s'" (Var.to_string v)
   | Var v -> Var.to_string v
-  | Int n -> Hstring.view n
-  | Real n -> Hstring.view n
-  | Bitv s -> "[|"^s^"|]"
+  | Int n -> Z.to_string n
+  | Real n -> Q.to_string n
+  | Bitv (n, s) -> Fmt.str "[|%s|]" (Z.format (Fmt.str "%%0%db" n) s)
   | Op Plus -> "+"
   | Op Minus -> "-"
   | Op Mult -> "*"

src/lib/structures/symbols.mli

@@ -85,9 +85,9 @@ type t =
   | False
   | Void
   | Name of Hstring.t * name_kind * bool
-  | Int of Hstring.t
-  | Real of Hstring.t
-  | Bitv of string
+  | Int of Z.t
+  | Real of Q.t
+  | Bitv of int * Z.t
   | Op of operator
   | Lit of lit
   | Form of form
@@ -100,6 +100,7 @@ val name : ?kind:name_kind -> ?defined:bool -> string -> t
 val var : Var.t -> t
 val underscore : t
 val int : string -> t
+val bitv : string -> t
 val real : string -> t
 val constr : string -> t
 val destruct : guarded:bool -> string -> t

src/lib/util/compat.ml

@@ -4,6 +4,13 @@ module String = struct
   let starts_with ~prefix s =
     length s >= length prefix &&
     equal (sub s 0 (length prefix)) prefix
+
+  let fold_left f x a =
+    let r = ref x in
+    for i = 0 to length a - 1 do
+      r := f !r (unsafe_get a i)
+    done;
+    !r
 end
 
 module Seq = struct

src/lib/util/compat.mli

@@ -34,6 +34,9 @@
 module String : sig
   (* @since 4.13.0 *)
   val starts_with : prefix:string -> string -> bool
+
+  (* @since 4.13.0 *)
+  val fold_left : ('acc -> char -> 'acc) -> 'acc -> string -> 'acc
 end
 
 module Seq : sig

src/lib/util/numbers.mli

@@ -86,7 +86,7 @@ end
 
 (** Rationals implementation. **)
 module Q : sig
-  type t
+  type t = Q.t
 
   exception Not_a_float