diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml index f28876b77..4949f74d4 100644 --- a/sledge/src/import/import.ml +++ b/sledge/src/import/import.ml @@ -310,5 +310,12 @@ module Z = struct | Sexp.Atom s -> Z.of_string s | _ -> assert false + (* the signed 1-bit integers are -1 and 0 *) + let true_ = Z.minus_one + let false_ = Z.zero + let of_bool = function true -> true_ | false -> false_ + let is_true = Z.equal true_ + let is_false = Z.equal false_ + include Z end diff --git a/sledge/src/import/import.mli b/sledge/src/import/import.mli index 0d80c9536..8e7b6b8b0 100644 --- a/sledge/src/import/import.mli +++ b/sledge/src/import/import.mli @@ -250,4 +250,9 @@ module Z : sig val t_of_sexp : Sexp.t -> t val sexp_of_t : t -> Sexp.t val pp : t pp + val true_ : t + val false_ : t + val of_bool : bool -> t + val is_true : t -> bool + val is_false : t -> bool end diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 7bbcd7766..51643fe88 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -11,13 +11,6 @@ module Z = struct include Z - (* the signed 1-bit integers are -1 and 0 *) - let true_ = Z.minus_one - let false_ = Z.zero - let of_bool = function true -> true_ | false -> false_ - let is_true = Z.equal true_ - let is_false = Z.equal false_ - (** Interpret as a bounded integer with specified signedness and width. *) let clamp ~signed bits z = if signed then Z.signed_extract z 0 bits else Z.extract z 0 bits diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 06f0659e6..7ac767768 100644 --- a/sledge/src/symbheap/sh.ml +++ b/sledge/src/symbheap/sh.ml @@ -134,7 +134,7 @@ let fv q = fv_union Var.Set.empty q let invariant_pure = function | Exp.Integer {data; typ} -> assert (Typ.equal Typ.bool typ) ; - assert (not (Z.equal Z.zero data)) + assert (not (Z.is_false data)) | _ -> assert true let invariant_seg _ = () @@ -381,7 +381,7 @@ let rec pure (e : Exp.t) = let us = Exp.fv e in ( match e with | Integer {data; typ= Integer {bits= 1}} -> - if Z.equal Z.zero data then false_ us else emp + if Z.is_false data then false_ us else emp | App {op= App {op= And; arg= e1}; arg= e2} -> star (pure e1) (pure e2) | App {op= App {op= Or; arg= e1}; arg= e2} -> or_ (pure e1) (pure e2) | App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els}