From e33c7f6ce09934f7348ef7794183cfe57aed4a1a Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 21 Feb 2021 13:19:47 -0800 Subject: [PATCH] [sledge] Change encoding of program var ids to preserve original order Summary: Negating the ids of program variables leads to inverting the order on them. This is logically fine, the order is still a valid total order. But it can lead to choosing younger variables as equality class representatives over older variables, and thereby lead to more churn as adding an equality is more likely to cause a change of representative, and hence additional normalizing rewrites. Reviewed By: jvillard Differential Revision: D26451304 fbshipit-source-id: eb20d1901 --- sledge/src/fol/trm.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index c73c385ad..726287c99 100644 --- a/sledge/src/fol/trm.ml +++ b/sledge/src/fol/trm.ml @@ -78,7 +78,8 @@ module Trm3 = struct let pf fmt = pp_boxed fs fmt in match trm with | Var {id; name} -> ( - if id < 0 then Trace.pp_styled `Bold "%%%s!%i" fs name (-id) + if id < 0 then + Trace.pp_styled `Bold "%%%s!%i" fs name (id + Int.max_int) else match strength trm with | None -> Format.fprintf fs "%%%s_%i" name id @@ -168,7 +169,7 @@ module Var = struct let program ?(name = "") ~id = assert (id > 0) ; - make ~id:(-id) ~name + make ~id:(id - Int.max_int) ~name let identified ~name ~id = make ~id ~name let of_ v = v |> check invariant