From d1de5db6c88036c5e7693b1de8ca6e81e845c08d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 24 Mar 2020 15:00:30 -0700 Subject: [PATCH] [sledge] Document Equality variable context handling Summary: Many Equality functions accept and return a set of variables, document their function. Reviewed By: ngorogiannis Differential Revision: D20596492 fbshipit-source-id: b91ae7197 --- sledge/lib/equality.mli | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/sledge/lib/equality.mli b/sledge/lib/equality.mli index ffae2a869..47c39687d 100644 --- a/sledge/lib/equality.mli +++ b/sledge/lib/equality.mli @@ -6,7 +6,12 @@ *) (** Constraints representing equivalence relations over uninterpreted - functions and linear rational arithmetic *) + functions and linear rational arithmetic. + + Functions that return relations that might be stronger than their + argument relations accept and return a set of variables. The input set + is the variables with which any generated variables must be chosen + fresh, and the output set is the variables that have been generated. *) type t [@@deriving compare, equal, sexp]