From 0aed6eeab67c2a3b10f8cf341ad198dd0a9884b8 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 9 Jul 2020 07:43:34 -0700 Subject: [PATCH] [sledge] Refactor: Rename to use "first-order logical context" terminology Summary: instead of "congruence relation". Reviewed By: ngorogiannis Differential Revision: D22170512 fbshipit-source-id: 2382248da --- sledge/src/domain_sh.ml | 14 +-- sledge/src/sh.ml | 188 ++++++++++++++++++++-------------------- sledge/src/sh.mli | 17 ++-- sledge/src/solver.ml | 57 ++++++------ 4 files changed, 136 insertions(+), 140 deletions(-) diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index cba093ba3..d1f2c8bb7 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -83,15 +83,15 @@ let exec_intrinsic ~skip_throw q r i es = (List.map ~f:Term.of_exp es) |> Option.map ~f:(Option.map ~f:simplify) -let term_eq_class_has_only_vars_in fvs cong term = +let term_eq_class_has_only_vars_in fvs ctx term = [%Trace.call fun {pf} -> - pf "@[ fvs: @[%a@] @,cong: @[%a@] @,term: @[%a@]@]" Var.Set.pp fvs - Context.pp cong Term.pp term] + pf "@[ fvs: @[%a@] @,ctx: @[%a@] @,term: @[%a@]@]" Var.Set.pp fvs + Context.pp ctx Term.pp term] ; let term_has_only_vars_in fvs term = Var.Set.is_subset (Term.fv term) ~of_:fvs in - let term_eq_class = Context.class_of cong term in + let term_eq_class = Context.class_of ctx term in List.exists ~f:(term_has_only_vars_in fvs) term_eq_class |> [%Trace.retn fun {pf} -> pf "%b"] @@ -106,8 +106,8 @@ let garbage_collect (q : t) ~wrt = else let new_set = List.fold ~init:current q.heap ~f:(fun current seg -> - if term_eq_class_has_only_vars_in current q.cong seg.loc then - List.fold (Context.class_of q.cong seg.seq) ~init:current + if term_eq_class_has_only_vars_in current q.ctx seg.loc then + List.fold (Context.class_of q.ctx seg.seq) ~init:current ~f:(fun c e -> Var.Set.union c (Term.fv e)) else current ) in @@ -115,7 +115,7 @@ let garbage_collect (q : t) ~wrt = in let r_vars = all_reachable_vars Var.Set.empty wrt q in Sh.filter_heap q ~f:(fun seg -> - term_eq_class_has_only_vars_in r_vars q.cong seg.loc ) + term_eq_class_has_only_vars_in r_vars q.ctx seg.loc ) |> [%Trace.retn fun {pf} -> pf "%a" pp] diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 32085d07e..a6178b946 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -17,7 +17,7 @@ type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t} type starjunction = { us: Var.Set.t ; xs: Var.Set.t - ; cong: Context.t + ; ctx: Context.t ; pure: Term.t ; heap: seg list ; djns: disjunction list } @@ -32,7 +32,7 @@ type t = starjunction [@@deriving compare, equal, sexp] let emp = { us= Var.Set.empty ; xs= Var.Set.empty - ; cong= Context.true_ + ; ctx= Context.true_ ; pure= Term.true_ ; heap= [] ; djns= [] } @@ -56,16 +56,16 @@ let map_seg ~f h = then h else {loc; bas; len; siz; seq} -let map ~f_sjn ~f_cong ~f_trm ({us; xs= _; cong; pure; heap; djns} as q) = +let map ~f_sjn ~f_ctx ~f_trm ({us; xs= _; ctx; pure; heap; djns} as q) = let pure = f_trm pure in if Term.is_false pure then false_ us else - let cong = f_cong cong in + let ctx = f_ctx ctx in let heap = List.map_endo heap ~f:(map_seg ~f:f_trm) in let djns = List.map_endo djns ~f:(List.map_endo ~f:f_sjn) in - if cong == q.cong && pure == q.pure && heap == q.heap && djns == q.djns + if ctx == q.ctx && pure == q.pure && heap == q.heap && djns == q.djns then q - else {q with cong; pure; heap; djns} + else {q with ctx; pure; heap; djns} let fold_terms_seg {loc; bas; len; siz; seq} ~init ~f = let f b s = f s b in @@ -74,18 +74,17 @@ let fold_terms_seg {loc; bas; len; siz; seq} ~init ~f = let fold_vars_seg seg ~init ~f = fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init) -let fold_vars_stem ?ignore_cong {us= _; xs= _; cong; pure; heap; djns= _} +let fold_vars_stem ?ignore_ctx {us= _; xs= _; ctx; pure; heap; djns= _} ~init ~f = List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init) |> fun init -> Term.fold_vars ~f ~init pure |> fun init -> - if Option.is_some ignore_cong then init - else - Context.fold_terms ~init cong ~f:(fun init -> Term.fold_vars ~f ~init) + if Option.is_some ignore_ctx then init + else Context.fold_terms ~init ctx ~f:(fun init -> Term.fold_vars ~f ~init) -let fold_vars ?ignore_cong fold_vars q ~init ~f = - fold_vars_stem ?ignore_cong ~init ~f q +let fold_vars ?ignore_ctx fold_vars q ~init ~f = + fold_vars_stem ?ignore_ctx ~init ~f q |> fun init -> List.fold ~init q.djns ~f:(fun init -> List.fold ~init ~f:fold_vars) @@ -100,7 +99,7 @@ let rec var_strength_ xs m q = in let xs = Var.Set.union xs q.xs in let m_stem = - fold_vars_stem ~ignore_cong:() q ~init:m ~f:(fun m var -> + fold_vars_stem ~ignore_ctx:() q ~init:m ~f:(fun m var -> if not (Var.Set.mem xs var) then Var.Map.set m ~key:var ~data:`Universal else add m var ) @@ -135,9 +134,9 @@ let pp_seg x fs {loc; bas; len; siz; seq} = Format.fprintf fs " %a, %a " term_pp bas term_pp len ) (bas, len) (pp_chunk x) (siz, seq) -let pp_seg_norm cong fs seg = +let pp_seg_norm ctx fs seg = let x _ = None in - pp_seg x fs (map_seg seg ~f:(Context.normalize cong)) + pp_seg x fs (map_seg seg ~f:(Context.normalize ctx)) let pp_block x fs segs = let is_full_alloc segs = @@ -171,7 +170,7 @@ let pp_block x fs segs = pp_chunks segs | [] -> () -let pp_heap x ?pre cong fs heap = +let pp_heap x ?pre ctx fs heap = let bas_off e = match Term.const_of e with | Some const -> (Term.sub e (Term.rational const), const) @@ -179,17 +178,15 @@ let pp_heap x ?pre cong fs heap = in let compare s1 s2 = [%compare: Term.t * (Term.t * Q.t)] - ( Context.normalize cong s1.bas - , bas_off (Context.normalize cong s1.loc) ) - ( Context.normalize cong s2.bas - , bas_off (Context.normalize cong s2.loc) ) + (Context.normalize ctx s1.bas, bas_off (Context.normalize ctx s1.loc)) + (Context.normalize ctx s2.bas, bas_off (Context.normalize ctx s2.loc)) in let break s1 s2 = (not (Term.equal s1.bas s2.bas)) || (not (Term.equal s1.len s2.len)) - || not (Context.entails_eq cong (Term.add s1.loc s1.siz) s2.loc) + || not (Context.entails_eq ctx (Term.add s1.loc s1.siz) s2.loc) in - let heap = List.map heap ~f:(map_seg ~f:(Context.normalize cong)) in + let heap = List.map heap ~f:(map_seg ~f:(Context.normalize ctx)) in let blocks = List.group ~break (List.sort ~compare heap) in List.pp ?pre "@ * " (pp_block x) fs blocks @@ -203,8 +200,8 @@ let pp_us ?(pre = ("" : _ fmt)) ?vs () fs us = [%Trace.fprintf fs "%( %)@[%a@] .@ " pre (Var.Set.pp_diff Var.pp) (vs, us)] -let rec pp_ ?var_strength vs parent_xs parent_cong fs - {us; xs; cong; pure; heap; djns} = +let rec pp_ ?var_strength vs parent_xs parent_ctx fs + {us; xs; ctx; pure; heap; djns} = Format.pp_open_hvbox fs 0 ; let x v = Option.bind ~f:(fun (_, m) -> Var.Map.find m v) var_strength in pp_us ~vs () fs us ; @@ -218,14 +215,14 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ; if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ; - let clss = Context.diff_classes cong parent_cong in + let clss = Context.diff_classes ctx parent_ctx in let first = Term.Map.is_empty clss in if not first then Format.fprintf fs " " ; Context.ppx_classes x fs clss ; let pure = if Option.is_none var_strength then [pure] else - let pure' = Context.normalize cong pure in + let pure' = Context.normalize ctx pure in if Term.is_true pure' then [] else [pure'] in List.pp @@ -236,7 +233,7 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs Format.fprintf fs ( if first then if List.is_empty djns then " emp" else "" else "@ @<5>∧ emp" ) - else pp_heap x ~pre:(if first then " " else "@ @<2>∧ ") cong fs heap ; + else pp_heap x ~pre:(if first then " " else "@ @<2>∧ ") ctx fs heap ; let first = first && List.is_empty heap in List.pp ~pre:(if first then " " else "@ * ") @@ -244,11 +241,11 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs (pp_djn ?var_strength (Var.Set.union vs (Var.Set.union us xs)) (Var.Set.union parent_xs xs) - cong) + ctx) fs djns ; Format.pp_close_box fs () -and pp_djn ?var_strength vs xs cong fs = function +and pp_djn ?var_strength vs xs ctx fs = function | [] -> Format.fprintf fs "false" | djn -> Format.fprintf fs "@[( %a@ )@]" @@ -258,22 +255,22 @@ and pp_djn ?var_strength vs xs cong fs = function var_strength_ xs var_strength_stem sjn in Format.fprintf fs "@[(%a)@]" - (pp_ ?var_strength vs (Var.Set.union xs sjn.xs) cong) + (pp_ ?var_strength vs (Var.Set.union xs sjn.xs) ctx) sjn )) djn -let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) cong fs q = - pp_ ~var_strength:(var_strength ~xs q) us xs cong fs q +let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) ctx fs q = + pp_ ~var_strength:(var_strength ~xs q) us xs ctx fs q let pp fs q = pp_diff_eq Context.true_ fs q let pp_djn fs d = pp_djn Var.Set.empty Var.Set.empty Context.true_ fs d let pp_raw fs q = pp_ Var.Set.empty Var.Set.empty Context.true_ fs q let fv_seg seg = fold_vars_seg seg ~f:Var.Set.add ~init:Var.Set.empty -let fv ?ignore_cong q = +let fv ?ignore_ctx q = let rec fv_union init q = Var.Set.diff - (fold_vars ?ignore_cong fv_union q ~init ~f:Var.Set.add) + (fold_vars ?ignore_ctx fv_union q ~init ~f:Var.Set.add) q.xs in fv_union Var.Set.empty q @@ -287,7 +284,7 @@ let invariant_seg _ = () let rec invariant q = let@ () = Invariant.invariant [%here] q [%sexp_of: t] in - let {us; xs; cong; pure; heap; djns} = q in + let {us; xs; ctx; pure; heap; djns} = q in try assert ( Var.Set.disjoint us xs @@ -297,13 +294,13 @@ let rec invariant q = Var.Set.is_subset (fv q) ~of_:us || fail "unbound but free: %a" Var.Set.pp (Var.Set.diff (fv q) us) () ) ; - Context.invariant cong ; + Context.invariant ctx ; ( match djns with | [[]] -> - assert (Context.is_true cong) ; + assert (Context.is_true ctx) ; assert (Term.is_true pure) ; assert (List.is_empty heap) - | _ -> assert (not (Context.is_false cong)) ) ; + | _ -> assert (not (Context.is_false ctx)) ) ; invariant_pure pure ; List.iter heap ~f:invariant_seg ; List.iter djns ~f:(fun djn -> @@ -320,7 +317,7 @@ let rec invariant q = invariant *) let rec apply_subst sub q = map q ~f_sjn:(rename sub) - ~f_cong:(fun r -> Context.rename r sub) + ~f_ctx:(fun r -> Context.rename r sub) ~f_trm:(Term.rename sub) |> check (fun q' -> assert (Var.Set.disjoint (fv q') (Var.Subst.domain sub)) ) @@ -435,19 +432,18 @@ let elim_exists xs q = (** Construct *) -(** conjoin an equality relation assuming vocabulary is compatible *) -let and_cong_ cong q = - assert (Var.Set.is_subset (Context.fv cong) ~of_:q.us) ; - let xs, cong = Context.and_ (Var.Set.union q.us q.xs) q.cong cong in - if Context.is_false cong then false_ q.us - else exists_fresh xs {q with cong} +(** conjoin an FOL context assuming vocabulary is compatible *) +let and_ctx_ ctx q = + assert (Var.Set.is_subset (Context.fv ctx) ~of_:q.us) ; + let xs, ctx = Context.and_ (Var.Set.union q.us q.xs) q.ctx ctx in + if Context.is_false ctx then false_ q.us else exists_fresh xs {q with ctx} -let and_cong cong q = - [%Trace.call fun {pf} -> pf "%a@ %a" Context.pp cong pp q] +let and_ctx ctx q = + [%Trace.call fun {pf} -> pf "%a@ %a" Context.pp ctx pp q] ; ( match q.djns with | [[]] -> q - | _ -> and_cong_ cong (extend_us (Context.fv cong) q) ) + | _ -> and_ctx_ ctx (extend_us (Context.fv ctx) q) ) |> [%Trace.retn fun {pf} q -> pf "%a" pp q ; @@ -459,30 +455,30 @@ let star q1 q2 = ( match (q1, q2) with | {djns= [[]]; _}, _ | _, {djns= [[]]; _} -> false_ (Var.Set.union q1.us q2.us) - | {us= _; xs= _; cong; pure; heap= []; djns= []}, _ - when Context.is_true cong && Term.is_true pure -> + | {us= _; xs= _; ctx; pure; heap= []; djns= []}, _ + when Context.is_true ctx && Term.is_true pure -> let us = Var.Set.union q1.us q2.us in if us == q2.us then q2 else {q2 with us} - | _, {us= _; xs= _; cong; pure; heap= []; djns= []} - when Context.is_true cong && Term.is_true pure -> + | _, {us= _; xs= _; ctx; pure; heap= []; djns= []} + when Context.is_true ctx && Term.is_true pure -> let us = Var.Set.union q1.us q2.us in if us == q1.us then q1 else {q1 with us} | _ -> let us = Var.Set.union q1.us q2.us in let q1 = freshen_xs q1 ~wrt:(Var.Set.union us q2.xs) in let q2 = freshen_xs q2 ~wrt:(Var.Set.union us q1.xs) in - let {us= us1; xs= xs1; cong= c1; pure= p1; heap= h1; djns= d1} = q1 in - let {us= us2; xs= xs2; cong= c2; pure= p2; heap= h2; djns= d2} = q2 in + let {us= us1; xs= xs1; ctx= c1; pure= p1; heap= h1; djns= d1} = q1 in + let {us= us2; xs= xs2; ctx= c2; pure= p2; heap= h2; djns= d2} = q2 in assert (Var.Set.equal us (Var.Set.union us1 us2)) ; - let xs, cong = + let xs, ctx = Context.and_ (Var.Set.union us (Var.Set.union xs1 xs2)) c1 c2 in - if Context.is_false cong then false_ us + if Context.is_false ctx then false_ us else exists_fresh xs { us ; xs= Var.Set.union xs1 xs2 - ; cong + ; ctx ; pure= Term.and_ p1 p2 ; heap= List.append h1 h2 ; djns= List.append d1 d2 } ) @@ -504,17 +500,17 @@ let or_ q1 q2 = | {djns= [[]]; _}, _ -> extend_us q1.us q2 | _, {djns= [[]]; _} -> extend_us q2.us q1 | ( ({djns= []; _} as q) - , ({us= _; xs; cong= _; pure; heap= []; djns= [djn]} as d) ) + , ({us= _; xs; ctx= _; pure; heap= []; djns= [djn]} as d) ) when Var.Set.is_empty xs && Term.is_true pure -> {d with us= Var.Set.union q.us d.us; djns= [q :: djn]} - | ( ({us= _; xs; cong= _; pure; heap= []; djns= [djn]} as d) + | ( ({us= _; xs; ctx= _; pure; heap= []; djns= [djn]} as d) , ({djns= []; _} as q) ) when Var.Set.is_empty xs && Term.is_true pure -> {d with us= Var.Set.union q.us d.us; djns= [q :: djn]} | _ -> { us= Var.Set.union q1.us q2.us ; xs= Var.Set.empty - ; cong= Context.true_ + ; ctx= Context.true_ ; pure= Term.true_ ; heap= [] ; djns= [[q1; q2]] } ) @@ -534,9 +530,9 @@ let pure (e : Term.t) = ; List.fold (Term.disjuncts e) ~init:(false_ Var.Set.empty) ~f:(fun q b -> let us = Term.fv b in - let xs, cong = Context.(and_term us b true_) in - if Context.is_false cong then false_ us - else or_ q (exists_fresh xs {emp with us; cong; pure= b}) ) + let xs, ctx = Context.(and_term us b true_) in + if Context.is_false ctx then false_ us + else or_ q (exists_fresh xs {emp with us; ctx; pure= b}) ) |> [%Trace.retn fun {pf} q -> pf "%a" pp q ; @@ -589,23 +585,23 @@ let filter_heap ~f q = (** Query *) let is_emp = function - | {us= _; xs= _; cong= _; pure; heap= []; djns= []} -> Term.is_true pure + | {us= _; xs= _; ctx= _; pure; heap= []; djns= []} -> Term.is_true pure | _ -> false let is_false = function | {djns= [[]]; _} -> true - | {cong; pure; heap; _} -> - Term.is_false (Context.normalize cong pure) + | {ctx; pure; heap; _} -> + Term.is_false (Context.normalize ctx pure) || List.exists heap ~f:(fun seg -> - Context.entails_eq cong seg.loc Term.zero ) + Context.entails_eq ctx seg.loc Term.zero ) -let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) = +let rec pure_approx ({us; xs; ctx; pure; heap= _; djns} as q) = let heap = emp.heap in let djns = List.map_endo djns ~f:(fun djn -> List.map_endo djn ~f:pure_approx) in if heap == q.heap && djns == q.djns then q - else {us; xs; cong; pure; heap; djns} |> check invariant + else {us; xs; ctx; pure; heap; djns} |> check invariant let pure_approx q = [%Trace.call fun {pf} -> pf "%a" pp q] @@ -650,10 +646,10 @@ let rec norm_ s q = [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Context.Subst.pp s pp_raw q] ; let q = - map q ~f_sjn:(norm_ s) ~f_cong:Fn.id ~f_trm:(Context.Subst.subst s) + map q ~f_sjn:(norm_ s) ~f_ctx:Fn.id ~f_trm:(Context.Subst.subst s) in - let xs, cong = Context.apply_subst (Var.Set.union q.us q.xs) s q.cong in - exists_fresh xs {q with cong} + let xs, ctx = Context.apply_subst (Var.Set.union q.us q.xs) s q.ctx in + exists_fresh xs {q with ctx} |> [%Trace.retn fun {pf} q' -> pf "%a" pp_raw q' ; @@ -693,9 +689,9 @@ let rec freshen_nested_xs q = pf "%a" pp q' ; invariant q'] -let rec propagate_equality_ ancestor_vs ancestor_cong q = +let rec propagate_context_ ancestor_vs ancestor_ctx q = [%Trace.call fun {pf} -> - pf "(%a)@ %a" Context.pp_classes ancestor_cong pp q] + pf "(%a)@ %a" Context.pp_classes ancestor_ctx pp q] ; (* extend vocabulary with variables in scope above *) let ancestor_vs = Var.Set.union ancestor_vs (Var.Set.union q.us q.xs) in @@ -703,33 +699,33 @@ let rec propagate_equality_ ancestor_vs ancestor_cong q = let xs, stem, djns = (q.xs, {q with us= ancestor_vs; xs= emp.xs; djns= emp.djns}, q.djns) in - (* strengthen equality relation with that from above *) - let ancestor_stem = and_cong_ ancestor_cong stem in - let ancestor_cong = ancestor_stem.cong in + (* strengthen context with that from above *) + let ancestor_stem = and_ctx_ ancestor_ctx stem in + let ancestor_ctx = ancestor_stem.ctx in exists xs (List.fold djns ~init:ancestor_stem ~f:(fun q' djn -> - let dj_congs, djn = + let dj_ctxs, djn = List.rev_map_unzip djn ~f:(fun dj -> - let dj = propagate_equality_ ancestor_vs ancestor_cong dj in - (dj.cong, dj) ) + let dj = propagate_context_ ancestor_vs ancestor_ctx dj in + (dj.ctx, dj) ) in - let new_xs, djn_cong = Context.orN ancestor_vs dj_congs in - (* hoist xs appearing in disjunction's equality relation *) - let djn_xs = Var.Set.diff (Context.fv djn_cong) q'.us in + let new_xs, djn_ctx = Context.orN ancestor_vs dj_ctxs in + (* hoist xs appearing in disjunction's context *) + let djn_xs = Var.Set.diff (Context.fv djn_ctx) q'.us in let djn = List.map ~f:(elim_exists djn_xs) djn in - let cong_djn = and_cong_ djn_cong (orN djn) in - assert (is_false cong_djn || Var.Set.is_subset new_xs ~of_:djn_xs) ; - star (exists djn_xs cong_djn) q' )) + let ctx_djn = and_ctx_ djn_ctx (orN djn) in + assert (is_false ctx_djn || Var.Set.is_subset new_xs ~of_:djn_xs) ; + star (exists djn_xs ctx_djn) q' )) |> [%Trace.retn fun {pf} q' -> pf "%a" pp q' ; invariant q'] -let propagate_equality ancestor_vs ancestor_cong q = +let propagate_context ancestor_vs ancestor_ctx q = [%Trace.call fun {pf} -> - pf "(%a)@ %a" Context.pp_classes ancestor_cong pp q] + pf "(%a)@ %a" Context.pp_classes ancestor_ctx pp q] ; - propagate_equality_ ancestor_vs ancestor_cong q + propagate_context_ ancestor_vs ancestor_ctx q |> [%Trace.retn fun {pf} q' -> pf "%a" pp q' ; @@ -745,19 +741,19 @@ let remove_absent_xs ks q = if Var.Set.is_empty ks then q else let xs = Var.Set.diff q.xs ks in - let cong = Context.elim ks q.cong in + let ctx = Context.elim ks q.ctx in let djns = let rec trim_ks ks djns = List.map djns ~f:(fun djn -> List.map djn ~f:(fun sjn -> { sjn with us= Var.Set.diff sjn.us ks - ; cong= Context.elim ks sjn.cong + ; ctx= Context.elim ks sjn.ctx ; djns= trim_ks ks sjn.djns } ) ) in trim_ks ks q.djns in - {q with xs; cong; djns} + {q with xs; ctx; djns} let rec simplify_ us rev_xss q = [%Trace.call fun {pf} -> pf "%a@ %a" pp_vss (List.rev rev_xss) pp_raw q] @@ -772,8 +768,8 @@ let rec simplify_ us rev_xss q = orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn)) ) )) in - (* try to solve equations in cong for variables in xss *) - let subst = Context.solve_for_vars (us :: List.rev rev_xss) q.cong in + (* try to solve equations in ctx for variables in xss *) + let subst = Context.solve_for_vars (us :: List.rev rev_xss) q.ctx in (* simplification can reveal inconsistency *) ( if is_false q then false_ q.us else if Context.Subst.is_empty subst then q @@ -784,7 +780,7 @@ let rec simplify_ us rev_xss q = let removed = Var.Set.diff (Var.Set.union_list rev_xss) - (fv ~ignore_cong:() (elim_exists q.xs q)) + (fv ~ignore_ctx:() (elim_exists q.xs q)) in let keep, removed, _ = Context.Subst.partition_valid removed subst in let q = and_subst keep q in @@ -799,7 +795,7 @@ let simplify q = [%Trace.call fun {pf} -> pf "%a" pp_raw q] ; let q = freshen_nested_xs q in - let q = propagate_equality Var.Set.empty Context.true_ q in + let q = propagate_context Var.Set.empty Context.true_ q in let q = simplify_ q.us [] q in q |> diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli index a3df73030..f96e54581 100644 --- a/sledge/src/sh.mli +++ b/sledge/src/sh.mli @@ -17,7 +17,8 @@ type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t} type starjunction = private { us: Var.Set.t (** vocabulary / variable context of formula *) ; xs: Var.Set.t (** existentially-bound variables *) - ; cong: Context.t (** congruence induced by rest of formula *) + ; ctx: Context.t + (** first-order logical context induced by rest of formula *) ; pure: Term.t (** pure boolean constraints *) ; heap: seg list (** star-conjunction of segment atomic formulas *) ; djns: disjunction list (** star-conjunction of disjunctions *) } @@ -61,8 +62,8 @@ val pure : Term.t -> t val and_ : Term.t -> t -> t (** Conjoin a boolean constraint to a formula. *) -val and_cong : Context.t -> t -> t -(** Conjoin constraints of a congruence to a formula, extending to a common +val and_ctx : Context.t -> t -> t +(** Conjoin a context to that of a formula, extending to a common vocabulary, and avoiding capturing existentials. *) val and_subst : Context.Subst.t -> t -> t @@ -73,9 +74,9 @@ val and_subst : Context.Subst.t -> t -> t val with_pure : Term.t -> t -> t (** [with_pure pure q] is [{q with pure}], which assumes that [q.pure] and - [pure] are defined in the same vocabulary. Note that [cong] is not - weakened, so if [pure] and [q.pure] do not induce the same congruence, - then the result will have a stronger [cong] than induced by its [pure]. *) + [pure] are defined in the same vocabulary. Note that [ctx] is not + weakened, so if [pure] and [q.pure] do not induce the same context, then + the result will have a stronger [ctx] than induced by its [pure]. *) val rem_seg : seg -> t -> t (** [star (seg s) (rem_seg s q)] is equivalent to [q], assuming that [s] is @@ -116,13 +117,13 @@ val extend_us : Var.Set.t -> t -> t (** Query *) val is_emp : t -> bool -(** Holds of [emp], with any vocabulary, existentials, and congruence. *) +(** Holds of [emp], with any vocabulary, existentials, and context. *) val is_false : t -> bool (** Holds only of inconsistent formulas, does not hold of all inconsistent formulas. *) -val fv : ?ignore_cong:unit -> t -> Var.Set.t +val fv : ?ignore_ctx:unit -> t -> Var.Set.t (** Free variables, a subset of vocabulary. *) val pure_approx : t -> t diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml index 5a137502f..9b6752e8f 100644 --- a/sledge/src/solver.ml +++ b/sledge/src/solver.ml @@ -26,10 +26,9 @@ module Goal : sig type t = private { us: Var.Set.t (** (universal) vocabulary of entire judgment *) ; com: Sh.t (** common star-conjunct of minuend and subtrahend *) - ; min: Sh.t - (** minuend, cong strengthened by pure_approx (com * min) *) + ; min: Sh.t (** minuend, ctx strengthened by pure_approx (com * min) *) ; xs: Var.Set.t (** existentials over subtrahend and remainder *) - ; sub: Sh.t (** subtrahend, cong strengthened by min.cong *) + ; sub: Sh.t (** subtrahend, ctx strengthened by min.ctx *) ; zs: Var.Set.t (** existentials over remainder *) ; pgs: bool (** indicates whether a deduction rule has been applied *) } @@ -71,7 +70,7 @@ end = struct Format.fprintf fs "@[%s %a@ | %a@ @[\\- %a%a@]@]" (if pgs then "t" else "f") Sh.pp com Sh.pp min Var.Set.pp_xs xs - (Sh.pp_diff_eq ~us:(Var.Set.union min.us sub.us) ~xs min.cong) + (Sh.pp_diff_eq ~us:(Var.Set.union min.us sub.us) ~xs min.ctx) sub let invariant g = @@ -156,15 +155,15 @@ let excise_exists goal = let solutions_for_xs = let xs = Var.Set.diff goal.xs - (Sh.fv ~ignore_cong:() (Sh.with_pure Term.true_ goal.sub)) + (Sh.fv ~ignore_ctx:() (Sh.with_pure Term.true_ goal.sub)) in - Context.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.cong + Context.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.ctx in if Context.Subst.is_empty solutions_for_xs then goal else let removed = Var.Set.diff goal.xs - (Sh.fv ~ignore_cong:() (Sh.norm solutions_for_xs goal.sub)) + (Sh.fv ~ignore_ctx:() (Sh.norm solutions_for_xs goal.sub)) in if Var.Set.is_empty removed then goal else @@ -183,7 +182,7 @@ let excise_exists goal = let excise_pure ({min; sub} as goal) = trace (fun {pf} -> pf "@[<2>excise_pure@ %a@]" pp goal) ; - let pure' = Context.normalize min.cong sub.pure in + let pure' = Context.normalize min.ctx sub.pure in if Term.is_false pure' then None else Some (goal |> with_ ~sub:(Sh.with_pure pure' sub)) @@ -202,8 +201,8 @@ let excise_pure ({min; sub} as goal) = *) let excise_seg_same ({com; min; sub} as goal) msg ssg = excise (fun {pf} -> - pf "@[excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.cong) - msg (Sh.pp_seg_norm sub.cong) ssg ) ; + pf "@[excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.ctx) + msg (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.bas= b; len= m; seq= a} = msg in let {Sh.bas= b'; len= m'; seq= a'} = ssg in let com = Sh.star (Sh.seg msg) com in @@ -231,7 +230,7 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n = excise (fun {pf} -> pf "@[excise_seg_sub_prefix@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; + (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in let {Sh.bas= b'; len= m'; siz= n; seq= a'} = ssg in let o_n = Term.integer o_n in @@ -271,7 +270,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o = excise (fun {pf} -> pf "@[excise_seg_min_prefix@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; + (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let n_o = Term.integer n_o in @@ -307,7 +306,7 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k = excise (fun {pf} -> pf "@[excise_seg_sub_suffix@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; + (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let l_k = Term.integer l_k in @@ -349,7 +348,7 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k ko_ln = excise (fun {pf} -> pf "@[excise_seg_sub_infix@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; + (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let l_k = Term.integer l_k in @@ -396,7 +395,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k ko_l ln_ko = excise (fun {pf} -> pf "@[excise_seg_min_skew@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; + (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let l_k = Term.integer l_k in @@ -446,7 +445,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l = excise (fun {pf} -> pf "@[excise_seg_min_suffix@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; + (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let k_l = Term.integer k_l in @@ -483,7 +482,7 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l ln_ko = excise (fun {pf} -> pf "@[excise_seg_min_infix@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; + (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let k_l = Term.integer k_l in @@ -524,7 +523,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l ln_k ko_ln = excise (fun {pf} -> pf "@[excise_seg_sub_skew@ %a@ \\- %a@]" - (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ; + (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in let k_l = Term.integer k_l in @@ -558,14 +557,14 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l (* C ❮ k-[b;m)->⟨o,α⟩ * M ⊢ ∃xs. l-[b';m')->⟨n,α'⟩ * S ❯ R *) let excise_seg ({sub} as goal) msg ssg = trace (fun {pf} -> - pf "@[<2>excise_seg@ %a@ |- %a@]" (Sh.pp_seg_norm sub.cong) msg - (Sh.pp_seg_norm sub.cong) ssg ) ; + pf "@[<2>excise_seg@ %a@ |- %a@]" (Sh.pp_seg_norm sub.ctx) msg + (Sh.pp_seg_norm sub.ctx) ssg ) ; let {Sh.loc= k; bas= b; len= m; siz= o} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n} = ssg in - let* k_l = Context.difference sub.cong k l in + let* k_l = Context.difference sub.ctx k l in if - (not (Context.entails_eq sub.cong b b')) - || not (Context.entails_eq sub.cong m m') + (not (Context.entails_eq sub.ctx b b')) + || not (Context.entails_eq sub.ctx m m') then Some ( goal @@ -578,11 +577,11 @@ let excise_seg ({sub} as goal) msg ssg = | Neg -> ( let ko = Term.add k o in let ln = Term.add l n in - let* ko_ln = Context.difference sub.cong ko ln in + let* ko_ln = Context.difference sub.ctx ko ln in match Int.sign (Z.sign ko_ln) with (* k+o-(l+n) < 0 so k+o < l+n *) | Neg -> ( - let* l_ko = Context.difference sub.cong l ko in + let* l_ko = Context.difference sub.ctx l ko in match Int.sign (Z.sign l_ko) with (* l-(k+o) < 0 [k; o) * so l < k+o ⊢ [l; n) *) @@ -600,7 +599,7 @@ let excise_seg ({sub} as goal) msg ssg = ) (* k-l = 0 so k = l *) | Zero -> ( - let* o_n = Context.difference sub.cong o n in + let* o_n = Context.difference sub.ctx o n in match Int.sign (Z.sign o_n) with (* o-n < 0 [k; o) * so o < n ⊢ [l; n) *) @@ -615,7 +614,7 @@ let excise_seg ({sub} as goal) msg ssg = | Pos -> ( let ko = Term.add k o in let ln = Term.add l n in - let* ko_ln = Context.difference sub.cong ko ln in + let* ko_ln = Context.difference sub.ctx ko ln in match Int.sign (Z.sign ko_ln) with (* k+o-(l+n) < 0 [k; o) * so k+o < l+n ⊢ [l; n) *) @@ -625,7 +624,7 @@ let excise_seg ({sub} as goal) msg ssg = | Zero -> Some (excise_seg_min_suffix goal msg ssg k_l) (* k+o-(l+n) > 0 so k+o > l+n *) | Pos -> ( - let* k_ln = Context.difference sub.cong k ln in + let* k_ln = Context.difference sub.ctx k ln in match Int.sign (Z.sign k_ln) with (* k-(l+n) < 0 [k; o) * so k < l+n ⊢ [l; n) *) @@ -673,7 +672,7 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option = List.find_map dnf_subtrahend ~f:(fun sub -> [%Trace.call fun {pf} -> pf "@[<2>subtrahend@ %a@]" Sh.pp sub] ; - let sub = Sh.and_cong min.cong (Sh.extend_us us sub) in + let sub = Sh.and_ctx min.ctx (Sh.extend_us us sub) in excise (goal ~us ~com ~min ~xs ~sub ~zs ~pgs:true) |> [%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" Sh.pp)] )