pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge] Add congruence closure with integer offsets

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D9846748

fbshipit-source-id: 575c6ee15
master
Josh Berdine 6 years ago committed by Facebook Github Bot
parent f7a9a0c323
commit a32890a1e3
3 changed files with 705 additions and 0 deletions
Show Stats Download Patch File Download Diff File

455
sledge/src/symbheap/congruence.ml
Unescape View File

@ -0,0 +1,455 @@
(*
* 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.
*)
(** Congruence closure with integer offsets *)
(* For background, see:
Robert Nieuwenhuis, Albert Oliveras: Fast congruence closure and
extensions. Inf. Comput. 205(4): 557-580 (2007)
and, for a more detailed correctness proof of the case without integer
offsets, see section 5 of:
Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine: Structuring the
verification of heap-manipulating programs. POPL 2010: 261-274 *)
(** set of exps representing congruence classes *)
module Cls = struct
type t = Exp.t list [@@deriving compare, sexp]
let pp fs cls =
Format.fprintf fs "@[<hov 1>{@[%a@]}@]" (List.pp ",@ " Exp.pp) cls
let singleton e = [e]
let add cls exp = exp :: cls
let remove_exn = List.remove_exn
let union = List.rev_append
let fold_map = List.fold_map
let is_empty = List.is_empty
let length = List.length
let mem = List.mem ~equal:Exp.equal
end
(** set of exps representing "use lists" encoding super-expression relation *)
module Use = struct
type t = Exp.t list [@@deriving compare, sexp]
let pp fs use =
Format.fprintf fs "@[<hov 1>{@[%a@]}@]" (List.pp ",@ " Exp.pp) use
let empty = []
let singleton exp = [exp]
let add use exp = exp :: use
let union = List.rev_append
let fold = List.fold
let is_empty = List.is_empty
end
type 'a exp_map = 'a Map.M(Exp).t [@@deriving compare, sexp]
let empty_map = Map.empty (module Exp)
type t =
{ sat: bool (** [false] if constraints are inconsistent *)
; rep: Exp.t exp_map
(** map [a] to [a'+k], indicating that [a=a'+k] holds, and that [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
[f(a+j)+k], an (offsetted) app(lication expression) in the
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)}] *)
; use: Use.t exp_map
(** super-expression relation for representatives: map each
representative [a'] of [a] to the application expressions in the
relation where [a] (possibly + an offset) appears as an
immediate sub-expression *)
; pnd: (Exp.t * Exp.t) list
(** equations to be added to the relation, to enable delaying adding
equations discovered while invariants are temporarily broken *)
}
[@@deriving compare, sexp]
(** The expressions in the range of [lkp] and [use], as well as those in
[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 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
in
Format.fprintf fs "[@[<hv>%a@]]" (List.pp ";@ " pp_assoc) alist
in
let pp_pnd fs pend =
let pp_eq fs (e, f) =
Format.fprintf fs "@[%a = %a@]" Exp.pp e Exp.pp f
in
if not (List.is_empty pend) then
Format.fprintf fs ";@ pend= @[%a@];" (List.pp ";@ " pp_eq) pend
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)
(Map.to_alist lkp) (pp_alist Exp.pp Cls.pp) (Map.to_alist cls)
(pp_alist Exp.pp Use.pp) (Map.to_alist use) pp_pnd pnd
let pp_classes fs {cls} =
List.pp "@ @<2>∧ "
(fun fs (key, data) ->
let es = Cls.remove_exn ~equal:Exp.equal data key in
if not (Cls.is_empty es) then
Format.fprintf fs "@[%a@ = %a@]" Exp.pp key (List.pp "@ = " Exp.pp)
es )
fs (Map.to_alist cls)
let invariant r =
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 *)
let map_sum e ~f =
match e with
| Exp.App {op= App {op= Add; arg= a}; arg= Integer _ as i} ->
let a' = f a in
if a' == a then e else Exp.add a' i
| a -> f a
let fold_sum e ~init ~f =
match e with
| Exp.App {op= App {op= Add; arg= a}; arg= Integer _} -> f init a
| a -> f init a
let base_of = function
| Exp.App {op= App {op= Add; arg= a}; arg= Integer _} -> a
| a -> a
(** solve a+i = b for a, yielding a = b-i *)
let solve_for_base ai b =
match ai with
| Exp.App {op= App {op= Add; arg= a}; arg= Integer _ as i} ->
(a, Exp.sub b i)
| _ -> (ai, b)
(** [norm r a+i] = [a'+k] where [r] implies [a+i=a'+k] and [a'] is a rep *)
let norm r e =
map_sum e ~f:(fun a -> try Map.find_exn r.rep a with Caml.Not_found -> a)
(* Core closure operations *)
type prefer = Exp.t -> over:Exp.t -> int
let true_ =
{ sat= true
; rep= empty_map
; lkp= empty_map
; cls= empty_map
; use= empty_map
; pnd= [] }
let false_ = {true_ with sat= false}
(** 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
is updated to map each element of [b]'s [cls] (including [b]) to [a].
This also adjusts the offsets in [b]'s [cls] and merges it into [a]'s.
Likewise [b]'s [use] exps are merged into [a]'s. Finally, [b]'s [use]
exps are used to traverse one step up the expression dag, looking for
new equations involving a super-expression of [b], whose rep changed. *)
let add_directed_equation r ~exp:bj ~rep:ai =
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_cls, cls =
try Map.find_and_remove_exn r.cls b with Caml.Not_found ->
(Cls.singleton b, r.cls)
in
let b_use, use =
try Map.find_and_remove_exn r.use b with Caml.Not_found ->
(Use.empty, r.use)
in
let rep, a_cls_delta =
Cls.fold_map b_cls ~init:r.rep ~f:(fun rep 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
if Exp.is_false (Exp.eq c ai_j_k) then raise Unsat ;
let rep = Map.set rep ~key:c ~data:ai_j_k in
(* a+i-j = c+k so a = c+k+j-i *)
let _, ckj_i = solve_for_base ai_j ck in
(rep, ckj_i) )
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 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
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
(since u' found in r.lkp) that is equal to v, so will be in
use of u's subexps, and u = v is added to pnd so propagate
will combine them later *)
(r, a_use_delta) )
~default:u
~if_added:(fun lkp ->
let r = {r with lkp} in
let a_use_delta = Use.add a_use_delta u in
(r, a_use_delta) ) )
in
let use =
if Use.is_empty a_use_delta then use
else
Map.update use a ~f:(function
| Some a_use -> Use.union a_use_delta a_use
| None -> a_use_delta )
in
let r = {r with use} in
r |> check invariant
(** Close the relation with the pending equations. *)
let rec propagate_ ?prefer r =
match r.pnd with
| [] -> r
| (d, e) :: pnd ->
let d' = norm r d in
let e' = norm r e in
let r = {r with pnd} in
let r =
if Exp.equal (base_of d') (base_of e') then
if Exp.equal d' e' then r else {r with sat= false; pnd= []}
else
let prefer_e_over_d =
match (Exp.is_constant d, Exp.is_constant e) with
| true, false -> -1
| false, true -> 1
| _ -> (
match prefer with
| 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
let propagate ?prefer r =
[%Trace.call fun {pf} -> pf "%a" pp r]
;
(try propagate_ ?prefer r with Unsat -> false_)
|>
[%Trace.retn fun {pf} -> pf "%a" pp]
let merge ?prefer r d e =
if not r.sat then r
else
let r, a = extend r d in
let r =
if Exp.equal d e then r
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 =
[%Trace.call fun {pf} -> pf "%a" Exp.pp e]
;
map_sum e ~f:(function
| App _ as fa -> (
let fa' = Exp.map ~f:(normalize_ r) fa in
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 =
[%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 and_eq = merge
let and_ ?prefer r s =
if not r.sat then r
else if not s.sat then s
else
Map.fold s.rep ~init:r ~f:(fun ~key:e ~data:e' r -> merge ?prefer r e e')
let or_ ?prefer 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 mem_eq r e e' then merge ?prefer rs e e' 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; lkp; cls; use; pnd} as r) ~f =
[%Trace.call fun {pf} -> pf "%a@." pp r]
;
assert (List.is_empty pnd) ;
let map ~equal_data ~f_data m =
Map.fold m ~init:m ~f:(fun ~key ~data m ->
let key' = f key in
let data' = f_data data in
if Exp.equal 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:(if data' == data then data else data') )
in
let exp_map = map ~equal_data:Exp.equal ~f_data:f in
let exp_list_map =
map ~equal_data:[%compare.equal: Exp.t list]
~f_data:(List.map_preserving_phys_equal ~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]
let rename r sub = map_exps r ~f:(fun e -> Exp.rename e sub)
let fold_exps r ~init ~f =
Map.fold r.lkp ~f:(fun ~key:_ ~data z -> f z data) ~init
|> fun init ->
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
let is_true {sat; rep; pnd; _} =
sat && Map.is_empty rep && List.is_empty pnd
let is_false {sat} = not sat
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, b = extend r b in
let r = propagate r in
let ci = normalize r a in
let dj = normalize r b in
(* a - b = (c+i) - (d+j) *)
( match solve_for_base dj ci with
(* d = (c+i)-j = c+(i-j) & c = d *)
| d, App {op= App {op= Add; arg= c}; arg= Integer {data= i_j}}
when Exp.equal d c ->
(* 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
| Some d -> pf "%a" Z.pp_print d
| None -> pf "c+i: %a@ d+j: %a" Exp.pp ci Exp.pp dj]
let%test_module _ =
( module struct
let printf pp = Format.printf "@.%a@." pp
let ( ! ) i = Exp.integer (Z.of_int i)
let%expect_test _ =
printf pp {true_ with pnd= [(!0, !1)]} ;
[%expect
{| {sat= true; rep= []; lkp= []; cls= []; use= []; pend= 0 = 1;} |}]
end )

66
sledge/src/symbheap/congruence.mli
Unescape View File

@ -0,0 +1,66 @@
(*
* 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 congruence relations *)
type t [@@deriving compare, sexp]
val pp : t pp
val pp_classes : t pp
include Invariant.S with type t := t
(** If [prefer a ~over:b] is positive, then [b] will not be used as the
representative of a class containing [a] and [b]. Similarly, if [prefer
a ~over:b] is negative, then [a] will not be used as the representative
of a class containing [a] and [b]. Otherwise the choice of
representative is unspecified, and made to be most efficient. *)
type prefer = Exp.t -> over:Exp.t -> int
val true_ : t
(** The diagonal relation, which only equates each exp with itself. *)
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
containing [a] and [b]. *)
val and_eq : ?prefer:prefer -> t -> Exp.t -> Exp.t -> t
val and_ : ?prefer:prefer -> t -> t -> t
(** Conjunction. *)
val or_ : ?prefer:prefer -> 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 classes : t -> (Exp.t, Exp.t list, Exp.comparator_witness) Map.t
val entails : t -> t -> bool
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

184
sledge/src/symbheap/congruence_test.ml
Unescape View File

@ -0,0 +1,184 @@
(*
* 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 Congruence
let printf pp = Format.printf "@.%a@." pp
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 i8 = Typ.integer ~bits:8
let i64 = Typ.integer ~bits:64
let ( ! ) i = Exp.integer (Z.of_int i)
let ( + ) = Exp.add
let ( - ) = Exp.sub
let f = Exp.convert ~dst:i64 ~src:i8
let g = Exp.xor
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%test _ = Map.is_empty (classes f1)
let%test _ = is_false (merge f1 !1 !1)
let f2 = of_eqs [(x, x + !1)]
let%test _ = is_false f2
let f3 = of_eqs [(x + !0, x + !1)]
let%test _ = is_false f3
let f4 = of_eqs [(x, y); (x + !0, y + !1)]
let%test _ = is_false f4
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 _ =
printf pp r0 ;
[%expect {| {sat= true; rep= []; lkp= []; cls= []; use= []} |}]
let%expect_test _ = printf 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 ;
[%expect
{|
{sat= true;
rep= [[%x_5 ↦ %y_6]];
lkp= [];
cls= [[%y_6 ↦ {%y_6, %x_5}]];
use= []} |}]
let%expect_test _ = printf pp_classes r1 ; [%expect {| %y_6 = %x_5 |}]
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 ;
[%expect
{|
{sat= true;
rep= [[%x_5 ↦ %y_6]; [%z_7 ↦ %y_6]];
lkp= [];
cls= [[%y_6 ↦ {%z_7, %y_6, %x_5}]];
use= []} |}]
let%expect_test _ =
printf pp_classes r2 ; [%expect {| %y_6 = %z_7 = %x_5 |}]
let%test _ = mem_eq x z r2
let%test _ = mem_eq x y (or_ r1 r2)
let%test _ = entails (or_ r1 r2) r1
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 (g x y) (g z y) r2
let%test _ =
mem_eq w z (rename r2 Var.Subst.(extend empty ~replace:x_ ~with_:w_))
let%test _ =
r2 == rename r2 Var.Subst.(extend empty ~replace:w_ ~with_:x_)
let%test _ =
mem_eq v w
(rename r2
Var.Subst.(
empty
|> extend ~replace:x_ ~with_:v_
|> extend ~replace:y_ ~with_: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 _ =
printf pp r3 ;
[%expect
{|
{sat= true;
rep= [[%t_1 ↦ %w_4];
[%u_2 ↦ %w_4];
[%v_3 ↦ %w_4];
[%x_5 ↦ %w_4];
[%z_7 ↦ %w_4];
[(%y_6 xor %w_4) ↦ %w_4];
[(%y_6 xor %z_7) ↦ %w_4]];
lkp= [[(%y_6 xor %w_4) ↦ (%y_6 xor %w_4)];
[(%y_6 xor %z_7) ↦ (%y_6 xor %z_7)];
[(xor %y_6) ↦ (xor %y_6)]];
cls= [[%w_4
↦ {(%y_6 xor %w_4), %t_1, %z_7, %u_2, %x_5, %v_3, %w_4,
(%y_6 xor %z_7)}]];
use= [[%w_4 ↦ {(%y_6 xor %w_4)}];
[%y_6 ↦ {(xor %y_6)}];
[(xor %y_6) ↦ {(%y_6 xor %w_4), (%y_6 xor %z_7)}]]} |}]
let%test _ = mem_eq t z r3
let%test _ = mem_eq x z r3
let%test _ = mem_eq x z (and_ r2 r3)
let r4 = of_eqs [(w + !2, x - !3); (x - !5, y + !7); (y, z - !4)]
let%test _ = mem_eq x (w + !5) r4
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%test _ = mem_eq x y r6
let r7 = of_eqs [(v, x); (w, z); (y, z)]
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
|> Exp.equal x
let%test _ = mem_eq (g w x) (g w z) (of_eqs [(g w x, g y z); (x, z)])
let%test _ = mem_eq (g w x) (g w z) (of_eqs [(g w x, g y w); (x, z)])
end )
Write Preview
Loading…
Cancel
Save