1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
type t = {
of_patterns: IntCollection.t Pattern.ObsMap.t;
of_unary_patterns: Mods.IntSet.t Mods.IntMap.t Pattern.ObsMap.t;
}
type mod_ccs_cache = (int, unit) Hashtbl.t
let empty env =
{
of_patterns =
Pattern.Env.new_obs_map (Model.domain env) (fun _ ->
IntCollection.create 64);
of_unary_patterns =
Pattern.Env.new_obs_map (Model.domain env) (fun _ -> Mods.IntMap.empty);
}
let state pattern matchings =
if IntCollection.is_empty (Pattern.ObsMap.get state.of_patterns pattern) then
Pattern.ObsMap.set state.of_patterns pattern matchings
let add_intset_in_intmap id set map =
if Mods.IntSet.is_empty set then
Mods.IntMap.remove id map
else
Mods.IntMap.add id set map
let break_apart_cc state edges ?mod_connectivity_store = function
| None -> ()
| Some (origin_cc, new_cc) ->
let () =
match mod_connectivity_store with
| None -> ()
| Some mod_conn ->
let () = Hashtbl.replace mod_conn new_cc () in
Hashtbl.replace mod_conn origin_cc ()
in
Pattern.ObsMap.iteri
(fun cc_id cc_map ->
let oset =
Mods.IntMap.find_default Mods.IntSet.empty origin_cc cc_map
in
if not (Mods.IntSet.is_empty oset) then (
let nset, oset' =
Mods.IntSet.partition
(fun x -> Edges.get_connected_component x edges = Some new_cc)
oset
in
Pattern.ObsMap.set state.of_unary_patterns cc_id
(add_intset_in_intmap new_cc nset
(add_intset_in_intmap origin_cc oset' cc_map))
))
state.of_unary_patterns
let merge_cc state ?mod_connectivity_store = function
| None -> ()
| Some (cc1, cc2) ->
let () =
match mod_connectivity_store with
| None -> ()
| Some mod_connectivity ->
let () = Hashtbl.replace mod_connectivity cc2 () in
Hashtbl.replace mod_connectivity cc1 ()
in
Pattern.ObsMap.iteri
(fun cc_id cc_map ->
match Mods.IntMap.pop cc2 cc_map with
| None, _ -> ()
| Some set2, cc_map' ->
let set1 = Mods.IntMap.find_default Mods.IntSet.empty cc1 cc_map in
Pattern.ObsMap.set state.of_unary_patterns cc_id
(add_intset_in_intmap cc1 (Mods.IntSet.union set1 set2) cc_map'))
state.of_unary_patterns
let update_roots state is_add unary_ccs edges mod_connectivity pattern root =
let va = Pattern.ObsMap.get state.of_patterns pattern in
let () =
(if is_add then
IntCollection.add
else
IntCollection.remove)
root va
in
if Pattern.Set.mem pattern unary_ccs then (
let cc_map = Pattern.ObsMap.get state.of_unary_patterns pattern in
let cc_id =
Option_util.unsome root (Edges.get_connected_component root edges)
in
let () = Hashtbl.replace mod_connectivity cc_id () in
let set = Mods.IntMap.find_default Mods.IntSet.empty cc_id cc_map in
let set' =
(if is_add then
Mods.IntSet.add
else
Mods.IntSet.remove)
root set
in
let cc_map' = add_intset_in_intmap cc_id set' cc_map in
Pattern.ObsMap.set state.of_unary_patterns pattern cc_map'
)
let number r pat = IntCollection.size (Pattern.ObsMap.get r.of_patterns pat)
let print_injections ~noCounters ?domain f roots_of_patterns =
Format.fprintf f "@[<v>%a@]"
(Pattern.ObsMap.print Pp.space (fun pattern f roots ->
if IntCollection.size roots > 0 then
Format.fprintf f "@[# @[%a@] ==>@ @[%a@]@]"
(Pattern.print ~noCounters ?domain ~with_id:true)
pattern IntCollection.print roots))
roots_of_patterns
let print_unary_injections ~noCounters ?domain f roots_of_patterns =
Format.fprintf f "@[<hov>%a@]"
(Pattern.ObsMap.print Pp.space (fun pattern f root_maps ->
Format.fprintf f "@[# @[%a@] ==>@ @[%a@]@]"
(Pattern.print ~noCounters ?domain ~with_id:true)
pattern
(Pp.set Mods.IntMap.bindings Pp.space (fun f (_cc_id, roots) ->
Mods.IntSet.print f roots))
root_maps))
roots_of_patterns
let debug_print f state =
let noCounters = true in
let domain = None in
let () = print_injections ~noCounters ?domain f state.of_patterns in
print_unary_injections ~noCounters ?domain f state.of_unary_patterns
let of_pattern pat_id state =
try Pattern.ObsMap.get state.of_patterns pat_id
with Not_found -> IntCollection.create 1
let of_unary_pattern pat_id state =
try Pattern.ObsMap.get state.of_unary_patterns pat_id
with Not_found -> Mods.IntMap.empty