From 209fef22568950992cf6f3feaa0bd1022c10a404 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 22 Apr 2020 08:02:29 -0700 Subject: [PATCH] [sledge] Optimize conjoining fresh equalities Reviewed By: jvillard Differential Revision: D21177358 fbshipit-source-id: 172f0974a --- sledge/src/equality.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/sledge/src/equality.ml b/sledge/src/equality.ml index 2327455b6..bac036fe8 100644 --- a/sledge/src/equality.ml +++ b/sledge/src/equality.ml @@ -542,11 +542,18 @@ let close us r = let and_eq_ us a b r = if not r.sat then r else + let r0 = r in let a' = canon r a in let b' = canon r b in let r = extend a' r in let r = extend b' r in - if Term.equal a' b' then r else close us (merge us a' b' r) + if Term.equal a' b' then r + else + let r = merge us a' b' r in + match (a, b) with + | (Var _ as v), _ when not (in_car r0 v) -> r + | _, (Var _ as v) when not (in_car r0 v) -> r + | _ -> close us r let extract_xs r = (r.xs, {r with xs= Var.Set.empty})