[sledge] Move ops on signed 1-bit Z integers to import

Summary:
The convenience wrappers for operations on signed 1-bit integers
represented by Z.t are not specific to Exp.

Reviewed By: ngorogiannis

Differential Revision: D17665252

fbshipit-source-id: d4b58e2a6

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

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

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

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}