From 8d6f3113924d716367adbf703f55f6289f566e4b Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sun, 21 Feb 2021 13:19:03 -0800
Subject: [PATCH] [sledge] Add congruence closure test

Reviewed By: jvillard

Differential Revision: D26400407

fbshipit-source-id: 55157f7d8
---
 sledge/src/test/fol_test.ml | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml
index e260c4384..433b8c0a1 100644
--- a/sledge/src/test/fol_test.ml
+++ b/sledge/src/test/fol_test.ml
@@ -518,6 +518,27 @@ let%test_module _ =
     let%test _ = implies_eq r19 y !0
     let%test _ = implies_eq r19 z !0
 
+    let r20 = of_eqs [(f x, t); (x, y); (f y, u)]
+
+    let%expect_test _ =
+      pp r20 ;
+      pp_raw r20 ;
+      [%expect
+        {|
+          %t_1 = %u_2 = f(%x_5) ∧ %x_5 = %y_6
+
+        { sat= true;
+          rep= [[%t_1 ↦ ];
+                [%u_2 ↦ %t_1];
+                [%x_5 ↦ ];
+                [%y_6 ↦ %x_5];
+                [f(%x_5) ↦ %t_1]];
+          cls= [[%t_1 ↦ {%u_2, f(%x_5)}]; [%x_5 ↦ {%y_6}]];
+          use= [[%x_5 ↦ f(%x_5)]] } |}]
+
+    (* f(x) = t; x = y; f(y) = u ⊢ t = u *)
+    let%test _ = implies_eq r20 t u
+
     let%expect_test _ =
       let f =
         Formula.(