simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 04:14:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(th-data): fix acyclicity

Browse source
This commit is contained in:
Simon Cruanes 2020-02-20 19:32:33 -06:00
parent 4e1b35d2c3
commit 7cfdb3507c
2 changed files with 33 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/cc/Sidekick_cc.ml
View file

@ -166,7 +166,7 @@ module Make (A: CC_ARG)
| E_lit lit -> Lit.pp out lit | E_lit lit -> Lit.pp out lit
| E_congruence (n1,n2) -> Fmt.fprintf out "(@[congruence@ %a@ %a@])" N.pp n1 N.pp n2 | E_congruence (n1,n2) -> Fmt.fprintf out "(@[congruence@ %a@ %a@])" N.pp n1 N.pp n2
| E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b | E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b
| E_merge_t (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" Term.pp a Term.pp b | E_merge_t (a,b) -> Fmt.fprintf out "(@[<hv>merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b
| E_theory e -> Fmt.fprintf out "(@[th@ %a@])" pp e | E_theory e -> Fmt.fprintf out "(@[th@ %a@])" pp e
| E_and (a,b) -> | E_and (a,b) ->
Format.fprintf out "(@[<hv1>and@ %a@ %a@])" pp a pp b Format.fprintf out "(@[<hv1>and@ %a@ %a@])" pp a pp b

42
src/th-data/Sidekick_th_data.ml
View file

@ -374,20 +374,31 @@ module Make(A : ARG) : S with module A = A = struct
type node = { type node = {
repr: N.t; (* repr *) repr: N.t; (* repr *)
cstor_n: N.t; (* the cstor node *) cstor_n: N.t; (* the cstor node *)
cstor_args: repr list; (* arguments to [cstor_n] *) cstor_args: (N.t*repr) list; (* arguments to [cstor_n] *)
mutable flag: flag; mutable flag: flag;
} }
and flag = New | Open | Done (* for cycle detection *) and flag = New | Open | Done (* for cycle detection *)
type graph = node N_tbl.t type graph = node N_tbl.t
let pp_node out (n:node) =
Fmt.fprintf out "(@[node@ :repr %a@ :cstor_n %a@ @[:cstor_args %a@]@])"
N.pp n.repr N.pp n.cstor_n
Fmt.(Dump.list @@ hvbox @@ pair ~sep:(return "@ --> ") N.pp N.pp) n.cstor_args
let pp_path = Fmt.Dump.(list@@pair N.pp pp_node)
let pp_graph out (g:graph) : unit =
let pp_entry out (n,node) =
Fmt.fprintf out "@[<1>@[graph_node[%a]@]@ := %a@]" N.pp n pp_node node
in
Fmt.fprintf out "(@[graph@ %a@])" (Fmt.seq pp_entry) (N_tbl.to_iter g)
let mk_graph (self:t) cc : graph = let mk_graph (self:t) cc : graph =
let g: graph = N_tbl.create ~size:32 () in let g: graph = N_tbl.create ~size:32 () in
let traverse_sub cstor : repr list = let traverse_sub cstor : _ list =
IArray.to_list_map IArray.to_list_map
(fun sub_t -> (fun sub_t ->
let sub = SI.CC.find_t cc sub_t in let sub_n = SI.CC.add_term cc sub_t in
sub) sub_n, SI.CC.find cc sub_n)
cstor.Monoid_cstor.c_args cstor.Monoid_cstor.c_args
in in
begin begin
@ -409,26 +420,37 @@ module Make(A : ARG) : S with module A = A = struct
let cc = SI.cc solver in let cc = SI.cc solver in
(* create graph *) (* create graph *)
let g = mk_graph self cc in let g = mk_graph self cc in
Log.debugf 50
(fun k->k"(@[%s.acyclicity.graph@ %a@])" name pp_graph g);
(* traverse the graph, looking for cycles *) (* traverse the graph, looking for cycles *)
let rec traverse ~path (r:repr) : unit = let rec traverse ~path (n:N.t) (r:repr) : unit =
assert (N.is_root r); assert (N.is_root r);
match N_tbl.find g r with match N_tbl.find g r with
| exception Not_found -> () | exception Not_found -> ()
| {flag=Done; _} -> () (* no need *) | {flag=Done; _} -> () (* no need *)
| {flag=Open; _} -> | {flag=Open; cstor_n; _} as node ->
(* conflict: the [path] forms a cycle *) (* conflict: the [path] forms a cycle *)
let path = (n, node) :: path in
let expl = let expl =
List.map (fun node -> Expl.mk_merge node.cstor_n node.repr) path path
|> CCList.flat_map
(fun (n,node) ->
[ Expl.mk_merge node.cstor_n node.repr;
Expl.mk_merge n node.repr;
])
|> Expl.mk_list |> Expl.mk_theory |> Expl.mk_list |> Expl.mk_theory
in in
Log.debugf 5
(fun k->k "(@[%s.acyclicity.raise_confl@ %a@ @[:path %a@]@])"
name Expl.pp expl pp_path path);
SI.CC.raise_conflict_from_expl cc acts expl SI.CC.raise_conflict_from_expl cc acts expl
| {flag=New; _} as node_r -> | {flag=New; _} as node_r ->
node_r.flag <- Open; node_r.flag <- Open;
let path = node_r :: path in let path = (n, node_r) :: path in
List.iter (fun sub -> traverse ~path sub) node_r.cstor_args; List.iter (fun (sub_n,sub_r) -> traverse ~path sub_n sub_r) node_r.cstor_args;
node_r.flag <- Done; node_r.flag <- Done;
in in
N_tbl.iter (fun r _ -> traverse ~path:[] r) g; N_tbl.iter (fun r _ -> traverse ~path:[] r r) g;
() ()
end end