From 19cc35b65e670f5055969f7bf9767ded01b8c66d Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 4 Sep 2020 13:37:01 -0700
Subject: [PATCH] [sledge] Add: Context.inter

Reviewed By: ngorogiannis

Differential Revision: D23459522

fbshipit-source-id: 7fd86df36
---
 sledge/src/fol.ml  | 4 ++++
 sledge/src/fol.mli | 6 +++++-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 557d18923..935c0d7ec 100644
--- a/sledge/src/fol.ml
+++ b/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)
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index d7982c8b6..ef197b3f1 100644
--- a/sledge/src/fol.mli
+++ b/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. *)