[sledge] Initial Shostak-style treatment of UIF+LIA

Summary:
This patch adds an embarrassingly inefficient implementation of a
decision procedure for equality in the theories of uninterpreted
functions and linear arithmetic. A Shostak-style approach, where a
single congruence closure structure is shared by all theories, is
used. This is mostly based on the corrected variant of Shostak's
algorithm from:

Harald Rueβ and Natarajan Shankar. 2001. Deconstructing Shostak. In
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer
Science (LICS '01).

Reviewed By: jvillard

Differential Revision: D14251655

fbshipit-source-id: 8a080145f

sledge/src/import/qset.ml

@@ -83,6 +83,7 @@ let count_and_remove m x =
   if Q.equal !found Q.zero then None else Some (!found, m)
 
 let min_elt = Map.min_elt
+let min_elt_exn = Map.min_elt_exn
 let fold m ~f ~init = Map.fold m ~f:(fun ~key ~data s -> f key data s) ~init
 
 let map m ~f =

sledge/src/import/qset.mli

@@ -103,5 +103,8 @@ val iter : ('a, _) t -> f:('a -> Q.t -> unit) -> unit
 val min_elt : ('a, _) t -> ('a * Q.t) option
 (** Minimum element. *)
 
+val min_elt_exn : ('a, _) t -> 'a * Q.t
+(** Minimum element. *)
+
 val to_list : ('a, _) t -> ('a * Q.t) list
 (** Convert to a list of elements in ascending order. *)

sledge/src/llair/exp.ml

@@ -362,6 +362,8 @@ let typ_of = function
       Some Typ.bool
   | _ -> None
 
+let typ = typ_of
+
 let type_check typ e =
   assert (Option.for_all ~f:(Typ.castable typ) (typ_of e))
 
@@ -1287,3 +1289,34 @@ let rec is_constant = function
   | Add {args} | Mul {args} ->
       Qset.for_all ~f:(fun arg _ -> is_constant arg) args
   | _ -> true
+
+let classify = function
+  | Add _ | Mul _ -> `Interpreted
+  | App _ -> `Uninterpreted
+  | _ -> `Atomic
+
+let solve e f =
+  [%Trace.call fun {pf} -> pf "%a@ %a" pp e pp f]
+  ;
+  ( match (typ e, typ f) with
+  | Some typ, _ | _, Some typ -> (
+    match sub typ e f with
+    | Add {args} ->
+        let c, q = Qset.min_elt_exn args in
+        let n = Sum.to_exp typ (Qset.remove args c) in
+        let d = rational (Q.neg q) typ in
+        let r = div n d in
+        Some (c, r)
+    | e_f ->
+        let z = integer Z.zero typ in
+        if is_constant e_f && not (equal e_f z) then None else Some (e_f, z)
+    )
+  | _ ->
+      let ord = compare e f in
+      if is_constant e && is_constant f && ord <> 0 then None
+      else if ord < 0 then Some (f, e)
+      else Some (e, f) )
+  |>
+  [%Trace.retn fun {pf} ->
+    function
+    | Some (e, f) -> pf "%a @<2>↦ %a" pp e pp f | None -> pf "false"]

sledge/src/llair/exp.mli

@@ -221,3 +221,6 @@ val is_true : t -> bool
 val is_false : t -> bool
 val is_simple : t -> bool
 val is_constant : t -> bool
+val typ : t -> Typ.t option
+val classify : t -> [> `Atomic | `Interpreted | `Uninterpreted]
+val solve : t -> t -> (t * t) option

sledge/src/symbheap/equality.ml

@@ -0,0 +1,276 @@
+(*
+ * 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.
+ *)
+
+(** Equality over uninterpreted functions and linear rational arithmetic *)
+
+type 'a exp_map = 'a Map.M(Exp).t [@@deriving compare, sexp]
+
+let empty_map = Map.empty (module Exp)
+
+type subst = Exp.t exp_map [@@deriving compare, sexp]
+
+(** see also [invariant] *)
+type t =
+  { sat: bool  (** [false] only if constraints are inconsistent *)
+  ; rep: subst
+        (** functional set of oriented equations: map [a] to [a'],
+            indicating that [a = a'] holds, and that [a'] is the
+            'rep(resentative)' of [a] *) }
+[@@deriving compare, sexp]
+
+(** Pretty-printing *)
+
+let pp fs {sat; rep} =
+  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 (k, v)
+    in
+    Format.fprintf fs "[@[<hv>%a@]]" (List.pp ";@ " pp_assoc) alist
+  in
+  let pp_exp_v fs (k, v) = if not (Exp.equal k v) then Exp.pp fs v in
+  Format.fprintf fs "@[{@[<hv>sat= %b;@ rep= %a@]}@]" sat
+    (pp_alist Exp.pp pp_exp_v)
+    (Map.to_alist rep)
+
+let pp_classes fs r =
+  let cls =
+    Map.fold r.rep ~init:empty_map ~f:(fun ~key ~data cls ->
+        if Exp.equal key data then cls
+        else Map.add_multi cls ~key:data ~data:key )
+  in
+  List.pp "@ @<2>∧ "
+    (fun fs (key, data) ->
+      Format.fprintf fs "@[%a@ = %a@]" Exp.pp key (List.pp "@ = " Exp.pp)
+        (List.sort ~compare:Exp.compare data) )
+    fs (Map.to_alist cls)
+
+let pp_diff fs (r, s) =
+  let pp_sdiff_map pp_elt_diff equal nam fs x y =
+    let sd = Sequence.to_list (Map.symmetric_diff ~data_equal:equal x y) in
+    if not (List.is_empty sd) then
+      Format.fprintf fs "%s= [@[<hv>%a@]];@ " nam
+        (List.pp ";@ " pp_elt_diff)
+        sd
+  in
+  let pp_sdiff_elt pp_key pp_val pp_sdiff_val fs = function
+    | k, `Left v ->
+        Format.fprintf fs "-- [@[%a@ @<2>↦ %a@]]" pp_key k pp_val v
+    | k, `Right v ->
+        Format.fprintf fs "++ [@[%a@ @<2>↦ %a@]]" pp_key k pp_val v
+    | k, `Unequal 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 Exp.pp pp_sdiff_exp) 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
+  Format.fprintf fs "@[{@[<hv>%t%t@]}@]" pp_sat pp_rep
+
+(** Invariant *)
+
+(** test membership in carrier *)
+let in_car r e = Map.mem r.rep e
+
+let invariant r =
+  Invariant.invariant [%here] r [%sexp_of: t]
+  @@ fun () ->
+  Map.iteri r.rep ~f:(fun ~key:a ~data:_ ->
+      (* no interpreted exps in carrier *)
+      assert (Poly.(Exp.classify a <> `Interpreted)) ;
+      (* carrier is closed under sub-expressions *)
+      Exp.iter a ~f:(fun b ->
+          assert (
+            in_car r b
+            || Trace.fail "@[subexp %a of %a not in carrier of@ %a@]" Exp.pp
+                 b Exp.pp a pp r ) ) )
+
+(** Core operations *)
+
+let true_ = {sat= true; rep= empty_map} |> check invariant
+
+(** apply a subst to an exp *)
+let apply s a = try Map.find_exn s a with Caml.Not_found -> a
+
+(** apply a subst to maximal non-interpreted subexps *)
+let rec norm s a =
+  match Exp.classify a with
+  | `Interpreted -> Exp.map ~f:(norm s) a
+  | _ -> apply s a
+
+(** exps are congruent if equal after normalizing subexps *)
+let congruent r a b =
+  Exp.equal (Exp.map ~f:(norm r.rep) a) (Exp.map ~f:(norm r.rep) b)
+
+(** [lookup r a] is [b'] if [a ~ b = b'] for some equation [b = b'] in rep *)
+let lookup r a =
+  With_return.with_return
+  @@ fun {return} ->
+  (* congruent specialized to assume [a] canonized and [b] non-interpreted *)
+  let semi_congruent r a b = Exp.equal a (Exp.map ~f:(apply r.rep) b) in
+  Map.iteri r.rep ~f:(fun ~key ~data ->
+      if semi_congruent r a key then return data ) ;
+  a
+
+(** rewrite an exp into canonical form using rep and, for uninterpreted
+    exps, congruence composed with rep *)
+let rec canon r a =
+  match Exp.classify a with
+  | `Interpreted -> Exp.map ~f:(canon r) a
+  | `Uninterpreted -> lookup r (Exp.map ~f:(canon r) a)
+  | `Atomic -> apply r.rep a
+
+(** add an exp to the carrier *)
+let rec extend a r =
+  match Exp.classify a with
+  | `Interpreted -> Exp.fold ~f:extend a ~init:r
+  | _ ->
+      Map.find_or_add r.rep a
+        ~if_found:(fun _ -> r)
+        ~default:a
+        ~if_added:(fun rep -> Exp.fold ~f:extend a ~init:{r with rep})
+
+let extend a r = extend a r |> check invariant
+
+let compose r a a' =
+  let s = Map.singleton (module Exp) a a' in
+  let rep = Map.map ~f:(norm s) r.rep in
+  let rep =
+    Map.update rep a ~f:(function
+      | None -> a'
+      | Some b when Exp.equal a' b -> b
+      | _ -> fail "domains intersect: %a" Exp.pp a () )
+  in
+  {r with rep} |> check invariant
+
+let merge a b r =
+  [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Exp.pp a Exp.pp b pp r]
+  ;
+  ( match Exp.solve a b with
+  | Some (c, c') -> compose r c c'
+  | None -> {r with sat= false} )
+  |>
+  [%Trace.retn fun {pf} r' ->
+    pf "%a" pp_diff (r, r') ;
+    invariant r']
+
+(** find an unproved equation between congruent exps *)
+let find_missing r =
+  With_return.with_return
+  @@ fun {return} ->
+  Map.iteri r.rep ~f:(fun ~key:a ~data:a' ->
+      Map.iteri r.rep ~f:(fun ~key:b ~data:b' ->
+          if
+            Exp.compare a b < 0
+            && (not (Exp.equal a' b'))
+            && congruent r a b
+          then return (Some (a', b')) ) ) ;
+  None
+
+let rec close r =
+  if not r.sat then r
+  else
+    match find_missing r with
+    | Some (a', b') -> close (merge a' b' r)
+    | None -> r
+
+let and_eq a b r =
+  if not r.sat then r
+  else
+    let a' = canon r a in
+    let b' = canon r b in
+    let r = extend a' r in
+    let r = extend b' r in
+    if Exp.equal a' b' then r else close (merge a' b' r)
+
+(** Exposed interface *)
+
+let is_true {sat; rep} =
+  sat && Map.for_alli rep ~f:(fun ~key:a ~data:a' -> Exp.equal a a')
+
+let is_false {sat} = not sat
+let entails_eq r d e = Exp.equal (canon r d) (canon r e)
+
+let entails r s =
+  Map.for_alli s.rep ~f:(fun ~key:e ~data:e' -> entails_eq r e e')
+
+let normalize = canon
+
+let difference r a b =
+  [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Exp.pp a Exp.pp b pp r]
+  ;
+  let a = canon r a in
+  let b = canon r b in
+  ( if Exp.equal a b then Some Z.zero
+  else
+    match (Exp.typ a, Exp.typ b) with
+    | Some typ, _ | _, Some typ -> (
+      match normalize r (Exp.sub typ a b) with
+      | Integer {data} -> Some data
+      | _ -> None )
+    | _ -> None )
+  |>
+  [%Trace.retn fun {pf} ->
+    function Some d -> pf "%a" Z.pp_print d | None -> ()]
+
+let and_ 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 -> and_eq e e' r)
+
+let or_ r s =
+  if not s.sat then r
+  else if not r.sat then s
+  else
+    let merge_mems rs r s =
+      Map.fold s.rep ~init:rs ~f:(fun ~key:e ~data:e' rs ->
+          if entails_eq r e e' then and_eq e e' rs else rs )
+    in
+    let rs = true_ in
+    let rs = merge_mems rs r s in
+    let rs = merge_mems rs s r in
+    rs
+
+(* assumes that f is injective and for any set of exps E, f[E] is disjoint
+   from E *)
+let map_exps ({sat= _; rep} as r) ~f =
+  [%Trace.call fun {pf} -> pf "%a" pp r]
+  ;
+  let map ~equal_key ~equal_data ~f_key ~f_data m =
+    Map.fold m ~init:m ~f:(fun ~key ~data m ->
+        let key' = f_key key in
+        let data' = f_data data in
+        if equal_key key' key then
+          if equal_data data' data then m else Map.set m ~key ~data:data'
+        else Map.remove m key |> Map.add_exn ~key:key' ~data:data' )
+  in
+  let rep' =
+    map rep ~equal_key:Exp.equal ~equal_data:Exp.equal ~f_key:f ~f_data:f
+  in
+  (if rep' == rep then r else {r with rep= rep'})
+  |>
+  [%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)
+
+let fold_exps r ~init ~f =
+  Map.fold r.rep ~f:(fun ~key ~data z -> f (f z data) key) ~init
+
+let fold_vars r ~init ~f =
+  fold_exps r ~init ~f:(fun init -> Exp.fold_vars ~f ~init)
+
+let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty

sledge/src/symbheap/equality.mli

@@ -0,0 +1,59 @@
+(*
+ * 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.
+ *)
+
+(** Constraints representing equivalence relations over uninterpreted
+    functions and linear rational arithmetic *)
+
+type t [@@deriving compare, sexp]
+
+val pp : t pp
+val pp_classes : t pp
+
+include Invariant.S with type t := t
+
+val true_ : t
+(** The diagonal relation, which only equates each exp with itself. *)
+
+val and_eq : Exp.t -> Exp.t -> t -> t
+(** Conjoin an equation to a relation. *)
+
+val and_ : t -> t -> t
+(** Conjunction. *)
+
+val or_ : t -> t -> t
+(** Disjunction. *)
+
+val rename : t -> Var.Subst.t -> t
+(** Apply a renaming substitution to the relation. *)
+
+val fv : t -> Var.Set.t
+(** The variables occurring in the exps of the relation. *)
+
+val is_true : t -> bool
+(** Test if the relation is diagonal. *)
+
+val is_false : t -> bool
+(** Test if the relation is empty / inconsistent. *)
+
+val entails_eq : t -> Exp.t -> Exp.t -> bool
+(** Test if an equation is entailed by a relation. *)
+
+val entails : t -> t -> bool
+(** Test if one relation entails another. *)
+
+val normalize : t -> Exp.t -> Exp.t
+(** Normalize an exp [e] to [e'] such that [e = e'] is implied by the
+    relation, where [e'] and its sub-exps are expressed in terms of the
+    relation's canonical representatives of each equivalence-modulo-offset
+    class. *)
+
+val difference : t -> Exp.t -> Exp.t -> Z.t option
+(** The difference as an offset. [difference r a b = Some k] if [r] implies
+    [a = b+k], or [None] if [a] and [b] are not equal up to an integer
+    offset. *)
+
+val fold_exps : t -> init:'a -> f:('a -> Exp.t -> 'a) -> 'a

sledge/src/symbheap/equality_test.ml

@@ -0,0 +1,330 @@
+(*
+ * 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.
+ *)
+
+let%test_module _ =
+  ( module struct
+    open Equality
+
+    (* 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 a b r)
+    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.rem
+    let wrt = Var.Set.empty
+    let t_, wrt = Var.fresh "t" ~wrt
+    let u_, wrt = Var.fresh "u" ~wrt
+    let v_, wrt = Var.fresh "v" ~wrt
+    let w_, wrt = Var.fresh "w" ~wrt
+    let x_, wrt = Var.fresh "x" ~wrt
+    let y_, wrt = Var.fresh "y" ~wrt
+    let z_, _ = Var.fresh "z" ~wrt
+    let t = Exp.var t_
+    let u = Exp.var u_
+    let v = Exp.var v_
+    let w = Exp.var w_
+    let x = Exp.var x_
+    let y = Exp.var y_
+    let z = Exp.var z_
+    let f1 = of_eqs [(!0, !1)]
+
+    let%test _ = is_false f1
+
+    let%expect_test _ =
+      pp f1 ; [%expect {| {sat= false; rep= [[0 ↦ ]; [1 ↦ ]]} |}]
+
+    let%test _ = is_false (and_eq !1 !1 f1)
+
+    let f2 = of_eqs [(x, x + !1)]
+
+    let%test _ = is_false f2
+
+    let%expect_test _ =
+      pp f2 ; [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [1 ↦ ]]} |}]
+
+    let f3 = of_eqs [(x + !0, x + !1)]
+
+    let%test _ = is_false f3
+
+    let%expect_test _ =
+      pp f3 ; [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [1 ↦ ]]} |}]
+
+    let f4 = of_eqs [(x, y); (x + !0, y + !1)]
+
+    let%test _ = is_false f4
+
+    let%expect_test _ =
+      pp f4 ;
+      [%expect
+        {| {sat= false; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [1 ↦ ]]} |}]
+
+    let t1 = of_eqs [(!1, !1)]
+
+    let%test _ = is_true t1
+
+    let t2 = of_eqs [(x, x)]
+
+    let%test _ = is_true t2
+    let%test _ = is_false (and_ f3 t2)
+    let%test _ = is_false (and_ t2 f3)
+
+    let r0 = true_
+
+    let%expect_test _ = pp r0 ; [%expect {| {sat= true; rep= []} |}]
+    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%expect_test _ =
+      pp_classes r1 ;
+      pp r1 ;
+      [%expect
+        {|
+          %x_5 = %y_6
+
+          {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]} |}]
+
+    let%test _ = entails_eq r1 x y
+
+    let r2 = of_eqs [(x, y); (f x, y); (f y, z)]
+
+    let%expect_test _ =
+      pp_classes r2 ;
+      pp r2 ;
+      [%expect
+        {|
+          %x_5 = ((i64)(i8) %x_5) = %y_6 = %z_7
+
+          {sat= true;
+           rep= [[((i64)(i8) %x_5) ↦ %x_5];
+                 [%x_5 ↦ ];
+                 [%y_6 ↦ %x_5];
+                 [%z_7 ↦ %x_5];
+                 [(i64)(i8) ↦ ]]} |}]
+
+    let%test _ = entails_eq r2 x z
+    let%test _ = entails_eq (or_ r1 r2) x y
+    let%test _ = not (entails_eq (or_ r1 r2) x z)
+    let%test _ = entails_eq (or_ f1 r2) x z
+    let%test _ = entails_eq (or_ r2 f3) x z
+    let%test _ = entails_eq r2 (f y) y
+    let%test _ = entails_eq r2 (f x) (f z)
+    let%test _ = entails_eq r2 (g x y) (g z y)
+
+    let%test _ =
+      entails_eq
+        (rename r2 Var.Subst.(extend empty ~replace:x_ ~with_:w_))
+        w z
+
+    let%test _ =
+      r2 == rename r2 Var.Subst.(extend empty ~replace:w_ ~with_:x_)
+
+    let%test _ =
+      entails_eq
+        (rename r2
+           Var.Subst.(
+             empty
+             |> extend ~replace:x_ ~with_:v_
+             |> extend ~replace:y_ ~with_:w_))
+        v w
+
+    let%test _ = difference (or_ r1 r2) x z |> Poly.equal None
+
+    let r3 = of_eqs [(g y z, w); (v, w); (g y w, t); (x, v); (x, u); (u, z)]
+
+    let%expect_test _ =
+      pp_classes r3 ;
+      pp r3 ;
+      [%expect
+        {|
+      (%y_6 rem (%y_6 rem %z_7)) = (%y_6 rem %z_7) = %t_1 = %u_2 = %v_3
+      = %w_4 = %x_5 = %z_7
+
+      {sat= true;
+       rep= [[(%y_6 rem (%y_6 rem %z_7)) ↦ ];
+             [(%y_6 rem %z_7) ↦ (%y_6 rem (%y_6 rem %z_7))];
+             [(rem %y_6) ↦ ];
+             [%t_1 ↦ (%y_6 rem (%y_6 rem %z_7))];
+             [%u_2 ↦ (%y_6 rem (%y_6 rem %z_7))];
+             [%v_3 ↦ (%y_6 rem (%y_6 rem %z_7))];
+             [%w_4 ↦ (%y_6 rem (%y_6 rem %z_7))];
+             [%x_5 ↦ (%y_6 rem (%y_6 rem %z_7))];
+             [%y_6 ↦ ];
+             [%z_7 ↦ (%y_6 rem (%y_6 rem %z_7))];
+             [rem ↦ ]]} |}]
+
+    let%test _ = entails_eq r3 t z
+    let%test _ = entails_eq r3 x z
+    let%test _ = entails_eq (and_ r2 r3) x z
+
+    let r4 = of_eqs [(w + !2, x - !3); (x - !5, y + !7); (y, z - !4)]
+
+    let%expect_test _ =
+      pp_classes r4 ;
+      pp r4 ;
+      [%expect
+        {|
+      (%z_7 + -4) = %y_6 ∧ (%z_7 + 3) = %w_4
+      ∧ (%z_7 + 8) = %x_5
+
+      {sat= true;
+       rep= [[%w_4 ↦ (%z_7 + 3)];
+             [%x_5 ↦ (%z_7 + 8)];
+             [%y_6 ↦ (%z_7 + -4)];
+             [%z_7 ↦ ];
+             [1 ↦ ]]} |}]
+
+    let%test _ = entails_eq r4 x (w + !5)
+    let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5))
+
+    let r5 = of_eqs [(x, y); (g w x, y); (g w y, f z)]
+
+    let%test _ =
+      Set.equal (fv r5) (Set.of_list (module Var) [w_; x_; y_; z_])
+
+    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]; [1 ↦ ]]} |}]
+
+    let%test _ = entails_eq r6 x y
+
+    let r7 = of_eqs [(v, x); (w, z); (y, z)]
+
+    let%expect_test _ =
+      pp_classes r7 ;
+      pp r7 ;
+      pp (and_eq x z r7) ;
+      pp_classes (and_eq x z r7) ;
+      [%expect
+        {|
+      %v_3 = %x_5
+      ∧ %w_4 = %y_6 = %z_7
+
+      {sat= true;
+       rep= [[%v_3 ↦ ];
+             [%w_4 ↦ ];
+             [%x_5 ↦ %v_3];
+             [%y_6 ↦ %w_4];
+             [%z_7 ↦ %w_4]]}
+
+      {sat= true;
+       rep= [[%v_3 ↦ ];
+             [%w_4 ↦ %v_3];
+             [%x_5 ↦ %v_3];
+             [%y_6 ↦ %v_3];
+             [%z_7 ↦ %v_3]]}
+
+      %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}]
+
+    let r7' = and_eq x z r7
+
+    let%expect_test _ =
+      pp_classes r7' ;
+      pp r7' ;
+      [%expect
+        {|
+      %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]]} |}]
+
+    let%test _ = normalize r7' w |> Exp.equal v
+
+    let%test _ =
+      entails_eq (of_eqs [(g w x, g y z); (x, z)]) (g w x) (g w z)
+
+    let%test _ =
+      entails_eq (of_eqs [(g w x, g y w); (x, z)]) (g w x) (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
+        {|
+      (13 × %z_7) = %x_5
+      ∧ 14 = %y_6
+
+      {sat= true;
+       rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]; [%z_7 ↦ ]; [1 ↦ ]]} |}]
+
+    let%test _ = entails_eq r8 y !14
+
+    let r9 = of_eqs [(x, z - !16)]
+
+    let%expect_test _ =
+      pp_classes r9 ;
+      pp r9 ;
+      [%expect
+        {|
+       (%z_7 + -16) = %x_5
+
+       {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [1 ↦ ]]} |}]
+
+    let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
+
+    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
+        {|
+      (%z_7 + -16) = %x_5
+
+      {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [16 ↦ ]]}
+
+      (-1 × %x_5 + %z_7 + -8)
+
+      8
+
+      (%x_5 + -1 × %z_7 + 8)
+
+      -8 |}]
+
+    let%test _ = difference r10 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
+
+    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 {|
+        (%z_7 + -16) = %x_5 |}]
+
+    let r12 = of_eqs [(!16, z - x); (x + !8 - z, z + !16 + !8 - z)]
+
+    let%expect_test _ = pp_classes r12 ; [%expect {| (%z_7 + -16) = %x_5 |}]
+  end )

sledge/src/symbheap/sh.ml

@@ -15,7 +15,7 @@ type seg = {loc: Exp.t; bas: Exp.t; len: Exp.t; siz: Exp.t; arr: Exp.t}
 type starjunction =
   { us: Var.Set.t
   ; xs: Var.Set.t
-  ; cong: Congruence.t
+  ; cong: Equality.t
   ; pure: Exp.t list
   ; heap: seg list
   ; djns: disjunction list }
@@ -45,12 +45,12 @@ let rec pp_ vs fs {us; xs; cong; pure; heap; djns} =
   if not (Set.is_empty xs) then
     Format.fprintf fs "@<2>∃ @[%a@] .@ ∃ @[%a@] .@ " Var.Set.pp
       (Set.inter xs vs) Var.Set.pp (Set.diff xs vs) ;
-  let first = Map.is_empty (Congruence.classes cong) in
+  let first = Equality.is_true cong in
   if not first then Format.fprintf fs "  " ;
-  Congruence.pp_classes fs cong ;
+  Equality.pp_classes fs cong ;
   let pure_exps =
     List.filter_map pure ~f:(fun e ->
-        let e' = Congruence.normalize cong e in
+        let e' = Equality.normalize cong e in
         if Exp.is_true e' then None else Some e' )
   in
   List.pp
@@ -64,7 +64,7 @@ let rec pp_ vs fs {us; xs; cong; pure; heap; djns} =
       ~pre:(if first then "  " else "@ @<2>∧ ")
       "@ * " pp_seg fs
       (List.sort
-         (List.map ~f:(map_seg ~f:(Congruence.normalize cong)) heap)
+         (List.map ~f:(map_seg ~f:(Equality.normalize cong)) heap)
          ~compare:(fun s1 s2 ->
            let b_o = function
              | Exp.App {op= App {op= Add _; arg}; arg= Integer {data; _}} ->
@@ -100,7 +100,7 @@ let fold_vars_seg seg ~init ~f =
 let fv_seg seg = fold_vars_seg seg ~f:Set.add ~init:Var.Set.empty
 
 let fold_exps fold_exps {us= _; xs= _; cong; pure; heap; djns} ~init ~f =
-  Congruence.fold_exps ~init cong ~f
+  Equality.fold_exps ~init cong ~f
   |> fun init ->
   List.fold ~init pure ~f:(fun init -> Exp.fold_exps ~f ~init)
   |> fun init ->
@@ -137,13 +137,13 @@ let rec invariant q =
       Set.is_subset (fv q) ~of_:us
       || Trace.fail "unbound but free: %a" Var.Set.pp (Set.diff (fv q) us)
     ) ;
-    Congruence.invariant cong ;
+    Equality.invariant cong ;
     ( match djns with
     | [[]] ->
-        assert (Congruence.is_true cong) ;
+        assert (Equality.is_true cong) ;
         assert (List.is_empty pure) ;
         assert (List.is_empty heap)
-    | _ -> assert (not (Congruence.is_false cong)) ) ;
+    | _ -> assert (not (Equality.is_false cong)) ) ;
     List.iter pure ~f:invariant_pure ;
     List.iter heap ~f:invariant_seg ;
     List.iter djns ~f:(fun djn ->
@@ -171,7 +171,7 @@ let rename_seg sub ({loc; bas; len; siz; arr} as h) =
 (** primitive application of a substitution, ignores us and xs, may violate
     invariant *)
 let rec apply_subst sub ({us= _; xs= _; cong; pure; heap; djns} as q) =
-  let cong = Congruence.rename cong sub in
+  let cong = Equality.rename cong sub in
   let pure =
     List.map_preserving_phys_equal pure ~f:(fun b -> Exp.rename b sub)
   in
@@ -251,7 +251,7 @@ let exists xs q =
 let emp =
   { us= Var.Set.empty
   ; xs= Var.Set.empty
-  ; cong= Congruence.true_
+  ; cong= Equality.true_
   ; pure= []
   ; heap= []
   ; djns= [] }
@@ -260,11 +260,11 @@ let emp =
 let false_ us = {emp with us; djns= [[]]} |> check invariant
 
 let and_cong cong q =
-  [%Trace.call fun {pf} -> pf "%a@ %a" Congruence.pp cong pp q]
+  [%Trace.call fun {pf} -> pf "%a@ %a" Equality.pp cong pp q]
   ;
-  let q = extend_us (Congruence.fv cong) q in
+  let q = extend_us (Equality.fv cong) q in
-  let cong = Congruence.and_ q.cong cong in
+  let cong = Equality.and_ q.cong cong in
-  (if Congruence.is_false cong then false_ q.us else {q with cong})
+  (if Equality.is_false cong then false_ q.us else {q with cong})
   |>
   [%Trace.retn fun {pf} q -> pf "%a" pp q ; invariant q]
 
@@ -275,11 +275,11 @@ let star q1 q2 =
   | {djns= [[]]; _}, _ | _, {djns= [[]]; _} ->
       false_ (Set.union q1.us q2.us)
   | {us= _; xs= _; cong; pure= []; heap= []; djns= []}, _
-    when Congruence.is_true cong ->
+    when Equality.is_true cong ->
       let us = Set.union q1.us q2.us in
       if us == q2.us then q2 else {q2 with us}
   | _, {us= _; xs= _; cong; pure= []; heap= []; djns= []}
-    when Congruence.is_true cong ->
+    when Equality.is_true cong ->
       let us = Set.union q1.us q2.us in
       if us == q1.us then q1 else {q1 with us}
   | _ ->
@@ -289,8 +289,8 @@ let star q1 q2 =
       let {us= us1; xs= xs1; cong= c1; pure= p1; heap= h1; djns= d1} = q1 in
       let {us= us2; xs= xs2; cong= c2; pure= p2; heap= h2; djns= d2} = q2 in
       assert (Set.equal us (Set.union us1 us2)) ;
-      let cong = Congruence.and_ c1 c2 in
+      let cong = Equality.and_ c1 c2 in
-      if Congruence.is_false cong then false_ us
+      if Equality.is_false cong then false_ us
       else
         { us
         ; xs= Set.union xs1 xs2
@@ -320,7 +320,7 @@ let or_ q1 q2 =
   | _ ->
       { us= Set.union q1.us q2.us
       ; xs= Var.Set.empty
-      ; cong= Congruence.true_
+      ; cong= Equality.true_
       ; pure= []
       ; heap= []
       ; djns= [[q1; q2]] } )
@@ -345,8 +345,8 @@ let rec pure (e : Exp.t) =
         (star (pure cnd) (pure thn))
         (star (pure (Exp.not_ Typ.bool cnd)) (pure els))
   | App {op= App {op= Eq; arg= e1}; arg= e2} ->
-      let cong = Congruence.(and_eq true_ e1 e2) in
+      let cong = Equality.(and_eq e1 e2 true_) in
-      if Congruence.is_false cong then false_ us
+      if Equality.is_false cong then false_ us
       else {emp with us; cong; pure= [e]}
   | _ -> {emp with us; pure= [e]} )
   |>
@@ -371,8 +371,7 @@ let is_emp = function
 let is_false = function
   | {djns= [[]]; _} -> true
   | {cong; pure; _} ->
-      List.exists pure ~f:(fun b ->
+      List.exists pure ~f:(fun b -> Exp.is_false (Equality.normalize cong b))
-          Exp.is_false (Congruence.normalize cong b) )
 
 let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) =
   let heap = emp.heap in

sledge/src/symbheap/sh.mli

@@ -16,7 +16,7 @@ type seg = {loc: Exp.t; bas: Exp.t; len: Exp.t; siz: Exp.t; arr: Exp.t}
 type starjunction = private
   { us: Var.Set.t  (** vocabulary / variable context of formula *)
   ; xs: Var.Set.t  (** existentially-bound variables *)
-  ; cong: Congruence.t  (** congruence induced by rest of formula *)
+  ; cong: Equality.t  (** congruence induced by rest of formula *)
   ; pure: Exp.t list  (** conjunction of pure boolean constraints *)
   ; heap: seg list  (** star-conjunction of segment atomic formulas *)
   ; djns: disjunction list  (** star-conjunction of disjunctions *) }
@@ -56,7 +56,7 @@ val pure : Exp.t -> t
 val and_ : Exp.t -> t -> t
 (** Conjoin a boolean constraint to a formula. *)
 
-val and_cong : Congruence.t -> t -> t
+val and_cong : Equality.t -> t -> t
 (** Conjoin constraints of a congruence to a formula, extending to a common
     vocabulary, and avoiding capturing existentials. *)
 

sledge/src/symbheap/solver.ml

@@ -61,7 +61,7 @@ let single_existential_occurrence xs exp =
   with Multiple_existential_occurrences -> Many
 
 let excise_exp ({us; min; xs} as goal) pure exp =
-  let exp' = Congruence.normalize min.cong exp in
+  let exp' = Equality.normalize min.cong exp in
   if Exp.is_true exp' then Some ({goal with pgs= true}, pure)
   else
     match single_existential_occurrence xs exp' with
@@ -496,19 +496,19 @@ let excise_seg ({sub} as goal) msg ssg =
   [%Trace.info "@[<2>excise_seg@ %a@  |-  %a@]" Sh.pp_seg msg Sh.pp_seg ssg] ;
   let {Sh.loc= k; siz= o} = msg in
   let {Sh.loc= l; siz= n} = ssg in
-  Congruence.difference sub.cong k l
+  Equality.difference sub.cong k l
   >>= fun k_l ->
   match[@warning "-p"] Z.sign k_l with
   (* k-l < 0 so k < l *)
   | -1 -> (
       let ko = Exp.add Typ.ptr k o in
       let ln = Exp.add Typ.ptr l n in
-      Congruence.difference sub.cong ko ln
+      Equality.difference sub.cong ko ln
       >>= fun ko_ln ->
       match[@warning "-p"] Z.sign ko_ln with
       (* k+o-(l+n) < 0 so k+o < l+n *)
       | -1 -> (
-          Congruence.difference sub.cong l ko
+          Equality.difference sub.cong l ko
           >>= fun l_ko ->
           match[@warning "-p"] Z.sign l_ko with
           (* l-(k+o) < 0     [k;   o)
@@ -526,7 +526,7 @@ let excise_seg ({sub} as goal) msg ssg =
       | 1 -> Some (excise_seg_sub_infix goal msg ssg (Z.neg k_l) ko_ln) )
   (* k-l = 0 so k = l *)
   | 0 -> (
-    match Congruence.difference sub.cong o n with
+    match Equality.difference sub.cong o n with
     | None -> Some {goal with sub= Sh.and_ (Exp.eq o n) goal.sub}
     | Some o_n -> (
       match[@warning "-p"] Z.sign o_n with
@@ -543,7 +543,7 @@ let excise_seg ({sub} as goal) msg ssg =
   | 1 -> (
       let ko = Exp.add Typ.ptr k o in
       let ln = Exp.add Typ.ptr l n in
-      Congruence.difference sub.cong ko ln
+      Equality.difference sub.cong ko ln
       >>= fun ko_ln ->
       match[@warning "-p"] Z.sign ko_ln with
       (* k+o-(l+n) < 0        [k; o)
@@ -554,7 +554,7 @@ let excise_seg ({sub} as goal) msg ssg =
       | 0 -> Some (excise_seg_min_suffix goal msg ssg k_l)
       (* k+o-(l+n) > 0 so k+o > l+n *)
       | 1 -> (
-          Congruence.difference sub.cong k ln
+          Equality.difference sub.cong k ln
           >>= fun k_ln ->
           match[@warning "-p"] Z.sign k_ln with
           (* k-(l+n) < 0        [k;  o)