|
|
|
@ -28,8 +28,38 @@ type t = starjunction [@@deriving compare, equal, sexp]
|
|
|
|
let map_seg {loc; bas; len; siz; arr} ~f =
|
|
|
|
let map_seg {loc; bas; len; siz; arr} ~f =
|
|
|
|
{loc= f loc; bas= f bas; len= f len; siz= f siz; arr= f arr}
|
|
|
|
{loc= f loc; bas= f bas; len= f len; siz= f siz; arr= f arr}
|
|
|
|
|
|
|
|
|
|
|
|
let pp_seg ?is_x fs {loc; bas; len; siz; arr} =
|
|
|
|
let fold_terms_seg {loc; bas; len; siz; arr} ~init ~f =
|
|
|
|
let term_pp = Term.pp_full ?is_x in
|
|
|
|
let f b s = f s b in
|
|
|
|
|
|
|
|
f loc (f bas (f len (f siz (f arr init))))
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let fold_vars_seg seg ~init ~f =
|
|
|
|
|
|
|
|
fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let fold_vars fold_vars {us= _; xs= _; cong; pure; heap; djns} ~init ~f =
|
|
|
|
|
|
|
|
Equality.fold_terms ~init cong ~f:(fun init -> Term.fold_vars ~f ~init)
|
|
|
|
|
|
|
|
|> fun init ->
|
|
|
|
|
|
|
|
List.fold ~init pure ~f:(fun init -> Term.fold_vars ~f ~init)
|
|
|
|
|
|
|
|
|> fun init ->
|
|
|
|
|
|
|
|
List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init)
|
|
|
|
|
|
|
|
|> fun init ->
|
|
|
|
|
|
|
|
List.fold ~init djns ~f:(fun init -> List.fold ~init ~f:fold_vars)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let var_strength q =
|
|
|
|
|
|
|
|
let rec var_strength_ xs m q =
|
|
|
|
|
|
|
|
let xs = Set.union xs q.xs in
|
|
|
|
|
|
|
|
fold_vars (var_strength_ xs) {q with cong= Equality.true_} ~init:m
|
|
|
|
|
|
|
|
~f:(fun m var ->
|
|
|
|
|
|
|
|
if not (Set.mem xs var) then Map.set m ~key:var ~data:`Universal
|
|
|
|
|
|
|
|
else
|
|
|
|
|
|
|
|
match Map.find m var with
|
|
|
|
|
|
|
|
| None -> Map.set m ~key:var ~data:`Anonymous
|
|
|
|
|
|
|
|
| Some `Anonymous -> Map.set m ~key:var ~data:`Existential
|
|
|
|
|
|
|
|
| Some _ -> m )
|
|
|
|
|
|
|
|
in
|
|
|
|
|
|
|
|
var_strength_ Var.Set.empty Var.Map.empty q
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let pp_seg x fs {loc; bas; len; siz; arr} =
|
|
|
|
|
|
|
|
let term_pp = Term.ppx x in
|
|
|
|
Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" term_pp loc
|
|
|
|
Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" term_pp loc
|
|
|
|
(fun fs (bas, len) ->
|
|
|
|
(fun fs (bas, len) ->
|
|
|
|
if (not (Term.equal loc bas)) || not (Term.equal len siz) then
|
|
|
|
if (not (Term.equal loc bas)) || not (Term.equal len siz) then
|
|
|
|
@ -37,9 +67,10 @@ let pp_seg ?is_x fs {loc; bas; len; siz; arr} =
|
|
|
|
(bas, len) term_pp (Term.memory ~siz ~arr)
|
|
|
|
(bas, len) term_pp (Term.memory ~siz ~arr)
|
|
|
|
|
|
|
|
|
|
|
|
let pp_seg_norm cong fs seg =
|
|
|
|
let pp_seg_norm cong fs seg =
|
|
|
|
pp_seg fs (map_seg seg ~f:(Equality.normalize cong))
|
|
|
|
let x _ = None in
|
|
|
|
|
|
|
|
pp_seg x fs (map_seg seg ~f:(Equality.normalize cong))
|
|
|
|
|
|
|
|
|
|
|
|
let pp_block ?is_x fs segs =
|
|
|
|
let pp_block x fs segs =
|
|
|
|
let is_full_alloc segs =
|
|
|
|
let is_full_alloc segs =
|
|
|
|
match segs with
|
|
|
|
match segs with
|
|
|
|
| {loc; bas; len; _} :: _ -> (
|
|
|
|
| {loc; bas; len; _} :: _ -> (
|
|
|
|
@ -58,7 +89,7 @@ let pp_block ?is_x fs segs =
|
|
|
|
| _ -> false )
|
|
|
|
| _ -> false )
|
|
|
|
| [] -> false
|
|
|
|
| [] -> false
|
|
|
|
in
|
|
|
|
in
|
|
|
|
let term_pp = Term.pp_full ?is_x in
|
|
|
|
let term_pp = Term.ppx x in
|
|
|
|
let pp_mems =
|
|
|
|
let pp_mems =
|
|
|
|
List.pp "@,^" (fun fs seg ->
|
|
|
|
List.pp "@,^" (fun fs seg ->
|
|
|
|
term_pp fs (Term.memory ~siz:seg.siz ~arr:seg.arr) )
|
|
|
|
term_pp fs (Term.memory ~siz:seg.siz ~arr:seg.arr) )
|
|
|
|
@ -72,7 +103,7 @@ let pp_block ?is_x fs segs =
|
|
|
|
pp_mems segs
|
|
|
|
pp_mems segs
|
|
|
|
| [] -> ()
|
|
|
|
| [] -> ()
|
|
|
|
|
|
|
|
|
|
|
|
let pp_heap ?is_x ?pre cong fs heap =
|
|
|
|
let pp_heap x ?pre cong fs heap =
|
|
|
|
let bas_off = function
|
|
|
|
let bas_off = function
|
|
|
|
| Term.Add poly as sum ->
|
|
|
|
| Term.Add poly as sum ->
|
|
|
|
let const = Qset.count poly Term.one in
|
|
|
|
let const = Qset.count poly Term.one in
|
|
|
|
@ -81,92 +112,90 @@ let pp_heap ?is_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)]
|
|
|
|
(s1.bas, bas_off s1.loc)
|
|
|
|
( Equality.normalize cong s1.bas
|
|
|
|
(s2.bas, bas_off s2.loc)
|
|
|
|
, bas_off (Equality.normalize cong s1.loc) )
|
|
|
|
|
|
|
|
( Equality.normalize cong s2.bas
|
|
|
|
|
|
|
|
, bas_off (Equality.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 (Term.is_constant (Term.sub s2.loc s1.loc))
|
|
|
|
|| not (Equality.entails_eq cong (Term.add s1.loc s1.siz) s2.loc)
|
|
|
|
in
|
|
|
|
|
|
|
|
let blocks =
|
|
|
|
|
|
|
|
List.group ~break
|
|
|
|
|
|
|
|
(List.sort ~compare
|
|
|
|
|
|
|
|
(List.map ~f:(map_seg ~f:(Equality.normalize cong)) heap))
|
|
|
|
|
|
|
|
in
|
|
|
|
in
|
|
|
|
List.pp ?pre "@ * " (pp_block ?is_x) fs blocks
|
|
|
|
let heap = List.map heap ~f:(map_seg ~f:(Equality.normalize cong)) in
|
|
|
|
|
|
|
|
let blocks = List.group ~break (List.sort ~compare heap) in
|
|
|
|
|
|
|
|
List.pp ?pre "@ * " (pp_block x) fs blocks
|
|
|
|
|
|
|
|
|
|
|
|
let pp_us ?(pre = ("" : _ fmt)) fs us =
|
|
|
|
let pp_us ?(pre = ("" : _ fmt)) fs us =
|
|
|
|
if not (Set.is_empty us) then
|
|
|
|
if not (Set.is_empty us) then
|
|
|
|
[%Trace.fprintf fs "%( %)@[%a@] .@ " pre Var.Set.pp us]
|
|
|
|
[%Trace.fprintf fs "%( %)@[%a@] .@ " pre Var.Set.pp us]
|
|
|
|
|
|
|
|
|
|
|
|
let rec pp vs all_xs fs {us; xs; cong; pure; heap; djns} =
|
|
|
|
let rec pp_ ?var_strength vs parent_cong fs {us; xs; cong; pure; heap; djns}
|
|
|
|
|
|
|
|
=
|
|
|
|
Format.pp_open_hvbox fs 0 ;
|
|
|
|
Format.pp_open_hvbox fs 0 ;
|
|
|
|
let all_xs = Set.union all_xs xs in
|
|
|
|
let x v = Option.bind ~f:(fun m -> Map.find m v) var_strength in
|
|
|
|
let is_x var = Set.mem all_xs (Option.value_exn (Var.of_term var)) in
|
|
|
|
|
|
|
|
pp_us fs us ;
|
|
|
|
pp_us fs us ;
|
|
|
|
let xs_d_vs, xs_i_vs = Set.diff_inter xs vs in
|
|
|
|
let xs_d_vs, xs_i_vs =
|
|
|
|
|
|
|
|
Set.diff_inter
|
|
|
|
|
|
|
|
(Set.filter xs ~f:(fun v -> Poly.(x v <> Some `Anonymous)))
|
|
|
|
|
|
|
|
vs
|
|
|
|
|
|
|
|
in
|
|
|
|
if not (Set.is_empty xs_i_vs) then (
|
|
|
|
if not (Set.is_empty xs_i_vs) then (
|
|
|
|
Format.fprintf fs "@<2>∃ @[%a@] ." (Var.Set.pp_full ~is_x) xs_i_vs ;
|
|
|
|
Format.fprintf fs "@<2>∃ @[%a@] ." (Var.Set.ppx x) xs_i_vs ;
|
|
|
|
if not (Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ;
|
|
|
|
if not (Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ;
|
|
|
|
if not (Set.is_empty xs_d_vs) then
|
|
|
|
if not (Set.is_empty xs_d_vs) then
|
|
|
|
Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.pp_full ~is_x) xs_d_vs ;
|
|
|
|
Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ;
|
|
|
|
let first = Equality.is_true cong in
|
|
|
|
let first = Equality.entails parent_cong cong in
|
|
|
|
if not first then Format.fprintf fs " " ;
|
|
|
|
if not first then Format.fprintf fs " " ;
|
|
|
|
Equality.pp_classes ~is_x fs cong ;
|
|
|
|
Equality.pp_classes_diff x fs (parent_cong, cong) ;
|
|
|
|
let pure_terms =
|
|
|
|
let pure =
|
|
|
|
List.filter_map pure ~f:(fun e ->
|
|
|
|
List.filter_map pure ~f:(fun e ->
|
|
|
|
let e' = Equality.normalize cong e in
|
|
|
|
let e' = Equality.normalize cong e in
|
|
|
|
if Term.is_true e' then None else Some e' )
|
|
|
|
if Term.is_true e' then None else Some e' )
|
|
|
|
in
|
|
|
|
in
|
|
|
|
List.pp
|
|
|
|
List.pp
|
|
|
|
~pre:(if first then " " else "@ @<2>∧ ")
|
|
|
|
~pre:(if first then "@[ " else "@ @[@<2>∧ ")
|
|
|
|
"@ @<2>∧ " (Term.pp_full ~is_x) fs pure_terms ;
|
|
|
|
"@ @<2>∧ " (Term.ppx x) fs
|
|
|
|
let first = first && List.is_empty pure_terms in
|
|
|
|
(List.dedup_and_sort ~compare:Term.compare pure)
|
|
|
|
|
|
|
|
~suf:"@]" ;
|
|
|
|
|
|
|
|
let first = first && List.is_empty pure in
|
|
|
|
if List.is_empty heap then
|
|
|
|
if List.is_empty heap then
|
|
|
|
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
|
|
|
|
else pp_heap x ~pre:(if first then " " else "@ @<2>∧ ") cong fs heap ;
|
|
|
|
pp_heap ~is_x ~pre:(if first then " " else "@ @<2>∧ ") cong 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 "@ * ")
|
|
|
|
"@ * "
|
|
|
|
"@ * "
|
|
|
|
(pp_djn (Set.union vs (Set.union us xs)) all_xs)
|
|
|
|
(pp_djn ?var_strength (Set.union vs (Set.union us xs)) cong)
|
|
|
|
fs djns ;
|
|
|
|
fs djns ;
|
|
|
|
Format.pp_close_box fs ()
|
|
|
|
Format.pp_close_box fs ()
|
|
|
|
|
|
|
|
|
|
|
|
and pp_djn vs all_xs fs = function
|
|
|
|
and pp_djn ?var_strength:parent_var_strength vs cong fs = function
|
|
|
|
| [] -> Format.fprintf fs "false"
|
|
|
|
| [] -> Format.fprintf fs "false"
|
|
|
|
| djn ->
|
|
|
|
| djn ->
|
|
|
|
Format.fprintf fs "@[<hv>( %a@ )@]"
|
|
|
|
Format.fprintf fs "@[<hv>( %a@ )@]"
|
|
|
|
(List.pp "@ @<2>∨ " (fun fs sjn ->
|
|
|
|
(List.pp "@ @<2>∨ " (fun fs sjn ->
|
|
|
|
Format.fprintf fs "@[<hv 1>(%a)@]" (pp vs all_xs)
|
|
|
|
let var_strength =
|
|
|
|
|
|
|
|
let combine ~key sjn_v m_v =
|
|
|
|
|
|
|
|
if Set.mem sjn.xs key then sjn_v else m_v
|
|
|
|
|
|
|
|
in
|
|
|
|
|
|
|
|
Option.map
|
|
|
|
|
|
|
|
~f:(Map.merge_skewed ~combine (var_strength sjn))
|
|
|
|
|
|
|
|
parent_var_strength
|
|
|
|
|
|
|
|
in
|
|
|
|
|
|
|
|
Format.fprintf fs "@[<hv 1>(%a)@]"
|
|
|
|
|
|
|
|
(pp_ ?var_strength vs cong)
|
|
|
|
{sjn with us= Set.diff sjn.us vs} ))
|
|
|
|
{sjn with us= Set.diff sjn.us vs} ))
|
|
|
|
djn
|
|
|
|
djn
|
|
|
|
|
|
|
|
|
|
|
|
let pp = pp Var.Set.empty Var.Set.empty
|
|
|
|
let pp fs q =
|
|
|
|
let pp_djn = pp_djn Var.Set.empty Var.Set.empty
|
|
|
|
pp_ ~var_strength:(var_strength q) Var.Set.empty Equality.true_ fs q
|
|
|
|
|
|
|
|
|
|
|
|
let fold_terms_seg {loc; bas; len; siz; arr} ~init ~f =
|
|
|
|
|
|
|
|
let f b s = f s b in
|
|
|
|
|
|
|
|
f loc (f bas (f len (f siz (f arr init))))
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let fold_vars_seg seg ~init ~f =
|
|
|
|
|
|
|
|
fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let pp_djn fs d = pp_djn Var.Set.empty Equality.true_ fs d
|
|
|
|
let fv_seg seg = fold_vars_seg seg ~f:Set.add ~init:Var.Set.empty
|
|
|
|
let fv_seg seg = fold_vars_seg seg ~f:Set.add ~init:Var.Set.empty
|
|
|
|
|
|
|
|
|
|
|
|
let fold_vars fold_vars {us= _; xs= _; cong; pure; heap; djns} ~init ~f =
|
|
|
|
|
|
|
|
Equality.fold_terms ~init cong ~f:(fun init -> Term.fold_vars ~f ~init)
|
|
|
|
|
|
|
|
|> fun init ->
|
|
|
|
|
|
|
|
List.fold ~init pure ~f:(fun init -> Term.fold_vars ~f ~init)
|
|
|
|
|
|
|
|
|> fun init ->
|
|
|
|
|
|
|
|
List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init)
|
|
|
|
|
|
|
|
|> fun init ->
|
|
|
|
|
|
|
|
List.fold ~init djns ~f:(fun init -> List.fold ~init ~f:fold_vars)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let rec fv_union init q =
|
|
|
|
let rec fv_union init q =
|
|
|
|
Set.diff (fold_vars fv_union q ~init ~f:Set.add) q.xs
|
|
|
|
Set.diff (fold_vars fv_union q ~init ~f:Set.add) q.xs
|
|
|
|
|
|
|
|
|
|
|
|
|
Josh Berdine
5 years ago
committed by
Facebook Github Bot