[sledge] Move mediation between Term and Equality APIs from Sh to Equality

Summary: Add `Equality.and_term` and replace most of `Sh.pure` with it.

Reviewed By: ngorogiannis

Differential Revision: D20029742

fbshipit-source-id: 07c2f1fe6

sledge/src/symbheap/equality.ml

@@ -391,6 +391,8 @@ let invariant r =
 let true_ =
   {xs= Var.Set.empty; sat= true; rep= Subst.empty} |> check invariant
 
+let false_ = {true_ with sat= false}
+
 (** terms are congruent if equal after normalizing subterms *)
 let congruent r a b =
   Term.equal
@@ -561,6 +563,18 @@ let or_ us r s =
   |>
   [%Trace.retn fun {pf} (_, r) -> pf "%a" pp r]
 
+let rec and_term_ us e r =
+  let eq_false b r = and_eq us b Term.false_ r in
+  match (e : Term.t) with
+  | Integer {data} -> if Z.is_false data then false_ else true_
+  | Ap2 (And, a, b) -> and_term_ us a (and_term_ us b r)
+  | Ap2 (Eq, a, b) -> and_eq us a b r
+  | Ap2 (Xor, Integer {data}, a) when Z.is_true data -> eq_false a r
+  | Ap2 (Xor, a, Integer {data}) when Z.is_true data -> eq_false a r
+  | _ -> r
+
+let and_term us e r = and_term_ us e r |> extract_xs
+
 let and_eq us a b r =
   [%Trace.call fun {pf} -> pf "%a = %a@ %a" Term.pp a Term.pp b pp r]
   ;

sledge/src/symbheap/equality.mli

@@ -23,6 +23,9 @@ val true_ : t
 val and_eq : Var.Set.t -> Term.t -> Term.t -> t -> Var.Set.t * t
 (** Conjoin an equation to a relation. *)
 
+val and_term : Var.Set.t -> Term.t -> t -> Var.Set.t * t
+(** Conjoin a (Boolean) term to a relation. *)
+
 val and_ : Var.Set.t -> t -> t -> Var.Set.t * t
 (** Conjunction. *)
 

sledge/src/symbheap/sh.ml

@@ -497,27 +497,17 @@ let or_ q1 q2 =
 let rec pure (e : Term.t) =
   [%Trace.call fun {pf} -> pf "%a" Term.pp e]
   ;
-  let us = Term.fv e in
-  let eq_false b =
-    let xs, cong = Equality.and_eq us b Term.false_ Equality.true_ in
-    exists_fresh xs {emp with us; cong; pure= [e]}
-  in
   ( match e with
-  | Integer {data} -> if Z.is_false data then false_ us else emp
-  (* ¬b ==> false = b *)
-  | Ap2 (Xor, Integer {data}, arg) when Z.is_true data -> eq_false arg
-  | Ap2 (Xor, arg, Integer {data}) when Z.is_true data -> eq_false arg
-  | Ap2 (And, e1, e2) -> star (pure e1) (pure e2)
   | Ap2 (Or, e1, e2) -> or_ (pure e1) (pure e2)
   | Ap3 (Conditional, cnd, thn, els) ->
       or_
         (star (pure cnd) (pure thn))
         (star (pure (Term.not_ cnd)) (pure els))
-  | Ap2 (Eq, e1, e2) ->
-      let xs, cong = Equality.(and_eq us e1 e2 true_) in
+  | _ ->
+      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]}
-  | _ -> {emp with us; pure= [e]} )
+      else exists_fresh xs {emp with us; cong; pure= [e]} )
   |>
   [%Trace.retn fun {pf} q -> pf "%a" pp q ; invariant q]