[sledge] Pass universal context to Equality.solve

Summary:
In order for Equality.solve to generate fresh variables, it needs to
be passed the universal context with respect to which variables must
be chosen fresh.

Reviewed By: ngorogiannis

Differential Revision: D19286630

fbshipit-source-id: ebbedd954

sledge/src/symbheap/equality.ml

@@ -142,7 +142,7 @@ let rec is_constant e =
       Qset.for_all ~f:(fun arg _ -> is_constant arg) args
   | Label _ | Float _ | Integer _ -> true
 
-let solve e f =
+let solve _ e f =
   [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp e Term.pp f]
   ;
   let rec solve_ e f s =
@@ -314,10 +314,10 @@ let rec extend a r =
 
 let extend a r = extend a r |> check invariant
 
-let merge a b r =
+let merge us a b r =
   [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Term.pp a Term.pp b pp r]
   ;
-  ( match solve a b with
+  ( match solve us a b with
   | Some s -> {r with rep= Subst.compose r.rep s}
   | None -> {r with sat= false} )
   |>
@@ -338,17 +338,17 @@ let find_missing r =
           then return (Some (a', b')) ) ) ;
   None
 
-let rec close r =
+let rec close us r =
   if not r.sat then r
   else
     match find_missing r with
-    | Some (a', b') -> close (merge a' b' r)
+    | Some (a', b') -> close us (merge us a' b' r)
     | None -> r
 
-let close r =
+let close us r =
   [%Trace.call fun {pf} -> pf "%a" pp r]
   ;
-  close r
+  close us r
   |>
   [%Trace.retn fun {pf} r' ->
     pf "%a" pp_diff (r, r') ;
@@ -356,7 +356,7 @@ let close r =
 
 (** Exposed interface *)
 
-let and_eq a b r =
+let and_eq us a b r =
   [%Trace.call fun {pf} -> pf "%a = %a@ %a" Term.pp a Term.pp b pp r]
   ;
   ( if not r.sat then r
@@ -365,7 +365,7 @@ let and_eq a b r =
     let b' = canon r b in
     let r = extend a' r in
     let r = extend b' r in
-    if Term.equal a' b' then r else close (merge a' b' r) )
+    if Term.equal a' b' then r else close us (merge us a' b' r) )
   |>
   [%Trace.retn fun {pf} r' ->
     pf "%a" pp_diff (r, r') ;
@@ -400,16 +400,16 @@ let difference r a b =
   [%Trace.retn fun {pf} ->
     function Some d -> pf "%a" Z.pp_print d | None -> pf ""]
 
-let and_ r s =
+let and_ us r s =
   if not r.sat then r
   else if not s.sat then s
   else
     let s, r =
       if Subst.length s.rep <= Subst.length r.rep then (s, r) else (r, s)
     in
-    Subst.fold s.rep ~init:r ~f:(fun ~key:e ~data:e' r -> and_eq e e' r)
+    Subst.fold s.rep ~init:r ~f:(fun ~key:e ~data:e' r -> and_eq us e e' r)
 
-let or_ r s =
+let or_ us r s =
   [%Trace.call fun {pf} -> pf "@[<hv 1>   %a@ @<2>∨ %a@]" pp r pp s]
   ;
   ( if not s.sat then r
@@ -421,7 +421,7 @@ let or_ r s =
             ~init:([rep], rs)
             ~f:(fun (reps, rs) exp ->
               match List.find ~f:(entails_eq r exp) reps with
-              | Some rep -> (reps, and_eq exp rep rs)
+              | Some rep -> (reps, and_eq us exp rep rs)
               | None -> (exp :: reps, rs) )
           |> snd )
     in

sledge/src/symbheap/equality.mli

@@ -20,13 +20,13 @@ include Invariant.S with type t := t
 val true_ : t
 (** The diagonal relation, which only equates each term with itself. *)
 
-val and_eq : Term.t -> Term.t -> t -> t
+val and_eq : Var.Set.t -> Term.t -> Term.t -> t -> t
 (** Conjoin an equation to a relation. *)
 
-val and_ : t -> t -> t
+val and_ : Var.Set.t -> t -> t -> t
 (** Conjunction. *)
 
-val or_ : t -> t -> t
+val or_ : Var.Set.t -> t -> t -> t
 (** Disjunction. *)
 
 val rename : t -> Var.Subst.t -> t

sledge/src/symbheap/equality_test.ml

@@ -15,7 +15,6 @@ let%test_module _ =
     let printf pp = Format.printf "@\n%a@." pp
     let pp = printf pp
     let pp_classes = Format.printf "@\n@[<hv>  %a@]@." pp_classes
-    let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r)
     let ( ! ) i = Term.integer (Z.of_int i)
     let ( + ) = Term.add
     let ( - ) = Term.sub
@@ -29,7 +28,7 @@ let%test_module _ =
     let w_, wrt = Var.fresh "w" ~wrt
     let x_, wrt = Var.fresh "x" ~wrt
     let y_, wrt = Var.fresh "y" ~wrt
-    let z_, _ = Var.fresh "z" ~wrt
+    let z_, wrt = Var.fresh "z" ~wrt
     let t = Term.var t_
     let u = Term.var u_
     let v = Term.var v_
@@ -37,6 +36,10 @@ let%test_module _ =
     let x = Term.var x_
     let y = Term.var y_
     let z = Term.var z_
+    let and_eq = and_eq wrt
+    let and_ = and_ wrt
+    let or_ = or_ wrt
+    let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r)
     let f1 = of_eqs [(!0, !1)]
 
     let%test _ = is_false f1

sledge/src/symbheap/sh.ml

@@ -380,7 +380,7 @@ let and_cong cong q =
   [%Trace.call fun {pf} -> pf "%a@ %a" Equality.pp cong pp q]
   ;
   let q = extend_us (Equality.fv cong) q in
-  let cong = Equality.and_ q.cong cong in
+  let cong = Equality.and_ q.us q.cong cong in
   (if Equality.is_false cong then false_ q.us else {q with cong})
   |>
   [%Trace.retn fun {pf} q -> pf "%a" pp q ; invariant q]
@@ -406,7 +406,7 @@ let star q1 q2 =
       let {us= us1; xs= xs1; cong= c1; pure= p1; heap= h1; djns= d1} = q1 in
       let {us= us2; xs= xs2; cong= c2; pure= p2; heap= h2; djns= d2} = q2 in
       assert (Set.equal us (Set.union us1 us2)) ;
-      let cong = Equality.and_ c1 c2 in
+      let cong = Equality.and_ us c1 c2 in
       if Equality.is_false cong then false_ us
       else
         { us
@@ -462,7 +462,7 @@ let rec pure (e : Term.t) =
   ;
   let us = Term.fv e in
   let eq_false b =
-    let cong = Equality.and_eq b Term.false_ Equality.true_ in
+    let cong = Equality.and_eq us b Term.false_ Equality.true_ in
     {emp with us; cong; pure= [e]}
   in
   ( match e with
@@ -477,7 +477,7 @@ let rec pure (e : Term.t) =
         (star (pure cnd) (pure thn))
         (star (pure (Term.not_ cnd)) (pure els))
   | Ap2 (Eq, e1, e2) ->
-      let cong = Equality.(and_eq e1 e2 true_) in
+      let cong = Equality.(and_eq us e1 e2 true_) in
       if Equality.is_false cong then false_ us
       else {emp with us; cong; pure= [e]}
   | _ -> {emp with us; pure= [e]} )