From 1ddb5fb249df35ac43e14be1fb5a06feeaec470e Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Feb 2021 04:33:23 -0800 Subject: [PATCH] [sledge] Represent equality classes explicitly Summary: Currently the equality classes are computed from the representatives solution substitution when needed. This diff instead maintains them as part of the representation of the context. By itself this does not make a huge difference, but it is necessary to make other operations incremental. Reviewed By: jvillard Differential Revision: D25883715 fbshipit-source-id: 1b444a0dc --- sledge/nonstdlib/list.ml | 4 +- sledge/nonstdlib/list.mli | 2 + sledge/src/fol/context.ml | 348 ++++++++++++++++++++------------ sledge/src/fol/trm.ml | 5 + sledge/src/fol/trm.mli | 1 + sledge/src/test/context_test.ml | 50 ++--- sledge/src/test/fol_test.ml | 129 ++++++++---- sledge/src/test/sh_test.ml | 4 +- 8 files changed, 342 insertions(+), 201 deletions(-) diff --git a/sledge/nonstdlib/list.ml b/sledge/nonstdlib/list.ml index 2a2457a59..f2424ce3d 100644 --- a/sledge/nonstdlib/list.ml +++ b/sledge/nonstdlib/list.ml @@ -91,13 +91,13 @@ let rec pp ?pre ?suf sep pp_elt fs = function | xs -> Format.fprintf fs "%( %)%a" sep (pp sep pp_elt) xs ) ; Option.iter ~f:(Format.fprintf fs) suf -let pp_diff ~cmp sep pp_elt fs (xs, ys) = +let pp_diff ~cmp ?pre ?suf sep pp_elt fs (xs, ys) = let pp_diff_elt fs (elt : _ Either.t) = match elt with | Left x -> Format.fprintf fs "-- %a" pp_elt x | Right y -> Format.fprintf fs "++ %a" pp_elt y in - pp sep pp_diff_elt fs (symmetric_diff ~cmp xs ys) + pp ?pre ?suf sep pp_diff_elt fs (symmetric_diff ~cmp xs ys) module Assoc = struct include Assoc diff --git a/sledge/nonstdlib/list.mli b/sledge/nonstdlib/list.mli index 2825703e3..28a235d40 100644 --- a/sledge/nonstdlib/list.mli +++ b/sledge/nonstdlib/list.mli @@ -20,6 +20,8 @@ val pp : val pp_diff : cmp:('a -> 'a -> int) + -> ?pre:(unit, unit) fmt + -> ?suf:(unit, unit) fmt -> (unit, unit) fmt -> 'a pp -> ('a list * 'a list) pp diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index c6ca7c6b3..b843cb196 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -12,7 +12,7 @@ open Exp (* Solution Substitutions =================================================*) module Subst : sig - type t [@@deriving compare, equal, sexp] + type t = Trm.t Trm.Map.t [@@deriving compare, equal, sexp] val pp : t pp val pp_diff : (t * t) pp @@ -34,6 +34,7 @@ module Subst : sig val extend : Trm.t -> t -> t option val map_entries : f:(Trm.t -> Trm.t) -> t -> t val to_iter : t -> (Trm.t * Trm.t) iter + val to_list : t -> (Trm.t * Trm.t) list val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t (* direct representation manipulation *) @@ -58,6 +59,7 @@ end = struct let iteri = Trm.Map.iteri let for_alli = Trm.Map.for_alli let to_iter = Trm.Map.to_iter + let to_list = Trm.Map.to_list (** look up a term in a substitution *) let apply s a = Trm.Map.find a s |> Option.value ~default:a @@ -92,7 +94,8 @@ end = struct else ( assert ( Option.for_all ~f:(Trm.equal key) (Trm.Map.find key r) - || fail "domains intersect: %a" Trm.pp key () ) ; + || fail "domains intersect: %a ↦ %a in %a" Trm.pp key Trm.pp data + pp r () ) ; let s = Trm.Map.singleton key data in let r' = Trm.Map.map_endo ~f:(norm s) r in Trm.Map.add ~key ~data r' ) @@ -119,7 +122,7 @@ end = struct if Trm.equal data' data then s else Trm.Map.add ~key ~data:data' s else let s = Trm.Map.remove key s in - match (key : Trm.t) with + match (key' : Trm.t) with | Z _ | Q _ -> s | _ -> Trm.Map.add_exn ~key:key' ~data:data' s ) @@ -178,7 +181,7 @@ end (* Equality classes =======================================================*) module Cls : sig - type t [@@deriving equal] + type t [@@deriving compare, equal, sexp] val empty : t val of_ : Trm.t -> t @@ -190,14 +193,16 @@ module Cls : sig val filter : t -> f:(Trm.t -> bool) -> t val partition : t -> f:(Trm.t -> bool) -> t * t val fold : t -> 's -> f:(Trm.t -> 's -> 's) -> 's + val map : t -> f:(Trm.t -> Trm.t) -> t val to_iter : t -> Trm.t iter val to_set : t -> Trm.Set.t - val sort : t -> t + val of_set : Trm.Set.t -> t val ppx : Trm.Var.strength -> t pp val pp : t pp + val pp_raw : t pp val pp_diff : (t * t) pp end = struct - type t = Trm.t list [@@deriving equal] + type t = Trm.t list [@@deriving compare, equal, sexp] let empty = [] let of_ e = [e] @@ -209,11 +214,19 @@ end = struct let filter = List.filter let partition = List.partition let fold = List.fold + let map = List.map_endo let to_iter = List.to_iter let to_set = Trm.Set.of_list - let sort = List.sort ~cmp:Trm.compare - let ppx x = List.pp "@ = " (Trm.ppx x) + let of_set s = Iter.to_list (Trm.Set.to_iter s) + + let ppx x fs es = + List.pp "@ = " (Trm.ppx x) fs (List.sort_uniq ~cmp:Trm.compare es) + let pp = ppx (fun _ -> None) + + let pp_raw fs es = + Trm.Set.pp_full ~pre:"{@[" ~suf:"@]}" ~sep:",@ " Trm.pp fs (to_set es) + let pp_diff = List.pp_diff ~cmp:Trm.compare "@ = " Trm.pp end @@ -222,49 +235,41 @@ end (** see also [invariant] *) type t = { xs: Var.Set.t - (** existential variables that did not appear in input equations *) + (** existential variables that did not appear in input formulas *) ; sat: bool (** [false] only if constraints are inconsistent *) ; rep: Subst.t (** functional set of oriented equations: map [a] to [a'], indicating that [a = a'] holds, and that [a'] is the 'rep(resentative)' of [a] *) + ; cls: Cls.t Trm.Map.t + (** map each representative to the set of terms in its class *) ; pnd: (Trm.t * Trm.t) list (** pending equations to add (once invariants are reestablished) *) } [@@deriving compare, equal, sexp] -let classes r = - Subst.fold r.rep Trm.Map.empty ~f:(fun ~key:elt ~data:rep cls -> - if Trm.equal elt rep then cls - else - Trm.Map.update rep cls ~f:(fun cls0 -> - Cls.add elt (Option.value cls0 ~default:Cls.empty) ) ) - -let cls_of r e = - let e' = Subst.apply r.rep e in - Trm.Map.find e' (classes r) |> Option.value ~default:(Cls.of_ e') - (* Pretty-printing ========================================================*) let pp_eq fs (e, f) = Format.fprintf fs "@[%a = %a@]" Trm.pp e Trm.pp f -let pp_pnd = List.pp ";@ " pp_eq -let pp_raw fs {sat; rep; pnd} = +let pp_raw fs {sat; rep; cls; 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 (k, v) in Format.fprintf fs "[@[%a@]]" (List.pp ";@ " pp_assoc) alist in - let pp_term_v fs (k, v) = if not (Trm.equal k v) then Trm.pp fs v in + let pp_trm_v fs (k, v) = if not (Trm.equal k v) then Trm.pp fs v in + let pp_cls_v fs (_, cls) = Cls.pp_raw fs cls in let pp_pnd fs pnd = if not (List.is_empty pnd) then - Format.fprintf fs ";@ pnd= @[%a@]" pp_pnd pnd + Format.fprintf fs ";@ pnd= @[%a@]" (List.pp ";@ " pp_eq) pnd in - Format.fprintf fs "@[{@[sat= %b;@ rep= %a%a@]}@]" sat - (pp_alist Trm.pp pp_term_v) - (Iter.to_list (Subst.to_iter rep)) - pp_pnd pnd + Format.fprintf fs "@[{@[sat= %b;@ rep= %a;@ cls= %a%a@]}@]" sat + (pp_alist Trm.pp pp_trm_v) + (Subst.to_list rep) + (pp_alist Trm.pp pp_cls_v) + (Trm.Map.to_list cls) pp_pnd pnd let pp_diff fs (r, s) = let pp_sat fs = @@ -275,33 +280,35 @@ let pp_diff fs (r, s) = if not (Subst.is_empty r.rep) then Format.fprintf fs "rep= %a;@ " Subst.pp_diff (r.rep, s.rep) in + let pp_cls fs = + if not (Trm.Map.equal Cls.equal r.cls s.cls) then + Format.fprintf fs "cls= %a;@ " + (Trm.Map.pp_diff ~eq:Cls.equal Trm.pp Cls.pp_raw Cls.pp_diff) + (r.cls, s.cls) + in let pp_pnd fs = - Format.fprintf fs "pnd= @[%a@]" - (List.pp_diff ~cmp:[%compare: Trm.t * Trm.t] ";@ " pp_eq) - (r.pnd, s.pnd) + List.pp_diff ~cmp:[%compare: Trm.t * Trm.t] ~pre:"pnd= @[" ~suf:"@]" + ";@ " pp_eq fs (r.pnd, s.pnd) in - Format.fprintf fs "@[{@[%t%t%t@]}@]" pp_sat pp_rep pp_pnd + Format.fprintf fs "@[{@[%t%t%t%t@]}@]" pp_sat pp_rep pp_cls pp_pnd let ppx_classes x fs clss = List.pp "@ @<2>∧ " (fun fs (rep, cls) -> if not (Cls.is_empty cls) then Format.fprintf fs "@[%a@ = %a@]" (Trm.ppx x) rep (Cls.ppx x) cls ) - fs - (Iter.to_list (Trm.Map.to_iter clss)) + fs (Trm.Map.to_list clss) -let pp_classes fs r = ppx_classes (fun _ -> None) fs (classes r) -let pp_diff_clss = Trm.Map.pp_diff ~eq:Cls.equal Trm.pp Cls.pp Cls.pp_diff +let pp_classes fs r = ppx_classes (fun _ -> None) fs r.cls let pp fs r = - let clss = classes r in - if Trm.Map.is_empty clss then + if Trm.Map.is_empty r.cls then Format.fprintf fs (if r.sat then "tt" else "ff") - else ppx_classes (fun _ -> None) fs clss + else pp_classes fs r let ppx var_strength fs clss noneqs = - let without_anon_vars = - Cls.filter ~f:(fun e -> + let without_anon_vars es = + Cls.filter es ~f:(fun e -> match Var.of_trm e with | Some v -> Poly.(var_strength v <> Some `Anonymous) | None -> true ) @@ -309,8 +316,7 @@ let ppx var_strength fs clss noneqs = let clss = Trm.Map.fold clss Trm.Map.empty ~f:(fun ~key:rep ~data:cls m -> let cls = without_anon_vars cls in - if not (Cls.is_empty cls) then - Trm.Map.add ~key:rep ~data:(Cls.sort cls) m + if not (Cls.is_empty cls) then Trm.Map.add ~key:rep ~data:cls m else m ) in let first = Trm.Map.is_empty clss in @@ -321,6 +327,8 @@ let ppx var_strength fs clss noneqs = "@ @<2>∧ " (Fml.ppx var_strength) fs noneqs ~suf:"@]" ; first && List.is_empty noneqs +let pp_diff_cls = Trm.Map.pp_diff ~eq:Cls.equal Trm.pp Cls.pp Cls.pp_diff + (* Basic queries ==========================================================*) (** test membership in carrier *) @@ -355,12 +363,28 @@ let pre_invariant r = let rep' = Subst.norm r.rep rep in Trm.equal rep rep' || fail "not idempotent: %a != %a in@ %a" Trm.pp rep Trm.pp rep' - Subst.pp r.rep () ) ) + Subst.pp r.rep () ) ; + (* every term is in the class of its rep *) + assert ( + Trm.equal trm rep + || Trm.Set.mem trm + (Cls.to_set + (Trm.Map.find rep r.cls |> Option.value ~default:Cls.empty)) + || fail "%a not in cls of %a = {%a}@ %a" Trm.pp trm Trm.pp rep + Cls.pp + (Trm.Map.find rep r.cls |> Option.value ~default:Cls.empty) + pp_raw r () ) ) ; + Trm.Map.iteri r.cls ~f:(fun ~key:rep ~data:cls -> + (* each class does not include its rep *) + assert (not (Trm.Set.mem rep (Cls.to_set cls))) ; + (* representative of every element of [rep]'s class is [rep] *) + Iter.iter (Cls.to_iter cls) ~f:(fun elt -> + assert (Option.exists ~f:(Trm.equal rep) (Subst.find elt r.rep)) ) ) let invariant r = let@ () = Invariant.invariant [%here] r [%sexp_of: t] in - pre_invariant r ; assert (List.is_empty r.pnd) ; + pre_invariant r ; assert ( (not r.sat) || Subst.for_alli r.rep ~f:(fun ~key:a ~data:a' -> @@ -371,21 +395,67 @@ let invariant r = || fail "not congruent %a@ %a@ in@ %a" Trm.pp a Trm.pp b pp r () ) ) ) -(* Representation helpers =================================================*) +(* Extending the carrier ==================================================*) + +let rec extend_ a s = + [%trace] + ~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a Subst.pp s) + ~retn:(fun {pf} s' -> pf "%a" Subst.pp_diff (s, s')) + @@ fun () -> + match (a : Trm.t) with + | Z _ | Q _ -> s + | _ -> ( + if Theory.is_interpreted a then Iter.fold ~f:extend_ (Trm.trms a) s + else + (* add uninterpreted terms *) + match Subst.extend a s with + (* and their subterms if newly added *) + | Some s -> Iter.fold ~f:extend_ (Trm.trms a) s + | None -> s ) -let add_to_pnd a a' x = - if Trm.equal a a' then x else {x with pnd= (a, a') :: x.pnd} +(** add a term to the carrier *) +let extend a x = + [%trace] + ~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a pp x) + ~retn:(fun {pf} x' -> + pf "%a" pp_diff (x, x') ; + pre_invariant x' ) + @@ fun () -> + let rep = extend_ a x.rep in + if rep == x.rep then x else {x with rep} (* Propagation ============================================================*) -let propagate1 (trm, rep) x = +(** add a=a' to x using a' as the representative *) +let propagate1 (a, a') x = [%trace] - ~call:(fun {pf} -> - pf "@ @[%a ↦ %a@]@ %a" Trm.pp trm Trm.pp rep pp_raw x ) + ~call:(fun {pf} -> pf "@ @[%a ↦ %a@]@ %a" Trm.pp a Trm.pp a' pp_raw x) ~retn:(fun {pf} -> pf "%a" pp_raw) @@ fun () -> - let rep = Subst.compose1 ~key:trm ~data:rep x.rep in - {x with rep} + (* pending equations need not be between terms in the carrier *) + let x = extend a (extend a' x) in + let s = Trm.Map.singleton a a' in + Trm.Map.fold x.rep x ~f:(fun ~key:_ ~data:b0' x -> + let b' = Subst.norm s b0' in + if b' == b0' then x + else + let b0'_cls, cls = + Trm.Map.find_and_remove b0' x.cls + |> Option.value ~default:(Cls.empty, x.cls) + in + let b0'_cls, pnd = + if Theory.is_interpreted b0' then (b0'_cls, (b0', b') :: x.pnd) + else (Cls.add b0' b0'_cls, x.pnd) + in + let rep = + Cls.fold b0'_cls x.rep ~f:(fun c rep -> + Trm.Map.add ~key:c ~data:b' rep ) + in + let cls = + Trm.Map.update b' cls ~f:(fun b'_cls -> + Cls.union b0'_cls (Option.value b'_cls ~default:Cls.empty) ) + in + {x with rep; cls; pnd} ) let solve ~wrt ~xs d e pending = [%trace] @@ -416,7 +486,8 @@ let rec propagate ~wrt x = let empty = let rep = Subst.empty in - {xs= Var.Set.empty; sat= true; rep; pnd= []} |> check invariant + {xs= Var.Set.empty; sat= true; rep; cls= Trm.Map.empty; pnd= []} + |> check invariant let unsat = {empty with sat= false} @@ -453,30 +524,15 @@ let canon_f r b = ~retn:(fun {pf} -> pf "%a" Fml.pp) @@ fun () -> Fml.map_trms ~f:(canon r) b -let rec extend_ a r = - match (a : Trm.t) with - | Z _ | Q _ -> r - | _ -> ( - if Theory.is_interpreted a then Iter.fold ~f:extend_ (Trm.trms a) r - else - (* add uninterpreted terms *) - match Subst.extend a r with - (* and their subterms if newly added *) - | Some r -> Iter.fold ~f:extend_ (Trm.trms a) r - | None -> r ) - -(** add a term to the carrier *) -let extend a r = - let rep = extend_ a r.rep in - if rep == r.rep then r else {r with rep} |> check pre_invariant - let merge ~wrt a b x = [%trace] ~call:(fun {pf} -> pf "@ %a@ %a@ %a" Trm.pp a Trm.pp b pp x) ~retn:(fun {pf} x' -> pf "%a" pp_diff (x, x') ; pre_invariant x' ) - @@ fun () -> propagate ~wrt (add_to_pnd a b x) + @@ fun () -> + let x = {x with pnd= (a, b) :: x.pnd} in + propagate ~wrt x (** find an unproved equation between congruent terms *) let find_missing r = @@ -510,21 +566,25 @@ let close ~wrt r = pf "%a" pp_diff (r, r') ; invariant r'] -let and_eq_ ~wrt a b r = - if not r.sat then r +let and_eq_ ~wrt a b x = + [%trace] + ~call:(fun {pf} -> pf "@ @[%a = %a@]@ %a" Trm.pp a Trm.pp b pp x) + ~retn:(fun {pf} x' -> + pf "%a" pp_diff (x, x') ; + invariant x' ) + @@ fun () -> + if not x.sat then x else - let r0 = r in - 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 Trm.equal a' b' then r + let x0 = x in + let a' = canon x a in + let b' = canon x b in + if Trm.equal a' b' then extend a' (extend b' x) else - let r = merge ~wrt a' b' r in + let x = merge ~wrt a' b' x in match (a, b) with - | (Var _ as v), _ when not (in_car r0 v) -> r - | _, (Var _ as v) when not (in_car r0 v) -> r - | _ -> close ~wrt r + | (Var _ as v), _ when not (in_car x0 v) -> x + | _, (Var _ as v) when not (in_car x0 v) -> x + | _ -> close ~wrt x let extract_xs r = (r.xs, {r with xs= Var.Set.empty}) @@ -545,6 +605,10 @@ let implies r b = let refutes r b = Fml.equal Fml.ff (canon_f r b) let normalize r e = Term.map_trms ~f:(canon r) e +let cls_of r e = + let e' = Subst.apply r.rep e in + Trm.Map.find e' r.cls |> Option.value ~default:(Cls.of_ e') + let class_of r e = match Term.get_trm (normalize r e) with | Some e' -> @@ -552,7 +616,7 @@ let class_of r e = | None -> [] let diff_classes r s = - Trm.Map.filter_mapi (classes r) ~f:(fun ~key:rep ~data:cls -> + Trm.Map.filter_mapi r.cls ~f:(fun ~key:rep ~data:cls -> let cls' = Cls.filter cls ~f:(fun exp -> not (implies s (Fml.eq rep exp))) in @@ -584,7 +648,7 @@ let apply_subst wrt s r = ; ( if Subst.is_empty s then r else - Trm.Map.fold (classes r) {r with rep= Subst.empty} + Trm.Map.fold r.cls {r with rep= Subst.empty; cls= Trm.Map.empty} ~f:(fun ~key:rep ~data:cls r -> let rep' = Subst.subst_ s rep in Cls.fold cls r ~f:(fun trm r -> @@ -619,7 +683,7 @@ let inter wrt r s = else if not r.sat then s else let merge_mems rs r s = - Trm.Map.fold (classes s) rs ~f:(fun ~key:rep ~data:cls rs -> + Trm.Map.fold s.cls rs ~f:(fun ~key:rep ~data:cls rs -> Cls.fold cls ([rep], rs) ~f:(fun exp (reps, rs) -> @@ -673,17 +737,23 @@ let dnf f = let bot = Iter.empty in Fml.fold_dnf ~meet1 ~join1 ~top ~bot f -let rename r sub = - [%Trace.call fun {pf} -> pf "@ @[%a@]@ %a" Var.Subst.pp sub pp r] - ; - let rep = - Subst.map_entries ~f:(Trm.map_vars ~f:(Var.Subst.apply sub)) r.rep +let rename x sub = + [%trace] + ~call:(fun {pf} -> pf "@ @[%a@]@ %a" Var.Subst.pp sub pp x) + ~retn:(fun {pf} x' -> + pf "%a" pp_diff (x, x') ; + invariant x' ) + @@ fun () -> + let apply_sub = Trm.map_vars ~f:(Var.Subst.apply sub) in + let rep = Subst.map_entries ~f:apply_sub x.rep in + let cls = + Trm.Map.fold x.cls x.cls ~f:(fun ~key:a0' ~data:a0'_cls cls -> + let a' = apply_sub a0' in + let a'_cls = Cls.map ~f:apply_sub a0'_cls in + Trm.Map.add ~key:a' ~data:a'_cls + (if a' == a0' then cls else Trm.Map.remove a0' cls) ) in - (if rep == r.rep then r else {r with rep}) - |> - [%Trace.retn fun {pf} r' -> - pf "%a" pp_diff (r, r') ; - invariant r'] + if rep == x.rep && cls == x.cls then x else {x with rep; cls} let trms r = Iter.flat_map ~f:(fun (k, v) -> Iter.doubleton k v) (Subst.to_iter r.rep) @@ -904,6 +974,8 @@ let solve_uninterp_eqs us (cls, subst) = let cls = Cls.add rep_xs cls_us in let subst = Cls.fold cls_xs subst ~f:(fun trm_xs subst -> + let trm_xs = Subst.subst_ subst trm_xs in + let rep_xs = Subst.subst_ subst rep_xs in Subst.compose1 ~key:trm_xs ~data:rep_xs subst ) in (cls, subst) @@ -941,7 +1013,7 @@ let solve_class us us_xs ~key:rep ~data:cls (classes, subst) = |> [%Trace.retn fun {pf} (classes', subst') -> pf "subst: @[%a@]@ classes: @[%a@]" Subst.pp_diff (subst, subst') - pp_diff_clss (classes0, classes')] + pp_diff_cls (classes0, classes')] let solve_concat_extracts_eq r x = [%Trace.call fun {pf} -> pf "@ %a@ %a" Trm.pp x pp r] @@ -1022,7 +1094,7 @@ let solve_classes r xs (classes, subst, us) = |> [%Trace.retn fun {pf} (classes', subst', _) -> pf "subst: @[%a@]@ classes: @[%a@]" Subst.pp_diff (subst, subst') - pp_diff_clss (classes, classes')] + pp_diff_cls (classes, classes')] let pp_vss fs vss = Format.fprintf fs "[@[%a@]]" @@ -1042,7 +1114,7 @@ let solve_for_vars vss r = let us, vss = match vss with us :: vss -> (us, vss) | [] -> (Var.Set.empty, vss) in - List.fold ~f:(solve_classes r) vss (classes r, Subst.empty, us) |> snd3 + List.fold ~f:(solve_classes r) vss (r.cls, Subst.empty, us) |> snd3 |> [%Trace.retn fun {pf} subst -> pf "%a" Subst.pp subst ; @@ -1079,57 +1151,73 @@ let trivial vs r = Var.Set.add v ks | _ -> ks ) -let trim ks r = +let trim ks x = [%trace] - ~call:(fun {pf} -> pf "@ %a@ %a" Var.Set.pp_xs ks pp_raw r) - ~retn:(fun {pf} r' -> - pf "%a" pp_raw r' ; - assert (Var.Set.disjoint ks (fv r')) ) + ~call:(fun {pf} -> pf "@ %a@ %a" Var.Set.pp_xs ks pp_raw x) + ~retn:(fun {pf} x' -> + pf "%a" pp_raw x' ; + invariant x' ; + assert (Var.Set.disjoint ks (fv x')) ) @@ fun () -> - let kills = Trm.Set.of_iter (Iter.map ~f:Trm.var (Var.Set.to_iter ks)) in - (* compute classes including reps *) + (* expand classes to include reps *) let reps = - Subst.fold r.rep Trm.Set.empty ~f:(fun ~key:_ ~data:rep reps -> + Subst.fold x.rep Trm.Set.empty ~f:(fun ~key:_ ~data:rep reps -> Trm.Set.add rep reps ) in let clss = - Trm.Set.fold reps (classes r) ~f:(fun rep clss -> + Trm.Set.fold reps x.cls ~f:(fun rep clss -> Trm.Map.update rep clss ~f:(fun cls0 -> Cls.add rep (Option.value cls0 ~default:Cls.empty) ) ) in - (* trim classes to those that intersect kills *) - let clss = - Trm.Map.filter_mapi clss ~f:(fun ~key:_ ~data:cls -> - let cls = Cls.to_set cls in - if Trm.Set.disjoint kills cls then None else Some cls ) - in - (* enumerate affected classes and update solution subst *) - let rep = - Trm.Map.fold clss r.rep ~f:(fun ~key:rep ~data:cls s -> - (* remove mappings for non-rep class elements to kill *) - let drop = Trm.Set.inter cls kills in - let s = Trm.Set.fold ~f:Subst.remove drop s in - if not (Trm.Set.mem rep kills) then s + (* enumerate expanded classes and update solution subst *) + let kills = Trm.Set.of_vars ks in + Trm.Map.fold clss x ~f:(fun ~key:a' ~data:ecls x -> + (* remove mappings for non-rep class elements to kill *) + let keep, drop = Trm.Set.diff_inter (Cls.to_set ecls) kills in + if Trm.Set.is_empty drop then x + else + let rep = Trm.Set.fold ~f:Subst.remove drop x.rep in + let x = {x with rep} in + (* new class is keepers without rep *) + let keep' = Trm.Set.remove a' keep in + let ecls = Cls.of_set keep' in + if keep' != keep then + (* a' is to be kept: continue to use it as rep *) + let cls = + if Cls.is_empty ecls then Trm.Map.remove a' x.cls + else Trm.Map.add ~key:a' ~data:ecls x.cls + in + {x with cls} else - (* if rep is to be removed, choose new one from the keepers *) - let keep = Trm.Set.diff cls drop in + (* a' is to be removed: choose new rep from the keepers *) + let cls = Trm.Map.remove a' x.cls in + let x = {x with cls} in match Trm.Set.reduce keep ~f:(fun x y -> if Theory.prefer x y < 0 then x else y ) with - | Some rep' -> + | Some b' -> (* add mappings from each keeper to the new representative *) - Trm.Set.fold keep s ~f:(fun elt s -> - Subst.add ~key:elt ~data:rep' s ) - | None -> s ) - in - {r with rep} + let rep = + Trm.Set.fold keep x.rep ~f:(fun elt rep -> + Subst.add ~key:elt ~data:b' rep ) + in + (* add trimmed class to new rep *) + let cls = + if Cls.is_empty ecls then x.cls + else Trm.Map.add ~key:b' ~data:ecls x.cls + in + {x with rep; cls} + | None -> + (* entire class removed *) + x ) let apply_and_elim ~wrt xs s r = [%trace] ~call:(fun {pf} -> pf "@ %a%a@ %a" Var.Set.pp_xs xs Subst.pp s pp_raw r) ~retn:(fun {pf} (zs, r', ks) -> pf "%a@ %a@ %a" Var.Set.pp_xs zs pp_raw r' Var.Set.pp_xs ks ; + invariant r' ; assert (Var.Set.subset ks ~of_:xs) ; assert (Var.Set.disjoint ks (fv r')) ) @@ fun () -> diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index 328ab7ba0..b623b2f4e 100644 --- a/sledge/src/fol/trm.ml +++ b/sledge/src/fol/trm.ml @@ -393,6 +393,11 @@ module Set = struct include Set.Make (T) include Provide_of_sexp (T) include Provide_pp (T) + + let of_vars : Var.Set.t -> t = + fun vs -> + of_iter + (Iter.map ~f:(fun v -> (v : Var.t :> Trm.t)) (Var.Set.to_iter vs)) end module Map = struct diff --git a/sledge/src/fol/trm.mli b/sledge/src/fol/trm.mli index 969a3cd4a..92b602f65 100644 --- a/sledge/src/fol/trm.mli +++ b/sledge/src/fol/trm.mli @@ -43,6 +43,7 @@ module Set : sig val t_of_sexp : Sexp.t -> t val pp : t pp val pp_diff : (t * t) pp + val of_vars : Var.Set.t -> t end module Map : sig diff --git a/sledge/src/test/context_test.ml b/sledge/src/test/context_test.ml index da14a7fe2..2ec16e59d 100644 --- a/sledge/src/test/context_test.ml +++ b/sledge/src/test/context_test.ml @@ -61,8 +61,8 @@ let%test_module _ = pp r3 ; [%expect {| - %t_1 = g(%y_6, %z_7) = g(%y_6, %v_3) = %z_7 = %x_5 = %w_4 = %v_3 - = %u_2 + %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %v_3) + = g(%y_6, %z_7) {sat= true; rep= [[%t_1 ↦ ]; @@ -73,7 +73,10 @@ let%test_module _ = [%y_6 ↦ ]; [%z_7 ↦ %t_1]; [g(%y_6, %v_3) ↦ %t_1]; - [g(%y_6, %z_7) ↦ %t_1]]} |}] + [g(%y_6, %z_7) ↦ %t_1]]; + cls= [[%t_1 + ↦ {%u_2, %v_3, %w_4, %x_5, %z_7, g(%y_6, %v_3), + g(%y_6, %z_7)}]]} |}] let%test _ = implies_eq r3 t z @@ -82,8 +85,9 @@ let%test_module _ = let%expect_test _ = pp r15 ; - [%expect {| - {sat= true; rep= [[%x_5 ↦ 1]]} |}] + [%expect + {| + {sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]} |}] let%test _ = implies_eq r15 (Term.neg b) (Term.apply (Signed 1) [|!1|]) let%test _ = implies_eq r15 (Term.apply (Unsigned 1) [|b|]) !1 @@ -91,24 +95,22 @@ let%test_module _ = let%expect_test _ = replay {|(Solve_for_vars - (((Var (id 0) (name 2)) (Var (id 0) (name 6)) (Var (id 0) (name 8))) - ((Var (id 5) (name a0)) (Var (id 6) (name b)) (Var (id 7) (name m)) - (Var (id 8) (name a)) (Var (id 9) (name a0)))) - ((xs ()) (sat true) - (rep - (((Var (id 9) (name a0)) (Var (id 5) (name a0))) - ((Var (id 8) (name a)) - (Concat - ((Sized (seq (Var (id 5) (name a0))) (siz (Z 4))) - (Sized (seq (Z 0)) (siz (Z 4)))))) - ((Var (id 7) (name m)) (Z 8)) - ((Var (id 6) (name b)) (Var (id 0) (name 2))) - ((Var (id 5) (name a0)) (Var (id 5) (name a0))) - ((Var (id 0) (name 6)) - (Concat - ((Sized (seq (Var (id 5) (name a0))) (siz (Z 4))) - (Sized (seq (Z 0)) (siz (Z 4)))))) - ((Var (id 0) (name 2)) (Var (id 0) (name 2))))) - (pnd ())))|} ; + (() + ((Var (id 0) (name 0)) (Var (id 0) (name 2)) (Var (id 0) (name 4)) + (Var (id 0) (name 5)) (Var (id 0) (name 7)) (Var (id 0) (name 8)) + (Var (id 0) (name 9)) (Var (id 1) (name a)) (Var (id 2) (name a)) + (Var (id 3) (name a))) + ()) + ((xs ()) (sat true) + (rep + (((Apply (Uninterp g.1) ()) (Apply (Uninterp g.1) ())) + ((Var (id 0) (name 4)) (Var (id 0) (name 0))) + ((Var (id 0) (name 2)) (Var (id 0) (name 0))) + ((Var (id 0) (name 0)) (Var (id 0) (name 0))))) + (cls + (((Var (id 0) (name 0)) + ((Var (id 0) (name 2)) (Var (id 0) (name 4)) + (Var (id 0) (name 2)))))) + (pnd ())))|} ; [%expect {| |}] end ) diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml index ca3293b8f..2bfefd25b 100644 --- a/sledge/src/test/fol_test.ml +++ b/sledge/src/test/fol_test.ml @@ -16,7 +16,10 @@ let%test_module _ = (* let () = * Trace.init ~margin:160 - * ~config:(Result.get_ok (Trace.parse "+Fol+Context+Arithmetic")) + * ~config: + * (Result.get_ok + * (Trace.parse + * "+Fol+Context-Context.canon-Context.canon_f-Context.norm")) * () *) [@@@warning "-32"] @@ -66,7 +69,7 @@ let%test_module _ = let%expect_test _ = pp_raw f1 ; - [%expect {| {sat= false; rep= []} |}] + [%expect {| {sat= false; rep= []; cls= []} |}] let%test _ = is_unsat (add_eq !1 !1 f1) @@ -76,7 +79,7 @@ let%test_module _ = let%expect_test _ = pp_raw f2 ; - [%expect {| {sat= false; rep= []} |}] + [%expect {| {sat= false; rep= []; cls= []} |}] let f3 = of_eqs [(x + !0, x + !1)] @@ -84,7 +87,7 @@ let%test_module _ = let%expect_test _ = pp_raw f3 ; - [%expect {| {sat= false; rep= []} |}] + [%expect {| {sat= false; rep= []; cls= []} |}] let f4 = of_eqs [(x, y); (x + !0, y + !1)] @@ -92,7 +95,11 @@ let%test_module _ = let%expect_test _ = pp_raw f4 ; - [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]} |}] + [%expect + {| + {sat= false; + rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]; + cls= [[%x_5 ↦ {%y_6}]]} |}] let t1 = of_eqs [(!1, !1)] @@ -108,7 +115,7 @@ let%test_module _ = let%expect_test _ = pp_raw r0 ; - [%expect {| {sat= true; rep= []} |}] + [%expect {| {sat= true; rep= []; cls= []} |}] let%expect_test _ = pp r0 ; @@ -127,7 +134,7 @@ let%test_module _ = %x_5 = %y_6 - {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]} |}] + {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]; cls= [[%x_5 ↦ {%y_6}]]} |}] let%test _ = implies_eq r1 x y @@ -138,10 +145,11 @@ let%test_module _ = pp_raw r2 ; [%expect {| - %x_5 = f(%x_5) = %z_7 = %y_6 + %x_5 = %y_6 = %z_7 = f(%x_5) {sat= true; - rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [f(%x_5) ↦ %x_5]]} |}] + rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [f(%x_5) ↦ %x_5]]; + cls= [[%x_5 ↦ {%y_6, %z_7, f(%x_5)}]]} |}] let%test _ = implies_eq r2 x z let%test _ = implies_eq (inter r1 r2) x y @@ -162,11 +170,15 @@ let%test_module _ = pp_raw rs ; [%expect {| - {sat= true; rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]} + {sat= true; + rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]; + cls= [[%w_4 ↦ {%y_6, %z_7}]]} - {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]} + {sat= true; + rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]; + cls= [[%x_5 ↦ {%y_6, %z_7}]]} - {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]} |}] + {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]; cls= [[%y_6 ↦ {%z_7}]]} |}] let%test _ = let r = of_eqs [(w, y); (y, z)] in @@ -181,9 +193,9 @@ let%test_module _ = pp_raw r3 ; [%expect {| - %t_1 = g(%y_6, %z_7) = g(%y_6, %v_3) = %z_7 = %x_5 = %w_4 = %v_3 - = %u_2 - + %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %v_3) + = g(%y_6, %z_7) + {sat= true; rep= [[%t_1 ↦ ]; [%u_2 ↦ %t_1]; @@ -193,7 +205,10 @@ let%test_module _ = [%y_6 ↦ ]; [%z_7 ↦ %t_1]; [g(%y_6, %v_3) ↦ %t_1]; - [g(%y_6, %z_7) ↦ %t_1]]} |}] + [g(%y_6, %z_7) ↦ %t_1]]; + cls= [[%t_1 + ↦ {%u_2, %v_3, %w_4, %x_5, %z_7, g(%y_6, %v_3), + g(%y_6, %z_7)}]]} |}] let%test _ = implies_eq r3 t z let%test _ = implies_eq r3 x z @@ -212,7 +227,10 @@ let%test_module _ = rep= [[%w_4 ↦ (3 + %z_7)]; [%x_5 ↦ (8 + %z_7)]; [%y_6 ↦ (-4 + %z_7)]; - [%z_7 ↦ ]]} |}] + [%z_7 ↦ ]]; + cls= [[(-4 + %z_7) ↦ {%y_6}]; + [(3 + %z_7) ↦ {%w_4}]; + [(8 + %z_7) ↦ {%x_5}]]} |}] let%test _ = implies_eq r4 x (w + !5) let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5)) @@ -228,9 +246,11 @@ let%test_module _ = pp_raw r6 ; [%expect {| - 1 = %y_6 = %x_5 + 1 = %x_5 = %y_6 - {sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]]} |}] + {sat= true; + rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]]; + cls= [[1 ↦ {%x_5, %y_6}]]} |}] let%test _ = implies_eq r6 x y @@ -241,14 +261,15 @@ let%test_module _ = pp_raw r7 ; [%expect {| - %v_3 = %x_5 ∧ %w_4 = %z_7 = %y_6 + %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]]} |}] + [%z_7 ↦ %w_4]]; + cls= [[%v_3 ↦ {%x_5}]; [%w_4 ↦ {%y_6, %z_7}]]} |}] let r7' = add_eq x z r7 @@ -257,14 +278,15 @@ let%test_module _ = pp_raw r7' ; [%expect {| - %v_3 = %z_7 = %y_6 = %x_5 = %w_4 + %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]]} |}] + [%z_7 ↦ %v_3]]; + cls= [[%v_3 ↦ {%w_4, %x_5, %y_6, %z_7}]]} |}] let%test _ = normalize r7' w |> Term.equal v @@ -283,7 +305,9 @@ let%test_module _ = {| 14 = %y_6 ∧ 13×%z_7 = %x_5 - {sat= true; rep= [[%x_5 ↦ 13×%z_7]; [%y_6 ↦ 14]; [%z_7 ↦ ]]} |}] + {sat= true; + rep= [[%x_5 ↦ 13×%z_7]; [%y_6 ↦ 14]; [%z_7 ↦ ]]; + cls= [[14 ↦ {%y_6}]; [13×%z_7 ↦ {%x_5}]]} |}] let%test _ = implies_eq r8 y !14 @@ -294,9 +318,13 @@ let%test_module _ = pp_raw r9 ; [%expect {| - {sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]} - - {sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]} |}] + {sat= true; + rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]; + cls= [[(-16 + %z_7) ↦ {%x_5}]]} + + {sat= true; + rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]; + cls= [[(-16 + %z_7) ↦ {%x_5}]]} |}] let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8)) @@ -311,16 +339,20 @@ let%test_module _ = Format.printf "@.%a@." Term.pp (normalize r10 (x + !8 - z)) ; [%expect {| - {sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]} + {sat= true; + rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]; + cls= [[(-16 + %z_7) ↦ {%x_5}]]} - {sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]} + {sat= true; + rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]; + cls= [[(-16 + %z_7) ↦ {%x_5}]]} (-8 + -1×%x_5 + %z_7) 8 - + (8 + %x_5 + -1×%z_7) - + -8 |}] let%test _ = difference r10 z (x + !8) |> Poly.equal (Some (Z.of_int 8)) @@ -348,7 +380,8 @@ let%test_module _ = let%expect_test _ = pp_raw r13 ; - [%expect {| {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]} |}] + [%expect + {| {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]; cls= [[%y_6 ↦ {%z_7}]]} |}] let%test _ = not (is_unsat r13) (* incomplete *) @@ -357,8 +390,9 @@ let%test_module _ = let%expect_test _ = pp_raw r14 ; - [%expect {| - {sat= true; rep= [[%x_5 ↦ 1]]} |}] + [%expect + {| + {sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]} |}] let%test _ = implies_eq r14 a (Formula.inject Formula.tt) @@ -367,8 +401,9 @@ let%test_module _ = let%expect_test _ = pp_raw r14 ; - [%expect {| - {sat= true; rep= [[%x_5 ↦ 1]]} |}] + [%expect + {| + {sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]} |}] let%test _ = implies_eq r14 a (Formula.inject Formula.tt) (* incomplete *) @@ -379,8 +414,9 @@ let%test_module _ = let%expect_test _ = pp_raw r15 ; - [%expect {| - {sat= true; rep= [[%x_5 ↦ 1]]} |}] + [%expect + {| + {sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]} |}] (* f(x−1)−1=x+1, f(y)+1=y−1, y+1=x ⊢ false *) let r16 = @@ -394,7 +430,10 @@ let%test_module _ = rep= [[%x_5 ↦ (1 + %y_6)]; [%y_6 ↦ ]; [f(%y_6) ↦ (-2 + %y_6)]; - [f((-1 + %x_5)) ↦ (3 + %y_6)]]} |}] + [f((-1 + %x_5)) ↦ (3 + %y_6)]]; + cls= [[(-2 + %y_6) ↦ {f(%y_6)}]; + [(1 + %y_6) ↦ {%x_5}]; + [(3 + %y_6) ↦ {f((-1 + %x_5))}]]} |}] let%test _ = is_unsat r16 @@ -409,7 +448,8 @@ let%test_module _ = rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [f(%x_5) ↦ %x_5]; - [f(%y_6) ↦ (-1 + %x_5)]]} |}] + [f(%y_6) ↦ (-1 + %x_5)]]; + cls= [[%x_5 ↦ {%y_6, f(%x_5)}]; [(-1 + %x_5) ↦ {f(%y_6)}]]} |}] let%test _ = is_unsat r17 @@ -423,8 +463,9 @@ let%test_module _ = rep= [[%x_5 ↦ ]; [%y_6 ↦ ]; [f(%x_5) ↦ %x_5]; - [f(%y_6) ↦ (-1 + %y_6)]]} - + [f(%y_6) ↦ (-1 + %y_6)]]; + cls= [[%x_5 ↦ {f(%x_5)}]; [(-1 + %y_6) ↦ {f(%y_6)}]]} + %x_5 = f(%x_5) ∧ (-1 + %y_6) = f(%y_6) |}] let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)] @@ -433,7 +474,9 @@ let%test_module _ = pp_raw r19 ; [%expect {| - {sat= true; rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]]} |}] + {sat= true; + rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]]; + cls= [[0 ↦ {%x_5, %y_6, %z_7}]]} |}] let%test _ = implies_eq r19 x !0 let%test _ = implies_eq r19 y !0 diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml index e0f972940..ec92bde32 100644 --- a/sledge/src/test/sh_test.ml +++ b/sledge/src/test/sh_test.ml @@ -101,7 +101,7 @@ let%test_module _ = ( ( 0 = %x_7 ∧ emp) ∨ ( ( ( 1 = %y_8 ∧ emp) ∨ ( emp) )) ) ( (∃ %x_7, %x_8 . 2 = %x_8 ∧ (2 = %x_8) ∧ emp) - ∨ (∃ %x_7 . 1 = %y_8 = %x_7 ∧ ((1 = %x_7) ∧ (1 = %y_8)) ∧ emp) + ∨ (∃ %x_7 . 1 = %x_7 = %y_8 ∧ ((1 = %x_7) ∧ (1 = %y_8)) ∧ emp) ∨ ( 0 = %x_7 ∧ (0 = %x_7) ∧ emp) ) |}] @@ -125,7 +125,7 @@ let%test_module _ = ( (∃ %x_7, %x_9, %x_10 . 2 = %x_10 ∧ (2 = %x_10) ∧ emp) ∨ (∃ %x_7, %x_9 . - 1 = %x_9 = %y_8 ∧ ((1 = %y_8) ∧ (1 = %x_9)) + 1 = %y_8 = %x_9 ∧ ((1 = %y_8) ∧ (1 = %x_9)) ∧ emp) ∨ (∃ %x_7 . 0 = %x_7 ∧ (0 = %x_7) ∧ emp) ) |}]