Add support for ground bv2nat and int2bv reasoning

This patch adds support for "combined" reasoning about the int2bv and
bv2nat symbols in the arith and bitv reasoners.

More specifically:

 - The constructors for bv2nat and int2bv in `expr.ml` are now "smart"
   and know that they are related, so that we effectivly have the
   following rewrite rules:

    `(bv2nat ((_ int2bv n) x))` -> `(mod x (pow 2 n))`
    `((_ int2bv n) (bv2nat (as x (_ BitVec m))))`
      -> `(ite (> m n) (extract (- n 1) 0 x) (zero_extend (- m n) x))`

   These are added early in the bv2nat and int2bv constructors to ensure
   that we *never* actually build `((_ int2bv n) (bv2nat e))` or
   `(bv2nat ((_ int2bv n) e))` terms. This is actualy useful because the
   simplifications done for `bv2nat` (see below) are more powerful than
   what `int2bv` can recover, and there would be information loss
   otherwise e.g. for `((_ int2bv n) (bv2nat (concat e1 e2)))` which
   would become

     `((_ int2bv n) (+ (* (bv2nat e1) (pow 2 m)) (bv2nat e2)))`

   instead of

      `(concat e1 e2)`

   (assuming that `e2` is of type `(_ BitVec m)` and `e1` of type
   `(_ BitVec |n - m|)`).

 - The arith and bitv reasoners perform constant propagation of int2bv
   and bv2nat

 - The arith reasoner performs the `((_ int2bv n) (bv2nat x))`
   conversion more aggressivey, i.e. it performs the conversion for
   terms of the form `((_ int2bv n) e)` where the semantic value of `e`
   is of the form `(bv2nat e')`

   More complex transformations, such as transforming
   `(int2bv (* 2 (bv2nat e)))` into `(concat e #b0)`, are not
   supported.

 - The bitv reasoner also performs the `(bv2nat ((_ int2bv n) e))`
   conversion more aggressively, i.e. for terms that reduce to
   `((_ int2bv n) e)` after simplification.

 - The bitv reasoner performs additional simplifications on `bv2nat`
   terms after normalization. For instance, `(bv2nat (concat x y))`
   becomes `(+ (* (pow 2 n) (bv2nat x)) (bv2nat y))` when `y` is a
   bit-vector of size `n`, and `(bv2nat (extract j i x))` becomes
   `(mod (div (bv2nat x) (pow 2 i)) (pow 2 (+ (- j i) 1)))`

 - Finally, the bitv reasoner requires that the result of `bv2nat` for a
   bitvector of size `n` is in the range `0 ..< 2^n`

Combined, this allows exploiting the arith reasoner for a variety of
problems mostly involving bitvector arithmetic with constants. In
particular, we are able to handle many aritmetic expressions involving
`bv2nat`.

On the other hand, bitvector expressions involving `int2bv` have more
limited support. Indeed, not only does `int2bv` perform less
simplifications, we are currently not able to exploit the relevant
equivalence:

  `int2bv[n](x) = int2bv[n](y) iff x = y  (mod 2^n)`

src/lib/reasoners/arith.ml

@@ -31,6 +31,7 @@
 module Sy = Symbols
 module E = Expr
 
+module ZA = Z
 module Z = Numbers.Z
 module Q = Numbers.Q
 
@@ -119,7 +120,7 @@ module Shostak
          | Sqrt_real_default | Sqrt_real_excess
          | Real_of_int | Int_floor | Int_ceil
          | Max_int | Max_real | Min_int | Min_real
-         | Pow | Integer_log2
+         | Pow | Integer_log2 | Int2BV _
          | Integer_round) -> true
     | _ -> false
 
@@ -365,10 +366,64 @@ module Shostak
       | _ -> P.add p (P.create [coef, a] Q.zero ty), ctx
 
   let make t =
-    Options.tool_req 4 "TR-Arith-Make";
-    let ty = E.type_info t in
-    let p, ctx = mke Q.one (empty_polynome ty) t [] in
-    is_mine p, ctx
+    let { E.f; xs; _ } = E.term_view t in
+    match f, xs with
+    | Op Int2BV n, [x] ->
+      (* When we have an Int2BV expression, we try our best to convert it to
+         something that is usable by the bitv theory.
+
+         More precisely:
+
+         - If we have (int2bv c) where [c] is a constant, we convert the
+             constant to a bitvector constant of the appropriate size and
+             create the corresponding [Bitv] term. The call to [X.make] will be
+             dispatched to the bitvector theory.
+
+         - If we have (int2bv [1 * (bv2nat e) + 0]) -- that is, int2bv of a
+             single alien that is equal to a [bv2nat] expression -- we convert
+             [e] to the appropriate bitvector size using [extract] or
+             [zero_extend]. This is done by a roundtrip through E.BV.int2bv.
+
+         - There are some other expressions where we could convert, for
+             instance, disjoint sums of bv2nat terms multiplied by powers of
+             two, but we only handle the simple cases for now.
+
+         - In all other cases, Int2BV becomes uninterpreted. *)
+      let p, ctx = mke Q.one (empty_polynome Tint) x [] in
+      begin match P.to_list p with
+        | [], c ->
+          let c = Q.to_z c in
+          let c = ZA.(erem c @@ pow ~$2 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
+          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
+            | Some tx, _ ->
+              begin match (E.term_view tx).f with
+                | Op BV2Nat ->
+                  (* int2bv will simplify BV2Nat: we must [X.make] again *)
+                  let r, ctx' = E.BV.int2bv n tx |> X.make in
+                  r, List.rev_append ctx' ctx
+                | _ ->
+                  (* Otherwise we must become uninterpreted *)
+                  E.BV.int2bv n tx |> X.term_embed, ctx
+              end
+            | None, _ ->
+              X.term_embed t, []
+          end
+        | _ ->
+          X.term_embed t, []
+      end
+    | _ ->
+      Options.tool_req 4 "TR-Arith-Make";
+      let ty = E.type_info t in
+      let p, ctx = mke Q.one (empty_polynome ty) t [] in
+      is_mine p, ctx
 
   let rec expand p n acc =
     assert (n >=0);

src/lib/reasoners/bitv.ml

@@ -139,7 +139,7 @@ module Shostak(X : ALIEN) = struct
 
   let is_mine_symb sy _ =
     match sy with
-    | Sy.Bitv _ | Sy.Op (Sy.Concat | Sy.Extract _)  -> true
+    | Sy.Bitv _ | Sy.Op (Concat | Extract _ | BV2Nat)  -> true
     | _ -> false
 
   let embed r =
@@ -1125,13 +1125,88 @@ module Shostak(X : ALIEN) = struct
          | Other t | Ext(t,_,_,_) -> (X.leaves t)@acc
       ) [] bitv
 
-  let is_mine = function [{ bv = Other r; _ }] -> r | bv -> X.embed bv
+  let is_mine_opt = function [{ bv = Other r; _ }] -> Some r | _ -> None
+
+  let is_mine bv =
+    match is_mine_opt bv with
+    | Some r -> r
+    | None -> X.embed bv
 
   let print = Debug.print_C_ast
 
+  (* This is used to extract terms from non-bitv semantic values.
+
+     We assume that non-bitv semantic values of a bitvector type are
+     necessarily uninterpreted terms, because that should be the case at the
+     time this code is written.
+
+     If this ever ceases to be the case, we should either preserve the original
+     term along with the semantic value, or fail more gracefully here. *)
+  let term_extract r =
+    match X.term_extract r with
+    | Some t, _ -> t
+    | None, _ ->
+      Util.internal_error "Non-BV semantic value: %a" X.print r
+
+  (* This is a helper function that converts a [simple_term] to an integer
+     expression. *)
+  let simple_term_to_nat acc st =
+    match st.bv with
+    | Cte false -> E.Ints.(acc * ~$Z.(pow ~$2 st.sz))
+    | Cte true -> E.Ints.((acc + ~$$1) * ~$Z.(pow ~$2 st.sz) - ~$$1)
+    | Other r ->
+      let t = term_extract r in
+      E.Ints.(acc * ~$Z.(pow ~$2 st.sz) + E.BV.bv2nat t)
+    | Ext (o, _, i, j) ->
+      assert (st.sz = j - i + 1);
+      let t = term_extract o in
+      E.Ints.(
+        acc * ~$Z.(pow ~$2 st.sz) +
+        (E.BV.bv2nat t / ~$Z.(pow ~$2 i)) mod ~$Z.(pow ~$2 st.sz))
+
+  let abstract_to_nat r =
+    List.fold_left simple_term_to_nat (E.Ints.of_int 0) r
+
+  (* Ideally, we would want to just call [abstract_to_nat r |> X.make]. But if
+     we do so, we may end up in a loop where we repeatedly call [X.make] on a
+     [BV2Nat] term -- so instead if we are a single [Other] term, we become
+     uninterpreted. *)
+  let bv2nat bv =
+    match is_mine_opt bv with
+    | Some r ->
+      let t = term_extract r in
+      begin match E.term_view t with
+        | { f = Op Int2BV _; _ } ->
+          (* bv2nat will simplify: we must call [X.make] again *)
+          E.BV.bv2nat t |> X.make
+        | { ty = Tbitv n; _ } ->
+          (* bv2nat will *not* simplify: become uninterpreted with interval
+             information *)
+          let t = E.BV.bv2nat t in
+          X.term_embed t, [ E.Ints.(~$$0 <= t) ; E.Ints.(t < ~$Z.(pow ~$2 n)) ]
+        | { ty; _ } ->
+          Util.internal_error "expected bitv, got %a" Ty.print ty
+      end
+    | None -> abstract_to_nat bv |> X.make
+
   let make t =
-    let r, ctx = Canonizer.make t in
-    is_mine r, ctx
+    let { E.f; xs; _ } = E.term_view t in
+    match f, xs with
+    | Op BV2Nat, [x] ->
+      (* When we have a BV2Nat expression, we try our best to convert it to
+         something that is usable by the arithmetic theory.
+
+         More precisely, after simplification of the argument, we get a
+         composition of constants and aliens or alien extractions, to which we
+         apply [bv2nat] recursively. If the alien or alien extraction are
+         [int2bv] terms, we convert the composition [(bv2nat ((_ int2bv n) x))]
+         into [(mod x (pow 2 n))]. *)
+      let r, ctx = Canonizer.make x in
+      let r, ctx' = bv2nat r in
+      r, List.rev_append ctx' ctx
+    | _ ->
+      let r, ctx = Canonizer.make t in
+      is_mine r, ctx
 
   let color _ = assert false
 

src/lib/structures/expr.ml

@@ -2912,9 +2912,6 @@ module BV = struct
     assert (size t = m);
     m
 
-  let int2bv n t = mk_term (Op (Int2BV n)) [t] (Tbitv n)
-  let bv2nat t = mk_term (Op BV2Nat) [t] Tint
-
   (* Function symbols for concatenation *)
   let concat s t =
     let n = size s and m = size t in
@@ -2956,6 +2953,26 @@ module BV = struct
       else
         concat (extract (i - 1) 0 t) (extract (m - 1) i t)
 
+  (* int2bv and bv2nat *)
+  let int2bv n t =
+    (* Note: arith.ml calls [int2bv] in [make]. If additional simplifications
+       are added here, arith.ml must be updated as well. *)
+    match term_view t with
+    | { f = Op BV2Nat; xs = [ t ]; ty = Tbitv m; _ } ->
+      if m > n then
+        extract (n - 1) 0 t
+      else
+        zero_extend (n - m) t
+    | _ -> mk_term (Op (Int2BV n)) [t] (Tbitv n)
+
+  let bv2nat t =
+    (* Note: bitv.ml calls [bv2nat] in [make]. If additional simplifications
+       are added here, bitv.ml must be updated as well. *)
+    match term_view t with
+    | { f = Op Int2BV n; xs = [ t ]; _ } ->
+      Ints.(t mod ~$Z.(pow ~$2 n))
+    | _ -> mk_term (Op BV2Nat) [t] Tint
+
   (* Bit-wise operations *)
   let bvnot s = mk_term (Op BVnot) [s] (type_info s)
   let bvand s t = mk_term (Op BVand) [s; t] (type_info s)

src/lib/util/numbers.mli

@@ -30,7 +30,7 @@
 
 (** Integers implementation. **)
 module Z : sig
-  type t
+  type t = Z.t
   val zero : t
   val one : t
   val m_one : t (* minus one *)

src/lib/util/util.ml

@@ -34,12 +34,15 @@ exception Unsolvable
 exception Cmp of int
 
 exception Not_implemented of string
+exception Internal_error of string
 
 let () =
   Printexc.register_printer
     (function
       | Not_implemented s ->
         Some (Format.sprintf "Feature not implemented (%s)" s)
+      | Internal_error s ->
+        Some (Format.sprintf "Internal error: %s" s)
       | _ -> None
     )
 
@@ -183,3 +186,6 @@ let rec print_list_pp ~sep ~pp fmt = function
     print_list_pp ~sep ~pp fmt l
 
 let failwith msg = Format.kasprintf failwith msg
+
+let internal_error msg =
+  Format.kasprintf (fun s -> raise (Internal_error s)) msg

src/lib/util/util.mli

@@ -119,3 +119,5 @@ val print_list_pp:
   Format.formatter -> 'a list -> unit
 
 val failwith: ('a, Format.formatter, unit, 'b) format4 -> 'a
+
+val internal_error : ('a, Format.formatter, unit, 'b) format4 -> 'a