[sledge] Refactor: Remove Term.null redundant with Term.zero

Summary:
Previously `null` and `zero` had different sorts/types, but now they
are equivalent.

Reviewed By: jvillard

Differential Revision: D21721023

fbshipit-source-id: 485219f6a

sledge/src/exec.ml

@@ -31,7 +31,7 @@ let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us =
   let arr, us, xs = freshen arr "a" us xs in
   {us; xs; seg= {loc; bas; len; siz; arr}}
 
-let null_eq ptr = Sh.pure (Term.eq Term.null ptr)
+let null_eq ptr = Sh.pure (Term.eq Term.zero ptr)
 
 (* Overwritten variables renaming and remaining modified variables. [ws] are
    the written variables; [rs] are the variables read or in the
@@ -374,7 +374,7 @@ let realloc_spec us reg ptr siz =
   let a2, _, xs = fresh_var "a" us xs in
   let post =
     Sh.or_
-      (Sh.and_ Term.(eq loc null) (Sh.rename sub foot))
+      (Sh.and_ Term.(eq loc zero) (Sh.rename sub foot))
       (Sh.and_
          Term.(
            conditional ~cnd:(le len siz)
@@ -406,7 +406,7 @@ let rallocx_spec us reg ptr siz =
   let a2, _, xs = fresh_var "a" us xs in
   let post =
     Sh.or_
-      (Sh.and_ Term.(eq loc null) (Sh.rename sub pheap))
+      (Sh.and_ Term.(eq loc zero) (Sh.rename sub pheap))
       (Sh.and_
          Term.(
            conditional ~cnd:(le len siz)
@@ -501,7 +501,7 @@ let mallctl_read_spec us r i w n =
   let a, _, xs = fresh_var "a" us xs in
   let foot =
     Sh.and_
-      Term.(eq w null)
+      Term.(eq w zero)
       (Sh.and_ Term.(eq n zero) (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
   in
   let rseg' = {rseg with arr= a} in
@@ -523,7 +523,7 @@ let mallctlbymib_read_spec us p l r i w n =
   let a, _, xs = fresh_var "a" us xs in
   let foot =
     Sh.and_
-      Term.(eq w null)
+      Term.(eq w zero)
       (Sh.and_ Term.(eq n zero) (Sh.star const (Sh.seg rseg)))
   in
   let rseg' = {rseg with arr= a} in
@@ -537,7 +537,7 @@ let mallctlbymib_read_spec us p l r i w n =
 let mallctl_write_spec us r i w n =
   let {us= _; xs; seg} = fresh_seg ~loc:w ~siz:n us in
   let post = Sh.seg seg in
-  let foot = Sh.and_ Term.(eq r null) (Sh.and_ Term.(eq i zero) post) in
+  let foot = Sh.and_ Term.(eq r zero) (Sh.and_ Term.(eq i zero) post) in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 (* { p-[_;_)->⟨W×l,_⟩ * r=0 * i=0 * w-[_;_)->⟨n,_⟩ }
@@ -550,7 +550,7 @@ let mallctlbymib_write_spec us p l r i w n =
   let {us; xs; seg= pseg} = fresh_seg ~loc:p ~siz:wl us in
   let {us= _; xs; seg= wseg} = fresh_seg ~loc:w ~siz:n ~xs us in
   let post = Sh.star (Sh.seg pseg) (Sh.seg wseg) in
-  let foot = Sh.and_ Term.(eq r null) (Sh.and_ Term.(eq i zero) post) in
+  let foot = Sh.and_ Term.(eq r zero) (Sh.and_ Term.(eq i zero) post) in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 let mallctl_specs us r i w n =

sledge/src/sh.ml

@@ -565,7 +565,7 @@ let subst sub q =
 
 let seg pt =
   let us = fv_seg pt in
-  if Term.equal Term.null pt.loc then false_ us
+  if Term.equal Term.zero pt.loc then false_ us
   else {emp with us; heap= [pt]} |> check invariant
 
 (** Update *)
@@ -590,7 +590,7 @@ let is_false = function
       List.exists pure ~f:(fun b ->
           Term.is_false (Equality.normalize cong b) )
       || List.exists heap ~f:(fun seg ->
-             Equality.entails_eq cong seg.loc Term.null )
+             Equality.entails_eq cong seg.loc Term.zero )
 
 let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) =
   let heap = emp.heap in

sledge/src/term.ml

@@ -333,7 +333,6 @@ let rational data =
   else Rational {data} )
   |> check invariant
 
-let null = integer Z.zero
 let zero = integer Z.zero
 let one = integer Z.one
 let minus_one = integer Z.minus_one

sledge/src/term.mli

@@ -171,7 +171,6 @@ val var : Var.t -> t
 
 (* constants *)
 val label : parent:string -> name:string -> t
-val null : t
 val bool : bool -> t
 val true_ : t
 val false_ : t

sledge/src/term_test.ml

@@ -282,9 +282,9 @@ let%test_module _ =
       [%expect {| ((%y_1 < 2) && (3 ≤ %z_2)) |}]
 
     let%expect_test _ =
-      pp (eq z null) ;
-      pp (eq null z) ;
-      pp (dq (eq null z) false_) ;
+      pp (eq z zero) ;
+      pp (eq zero z) ;
+      pp (dq (eq zero z) false_) ;
       [%expect
         {|
         (%z_2 = 0)