From f7707ff4befac701f0e5ba4870b85b95bada8346 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 2 Mar 2020 08:44:24 -0800 Subject: [PATCH] [sledge] Comments Reviewed By: ngorogiannis Differential Revision: D20120267 fbshipit-source-id: 4ae78bec8 --- sledge/src/symbheap/equality.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml index a483e513b..21892fb8e 100644 --- a/sledge/src/symbheap/equality.ml +++ b/sledge/src/symbheap/equality.ml @@ -156,8 +156,8 @@ end (** Theory Solver *) -(* orient equations s.t. Var < Memory < Extract < Concat < others, then - using height of aggregate nesting, and then using Term.compare *) +(** orient equations s.t. Var < Memory < Extract < Concat < others, then + using height of aggregate nesting, and then using Term.compare *) let orient e f = let compare e f = let rank e = @@ -681,9 +681,10 @@ let subst_invariant us s0 s = type 'a zom = Zero | One of 'a | Many -(* try to solve [p = q] such that [fv (p - q) ⊆ us ∪ xs] and [p - q] has at - most one maximal solvable subterm, [kill], where [fv kill ⊈ us]; solve [p - = q] for [kill]; extend subst mapping [kill] to the solution *) +(** try to solve [p = q] such that [fv (p - q) ⊆ us ∪ xs] and [p - q] + has at most one maximal solvable subterm, [kill], where + [fv kill ⊈ us]; solve [p = q] for [kill]; extend subst mapping [kill] + to the solution *) let solve_poly_eq us p' q' subst = let diff = Term.sub p' q' in let max_solvables_not_ito_us =