[sledge] Refactor: Term.disjuncts out of Sh.pure

Summary:
It is suboptimal for `Sh` to destruct terms with detailed knowledge of
their representation. So add `Term.disjuncts` to obtain the toplevel
disjuncts of a term.

Reviewed By: jvillard

Differential Revision: D21721016

fbshipit-source-id: 809da9b1b

sledge/src/sh.ml

@@ -521,22 +521,14 @@ let orN = function
   | [q] -> q
   | q :: qs -> List.fold ~f:or_ ~init:q qs
 
-let rec pure (e : Term.t) =
+let pure (e : Term.t) =
   [%Trace.call fun {pf} -> pf "%a" Term.pp e]
   ;
-  ( match e with
+  List.fold (Term.disjuncts e) ~init:(false_ Var.Set.empty) ~f:(fun q b ->
-  | Or es ->
+      let us = Term.fv b in
-      let e0, e1N = Term.Set.pop_exn es in
+      let xs, cong = Equality.(and_term us b true_) in
-      Term.Set.fold e1N ~init:(pure e0) ~f:(fun q e -> or_ q (pure e))
-  | Ap3 (Conditional, cnd, thn, els) ->
-      or_
-        (star (pure cnd) (pure thn))
-        (star (pure (Term.not_ cnd)) (pure els))
-  | _ ->
-      let us = Term.fv e in
-      let xs, cong = Equality.(and_term us e true_) in
       if Equality.is_false cong then false_ us
-      else exists_fresh xs {emp with us; cong; pure= [e]} )
+      else or_ q (exists_fresh xs {emp with us; cong; pure= [b]}) )
   |>
   [%Trace.retn fun {pf} q ->
     pf "%a" pp q ;

sledge/src/term.ml

@@ -1199,6 +1199,21 @@ let rec fold_map_rec_pre e ~init:s ~f =
   | Some (s, e') -> (s, e')
   | None -> fold_map ~f:(fun s e -> fold_map_rec_pre ~f ~init:s e) ~init:s e
 
+let disjuncts e =
+  let rec disjuncts_ e =
+    match e with
+    | Or es ->
+        let e0, e1N = Set.pop_exn es in
+        Set.fold e1N ~init:(disjuncts_ e0) ~f:(fun cs e ->
+            Set.union cs (disjuncts_ e) )
+    | Ap3 (Conditional, cnd, thn, els) ->
+        Set.add
+          (Set.of_ (and_ (orN (disjuncts_ cnd)) (orN (disjuncts_ thn))))
+          (and_ (orN (disjuncts_ (not_ cnd))) (orN (disjuncts_ els)))
+    | _ -> Set.of_ e
+  in
+  Set.elements (disjuncts_ e)
+
 let rename sub e =
   map_rec_pre e ~f:(function
     | Var _ as v -> Some (Var.Subst.apply sub v)

sledge/src/term.mli

@@ -253,6 +253,7 @@ val fold_map : t -> init:'a -> f:('a -> t -> 'a * t) -> 'a * t
 val fold_map_rec_pre :
   t -> init:'a -> f:('a -> t -> ('a * t) option) -> 'a * t
 
+val disjuncts : t -> t list
 val rename : Var.Subst.t -> t -> t
 
 (** Traverse *)