[sledge] Make aggregate sizes explicit when constructing equalities

Summary:
In an equation such as `x = ⟨n,a⟩`, `x` is implicitly an aggregate of
size `n` (or else the equation is ill-typed). Make this explicit by
normalizing such equations to e.g. `⟨|⟨n,a⟩|,x⟩ = ⟨n,a⟩`.

Reviewed By: ngorogiannis

Differential Revision: D19358546

fbshipit-source-id: 77f67a0da

sledge/src/llair/term.ml

@@ -621,6 +621,17 @@ let simp_cond cnd thn els =
   | Integer {data} when Z.is_false data -> els
   | _ -> Ap3 (Conditional, cnd, thn, els)
 
+(* aggregate sizes *)
+
+let rec agg_size_exn = function
+  | Ap2 (Memory, n, _) | Ap3 (Extract, _, _, n) -> n
+  | ApN (Concat, a0U) ->
+      Vector.fold a0U ~init:zero ~f:(fun a0I aJ ->
+          simp_add2 a0I (agg_size_exn aJ) )
+  | _ -> invalid_arg "agg_size_exn"
+
+let agg_size e = try Some (agg_size_exn e) with Invalid_argument _ -> None
+
 (* boolean / bitwise *)
 
 let rec is_boolean = function
@@ -682,24 +693,37 @@ let simp_ord x y = Ap2 (Ord, x, y)
 let simp_uno x y = Ap2 (Uno, x, y)
 
 let rec simp_eq x y =
-  match (x, y) with
+  match
-  (* i = j *)
+    match Ordering.of_int (compare x y) with
-  | Integer {data= i}, Integer {data= j} -> bool (Z.equal i j)
+    | Equal -> None
-  (* b = false ==> ¬b *)
+    | Less -> Some (x, y)
-  | b, Integer {data} when Z.is_false data && is_boolean b -> simp_not b
+    | Greater -> Some (y, x)
-  | Integer {data}, b when Z.is_false data && is_boolean b -> simp_not b
+  with
-  (* b = true ==> b *)
+  (* e = e ==> true *)
-  | b, Integer {data} when Z.is_true data && is_boolean b -> b
+  | None -> bool true
-  | Integer {data}, b when Z.is_true data && is_boolean b -> b
+  | Some (x, y) -> (
-  (* e = (c ? t : f) ==> (c ? e = t : e = f) *)
+    match (x, y) with
-  | e, Ap3 (Conditional, c, t, f) | Ap3 (Conditional, c, t, f), e ->
+    (* i = j ==> false when i ≠ j *)
-      simp_cond c (simp_eq e t) (simp_eq e f)
+    | Integer _, Integer _ -> bool false
-  | x, y -> (
+    (* b = false ==> ¬b *)
-    match Int.sign (compare x y) with
+    | b, Integer {data} when Z.is_false data && is_boolean b -> simp_not b
-    (* e = e ==> true *)
+    (* b = true ==> b *)
-    | Zero -> bool true
+    | b, Integer {data} when Z.is_true data && is_boolean b -> b
-    | Neg -> Ap2 (Eq, x, y)
+    (* e = (c ? t : f) ==> (c ? e = t : e = f) *)
-    | Pos -> Ap2 (Eq, y, x) )
+    | e, Ap3 (Conditional, c, t, f) | Ap3 (Conditional, c, t, f), e ->
+        simp_cond c (simp_eq e t) (simp_eq e f)
+    | ( (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _))
+      , (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) ) ->
+        Ap2 (Eq, x, y)
+    (* x = α ==> ⟨x,|α|⟩ = α *)
+    | ( x
+      , ( (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) as
+        a ) )
+     |( ( (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) as
+        a )
+      , x ) ->
+        simp_eq (Ap2 (Memory, agg_size_exn a, x)) a
+    | x, y -> Ap2 (Eq, x, y) )
 
 and simp_dq x y =
   match (x, y) with
@@ -781,17 +805,6 @@ let simp_ashr x y =
   | e, Integer {data} when Z.equal Z.zero data -> e
   | _ -> Ap2 (Ashr, x, y)
 
-(* aggregate sizes *)
-
-let rec agg_size_exn = function
-  | Ap2 (Memory, n, _) | Ap3 (Extract, _, _, n) -> n
-  | ApN (Concat, a0U) ->
-      Vector.fold a0U ~init:zero ~f:(fun a0I aJ ->
-          simp_add2 a0I (agg_size_exn aJ) )
-  | _ -> invalid_arg "agg_size_exn"
-
-let agg_size e = try Some (agg_size_exn e) with Invalid_argument _ -> None
-
 (* memory *)
 
 let empty_agg = ApN (Concat, Vector.of_array [||])

sledge/src/symbheap/equality.ml

@@ -468,7 +468,7 @@ let is_true {sat; rep} =
   sat && Subst.for_alli rep ~f:(fun ~key:a ~data:a' -> Term.equal a a')
 
 let is_false {sat} = not sat
-let entails_eq r d e = Term.equal (canon r d) (canon r e)
+let entails_eq r d e = Term.is_true (canon r (Term.eq d e))
 
 let entails r s =
   Subst.for_alli s.rep ~f:(fun ~key:e ~data:e' -> entails_eq r e e')