[sledge] Reimplement arithmetic and congruence closure

Summary:
- Add nary expressions implemented using a form of multisets which
  support any integer multiplicity

- Reimplement polynomials using new nary expressions

- Move the decomposition of exps into "base plus offset" form into
  Exp, to enforce simplification invariants

- Revise expression simplification to cooperate with congruence
  closure (mainly: simplification should not invent new
  subexpressions)

- Reimplement congruence closure plus integer offsets to

  + cope with new representation of polynomials using nary expression forms

  + be diligent about maintaining which expressions are in the relation

  + add lots of invariant checking for the correlations between the
    componnents of the congruence closure data structures

Reviewed By: jvillard

Differential Revision: D14075512

fbshipit-source-id: 2dbaf3d11

sledge/TODO.org

@@ -1,3 +1,5 @@
+* overall
+** rename accumulators from [z] to [s] for "state"
 * llvm
 * import
 ** consider adding set ops that operate on a set and the domain of a map
@@ -16,7 +18,16 @@ rather than nearest enclosing
 ** revise spec of strlen to account for non-max length strings
 ** convert strlen inst into a primitive to return the end of the block containing a pointer, and model strlen in code
 * llair
-** simplify "greater-than" exps to "less-than" in reverse order
+** divide Exp into two: one for code and one for formulas
+- Exp simplification does not preserve order of operations, which is wrong wrt overflow
+- code Exps don't need polynomial simplification
+- code Exps could be given strong types in order to check the frontend, while letting formula Exps have weaker types as dictated by the logic
+- treat formula exps as unbounded, clamp to bounded range when conferting to a code exp
+** check if simplification via simp_sub in simp_eq is still needed
+- it leads to violations of the subexp assertion on app1
+** replace Option.value_exn (Typ.prim_bit_size_of typ) with bits_of_int
+** simplify combinations of mul and div, e.g. x * (y / z) ==> (x * y) / z
+** ? simplify "greater-than" exps to "less-than" in reverse order
 ** when Xor exps have types, simplify e xor e to 0
 ** normalize polynomial equations by dividing coefficients by their gcd
 ** treat Typ.ptr as an integer of some particular size (i.e. ptr = intptr)
@@ -215,6 +226,14 @@ it is not obvious whether it will be simpler to use free variables instead of No
 ** llvm bugs?
 - Why aren't shufflevector instructions with zeroinitializer masks eliminated by the scalarizer pass?
 * congruence
+** should handle equality and disequality simplification
+- equalities of equalities to integers currently handled by Sh.pure
+- doing it in Exp leads to violations of the subexp assertion on app1
+** optimize: change Cls.t and Use.t from a list to an unbalanced tree data structure
+- only need empty, add, union, map, fold, fold_map to be fast, so no need for balancing
+- detecting duplicates probably not worth the time since if any occur, the only cost is adding a redundant equation to pnd which will be quickly processed
+** optimize: when called from extend, norm_extend calls norm unnecessarily
+** revise mli to two sections, one for a "relation" api (with merge, mem/check, etc) and one for a "formula" api (with and_, or_, etc.)
 ** ? assert exps in formulas are in the carrier
 us and xs, or just fv?
 ** strengthen invariant
@@ -222,8 +241,6 @@ us and xs, or just fv?
 since they (could) have the same domain
 ** optimize: can identity mappings in lkp be removed?
 * symbolic heap
-** Congruence should handle equalities of equalities to integers
-currently handled by Sh.pure
 ** normalize exps in terms of reps
 - add operation to normalize by rewriting in terms of reps
 - check for unsat

sledge/src/import/import.ml

@@ -265,6 +265,12 @@ module Set = struct
   let to_tree = Using_comparator.to_tree
 end
 
+module Mset = struct
+  include Mset
+
+  let pp sep pp_elt fs s = List.pp sep pp_elt fs (to_list s)
+end
+
 module Z = struct
   include Z
 

sledge/src/import/import.mli

@@ -212,8 +212,15 @@ module Set : sig
   val to_tree : ('e, 'c) t -> ('e, 'c) tree
 end
 
+module Mset : sig
+  include module type of Mset
+
+  val pp : (unit, unit) fmt -> ('a * Z.t) pp -> ('a, _) t pp
+  (** Pretty-print a multiset. *)
+end
+
 module Z : sig
-  include module type of Z
+  include module type of struct include Z end
 
   val hash_fold_t : t Hash.folder
   val t_of_sexp : Sexp.t -> t

sledge/src/import/mset.ml

@@ -0,0 +1,106 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Mset - Set with integer (positive, negative, or zero) multiplicity for
+    each element *)
+
+open Base
+
+type ('elt, 'cmp) t = ('elt, Z.t, 'cmp) Map.t
+
+module M (Elt : sig
+  type t
+  type comparator_witness
+end) =
+struct
+  type nonrec t = (Elt.t, Elt.comparator_witness) t
+end
+
+module type Sexp_of_m = sig
+  type t [@@deriving sexp_of]
+end
+
+module type M_of_sexp = sig
+  type t [@@deriving of_sexp]
+
+  include Comparator.S with type t := t
+end
+
+module type Compare_m = sig end
+module type Hash_fold_m = Hasher.S
+
+let sexp_of_z z = Sexp.Atom (Z.to_string z)
+let z_of_sexp = function Sexp.Atom s -> Z.of_string s | _ -> assert false
+let hash_fold_z state z = Hash.fold_int state (Z.hash z)
+
+let sexp_of_m__t (type elt) (module Elt : Sexp_of_m with type t = elt) t =
+  Map.sexp_of_m__t (module Elt) sexp_of_z t
+
+let m__t_of_sexp (type elt cmp)
+    (module Elt : M_of_sexp
+      with type t = elt and type comparator_witness = cmp) sexp =
+  Map.m__t_of_sexp (module Elt) z_of_sexp sexp
+
+let compare_m__t (module Elt : Compare_m) = Map.compare_direct Z.compare
+
+let hash_fold_m__t (type elt) (module Elt : Hash_fold_m with type t = elt)
+    state =
+  Map.hash_fold_m__t (module Elt) hash_fold_z state
+
+let hash_m__t (type elt) (module Elt : Hash_fold_m with type t = elt) =
+  Hash.of_fold (hash_fold_m__t (module Elt))
+
+type ('elt, 'cmp) comparator =
+  (module Comparator.S with type t = 'elt and type comparator_witness = 'cmp)
+
+let empty cmp = Map.empty cmp
+let if_nz z = if Z.equal Z.zero z then None else Some z
+
+let add m x i =
+  Map.change m x ~f:(function Some j -> if_nz Z.(i + j) | None -> if_nz i)
+
+let remove m x = Map.remove m x
+
+let union m n =
+  Map.merge m n ~f:(fun ~key:_ -> function
+    | `Both (i, j) -> if_nz Z.(i + j) | `Left i | `Right i -> Some i )
+
+let length m = Map.length m
+let count m x = match Map.find m x with Some z -> z | None -> Z.zero
+
+let count_and_remove m x =
+  let found = ref Z.zero in
+  let m =
+    Map.change m x ~f:(function
+      | None -> None
+      | Some i ->
+          found := i ;
+          None )
+  in
+  if Z.equal !found Z.zero then None else Some (!found, m)
+
+let min_elt = Map.min_elt
+let fold m ~f ~init = Map.fold m ~f:(fun ~key ~data s -> f key data s) ~init
+
+let map m ~f =
+  fold m ~init:m ~f:(fun x i m ->
+      let x', i' = f x i in
+      if phys_equal x' x then
+        if Z.equal i' i then m else Map.set m ~key:x ~data:i'
+      else add (Map.remove m x) x' i' )
+
+let fold_map m ~f ~init:s =
+  fold m ~init:(m, s) ~f:(fun x i (m, s) ->
+      let x', i', s = f x i s in
+      if phys_equal x' x then
+        if Z.equal i' i then (m, s) else (Map.set m ~key:x ~data:i', s)
+      else (add (Map.remove m x) x' i', s) )
+
+let for_all m ~f = Map.for_alli m ~f:(fun ~key ~data -> f key data)
+let map_counts m ~f = Map.mapi m ~f:(fun ~key ~data -> f key data)
+let iter m ~f = Map.iteri m ~f:(fun ~key ~data -> f key data)
+let to_list m = Map.to_alist m

sledge/src/import/mset.mli

@@ -0,0 +1,108 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Mset - Set with integer (positive, negative, or zero) multiplicity for
+    each element *)
+
+open Base
+
+type ('elt, 'cmp) t
+
+type ('elt, 'cmp) comparator =
+  (module Comparator.S with type t = 'elt and type comparator_witness = 'cmp)
+
+module M (Elt : sig
+  type t
+  type comparator_witness
+end) : sig
+  type nonrec t = (Elt.t, Elt.comparator_witness) t
+end
+
+module type Sexp_of_m = sig
+  type t [@@deriving sexp_of]
+end
+
+module type M_of_sexp = sig
+  type t [@@deriving of_sexp]
+
+  include Comparator.S with type t := t
+end
+
+module type Compare_m = sig end
+module type Hash_fold_m = Hasher.S
+
+val sexp_of_m__t :
+  (module Sexp_of_m with type t = 'elt) -> ('elt, 'cmp) t -> Sexp.t
+
+val m__t_of_sexp :
+     (module M_of_sexp with type t = 'elt and type comparator_witness = 'cmp)
+  -> Sexp.t
+  -> ('elt, 'cmp) t
+
+val compare_m__t :
+  (module Compare_m) -> ('elt, 'cmp) t -> ('elt, 'cmp) t -> int
+
+val hash_fold_m__t :
+     (module Hash_fold_m with type t = 'elt)
+  -> Hash.state
+  -> ('elt, _) t
+  -> Hash.state
+
+val hash_m__t :
+  (module Hash_fold_m with type t = 'elt) -> ('elt, _) t -> Hash.hash_value
+
+val empty : ('elt, 'cmp) comparator -> ('elt, 'cmp) t
+(** The empty multiset over the provided order. *)
+
+val add : ('a, 'c) t -> 'a -> Z.t -> ('a, 'c) t
+(** Add to multiplicity of single element. [O(log n)] *)
+
+val remove : ('a, 'c) t -> 'a -> ('a, 'c) t
+(** Set the multiplicity of an element to zero. [O(log n)] *)
+
+val union : ('a, 'c) t -> ('a, 'c) t -> ('a, 'c) t
+(** Sum multiplicities pointwise. [O(n + m)] *)
+
+val length : _ t -> int
+(** Number of elements with non-zero multiplicity. [O(1)]. *)
+
+val count : ('a, _) t -> 'a -> Z.t
+(** Multiplicity of an element. [O(log n)]. *)
+
+val count_and_remove : ('a, 'c) t -> 'a -> (Z.t * ('a, 'c) t) option
+(** Multiplicity of an element, and remove it. [O(log n)]. *)
+
+val map : ('a, 'c) t -> f:('a -> Z.t -> 'a * Z.t) -> ('a, 'c) t
+(** Map over the elements in ascending order. Preserves physical equality if
+    [f] does. *)
+
+val map_counts : ('a, 'c) t -> f:('a -> Z.t -> Z.t) -> ('a, 'c) t
+(** Map over the multiplicities of the elements in ascending order. *)
+
+val fold : ('a, _) t -> f:('a -> Z.t -> 's -> 's) -> init:'s -> 's
+(** Fold over the elements in ascending order. *)
+
+val fold_map :
+     ('a, 'c) t
+  -> f:('a -> Z.t -> 's -> 'a * Z.t * 's)
+  -> init:'s
+  -> ('a, 'c) t * 's
+(** Folding map over the elements in ascending order. Preserves physical
+    equality if [f] does. *)
+
+val for_all : ('a, _) t -> f:('a -> Z.t -> bool) -> bool
+(** Universal property test. [O(n)] but returns as soon as a violation is
+    found, in ascending order. *)
+
+val iter : ('a, _) t -> f:('a -> Z.t -> unit) -> unit
+(** Iterate over the elements in ascending order. *)
+
+val min_elt : ('a, _) t -> ('a * Z.t) option
+(** Minimum element. *)
+
+val to_list : ('a, _) t -> ('a * Z.t) list
+(** Convert to a list of elements in ascending order. *)

sledge/src/import/vector.ml

@@ -74,5 +74,6 @@ let of_array = v
 let of_list x = v (Array.of_list x)
 let of_list_rev x = v (Array.of_list_rev x)
 let of_option x = v (Option.to_array x)
+let reduce_exn x ~f = Array.reduce_exn (a x) ~f
 let to_list x = Array.to_list (a x)
 let to_array = a

sledge/src/import/vector.mli

@@ -167,7 +167,7 @@ val find_exn : 'a t -> f:('a -> bool) -> 'a
 val contains_dup : compare:('a -> 'a -> int) -> 'a t -> bool
 
 (* val reduce : 'a t -> f:('a -> 'a -> 'a) -> 'a option *)
-(* val reduce_exn : 'a t -> f:('a -> 'a -> 'a) -> 'a *)
+val reduce_exn : 'a t -> f:('a -> 'a -> 'a) -> 'a
 
 (* val random_element :
  *   ?random_state:Base.Random.State.t -> 'a t -> 'a option *)

sledge/src/llair/exp.mli

@@ -21,9 +21,14 @@
     treated as atomic since, as they are recursive, doing otherwise would
     require inductive reasoning. *)
 
-type t = private
+type comparator_witness
+
+type mset = (t, comparator_witness) Mset.t
+
+and t = private
   | App of {op: t; arg: t}
       (** Application of function symbol to argument, curried *)
+  | AppN of {op: t; args: mset}
   | Var of {id: int; name: string}  (** Local variable / virtual register *)
   | Nondet of {msg: string}
       (** Anonymous local variable with arbitrary value, representing
@@ -72,9 +77,9 @@ type t = private
       (** Convert between specified types, possibly with loss of information *)
 [@@deriving compare, hash, sexp]
 
-type exp = t
+val comparator : (t, comparator_witness) Comparator.t
 
-include Comparator.S with type t := t
+type exp = t
 
 val equal : t -> t -> bool
 val sort : t -> t -> t * t
@@ -150,6 +155,7 @@ val ult : t -> t -> t
 val ule : t -> t -> t
 val ord : t -> t -> t
 val uno : t -> t -> t
+val neg : Typ.t -> t -> t
 val add : Typ.t -> t -> t -> t
 val sub : Typ.t -> t -> t -> t
 val mul : Typ.t -> t -> t -> t
@@ -182,16 +188,30 @@ val struct_rec :
 
 val convert : ?signed:bool -> dst:Typ.t -> src:Typ.t -> t -> t
 
+(** Destruct *)
+
+val base_offset : t -> (t * Z.t * Typ.t) option
+(** Decompose an addition of a constant "offset" to a "base" exp. *)
+
+val base : t -> t
+(** Like [base_offset] but does not construct the "offset" exp. *)
+
+val offset : t -> (Z.t * Typ.t) option
+(** Like [base_offset] but does not construct the "base" exp. *)
+
 (** Access *)
 
+val iter : t -> f:(t -> unit) -> unit
 val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a
 val fold_exps : t -> init:'a -> f:('a -> t -> 'a) -> 'a
 val fold : t -> init:'a -> f:('a -> t -> 'a) -> 'a
-val fold_map : t -> init:'a -> f:('a -> t -> 'a * t) -> 'a * t
+val for_all : t -> f:(t -> bool) -> bool
-val map : t -> f:(t -> t) -> t
+val exists : t -> f:(t -> bool) -> bool
 
-(** Update *)
+(** Transform *)
 
+val map : t -> f:(t -> t) -> t
+val fold_map : t -> init:'a -> f:('a -> t -> 'a * t) -> 'a * t
 val rename : t -> Var.Subst.t -> t
 
 (** Query *)
@@ -199,4 +219,5 @@ val rename : t -> Var.Subst.t -> t
 val fv : t -> Var.Set.t
 val is_true : t -> bool
 val is_false : t -> bool
+val is_simple : t -> bool
 val is_constant : t -> bool

sledge/src/llair/exp_test.ml

@@ -7,8 +7,9 @@
 
 let%test_module _ =
   ( module struct
+    (* let () = Trace.init ~margin:68 ~config:all () *)
     let () = Trace.init ~margin:68 ~config:none ()
-    let pp = Format.printf "%t%a@." (fun _ -> Trace.flush ()) Exp.pp
+    let pp = Format.printf "@\n%a@." Exp.pp
     let char = Typ.integer ~bits:8
     let ( ! ) i = Exp.integer (Z.of_int i) char
     let ( + ) = Exp.add char
@@ -63,16 +64,6 @@ let%test_module _ =
       pp (!(-128) || !127) ;
       [%expect {| -1 |}]
 
-    let%test "monomial coefficient must be toplevel" =
-      match !7 * z * (!2 * y) with
-      | App {op= App {op= Mul _}; arg= Integer _} -> true
-      | _ -> false
-
-    let%test "polynomial constant must be toplevel" =
-      match (!13 * z) + !42 + (!3 * y) with
-      | App {op= App {op= Add _}; arg= Integer _} -> true
-      | _ -> false
-
     let%expect_test _ =
       pp (z + !42 + !13) ;
       [%expect {| (%z_2 + 55) |}]
@@ -87,11 +78,11 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (y * z * y) ;
-      [%expect {| (%y_1 × %y_1 × %z_2) |}]
+      [%expect {| (%y_1^2 × %z_2) |}]
 
     let%expect_test _ =
       pp ((!2 * z * z) + (!3 * z) + !4) ;
-      [%expect {| ((2 × %z_2 × %z_2) + (3 × %z_2) + 4) |}]
+      [%expect {| (2 × (%z_2^2) + 3 × %z_2 + 4) |}]
 
     let%expect_test _ =
       pp
@@ -104,9 +95,9 @@ let%test_module _ =
         + (!9 * z * z * z) ) ;
       [%expect
         {|
-         ((7 × %y_1 × %y_1 × %z_2) + (8 × %y_1 × %z_2 × %z_2)
+         (6 × (%y_1 × %z_2) + 8 × (%y_1 × %z_2^2) + 5 × (%y_1^2)
-          + (9 × %z_2 × %z_2 × %z_2) + (5 × %y_1 × %y_1) + (6 × %y_1 × %z_2)
+           + 7 × (%y_1^2 × %z_2) + 4 × (%z_2^2) + 9 × (%z_2^3) + 3 × %y_1
-          + (4 × %z_2 × %z_2) + (3 × %y_1) + (2 × %z_2) + 1) |}]
+           + 2 × %z_2 + 1) |}]
 
     let%expect_test _ =
       pp (!0 * z * y) ;
@@ -118,15 +109,15 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (!7 * z * (!2 * y)) ;
-      [%expect {| (14 × %y_1 × %z_2) |}]
+      [%expect {| (14 × (%y_1 × %z_2)) |}]
 
     let%expect_test _ =
       pp (!13 + (!42 * z)) ;
-      [%expect {| ((42 × %z_2) + 13) |}]
+      [%expect {| (42 × %z_2 + 13) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42) ;
-      [%expect {| ((13 × %z_2) + 42) |}]
+      [%expect {| (13 × %z_2 + 42) |}]
 
     let%expect_test _ =
       pp ((!2 * z) - !3 + ((!(-2) * z) + !3)) ;
@@ -134,32 +125,31 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!3 * y) + (!13 * z) + !42) ;
-      [%expect {| ((3 × %y_1) + (13 × %z_2) + 42) |}]
+      [%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y)) ;
-      [%expect {| ((3 × %y_1) + (13 × %z_2) + 42) |}]
+      [%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y) + (!2 * z)) ;
-      [%expect {| ((3 × %y_1) + (15 × %z_2) + 42) |}]
+      [%expect {| (3 × %y_1 + 15 × %z_2 + 42) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 + (!3 * y) + (!(-13) * z)) ;
-      [%expect {| ((3 × %y_1) + 42) |}]
+      [%expect {| (3 × %y_1 + 42) |}]
 
     let%expect_test _ =
       pp (z + !42 + ((!3 * y) + (!(-1) * z))) ;
-      [%expect {| ((3 × %y_1) + 42) |}]
+      [%expect {| (3 × %y_1 + 42) |}]
 
     let%expect_test _ =
       pp (!(-1) * (z + (!(-1) * y))) ;
-      [%expect {| (%y_1 + (-1 × %z_2)) |}]
+      [%expect {| (%y_1 + -1 × %z_2) |}]
 
     let%expect_test _ =
       pp (((!3 * y) + !2) * (!4 + (!5 * z))) ;
-      [%expect
+      [%expect {| (15 × (%y_1 × %z_2) + 12 × %y_1 + 10 × %z_2 + 8) |}]
-        {| ((15 × %y_1 × %z_2) + (12 × %y_1) + (10 × %z_2) + 8) |}]
 
     let%expect_test _ =
       pp (((!2 * z) - !3 + ((!(-2) * z) + !3)) * (!4 + (!5 * z))) ;
@@ -167,11 +157,11 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!13 * z) + !42 - ((!3 * y) + (!13 * z))) ;
-      [%expect {| ((-3 × %y_1) + 42) |}]
+      [%expect {| (-3 × %y_1 + 42) |}]
 
     let%expect_test _ =
       pp (z = y) ;
-      [%expect {| (%y_1 = %z_2) |}]
+      [%expect {| (%z_2 = %y_1) |}]
 
     let%expect_test _ =
       pp (z = z) ;
@@ -203,55 +193,55 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (y - (!(-3) * y) + !4) ;
-      [%expect {| ((4 × %y_1) + 4) |}]
+      [%expect {| (4 × %y_1 + 4) |}]
 
     let%expect_test _ =
       pp ((!(-3) * y) + !4 - y) ;
-      [%expect {| ((-4 × %y_1) + 4) |}]
+      [%expect {| (-4 × %y_1 + 4) |}]
 
     let%expect_test _ =
       pp (y = (!(-3) * y) + !4) ;
-      [%expect {| ((4 × %y_1) = 4) |}]
+      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
 
     let%expect_test _ =
       pp ((!(-3) * y) + !4 = y) ;
-      [%expect {| ((4 × %y_1) = 4) |}]
+      [%expect {| ((-3 × %y_1 + 4) = %y_1) |}]
 
     let%expect_test _ =
       pp (Exp.sub Typ.bool (Exp.bool true) (z = !4)) ;
-      [%expect {| ((%z_2 = 4) + -1) |}]
+      [%expect {| (-1 × (%z_2 = 4) + -1) |}]
 
     let%expect_test _ =
       pp (Exp.add Typ.bool (Exp.bool true) (z = !4) = (z = !4)) ;
-      [%expect {| 0 |}]
+      [%expect {| (((%z_2 = 4) + -1) = (%z_2 = 4)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((3 × %y_1) = 42) |}]
+      [%expect {| ((13 × %z_2 + 42) = (3 × %y_1 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !(-42) = (!3 * y) + (!13 * z)) ;
-      [%expect {| ((-3 × %y_1) = 42) |}]
+      [%expect {| ((13 × %z_2 + -42) = (3 × %y_1 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| ((-3 × %y_1) = 42) |}]
+      [%expect {| ((13 × %z_2 + 42) = (-3 × %y_1 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ((!10 * z) + !42 = (!(-3) * y) + (!13 * z)) ;
-      [%expect {| (((-3 × %y_1) + (3 × %z_2)) = 42) |}]
+      [%expect {| ((10 × %z_2 + 42) = (-3 × %y_1 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ~~((!13 * z) + !(-42) != (!3 * y) + (!13 * z)) ;
-      [%expect {| ((-3 × %y_1) = 42) |}]
+      [%expect {| ((13 × %z_2 + -42) = (3 × %y_1 + 13 × %z_2)) |}]
 
     let%expect_test _ =
       pp ~~(y > !2 && z <= !3) ;
-      [%expect {| ((%z_2 > 3) || (%y_1 <= 2)) |}]
+      [%expect {| ((%y_1 <= 2) || (%z_2 > 3)) |}]
 
     let%expect_test _ =
       pp ~~(y >= !2 || z < !3) ;
-      [%expect {| ((%z_2 >= 3) && (%y_1 < 2)) |}]
+      [%expect {| ((%y_1 < 2) && (%z_2 >= 3)) |}]
 
     let%expect_test _ =
       pp Exp.(eq z null) ;
@@ -261,7 +251,7 @@ let%test_module _ =
         {|
         (%z_2 = null)
 
-        (%z_2 = null)
+        (null = %z_2)
 
-        (%z_2 = null) |}]
+        (null = %z_2) |}]
   end )

sledge/src/symbheap/congruence.ml

@@ -7,16 +7,65 @@
 
 (** Congruence closure with integer offsets *)
 
-(* For background, see:
+(** For background, see:
-
+
-   Robert Nieuwenhuis, Albert Oliveras: Fast congruence closure and
+    Robert Nieuwenhuis, Albert Oliveras: Fast congruence closure and
-   extensions. Inf. Comput. 205(4): 557-580 (2007)
+    extensions. Inf. Comput. 205(4): 557-580 (2007)
-
+
-   and, for a more detailed correctness proof of the case without integer
+    and, for a more detailed correctness proof of the case without integer
-   offsets, see section 5 of:
+    offsets, see section 5 of:
-
+
-   Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine: Structuring the
+    Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine: Structuring the
-   verification of heap-manipulating programs. POPL 2010: 261-274 *)
+    verification of heap-manipulating programs. POPL 2010: 261-274 *)
+
+(** Lazy flattening:
+
+    The congruence closure data structure is used to lazily flatten
+    expressions. Flattening expressions gives each compound expression (e.g.
+    an application) a "name", which is treated as an atomic symbol. In the
+    background papers, fresh symbols are introduced to name compound
+    expressions in a pre-processing pass, but here we do not a priori know
+    the carrier (set of all expressions equations might relate). Instead, we
+    use the expression itself as its "name" and use the representative map
+    to record this naming. That is, if [f(a+i)] is in the domain of the
+    representative map, then "f(a+i)" is the name of the compound expression
+    [f(a+i)]. If [f(a+i)] is not in the domain of the representative map,
+    then it is not yet in the "carrier" of the relation. Adding it to the
+    carrier, which logically amounts to adding the equation [f(a+i) =
+    "f(a+i)"], extends the representative map, as well as the lookup map and
+    use lists, after which [f(a+i)] can be used as if it was a simple symbol
+    name for the compound expression.
+
+    Note that merging a compound equation of the form [f(a+i)+j = b+k]
+    results in naming [f(a+i)] and then merging the simple equation
+    ["f(a+i)"+j = b+k] normalized to ["f(a+i)" = b+(k-j)]. In particular,
+    every equation is either of the form ["f(a+i)" = f(a+i)] or of the form
+    [a = b+i], but not of the form [f(a+i) = b+j].
+
+    By the same reasoning, the range of the lookup table does not need
+    offsets, as every exp in the range of the lookup table will be the name
+    of a compound exp.
+
+    A consequence of lazy flattening is that the equations stored in the
+    lookup table, use lists, and pending equation list in the background
+    papers are here all of the form [f(a+i) = "f(a+i)"], and hence are
+    represented by the application expression itself.
+
+    Sparse carrier:
+
+    For symbols, that is expressions that are not compound [App]lications,
+    there are no cooperative invariants between components of the data
+    structure that need to be established. So adding a symbol to the carrier
+    would amount to adding an identity association to the representatives
+    map. Since we need to use a map instead of an array anyhow, this can be
+    represented sparsely by omitting identity associations in the
+    representative map. Note that identity associations for compound
+    expressions are still needed to record which compound expressions have
+    been added to the carrier.
+
+    Notation:
+
+    - often use identifiers such as [a'] for the representative of [a] *)
 
 (** set of exps representing congruence classes *)
 module Cls = struct
@@ -33,8 +82,10 @@ module Cls = struct
   let remove_exn = List.remove_exn
   let union = List.rev_append
   let fold_map = List.fold_map
+  let iter = List.iter
   let is_empty = List.is_empty
   let length = List.length
+  let map = List.map_preserving_phys_equal
   let mem = List.mem ~equal:Exp.equal
 end
 
@@ -44,70 +95,71 @@ module Use = struct
 
   let equal = [%compare.equal: t]
 
-  let pp fs use =
+  let pp fs uses =
-    Format.fprintf fs "@[<hov 1>{@[%a@]}@]" (List.pp ",@ " Exp.pp) use
+    Format.fprintf fs "@[<hov 1>{@[%a@]}@]" (List.pp ",@ " Exp.pp) uses
 
   let empty = []
-  let singleton exp = [exp]
+  let singleton use = [use]
-  let add use exp = exp :: use
+  let add uses use = use :: uses
   let union = List.rev_append
   let fold = List.fold
+  let iter = List.iter
+  let exists = List.exists
   let is_empty = List.is_empty
+  let map = List.map_preserving_phys_equal
 end
 
 type 'a exp_map = 'a Map.M(Exp).t [@@deriving compare, sexp]
 
-let empty_map = Map.empty (module Exp)
+(** see also [invariant] *)
-
 type t =
-  { sat: bool  (** [false] if constraints are inconsistent *)
+  { sat: bool  (** [false] only if constraints are inconsistent *)
   ; rep: Exp.t exp_map
-        (** map [a] to [a'+k], indicating that [a=a'+k] holds, and that [a']
+        (** map [a] to [a'+k], indicating that [a = a'+k] holds, and that
-            (without the offset [k]) is the 'rep(resentative)' of [a] *)
+            [a'] (without the offset [k]) is the 'rep(resentative)' of [a] *)
   ; lkp: Exp.t exp_map
-        (** inverse of mapping rep over sub-expressions: map [f'(a'+i)] to
+        (** map [f'(a'+i)] to [f(a+j)], indicating that [f'(a'+i) = f(a+j)]
-            [f(a+j)+k], an (offsetted) app(lication expression) in the
+            holds, where [f(a+j)] is in the carrier *)
-            relation which normalizes to one in the 'equivalence modulo
-            offset' class of [f'(a'+i)], indicating that [f'(a'+i) =
-            f(a+j)+k] holds, for some [k] where [rep f = f'] and [rep a =
-            a'+(i-j)] *)
   ; cls: Cls.t exp_map
         (** inverse rep: map each rep [a'] to all the [a+k] in its class,
-            i.e., [cls a' = {a+k | rep a = a'+(-k)}] *)
+            i.e., [cls a' = {a+(-k) | rep a = a'+k}] *)
   ; use: Use.t exp_map
         (** super-expression relation for representatives: map each
-            representative [a'] of [a] to the application expressions in the
+            representative [a'] of [a] to the compound expressions in the
-            relation where [a] (possibly + an offset) appears as an
+            carrier where [a] (possibly + an offset) appears as an immediate
-            immediate sub-expression *)
+            sub-expression *)
   ; pnd: (Exp.t * Exp.t) list
-        (** equations to be added to the relation, to enable delaying adding
+        (** equations of the form [a+i = b+j], where [a] and [b] are in the
-            equations discovered while invariants are temporarily broken *)
+            carrier, to be added to the relation by merging the classes of
-  }
+            [a] and [b] *) }
 [@@deriving compare, sexp]
 
-(** The expressions in the range of [lkp] and [use], as well as those in
+(** Pretty-printing *)
-    [pnd], are 'in the relation' in the sense that there is some constraint
-    involving them, and in practice are expressions which have been passed
-    to [merge] as opposed to having been constructed internally. *)
 
 let pp_eq fs (e, f) = Format.fprintf fs "@[%a = %a@]" Exp.pp e Exp.pp f
 
 let pp fs {sat; rep; lkp; cls; use; pnd} =
   let pp_alist pp_k pp_v fs alist =
     let pp_assoc fs (k, v) =
-      Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_k k pp_v v
+      Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_k k pp_v (k, v)
     in
     Format.fprintf fs "[@[<hv>%a@]]" (List.pp ";@ " pp_assoc) alist
   in
-  let pp_pnd fs pnd =
+  let pp_exp_v fs (k, v) = if not (Exp.equal k v) then Exp.pp fs v in
-    if not (List.is_empty pnd) then
+  let pp_cls_v fs (_, v) = Cls.pp fs v in
-      Format.fprintf fs ";@ pnd= [@[<hv>%a@]];" (List.pp ";@ " pp_eq) pnd
+  let pp_use_v fs (_, v) = Use.pp fs v in
-  in
   Format.fprintf fs
     "@[{@[<hv>sat= %b;@ rep= %a;@ lkp= %a;@ cls= %a;@ use= %a%a@]}@]" sat
-    (pp_alist Exp.pp Exp.pp) (Map.to_alist rep) (pp_alist Exp.pp Exp.pp)
+    (pp_alist Exp.pp pp_exp_v)
-    (Map.to_alist lkp) (pp_alist Exp.pp Cls.pp) (Map.to_alist cls)
+    (Map.to_alist rep)
-    (pp_alist Exp.pp Use.pp) (Map.to_alist use) pp_pnd pnd
+    (pp_alist Exp.pp pp_exp_v)
+    (Map.to_alist lkp)
+    (pp_alist Exp.pp pp_cls_v)
+    (Map.to_alist cls)
+    (pp_alist Exp.pp pp_use_v)
+    (Map.to_alist use)
+    (List.pp ~pre:";@ pnd= [@[<hv>" ";@ " pp_eq ~suf:"@]];")
+    pnd
 
 let pp_classes fs {cls} =
   List.pp "@ @<2>∧ "
@@ -138,32 +190,41 @@ let pp_diff fs (r, s) =
   let pp_sdiff_exps fs (c, d) =
     pp_sdiff_list "" Exp.pp Exp.compare fs (c, d)
   in
-  let pp_sdiff_elt pp_val pp_sdiff_val fs = function
+  let pp_sdiff_uses fs (c, d) =
+    pp_sdiff_list "" Exp.pp Exp.compare fs (c, d)
+  in
+  let pp_sdiff_elt pp_key pp_val pp_sdiff_val fs = function
     | k, `Left v ->
-        Format.fprintf fs "-- [@[%a@ @<2>↦ %a@]]" Exp.pp k pp_val v
+        Format.fprintf fs "-- [@[%a@ @<2>↦ %a@]]" pp_key k pp_val v
     | k, `Right v ->
-        Format.fprintf fs "++ [@[%a@ @<2>↦ %a@]]" Exp.pp k pp_val v
+        Format.fprintf fs "++ [@[%a@ @<2>↦ %a@]]" pp_key k pp_val v
     | k, `Unequal vv ->
-        Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" Exp.pp k pp_sdiff_val vv
+        Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_key k pp_sdiff_val vv
   in
   let pp_sdiff_exp_map =
     let pp_sdiff_exp fs (u, v) =
       Format.fprintf fs "-- %a ++ %a" Exp.pp u Exp.pp v
     in
-    pp_sdiff_map (pp_sdiff_elt Exp.pp pp_sdiff_exp) Exp.equal
+    pp_sdiff_map (pp_sdiff_elt Exp.pp Exp.pp pp_sdiff_exp) Exp.equal
+  in
+  let pp_sdiff_app_map =
+    let pp_sdiff_app fs (u, v) =
+      Format.fprintf fs "-- %a ++ %a" Exp.pp u Exp.pp v
+    in
+    pp_sdiff_map (pp_sdiff_elt Exp.pp Exp.pp pp_sdiff_app) Exp.equal
   in
   let pp_sat fs =
     if not (Bool.equal r.sat s.sat) then
       Format.fprintf fs "sat= @[-- %b@ ++ %b@];@ " r.sat s.sat
   in
   let pp_rep fs = pp_sdiff_exp_map "rep" fs r.rep s.rep in
-  let pp_lkp fs = pp_sdiff_exp_map "lkp" fs r.lkp s.lkp in
+  let pp_lkp fs = pp_sdiff_app_map "lkp" fs r.lkp s.lkp in
   let pp_cls fs =
-    let pp_sdiff_cls = pp_sdiff_elt Cls.pp pp_sdiff_exps in
+    let pp_sdiff_cls = pp_sdiff_elt Exp.pp Cls.pp pp_sdiff_exps in
     pp_sdiff_map pp_sdiff_cls Cls.equal "cls" fs r.cls s.cls
   in
   let pp_use fs =
-    let pp_sdiff_use = pp_sdiff_elt Use.pp pp_sdiff_exps in
+    let pp_sdiff_use = pp_sdiff_elt Exp.pp Use.pp pp_sdiff_uses in
     pp_sdiff_map pp_sdiff_use Use.equal "use" fs r.use s.use
   in
   let pp_pnd fs =
@@ -172,46 +233,177 @@ let pp_diff fs (r, s) =
   Format.fprintf fs "@[{@[<hv>%t%t%t%t%t%t@]}@]" pp_sat pp_rep pp_lkp pp_cls
     pp_use pp_pnd
 
-let invariant r =
+(** Auxiliary functions for manipulating "base plus offset" expressions *)
-  Invariant.invariant [%here] r [%sexp_of: t]
-  @@ fun () ->
-  Map.iteri r.rep ~f:(fun ~key:e ~data:e' -> assert (not (Exp.equal e e'))) ;
-  Map.iteri r.cls ~f:(fun ~key:e' ~data:cls -> assert (Cls.mem cls e')) ;
-  Map.iteri r.use ~f:(fun ~key:_ ~data:use -> assert (not (Use.is_empty use))
-  )
 
-(* Auxiliary functions for manipulating "base plus offset" expressions *)
+(** solve a+i = b for a, yielding a = b-i *)
-
+let solve_for_base ai b =
-let map_sum e ~f =
+  match Exp.base_offset ai with
-  match e with
+  | Some (a, i, typ) -> (a, Exp.sub typ b (Exp.integer i typ))
-  | Exp.App {op= App {op= Add {typ}; arg= a}; arg= i} ->
+  | None -> (ai, b)
+
+(** subtract offset from both sides of equation a+i = b, yielding b-i *)
+let subtract_offset ai b =
+  match Exp.offset ai with
+  | Some (i, typ) -> Exp.sub typ b (Exp.integer i typ)
+  | None -> b
+
+(** [map_base ~f a+i] is [f(a) + i] and [map_base ~f a] is [f(a)] *)
+let map_base ai ~f =
+  match Exp.base_offset ai with
+  | Some (a, i, typ) ->
       let a' = f a in
-      if a' == a then e else Exp.add typ a' i
+      if a' == a then ai else Exp.add typ a' (Exp.integer i typ)
-  | a -> f a
+  | None -> f ai
 
-let fold_sum e ~init ~f =
+(** [norm_base r a] is [a'+k] where [r] implies [a = a'+k] and [a'] is a
-  match e with
+    rep, requires [a] to not have any offset and be in the carrier *)
-  | Exp.App {op= App {op= Add _; arg= a}; arg= Integer _} -> f init a
+let norm_base r e =
-  | a -> f init a
+  assert (Option.is_none (Exp.offset e)) ;
+  try Map.find_exn r.rep e with Caml.Not_found ->
+    assert (Exp.is_simple e) ;
+    e
 
-let base_of = function
+(** [norm r a+i] is [a'+k] where [r] implies [a+i = a'+k] and [a'] is a rep,
-  | Exp.App {op= App {op= Add _; arg= a}; arg= Integer _} -> a
+    requires [a] to be in the carrier *)
-  | a -> a
+let norm r e = map_base ~f:(norm_base r) e
 
-(** solve a+i = b for a, yielding a = b-i *)
+(** test membership in carrier, strictly in the sense that an exp with an
-let solve_for_base ai b =
+    offset is not in the carrier even when its base is *)
-  match ai with
+let in_car r e = Exp.is_simple e || Map.mem r.rep e
-  | Exp.App {op= App {op= Add {typ}; arg= a}; arg= i} -> (a, Exp.sub typ b i)
-  | _ -> (ai, b)
 
-(** [norm r a+i] = [a'+k] where [r] implies [a+i=a'+k] and [a'] is a rep *)
+(** test if an exp is a representative, requires exp to have no offset *)
-let norm r e =
+let is_rep r e = Exp.equal e (norm_base r e)
-  map_sum e ~f:(fun a -> try Map.find_exn r.rep a with Caml.Not_found -> a)
 
-(* Core closure operations *)
+let pre_invariant r =
+  Invariant.invariant [%here] r [%sexp_of: t]
+  @@ fun () ->
+  Map.iteri r.rep ~f:(fun ~key:a ~data:a'k ->
+      (* carrier is stored without offsets *)
+      assert (Option.is_none (Exp.offset a)) ;
+      (* carrier is closed under sub-expressions *)
+      Exp.iter a ~f:(fun bj ->
+          assert (
+            in_car r (Exp.base bj)
+            || Trace.report "@[subexp %a of %a not in carrier of@ %a@]"
+                 Exp.pp bj Exp.pp a pp r ) ) ;
+      let a', a_k = solve_for_base a'k a in
+      (* carrier is closed under rep *)
+      assert (in_car r a') ;
+      if Exp.is_simple a' then
+        (* rep is sparse for symbols *)
+        assert (
+          (not (Map.mem r.rep a'))
+          || Trace.report
+               "no symbol rep should be in rep domain: %a @<2>↦ %a@\n%a"
+               Exp.pp a Exp.pp a' pp r )
+      else
+        (* rep is idempotent for applications *)
+        assert (
+          is_rep r a'
+          || Trace.report
+               "every app rep should be its own rep: %a @<2>↦ %a" Exp.pp a
+               Exp.pp a' ) ;
+      match Map.find r.cls a' with
+      | None ->
+          (* every rep in dom of cls *)
+          assert (
+            Trace.report "rep not in dom of cls: %a@\n%a" Exp.pp a' pp r )
+      | Some a_cls ->
+          (* every exp is in class of its rep *)
+          assert (
+            (* rep a = a'+k so expect a-k in cls a' *)
+            Cls.mem a_cls a_k
+            || Trace.report "%a = %a by rep but %a not in cls@\n%a" Exp.pp a
+                 Exp.pp a'k Exp.pp a_k pp r ) ) ;
+  Map.iteri r.cls ~f:(fun ~key:a' ~data:a_cls ->
+      (* domain of cls are reps *)
+      assert (is_rep r a') ;
+      (* cls contained in inverse of rep *)
+      Cls.iter a_cls ~f:(fun ak ->
+          let a, a'_k = solve_for_base ak a' in
+          assert (
+            in_car r a
+            || Trace.report "%a in cls of %a but not in carrier" Exp.pp a
+                 Exp.pp a' ) ;
+          let a'' = norm_base r a in
+          assert (
+            (* a' = a+k in cls so expect rep a = a'-k *)
+            Exp.equal a'' a'_k
+            || Trace.report "%a = %a by cls but @<2>≠ %a by rep" Exp.pp a'
+                 Exp.pp ak Exp.pp a'' ) ) ) ;
+  Map.iteri r.use ~f:(fun ~key:a' ~data:a_use ->
+      assert (
+        (not (Use.is_empty a_use))
+        || Trace.report "empty use list should not have been added" ) ;
+      Use.iter a_use ~f:(fun u ->
+          (* uses are applications *)
+          assert (not (Exp.is_simple u)) ;
+          (* uses have no offsets *)
+          assert (Option.is_none (Exp.offset u)) ;
+          (* subexps of uses in carrier *)
+          Exp.iter u ~f:(fun bj -> assert (in_car r (Exp.base bj))) ;
+          (* every rep is a subexp-modulo-rep of each of its uses *)
+          assert (
+            Exp.exists u ~f:(fun bj -> Exp.equal a' (Exp.base (norm r bj)))
+            || Trace.report
+                 "rep %a has use %a, but is not the rep of any immediate \
+                  subexp of the use"
+                 Exp.pp a' Exp.pp u ) ;
+          (* every use has a corresponding entry in lkp... *)
+          let v =
+            try Map.find_exn r.lkp (Exp.map ~f:(norm r) u)
+            with Caml.Not_found ->
+              fail "no lkp entry for use %a of %a" Exp.pp u Exp.pp a'
+          in
+          (* ...which is (eventually) provably equal *)
+          if List.is_empty r.pnd then
+            assert (Exp.equal (norm_base r u) (norm_base r v)) ) ) ;
+  Map.iteri r.lkp ~f:(fun ~key:a ~data:c ->
+      (* subexps of domain of lkp in carrier *)
+      Exp.iter a ~f:(fun bj -> assert (in_car r (Exp.base bj))) ;
+      (* range of lkp are applications in carrier *)
+      assert (in_car r c) ;
+      (* there may be stale entries in lkp whose subexps are no longer reps,
+         which will therefore never be used, and hence are unconstrained *)
+      if Exp.equal a (Exp.map ~f:(norm r) a) then (
+        let c_' = Exp.map ~f:(norm r) c in
+        (* lkp contains equalities provable modulo normalizing sub-exps *)
+        assert (
+          Exp.equal a c_'
+          || Trace.report "%a sub-normalizes to %a @<2>≠ %a" Exp.pp c
+               Exp.pp c_' Exp.pp a ) ;
+        let c' = norm_base r c in
+        Exp.iter a ~f:(fun bj ->
+            (* every subexp of an app in domain of lkp has an associated use *)
+            let b' = Exp.base (norm r bj) in
+            let b_use =
+              try Map.find_exn r.use b' with Caml.Not_found ->
+                fail "no use list for subexp %a of lkp key %a" Exp.pp bj
+                  Exp.pp a
+            in
+            assert (
+              Use.exists b_use ~f:(fun u ->
+                  Exp.equal a (Exp.map ~f:(norm r) u)
+                  && Exp.equal c' (norm_base r u) )
+              || Trace.report
+                   "no corresponding use for subexp %a of lkp key %a" Exp.pp
+                   bj Exp.pp a ) ) ) ) ;
+  List.iter r.pnd ~f:(fun (ai, bj) ->
+      assert (in_car r (Exp.base ai)) ;
+      assert (in_car r (Exp.base bj)) )
+
+let invariant r =
+  Invariant.invariant [%here] r [%sexp_of: t]
+  @@ fun () ->
+  pre_invariant r ;
+  assert (List.is_empty r.pnd)
+
+(** Core closure operations *)
 
 type prefer = Exp.t -> over:Exp.t -> int
 
+let empty_map = Map.empty (module Exp)
+
 let true_ =
   { sat= true
   ; rep= empty_map
@@ -219,42 +411,9 @@ let true_ =
   ; cls= empty_map
   ; use= empty_map
   ; pnd= [] }
+  |> check invariant
 
-let false_ = {true_ with sat= false}
+let false_ = {true_ with sat= false} |> check invariant
-
-(** Add app exps (and sub-exps) to the relation. This populates the [lkp]
-    and [use] maps, treating an exp [e] of form [f(a)] as an equation
-    between the app [f(a)] and the 'symbol' [e]. This has the effect of
-    using [e] as a 'name' of the app [f(a)], rather than using an explicit
-    'flattening' transformation introducing new symbols for each
-    application. *)
-let rec extend r e =
-  fold_sum e ~init:r ~f:(fun r -> function
-    | App _ as fa ->
-        let r, fa' =
-          Exp.fold_map fa ~init:r ~f:(fun r b ->
-              let r, c = extend r b in
-              (r, norm r c) )
-        in
-        Map.find_or_add r.lkp fa'
-          ~if_found:(fun d ->
-            let r = {r with pnd= (e, d) :: r.pnd} in
-            (r, d) )
-          ~default:e
-          ~if_added:(fun lkp ->
-            let use =
-              Exp.fold fa' ~init:r.use ~f:(fun use b' ->
-                  if Exp.is_constant b' then use
-                  else
-                    Map.update use b' ~f:(function
-                      | Some b_use -> Use.add b_use fa
-                      | None -> Use.singleton fa ) )
-            in
-            let r = {r with lkp; use} in
-            (r, e) )
-    | _ -> (r, e) )
-
-exception Unsat
 
 (** Add an equation [b+j] = [a+i] using [a] as the new rep. This removes [b]
     from the [cls] and [use] maps, as it is no longer a rep. The [rep] map
@@ -267,9 +426,12 @@ let add_directed_equation r0 ~exp:bj ~rep:ai =
   [%Trace.call fun {pf} -> pf "@[%a@ %a@]@ %a" Exp.pp bj Exp.pp ai pp r0]
   ;
   let r = r0 in
-  let a = base_of ai in
   (* b+j = a+i so b = a+i-j *)
-  let b, ai_j = solve_for_base bj ai in
+  let b, aij = solve_for_base bj ai in
+  assert ((not (in_car r b)) || is_rep r b) ;
+  (* compute a from aij in case ai is an int and j is a non-0 offset *)
+  let a = Exp.base aij in
+  assert ((not (in_car r a)) || is_rep r a) ;
   let b_cls, cls =
     try Map.find_and_remove_exn r.cls b with Caml.Not_found ->
       (Cls.singleton b, r.cls)
@@ -278,32 +440,29 @@ let add_directed_equation r0 ~exp:bj ~rep:ai =
     try Map.find_and_remove_exn r.use b with Caml.Not_found ->
       (Use.empty, r.use)
   in
-  let rep, a_cls_delta =
+  let r, a_cls_delta =
-    Cls.fold_map b_cls ~init:r.rep ~f:(fun rep ck ->
+    Cls.fold_map b_cls ~init:r ~f:(fun r ck ->
         (* c+k = b = a+i-j so c = a+i-j-k *)
-        let c, ai_j_k = solve_for_base ck ai_j in
+        let c, aijk = solve_for_base ck aij in
-        if Exp.is_false (Exp.eq c ai_j_k) then raise Unsat ;
+        let r =
-        let rep = Map.set rep ~key:c ~data:ai_j_k in
+          if Exp.equal a c || Exp.is_false (Exp.eq c aijk) then false_
-        (* a+i-j = c+k so a = c+k+j-i *)
+          else if Exp.is_simple c && Exp.equal c aijk then r
-        let _, ckj_i = solve_for_base ai_j ck in
+          else {r with rep= Map.set r.rep ~key:c ~data:aijk}
-        (rep, ckj_i) )
+        in
-  in
+        (* a+i-j-k = c so a = c-i+j+k *)
-  let cls =
+        let cijk = subtract_offset aijk c in
-    Map.update cls a ~f:(function
+        (r, cijk) )
-      | Some a_cls -> Cls.union a_cls_delta a_cls
-      | None -> Cls.add a_cls_delta a )
   in
-  let r = {r with rep; cls; use} in
   let r, a_use_delta =
     Use.fold b_use ~init:(r, Use.empty) ~f:(fun (r, a_use_delta) u ->
-        let u' = Exp.map ~f:(norm r) u in
+        let u_' = Exp.map ~f:(norm r) u in
-        Map.find_or_add r.lkp u'
+        Map.find_or_add r.lkp u_'
           ~if_found:(fun v ->
             let r = {r with pnd= (u, v) :: r.pnd} in
-            (* no need to add u to use a since u is an app already in r
+            (* no need to add u to use a since u is already in r (since u_'
-               (since u' found in r.lkp) that is equal to v, so will be in
+               found in r.lkp) that is equal to v, so will be in use of u_'s
-               use of u's subexps, and u = v is added to pnd so propagate
+               subexps, and u = v is added to pnd so propagate will combine
-               will combine them later *)
+               them later *)
             (r, a_use_delta) )
           ~default:u
           ~if_added:(fun lkp ->
@@ -311,6 +470,11 @@ let add_directed_equation r0 ~exp:bj ~rep:ai =
             let a_use_delta = Use.add a_use_delta u in
             (r, a_use_delta) ) )
   in
+  let cls =
+    Map.update cls a ~f:(function
+      | Some a_cls -> Cls.union a_cls_delta a_cls
+      | None -> Cls.add a_cls_delta a )
+  in
   let use =
     if Use.is_empty a_use_delta then use
     else
@@ -318,105 +482,136 @@ let add_directed_equation r0 ~exp:bj ~rep:ai =
         | Some a_use -> Use.union a_use_delta a_use
         | None -> a_use_delta )
   in
-  let r = {r with use} in
+  let r = if not r.sat then false_ else {r with cls; use} in
-  r |> check invariant
+  r
   |>
-  [%Trace.retn fun {pf} r -> pf "%a" pp_diff (r0, r)]
+  [%Trace.retn fun {pf} r ->
+    pf "%a" pp_diff (r0, r) ;
+    pre_invariant r]
 
-(** Close the relation with the pending equations. *)
+let prefer_rep ?prefer r e ~over:d =
-let rec propagate_ ?prefer r =
+  [%Trace.call fun {pf} -> pf "@[%a@ %a@]@ %a" Exp.pp d Exp.pp e pp r]
-  [%Trace.call fun {pf} -> pf "%a" pp r]
   ;
-  ( match r.pnd with
+  let prefer_e_over_d =
-  | [] -> r
+    match (Exp.is_constant d, Exp.is_constant e) with
-  | (d, e) :: pnd ->
+    | true, false -> -1
-      let d' = norm r d in
+    | false, true -> 1
-      let e' = norm r e in
+    | _ -> (
-      let r = {r with pnd} in
+      match prefer with Some prefer -> prefer e ~over:d | None -> 0 )
-      let r =
+  in
-        if Exp.equal (base_of d') (base_of e') then
+  ( match prefer_e_over_d with
-          if Exp.equal d' e' then r else {r with sat= false; pnd= []}
+  | n when n < 0 -> false
-        else
+  | p when p > 0 -> true
-          let prefer_e_over_d =
+  | _ ->
-            match (Exp.is_constant d, Exp.is_constant e) with
+      let len_e =
-            | true, false -> -1
+        try Cls.length (Map.find_exn r.cls e) with Caml.Not_found -> 1
-            | false, true -> 1
+      in
-            | _ -> (
+      let len_d =
-              match prefer with
+        try Cls.length (Map.find_exn r.cls d) with Caml.Not_found -> 1
-              | Some prefer -> prefer e' ~over:d'
-              | None -> 0 )
-          in
-          match prefer_e_over_d with
-          | n when n < 0 -> add_directed_equation r ~exp:e' ~rep:d'
-          | p when p > 0 -> add_directed_equation r ~exp:d' ~rep:e'
-          | _ ->
-              let len_d =
-                try Cls.length (Map.find_exn r.cls d')
-                with Caml.Not_found -> 1
-              in
-              let len_e =
-                try Cls.length (Map.find_exn r.cls e')
-                with Caml.Not_found -> 1
-              in
-              if len_d > len_e then add_directed_equation r ~exp:e' ~rep:d'
-              else add_directed_equation r ~exp:d' ~rep:e'
       in
-      propagate_ ?prefer r )
+      len_e >= len_d )
   |>
-  [%Trace.retn fun {pf} r' -> pf "%a" pp_diff (r, r')]
+  [%Trace.retn fun {pf} -> pf "%b"]
+
+let choose_preferred ?prefer r d e =
+  if prefer_rep ?prefer r e ~over:d then (d, e) else (e, d)
+
+let add_equation ?prefer r d e =
+  let d = norm r d in
+  let e = norm r e in
+  if (not r.sat) || Exp.equal d e then r
+  else (
+    [%Trace.call fun {pf} -> pf "@[%a@ %a@]@ %a" Exp.pp d Exp.pp e pp r]
+    ;
+    let exp, rep = choose_preferred ?prefer r d e in
+    add_directed_equation r ~exp ~rep
+    |>
+    [%Trace.retn fun {pf} r' -> pf "%a" pp_diff (r, r')] )
+
+(** normalize, and add base to carrier if needed *)
+let rec norm_extend r ek =
+  [%Trace.call fun {pf} -> pf "%a@ %a" Exp.pp ek pp r]
+  ;
+  let e = Exp.base ek in
+  ( if Exp.is_simple e then (r, norm r ek)
+  else
+    Map.find_or_add r.rep e
+      ~if_found:(fun e' ->
+        match Exp.offset ek with
+        | Some (k, typ) -> (r, Exp.add typ e' (Exp.integer k typ))
+        | None -> (r, e') )
+      ~default:e
+      ~if_added:(fun rep ->
+        let cls = Map.set r.cls ~key:e ~data:(Cls.singleton e) in
+        let r = {r with rep; cls} in
+        let r, e_' = Exp.fold_map ~f:norm_extend ~init:r e in
+        Map.find_or_add r.lkp e_'
+          ~if_found:(fun d ->
+            let pnd = (e, d) :: r.pnd in
+            let d' = norm_base r d in
+            ({r with rep; pnd}, d') )
+          ~default:e
+          ~if_added:(fun lkp ->
+            let use =
+              Exp.fold e_' ~init:r.use ~f:(fun use b'j ->
+                  let b' = Exp.base b'j in
+                  Map.update use b' ~f:(function
+                    | Some b_use -> Use.add b_use e
+                    | None -> Use.singleton e ) )
+            in
+            ({r with lkp; use}, e) ) ) )
+  |>
+  [%Trace.retn fun {pf} (r', e') -> pf "%a@ %a" Exp.pp e' pp_diff (r, r')]
 
-let propagate ?prefer r =
+let norm_extend r ek = norm_extend r ek |> check (fst >> pre_invariant)
+let extend r ek = fst (norm_extend r ek)
+
+(** Close the relation with the pending equations. *)
+let rec propagate ?prefer r =
   [%Trace.call fun {pf} -> pf "%a" pp r]
   ;
-  (try propagate_ ?prefer r with Unsat -> false_)
+  ( match r.pnd with
+  | (d, e) :: pnd ->
+      let r = {r with pnd} in
+      let r = add_equation ?prefer r d e in
+      propagate ?prefer r
+  | [] -> r )
   |>
-  [%Trace.retn fun {pf} r' -> pf "%a" pp_diff (r, r')]
+  [%Trace.retn fun {pf} r' ->
+    pf "%a" pp_diff (r, r') ;
+    invariant r']
 
 let merge ?prefer r d e =
   if not r.sat then r
   else
-    let r, a = extend r d in
+    let r = extend r d in
-    let r =
+    let r = extend r e in
-      if Exp.equal d e then r
+    let r = add_equation ?prefer r d e in
-      else
-        let r, b = extend r e in
-        let r = {r with pnd= (a, b) :: r.pnd} in
-        r
-    in
     propagate ?prefer r
 
-let rec normalize_ r e =
+let rec normalize r ek =
-  [%Trace.call fun {pf} -> pf "%a" Exp.pp e]
+  [%Trace.call fun {pf} -> pf "%a@ %a" Exp.pp ek pp r]
   ;
-  map_sum e ~f:(function
+  map_base ek ~f:(fun e ->
-    | App _ as fa -> (
+      try Map.find_exn r.rep e with Caml.Not_found ->
-        let fa' = Exp.map ~f:(normalize_ r) fa in
+        Exp.map ~f:(normalize r) e )
-        match Map.find_exn r.lkp fa' with
-        | exception _ -> fa'
-        | c -> norm r (Exp.map ~f:(norm r) c) )
-    | c ->
-        let c' = norm r c in
-        if c' == c then c else normalize_ r c' )
   |>
   [%Trace.retn fun {pf} -> pf "%a" Exp.pp]
 
-let normalize r e =
+let mem_eq r d e = Exp.equal (normalize r d) (normalize r e)
-  [%Trace.call fun {pf} -> pf "%a" pp r]
-  ;
-  normalize_ r e
-  |>
-  [%Trace.retn fun {pf} -> pf "%a" Exp.pp]
-
-let mem_eq r e f = Exp.equal (normalize r e) (normalize r f)
 
 (** Exposed interface *)
 
+let extend r e = propagate (extend r e)
 let and_eq = merge
 
 let and_ ?prefer r s =
   if not r.sat then r
   else if not s.sat then s
   else
+    let s, r =
+      if Map.length s.rep <= Map.length r.rep then (s, r) else (r, s)
+    in
     Map.fold s.rep ~init:r ~f:(fun ~key:e ~data:e' r -> merge ?prefer r e e')
 
 let or_ ?prefer r s =
@@ -435,33 +630,36 @@ let or_ ?prefer r s =
 (* assumes that f is injective and for any set of exps E, f[E] is disjoint
    from E *)
 let map_exps ({sat= _; rep; lkp; cls; use; pnd} as r) ~f =
-  [%Trace.call fun {pf} -> pf "%a@." pp r]
+  [%Trace.call fun {pf} ->
+    pf "%a" pp r ;
+    assert (List.is_empty pnd)]
   ;
-  assert (List.is_empty pnd) ;
+  let map ~equal_key ~equal_data ~f_key ~f_data m =
-  let map ~equal_data ~f_data m =
     Map.fold m ~init:m ~f:(fun ~key ~data m ->
-        let key' = f key in
+        let key' = f_key key in
         let data' = f_data data in
-        if Exp.equal key' key then
+        if equal_key key' key then
           if equal_data data' data then m else Map.set m ~key ~data:data'
-        else
+        else Map.remove m key |> Map.add_exn ~key:key' ~data:data' )
-          Map.remove m key
+  in
-          |> Map.add_exn ~key:key'
+  let rep' =
-               ~data:(if data' == data then data else data') )
+    map rep ~equal_key:Exp.equal ~equal_data:Exp.equal ~f_key:f ~f_data:f
+  in
+  let lkp' =
+    map lkp ~equal_key:Exp.equal ~equal_data:Exp.equal ~f_key:f ~f_data:f
   in
-  let exp_map = map ~equal_data:Exp.equal ~f_data:f in
+  let cls' =
-  let exp_list_map =
+    map cls ~equal_key:Exp.equal ~equal_data:[%compare.equal: Exp.t list]
-    map ~equal_data:[%compare.equal: Exp.t list]
+      ~f_key:f ~f_data:(Cls.map ~f)
-      ~f_data:(List.map_preserving_phys_equal ~f)
+  in
+  let use' =
+    map use ~equal_key:Exp.equal ~equal_data:[%compare.equal: Exp.t list]
+      ~f_key:f ~f_data:(Use.map ~f)
   in
-  let rep' = exp_map rep in
-  let lkp' = exp_map lkp in
-  let cls' = exp_list_map cls in
-  let use' = exp_list_map use in
   ( if rep' == rep && lkp' == lkp && cls' == cls && use' == use then r
   else {r with rep= rep'; lkp= lkp'; cls= cls'; use= use'} )
   |>
-  [%Trace.retn fun {pf} -> pf "%a@." pp]
+  [%Trace.retn fun {pf} r -> pf "%a" pp r ; invariant r]
 
 let rename r sub = map_exps r ~f:(fun e -> Exp.rename e sub)
 
@@ -484,30 +682,25 @@ let classes {cls} = cls
 let entails r s =
   Map.for_alli s.rep ~f:(fun ~key:e ~data:e' -> mem_eq r e e')
 
-(* a - b = k if a = b+k *)
 let difference r a b =
   [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Exp.pp a Exp.pp b pp r]
   ;
-  let r, a = extend r a in
+  let r, a = norm_extend r a in
-  let r, b = extend r b in
+  let r, b = norm_extend r b in
-  let r = propagate r in
+  ( match (a, b) with
-  let ci = normalize r a in
+  | _ when Exp.equal a b -> Some Z.zero
-  let dj = normalize r b in
+  | (AppN {op= Add {typ} | Mul {typ}} | Integer {typ}), _
-  (* a - b = (c+i) - (d+j) *)
+   |_, (AppN {op= Add {typ} | Mul {typ}} | Integer {typ}) -> (
-  ( match solve_for_base dj ci with
+      let a_b = Exp.sub typ a b in
-  (* d = (c+i)-j = c+(i-j) & c = d *)
+      let r, a_b = norm_extend r a_b in
-  | d, App {op= App {op= Add _; arg= c}; arg= Integer {data= i_j}}
+      let r = propagate r in
-    when Exp.equal d c ->
+      match normalize r a_b with Integer {data} -> Some data | _ -> None )
-      (* a - b = (c+i) - (d+j) = i-j *)
-      Some i_j
-  | Integer {data= j}, Integer {data= i} -> Some (Z.sub i j)
-  | d, ci_j when Exp.equal d ci_j -> Some Z.zero
   | _ -> None )
   |>
   [%Trace.retn fun {pf} ->
-    function
+    function Some d -> pf "%a" Z.pp_print d | None -> ()]
-    | Some d -> pf "%a" Z.pp_print d
+
-    | None -> pf "c+i: %a@ d+j: %a" Exp.pp ci Exp.pp dj]
+(** Tests *)
 
 let%test_module _ =
   ( module struct

sledge/src/symbheap/congruence.mli

@@ -24,6 +24,9 @@ type prefer = Exp.t -> over:Exp.t -> int
 val true_ : t
 (** The diagonal relation, which only equates each exp with itself. *)
 
+val extend : t -> Exp.t -> t
+(** Extend the carrier of the relation. *)
+
 val merge : ?prefer:prefer -> t -> Exp.t -> Exp.t -> t
 (** Merge the equivalence classes of exps together. If [prefer a ~over:b] is
     positive, then [b] will not be used as the representative of a class

sledge/src/symbheap/congruence_test.ml

@@ -9,16 +9,22 @@ let%test_module _ =
   ( module struct
     open Congruence
 
-    let printf pp = Format.printf "@.%a@." pp
+    (* let () = Trace.init ~margin:160 ~config:all () *)
+
+    let () = Trace.init ~margin:68 ~config:none ()
+    let printf pp = Format.printf "@\n%a@." pp
+    let pp = printf pp
+    let pp_classes = printf pp_classes
     let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq r a b)
-    let mem_eq x y r = entails r (and_eq true_ x y)
+    let mem_eq x y r = Exp.equal (normalize r x) (normalize r y)
     let i8 = Typ.integer ~bits:8
     let i64 = Typ.integer ~bits:64
     let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz
     let ( + ) = Exp.add Typ.siz
     let ( - ) = Exp.sub Typ.siz
+    let ( * ) = Exp.mul Typ.siz
     let f = Exp.convert ~dst:i64 ~src:i8
-    let g = Exp.xor
+    let g = Exp.rem
     let wrt = Var.Set.empty
     let t_, wrt = Var.fresh "t" ~wrt
     let u_, wrt = Var.fresh "u" ~wrt
@@ -37,6 +43,11 @@ let%test_module _ =
     let f1 = of_eqs [(!0, !1)]
 
     let%test _ = is_false f1
+
+    let%expect_test _ =
+      pp f1 ;
+      [%expect {| {sat= false; rep= []; lkp= []; cls= []; use= []} |}]
+
     let%test _ = Map.is_empty (classes f1)
     let%test _ = is_false (merge f1 !1 !1)
 
@@ -65,49 +76,73 @@ let%test_module _ =
     let r0 = true_
 
     let%expect_test _ =
-      printf pp r0 ;
+      pp r0 ;
       [%expect {| {sat= true; rep= []; lkp= []; cls= []; use= []} |}]
 
-    let%expect_test _ = printf pp_classes r0 ; [%expect {| |}]
+    let%expect_test _ = pp_classes r0 ; [%expect {| |}]
     let%test _ = difference r0 (f x) (f x) |> Poly.equal (Some (Z.of_int 0))
     let%test _ = difference r0 !4 !3 |> Poly.equal (Some (Z.of_int 1))
 
     let r1 = of_eqs [(x, y)]
 
-    let%test _ = not (Map.is_empty (classes r1))
-
     let%expect_test _ =
-      printf pp r1 ;
+      pp_classes r1 ;
+      pp r1 ;
       [%expect
         {|
+          %y_6 = %x_5
+
           {sat= true;
            rep= [[%x_5 ↦ %y_6]];
            lkp= [];
            cls= [[%y_6 ↦ {%x_5, %y_6}]];
            use= []} |}]
 
-    let%expect_test _ = printf pp_classes r1 ; [%expect {| %y_6 = %x_5 |}]
+    let%test _ = not (Map.is_empty (classes r1))
     let%test _ = mem_eq x y r1
 
     let r2 = of_eqs [(x, y); (f x, y); (f y, z)]
 
     let%expect_test _ =
-      printf pp r2 ;
+      pp_classes r2 ;
+      pp r2 ;
       [%expect
         {|
+          %y_6 = ((i64)(i8) %x_5) = ((i64)(i8) %y_6) = %x_5 = %z_7
+
           {sat= true;
            rep= [[((i64)(i8) %x_5) ↦ %y_6];
                  [((i64)(i8) %y_6) ↦ %y_6];
                  [%x_5 ↦ %y_6];
                  [%z_7 ↦ %y_6]];
            lkp= [[((i64)(i8) %y_6) ↦ ((i64)(i8) %x_5)]];
-           cls= [[%y_6 ↦ {((i64)(i8) %x_5), ((i64)(i8) %y_6), %x_5, %y_6, %z_7}]];
+           cls= [[%y_6
-           use= [[%y_6 ↦ {((i64)(i8) %x_5)}]]} |}]
+                  ↦ {((i64)(i8) %x_5), ((i64)(i8) %y_6), %x_5, %y_6, %z_7}]];
+           use= [[%y_6 ↦ {((i64)(i8) %x_5)}];
+                 [(i64)(i8) ↦ {((i64)(i8) %x_5)}]]} |}]
+
+    let r2' = extend r2 (f z)
 
     let%expect_test _ =
-      printf pp_classes r2 ;
+      pp_classes r2' ;
+      pp r2' ;
       [%expect
-        {| %y_6 = ((i64)(i8) %x_5) = ((i64)(i8) %y_6) = %x_5 = %z_7 |}]
+        {|
+          %y_6 = ((i64)(i8) %x_5) = ((i64)(i8) %y_6) = ((i64)(i8) %z_7)
+          = %x_5 = %z_7
+
+          {sat= true;
+           rep= [[((i64)(i8) %x_5) ↦ %y_6];
+                 [((i64)(i8) %y_6) ↦ %y_6];
+                 [((i64)(i8) %z_7) ↦ %y_6];
+                 [%x_5 ↦ %y_6];
+                 [%z_7 ↦ %y_6]];
+           lkp= [[((i64)(i8) %y_6) ↦ ((i64)(i8) %x_5)]];
+           cls= [[%y_6
+                  ↦ {((i64)(i8) %x_5), ((i64)(i8) %y_6), ((i64)(i8) %z_7),
+                     %x_5, %y_6, %z_7}]];
+           use= [[%y_6 ↦ {((i64)(i8) %x_5)}];
+                 [(i64)(i8) ↦ {((i64)(i8) %x_5)}]]} |}]
 
     let%test _ = mem_eq x z r2
     let%test _ = mem_eq x y (or_ r1 r2)
@@ -115,7 +150,9 @@ let%test_module _ =
     let%test _ = not (mem_eq x z (or_ r1 r2))
     let%test _ = mem_eq x z (or_ f1 r2)
     let%test _ = mem_eq x z (or_ r2 f3)
-    let%test _ = mem_eq (f x) (f z) r2
+    let%test _ = mem_eq (f y) y r2
+    let%test _ = mem_eq (f x) (f z) r2'
+    let%test _ = not (mem_eq (f x) (f z) r2)
     let%test _ = mem_eq (g x y) (g z y) r2
 
     let%test _ =
@@ -137,28 +174,31 @@ let%test_module _ =
     let r3 = of_eqs [(g y z, w); (v, w); (g y w, t); (x, v); (x, u); (u, z)]
 
     let%expect_test _ =
-      printf pp r3 ;
+      pp_classes r3 ;
+      pp r3 ;
       [%expect
         {|
+      ∧ %w_4 = (%y_6 rem %w_4) = (%y_6 rem %z_7) = %t_1 = %u_2 = %v_3
+        = %x_5 = %z_7
+
       {sat= true;
-       rep= [[(%w_4 xor %y_6) ↦ %w_4];
+       rep= [[(%y_6 rem %w_4) ↦ %w_4];
-             [(%y_6 xor %z_7) ↦ %w_4];
+             [(%y_6 rem %z_7) ↦ %w_4];
+             [(rem %y_6) ↦ ];
              [%t_1 ↦ %w_4];
              [%u_2 ↦ %w_4];
              [%v_3 ↦ %w_4];
              [%x_5 ↦ %w_4];
              [%z_7 ↦ %w_4]];
-       lkp= [[(%w_4 xor %y_6) ↦ (%w_4 xor %y_6)];
+       lkp= [[(%y_6 rem %w_4) ↦ ]; [(%y_6 rem %z_7) ↦ ]; [(rem %y_6) ↦ ]];
-             [(%y_6 xor %z_7) ↦ (%y_6 xor %z_7)];
+       cls= [[(rem %y_6) ↦ {(rem %y_6)}];
-             [(xor %w_4) ↦ (xor %w_4)];
+             [%w_4
-             [(xor %y_6) ↦ (xor %y_6)]];
+              ↦ {(%y_6 rem %w_4), (%y_6 rem %z_7), %t_1, %u_2, %v_3,
-       cls= [[%w_4
+                 %w_4, %x_5, %z_7}]];
-              ↦ {(%w_4 xor %y_6), (%y_6 xor %z_7), %t_1, %u_2, %v_3, %w_4,
+       use= [[(rem %y_6) ↦ {(%y_6 rem %w_4), (%y_6 rem %z_7)}];
-                 %x_5, %z_7}]];
+             [%w_4 ↦ {(%y_6 rem %w_4)}];
-       use= [[(xor %w_4) ↦ {(%w_4 xor %y_6)}];
+             [%y_6 ↦ {(rem %y_6)}];
-             [(xor %y_6) ↦ {(%y_6 xor %z_7)}];
+             [rem ↦ {(rem %y_6)}]]} |}]
-             [%w_4 ↦ {(xor %w_4)}];
-             [%y_6 ↦ {(%w_4 xor %y_6), (xor %y_6)}]]} |}]
 
     let%test _ = mem_eq t z r3
     let%test _ = mem_eq x z r3
@@ -166,6 +206,21 @@ let%test_module _ =
 
     let r4 = of_eqs [(w + !2, x - !3); (x - !5, y + !7); (y, z - !4)]
 
+    let%expect_test _ =
+      pp_classes r4 ;
+      pp r4 ;
+      [%expect
+        {|
+      %y_6 = (%w_4 + -7) = (%x_5 + -12) = (%z_7 + -4)
+
+      {sat= true;
+       rep= [[%w_4 ↦ (%y_6 + 7)];
+             [%x_5 ↦ (%y_6 + 12)];
+             [%z_7 ↦ (%y_6 + 4)]];
+       lkp= [];
+       cls= [[%y_6 ↦ {(%w_4 + -7), (%x_5 + -12), (%z_7 + -4), %y_6}]];
+       use= []} |}]
+
     let%test _ = mem_eq x (w + !5) r4
     let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5))
 
@@ -176,16 +231,164 @@ let%test_module _ =
 
     let r6 = of_eqs [(x, !1); (!1, y)]
 
+    let%expect_test _ =
+      pp_classes r6 ;
+      pp r6 ;
+      [%expect
+        {|
+      1 = %x_5 = %y_6
+
+      {sat= true;
+       rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]];
+       lkp= [];
+       cls= [[1 ↦ {%x_5, %y_6, 1}]];
+       use= []} |}]
+
     let%test _ = mem_eq x y r6
 
     let r7 = of_eqs [(v, x); (w, z); (y, z)]
 
+    let%expect_test _ =
+      pp_classes r7 ;
+      pp r7 ;
+      pp (merge ~prefer:(fun e ~over:f -> Exp.compare e f) r7 x z) ;
+      pp (merge ~prefer:(fun e ~over:f -> Exp.compare f e) r7 x z) ;
+      [%expect
+        {|
+      %x_5 = %v_3
+      ∧ %z_7 = %w_4 = %y_6
+
+      {sat= true;
+       rep= [[%v_3 ↦ %x_5]; [%w_4 ↦ %z_7]; [%y_6 ↦ %z_7]];
+       lkp= [];
+       cls= [[%x_5 ↦ {%v_3, %x_5}]; [%z_7 ↦ {%w_4, %y_6, %z_7}]];
+       use= []}
+
+      {sat= true;
+       rep= [[%v_3 ↦ %z_7]; [%w_4 ↦ %z_7]; [%x_5 ↦ %z_7]; [%y_6 ↦ %z_7]];
+       lkp= [];
+       cls= [[%z_7 ↦ {%v_3, %w_4, %x_5, %y_6, %z_7}]];
+       use= []}
+
+      {sat= true;
+       rep= [[%v_3 ↦ %x_5]; [%w_4 ↦ %x_5]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]];
+       lkp= [];
+       cls= [[%x_5 ↦ {%v_3, %w_4, %x_5, %y_6, %z_7}]];
+       use= []} |}]
+
     let%test _ = normalize (merge r7 x z) w |> Exp.equal z
 
     let%test _ =
-      normalize (merge ~prefer:(fun e ~over:f -> Exp.compare f e) r7 x z) w
+      let prefer e ~over:f = Exp.compare e f in
-      |> Exp.equal x
+      prefer z ~over:x > 0
+
+    let%test _ =
+      let prefer e ~over:f = Exp.compare e f in
+      prefer z ~over:x > 0
+      (* so x should not be the rep *)
+      && normalize (merge ~prefer r7 x z) w |> Exp.equal z
+
+    let%test _ =
+      let prefer e ~over:f = Exp.compare f e in
+      prefer x ~over:z > 0
+      (* so z should not be the rep *)
+      && normalize (merge ~prefer r7 x z) w |> Exp.equal x
+
+    let%test _ =
+      mem_eq (g w x) (g w z)
+        (extend (of_eqs [(g w x, g y z); (x, z)]) (g w z))
+
+    let%test _ =
+      mem_eq (g w x) (g w z)
+        (extend (of_eqs [(g w x, g y w); (x, z)]) (g w z))
+
+    let r8 = of_eqs [(x + !42, (!3 * y) + (!13 * z)); (!13 * z, x)]
+
+    let%expect_test _ =
+      pp_classes r8 ;
+      pp r8 ;
+      [%expect
+        {|
+      (3 × %y_6 + 13 × %z_7) = (%x_5 + 42) = (13 × %z_7 + 42)
+
+      {sat= true;
+       rep= [[(3 × %y_6 + 13 × %z_7) ↦ ];
+             [(13 × %z_7) ↦ (3 × %y_6 + 13 × %z_7 + -42)];
+             [%x_5 ↦ (3 × %y_6 + 13 × %z_7 + -42)]];
+       lkp= [[(3 × %y_6 + 13 × %z_7) ↦ ]; [(13 × %z_7) ↦ ]];
+       cls= [[(3 × %y_6 + 13 × %z_7)
+              ↦ {(%x_5 + 42), (3 × %y_6 + 13 × %z_7), (13 × %z_7 + 42)}]];
+       use= [[%y_6 ↦ {(3 × %y_6 + 13 × %z_7)}];
+             [%z_7 ↦ {(13 × %z_7), (3 × %y_6 + 13 × %z_7)}];
+             [+ ↦ {(13 × %z_7), (3 × %y_6 + 13 × %z_7)}]]} |}]
+
+    (* (* incomplete *)
+     * let%test _ = mem_eq y !14 r8 *)
+
+    let r9 = of_eqs [(x, z - !16)]
+
+    let%expect_test _ =
+      pp_classes r9 ;
+      pp r9 ;
+      [%expect
+        {|
+       %z_7 = (%x_5 + 16)
+
+       {sat= true;
+        rep= [[%x_5 ↦ (%z_7 + -16)]];
+        lkp= [];
+        cls= [[%z_7 ↦ {(%x_5 + 16), %z_7}]];
+        use= []} |}]
 
-    let%test _ = mem_eq (g w x) (g w z) (of_eqs [(g w x, g y z); (x, z)])
+    let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
-    let%test _ = mem_eq (g w x) (g w z) (of_eqs [(g w x, g y w); (x, z)])
+
+    let r10 = of_eqs [(!16, z - x)]
+
+    let%expect_test _ =
+      pp_classes r10 ;
+      pp r10 ;
+      Format.printf "@.%a@." Exp.pp (z - (x + !8)) ;
+      Format.printf "@.%a@." Exp.pp (normalize r10 (z - (x + !8))) ;
+      Format.printf "@.%a@." Exp.pp (x + !8 - z) ;
+      Format.printf "@.%a@." Exp.pp (normalize r10 (x + !8 - z)) ;
+      [%expect
+        {|
+      16 = (-1 × %x_5 + %z_7)
+
+      {sat= true;
+       rep= [[(-1 × %x_5 + %z_7) ↦ 16]];
+       lkp= [[(-1 × %x_5 + %z_7) ↦ ]];
+       cls= [[16 ↦ {(-1 × %x_5 + %z_7), 16}]];
+       use= [[%x_5 ↦ {(-1 × %x_5 + %z_7)}];
+             [%z_7 ↦ {(-1 × %x_5 + %z_7)}];
+             [+ ↦ {(-1 × %x_5 + %z_7)}]]}
+
+      (-1 × %x_5 + %z_7 + -8)
+
+      8
+
+      (%x_5 + -1 × %z_7 + 8)
+
+      (%x_5 + -1 × %z_7 + 8) |}]
+
+    let%test _ = difference r10 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
+
+    (* (* incomplete *)
+     * let%test _ =
+     *   difference r10 (x + !8) z |> Poly.equal (Some (Z.of_int (-8))) *)
+
+    let r11 = of_eqs [(!16, z - x); (x + !8 - z, z - !16 + !8 - z)]
+
+    let%expect_test _ =
+      pp_classes r11 ;
+      [%expect
+        {|
+        -16 = (%x_5 + -1 × %z_7)
+        ∧ 16 = (-1 × %x_5 + %z_7) |}]
+
+    let r12 = of_eqs [(!16, z - x); (x + !8 - z, z + !16 + !8 - z)]
+
+    let%expect_test _ =
+      pp_classes r12 ;
+      [%expect {| 16 = (-1 × %x_5 + %z_7) = (%x_5 + -1 × %z_7) |}]
   end )