From ee9aa931c44137fb3a070cd077d364a80dc3bae7 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Feb 2021 04:36:29 -0800 Subject: [PATCH] [sledge] Reimplement equality solver based on "use" superterm index Summary: Currently detection and propagation of consequences of newly added equality constraints is implemented using some operations that traverse the entire representation of the equality relation. This implementation strategy makes it relatively easy and robust to ensure that the consequences of constraints are treated in a sound and complete way. It does have the drawback that adding a constraint involves work that is proportional (nonlinearly even) to the number of all constraints. This can become a performance bottleneck. This diff reimplements the core operations using an additional data structure that essentially tracks the "super-term" relation between terms, which can be used to look up the existing constraints that might be involved in deriving new consequences when adding equalities. This means that adding new equalities no longer takes time proportional to the size of the entire equality context representation, but only to the number of existing constraints that might interact with the new constraint. Also, rewriting terms into canonical form no longer takes time proportional to size of the whole context, but only performs table lookups on the subterms of the term to canonize. Reviewed By: jvillard Differential Revision: D25883705 fbshipit-source-id: b3f266533 --- sledge/nonstdlib/set.ml | 1 + sledge/nonstdlib/set_intf.ml | 1 + sledge/src/fol/context.ml | 554 ++++++++++++++++++++------------ sledge/src/test/context_test.ml | 241 +++++++++++--- sledge/src/test/fol_test.ml | 246 ++++++++------ sledge/src/test/sh_test.ml | 18 +- 6 files changed, 684 insertions(+), 377 deletions(-) diff --git a/sledge/nonstdlib/set.ml b/sledge/nonstdlib/set.ml index 8783dbc81..92e08c6ab 100644 --- a/sledge/nonstdlib/set.ml +++ b/sledge/nonstdlib/set.ml @@ -56,6 +56,7 @@ end) : S with type elt = Elt.t = struct let inter = S.inter let union = S.union let diff_inter s t = (diff s t, inter s t) + let diff_inter_diff s t = (diff s t, inter s t, diff t s) let union_list ss = List.fold ~f:union ss empty let is_empty = S.is_empty let cardinal = S.cardinal diff --git a/sledge/nonstdlib/set_intf.ml b/sledge/nonstdlib/set_intf.ml index 30b1a6c8d..3dae44b13 100644 --- a/sledge/nonstdlib/set_intf.ml +++ b/sledge/nonstdlib/set_intf.ml @@ -60,6 +60,7 @@ module type S = sig val inter : t -> t -> t val union : t -> t -> t val diff_inter : t -> t -> t * t + val diff_inter_diff : t -> t -> t * t * t val union_list : t list -> t (** {1 Query} *) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index 483a3f5dc..9eef78307 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -177,50 +177,50 @@ end module Cls : sig type t [@@deriving compare, equal, sexp] + val ppx : Trm.Var.strength -> t pp + val pp : t pp + val pp_raw : t pp + val pp_diff : (t * t) pp val empty : t val add : Trm.t -> t -> t val remove : Trm.t -> t -> t val union : t -> t -> t val is_empty : t -> bool val pop : t -> (Trm.t * t) option + val fold : t -> 's -> f:(Trm.t -> 's -> 's) -> 's 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 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 compare, equal, sexp] - - let empty = [] - let add = List.cons - let remove = List.remove ~eq:Trm.equal - let union = List.rev_append - let is_empty = List.is_empty - let pop = function [] -> None | x :: xs -> Some (x, xs) - 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 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) + include Trm.Set + let to_set s = s + let of_set s = s + let ppx x fs es = pp_full ~sep:"@ = " (Trm.ppx x) fs es let pp = ppx (fun _ -> None) + let pp_raw fs es = pp_full ~pre:"{@[" ~suf:"@]}" ~sep:",@ " Trm.pp fs es +end - let pp_raw fs es = - Trm.Set.pp_full ~pre:"{@[" ~suf:"@]}" ~sep:",@ " Trm.pp fs (to_set es) +(* Use lists / Super-expressions ==========================================*) - let pp_diff = List.pp_diff ~cmp:Trm.compare "@ = " Trm.pp -end +module Use : sig + type t [@@deriving compare, equal, sexp] + + val pp : t pp + val pp_diff : (t * t) pp + val empty : t + val add : Trm.t -> t -> t + val remove : Trm.t -> t -> t + val is_empty : t -> bool + val mem : Trm.t -> t -> bool + val iter : t -> f:(Trm.t -> unit) -> unit + val fold : t -> 's -> f:(Trm.t -> 's -> 's) -> 's + val map : t -> f:(Trm.t -> Trm.t) -> t +end = + Trm.Set (* Conjunctions of atomic formula assumptions =============================*) @@ -235,6 +235,8 @@ type t = 'rep(resentative)' of [a] *) ; cls: Cls.t Trm.Map.t (** map each representative to the set of terms in its class *) + ; use: Use.t Trm.Map.t + (** map each solvable in the carrier to its immediate super-terms *) ; pnd: (Trm.t * Trm.t) list (** pending equations to add (once invariants are reestablished) *) } @@ -244,7 +246,7 @@ type t = let pp_eq fs (e, f) = Format.fprintf fs "@[%a = %a@]" Trm.pp e Trm.pp f -let pp_raw fs {sat; rep; cls; pnd} = +let pp_raw fs {sat; rep; 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 (k, v) @@ -253,14 +255,18 @@ let pp_raw fs {sat; rep; cls; pnd} = 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_use_v fs (_, use) = Use.pp fs use in let pp_pnd fs pnd = List.pp ~pre:";@ pnd= [@[" ";@ " ~suf:"@]]" pp_eq fs pnd in - Format.fprintf fs "@[{@[sat= %b;@ rep= %a;@ cls= %a%a@]}@]" sat + Format.fprintf fs + "@[{ @[sat= %b;@ rep= %a;@ cls= %a;@ use= %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 + (Trm.Map.to_list cls) + (pp_alist Trm.pp pp_use_v) + (Trm.Map.to_list use) pp_pnd pnd let pp_diff fs (r, s) = let pp_sat fs = @@ -275,11 +281,16 @@ let pp_diff fs (r, s) = Trm.Map.pp_diff ~eq:Cls.equal ~pre:";@ cls= @[" ~sep:";@ " ~suf:"@]" Trm.pp Cls.pp_raw Cls.pp_diff fs (r.cls, s.cls) in + let pp_use fs = + Trm.Map.pp_diff ~eq:Use.equal ~pre:";@ use= @[" ~sep:";@ " ~suf:"@]" + Trm.pp Use.pp Use.pp_diff fs (r.use, s.use) + in let pp_pnd fs = 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%t@] }@]" pp_sat pp_rep pp_cls pp_pnd + Format.fprintf fs "@[{ @[%t%t%t%t%t }@]@]" pp_sat pp_rep pp_cls pp_use + pp_pnd let ppx_classes x fs clss = List.pp "@ @<2>∧ " @@ -326,11 +337,15 @@ let trms r = let vars r = Iter.flat_map ~f:Trm.vars (trms r) let fv r = Var.Set.of_iter (vars r) -(** test membership in carrier *) -let in_car r e = Subst.mem e r.rep +(** test if a term is in the carrier *) +let in_car a x = Subst.mem a x.rep + +(** test if a term is a representative *) +let is_rep a x = + match Subst.find a x.rep with Some a' -> Trm.equal a a' | None -> false -(** congruent specialized to assume subterms of [a'] are [Subst.norm]alized - wrt [r] (or canonized) *) +(** congruent specialized to assume subterms of [a'] are normalized wrt [r] + (or canonized) *) let semi_congruent r a' b = Trm.equal a' (Trm.map ~f:(Subst.norm r.rep) b) (** terms are congruent if equal after normalizing subterms *) @@ -338,128 +353,291 @@ let congruent r a b = semi_congruent r (Trm.map ~f:(Subst.norm r.rep) a) b (* Invariant ==============================================================*) -let pre_invariant r = - let@ () = Invariant.invariant [%here] r [%sexp_of: t] in - Subst.iteri r.rep ~f:(fun ~key:trm ~data:rep -> - (* no interpreted terms in carrier *) - assert ( - Theory.is_noninterpreted trm || fail "non-interp %a" Trm.pp trm () - ) ; - (* carrier is closed under solvable subterms *) - Iter.iter (Theory.solvable_trms trm) ~f:(fun subtrm -> - assert ( - in_car r subtrm - || fail "@[subterm %a@ of %a@ not in carrier of@ %a@]" Trm.pp - subtrm Trm.pp trm pp r () ) ) ; - (* rep is idempotent *) - assert ( - 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 () ) ; - (* 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 - assert (List.is_empty r.pnd) ; - pre_invariant r ; +let find_check a x = + if not (Theory.is_noninterpreted a) then a + else + match Trm.Map.find a x.rep with + | Some a' -> a' + | None -> fail "%a not in carrier" Trm.pp a () + +let pre_invariant x = + let@ () = Invariant.invariant [%here] x [%sexp_of: t] in + try + Subst.iteri x.rep ~f:(fun ~key:a ~data:a' -> + (* only noninterpreted terms in dom of rep, except reps of + nontrivial classes *) + assert ( + Theory.is_noninterpreted a + || is_rep a x + && not + (Cls.is_empty + ( Trm.Map.find a' x.cls + |> Option.value ~default:Cls.empty )) + || fail "interp in rep dom %a" Trm.pp a () ) ; + (* carrier is closed under solvable subterms *) + Iter.iter (Theory.solvable_trms a) ~f:(fun b -> + assert ( + in_car b x + || fail "@[subterm %a@ of %a@ not in carrier@]" Trm.pp b + Trm.pp a () ) ) ; + (* rep is idempotent *) + assert ( + let a'' = Subst.norm x.rep a' in + Trm.equal a' a'' + || fail "not idempotent:@ @[%a@ <> %a@]@ %a" Trm.pp a' Trm.pp a'' + Subst.pp x.rep () ) ; + (* every term is in class of its rep *) + assert ( + let a'_cls = + Trm.Map.find a' x.cls |> Option.value ~default:Cls.empty + in + Trm.equal a a' + || Trm.Set.mem a (Cls.to_set a'_cls) + || fail "%a not in cls of %a = {%a}" Trm.pp a Trm.pp a' Cls.pp + a'_cls () ) ; + (* each term in carrier is in use list of each of its solvable + subterms *) + Iter.iter (Theory.solvable_trms a) ~f:(fun b -> + assert ( + let b_use = + Trm.Map.find b x.use |> Option.value ~default:Use.empty + in + Use.mem a b_use + || fail "@[subterm %a@ of %a@ not in use %a@]" Trm.pp b Trm.pp + a Use.pp b_use () ) ) ) ; + Trm.Map.iteri x.cls ~f:(fun ~key:a' ~data:cls -> + (* each class does not include its rep *) + assert ( + (not (Trm.Set.mem a' (Cls.to_set cls))) + || fail "rep %a in cls %a" Trm.pp a' Cls.pp cls () ) ; + (* rep of every element in class of [a'] is [a'] *) + Iter.iter (Cls.to_iter cls) ~f:(fun e -> + assert ( + let e' = find_check e x in + Trm.equal e' a' + || fail "rep of %a = %a but should = %a, cls: %a" Trm.pp e + Trm.pp e' Trm.pp a' Cls.pp cls () ) ) ) ; + Trm.Map.iteri x.use ~f:(fun ~key:a ~data:use -> + (* dom of use are solvable terms *) + assert (Theory.is_noninterpreted a) ; + (* terms occur in each of their uses *) + Use.iter use ~f:(fun u -> + assert ( + Iter.mem ~eq:Trm.equal a (Theory.solvable_trms u) + || fail "%a does not occur in its use %a" Trm.pp a Trm.pp u () + ) ) ) + with exc -> + let bt = Printexc.get_raw_backtrace () in + [%Trace.info "%a" pp_raw x] ; + Printexc.raise_with_backtrace exc bt + +let invariant x = + let@ () = Invariant.invariant [%here] x [%sexp_of: t] in + assert (List.is_empty x.pnd) ; + pre_invariant x ; assert ( - (not r.sat) - || Subst.for_alli r.rep ~f:(fun ~key:a ~data:a' -> - Subst.for_alli r.rep ~f:(fun ~key:b ~data:b' -> + (not x.sat) + || Subst.for_alli x.rep ~f:(fun ~key:a ~data:a' -> + Subst.for_alli x.rep ~f:(fun ~key:b ~data:b' -> Trm.compare a b >= 0 - || (not (congruent r a b)) + || (not (congruent x a b)) || Trm.equal a' b' - || fail "not congruent %a@ %a@ in@ %a" Trm.pp a Trm.pp b pp r + || fail "not congruent %a@ %a@ in@ %a" Trm.pp a Trm.pp b pp x () ) ) ) +(* Representation queries =================================================*) + +(** [norm0 s a = norm0 s b] if [a] and [b] are equal in [s], that is, + congruent using 0 applications of the congruence rule. *) +let norm0 s a = Subst.apply s a + +(** [norm1 s a = norm1 s b] if [a] and [b] are congruent in [s] using 0 or 1 + application of the congruence rule. *) +let norm1 s a = + match Theory.classify a with + | InterpAtom -> a + | NonInterpAtom -> norm0 s a + | InterpApp | UninterpApp -> ( + match Trm.Map.find a s with + | Some a' -> a' + | None -> + let a_norm = Trm.map ~f:(Theory.map_solvables ~f:(norm0 s)) a in + if a_norm == a then a_norm else norm0 s a_norm ) + +(** rewrite a term into canonical form using rep recursively *) +let rec canon x a = + match Theory.classify a with + | InterpAtom -> a + | NonInterpAtom -> norm0 x.rep a + | InterpApp | UninterpApp -> ( + match Trm.Map.find a x.rep with + | Some a' -> a' + | None -> + let a_can = Trm.map ~f:(Theory.map_solvables ~f:(canon x)) a in + if a_can == a then a_can else norm0 x.rep a_can ) + (* Extending the carrier ==================================================*) -let rec norm_extend_ a x = +let add_to_cls elt rep cls = + Trm.Map.update rep cls ~f:(fun elts0 -> + Cls.add elt (Option.value elts0 ~default:Cls.empty) ) + +let add_use_of sup sub use = + Trm.Map.update sub use ~f:(fun u -> + Use.add sup (Option.value ~default:Use.empty u) ) + +let add_uses_of a use = + Iter.fold ~f:(add_use_of a) (Theory.solvable_trms a) use + +let add_eq v ~rep:r x = [%trace] - ~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a pp_raw x) + ~call:(fun {pf} -> pf "@ @[%a ↦ %a@]@ %a" Trm.pp v Trm.pp r pp_raw x) + ~retn:(fun {pf} (_, x') -> pf "%a" pp_raw x') + @@ fun () -> + match Trm.Map.find_or_add v r x.rep with + | `Found v' -> + (* v ↦ v' already, so v' and r are congruent but not (yet) equal, + therefore add pending v' = r *) + let pnd = (v', r) :: x.pnd in + (v', {x with pnd}) + | `Added rep -> + (* v ↦ r newly added, so can directly add v = r *) + let cls = add_to_cls v r x.cls in + let use = add_uses_of v x.use in + (r, {x with rep; cls; use}) + +(** [find_extend_ a x] is [a', x'] where [x'] is [x] extended so that + [a' = find_exn a x']. This adds [a] and all its subterms, normalizes [a] + to [a'], and uses the result to find equalities needed to reestablish + congruence closure. *) +let rec find_extend_ a x = + [%trace] + ~call:(fun {pf} -> pf "@ %a@ | %a" Trm.pp a pp_raw x) ~retn:(fun {pf} (a', x') -> pf "%a@ %a" Trm.pp a' pp_diff (x, x') ; - assert (Trm.equal a' (Subst.norm x'.rep a)) ) + assert (Trm.equal a' (find_check a x')) ) @@ fun () -> - if Theory.is_noninterpreted a then - (* add noninterpreted terms *) + match Theory.classify a with + | InterpAtom -> (a, x) + | NonInterpAtom -> ( match Trm.Map.find_or_add a a x.rep with | `Found a' -> (a', x) - | `Added rep -> - (* and their subterms if newly added *) - let x = {x with rep} in - let a', x = Trm.fold_map ~f:norm_extend_ a x in + | `Added rep -> (a, {x with rep}) ) + | InterpApp -> + if Trm.Map.mem a x.rep then (a, x) + else Trm.fold_map ~f:find_extend_ a x + | UninterpApp -> ( + match Trm.Map.find_or_add a a x.rep with + | `Found a' -> + (* a already has rep a' *) (a', x) - else - (* add subterms of interpreted terms *) - Trm.fold_map ~f:norm_extend_ a x - -let norm_extend a x = + | `Added rep -> + (* a now its own rep *) + let use = add_uses_of a x.use in + let x = {x with rep; use} in + (* add subterms and norm a using (old) reps *) + let a_norm, x = Trm.fold_map ~f:find_extend_ a x in + if Trm.equal a_norm a then (* a already normalized *) + (a_norm, x) + else add_eq a_norm ~rep:a x ) + +let find_extend a x = [%trace] ~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a pp_raw x) - ~retn:(fun {pf} (a', x') -> - pf "%a@ %a" Trm.pp a' pp_diff (x, x') ; - pre_invariant x' ; - assert (Trm.equal a' (Subst.norm x'.rep a)) ) - @@ fun () -> norm_extend_ a x + ~retn:(fun {pf} (a', x') -> pf "%a@ %a" Trm.pp a' pp_diff (x, x')) + @@ fun () -> find_extend_ a x (** add a term to the carrier *) let extend a x = [%trace] - ~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a pp x) + ~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 () -> snd (norm_extend a x) + @@ fun () -> snd (find_extend a x) (* Propagation ============================================================*) -(** add a=a' to x using a' as the representative *) -let propagate1 (a, a') x = +let move_cls_to_rep a_cls a' rep = + Cls.fold a_cls rep ~f:(fun e rep -> Trm.Map.add ~key:e ~data:a' rep) + +let find_and_move_cls noninterp ~of_:u ~to_:u' cls = + let u_cls, cls = + Trm.Map.find_and_remove u cls |> Option.value ~default:(Cls.empty, cls) + in + let u_cls = if noninterp then Cls.add u u_cls else u_cls in + let cls = + Trm.Map.update u' cls ~f:(fun u'_cls -> + Cls.union u_cls (Option.value u'_cls ~default:Cls.empty) ) + in + (u_cls, cls) + +let move_uses ~rem:f ~add:t use = + let f_trms = Theory.solvable_trms f |> Trm.Set.of_iter in + let t_trms = Theory.solvable_trms t |> Trm.Set.of_iter in + let f_trms, ft_trms, t_trms = Trm.Set.diff_inter_diff f_trms t_trms in + (* remove f from use of each of its subterms not shared with t *) + let use = + Trm.Set.fold f_trms use ~f:(fun e use -> + Trm.Map.change e use ~f:(function + | Some e_use -> + let e_use' = Use.remove f e_use in + if Use.is_empty e_use' then None else Some e_use' + | None -> assert false ) ) + in + (* move each subterm of both f and t from a use of f to a use of t *) + let use = + Trm.Set.fold ft_trms use ~f:(fun e use -> + Trm.Map.update e use ~f:(function + | Some e_use -> Use.add t (Use.remove f e_use) + | None -> assert false ) ) + in + (* add t to use of each of its subterms not shared with f *) + let use = + Trm.Set.fold t_trms use ~f:(fun e use -> + Trm.Map.update e use ~f:(fun e_use -> + Use.add t (Option.value e_use ~default:Use.empty) ) ) + in + use + +let update_rep noninterp ~from:r ~to_:r' x = + [%trace] + ~call:(fun {pf} -> pf "@ @[%a ↦ %a@]@ %a" Trm.pp r Trm.pp r' pp_raw x) + ~retn:(fun {pf} x' -> pf "%a" pp_diff (x, x')) + @@ fun () -> + let r_cls, cls = find_and_move_cls noninterp ~of_:r ~to_:r' x.cls in + let rep = move_cls_to_rep r_cls r' x.rep in + let use = + if Trm.Map.mem r rep then add_uses_of r' x.use + else move_uses ~rem:r ~add:r' x.use + in + {x with rep; cls; use} + +(** add v ↦ t to x *) +let propagate1 (v, t) x = [%trace] - ~call:(fun {pf} -> pf "@ @[%a ↦ %a@]@ %a" Trm.pp a Trm.pp a' pp_raw x) + ~call:(fun {pf} -> + pf "@ @[%a ↦ %a@]@ %a" Trm.pp v Trm.pp t pp_raw x ; + (* v should be a solvable term that is a representative or absent *) + assert (Theory.is_noninterpreted v) ; + assert ( + match Trm.Map.find v x.rep with + | Some v' -> Trm.equal v v' + | None -> true ) ; + (* while t may be an interpreted term and may not be in the carrier, + it should already be normalized *) + assert (Trm.equal t (norm1 x.rep t)) ) ~retn:(fun {pf} -> pf "%a" pp_raw) @@ fun () -> - (* 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_noninterpreted b0' then (Cls.add b0' b0'_cls, x.pnd) - else (b0'_cls, (b0', b') :: 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 s = Trm.Map.singleton v t in + let v_use = Trm.Map.find v x.use |> Option.value ~default:Use.empty in + let x = update_rep true ~from:v ~to_:t x in + Use.fold v_use x ~f:(fun u x -> + let w = norm1 s u in + let x = {x with pnd= (u, w) :: x.pnd} in + if Theory.is_noninterpreted u then + if in_car w x then x else {x with use= add_uses_of w x.use} + else update_rep false ~from:u ~to_:w x ) let solve ~wrt ~xs d e pending = [%trace] @@ -472,124 +650,65 @@ let solve ~wrt ~xs d e pending = let rec propagate ~wrt x = [%trace] ~call:(fun {pf} -> pf "@ %a" pp_raw x) - ~retn:(fun {pf} -> pf "%a" pp_raw) + ~retn:(fun {pf} x' -> pf "%a" pp_diff (x, x')) @@ fun () -> match x.pnd with | (a, b) :: pnd -> ( let a' = Subst.norm x.rep a in let b' = Subst.norm x.rep b in - match solve ~wrt ~xs:x.xs a' b' pnd with - | {solved= Some solved; wrt; fresh; pending} -> - let xs = Var.Set.union x.xs fresh in - let x = {x with xs; pnd= pending} in - propagate ~wrt (List.fold ~f:propagate1 solved x) - | {solved= None} -> {x with sat= false; pnd= []} ) + if Trm.equal a' b' then propagate ~wrt {x with pnd} + else + match solve ~wrt ~xs:x.xs a' b' pnd with + | {solved= Some solved; wrt; fresh; pending} -> + let xs = Var.Set.union x.xs fresh in + let x = {x with xs; pnd= pending} in + propagate ~wrt (List.fold ~f:propagate1 solved x) + | {solved= None} -> {x with sat= false; pnd= []} ) | [] -> x (* Core operations ========================================================*) let empty = let rep = Subst.empty in - {xs= Var.Set.empty; sat= true; rep; cls= Trm.Map.empty; pnd= []} + { xs= Var.Set.empty + ; sat= true + ; rep + ; cls= Trm.Map.empty + ; use= Trm.Map.empty + ; pnd= [] } |> check invariant let unsat = {empty with sat= false} -(** [lookup r a] is [b'] if [a ~ b = b'] for some equation [b = b'] in rep *) -let lookup r a = - ([%Trace.call fun {pf} -> pf "@ %a" Trm.pp a] - ; - Iter.find_map (Subst.to_iter r.rep) ~f:(fun (b, b') -> - Option.return_if (semi_congruent r a b) b' ) - |> Option.value ~default:a) - |> - [%Trace.retn fun {pf} -> pf "%a" Trm.pp] - -(** rewrite a term into canonical form using rep and, for noninterpreted - terms, congruence composed with rep *) -let rec canon r a = - [%Trace.call fun {pf} -> pf "@ %a" Trm.pp a] - ; - ( match Theory.classify a with - | InterpAtom -> a - | NonInterpAtom -> Subst.apply r.rep a - | InterpApp -> Trm.map ~f:(canon r) a - | UninterpApp -> ( - let a' = Trm.map ~f:(canon r) a in - match Theory.classify a' with - | InterpAtom | InterpApp -> a' - | NonInterpAtom -> Subst.apply r.rep a' - | UninterpApp -> lookup r a' ) ) - |> - [%Trace.retn fun {pf} -> pf "%a" Trm.pp] - let canon_f r b = [%trace] - ~call:(fun {pf} -> pf "@ %a@ %a" Fml.pp b pp_raw r) + ~call:(fun {pf} -> pf "@ %a@ | %a" Fml.pp b pp_raw r) ~retn:(fun {pf} -> pf "%a" Fml.pp) @@ fun () -> Fml.map_trms ~f:(canon r) b let merge ~wrt a b x = [%trace] - ~call:(fun {pf} -> pf "@ %a@ %a@ %a" Trm.pp a Trm.pp b pp x) + ~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' ) + invariant 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 = - Iter.find_map (Subst.to_iter r.rep) ~f:(fun (a, a') -> - let a_subnorm = Trm.map ~f:(Subst.norm r.rep) a in - Iter.find_map (Subst.to_iter r.rep) ~f:(fun (b, b') -> - (* need to equate a' and b'? *) - let need_a'_eq_b' = - (* optimize: do not consider both a = b and b = a *) - Trm.compare a b < 0 - (* a and b are not already equal *) - && (not (Trm.equal a' b')) - (* a and b are congruent *) - && semi_congruent r a_subnorm b - in - Option.return_if need_a'_eq_b' (a', b') ) ) - -let rec close ~wrt x = - if not x.sat then x - else - match find_missing x with - | Some (a', b') -> close ~wrt (merge ~wrt a' b' x) - | None -> x - -let close ~wrt r = - [%Trace.call fun {pf} -> pf "@ %a" pp r] - ; - close ~wrt r - |> - [%Trace.retn fun {pf} r' -> - pf "%a" pp_diff (r, r') ; - invariant r'] - let and_eq_ ~wrt a b x = [%trace] - ~call:(fun {pf} -> pf "@ @[%a = %a@]@ %a" Trm.pp a Trm.pp b pp x) + ~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 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 x = merge ~wrt a' b' x in - match (a, b) with - | (Var _ as v), _ when not (in_car x0 v) -> x - | _, (Var _ as v) when not (in_car x0 v) -> x - | _ -> close ~wrt x + let x = extend a' (extend b' x) in + if Trm.equal a' b' then x else merge ~wrt a' b' x let extract_xs r = (r.xs, {r with xs= Var.Set.empty}) @@ -601,7 +720,7 @@ let is_empty {sat; rep} = let is_unsat {sat} = not sat let implies r b = - [%Trace.call fun {pf} -> pf "@ %a@ %a" Fml.pp b pp r] + [%Trace.call fun {pf} -> pf "@ %a@ | %a" Fml.pp b pp r] ; Fml.equal Fml.tt (canon_f r b) |> @@ -611,7 +730,7 @@ let refutes r b = Fml.equal Fml.ff (canon_f r b) let normalize x a = [%trace] - ~call:(fun {pf} -> pf "@ %a@ %a" Term.pp a pp x) + ~call:(fun {pf} -> pf "@ %a@ | %a" Term.pp a pp x) ~retn:(fun {pf} -> pf "%a" Term.pp) @@ fun () -> Term.map_trms ~f:(canon x) a @@ -658,7 +777,8 @@ let apply_subst wrt s r = ; ( if Subst.is_empty s then r else - Trm.Map.fold r.cls {r with rep= Subst.empty; cls= Trm.Map.empty} + Trm.Map.fold r.cls + {r with rep= Subst.empty; cls= Trm.Map.empty; use= Trm.Map.empty} ~f:(fun ~key:rep ~data:cls r -> let rep' = Subst.apply_rec s rep in Cls.fold cls r ~f:(fun trm r -> @@ -729,7 +849,7 @@ let rec add_ wrt b r = | Pos _ | Not _ | Or _ | Iff _ | Cond _ | Lit _ -> r let add us b r = - [%Trace.call fun {pf} -> pf "@ %a@ %a" Fml.pp b pp r] + [%Trace.call fun {pf} -> pf "@ %a@ | %a" Fml.pp b pp r] ; add_ us b r |> extract_xs |> @@ -763,7 +883,15 @@ let rename x sub = Trm.Map.add ~key:a' ~data:a'_cls (if a' == a0' then cls else Trm.Map.remove a0' cls) ) in - if rep == x.rep && cls == x.cls then x else {x with rep; cls} + let use = + Trm.Map.fold x.use x.use ~f:(fun ~key:a0' ~data:a0'_use use -> + let a' = apply_sub a0' in + let a'_use = Use.map a0'_use ~f:apply_sub in + Trm.Map.add ~key:a' ~data:a'_use + (if a' == a0' then use else Trm.Map.remove a0' use) ) + in + if rep == x.rep && cls == x.cls && use == x.use then x + else {x with rep; cls; use} let trivial vs r = [%trace] diff --git a/sledge/src/test/context_test.ml b/sledge/src/test/context_test.ml index 17b2acbe0..38ced39c6 100644 --- a/sledge/src/test/context_test.ml +++ b/sledge/src/test/context_test.ml @@ -18,7 +18,7 @@ let%test_module _ = * ~config: * (Result.get_ok * (Trace.parse - * "+Context-Context.canon-Context.canon_f-Context.norm")) + * "+Context-Context.canon-Context.canon_f-Context.norm-Context.find_extend_")) * () *) [@@@warning "-32"] @@ -61,22 +61,30 @@ let%test_module _ = pp r3 ; [%expect {| - %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %v_3) - = g(%y_6, %z_7) + %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %t_1) + = g(%y_6, %u_2) = g(%y_6, %v_3) = g(%y_6, %z_7) - {sat= true; - rep= [[%t_1 ↦ ]; - [%u_2 ↦ %t_1]; - [%v_3 ↦ %t_1]; - [%w_4 ↦ %t_1]; - [%x_5 ↦ %t_1]; - [%y_6 ↦ ]; - [%z_7 ↦ %t_1]; - [g(%y_6, %v_3) ↦ %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)}]]} |}] + { sat= true; + rep= [[%t_1 ↦ ]; + [%u_2 ↦ %t_1]; + [%v_3 ↦ %t_1]; + [%w_4 ↦ %t_1]; + [%x_5 ↦ %t_1]; + [%y_6 ↦ ]; + [%z_7 ↦ %t_1]; + [g(%y_6, %t_1) ↦ %t_1]; + [g(%y_6, %u_2) ↦ %t_1]; + [g(%y_6, %v_3) ↦ %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, %t_1), + g(%y_6, %u_2), g(%y_6, %v_3), g(%y_6, %z_7)}]]; + use= [[%t_1 ↦ g(%y_6, %t_1)]; + [%u_2 ↦ g(%y_6, %u_2)]; + [%v_3 ↦ g(%y_6, %v_3)]; + [%y_6 ↦ g(%y_6, %t_1), g(%y_6, %u_2), g(%y_6, %v_3), + g(%y_6, %z_7)]; + [%z_7 ↦ g(%y_6, %z_7)]] } |}] let%test _ = implies_eq r3 t z @@ -87,60 +95,193 @@ let%test_module _ = pp r15 ; [%expect {| - {sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]} |}] + { sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]; use= [] } |}] let%test _ = implies_eq r15 (Term.neg b) (Term.apply (Signed 1) [|!1|]) let%test _ = implies_eq r15 (Term.apply (Unsigned 1) [|b|]) !1 let%expect_test _ = replay - {|(Solve_for_vars - (() - ((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))) - ()) + {|(Dnf + (Eq (Sized (seq (Var (id 1) (name a))) (siz (Z 8))) + (Concat + ((Sized (seq (Var (id 3) (name c))) (siz (Z 4))) + (Sized (seq (Var (id 2) (name b))) (siz (Z 4)))))))|} ; + [%expect {| |}] + + let%expect_test _ = + replay + {|(Union + ((Var (id 1) (name a)) (Var (id 2) (name a)) (Var (id 3) (name a)) + (Var (id 6) (name l)) (Var (id 7) (name a1))) ((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))))) + (((Var (id 7) (name a1)) (Var (id 2) (name a))) + ((Var (id 2) (name a)) (Var (id 2) (name a))))) + (cls (((Var (id 2) (name a)) ((Var (id 7) (name a1)))))) (use ()) + (pnd ())) + ((xs ()) (sat true) + (rep + (((Var (id 7) (name a1)) (Var (id 7) (name a1))) + ((Var (id 3) (name a)) + (Concat + ((Sized (seq (Var (id 1) (name a))) (siz (Z 8))) + (Sized (seq (Var (id 7) (name a1))) (siz (Z 8)))))) + ((Var (id 1) (name a)) (Var (id 1) (name a))))) (cls - (((Var (id 0) (name 0)) - ((Var (id 0) (name 2)) (Var (id 0) (name 4)) - (Var (id 0) (name 2)))))) + (((Concat + ((Sized (seq (Var (id 1) (name a))) (siz (Z 8))) + (Sized (seq (Var (id 7) (name a1))) (siz (Z 8))))) + ((Var (id 3) (name a)))))) + (use + (((Var (id 7) (name a1)) + ((Concat + ((Sized (seq (Var (id 1) (name a))) (siz (Z 8))) + (Sized (seq (Var (id 7) (name a1))) (siz (Z 8))))))) + ((Var (id 1) (name a)) + ((Concat + ((Sized (seq (Var (id 1) (name a))) (siz (Z 8))) + (Sized (seq (Var (id 7) (name a1))) (siz (Z 8))))))))) (pnd ())))|} ; [%expect {| |}] let%expect_test _ = replay - {|(Dnf - (Eq0 - (Arith - (((((Var (id 0) (name 11)) 1) ((Var (id 0) (name 12)) 1)) 1) - ((((Var (id 11) (name a)) 1)) -1)))))|} ; + {|(Union + ((Var (id 0) (name 1)) (Var (id 0) (name 4)) (Var (id 0) (name 6)) + (Var (id 0) (name 8)) (Var (id 0) (name freturn)) + (Var (id 1) (name freturn))) + ((xs ()) (sat true) + (rep + (((Apply (Signed 8) ((Var (id 0) (name 8)))) + (Var (id 0) (name freturn))) + ((Var (id 0) (name freturn)) (Var (id 0) (name freturn))) + ((Var (id 0) (name 8)) (Var (id 0) (name 8))))) + (cls + (((Var (id 0) (name freturn)) + ((Apply (Signed 8) ((Var (id 0) (name 8)))))))) + (use + (((Var (id 0) (name 8)) ((Apply (Signed 8) ((Var (id 0) (name 8)))))))) + (pnd ())) + ((xs ()) (sat true) + (rep + (((Apply (Uninterp .str) ()) (Var (id 0) (name 6))) + ((Var (id 0) (name 8)) (Z 73)) + ((Var (id 0) (name 6)) (Var (id 0) (name 6))))) + (cls + (((Z 73) ((Var (id 0) (name 8)))) + ((Var (id 0) (name 6)) ((Apply (Uninterp .str) ()))))) + (use ()) (pnd ())))|} ; + [%expect {||}] + + let%expect_test _ = + replay + {|(Apply_and_elim + ((Var (id 0) (name 12)) (Var (id 0) (name 16)) (Var (id 0) (name 19)) + (Var (id 0) (name 22)) (Var (id 0) (name 23)) (Var (id 0) (name 26)) + (Var (id 0) (name 29)) (Var (id 0) (name 33)) (Var (id 0) (name 35)) + (Var (id 0) (name 39)) (Var (id 0) (name 4)) (Var (id 0) (name 40)) + (Var (id 0) (name 41)) (Var (id 0) (name 47)) (Var (id 0) (name 5)) + (Var (id 0) (name 52)) (Var (id 0) (name 8)) (Var (id 1) (name m)) + (Var (id 2) (name a)) (Var (id 6) (name b))) + ((Var (id 1) (name m)) (Var (id 2) (name a)) (Var (id 6) (name b))) + (((Var (id 6) (name b)) (Var (id 2) (name a))) + ((Var (id 1) (name m)) + (Apply (Signed 32) + ((Apply (Signed 32) ((Arith (((((Var (id 0) (name 23)) 1)) 4))))))))) + ((xs ()) (sat true) + (rep + (((Apply (Signed 32) + ((Apply (Signed 32) ((Arith (((((Var (id 0) (name 23)) 1)) 4))))))) + (Var (id 1) (name m))) + ((Apply (Signed 32) ((Arith (((((Var (id 0) (name 23)) 1)) 4))))) + (Apply (Signed 32) ((Arith (((((Var (id 0) (name 23)) 1)) 4)))))) + ((Apply (Signed 32) ((Var (id 0) (name 5)))) + (Arith ((() -1) ((((Var (id 0) (name 23)) 1)) 1)))) + ((Var (id 6) (name b)) (Var (id 2) (name a))) + ((Var (id 2) (name a)) (Var (id 2) (name a))) + ((Var (id 1) (name m)) (Var (id 1) (name m))) + ((Var (id 0) (name 8)) + (Arith ((() -1) ((((Var (id 0) (name 23)) 1)) 1)))) + ((Var (id 0) (name 52)) (Var (id 0) (name 26))) + ((Var (id 0) (name 5)) (Var (id 0) (name 5))) + ((Var (id 0) (name 35)) (Var (id 0) (name 23))) + ((Var (id 0) (name 33)) (Z 0)) + ((Var (id 0) (name 26)) (Var (id 0) (name 26))) + ((Var (id 0) (name 23)) (Var (id 0) (name 23))) + ((Var (id 0) (name 22)) (Var (id 0) (name 22))) + ((Var (id 0) (name 19)) + (Arith ((() -1) ((((Var (id 0) (name 23)) 1)) 1)))) + ((Var (id 0) (name 16)) + (Arith ((() -1) ((((Var (id 0) (name 23)) 1)) 1)))))) + (cls + (((Arith ((() -1) ((((Var (id 0) (name 23)) 1)) 1))) + ((Var (id 0) (name 16)) (Var (id 0) (name 8)) + (Var (id 0) (name 19)) + (Apply (Signed 32) ((Var (id 0) (name 5)))))) + ((Z 0) ((Var (id 0) (name 33)))) + ((Var (id 2) (name a)) ((Var (id 6) (name b)))) + ((Var (id 1) (name m)) + ((Apply (Signed 32) + ((Apply (Signed 32) + ((Arith (((((Var (id 0) (name 23)) 1)) 4))))))))) + ((Var (id 0) (name 26)) ((Var (id 0) (name 52)))) + ((Var (id 0) (name 23)) ((Var (id 0) (name 35)))))) + (use + (((Apply (Signed 32) ((Arith (((((Var (id 0) (name 23)) 1)) 4))))) + ((Apply (Signed 32) + ((Apply (Signed 32) + ((Arith (((((Var (id 0) (name 23)) 1)) 4))))))))) + ((Var (id 0) (name 5)) + ((Apply (Signed 32) ((Var (id 0) (name 5)))))) + ((Var (id 0) (name 23)) + ((Arith ((() -1) ((((Var (id 0) (name 23)) 1)) 1))) + (Apply (Signed 32) + ((Arith (((((Var (id 0) (name 23)) 1)) 4))))))))) + (pnd ())))|} ; [%expect {| |}] let%expect_test _ = replay - {|(Normalize + {|(Add () (Eq (Var (id 2) (name u)) (Var (id 5) (name x))) ((xs ()) (sat true) (rep - (((Var (id 7) (name 16)) (Z 8)) ((Var (id 0) (name 8)) (Q 3/2)) - ((Var (id 0) (name 17)) (Z 3)) ((Var (id 0) (name 12)) (Z 8)) - ((Var (id 0) (name 11)) (Z 8)) - ((Var (id 0) (name 10)) (Var (id 0) (name 10))) - ((Var (id 0) (name 1)) (Z 3)) ((Var (id 0) (name 0)) (Z 8)))) + (((Apply (Uninterp g) ((Var (id 6) (name y)) (Var (id 7) (name z)))) + (Var (id 3) (name v))) + ((Apply (Uninterp g) ((Var (id 6) (name y)) (Var (id 3) (name v)))) + (Var (id 1) (name t))) + ((Var (id 7) (name z)) (Var (id 7) (name z))) + ((Var (id 6) (name y)) (Var (id 6) (name y))) + ((Var (id 5) (name x)) (Var (id 3) (name v))) + ((Var (id 4) (name w)) (Var (id 3) (name v))) + ((Var (id 3) (name v)) (Var (id 3) (name v))) + ((Var (id 1) (name t)) (Var (id 1) (name t))))) (cls - (((Q 3/2) ((Var (id 0) (name 8)))) - ((Z 8) - ((Var (id 0) (name 12)) (Var (id 0) (name 0)) - (Var (id 7) (name 16)) (Var (id 0) (name 11)))) - ((Z 3) ((Var (id 0) (name 17)) (Var (id 0) (name 1)))))) - (pnd ())) - (Trm - (Arith (((((Var (id 0) (name 11)) 1) ((Var (id 0) (name 12)) 1)) 1)))))|} ; + (((Var (id 3) (name v)) + ((Var (id 5) (name x)) + (Apply (Uninterp g) + ((Var (id 6) (name y)) (Var (id 7) (name z)))) + (Var (id 4) (name w)))) + ((Var (id 1) (name t)) + ((Apply (Uninterp g) + ((Var (id 6) (name y)) (Var (id 3) (name v)))))))) + (use + (((Var (id 7) (name z)) + ((Apply (Uninterp g) + ((Var (id 6) (name y)) (Var (id 7) (name z)))))) + ((Var (id 6) (name y)) + ((Apply (Uninterp g) + ((Var (id 6) (name y)) (Var (id 3) (name v)))) + (Apply (Uninterp g) + ((Var (id 6) (name y)) (Var (id 7) (name z)))))) + ((Var (id 3) (name v)) + ((Apply (Uninterp g) + ((Var (id 6) (name y)) (Var (id 3) (name v)))))))) + (pnd ())))|} ; [%expect {| |}] + + (* let%expect_test _ = + * replay + * {||} ; + * [%expect {| |}] *) end ) diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml index 2bfefd25b..e260c4384 100644 --- a/sledge/src/test/fol_test.ml +++ b/sledge/src/test/fol_test.ml @@ -69,7 +69,7 @@ let%test_module _ = let%expect_test _ = pp_raw f1 ; - [%expect {| {sat= false; rep= []; cls= []} |}] + [%expect {| { sat= false; rep= []; cls= []; use= [] } |}] let%test _ = is_unsat (add_eq !1 !1 f1) @@ -79,7 +79,7 @@ let%test_module _ = let%expect_test _ = pp_raw f2 ; - [%expect {| {sat= false; rep= []; cls= []} |}] + [%expect {| { sat= false; rep= []; cls= []; use= [] } |}] let f3 = of_eqs [(x + !0, x + !1)] @@ -87,7 +87,7 @@ let%test_module _ = let%expect_test _ = pp_raw f3 ; - [%expect {| {sat= false; rep= []; cls= []} |}] + [%expect {| { sat= false; rep= []; cls= []; use= [] } |}] let f4 = of_eqs [(x, y); (x + !0, y + !1)] @@ -97,9 +97,10 @@ let%test_module _ = pp_raw f4 ; [%expect {| - {sat= false; - rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]; - cls= [[%x_5 ↦ {%y_6}]]} |}] + { sat= false; + rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]; + cls= [[%x_5 ↦ {%y_6}]]; + use= [] } |}] let t1 = of_eqs [(!1, !1)] @@ -115,7 +116,7 @@ let%test_module _ = let%expect_test _ = pp_raw r0 ; - [%expect {| {sat= true; rep= []; cls= []} |}] + [%expect {| { sat= true; rep= []; cls= []; use= [] } |}] let%expect_test _ = pp r0 ; @@ -134,7 +135,10 @@ let%test_module _ = %x_5 = %y_6 - {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]; cls= [[%x_5 ↦ {%y_6}]]} |}] + { sat= true; + rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]; + cls= [[%x_5 ↦ {%y_6}]]; + use= [] } |}] let%test _ = implies_eq r1 x y @@ -147,9 +151,10 @@ let%test_module _ = {| %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]]; - cls= [[%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]]; + cls= [[%x_5 ↦ {%y_6, %z_7, f(%x_5)}]]; + use= [[%x_5 ↦ f(%x_5)]] } |}] let%test _ = implies_eq r2 x z let%test _ = implies_eq (inter r1 r2) x y @@ -170,15 +175,20 @@ let%test_module _ = pp_raw rs ; [%expect {| - {sat= true; - rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]; - cls= [[%w_4 ↦ {%y_6, %z_7}]]} + { sat= true; + rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]; + cls= [[%w_4 ↦ {%y_6, %z_7}]]; + use= [] } - {sat= true; - rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]; - cls= [[%x_5 ↦ {%y_6, %z_7}]]} + { sat= true; + rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]; + cls= [[%x_5 ↦ {%y_6, %z_7}]]; + use= [] } - {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]; cls= [[%y_6 ↦ {%z_7}]]} |}] + { sat= true; + rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]; + cls= [[%y_6 ↦ {%z_7}]]; + use= [] } |}] let%test _ = let r = of_eqs [(w, y); (y, z)] in @@ -193,22 +203,30 @@ let%test_module _ = pp_raw r3 ; [%expect {| - %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]; - [%v_3 ↦ %t_1]; - [%w_4 ↦ %t_1]; - [%x_5 ↦ %t_1]; - [%y_6 ↦ ]; - [%z_7 ↦ %t_1]; - [g(%y_6, %v_3) ↦ %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)}]]} |}] + %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %t_1) + = g(%y_6, %u_2) = g(%y_6, %v_3) = g(%y_6, %z_7) + + { sat= true; + rep= [[%t_1 ↦ ]; + [%u_2 ↦ %t_1]; + [%v_3 ↦ %t_1]; + [%w_4 ↦ %t_1]; + [%x_5 ↦ %t_1]; + [%y_6 ↦ ]; + [%z_7 ↦ %t_1]; + [g(%y_6, %t_1) ↦ %t_1]; + [g(%y_6, %u_2) ↦ %t_1]; + [g(%y_6, %v_3) ↦ %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, %t_1), + g(%y_6, %u_2), g(%y_6, %v_3), g(%y_6, %z_7)}]]; + use= [[%t_1 ↦ g(%y_6, %t_1)]; + [%u_2 ↦ g(%y_6, %u_2)]; + [%v_3 ↦ g(%y_6, %v_3)]; + [%y_6 ↦ g(%y_6, %t_1), g(%y_6, %u_2), g(%y_6, %v_3), + g(%y_6, %z_7)]; + [%z_7 ↦ g(%y_6, %z_7)]] } |}] let%test _ = implies_eq r3 t z let%test _ = implies_eq r3 x z @@ -223,14 +241,15 @@ let%test_module _ = {| (-4 + %z_7) = %y_6 ∧ (3 + %z_7) = %w_4 ∧ (8 + %z_7) = %x_5 - {sat= true; - rep= [[%w_4 ↦ (3 + %z_7)]; - [%x_5 ↦ (8 + %z_7)]; - [%y_6 ↦ (-4 + %z_7)]; - [%z_7 ↦ ]]; - cls= [[(-4 + %z_7) ↦ {%y_6}]; - [(3 + %z_7) ↦ {%w_4}]; - [(8 + %z_7) ↦ {%x_5}]]} |}] + { sat= true; + rep= [[%w_4 ↦ (3 + %z_7)]; + [%x_5 ↦ (8 + %z_7)]; + [%y_6 ↦ (-4 + %z_7)]; + [%z_7 ↦ ]]; + cls= [[(-4 + %z_7) ↦ {%y_6}]; + [(3 + %z_7) ↦ {%w_4}]; + [(8 + %z_7) ↦ {%x_5}]]; + use= [[%z_7 ↦ (-4 + %z_7), (3 + %z_7), (8 + %z_7)]] } |}] let%test _ = implies_eq r4 x (w + !5) let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5)) @@ -248,9 +267,10 @@ let%test_module _ = {| 1 = %x_5 = %y_6 - {sat= true; - rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]]; - cls= [[1 ↦ {%x_5, %y_6}]]} |}] + { sat= true; + rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]]; + cls= [[1 ↦ {%x_5, %y_6}]]; + use= [] } |}] let%test _ = implies_eq r6 x y @@ -263,13 +283,14 @@ let%test_module _ = {| %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]]; - cls= [[%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]]; + cls= [[%v_3 ↦ {%x_5}]; [%w_4 ↦ {%y_6, %z_7}]]; + use= [] } |}] let r7' = add_eq x z r7 @@ -280,13 +301,14 @@ let%test_module _ = {| %v_3 = %w_4 = %x_5 = %y_6 = %z_7 - {sat= true; - rep= [[%v_3 ↦ ]; - [%w_4 ↦ %v_3]; - [%x_5 ↦ %v_3]; - [%y_6 ↦ %v_3]; - [%z_7 ↦ %v_3]]; - cls= [[%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]]; + cls= [[%v_3 ↦ {%w_4, %x_5, %y_6, %z_7}]]; + use= [] } |}] let%test _ = normalize r7' w |> Term.equal v @@ -305,9 +327,10 @@ let%test_module _ = {| 14 = %y_6 ∧ 13×%z_7 = %x_5 - {sat= true; - rep= [[%x_5 ↦ 13×%z_7]; [%y_6 ↦ 14]; [%z_7 ↦ ]]; - cls= [[14 ↦ {%y_6}]; [13×%z_7 ↦ {%x_5}]]} |}] + { sat= true; + rep= [[%x_5 ↦ 13×%z_7]; [%y_6 ↦ 14]; [%z_7 ↦ ]]; + cls= [[14 ↦ {%y_6}]; [13×%z_7 ↦ {%x_5}]]; + use= [[%z_7 ↦ 13×%z_7]] } |}] let%test _ = implies_eq r8 y !14 @@ -318,13 +341,15 @@ let%test_module _ = pp_raw r9 ; [%expect {| - {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}]]} |}] + { sat= true; + rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]; + cls= [[(-16 + %z_7) ↦ {%x_5}]]; + use= [[%z_7 ↦ (-16 + %z_7)]] } + + { sat= true; + rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]; + cls= [[(-16 + %z_7) ↦ {%x_5}]]; + use= [[%z_7 ↦ (-16 + %z_7)]] } |}] let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8)) @@ -339,20 +364,22 @@ let%test_module _ = Format.printf "@.%a@." Term.pp (normalize r10 (x + !8 - z)) ; [%expect {| - {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}]]; + use= [[%z_7 ↦ (-16 + %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}]]; + use= [[%z_7 ↦ (-16 + %z_7)]] } (-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)) @@ -381,7 +408,11 @@ let%test_module _ = let%expect_test _ = pp_raw r13 ; [%expect - {| {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]; cls= [[%y_6 ↦ {%z_7}]]} |}] + {| + { sat= true; + rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]; + cls= [[%y_6 ↦ {%z_7}]]; + use= [] } |}] let%test _ = not (is_unsat r13) (* incomplete *) @@ -392,7 +423,7 @@ let%test_module _ = pp_raw r14 ; [%expect {| - {sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]} |}] + { sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]; use= [] } |}] let%test _ = implies_eq r14 a (Formula.inject Formula.tt) @@ -403,7 +434,7 @@ let%test_module _ = pp_raw r14 ; [%expect {| - {sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]} |}] + { sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]; use= [] } |}] let%test _ = implies_eq r14 a (Formula.inject Formula.tt) (* incomplete *) @@ -416,7 +447,7 @@ let%test_module _ = pp_raw r15 ; [%expect {| - {sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]} |}] + { sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]; use= [] } |}] (* f(x−1)−1=x+1, f(y)+1=y−1, y+1=x ⊢ false *) let r16 = @@ -426,14 +457,16 @@ let%test_module _ = pp_raw r16 ; [%expect {| - {sat= false; - rep= [[%x_5 ↦ (1 + %y_6)]; - [%y_6 ↦ ]; - [f(%y_6) ↦ (-2 + %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))}]]} |}] + { sat= false; + rep= [[%x_5 ↦ (1 + %y_6)]; + [%y_6 ↦ ]; + [f(%y_6) ↦ (-2 + %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))}]]; + use= [[%x_5 ↦ f((-1 + %x_5))]; + [%y_6 ↦ (-2 + %y_6), (1 + %y_6), (3 + %y_6), f(%y_6)]] } |}] let%test _ = is_unsat r16 @@ -444,12 +477,13 @@ let%test_module _ = pp_raw r17 ; [%expect {| - {sat= false; - rep= [[%x_5 ↦ ]; - [%y_6 ↦ %x_5]; - [f(%x_5) ↦ %x_5]; - [f(%y_6) ↦ (-1 + %x_5)]]; - cls= [[%x_5 ↦ {%y_6, f(%x_5)}]; [(-1 + %x_5) ↦ {f(%y_6)}]]} |}] + { sat= false; + rep= [[%x_5 ↦ ]; + [%y_6 ↦ %x_5]; + [f(%x_5) ↦ %x_5]; + [f(%y_6) ↦ (-1 + %x_5)]]; + cls= [[%x_5 ↦ {%y_6, f(%x_5)}]; [(-1 + %x_5) ↦ {f(%y_6)}]]; + use= [[%x_5 ↦ (-1 + %x_5), f(%x_5)]; [%y_6 ↦ f(%y_6)]] } |}] let%test _ = is_unsat r17 @@ -459,13 +493,14 @@ let%test_module _ = pp r18 ; [%expect {| - {sat= true; - rep= [[%x_5 ↦ ]; - [%y_6 ↦ ]; - [f(%x_5) ↦ %x_5]; - [f(%y_6) ↦ (-1 + %y_6)]]; - cls= [[%x_5 ↦ {f(%x_5)}]; [(-1 + %y_6) ↦ {f(%y_6)}]]} - + { sat= true; + rep= [[%x_5 ↦ ]; + [%y_6 ↦ ]; + [f(%x_5) ↦ %x_5]; + [f(%y_6) ↦ (-1 + %y_6)]]; + cls= [[%x_5 ↦ {f(%x_5)}]; [(-1 + %y_6) ↦ {f(%y_6)}]]; + use= [[%x_5 ↦ f(%x_5)]; [%y_6 ↦ (-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)] @@ -474,9 +509,10 @@ let%test_module _ = pp_raw r19 ; [%expect {| - {sat= true; - rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]]; - cls= [[0 ↦ {%x_5, %y_6, %z_7}]]} |}] + { sat= true; + rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]]; + cls= [[0 ↦ {%x_5, %y_6, %z_7}]]; + use= [] } |}] 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 ec92bde32..279a6b124 100644 --- a/sledge/src/test/sh_test.ml +++ b/sledge/src/test/sh_test.ml @@ -79,9 +79,9 @@ let%test_module _ = [%expect {| ∃ %x_7 . emp - + 0 = %x_7 ∧ emp - + 0 = %x_7 ∧ emp |}] let%expect_test _ = @@ -99,7 +99,7 @@ let%test_module _ = [%expect {| ( ( 0 = %x_7 ∧ emp) ∨ ( ( ( 1 = %y_8 ∧ emp) ∨ ( emp) )) ) - + ( (∃ %x_7, %x_8 . 2 = %x_8 ∧ (2 = %x_8) ∧ emp) ∨ (∃ %x_7 . 1 = %x_7 = %y_8 ∧ ((1 = %x_7) ∧ (1 = %y_8)) ∧ emp) ∨ ( 0 = %x_7 ∧ (0 = %x_7) ∧ emp) @@ -122,7 +122,7 @@ let%test_module _ = [%expect {| ( ( emp) ∨ ( ( ( 1 = %y_8 ∧ emp) ∨ ( emp) )) ) - + ( (∃ %x_7, %x_9, %x_10 . 2 = %x_10 ∧ (2 = %x_10) ∧ emp) ∨ (∃ %x_7, %x_9 . 1 = %y_8 = %x_9 ∧ ((1 = %y_8) ∧ (1 = %x_9)) @@ -147,7 +147,7 @@ let%test_module _ = [%expect {| ( ( emp) ∨ ( ( ( 1 = %y_8 ∧ emp) ∨ ( emp) )) ) - + ( ( emp) ∨ ( 1 = %y_8 ∧ emp) ∨ ( emp) ) |}] let%expect_test _ = @@ -159,9 +159,9 @@ let%test_module _ = [%expect {| ∃ %x_7 . %x_7 = f(%x_7) ∧ (-1 + %y_8) = f(%y_8) ∧ emp - + (-1 + %y_8) = f(%y_8) ∧ ((1 + f(%y_8)) = %y_8) ∧ emp - + (-1 + %y_8) = f(%y_8) ∧ emp |}] let%expect_test _ = @@ -222,14 +222,14 @@ let%test_module _ = ∧ ((%b_2 = %z_9) ∧ (%c_3 = %m_6)) ∧ emp) ) - + ∃ %b_2 . tt ∧ tt ∧ %x_7 -[ %b_2, %c_3 )-> ⟨8,0⟩ * ( ( %b_2 = %z_9 ∧ (%b_2 = %z_9) ∧ emp) ∨ ( %b_2 = %y_8 ∧ (%b_2 = %y_8) ∧ emp) ) - + ∃ %b_2 . %x_7 -[ %b_2, %c_3 )-> ⟨8,0⟩ * ( ( %b_2 = %z_9 ∧ emp) ∨ ( %b_2 = %y_8 ∧ emp) ) |}]