[sledge] Add: Context.inter

Reviewed By: ngorogiannis

Differential Revision: D23459522

fbshipit-source-id: 7fd86df36

sledge/src/fol.ml

@@ -1533,6 +1533,10 @@ module Context = struct
     let vs', z = Ses.Equality.and_ (vs_to_ses vs) x y in
     (vs_of_ses vs', z)
 
+  let inter vs x y =
+    let vs', z = Ses.Equality.or_ (vs_to_ses vs) x y in
+    (vs_of_ses vs', z)
+
   let interN vs xs =
     let vs', z = Ses.Equality.orN (vs_to_ses vs) xs in
     (vs_of_ses vs', z)

sledge/src/fol.mli

@@ -205,9 +205,13 @@ module Context : sig
   val union : Var.Set.t -> t -> t -> Var.Set.t * t
   (** Union (that is, conjoin) two contexts of assumptions. *)
 
-  val interN : Var.Set.t -> t list -> Var.Set.t * t
+  val inter : Var.Set.t -> t -> t -> Var.Set.t * t
   (** Intersect (that is, disjoin) contexts of assumptions. *)
 
+  val interN : Var.Set.t -> t list -> Var.Set.t * t
+  (** Intersect contexts of assumptions. Possibly weaker than logical
+      disjunction. *)
+
   val rename : t -> Var.Subst.t -> t
   (** Apply a renaming substitution to the context. *)