From 7a9fe9184659e25ec61e25046c7170de45a731ba Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 4 Nov 2020 02:08:12 -0800
Subject: [PATCH] [sledge] Strengthen normalization by flattening nested And
 and Or formulas

Reviewed By: jvillard

Differential Revision: D24549075

fbshipit-source-id: 96b602f04
---
 sledge/src/fol/propositional.ml | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/sledge/src/fol/propositional.ml b/sledge/src/fol/propositional.ml
index 082ab02d4..35e4656c2 100644
--- a/sledge/src/fol/propositional.ml
+++ b/sledge/src/fol/propositional.ml
@@ -94,9 +94,37 @@ module Make (Trm : TERM) = struct
         | _ -> cons ~pos ~neg
 
     let _And ~pos ~neg =
+      let pos, neg =
+        Fmls.fold pos (pos, neg) ~f:(fun b (pos, neg) ->
+            match b with
+            | And {pos= p; neg= n} ->
+                (Fmls.union p (Fmls.remove b pos), Fmls.union n neg)
+            | _ -> (pos, neg) )
+      in
+      let pos, neg =
+        Fmls.fold neg (pos, neg) ~f:(fun b (pos, neg) ->
+            match b with
+            | Or {pos= p; neg= n} ->
+                (Fmls.union n pos, Fmls.union p (Fmls.remove b neg))
+            | _ -> (pos, neg) )
+      in
       _Join (fun ~pos ~neg -> And {pos; neg}) tt ff ~pos ~neg
 
     let _Or ~pos ~neg =
+      let pos, neg =
+        Fmls.fold pos (pos, neg) ~f:(fun b (pos, neg) ->
+            match b with
+            | Or {pos= p; neg= n} ->
+                (Fmls.union p (Fmls.remove b pos), Fmls.union n neg)
+            | _ -> (pos, neg) )
+      in
+      let pos, neg =
+        Fmls.fold neg (pos, neg) ~f:(fun b (pos, neg) ->
+            match b with
+            | And {pos= p; neg= n} ->
+                (Fmls.union n pos, Fmls.union p (Fmls.remove b neg))
+            | _ -> (pos, neg) )
+      in
       _Join (fun ~pos ~neg -> Or {pos; neg}) ff tt ~pos ~neg
 
     let join _Cons zero split_pos_neg p q =