Use ZArith-based representations for numbers and bitvectors (#850)

Alt-Ergo uses strings to represent terms containing numbers and/or
bitvectors. In addition to a (slight) overhead, it also caused issues in
the past with different string representations of the same value being
considered distinct.

This patch uses Z.t (Q.t for reals) to represent integers, bitvectors
and reals instead of strings.

Fixes #668

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