From 1ad2c9025a29c1c8716fc9e2c3452c6c1c6f3afa Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 9 Jan 2020 05:06:32 -0800 Subject: [PATCH] [sledge] Improve Sh docs Reviewed By: ngorogiannis Differential Revision: D19221879 fbshipit-source-id: 5ef052877 --- sledge/src/symbheap/sh.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli index 874d65bed..fe8cee8af 100644 --- a/sledge/src/symbheap/sh.mli +++ b/sledge/src/symbheap/sh.mli @@ -66,9 +66,9 @@ val and_cong : Equality.t -> t -> t val with_pure : Term.t list -> t -> t (** [with_pure pure q] is [{q with pure}], which assumes that [q.pure] and - [pure] are defined in the same vocabulary, induce the same congruence, - etc. It can essentially only be used when [pure] is logically equivalent - to [q.pure], but perhaps syntactically simpler. *) + [pure] are defined in the same vocabulary. Note that [cong] is not + weakened, so if [pure] and [q.pure] do not induce the same congruence, + then the result will have a stronger [cong] than induced by its [pure]. *) val rem_seg : seg -> t -> t (** [star (seg s) (rem_seg s q)] is equivalent to [q], assuming that [s] is @@ -105,7 +105,7 @@ val extend_us : Var.Set.t -> t -> t (** Query *) val is_emp : t -> bool -(** Holds of [emp]. *) +(** Holds of [emp], with any vocabulary, existentials, and congruence. *) val is_false : t -> bool (** Holds only of inconsistent formulas, does not hold of all inconsistent