[sledge] Do not normalize class members

Reviewed By: jvillard

Differential Revision: D25756572

fbshipit-source-id: ff329ce0c

sledge/src/fol/context.ml

@@ -428,14 +428,9 @@ type t =
 [@@deriving compare, equal, sexp]
 
 let classes r =
-  let add elt rep cls =
-    if Trm.equal elt rep then cls
-    else Trm.Map.add_multi ~key:rep ~data:elt cls
-  in
   Subst.fold r.rep Trm.Map.empty ~f:(fun ~key:elt ~data:rep cls ->
-      match classify elt with
+      if Trm.equal elt rep then cls
-      | Interpreted | Atomic -> add elt rep cls
+      else Trm.Map.add_multi ~key:rep ~data:elt cls )
-      | Uninterpreted -> add (Trm.map ~f:(Subst.apply r.rep) elt) rep cls )
 
 let cls_of r e =
   let e' = Subst.apply r.rep e in

sledge/src/test/context_test.ml

@@ -16,9 +16,9 @@ let%test_module _ =
     (* let () =
      *   Trace.init ~margin:160
      *     ~config:(Result.get_ok (Trace.parse "+Equality"))
-     *     ()
+     *     () *)
-     *
+
-     * [@@@warning "-32"] *)
+    [@@@warning "-32"]
 
     let printf pp = Format.printf "@\n%a@." pp
     let pp = printf Context.pp_raw
@@ -58,7 +58,7 @@ let%test_module _ =
       pp r3 ;
       [%expect
         {|
-        %t_1 = g(%y_6, %t_1) = g(%y_6, %t_1) = %z_7 = %x_5 = %w_4 = %v_3
+        %t_1 = g(%y_6, %z_7) = g(%y_6, %v_3) = %z_7 = %x_5 = %w_4 = %v_3
         = %u_2
 
       {sat= true;

sledge/src/test/fol_test.ml

@@ -181,7 +181,7 @@ let%test_module _ =
       pp_raw r3 ;
       [%expect
         {|
-        %t_1 = g(%y_6, %t_1) = g(%y_6, %t_1) = %z_7 = %x_5 = %w_4 = %v_3
+        %t_1 = g(%y_6, %z_7) = g(%y_6, %v_3) = %z_7 = %x_5 = %w_4 = %v_3
         = %u_2
 
       {sat= true;