diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index b70a5615d..92b7a4398 100644 --- a/src/lib/reasoners/arith.ml +++ b/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 @@ ~$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 + 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); diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 097f00781..a21ff2831 100644 --- a/src/lib/reasoners/bitv.ml +++ b/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 = @@ -1123,13 +1123,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.(~$1 lsl st.sz)) + | Cte true -> E.Ints.((acc + ~$$1) * ~$Z.(~$1 lsl st.sz) - ~$$1) + | Other r -> + let t = term_extract r in + E.Ints.(acc * ~$Z.(~$1 lsl 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.(~$1 lsl st.sz) + + (E.BV.bv2nat t / ~$Z.(~$1 lsl i)) mod ~$Z.(~$1 lsl 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.(~$1 lsl 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 = Canon.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 = Canon.make x in + let r, ctx' = bv2nat r in + r, List.rev_append ctx' ctx + | _ -> + let r, ctx = Canon.make t in + is_mine r, ctx let color _ = assert false diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7060ec1fd..d8d076213 100644 --- a/src/lib/structures/expr.ml +++ b/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,27 @@ 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 ]; _ } -> + let m = match type_info t with Tbitv m -> m | _ -> assert false in + 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.(~$1 lsl 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) @@ -2979,7 +2997,7 @@ module BV = struct (* Arithmetic operations *) let bvneg s = let m = size s in - int2bv m Ints.(~$Z.(pow ~$2 m) - bv2nat s) + int2bv m Ints.(~$Z.(~$1 lsl m) - bv2nat s) let bvadd s t = int2bv (size s) Ints.(bv2nat s + bv2nat t) let bvsub s t = bvadd s (bvneg t) let bvmul s t = int2bv (size s) Ints.(bv2nat s * bv2nat t) diff --git a/src/lib/util/numbers.mli b/src/lib/util/numbers.mli index c5379bbad..dccfa208d 100644 --- a/src/lib/util/numbers.mli +++ b/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 *) diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index f4975df99..3817c5720 100644 --- a/src/lib/util/util.ml +++ b/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 diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 93c7b7e30..31636e8ee 100644 --- a/src/lib/util/util.mli +++ b/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