[Bitv] Add support for the SMT-LIB2's BV primitives

src/lib/frontend/d_cnf.ml

@@ -940,8 +940,7 @@ let rec mk_expr
             E.mk_term (Sy.Op Sy.Minus) [e1; aux_mk_expr x] ty
 
           | B.Bitv_extract { i; j; _ }, [x] ->
-            E.mk_term
-              (Sy.Op (Sy.Extract (j, i))) [aux_mk_expr x] (Ty.Tbitv (i - j + 1))
+            E.mk_bvextract j i (aux_mk_expr x)
 
           | B.Destructor { case; field; adt; _ }, [x] ->
             begin match DT.definition adt with
@@ -1020,11 +1019,132 @@ let rec mk_expr
             in
             semantic_trigger ~loc ?var trigger
 
+          | B.Bitv_repeat { n; k }, [t] ->
+            E.mk_term (Op (BV_repeat k)) [aux_mk_expr t] (Tbitv (n*k))
+
+          | B.Bitv_zero_extend { n; k }, [t] ->
+            E.mk_bvextend false n k (aux_mk_expr t)
+
+          | B.Bitv_sign_extend { n; k }, [t] ->
+            E.mk_bvextend true n k (aux_mk_expr t)
+
+          | B.Bitv_rotate_left { n; i }, [t] ->
+            let t' = aux_mk_expr t in
+            if n < 2 then t' else
+              E.mk_term (Op (BV_rotate (-i))) [t'] (Tbitv n)
+
+          | B.Bitv_rotate_right { n; i }, [t] ->
+            let t' = aux_mk_expr t in
+            if n < 2 then t' else
+              E.mk_term (Op (BV_rotate i)) [t'] (Tbitv n)
+
+          | B.Bitv_neg n, [t] ->
+            E.mk_term (Op BVneg) [aux_mk_expr t] (Tbitv n)
+
+          | B.Bitv_not n, [t] ->
+            E.mk_term (Op BVnot) [aux_mk_expr t] (Tbitv n)
+
           (* Binary applications *)
 
           | B.Bitv_concat { n; m; }, [ x; y ] ->
-            let rty = Ty.Tbitv (n+m) in
-            E.mk_term (Sy.Op Sy.Concat) [aux_mk_expr x; aux_mk_expr y] rty
+            E.mk_bvconcat (aux_mk_expr x) (aux_mk_expr y) (n + m)
+
+          | B.Bitv_or n, [ x; y ] ->
+            E.mk_term
+              (Op Sy.BVor) [aux_mk_expr x; aux_mk_expr y] (Tbitv n)
+
+          | B.Bitv_and n, [ x; y ] ->
+            E.mk_term
+              (Op Sy.BVand) [aux_mk_expr x; aux_mk_expr y] (Tbitv n)
+
+          | B.Bitv_nor n, [ x; y ] ->
+            E.mk_term
+              (Op Sy.BVnor) [aux_mk_expr x; aux_mk_expr y] (Tbitv n)
+
+          | B.Bitv_nand n, [ x; y ] ->
+            E.mk_term
+              (Op Sy.BVnand) [aux_mk_expr x; aux_mk_expr y] (Tbitv n)
+
+          | B.Bitv_xor n, [ x; y ] ->
+            E.mk_term
+              (Op Sy.BVxor) [aux_mk_expr x; aux_mk_expr y] (Tbitv n)
+
+          | B.Bitv_xnor n, [ x; y ] ->
+            E.mk_term
+              (Op Sy.BVxnor) [aux_mk_expr x; aux_mk_expr y] (Tbitv n)
+
+          | B.Bitv_comp n, [ x; y ] ->
+            E.mk_term
+              (Op Sy.BVcomp) [aux_mk_expr x; aux_mk_expr y] (Tbitv n)
+
+          | B.Bitv_add n, [ x; y ] ->
+            E.mk_term
+              (Op Sy.BVadd) [aux_mk_expr x; aux_mk_expr y] (Tbitv n)
+
+          | B.Bitv_sub n, [ x; y ] ->
+            E.mk_term
+              (Op Sy.BVsub) [aux_mk_expr x; aux_mk_expr y] (Tbitv n)
+
+          | B.Bitv_mul n, [ x; y ] ->
+            E.mk_term
+              (Op Sy.BVmul) [aux_mk_expr x; aux_mk_expr y] (Tbitv n)
+
+          | B.Bitv_shl n, [ x; y ] ->
+            E.mk_term
+              (Op Sy.BVshl) [aux_mk_expr x; aux_mk_expr y] (Tbitv n)
+
+          | B.Bitv_lshr n, [ x; y ] ->
+            E.mk_bvlshr n (aux_mk_expr x) (aux_mk_expr y)
+
+          (* BV operators that produce ITEs or booleans are partially expanded
+             here instead of in the theory. Currently it is not possible to
+             produce ITEs in the Bit-vector theory. *)
+
+          | B.Bitv_udiv n, [ x; y ] ->
+            E.mk_bvudiv n (aux_mk_expr x) (aux_mk_expr y)
+
+          | B.Bitv_urem n, [ x; y ] ->
+            E.mk_bvurem n (aux_mk_expr x) (aux_mk_expr y)
+
+          | B.Bitv_sdiv n, [ x; y ] ->
+            E.mk_bvsdiv n (aux_mk_expr x) (aux_mk_expr y)
+
+          | B.Bitv_srem n, [ x; y ] ->
+            E.mk_bvsrem n (aux_mk_expr x) (aux_mk_expr y)
+
+          | B.Bitv_smod n, [ x; y ] ->
+            E.mk_bvsmod n (aux_mk_expr x) (aux_mk_expr y)
+
+          | B.Bitv_ashr n, [ x; y ] ->
+            E.mk_bvashr n (aux_mk_expr x) (aux_mk_expr y)
+
+          | B.Bitv_ult n, [ x; y ] ->
+            E.mk_bvult n (aux_mk_expr x) (aux_mk_expr y)
+
+          | B.Bitv_ule n, [ x; y ] ->
+            E.mk_bvule n (aux_mk_expr x) (aux_mk_expr y)
+
+          | B.Bitv_ugt n, [ x; y ] ->
+            E.mk_bvult n (aux_mk_expr y) (aux_mk_expr x)
+
+          | B.Bitv_uge n, [ x; y ] ->
+            E.mk_bvule n (aux_mk_expr y) (aux_mk_expr x)
+
+          | B.Bitv_slt n, [ x; y ] ->
+            if n = 0 then E.faux else
+              E.mk_bvslt n (aux_mk_expr x) (aux_mk_expr y)
+
+          | B.Bitv_sle n, [ x; y ] ->
+            if n = 0 then E.faux else
+              E.mk_bvsle n (aux_mk_expr x) (aux_mk_expr y)
+
+          | B.Bitv_sgt n, [ x; y ] ->
+            if n = 0 then E.faux else
+              E.mk_bvslt n (aux_mk_expr y) (aux_mk_expr x)
+
+          | B.Bitv_sge n, [ x; y ] ->
+            if n = 0 then E.faux else
+              E.mk_bvsle n (aux_mk_expr y) (aux_mk_expr x)
 
           | B.Select, [ x; y ] ->
             let rty = dty_to_ty term_ty in
@@ -1141,8 +1261,7 @@ let rec mk_expr
 
           | B.Add ty, _ ->
             let rty = if ty == `Int then Ty.Tint else Treal in
-            let sy = Sy.Op Sy.Plus in
-            mk_add aux_mk_expr sy rty args
+            mk_add aux_mk_expr (Sy.Op Sy.Plus) rty args
 
           | B.Sub ty, h :: t ->
             let rty = if ty == `Int then Ty.Tint else Treal in

src/lib/reasoners/arith.ml

@@ -119,8 +119,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
-         | Integer_round) -> true
+         | Pow | Integer_log2 | Integer_round) -> true
     | _ -> false
 
   let empty_polynome ty = P.create [] Q.zero ty
@@ -721,7 +720,14 @@ module Shostak
     | Sy.Op (Sy.Plus | Sy.Minus) -> true
     | _ -> false
 
-  let term_extract _ = None, false
+  let term_extract r =
+    match P.extract r with
+    | None -> None, false
+    | Some pt ->
+      match P.is_const pt, P.type_info pt with
+      | Some q, Ty.Tint ->
+        Some (E.int (Q.to_string q)), false
+      | _ -> None, false (* TODO: extract for the other types? *)
 
   let abstract_selectors p acc =
     let p, acc = P.abstract_selectors p acc in