[sledge] Prefer simple exps over applications as class reps

Reviewed By: jvillard

Differential Revision: D14344293

fbshipit-source-id: 2097959b5

sledge/src/llair/exp.ml

@@ -57,7 +57,6 @@ module rec T : sig
   type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
 
   type t =
-    | App of {op: t; arg: t}
     (* nary: arithmetic, numeric and pointer *)
     | Add of {args: qset; typ: Typ.t}
     | Mul of {args: qset; typ: Typ.t}
@@ -69,6 +68,8 @@ module rec T : sig
     | Var of {id: int; name: string}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
+    (* curried application *)
+    | App of {op: t; arg: t}
     (* numeric constants *)
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
@@ -121,7 +122,6 @@ and T0 : sig
   type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
 
   type t =
-    | App of {op: t; arg: t}
     | Add of {args: qset; typ: Typ.t}
     | Mul of {args: qset; typ: Typ.t}
     | Splat of {byt: t; siz: t}
@@ -130,6 +130,7 @@ and T0 : sig
     | Var of {id: int; name: string}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
+    | App of {op: t; arg: t}
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
     | Eq
@@ -165,7 +166,6 @@ end = struct
   type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
 
   type t =
-    | App of {op: t; arg: t}
     | Add of {args: qset; typ: Typ.t}
     | Mul of {args: qset; typ: Typ.t}
     | Splat of {byt: t; siz: t}
@@ -174,6 +174,7 @@ end = struct
     | Var of {id: int; name: string}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
+    | App of {op: t; arg: t}
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
     | Eq

sledge/src/llair/exp.mli

@@ -26,8 +26,6 @@ type comparator_witness
 type qset = (t, comparator_witness) Qset.t
 
 and t = private
-  | App of {op: t; arg: t}
-      (** Application of function symbol to argument, curried *)
   | Add of {args: qset; typ: Typ.t}  (** Addition *)
   | Mul of {args: qset; typ: Typ.t}  (** Multiplication *)
   | Splat of {byt: t; siz: t}
@@ -40,6 +38,8 @@ and t = private
           non-deterministic approximation of value described by [msg] *)
   | Label of {parent: string; name: string}
       (** Address of named code block within parent function *)
+  | App of {op: t; arg: t}
+      (** Application of function symbol to argument, curried *)
   | Integer of {data: Z.t; typ: Typ.t}
       (** Integer constant, or if [typ] is a [Pointer], null pointer value
           that never refers to an object *)

sledge/src/symbheap/equality_test.ml

@@ -108,13 +108,13 @@ let%test_module _ =
       pp r2 ;
       [%expect
         {|
-          ((i64)(i8) %x_5) = %x_5 = %y_6 = %z_7
+          %x_5 = %y_6 = %z_7 = ((i64)(i8) %x_5)
 
           {sat= true;
-           rep= [[((i64)(i8) %x_5) ↦ ];
-                 [%x_5 ↦ ((i64)(i8) %x_5)];
-                 [%y_6 ↦ ((i64)(i8) %x_5)];
-                 [%z_7 ↦ ((i64)(i8) %x_5)];
+           rep= [[%x_5 ↦ ];
+                 [%y_6 ↦ %x_5];
+                 [%z_7 ↦ %x_5];
+                 [((i64)(i8) %x_5) ↦ %x_5];
                  [(i64)(i8) ↦ ]]} |}]
 
     let%test _ = entails_eq r2 x z
@@ -152,20 +152,20 @@ let%test_module _ =
       pp r3 ;
       [%expect
         {|
-      (%y_6 rem (%y_6 rem %z_7)) = (%y_6 rem %z_7) = %t_1 = %u_2 = %v_3
-      = %w_4 = %x_5 = %z_7
+      %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = (%y_6 rem %v_3)
+      = (%y_6 rem %z_7)
 
       {sat= true;
-       rep= [[(%y_6 rem (%y_6 rem %z_7)) ↦ ];
-             [(%y_6 rem %z_7) ↦ (%y_6 rem (%y_6 rem %z_7))];
-             [(rem %y_6) ↦ ];
-             [%t_1 ↦ (%y_6 rem (%y_6 rem %z_7))];
-             [%u_2 ↦ (%y_6 rem (%y_6 rem %z_7))];
-             [%v_3 ↦ (%y_6 rem (%y_6 rem %z_7))];
-             [%w_4 ↦ (%y_6 rem (%y_6 rem %z_7))];
-             [%x_5 ↦ (%y_6 rem (%y_6 rem %z_7))];
+       rep= [[%t_1 ↦ ];
+             [%u_2 ↦ %t_1];
+             [%v_3 ↦ %t_1];
+             [%w_4 ↦ %t_1];
+             [%x_5 ↦ %t_1];
              [%y_6 ↦ ];
-             [%z_7 ↦ (%y_6 rem (%y_6 rem %z_7))];
+             [%z_7 ↦ %t_1];
+             [(%y_6 rem %v_3) ↦ %t_1];
+             [(%y_6 rem %z_7) ↦ %t_1];
+             [(rem %y_6) ↦ ];
              [rem ↦ ]]} |}]
 
     let%test _ = entails_eq r3 t z