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

[sledge] Refactor: Rename to use "first-order logical context" terminology

Browse Source 
Summary: instead of "congruence relation".

Reviewed By: ngorogiannis

Differential Revision: D22170512

fbshipit-source-id: 2382248da
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent a629486c9f
commit 0aed6eeab6
4 changed files with 136 additions and 140 deletions
Show Stats Download Patch File Download Diff File

14
sledge/src/domain_sh.ml
Unescape View File

@ -83,15 +83,15 @@ let exec_intrinsic ~skip_throw q r i es =
(List.map ~f:Term.of_exp es) (List.map ~f:Term.of_exp es)
|> Option.map ~f:(Option.map ~f:simplify) |> 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} -> [%Trace.call fun {pf} ->
pf "@[<v> fvs: @[%a@] @,cong: @[%a@] @,term: @[%a@]@]" Var.Set.pp fvs pf "@[<v> fvs: @[%a@] @,ctx: @[%a@] @,term: @[%a@]@]" Var.Set.pp fvs
Context.pp cong Term.pp term] Context.pp ctx Term.pp term]
; ;
let term_has_only_vars_in fvs term = let term_has_only_vars_in fvs term =
Var.Set.is_subset (Term.fv term) ~of_:fvs Var.Set.is_subset (Term.fv term) ~of_:fvs
in 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 List.exists ~f:(term_has_only_vars_in fvs) term_eq_class
|> |>
[%Trace.retn fun {pf} -> pf "%b"] [%Trace.retn fun {pf} -> pf "%b"]
@ -106,8 +106,8 @@ let garbage_collect (q : t) ~wrt =
else else
let new_set = let new_set =
List.fold ~init:current q.heap ~f:(fun current seg -> List.fold ~init:current q.heap ~f:(fun current seg ->
if term_eq_class_has_only_vars_in current q.cong seg.loc then if term_eq_class_has_only_vars_in current q.ctx seg.loc then
List.fold (Context.class_of q.cong seg.seq) ~init:current List.fold (Context.class_of q.ctx seg.seq) ~init:current
~f:(fun c e -> Var.Set.union c (Term.fv e)) ~f:(fun c e -> Var.Set.union c (Term.fv e))
else current ) else current )
in in
@ -115,7 +115,7 @@ let garbage_collect (q : t) ~wrt =
in in
let r_vars = all_reachable_vars Var.Set.empty wrt q in let r_vars = all_reachable_vars Var.Set.empty wrt q in
Sh.filter_heap q ~f:(fun seg -> 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] [%Trace.retn fun {pf} -> pf "%a" pp]

188
sledge/src/sh.ml
Unescape View File

@ -17,7 +17,7 @@ type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
type starjunction = type starjunction =
{ us: Var.Set.t { us: Var.Set.t
; xs: Var.Set.t ; xs: Var.Set.t
; cong: Context.t ; ctx: Context.t
; pure: Term.t ; pure: Term.t
; heap: seg list ; heap: seg list
; djns: disjunction list } ; djns: disjunction list }
@ -32,7 +32,7 @@ type t = starjunction [@@deriving compare, equal, sexp]
let emp = let emp =
{ us= Var.Set.empty { us= Var.Set.empty
; xs= Var.Set.empty ; xs= Var.Set.empty
; cong= Context.true_ ; ctx= Context.true_
; pure= Term.true_ ; pure= Term.true_
; heap= [] ; heap= []
; djns= [] } ; djns= [] }
@ -56,16 +56,16 @@ let map_seg ~f h =
then h then h
else {loc; bas; len; siz; seq} 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 let pure = f_trm pure in
if Term.is_false pure then false_ us if Term.is_false pure then false_ us
else 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 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 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 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 fold_terms_seg {loc; bas; len; siz; seq} ~init ~f =
let f b s = f s b in 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 = let fold_vars_seg seg ~init ~f =
fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init) 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 = ~init ~f =
List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init) List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init)
|> fun init -> |> fun init ->
Term.fold_vars ~f ~init pure Term.fold_vars ~f ~init pure
|> fun init -> |> fun init ->
if Option.is_some ignore_cong then init if Option.is_some ignore_ctx then init
else else Context.fold_terms ~init ctx ~f:(fun init -> Term.fold_vars ~f ~init)
Context.fold_terms ~init cong ~f:(fun init -> Term.fold_vars ~f ~init)
let fold_vars ?ignore_cong fold_vars q ~init ~f = let fold_vars ?ignore_ctx fold_vars q ~init ~f =
fold_vars_stem ?ignore_cong ~init ~f q fold_vars_stem ?ignore_ctx ~init ~f q
|> fun init -> |> fun init ->
List.fold ~init q.djns ~f:(fun init -> List.fold ~init ~f:fold_vars) 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 in
let xs = Var.Set.union xs q.xs in let xs = Var.Set.union xs q.xs in
let m_stem = 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 if not (Var.Set.mem xs var) then
Var.Map.set m ~key:var ~data:`Universal Var.Map.set m ~key:var ~data:`Universal
else add m var ) 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 ) Format.fprintf fs " %a, %a " term_pp bas term_pp len )
(bas, len) (pp_chunk x) (siz, seq) (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 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 pp_block x fs segs =
let is_full_alloc segs = let is_full_alloc segs =
@ -171,7 +170,7 @@ let pp_block x fs segs =
pp_chunks segs pp_chunks segs
| [] -> () | [] -> ()
let pp_heap x ?pre cong fs heap = let pp_heap x ?pre ctx fs heap =
let bas_off e = let bas_off e =
match Term.const_of e with match Term.const_of e with
| Some const -> (Term.sub e (Term.rational const), const) | Some const -> (Term.sub e (Term.rational const), const)
@ -179,17 +178,15 @@ let pp_heap x ?pre cong fs heap =
in in
let compare s1 s2 = let compare s1 s2 =
[%compare: Term.t * (Term.t * Q.t)] [%compare: Term.t * (Term.t * Q.t)]
( Context.normalize cong s1.bas (Context.normalize ctx s1.bas, bas_off (Context.normalize ctx s1.loc))
, bas_off (Context.normalize cong s1.loc) ) (Context.normalize ctx s2.bas, bas_off (Context.normalize ctx s2.loc))
( Context.normalize cong s2.bas
, bas_off (Context.normalize cong s2.loc) )
in in
let break s1 s2 = let break s1 s2 =
(not (Term.equal s1.bas s2.bas)) (not (Term.equal s1.bas s2.bas))
|| (not (Term.equal s1.len s2.len)) || (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 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 let blocks = List.group ~break (List.sort ~compare heap) in
List.pp ?pre "@ * " (pp_block x) fs blocks List.pp ?pre "@ * " (pp_block x) fs blocks
@ -203,8 +200,8 @@ let pp_us ?(pre = ("" : _ fmt)) ?vs () fs us =
[%Trace.fprintf [%Trace.fprintf
fs "%( %)@[%a@] .@ " pre (Var.Set.pp_diff Var.pp) (vs, us)] fs "%( %)@[%a@] .@ " pre (Var.Set.pp_diff Var.pp) (vs, us)]
let rec pp_ ?var_strength vs parent_xs parent_cong fs let rec pp_ ?var_strength vs parent_xs parent_ctx fs
{us; xs; cong; pure; heap; djns} = {us; xs; ctx; pure; heap; djns} =
Format.pp_open_hvbox fs 0 ; Format.pp_open_hvbox fs 0 ;
let x v = Option.bind ~f:(fun (_, m) -> Var.Map.find m v) var_strength in let x v = Option.bind ~f:(fun (_, m) -> Var.Map.find m v) var_strength in
pp_us ~vs () fs us ; 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 "@ " ) ;
if not (Var.Set.is_empty xs_d_vs) then if not (Var.Set.is_empty xs_d_vs) then
Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ; 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 let first = Term.Map.is_empty clss in
if not first then Format.fprintf fs " " ; if not first then Format.fprintf fs " " ;
Context.ppx_classes x fs clss ; Context.ppx_classes x fs clss ;
let pure = let pure =
if Option.is_none var_strength then [pure] if Option.is_none var_strength then [pure]
else else
let pure' = Context.normalize cong pure in let pure' = Context.normalize ctx pure in
if Term.is_true pure' then [] else [pure'] if Term.is_true pure' then [] else [pure']
in in
List.pp List.pp
@ -236,7 +233,7 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs
Format.fprintf fs Format.fprintf fs
( if first then if List.is_empty djns then " emp" else "" ( if first then if List.is_empty djns then " emp" else ""
else "@ @<5>∧ emp" ) 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 let first = first && List.is_empty heap in
List.pp List.pp
~pre:(if first then " " else "@ * ") ~pre:(if first then " " else "@ * ")
@ -244,11 +241,11 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs
(pp_djn ?var_strength (pp_djn ?var_strength
(Var.Set.union vs (Var.Set.union us xs)) (Var.Set.union vs (Var.Set.union us xs))
(Var.Set.union parent_xs xs) (Var.Set.union parent_xs xs)
cong) ctx)
fs djns ; fs djns ;
Format.pp_close_box fs () 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" | [] -> Format.fprintf fs "false"
| djn -> | djn ->
Format.fprintf fs "@[<hv>( %a@ )@]" Format.fprintf fs "@[<hv>( %a@ )@]"
@ -258,22 +255,22 @@ and pp_djn ?var_strength vs xs cong fs = function
var_strength_ xs var_strength_stem sjn var_strength_ xs var_strength_stem sjn
in in
Format.fprintf fs "@[<hv 1>(%a)@]" Format.fprintf fs "@[<hv 1>(%a)@]"
(pp_ ?var_strength vs (Var.Set.union xs sjn.xs) cong) (pp_ ?var_strength vs (Var.Set.union xs sjn.xs) ctx)
sjn )) sjn ))
djn djn
let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) 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 cong 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 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_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 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_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 = let rec fv_union init q =
Var.Set.diff 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 q.xs
in in
fv_union Var.Set.empty q fv_union Var.Set.empty q
@ -287,7 +284,7 @@ let invariant_seg _ = ()
let rec invariant q = let rec invariant q =
let@ () = Invariant.invariant [%here] q [%sexp_of: t] in 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 try
assert ( assert (
Var.Set.disjoint us xs Var.Set.disjoint us xs
@ -297,13 +294,13 @@ let rec invariant q =
Var.Set.is_subset (fv q) ~of_:us Var.Set.is_subset (fv q) ~of_:us
|| fail "unbound but free: %a" Var.Set.pp (Var.Set.diff (fv q) us) () || fail "unbound but free: %a" Var.Set.pp (Var.Set.diff (fv q) us) ()
) ; ) ;
Context.invariant cong ; Context.invariant ctx ;
( match djns with ( match djns with
| [[]] -> | [[]] ->
assert (Context.is_true cong) ; assert (Context.is_true ctx) ;
assert (Term.is_true pure) ; assert (Term.is_true pure) ;
assert (List.is_empty heap) assert (List.is_empty heap)
| _ -> assert (not (Context.is_false cong)) ) ; | _ -> assert (not (Context.is_false ctx)) ) ;
invariant_pure pure ; invariant_pure pure ;
List.iter heap ~f:invariant_seg ; List.iter heap ~f:invariant_seg ;
List.iter djns ~f:(fun djn -> List.iter djns ~f:(fun djn ->
@ -320,7 +317,7 @@ let rec invariant q =
invariant *) invariant *)
let rec apply_subst sub q = let rec apply_subst sub q =
map q ~f_sjn:(rename sub) 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) ~f_trm:(Term.rename sub)
|> check (fun q' -> |> check (fun q' ->
assert (Var.Set.disjoint (fv q') (Var.Subst.domain sub)) ) assert (Var.Set.disjoint (fv q') (Var.Subst.domain sub)) )
@ -435,19 +432,18 @@ let elim_exists xs q =
(** Construct *) (** Construct *)
(** conjoin an equality relation assuming vocabulary is compatible *) (** conjoin an FOL context assuming vocabulary is compatible *)
let and_cong_ cong q = let and_ctx_ ctx q =
assert (Var.Set.is_subset (Context.fv cong) ~of_:q.us) ; assert (Var.Set.is_subset (Context.fv ctx) ~of_:q.us) ;
let xs, cong = Context.and_ (Var.Set.union q.us q.xs) q.cong cong in let xs, ctx = Context.and_ (Var.Set.union q.us q.xs) q.ctx ctx in
if Context.is_false cong then false_ q.us if Context.is_false ctx then false_ q.us else exists_fresh xs {q with ctx}
else exists_fresh xs {q with cong}
let and_cong cong q = let and_ctx ctx q =
[%Trace.call fun {pf} -> pf "%a@ %a" Context.pp cong pp q] [%Trace.call fun {pf} -> pf "%a@ %a" Context.pp ctx pp q]
; ;
( match q.djns with ( match q.djns with
| [[]] -> q | [[]] -> q
| _ -> and_cong_ cong (extend_us (Context.fv cong) q) ) | _ -> and_ctx_ ctx (extend_us (Context.fv ctx) q) )
|> |>
[%Trace.retn fun {pf} q -> [%Trace.retn fun {pf} q ->
pf "%a" pp q ; pf "%a" pp q ;
@ -459,30 +455,30 @@ let star q1 q2 =
( match (q1, q2) with ( match (q1, q2) with
| {djns= [[]]; _}, _ | _, {djns= [[]]; _} -> | {djns= [[]]; _}, _ | _, {djns= [[]]; _} ->
false_ (Var.Set.union q1.us q2.us) false_ (Var.Set.union q1.us q2.us)
| {us= _; xs= _; cong; pure; heap= []; djns= []}, _ | {us= _; xs= _; ctx; pure; heap= []; djns= []}, _
when Context.is_true cong && Term.is_true pure -> when Context.is_true ctx && Term.is_true pure ->
let us = Var.Set.union q1.us q2.us in let us = Var.Set.union q1.us q2.us in
if us == q2.us then q2 else {q2 with us} if us == q2.us then q2 else {q2 with us}
| _, {us= _; xs= _; cong; pure; heap= []; djns= []} | _, {us= _; xs= _; ctx; pure; heap= []; djns= []}
when Context.is_true cong && Term.is_true pure -> when Context.is_true ctx && Term.is_true pure ->
let us = Var.Set.union q1.us q2.us in let us = Var.Set.union q1.us q2.us in
if us == q1.us then q1 else {q1 with us} if us == q1.us then q1 else {q1 with us}
| _ -> | _ ->
let us = Var.Set.union q1.us q2.us in let us = Var.Set.union q1.us q2.us in
let q1 = freshen_xs q1 ~wrt:(Var.Set.union us q2.xs) 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 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= us1; xs= xs1; ctx= 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= us2; xs= xs2; ctx= c2; pure= p2; heap= h2; djns= d2} = q2 in
assert (Var.Set.equal us (Var.Set.union us1 us2)) ; 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 Context.and_ (Var.Set.union us (Var.Set.union xs1 xs2)) c1 c2
in in
if Context.is_false cong then false_ us if Context.is_false ctx then false_ us
else else
exists_fresh xs exists_fresh xs
{ us { us
; xs= Var.Set.union xs1 xs2 ; xs= Var.Set.union xs1 xs2
; cong ; ctx
; pure= Term.and_ p1 p2 ; pure= Term.and_ p1 p2
; heap= List.append h1 h2 ; heap= List.append h1 h2
; djns= List.append d1 d2 } ) ; djns= List.append d1 d2 } )
@ -504,17 +500,17 @@ let or_ q1 q2 =
| {djns= [[]]; _}, _ -> extend_us q1.us q2 | {djns= [[]]; _}, _ -> extend_us q1.us q2
| _, {djns= [[]]; _} -> extend_us q2.us q1 | _, {djns= [[]]; _} -> extend_us q2.us q1
| ( ({djns= []; _} as q) | ( ({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 -> when Var.Set.is_empty xs && Term.is_true pure ->
{d with us= Var.Set.union q.us d.us; djns= [q :: djn]} {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) ) , ({djns= []; _} as q) )
when Var.Set.is_empty xs && Term.is_true pure -> when Var.Set.is_empty xs && Term.is_true pure ->
{d with us= Var.Set.union q.us d.us; djns= [q :: djn]} {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
| _ -> | _ ->
{ us= Var.Set.union q1.us q2.us { us= Var.Set.union q1.us q2.us
; xs= Var.Set.empty ; xs= Var.Set.empty
; cong= Context.true_ ; ctx= Context.true_
; pure= Term.true_ ; pure= Term.true_
; heap= [] ; heap= []
; djns= [[q1; q2]] } ) ; 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 -> List.fold (Term.disjuncts e) ~init:(false_ Var.Set.empty) ~f:(fun q b ->
let us = Term.fv b in let us = Term.fv b in
let xs, cong = Context.(and_term us b true_) in let xs, ctx = Context.(and_term us b true_) in
if Context.is_false cong then false_ us if Context.is_false ctx then false_ us
else or_ q (exists_fresh xs {emp with us; cong; pure= b}) ) else or_ q (exists_fresh xs {emp with us; ctx; pure= b}) )
|> |>
[%Trace.retn fun {pf} q -> [%Trace.retn fun {pf} q ->
pf "%a" pp q ; pf "%a" pp q ;
@ -589,23 +585,23 @@ let filter_heap ~f q =
(** Query *) (** Query *)
let is_emp = function 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 | _ -> false
let is_false = function let is_false = function
| {djns= [[]]; _} -> true | {djns= [[]]; _} -> true
| {cong; pure; heap; _} -> | {ctx; pure; heap; _} ->
Term.is_false (Context.normalize cong pure) Term.is_false (Context.normalize ctx pure)
|| List.exists heap ~f:(fun seg -> || 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 heap = emp.heap in
let djns = let djns =
List.map_endo djns ~f:(fun djn -> List.map_endo djn ~f:pure_approx) List.map_endo djns ~f:(fun djn -> List.map_endo djn ~f:pure_approx)
in in
if heap == q.heap && djns == q.djns then q 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 = let pure_approx q =
[%Trace.call fun {pf} -> pf "%a" pp 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] [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Context.Subst.pp s pp_raw q]
; ;
let 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 in
let xs, cong = Context.apply_subst (Var.Set.union q.us q.xs) s q.cong in let xs, ctx = Context.apply_subst (Var.Set.union q.us q.xs) s q.ctx in
exists_fresh xs {q with cong} exists_fresh xs {q with ctx}
|> |>
[%Trace.retn fun {pf} q' -> [%Trace.retn fun {pf} q' ->
pf "%a" pp_raw q' ; pf "%a" pp_raw q' ;
@ -693,9 +689,9 @@ let rec freshen_nested_xs q =
pf "%a" pp q' ; pf "%a" pp q' ;
invariant 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} -> [%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 *) (* extend vocabulary with variables in scope above *)
let ancestor_vs = Var.Set.union ancestor_vs (Var.Set.union q.us q.xs) in 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 = let xs, stem, djns =
(q.xs, {q with us= ancestor_vs; xs= emp.xs; djns= emp.djns}, q.djns) (q.xs, {q with us= ancestor_vs; xs= emp.xs; djns= emp.djns}, q.djns)
in in
(* strengthen equality relation with that from above *) (* strengthen context with that from above *)
let ancestor_stem = and_cong_ ancestor_cong stem in let ancestor_stem = and_ctx_ ancestor_ctx stem in
let ancestor_cong = ancestor_stem.cong in let ancestor_ctx = ancestor_stem.ctx in
exists xs exists xs
(List.fold djns ~init:ancestor_stem ~f:(fun q' djn -> (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 -> List.rev_map_unzip djn ~f:(fun dj ->
let dj = propagate_equality_ ancestor_vs ancestor_cong dj in let dj = propagate_context_ ancestor_vs ancestor_ctx dj in
(dj.cong, dj) ) (dj.ctx, dj) )
in in
let new_xs, djn_cong = Context.orN ancestor_vs dj_congs in let new_xs, djn_ctx = Context.orN ancestor_vs dj_ctxs in
(* hoist xs appearing in disjunction's equality relation *) (* hoist xs appearing in disjunction's context *)
let djn_xs = Var.Set.diff (Context.fv djn_cong) q'.us in 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 djn = List.map ~f:(elim_exists djn_xs) djn in
let cong_djn = and_cong_ djn_cong (orN djn) in let ctx_djn = and_ctx_ djn_ctx (orN djn) in
assert (is_false cong_djn || Var.Set.is_subset new_xs ~of_:djn_xs) ; assert (is_false ctx_djn || Var.Set.is_subset new_xs ~of_:djn_xs) ;
star (exists djn_xs cong_djn) q' )) star (exists djn_xs ctx_djn) q' ))
|> |>
[%Trace.retn fun {pf} q' -> [%Trace.retn fun {pf} q' ->
pf "%a" pp q' ; pf "%a" pp q' ;
invariant q'] invariant q']
let propagate_equality ancestor_vs ancestor_cong q = let propagate_context ancestor_vs ancestor_ctx q =
[%Trace.call fun {pf} -> [%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' -> [%Trace.retn fun {pf} q' ->
pf "%a" pp q' ; pf "%a" pp q' ;
@ -745,19 +741,19 @@ let remove_absent_xs ks q =
if Var.Set.is_empty ks then q if Var.Set.is_empty ks then q
else else
let xs = Var.Set.diff q.xs ks in 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 djns =
let rec trim_ks ks djns = let rec trim_ks ks djns =
List.map djns ~f:(fun djn -> List.map djns ~f:(fun djn ->
List.map djn ~f:(fun sjn -> List.map djn ~f:(fun sjn ->
{ sjn with { sjn with
us= Var.Set.diff sjn.us ks 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 } ) ) ; djns= trim_ks ks sjn.djns } ) )
in in
trim_ks ks q.djns trim_ks ks q.djns
in in
{q with xs; cong; djns} {q with xs; ctx; djns}
let rec simplify_ us rev_xss q = let rec simplify_ us rev_xss q =
[%Trace.call fun {pf} -> pf "%a@ %a" pp_vss (List.rev rev_xss) pp_raw 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)) ) orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn)) )
)) ))
in in
(* try to solve equations in cong for variables in xss *) (* try to solve equations in ctx for variables in xss *)
let subst = Context.solve_for_vars (us :: List.rev rev_xss) q.cong in let subst = Context.solve_for_vars (us :: List.rev rev_xss) q.ctx in
(* simplification can reveal inconsistency *) (* simplification can reveal inconsistency *)
( if is_false q then false_ q.us ( if is_false q then false_ q.us
else if Context.Subst.is_empty subst then q else if Context.Subst.is_empty subst then q
@ -784,7 +780,7 @@ let rec simplify_ us rev_xss q =
let removed = let removed =
Var.Set.diff Var.Set.diff
(Var.Set.union_list rev_xss) (Var.Set.union_list rev_xss)
(fv ~ignore_cong:() (elim_exists q.xs q)) (fv ~ignore_ctx:() (elim_exists q.xs q))
in in
let keep, removed, _ = Context.Subst.partition_valid removed subst in let keep, removed, _ = Context.Subst.partition_valid removed subst in
let q = and_subst keep q in let q = and_subst keep q in
@ -799,7 +795,7 @@ let simplify q =
[%Trace.call fun {pf} -> pf "%a" pp_raw q] [%Trace.call fun {pf} -> pf "%a" pp_raw q]
; ;
let q = freshen_nested_xs q in 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 let q = simplify_ q.us [] q in
q q
|> |>

17
sledge/src/sh.mli
Unescape View File

@ -17,7 +17,8 @@ type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
type starjunction = private type starjunction = private
{ us: Var.Set.t (** vocabulary / variable context of formula *) { us: Var.Set.t (** vocabulary / variable context of formula *)
; xs: Var.Set.t (** existentially-bound variables *) ; 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 *) ; pure: Term.t (** pure boolean constraints *)
; heap: seg list (** star-conjunction of segment atomic formulas *) ; heap: seg list (** star-conjunction of segment atomic formulas *)
; djns: disjunction list (** star-conjunction of disjunctions *) } ; djns: disjunction list (** star-conjunction of disjunctions *) }
@ -61,8 +62,8 @@ val pure : Term.t -> t
val and_ : Term.t -> t -> t val and_ : Term.t -> t -> t
(** Conjoin a boolean constraint to a formula. *) (** Conjoin a boolean constraint to a formula. *)
val and_cong : Context.t -> t -> t val and_ctx : Context.t -> t -> t
(** Conjoin constraints of a congruence to a formula, extending to a common (** Conjoin a context to that of a formula, extending to a common
vocabulary, and avoiding capturing existentials. *) vocabulary, and avoiding capturing existentials. *)
val and_subst : Context.Subst.t -> t -> t 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 val with_pure : Term.t -> t -> t
(** [with_pure pure q] is [{q with pure}], which assumes that [q.pure] and (** [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 [pure] are defined in the same vocabulary. Note that [ctx] is not
weakened, so if [pure] and [q.pure] do not induce the same congruence, weakened, so if [pure] and [q.pure] do not induce the same context, then
then the result will have a stronger [cong] than induced by its [pure]. *) the result will have a stronger [ctx] than induced by its [pure]. *)
val rem_seg : seg -> t -> t val rem_seg : seg -> t -> t
(** [star (seg s) (rem_seg s q)] is equivalent to [q], assuming that [s] is (** [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 *) (** Query *)
val is_emp : t -> bool 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 val is_false : t -> bool
(** Holds only of inconsistent formulas, does not hold of all inconsistent (** Holds only of inconsistent formulas, does not hold of all inconsistent
formulas. *) 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. *) (** Free variables, a subset of vocabulary. *)
val pure_approx : t -> t val pure_approx : t -> t

57
sledge/src/solver.ml
Unescape View File

@ -26,10 +26,9 @@ module Goal : sig
type t = private type t = private
{ us: Var.Set.t (** (universal) vocabulary of entire judgment *) { us: Var.Set.t (** (universal) vocabulary of entire judgment *)
; com: Sh.t (** common star-conjunct of minuend and subtrahend *) ; com: Sh.t (** common star-conjunct of minuend and subtrahend *)
; min: Sh.t ; min: Sh.t (** minuend, ctx strengthened by pure_approx (com * min) *)
(** minuend, cong strengthened by pure_approx (com * min) *)
; xs: Var.Set.t (** existentials over subtrahend and remainder *) ; 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 *) ; zs: Var.Set.t (** existentials over remainder *)
; pgs: bool (** indicates whether a deduction rule has been applied *) ; pgs: bool (** indicates whether a deduction rule has been applied *)
} }
@ -71,7 +70,7 @@ end = struct
Format.fprintf fs "@[<hv>%s %a@ | %a@ @[\\- %a%a@]@]" Format.fprintf fs "@[<hv>%s %a@ | %a@ @[\\- %a%a@]@]"
(if pgs then "t" else "f") (if pgs then "t" else "f")
Sh.pp com Sh.pp min Var.Set.pp_xs xs 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 sub
let invariant g = let invariant g =
@ -156,15 +155,15 @@ let excise_exists goal =
let solutions_for_xs = let solutions_for_xs =
let xs = let xs =
Var.Set.diff goal.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 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 in
if Context.Subst.is_empty solutions_for_xs then goal if Context.Subst.is_empty solutions_for_xs then goal
else else
let removed = let removed =
Var.Set.diff goal.xs 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 in
if Var.Set.is_empty removed then goal if Var.Set.is_empty removed then goal
else else
@ -183,7 +182,7 @@ let excise_exists goal =
let excise_pure ({min; sub} as goal) = let excise_pure ({min; sub} as goal) =
trace (fun {pf} -> pf "@[<2>excise_pure@ %a@]" pp 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 if Term.is_false pure' then None
else Some (goal |> with_ ~sub:(Sh.with_pure pure' sub)) 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 = let excise_seg_same ({com; min; sub} as goal) msg ssg =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.cong) pf "@[<hv 2>excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.ctx)
msg (Sh.pp_seg_norm sub.cong) ssg ) ; 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} = msg in
let {Sh.bas= b'; len= m'; seq= a'} = ssg in let {Sh.bas= b'; len= m'; seq= a'} = ssg in
let com = Sh.star (Sh.seg msg) com 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} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_sub_prefix@ %a@ \\- %a@]" pf "@[<hv 2>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.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 {Sh.bas= b'; len= m'; siz= n; seq= a'} = ssg in
let o_n = Term.integer o_n 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} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_min_prefix@ %a@ \\- %a@]" pf "@[<hv 2>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.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 {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
let n_o = Term.integer n_o 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} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_sub_suffix@ %a@ \\- %a@]" pf "@[<hv 2>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= 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 {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
let l_k = Term.integer l_k 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 = ko_ln =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_sub_infix@ %a@ \\- %a@]" pf "@[<hv 2>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= 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 {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
let l_k = Term.integer l_k 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 = ko_l ln_ko =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_min_skew@ %a@ \\- %a@]" pf "@[<hv 2>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= 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 {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
let l_k = Term.integer l_k 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} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_min_suffix@ %a@ \\- %a@]" pf "@[<hv 2>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.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 {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
let k_l = Term.integer k_l 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 = ln_ko =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_min_infix@ %a@ \\- %a@]" pf "@[<hv 2>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= 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 {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
let k_l = Term.integer k_l 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 = ln_k ko_ln =
excise (fun {pf} -> excise (fun {pf} ->
pf "@[<hv 2>excise_seg_sub_skew@ %a@ \\- %a@]" pf "@[<hv 2>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= 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 {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
let k_l = Term.integer k_l 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 *) (* C ❮ k-[b;m)->⟨o,α⟩ * M ⊢ ∃xs. l-[b';m')->⟨n,α'⟩ * S ❯ R *)
let excise_seg ({sub} as goal) msg ssg = let excise_seg ({sub} as goal) msg ssg =
trace (fun {pf} -> trace (fun {pf} ->
pf "@[<2>excise_seg@ %a@ |- %a@]" (Sh.pp_seg_norm sub.cong) msg pf "@[<2>excise_seg@ %a@ |- %a@]" (Sh.pp_seg_norm sub.ctx) msg
(Sh.pp_seg_norm sub.cong) ssg ) ; (Sh.pp_seg_norm sub.ctx) ssg ) ;
let {Sh.loc= k; bas= b; len= m; siz= o} = msg in 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 {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 if
(not (Context.entails_eq sub.cong b b')) (not (Context.entails_eq sub.ctx b b'))
|| not (Context.entails_eq sub.cong m m') || not (Context.entails_eq sub.ctx m m')
then then
Some Some
( goal ( goal
@ -578,11 +577,11 @@ let excise_seg ({sub} as goal) msg ssg =
| Neg -> ( | Neg -> (
let ko = Term.add k o in let ko = Term.add k o in
let ln = Term.add l n 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 match Int.sign (Z.sign ko_ln) with
(* k+o-(l+n) < 0 so k+o < l+n *) (* k+o-(l+n) < 0 so k+o < l+n *)
| Neg -> ( | 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 match Int.sign (Z.sign l_ko) with
(* l-(k+o) < 0 [k; o) (* l-(k+o) < 0 [k; o)
* so l < k+o ⊢ [l; n) *) * so l < k+o ⊢ [l; n) *)
@ -600,7 +599,7 @@ let excise_seg ({sub} as goal) msg ssg =
) )
(* k-l = 0 so k = l *) (* k-l = 0 so k = l *)
| Zero -> ( | 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 match Int.sign (Z.sign o_n) with
(* o-n < 0 [k; o) (* o-n < 0 [k; o)
* so o < n ⊢ [l; n) *) * so o < n ⊢ [l; n) *)
@ -615,7 +614,7 @@ let excise_seg ({sub} as goal) msg ssg =
| Pos -> ( | Pos -> (
let ko = Term.add k o in let ko = Term.add k o in
let ln = Term.add l n 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 match Int.sign (Z.sign ko_ln) with
(* k+o-(l+n) < 0 [k; o) (* k+o-(l+n) < 0 [k; o)
* so k+o < l+n ⊢ [l; n) *) * 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) | Zero -> Some (excise_seg_min_suffix goal msg ssg k_l)
(* k+o-(l+n) > 0 so k+o > l+n *) (* k+o-(l+n) > 0 so k+o > l+n *)
| Pos -> ( | 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 match Int.sign (Z.sign k_ln) with
(* k-(l+n) < 0 [k; o) (* k-(l+n) < 0 [k; o)
* so k < l+n ⊢ [l; n) *) * 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 -> List.find_map dnf_subtrahend ~f:(fun sub ->
[%Trace.call fun {pf} -> pf "@[<2>subtrahend@ %a@]" Sh.pp 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) excise (goal ~us ~com ~min ~xs ~sub ~zs ~pgs:true)
|> |>
[%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" Sh.pp)] ) [%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" Sh.pp)] )

Write Preview
Loading…
Cancel
Save