[sledge] Switch from Base.Map to Containers.Map

Summary:
The form of the Base containers interface, in particular the way
comparison functions are passed using Comparators, is slower than
standard functors. Also Base.Map is missing some operations, such as
efficient merge and union.

Reviewed By: jvillard

Differential Revision: D24306047

fbshipit-source-id: e1623b693

sledge/nonstdlib/map.ml

@@ -11,24 +11,39 @@ include Map_intf
 module Make (Key : sig
   type t [@@deriving compare, sexp_of]
 end) : S with type key = Key.t = struct
-  module KeyMap = Core.Map.Make_plain (Key)
-  module Key = KeyMap.Key
+  module M = CCMap.Make (Key)
 
   type key = Key.t
-
-  include KeyMap.Tree
-
-  let compare = compare_direct
-
-  let to_map t =
-    Core.Map.Using_comparator.of_tree ~comparator:Key.comparator t
-
-  let of_map m = Base.Map.Using_comparator.to_tree m
-
-  let merge_skewed x y ~combine =
-    of_map (Core.Map.merge_skewed (to_map x) (to_map y) ~combine)
-
-  let map_endo t ~f = map_endo map t ~f
+  type 'a t = 'a M.t [@@deriving compare, equal]
+
+  let sexp_of_t sexp_of_data m =
+    M.to_list m
+    |> Sexplib.Conv.sexp_of_list
+         (Sexplib.Conv.sexp_of_pair Key.sexp_of_t sexp_of_data)
+
+  module Provide_of_sexp (Key : sig
+    type t = key [@@deriving of_sexp]
+  end) =
+  struct
+    let t_of_sexp data_of_sexp s =
+      s
+      |> Sexplib.Conv.list_of_sexp
+           (Sexplib.Conv.pair_of_sexp Key.t_of_sexp data_of_sexp)
+      |> M.of_list
+  end
+
+  let empty = M.empty
+  let singleton = M.singleton
+  let add_exn m ~key ~data = M.add key data m
+  let set m ~key ~data = M.add key data m
+
+  let add_multi m ~key ~data =
+    M.update key
+      (function Some vs -> Some (data :: vs) | None -> Some [data])
+      m
+
+  let remove m key = M.remove key m
+  let merge l r ~f = M.merge_safe l r ~f:(fun key -> f ~key)
 
   let merge_endo t u ~f =
     let change = ref false in
@@ -43,49 +58,107 @@ end) : S with type key = Key.t = struct
     in
     if !change then t' else t
 
-  let fold_until m ~init ~f ~finish =
-    let fold m ~init ~f =
-      let f ~key ~data s = f s (key, data) in
-      fold m ~init ~f
-    in
-    let f s (k, v) = f ~key:k ~data:v s in
-    Container.fold_until ~fold ~init ~f ~finish m
-
-  let root_key_exn m =
-    let@ {return} = with_return in
-    binary_search_segmented m `Last_on_left ~segment_of:(fun ~key ~data:_ ->
-        return key )
-    |> ignore ;
-    raise (Not_found_s (Atom __LOC__))
-
-  let choose_exn m =
-    let@ {return} = with_return in
-    binary_search_segmented m `Last_on_left ~segment_of:(fun ~key ~data ->
-        return (key, data) )
-    |> ignore ;
-    raise (Not_found_s (Atom __LOC__))
+  let merge_skewed x y ~combine =
+    M.union (fun key v1 v2 -> Some (combine ~key v1 v2)) x y
 
-  let choose m = try Some (choose_exn m) with Not_found_s _ -> None
-  let pop m = choose m |> Option.map ~f:(fun (k, v) -> (k, v, remove m k))
+  let union x y ~f = M.union f x y
+  let is_empty = M.is_empty
 
-  let pop_min_elt m =
-    min_elt m |> Option.map ~f:(fun (k, v) -> (k, v, remove m k))
+  let root_key m =
+    let exception Found in
+    let found = ref None in
+    try
+      M.find_first
+        (fun key ->
+          found := Some key ;
+          raise Found )
+        m
+      |> ignore ;
+      None
+    with
+    | Found -> !found
+    | Not_found -> None
+
+  let root_binding m =
+    let exception Found in
+    let found = ref None in
+    try
+      M.for_all
+        (fun key data ->
+          found := Some (key, data) ;
+          raise Found )
+        m
+      |> ignore ;
+      None
+    with
+    | Found -> !found
+    | Not_found -> None
 
   let is_singleton m =
-    try
-      let l, _, r = split m (root_key_exn m) in
-      is_empty l && is_empty r
-    with Not_found_s _ -> false
+    match root_key m with
+    | Some k ->
+        let l, _, r = M.split k m in
+        is_empty l && is_empty r
+    | None -> false
+
+  let length = M.cardinal
+  let choose_key = root_key
+  let choose = root_binding
+  let choose_exn m = CCOpt.get_exn (choose m)
+  let min_binding = M.min_binding_opt
+  let mem m k = M.mem k m
+  let find_exn m k = M.find k m
+  let find m k = M.find_opt k m
+
+  let find_multi m k =
+    match M.find_opt k m with None -> [] | Some vs -> vs
 
   let find_and_remove m k =
     let found = ref None in
     let m =
-      change m k ~f:(fun v ->
+      M.update k
+        (fun v ->
           found := v ;
           None )
+        m
     in
     Option.map ~f:(fun v -> (v, m)) !found
 
+  let pop m = choose m |> CCOpt.map (fun (k, v) -> (k, v, remove m k))
+
+  let pop_min_binding m =
+    min_binding m |> CCOpt.map (fun (k, v) -> (k, v, remove m k))
+
+  let change m key ~f = M.update key f m
+  let update m k ~f = M.update k (fun v -> Some (f v)) m
+  let map m ~f = M.map f m
+  let mapi m ~f = M.mapi (fun key data -> f ~key ~data) m
+  let map_endo t ~f = map_endo map t ~f
+  let filter_mapi m ~f = M.filter_map (fun key data -> f ~key ~data) m
+  let iter m ~f = M.iter (fun _ data -> f data) m
+  let iteri m ~f = M.iter (fun key data -> f ~key ~data) m
+  let existsi m ~f = M.exists (fun key data -> f ~key ~data) m
+  let for_alli m ~f = M.for_all (fun key data -> f ~key ~data) m
+  let fold m ~init ~f = M.fold (fun key data acc -> f ~key ~data acc) m init
+  let to_alist ?key_order:_ = M.to_list
+  let data m = Iter.to_list (M.values m)
+
+  let to_iter2 l r =
+    let seq = ref Iter.empty in
+    M.merge_safe l r ~f:(fun k vv ->
+        seq := Iter.cons (k, vv) !seq ;
+        None )
+    |> ignore ;
+    !seq
+
+  let symmetric_diff ~data_equal l r =
+    Iter.filter_map (to_iter2 l r) ~f:(fun (k, vv) ->
+        match vv with
+        | `Both (lv, rv) when data_equal lv rv -> None
+        | `Both vv -> Some (k, `Unequal vv)
+        | `Left lv -> Some (k, `Left lv)
+        | `Right rv -> Some (k, `Right rv) )
+
   let pp pp_k pp_v fs m =
     Format.fprintf fs "@[<1>[%a]@]"
       (List.pp ",@ " (fun fs (k, v) ->
@@ -101,7 +174,7 @@ end) : S with type key = Key.t = struct
       | k, `Unequal vv ->
           Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_key k pp_diff_val vv
     in
-    let sd = Sequence.to_list (symmetric_diff ~data_equal x y) in
+    let sd = Iter.to_list (symmetric_diff ~data_equal x y) in
     if not (List.is_empty sd) then
       Format.fprintf fs "[@[<hv>%a@]];@ " (List.pp ";@ " pp_diff_elt) sd
 end

sledge/nonstdlib/map_intf.ml

@@ -7,60 +7,127 @@
 
 open NS0
 
+exception Not_found = Stdlib.Not_found
+
 module type S = sig
   type key
+  type +'a t [@@deriving compare, equal, sexp_of]
 
-  module Key : sig
-    type t = key
-
-    include Comparator.S with type t := t
+  module Provide_of_sexp (_ : sig
+    type t = key [@@deriving of_sexp]
+  end) : sig
+    val t_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a t
   end
 
-  include Core_kernel.Map_intf.Make_S_plain_tree(Key).S
+  (** {1 Construct} *)
 
-  val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
-  val is_singleton : 'a t -> bool
+  val empty : 'a t
+  val singleton : key -> 'a -> 'a t
+  val add_exn : 'a t -> key:key -> data:'a -> 'a t
+  val set : 'a t -> key:key -> data:'a -> 'a t
+  val add_multi : 'a list t -> key:key -> data:'a -> 'a list t
+  val remove : 'a t -> key -> 'a t
 
-  val map_endo : 'a t -> f:('a -> 'a) -> 'a t
-  (** Like map, but specialized to require [f] to be an endofunction, which
-      enables preserving [==] if [f] preserves [==] of every element. *)
+  val merge :
+       'a t
+    -> 'b t
+    -> f:
+         (   key:key
+          -> [`Left of 'a | `Both of 'a * 'b | `Right of 'b]
+          -> 'c option)
+    -> 'c t
 
   val merge_endo :
        'a t
     -> 'b t
     -> f:
          (   key:key
-          -> [`Both of 'a * 'b | `Left of 'a | `Right of 'b]
+          -> [`Left of 'a | `Both of 'a * 'b | `Right of 'b]
           -> 'a option)
     -> 'a t
   (** Like merge, but specialized to require [f] to preserve the type of the
       left argument, which enables preserving [==] if [f] preserves [==] of
-      every element. *)
+      every value. *)
 
   val merge_skewed :
     'a t -> 'a t -> combine:(key:key -> 'a -> 'a -> 'a) -> 'a t
 
-  val fold_until :
-       'v t
-    -> init:'a
-    -> f:(key:key -> data:'v -> 'a -> ('a, 'r) Continue_or_stop.t)
-    -> finish:('a -> 'r)
-    -> 'r
+  val union : 'a t -> 'a t -> f:(key -> 'a -> 'a -> 'a option) -> 'a t
 
-  val choose_exn : 'a t -> key * 'a
-  (** Find an unspecified element. [O(1)]. *)
+  (** {1 Query} *)
+
+  val is_empty : 'a t -> bool
+  val is_singleton : 'a t -> bool
+  val length : 'a t -> int
+
+  val choose_key : 'a t -> key option
+  (** Find an unspecified key. Different keys may be chosen for equivalent
+      maps. [O(1)]. *)
 
   val choose : 'a t -> (key * 'a) option
-  (** Find an unspecified element. [O(1)]. *)
+  (** Find an unspecified binding. Different bindings may be chosen for
+      equivalent maps. [O(1)]. *)
 
-  val pop : 'a t -> (key * 'a * 'a t) option
-  (** Find and remove an unspecified element. [O(1)]. *)
+  val choose_exn : 'a t -> key * 'a
+  (** Find an unspecified binding. Different bindings may be chosen for
+      equivalent maps. [O(1)]. *)
 
-  val pop_min_elt : 'a t -> (key * 'a * 'a t) option
-  (** Find and remove minimum element. [O(log n)]. *)
+  val min_binding : 'a t -> (key * 'a) option
+  val mem : 'a t -> key -> bool
+  val find : 'a t -> key -> 'a option
+  val find_exn : 'a t -> key -> 'a
+  val find_multi : 'a list t -> key -> 'a list
 
   val find_and_remove : 'a t -> key -> ('a * 'a t) option
-  (** Find and remove an element. *)
+  (** Find and remove the binding for a key. *)
+
+  val pop : 'a t -> (key * 'a * 'a t) option
+  (** Find and remove an unspecified binding. Different bindings may be
+      chosen for equivalent maps. [O(1)]. *)
+
+  val pop_min_binding : 'a t -> (key * 'a * 'a t) option
+  (** Find and remove binding with minimum key. [O(log n)]. *)
+
+  (** {1 Transform} *)
+
+  val change : 'a t -> key -> f:('a option -> 'a option) -> 'a t
+  val update : 'a t -> key -> f:('a option -> 'a) -> 'a t
+  val map : 'a t -> f:('a -> 'b) -> 'b t
+  val mapi : 'a t -> f:(key:key -> data:'a -> 'b) -> 'b t
+
+  val map_endo : 'a t -> f:('a -> 'a) -> 'a t
+  (** Like map, but specialized to require [f] to be an endofunction, which
+      enables preserving [==] if [f] preserves [==] of every value. *)
+
+  val filter_mapi : 'a t -> f:(key:key -> data:'a -> 'b option) -> 'b t
+
+  (** {1 Traverse} *)
+
+  val iter : 'a t -> f:('a -> unit) -> unit
+  val iteri : 'a t -> f:(key:key -> data:'a -> unit) -> unit
+  val existsi : 'a t -> f:(key:key -> data:'a -> bool) -> bool
+  val for_alli : 'a t -> f:(key:key -> data:'a -> bool) -> bool
+  val fold : 'a t -> init:'b -> f:(key:key -> data:'a -> 'b -> 'b) -> 'b
+
+  (** {1 Convert} *)
+
+  val to_alist :
+    ?key_order:[`Increasing | `Decreasing] -> 'a t -> (key * 'a) list
+
+  val data : 'a t -> 'a list
+
+  val to_iter2 :
+       'a t
+    -> 'b t
+    -> (key * [`Left of 'a | `Both of 'a * 'b | `Right of 'b]) iter
+
+  val symmetric_diff :
+       data_equal:('a -> 'b -> bool)
+    -> 'a t
+    -> 'b t
+    -> (key * [> `Left of 'a | `Unequal of 'a * 'b | `Right of 'b]) iter
+
+  (** {1 Pretty-print} *)
 
   val pp : key pp -> 'a pp -> 'a t pp
 

sledge/nonstdlib/qset.ml

@@ -80,8 +80,8 @@ struct
   let choose = M.choose
   let choose_exn = M.choose_exn
   let pop = M.pop
-  let min_elt = M.min_elt
-  let pop_min_elt = M.pop_min_elt
+  let min_elt = M.min_binding
+  let pop_min_elt = M.pop_min_binding
 
   let classify s =
     match pop s with

sledge/src/test/equality_test.ml

@@ -62,17 +62,17 @@ let%test_module _ =
         = (%y_6 rem %t_1)
 
       {sat= true;
-       rep= [[%t_1 ↦ ];
-             [%u_2 ↦ %t_1];
-             [%v_3 ↦ %t_1];
-             [%w_4 ↦ %t_1];
-             [%x_5 ↦ %t_1];
-             [%y_6 ↦ ];
-             [%z_7 ↦ %t_1];
-             [(%y_6 rem %v_3) ↦ %t_1];
-             [(%y_6 rem %z_7) ↦ %t_1];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [(%y_6 rem %z_7) ↦ %t_1];
+             [(%y_6 rem %v_3) ↦ %t_1];
+             [%z_7 ↦ %t_1];
+             [%y_6 ↦ ];
+             [%x_5 ↦ %t_1];
+             [%w_4 ↦ %t_1];
+             [%v_3 ↦ %t_1];
+             [%u_2 ↦ %t_1];
+             [%t_1 ↦ ]]} |}]
 
     let%test _ = implies_eq r3 t z
 
@@ -83,7 +83,7 @@ let%test_module _ =
       pp r15 ;
       [%expect
         {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]; [-1 ↦ ]; [0 ↦ ]]} |}]
+          {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [(%x_5 ≠ 0) ↦ -1]; [%x_5 ↦ 1]]} |}]
 
     let%test _ = implies_eq r15 b (Term.signed 1 !1)
     let%test _ = implies_eq r15 (Term.unsigned 1 b) !1

sledge/src/test/fol_test.ml

@@ -66,7 +66,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw f1 ;
-      [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]]} |}]
 
     let%test _ = is_unsat (add_eq !1 !1 f1)
 
@@ -76,7 +76,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw f2 ;
-      [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ ]]} |}]
 
     let f3 = of_eqs [(x + !0, x + !1)]
 
@@ -84,7 +84,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw f3 ;
-      [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ ]]} |}]
 
     let f4 = of_eqs [(x, y); (x + !0, y + !1)]
 
@@ -93,7 +93,7 @@ let%test_module _ =
     let%expect_test _ =
       pp_raw f4 ;
       [%expect
-        {| {sat= false; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}]
+        {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]} |}]
 
     let t1 = of_eqs [(!1, !1)]
 
@@ -109,7 +109,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw r0 ;
-      [%expect {| {sat= true; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]]} |}]
 
     let%expect_test _ =
       pp r0 ;
@@ -128,7 +128,7 @@ let%test_module _ =
 
         %x_5 = %y_6
 
-      {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]} |}]
 
     let%test _ = implies_eq r1 x y
 
@@ -142,12 +142,12 @@ let%test_module _ =
         %x_5 = %y_6 = %z_7 = %x_5^
 
       {sat= true;
-       rep= [[%x_5 ↦ ];
-             [%y_6 ↦ %x_5];
-             [%z_7 ↦ %x_5];
-             [%x_5^ ↦ %x_5];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [%x_5^ ↦ %x_5];
+             [%z_7 ↦ %x_5];
+             [%y_6 ↦ %x_5];
+             [%x_5 ↦ ]]} |}]
 
     let%test _ = implies_eq r2 x z
     let%test _ = implies_eq (inter r1 r2) x y
@@ -169,12 +169,12 @@ let%test_module _ =
       [%expect
         {|
         {sat= true;
-         rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]; [-1 ↦ ]; [0 ↦ ]]}
+         rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %w_4]; [%y_6 ↦ %w_4]; [%w_4 ↦ ]]}
 
         {sat= true;
-         rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]}
+         rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %x_5]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]}
 
-        {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]; [-1 ↦ ]; [0 ↦ ]]} |}]
+        {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %y_6]; [%y_6 ↦ ]]} |}]
 
     let%test _ =
       let r = of_eqs [(w, y); (y, z)] in
@@ -189,21 +189,21 @@ let%test_module _ =
       pp_raw r3 ;
       [%expect
         {|
-        %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (%z_7 × %y_6)
-      ∧ (%z_7 × (%y_6 × %y_6)) = %t_1
+        (%z_7 × (%y_6 × %y_6)) = %t_1
+      ∧ %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (%z_7 × %y_6)
 
       {sat= true;
-       rep= [[%t_1 ↦ (%y_6^2 × %z_7)];
-             [%u_2 ↦ %z_7];
-             [%v_3 ↦ %z_7];
-             [%w_4 ↦ %z_7];
-             [%x_5 ↦ %z_7];
-             [%y_6 ↦ ];
-             [%z_7 ↦ ];
-             [(%y_6 × %z_7) ↦ %z_7];
-             [(%y_6^2 × %z_7) ↦ ];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [(%z_7 × %y_6^2) ↦ ];
+             [(%z_7 × %y_6) ↦ %z_7];
+             [%z_7 ↦ ];
+             [%y_6 ↦ ];
+             [%x_5 ↦ %z_7];
+             [%w_4 ↦ %z_7];
+             [%v_3 ↦ %z_7];
+             [%u_2 ↦ %z_7];
+             [%t_1 ↦ (%z_7 × %y_6^2)]]} |}]
 
     let%test _ = not (implies_eq r3 t z) (* incomplete *)
     let%test _ = implies_eq r3 x z
@@ -216,15 +216,15 @@ let%test_module _ =
       pp_raw r4 ;
       [%expect
         {|
-        (-4 + %z_7) = %y_6 ∧ (3 + %z_7) = %w_4 ∧ (8 + %z_7) = %x_5
+        (8 + %z_7) = %x_5 ∧ (3 + %z_7) = %w_4 ∧ (-4 + %z_7) = %y_6
 
       {sat= true;
-       rep= [[%w_4 ↦ (%z_7 + 3)];
-             [%x_5 ↦ (%z_7 + 8)];
-             [%y_6 ↦ (%z_7 + -4)];
-             [%z_7 ↦ ];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [%z_7 ↦ ];
+             [%y_6 ↦ (-4 + %z_7)];
+             [%x_5 ↦ (8 + %z_7)];
+             [%w_4 ↦ (3 + %z_7)]]} |}]
 
     let%test _ = implies_eq r4 x (w + !5)
     let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5))
@@ -242,7 +242,7 @@ let%test_module _ =
         {|
         1 = %x_5 = %y_6
 
-      {sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ 1]; [%x_5 ↦ 1]]} |}]
 
     let%test _ = implies_eq r6 x y
 
@@ -255,25 +255,25 @@ let%test_module _ =
       pp (add_eq x z r7) ;
       [%expect
         {|
-          %v_3 = %x_5 ∧ %w_4 = %y_6 = %z_7
+          %w_4 = %y_6 = %z_7 ∧ %v_3 = %x_5
     
         {sat= true;
-         rep= [[%v_3 ↦ ];
-               [%w_4 ↦ ];
-               [%x_5 ↦ %v_3];
-               [%y_6 ↦ %w_4];
-               [%z_7 ↦ %w_4];
+         rep= [[0 ↦ ];
                [-1 ↦ ];
-               [0 ↦ ]]}
+               [%z_7 ↦ %w_4];
+               [%y_6 ↦ %w_4];
+               [%x_5 ↦ %v_3];
+               [%w_4 ↦ ];
+               [%v_3 ↦ ]]}
 
         {sat= true;
-         rep= [[%v_3 ↦ ];
-               [%w_4 ↦ %v_3];
-               [%x_5 ↦ %v_3];
-               [%y_6 ↦ %v_3];
-               [%z_7 ↦ %v_3];
+         rep= [[0 ↦ ];
                [-1 ↦ ];
-               [0 ↦ ]]}
+               [%z_7 ↦ %v_3];
+               [%y_6 ↦ %v_3];
+               [%x_5 ↦ %v_3];
+               [%w_4 ↦ %v_3];
+               [%v_3 ↦ ]]}
 
           %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}]
 
@@ -299,13 +299,13 @@ let%test_module _ =
         %v_3 = %w_4 = %x_5 = %y_6 = %z_7
 
       {sat= true;
-       rep= [[%v_3 ↦ ];
-             [%w_4 ↦ %v_3];
-             [%x_5 ↦ %v_3];
-             [%y_6 ↦ %v_3];
-             [%z_7 ↦ %v_3];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [%z_7 ↦ %v_3];
+             [%y_6 ↦ %v_3];
+             [%x_5 ↦ %v_3];
+             [%w_4 ↦ %v_3];
+             [%v_3 ↦ ]]} |}]
 
     let%test _ = normalize r7' w |> Term.equal v
 
@@ -322,10 +322,10 @@ let%test_module _ =
       pp_raw r8 ;
       [%expect
         {|
-        14 = %y_6 ∧ (13 × %z_7) = %x_5
+        (13 × %z_7) = %x_5 ∧ 14 = %y_6
     
       {sat= true;
-       rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+       rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%y_6 ↦ 14]; [%x_5 ↦ (13 × %z_7)]]} |}]
 
     let%test _ = implies_eq r8 y !14
 
@@ -337,10 +337,10 @@ let%test_module _ =
       [%expect
         {|
       {sat= true;
-       rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
+       rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
 
       {sat= true;
-       rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+       rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]} |}]
 
     let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
 
@@ -356,10 +356,10 @@ let%test_module _ =
       [%expect
         {|
         {sat= true;
-         rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
+         rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
 
         {sat= true;
-         rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
+         rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
 
         (%z_7 - (%x_5 + 8))
 
@@ -395,7 +395,7 @@ let%test_module _ =
     let%expect_test _ =
       pp_raw r13 ;
       [%expect
-        {| {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]; [-1 ↦ ]; [0 ↦ ]]} |}]
+        {| {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %y_6]; [%y_6 ↦ ]]} |}]
 
     let%test _ = not (is_unsat r13) (* incomplete *)
 
@@ -406,7 +406,7 @@ let%test_module _ =
       pp_raw r14 ;
       [%expect
         {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
+          {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ 1]]} |}]
 
     let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
 
@@ -418,12 +418,12 @@ let%test_module _ =
       [%expect
         {|
           {sat= true;
-           rep= [[%x_5 ↦ 1];
-                 [%y_6 ↦ ];
-                 [(%x_5 ≠ 0) ↦ -1];
-                 [(%y_6 ≠ 0) ↦ -1];
+           rep= [[0 ↦ ];
                  [-1 ↦ ];
-                 [0 ↦ ]]} |}]
+                 [(%y_6 ≠ 0) ↦ -1];
+                 [(%x_5 ≠ 0) ↦ -1];
+                 [%y_6 ↦ ];
+                 [%x_5 ↦ 1]]} |}]
 
     let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
     let%test _ = implies_eq r14 b (Formula.inject Formula.tt)
@@ -435,7 +435,7 @@ let%test_module _ =
       pp_raw r15 ;
       [%expect
         {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}]
+          {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ 1]]} |}]
 
     (* f(x−1)−1=x+1, f(y)+1=y−1, y+1=x ⊢ false *)
     let r16 =
@@ -446,12 +446,12 @@ let%test_module _ =
       [%expect
         {|
       {sat= false;
-       rep= [[%x_5 ↦ (%y_6 + 1)];
-             [%y_6 ↦ ];
-             [%y_6^ ↦ (%y_6 + -2)];
-             [(%x_5 + -1)^ ↦ (%y_6 + 3)];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [(-1 + %x_5)^ ↦ (3 + %y_6)];
+             [%y_6^ ↦ (-2 + %y_6)];
+             [%y_6 ↦ ];
+             [%x_5 ↦ (1 + %y_6)]]} |}]
 
     let%test _ = is_unsat r16
 
@@ -463,12 +463,12 @@ let%test_module _ =
       [%expect
         {|
       {sat= false;
-       rep= [[%x_5 ↦ ];
-             [%y_6 ↦ %x_5];
-             [%x_5^ ↦ %x_5];
-             [%y_6^ ↦ (%x_5 + -1)];
+       rep= [[0 ↦ ];
              [-1 ↦ ];
-             [0 ↦ ]]} |}]
+             [%y_6^ ↦ (-1 + %x_5)];
+             [%x_5^ ↦ %x_5];
+             [%y_6 ↦ %x_5];
+             [%x_5 ↦ ]]} |}]
 
     let%test _ = is_unsat r17
 
@@ -479,14 +479,14 @@ let%test_module _ =
       [%expect
         {|
         {sat= true;
-         rep= [[%x_5 ↦ ];
-               [%y_6 ↦ ];
-               [%x_5^ ↦ %x_5];
-               [%y_6^ ↦ (%y_6 + -1)];
+         rep= [[0 ↦ ];
                [-1 ↦ ];
-               [0 ↦ ]]}
+               [%y_6^ ↦ (-1 + %y_6)];
+               [%x_5^ ↦ %x_5];
+               [%y_6 ↦ ];
+               [%x_5 ↦ ]]}
 
-          %x_5 = %x_5^ ∧ (-1 + %y_6) = %y_6^ |}]
+          (-1 + %y_6) = %y_6^ ∧ %x_5 = %x_5^ |}]
 
     let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)]
 
@@ -495,7 +495,7 @@ let%test_module _ =
       [%expect
         {|
           {sat= true;
-           rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]; [-1 ↦ ]; [0 ↦ ]]} |}]
+           rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ 0]; [%y_6 ↦ 0]; [%x_5 ↦ 0]]} |}]
 
     let%test _ = implies_eq r19 z !0
 

sledge/src/test/sh_test.ml

@@ -145,7 +145,7 @@ let%test_module _ =
       pp q' ;
       [%expect
         {|
-        ∃ %x_6 .   %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp
+        ∃ %x_6 .   (-1 + %y_7) = %y_7^ ∧ %x_6 = %x_6^ ∧ emp
     
           ((-1 + %y_7) = %y_7^) ∧ emp
 

sledge/src/test/solver_test.ml

@@ -143,7 +143,7 @@ let%test_module _ =
         {|
         ( infer_frame:
             %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3 .   %l_6 -[)-> ⟨16,%a_3⟩
-        ) infer_frame:   %a_2 = _ ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
+        ) infer_frame:   (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ %a_2 = _ ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -159,7 +159,7 @@ let%test_module _ =
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩
         ) infer_frame:
-            %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
+            (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 16 = %m_8 ∧ %a_2 = _ ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -175,7 +175,7 @@ let%test_module _ =
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩
         ) infer_frame:
-            %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
+            (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 16 = %m_8 ∧ %a_2 = _ ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -194,9 +194,9 @@ let%test_module _ =
               %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩
         ) infer_frame:
           ∃ %a0_10, %a1_11 .
-            %a_2 = %a0_10
+            (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
-          ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
+          ∧ %a_2 = %a0_10
           ∧ (16 + %k_5) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let%expect_test _ =
@@ -216,9 +216,9 @@ let%test_module _ =
               %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩
         ) infer_frame:
           ∃ %a0_10, %a1_11 .
-            %a_2 = %a0_10
+            (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
-          ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
+          ∧ %a_2 = %a0_10
           ∧ (16 + %k_5) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let seg_split_symbolically =
@@ -246,19 +246,19 @@ let%test_module _ =
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame:
-            ( (  %a_1 = %a_2
+            ( (  16 = %m_8
                ∧ 2 = %n_9
-               ∧ 16 = %m_8
+               ∧ %a_1 = %a_2
                ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
-            ∨ (  %a_3 = _
-               ∧ 1 = %n_9
+            ∨ (  (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
                ∧ 16 = %m_8
-               ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
+               ∧ 1 = %n_9
+               ∧ %a_3 = _
                ∧ emp)
-            ∨ (  %a_3 = _
-               ∧ 0 = %n_9
+            ∨ (  (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
                ∧ 16 = %m_8
-               ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
+               ∧ 0 = %n_9
+               ∧ %a_3 = _
                ∧ emp)
             ) |}]
 

sledge/src/test/term_test.ml

@@ -54,7 +54,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (z + !42 + !13) ;
-      [%expect {| (%z_2 + 55) |}]
+      [%expect {| (55 + %z_2) |}]
 
     let%expect_test _ =
       pp (z + !42 + !(-42)) ;
@@ -62,15 +62,15 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (z * y) ;
-      [%expect {| (%y_1 × %z_2) |}]
+      [%expect {| (%z_2 × %y_1) |}]
 
     let%expect_test _ =
       pp (y * z * y) ;
-      [%expect {| (%y_1^2 × %z_2) |}]
+      [%expect {| (%z_2 × %y_1^2) |}]
 
     let%expect_test _ =
       pp ((!2 * z * z) + (!3 * z) + !4) ;
-      [%expect {| (3 × %z_2 + 2 × (%z_2^2) + 4) |}]
+      [%expect {| (4 + 2 × (%z_2^2) + 3 × %z_2) |}]
 
     let%expect_test _ =
       pp
@@ -85,9 +85,8 @@ let%test_module _ =
         + (!9 * z * z * z) ) ;
       [%expect
         {|
-         (3 × %y_1 + 2 × %z_2 + 6 × (%y_1 × %z_2) + 8 × (%y_1 × %z_2^2)
-           + 5 × (%y_1^2) + 7 × (%y_1^2 × %z_2) + 4 × (%z_2^2) + 9 × (%z_2^3)
-           + 1) |}]
+         (1 + 9 × (%z_2^3) + 4 × (%z_2^2) + 7 × (%z_2 × %y_1^2) + 5 × (%y_1^2)
+           + 8 × (%z_2^2 × %y_1) + 6 × (%z_2 × %y_1) + 2 × %z_2 + 3 × %y_1) |}]
 
     let%expect_test _ =
       pp (!0 * z * y) ;
@@ -95,19 +94,19 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (!1 * z * y) ;
-      [%expect {| (%y_1 × %z_2) |}]
+      [%expect {| (%z_2 × %y_1) |}]
 
     let%expect_test _ =
       pp (!7 * z * (!2 * y)) ;
-      [%expect {| (14 × (%y_1 × %z_2)) |}]
+      [%expect {| (14 × (%z_2 × %y_1)) |}]
 
     let%expect_test _ =
       pp (!13 + (!42 * z)) ;
-      [%expect {| (42 × %z_2 + 13) |}]
+      [%expect {| (13 + 42 × %z_2) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42) ;
-      [%expect {| (13 × %z_2 + 42) |}]
+      [%expect {| (42 + 13 × %z_2) |}]
 
     let%expect_test _ =
       pp ((!2 * z) - !3 + ((!(-2) * z) + !3)) ;
@@ -115,31 +114,31 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!3 * y) + (!13 * z) + !42) ;
-      [%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}]
+      [%expect {| (42 + 13 × %z_2 + 3 × %y_1) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y)) ;
-      [%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}]
+      [%expect {| (42 + 13 × %z_2 + 3 × %y_1) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y) + (!2 * z)) ;
-      [%expect {| (3 × %y_1 + 15 × %z_2 + 42) |}]
+      [%expect {| (42 + 15 × %z_2 + 3 × %y_1) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y) + (!(-13) * z)) ;
-      [%expect {| (3 × %y_1 + 42) |}]
+      [%expect {| (42 + 3 × %y_1) |}]
 
     let%expect_test _ =
       pp (z + !42 + ((!3 * y) + (!(-1) * z))) ;
-      [%expect {| (3 × %y_1 + 42) |}]
+      [%expect {| (42 + 3 × %y_1) |}]
 
     let%expect_test _ =
       pp (!(-1) * (z + (!(-1) * y))) ;
-      [%expect {| (%y_1 + -1 × %z_2) |}]
+      [%expect {| (-1 × %z_2 + %y_1) |}]
 
     let%expect_test _ =
       pp (((!3 * y) + !2) * (!4 + (!5 * z))) ;
-      [%expect {| (12 × %y_1 + 10 × %z_2 + 15 × (%y_1 × %z_2) + 8) |}]
+      [%expect {| (8 + 15 × (%z_2 × %y_1) + 10 × %z_2 + 12 × %y_1) |}]
 
     let%expect_test _ =
       pp (((!2 * z) - !3 + ((!(-2) * z) + !3)) * (!4 + (!5 * z))) ;
@@ -147,7 +146,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!13 * z) + !42 - ((!3 * y) + (!13 * z))) ;
-      [%expect {| (-3 × %y_1 + 42) |}]
+      [%expect {| (42 + -3 × %y_1) |}]
 
     let%expect_test _ =
       pp (z = y) ;
@@ -183,47 +182,47 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (y - (!(-3) * y) + !4) ;
-      [%expect {| (4 × %y_1 + 4) |}]
+      [%expect {| (4 + 4 × %y_1) |}]
 
     let%expect_test _ =
       pp ((!(-3) * y) + !4 - y) ;
-      [%expect {| (-4 × %y_1 + 4) |}]
+      [%expect {| (4 + -4 × %y_1) |}]
 
     let%expect_test _ =
       pp (y = (!(-3) * y) + !4) ;
-      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
+      [%expect {| (%y_1 = (4 + -3 × %y_1)) |}]
 
     let%expect_test _ =
       pp ((!(-3) * y) + !4 = y) ;
-      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
+      [%expect {| (%y_1 = (4 + -3 × %y_1)) |}]
 
     let%expect_test _ =
       pp (sub true_ (z = !4)) ;
-      [%expect {| (-1 × (%z_2 = 4) + -1) |}]
+      [%expect {| (-1 + -1 × (%z_2 = 4)) |}]
 
     let%expect_test _ =
       pp (add true_ (z = !4) = (z = !4)) ;
-      [%expect {| ((%z_2 = 4) = ((%z_2 = 4) + -1)) |}]
+      [%expect {| ((%z_2 = 4) = (-1 + (%z_2 = 4))) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
+      [%expect {| ((13 × %z_2 + 3 × %y_1) = (42 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !(-42) = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
+      [%expect {| ((13 × %z_2 + 3 × %y_1) = (-42 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((-3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}]
+      [%expect {| ((13 × %z_2 + -3 × %y_1) = (42 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ((!10 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((-3 × %y_1 + 13 × %z_2) = (10 × %z_2 + 42)) |}]
+      [%expect {| ((13 × %z_2 + -3 × %y_1) = (42 + 10 × %z_2)) |}]
 
     let%expect_test _ =
       pp ~~((!13 * z) + !(-42) != (!3 * y) + (!13 * z)) ;
-      [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}]
+      [%expect {| ((13 × %z_2 + 3 × %y_1) = (-42 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ~~(!2 < y && z <= !3) ;
@@ -252,7 +251,7 @@ let%test_module _ =
       pp (z1_2 * z1_2) ;
       [%expect
         {|
-        (2 × %z_2 + (%z_2^2) + 1)
+        (1 + (%z_2^2) + 2 × %z_2)
 
-        (4 × %z_2 + 6 × (%z_2^2) + 4 × (%z_2^3) + (%z_2^4) + 1) |}]
+        (1 + (%z_2^4) + 4 × (%z_2^3) + 6 × (%z_2^2) + 4 × %z_2) |}]
   end )