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) ) |}]