1 | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(graph_iso_nauty,[print_nauty_graph/1, | |
6 | nauty_init/0, nauty_clear/0, | |
7 | add_nauty_graph/2]). | |
8 | ||
9 | ||
10 | /* Translate a state graph, as produced by | |
11 | - into an format that can be input into dreadnaut | |
12 | - insert it directly into the C-Interface to nauty with its internal DB of canoncial forms | |
13 | */ | |
14 | :- use_module(module_information). | |
15 | ||
16 | :- module_info(group,symmetry). | |
17 | :- module_info(description,'Translate a state graph into a form for nauty and insert into internal DB of nauty C-interface.'). | |
18 | ||
19 | :- use_module(library(lists)). | |
20 | :- use_module(library(avl)). | |
21 | :- use_module(self_check). | |
22 | :- use_module(error_manager). | |
23 | :- use_module(tools_meta,[reraise_important_exception/1]). | |
24 | ||
25 | sorted_list_to_keylist([],_,[]). | |
26 | sorted_list_to_keylist([H|T],N,[H-N|KT]) :- N1 is N+1, sorted_list_to_keylist(T,N1,KT). | |
27 | slist_to_avl(List,AVL) :- | |
28 | sorted_list_to_keylist(List,1,KL), % assign each element a number, starting at 1 | |
29 | list_to_avl(KL,AVL). | |
30 | ||
31 | ||
32 | :- dynamic computed_label_colours/4. | |
33 | ||
34 | get_label_colours(SG,Cols,AVLCols,AVLRange,TotalNrLabelCols) :- | |
35 | (computed_label_colours(Cols,AVLCols,AVLRange,TotalNrLabelCols) -> true | |
36 | ; add_error_fail(graph_iso_nauty,'Could not get label colours',SG)). | |
37 | ||
38 | compute_label_colours :- | |
39 | retractall(computed_label_colours(_,_,_,_)), | |
40 | b_get_machine_variables(TypedVarList), | |
41 | b_get_machine_constants(TypedCstList), | |
42 | append(TypedCstList,TypedVarList,TL), | |
43 | convert_typed_varlist(TL,Cols,_Types), | |
44 | retractall(cst_var_colournr(_,_)), retractall(colornr_used(_)), | |
45 | generate_col_keylist(TL,3,KL,TotalNrLabelCols), % start at 3, because of $from and $to_el | |
46 | % TO DO: check if $from and $to_el are really required given types of variables,constants ! | |
47 | print(label_colours(Cols,KL,TotalNrLabelCols)),nl, | |
48 | list_to_avl(['$from'-1,'$to_el'-2|KL],AVLCols), %%print(AVLCols),nl, | |
49 | avl_range(AVLCols,AVLRange), | |
50 | assert(computed_label_colours(Cols,AVLCols,AVLRange,TotalNrLabelCols)). | |
51 | ||
52 | % copy form tcltk_interface.pl: | |
53 | convert_typed_varlist([],[],[]). | |
54 | convert_typed_varlist([b(identifier(ID),Type,_)|T],[ID|IT],[Type|TT]) :- | |
55 | convert_typed_varlist(T,IT,TT). | |
56 | ||
57 | ||
58 | :- dynamic cst_var_colournr/2, colornr_used/1. | |
59 | ||
60 | generate_col_keylist([],N,[],TotalNrLabelCols) :- TotalNrLabelCols is N-1. | |
61 | generate_col_keylist([b(identifier(ID),Type,_)|T],N,[ID-IDNr|KT],TotalNrLabelCols) :- | |
62 | (find_existing_colour(Type,IDNr) -> N1=N /* we can reuse an existing colour nr without conflict */ | |
63 | ; IDNr=N,N1 is N+1, | |
64 | assert(colornr_used(IDNr)) /* we need to use a new colour number; entailing a new level */ | |
65 | ), assert(cst_var_colournr(Type,IDNr)), | |
66 | generate_col_keylist(T,N1,KT,TotalNrLabelCols). | |
67 | ||
68 | find_existing_colour(Type,Nr) :- /* check whether an existing colour number can be used for a variable/constant with type Type */ | |
69 | colornr_used(Nr), | |
70 | \+ find_incompatible_type(Type,Nr). | |
71 | find_incompatible_type(Type,Nr) :- cst_var_colournr(Type2,Nr), | |
72 | incompatible_type(Type,Type2). | |
73 | ||
74 | % TO DO: Check and extend this !!!!!!!!!! | |
75 | % two different types may still be problematic if put onto the same level?? | |
76 | % especially since there are currently only 4 colours for abstract nodes ?! | |
77 | incompatible_type(T,T). | |
78 | incompatible_type(T,set(T)). %% membership arrow could conflict with = arrow; but only at top-level ?? | |
79 | incompatible_type(set(T),T). | |
80 | ||
81 | ||
82 | ||
83 | ||
84 | get_nodes(SG,Nodes,AVLNodes) :- | |
85 | findall(N,(sg_arc(Orig,_C,Dest,SG),(N=Orig;N=Dest)),Ns), | |
86 | sort(Ns,Nodes), | |
87 | slist_to_avl(Nodes,AVLNodes). | |
88 | %% sg_arc(Orig,arc,Dest, StateGraph) :- | |
89 | sg_arc(Orig,ArcColour,Dest, StateGraph) :- | |
90 | member((Orig,ArcColour,Dest),StateGraph). | |
91 | ||
92 | ||
93 | :- dynamic partition/3. | |
94 | print_nauty_graph(SG) :- nauty_initialised,!, | |
95 | get_graph_info(SG, Cols,AVLRange,NrCols,Nodes,AVLNodes,NrNodesPerLevel,TotalNodes,TSG), | |
96 | format('% LabelColors=~w=Levels, Nodes/Level=~w, Cols=~w\n',[NrCols,NrNodesPerLevel,Cols]), | |
97 | format('n=~w $=0 g\n',[TotalNodes]), | |
98 | print_nodes(AVLRange,Nodes,AVLNodes,NrNodesPerLevel,NrCols,TSG), | |
99 | print('$$'),nl, | |
100 | %get_node_colours(Nodes,NCols), | |
101 | % print(node_colors(NCols)),nl, | |
102 | print_partitions. | |
103 | print_nauty_graph(_). % don't print it; we don't have the necessary info | |
104 | %get_node_colours(Nodes,NCols) :- | |
105 | % findall(fd(NC), member(fd(_,NC),Nodes), NCs), sort(NCs, NCols1), | |
106 | % findall(NC2, (member(NC2,Nodes), NC2 \= fd(_,_)), NC2s), | |
107 | % sort(NC2s, NCols2),append(NCols1,NCols2,NCols). | |
108 | ||
109 | ||
110 | print_partitions :- /* print the starting partion: partition into every level plus in | |
111 | each level partition according to the node colours */ | |
112 | findall(part(Col,Type),partition(_,Col,Type),Ps), | |
113 | sort(Ps,Partitions), | |
114 | print('% Starting Partitions: '),print(Partitions),nl, | |
115 | print('f ['), | |
116 | print_part(Partitions), | |
117 | nl. | |
118 | ||
119 | ||
120 | print_part([]). | |
121 | print_part([part(Col,Type)|T]) :- | |
122 | findall(Id,partition(Id,Col,Type),Ids), | |
123 | sort(Ids,SIds), | |
124 | print_individual_part(SIds), | |
125 | (T=[] -> print(']') ; print(' | ')), | |
126 | print_part(T). | |
127 | ||
128 | print_individual_part([]). | |
129 | print_individual_part([H|T]) :- print(H), print_individual_part2(T). | |
130 | print_individual_part2([]). | |
131 | print_individual_part2([H|T]) :- print(', '),print(H), print_individual_part2(T). | |
132 | ||
133 | ||
134 | print_nodes(AVLRange,Nodes,AVLNodes,NrNodesPerLevel,NrCols,TSG) :- | |
135 | get_node(AVLRange,Nodes,AVLNodes,NrNodesPerLevel,NrCols,TSG, NrC,Node,ID,Successors), | |
136 | print_node(Node, NrC, ID, Successors), | |
137 | fail. | |
138 | print_nodes(_AVLRange,_Nodes,_AVLNodes,_NrNodes,_NrCols,_TSG). | |
139 | ||
140 | ||
141 | translate_state_graph([],_AVLCols,_AVLNodes,[]). | |
142 | translate_state_graph([(Node,Col,Dest)|T],AVLCols,AVLNodes,[(NrN,NrC,NrD)|TT]) :- | |
143 | avl_member(Node,AVLNodes,NrN), | |
144 | (avl_member(Col,AVLCols,NrC) -> true | |
145 | ; add_error(translate_state_graph,'Unknown Label: ',Col:AVLCols),NrC=1), | |
146 | avl_member(Dest,AVLNodes,NrD), | |
147 | translate_state_graph(T,AVLCols,AVLNodes,TT). | |
148 | ||
149 | /* get general info about a state graph : */ | |
150 | get_graph_info(StateGraph,Cols,AVLRange,TotalNrLabelCols, | |
151 | Nodes,AVLNodes,NrNodesPerLevel,TotalNodes,TranslatedStateGraph) :- | |
152 | get_label_colours(StateGraph,Cols,AVLCols,AVLRange,TotalNrLabelCols), | |
153 | get_nodes(StateGraph,Nodes,AVLNodes), | |
154 | length(Nodes,NrNodesPerLevel), | |
155 | TotalNodes is NrNodesPerLevel*TotalNrLabelCols, | |
156 | translate_state_graph(StateGraph,AVLCols,AVLNodes,TranslatedStateGraph),!. | |
157 | get_graph_info(StateGraph,_,_,_,_,_,_,_,_) :- | |
158 | add_error(graph_iso_nauty,'get_graph_info failed: ',StateGraph),fail. | |
159 | ||
160 | /* get a node, its colour, its ID and its successors : */ | |
161 | ||
162 | ||
163 | get_node(AVLRange,_Nodes,AVLNodes,NrNodesPerLevel,TotalNrLabelCols,TSG, | |
164 | NrofLabelColour,Node,NodeID,Successors) :- | |
165 | avl_member(Node,AVLNodes,NrN), | |
166 | restrict_sg_for_node(TSG,NrN,RestrictedTSG), | |
167 | member(NrofLabelColour,AVLRange), | |
168 | % print(nr(NrN,NrofLabelColour)),nl, | |
169 | ||
170 | NodeID is (NrofLabelColour-1)*NrNodesPerLevel+NrN-1, | |
171 | (NrofLabelColour>1 | |
172 | -> N1 is (NrofLabelColour-2)*NrNodesPerLevel+NrN-1, Successors = [N1|S2] | |
173 | /* add link to layer above */ | |
174 | ; Successors=S2), | |
175 | ||
176 | % S2=S3, /* add no link to layer above; seems to be much slower ! */ | |
177 | (NrofLabelColour<TotalNrLabelCols | |
178 | -> N2 is (NrofLabelColour)*NrNodesPerLevel+NrN-1, S2 = [N2|S3] | |
179 | /* add link to layer above */ | |
180 | ; S2=S3), | |
181 | ||
182 | findall( DestID, (member((NrN,NrofLabelColour,DestNr),RestrictedTSG), | |
183 | DestID is (NrofLabelColour-1)*NrNodesPerLevel+DestNr-1), S3). | |
184 | ||
185 | % translate a node into the corresponding id for the label colour, i.e. level | |
186 | % has been inlined above for performance reasons | |
187 | %get_node_id(NrOfNode,NrOfLabelColour, NrNodesPerLevel, NodeID) :- | |
188 | % NodeID is (NrOfLabelColour-1)*NrNodesPerLevel+NrOfNode-1. | |
189 | ||
190 | % ---------------------------------------------------------- | |
191 | ||
192 | restrict_sg_for_node([],_,[]). | |
193 | restrict_sg_for_node([(Nr,Col,Dest)|T],NodeNr,Res) :- | |
194 | (Nr = NodeNr -> Res = [(Nr,Col,Dest)|TR] ; Res=TR), | |
195 | restrict_sg_for_node(T,NodeNr,TR). | |
196 | ||
197 | :- assert_must_succeed(( graph_iso_nauty:get_subgraph([(1,2,3),(1,2,5),(1,4,1),(1,4,2),(2,1,1),(2,1,2)],Sub,N,C), N==2, C==1, Sub == [(2,1,2),(2,1,1)] )). | |
198 | ||
199 | get_subgraph(StateGraph,SubGraph,SubNode,SubCol) :- | |
200 | get_subgraph(StateGraph, [],_,_, SubGraph,SubNode,SubCol). | |
201 | ||
202 | get_subgraph([],SubGraph,Node,Col,SubGraph,Node,Col). | |
203 | get_subgraph([(Src,Col,Dest)|T], CurSubGraph,CurNode,CurCol, SubGraph,SubNode,SubCol) :- | |
204 | ((CurNode=Src, CurCol = Col) | |
205 | -> get_subgraph(T,[(Src,Col,Dest)|CurSubGraph],CurNode,CurCol,SubGraph,SubNode,SubCol) | |
206 | ; ( (SubGraph = CurSubGraph, SubNode=CurNode, SubCol=CurCol) | |
207 | ; | |
208 | get_subgraph(T, [(Src,Col,Dest)],Src,Col, SubGraph,SubNode,SubCol) | |
209 | ) | |
210 | ). | |
211 | ||
212 | % ---------------------------------------------------------- | |
213 | ||
214 | print_node(Node, NrC, ID, Successors) :- | |
215 | (Node = fd(_,Type) -> assert(partition(ID,NrC,fd(Type))) ; assert(partition(ID,NrC,Node))), | |
216 | print(' '), print(ID), print(' : '), | |
217 | member(DestID,Successors), | |
218 | print(DestID), print(' '), | |
219 | fail. | |
220 | print_node(_Node, _NrC, _ID, _Successors) :- print(';'),nl. | |
221 | ||
222 | ||
223 | /* ------------------------------------------------------- */ | |
224 | ||
225 | ||
226 | /* INTERFACE FOR ADDING GRAPHS TO OUR C-Library for NAUTY */ | |
227 | :- dynamic nauty_initialised/0. | |
228 | ||
229 | %nauty_use_module | |
230 | :- use_module(extension('nauty/graphiso'),[graphiso_init/0, | |
231 | prob_start_graph/1, | |
232 | prob_add_edge/2, | |
233 | prob_get_number_of_colours/1, | |
234 | prob_set_colour_of_node/2, | |
235 | prob_exists_graph/1, | |
236 | prob_free_storage/0]). | |
237 | ||
238 | nauty_init :- %%print(nauty_init),nl, | |
239 | initialise_node_colours, | |
240 | % nauty_use_module, | |
241 | (nauty_initialised -> print(prob_free_storage),nl, prob_free_storage | |
242 | ; assert(nauty_initialised) ), | |
243 | %% print(graphiso_init),nl, | |
244 | on_exception(Exception, graphiso_init, | |
245 | (add_error(nauty_init,'Exception during graphiso_init: ',Exception), | |
246 | reraise_important_exception(Exception),fail)), | |
247 | nr_of_node_colours_per_level(NrOfNodeColours), | |
248 | max_nr_of_label_colours(MaxNrOfLabelColours), | |
249 | MaxNrOfNodeColours is NrOfNodeColours * MaxNrOfLabelColours, | |
250 | %% print(prob_get_number_of_colours(MaxNrOfNodeColours,NrOfNodeColours)),nl, flush_output(user), %% | |
251 | nauty_clear, | |
252 | prob_get_number_of_colours(MaxNrOfNodeColours), | |
253 | assert(total_nr_of_node_colours(MaxNrOfNodeColours)), | |
254 | print(done),nl,flush_output(user), | |
255 | compute_label_colours. | |
256 | nauty_clear :- | |
257 | retractall(colour_overflow), | |
258 | retractall(total_nr_of_node_colours(_)), | |
259 | retractall(computed_label_colours(_,_,_,_)). | |
260 | ||
261 | ||
262 | :- use_module(bmachine,[b_get_machine_constants/1,b_get_machine_variables/1]). | |
263 | ||
264 | max_nr_of_label_colours(Nr) :- | |
265 | b_get_machine_constants(C), | |
266 | length(C,NrOfConstants), | |
267 | b_get_machine_variables(V), | |
268 | length(V,NrOfVars), | |
269 | NrOfExtraArrows = 2, /* '$from', '$to_el'*/ | |
270 | Nr is NrOfConstants+NrOfVars + NrOfExtraArrows. | |
271 | ||
272 | %nauty_reset :- prob_free_storage. | |
273 | ||
274 | :- dynamic nr_of_node_colours_per_level/1. | |
275 | nr_of_node_colours_per_level(5). | |
276 | ||
277 | :- dynamic total_nr_of_node_colours/1. | |
278 | total_nr_of_node_colours(5). | |
279 | ||
280 | :- dynamic node_fd_colour/3. | |
281 | :- dynamic colour_for_int0/1. | |
282 | :- volatile colour_for_int0/1. | |
283 | ||
284 | :- use_module(b_global_sets,[b_global_deferred_set/1, is_used_b_global_constant/3,is_unused_b_global_constant/3, | |
285 | b_partially_deferred_set/1]). | |
286 | :- use_module(preferences,[get_preference/2]). | |
287 | ||
288 | initialise_node_colours :- retractall(nr_of_node_colours_per_level(_)), retractall(node_fd_colour(_,_,_)), | |
289 | assert(nr_of_node_colours_per_level(8)), % start off with number 8 ( last abs_cn colour is 7) | |
290 | is_used_b_global_constant(Type,Nr,_Cst), | |
291 | retract(nr_of_node_colours_per_level(NC)), | |
292 | NC1 is NC+1, | |
293 | assert(nr_of_node_colours_per_level(NC1)), | |
294 | assert(node_fd_colour(Type,Nr,NC)), | |
295 | %% print(enum_colour(Type,Nr,NC,_Cst)),nl, %% | |
296 | fail. | |
297 | initialise_node_colours :- | |
298 | b_partially_deferred_set(Type), | |
299 | retract(nr_of_node_colours_per_level(NC)), | |
300 | NC1 is NC+1, | |
301 | assert(nr_of_node_colours_per_level(NC1)), | |
302 | is_unused_b_global_constant(Type,Nr,_), | |
303 | assert(node_fd_colour(Type,Nr,NC)), | |
304 | %% print(partial_enum_colour(Type,Nr,NC)),nl, %% | |
305 | fail. | |
306 | initialise_node_colours :- | |
307 | b_global_deferred_set(Type), | |
308 | retract(nr_of_node_colours_per_level(NC)), | |
309 | NC1 is NC+1, | |
310 | assert(nr_of_node_colours_per_level(NC1)), | |
311 | assert(node_fd_colour(Type,_,NC)), | |
312 | %% print(node_fd_colour(Type,'ANY',NC)),nl, %% | |
313 | fail. | |
314 | initialise_node_colours :- nr_of_node_colours_per_level(C), | |
315 | get_preference(minint,MININT), | |
316 | get_preference(maxint,MAXINT), | |
317 | CNew is C + MAXINT+1-MININT, | |
318 | CNewIncreased is CNew + 14, /* to allow numbers which are greater than MAXINT or smaller than MININT */ | |
319 | retract(nr_of_node_colours_per_level(_)), | |
320 | assert(nr_of_node_colours_per_level(CNewIncreased)), | |
321 | retractall(colour_for_int0(_)), | |
322 | assert(colour_for_int0(C)), | |
323 | print('Colours initialised: '), print(CNewIncreased),nl, flush_output(user). | |
324 | ||
325 | get_colour_of_node(X,C) :- var(X), !, | |
326 | add_error(get_colour_of_node,'Argument is var: ',get_colour_of_node(X,C)), | |
327 | fail. | |
328 | get_colour_of_node(sg_root,C) :- !, C=0. | |
329 | %get_colour_of_node('$Empty_Set',C) :- !, C=1. | |
330 | get_colour_of_node([],C) :- !, C=1. | |
331 | get_colour_of_node(pred_true /* bool_true */,Colour) :- !, Colour = 3. | |
332 | get_colour_of_node(pred_false /* bool_false */,Colour) :- !, Colour = 2. | |
333 | get_colour_of_node(abs_cn(_,AbsCol),Colour) :- !, Colour is 4 + (AbsCol mod 4). %% TO DO: make more flexible | |
334 | get_colour_of_node(fd(Nr,Type),Colour) :- !, node_fd_colour(Type,Nr,Colour). | |
335 | get_colour_of_node(int(Nr),Colour) :- !, colour_for_int0(Max), /* + number of cn's !!! */ | |
336 | (Nr>=0 -> Colour is Max+Nr*2 | |
337 | ; Colour is Max-1-(Nr*2) | |
338 | ). | |
339 | /* get_colour_of_node(global_set(_)) :- ADD ... */ | |
340 | get_colour_of_node(string(S),C) :- !, print(strings_not_supported_in_nauty(S)),nl, C=0. | |
341 | get_colour_of_node((_A,_B),Col) :- !, Col = 4. /* internal node; just like abs_cn(_,_) */ | |
342 | get_colour_of_node(avl_set(A),Col) :- !, print(avl_set_as_node(A)),nl, Col = 1. /* should be handled in state graph ! */ | |
343 | get_colour_of_node(Node,0) :- print(unknown_node(Node)),nl. | |
344 | ||
345 | ||
346 | /* add SG as nauty graph to the nauty C library and check if it already exists */ | |
347 | add_nauty_graph([],Exists) :- !, | |
348 | prob_start_graph(1), prob_set_colour_of_node(0,0), | |
349 | prob_exists_graph(Exists). | |
350 | add_nauty_graph(SG,Exists) :- | |
351 | get_graph_info(SG, _Cols,AVLRange, NrLabelCols, | |
352 | Nodes,AVLNodes,NrNodesPerLevel,TotalNodes,TSG), | |
353 | %% format('% LabelColors=~w=Levels, Nodes/Level=~w\n',[NrLabelCols,NrNodesPerLevel]), %% | |
354 | % nr_of_node_colours_per_level(NrOfNodeColours), | |
355 | % print(prob_get_number_of_colours(NrOfNodeColours)),nl, | |
356 | % prob_get_number_of_colours(NrOfNodeColours), | |
357 | %% nl,nl,print(prob_start_graph(TotalNodes)),nl, %% | |
358 | prob_start_graph(TotalNodes), | |
359 | add_nodes(AVLRange,Nodes,AVLNodes,NrNodesPerLevel,NrLabelCols,TSG), | |
360 | %print(prob_exists_graph(Exists)),nl, | |
361 | prob_exists_graph(Exists) | |
362 | .%,print(added_graph(SG,Exists)),nl,nl. | |
363 | ||
364 | ||
365 | ||
366 | :- dynamic colour_overflow/0. | |
367 | ||
368 | add_nodes(AVLRange,Nodes,AVLNodes,NrNodesPerLevel,TotalNrLabelCols,TSG) :- | |
369 | %% print(add_nodes(AVLRange,Nodes,AVLNodes,NrNodesPerLevel,TotalNrLabelCols,TSG)),nl, | |
370 | %% portray_avl(AVLNodes),nl, | |
371 | total_nr_of_node_colours(MaxNrOfNodeColours), | |
372 | get_node(AVLRange,Nodes,AVLNodes,NrNodesPerLevel, | |
373 | TotalNrLabelCols,TSG, NrOfLabelColour,Node,ID,Successors), | |
374 | (get_colour_of_node(Node,Colour) -> true | |
375 | ; add_error(add_nodes,'Call failed: ',get_colour_of_node(Node,Colour)),Colour=0), | |
376 | %% print(node(Node,Colour)),nl, %% | |
377 | RealColour is (Colour*TotalNrLabelCols + NrOfLabelColour-1), | |
378 | (RealColour >= MaxNrOfNodeColours | |
379 | -> (RealColour2 is RealColour mod MaxNrOfNodeColours, | |
380 | (colour_overflow -> true | |
381 | ; (assert(colour_overflow), | |
382 | add_error(graph_iso_nauty,'Warning: Colour overflow in Nauty Symmetry Library. Some symmetry classes may not be explored!!! Try and increase MAXINT.',RealColour)) | |
383 | )) | |
384 | ; RealColour2 = RealColour | |
385 | ), %print(prob_set_colour_of_node(ID,RealColour,nodec(Colour),level(NrOfLabelColour),nroflabelcolours(TotalNrLabelCols))),nl, flush_output(user),%% | |
386 | prob_set_colour_of_node(ID,RealColour2), | |
387 | member(DestID,Successors), | |
388 | %% print(prob_add_edge(ID,DestID)),nl, flush_output(user),%% | |
389 | prob_add_edge(ID,DestID), | |
390 | fail. | |
391 | add_nodes(_AVLRange,_Nodes,_AVLNodes,_NrNodes,_TotalNrLabelCols,_TSG). | |
392 | ||
393 | ||
394 | /* ------------------------------------------------------- */ | |
395 | /* TESTS */ | |
396 | ||
397 | /* | |
398 | state_graph([ | |
399 | (fd(2,'Code'),activec,sg_root), | |
400 | (fd(1,'Code'),activec,sg_root), | |
401 | (fd(2,'Name'),active,sg_root), | |
402 | (fd(1,'Name'),active,sg_root), | |
403 | (fd(2,'Name'),db,fd(1,'Code')), | |
404 | (fd(1,'Name'),db,fd(2,'Code')) | |
405 | ]). | |
406 | ||
407 | ||
408 | tn :- state_graph(SG), print_nauty_graph(SG). | |
409 | tn2 :- state_graph(SG), nauty_init, add_nauty_graph(SG,Ex), print(exists(Ex)),nl, | |
410 | add_nauty_graph(SG,Ex2), print(exists(Ex2)),nl. | |
411 | ||
412 | % graph_iso_nauty:bench. For Phonebook7 | |
413 | | ?- graph_iso_nauty:bench. | |
414 | bench_state_graph | |
415 | time_state_graph(0) | |
416 | time_nauty_wo_exists(2390) | |
417 | time_nauty(2670) | |
418 | sg_overhead_ratio(0.0) | |
419 | ||
420 | ||
421 | %:- assert_must_succeed( (graph_iso_nauty:state_graph(SG), graph_iso_nauty:nauty_init, | |
422 | % graph_iso_nauty:add_nauty_graph(SG,Ex), Ex== -1, | |
423 | % graph_iso_nauty:add_nauty_graph(SG,Ex2), Ex2==1, graph_iso_nauty:nauty_init)). | |
424 | ||
425 | ||
426 | ||
427 | bench :- bench(10000). | |
428 | bench(N) :- print(bench_state_graph),nl, | |
429 | statistics(runtime,[_,_]), | |
430 | sg(N,SG), | |
431 | statistics(runtime,[_,T1]), | |
432 | print(time_state_graph(T1)),nl, | |
433 | statistics(runtime,[_,_]), | |
434 | adw(N,SG), | |
435 | statistics(runtime,[_,T2]), | |
436 | print(time_nauty_wo_exists(T2)),nl, | |
437 | statistics(runtime,[_,_]), | |
438 | ad(N,SG), | |
439 | statistics(runtime,[_,T3]), | |
440 | print(time_nauty(T3)),nl, | |
441 | Ratio is T1/T3, print(sg_overhead_ratio(Ratio)),nl. | |
442 | ||
443 | sg(1,SG) :- !,state_graph(SG). | |
444 | sg(N,SG) :- state_graph(_), N1 is N-1, sg(N1,SG). | |
445 | ||
446 | adw(1,SG) :- !,add_nauty_graph(SG,_). | |
447 | adw(N,SG) :- add_nauty_graph_wo_check(SG), N1 is N-1, adw(N1,SG). | |
448 | ad(1,SG) :- !,add_nauty_graph(SG,_). | |
449 | ad(N,SG) :- add_nauty_graph(SG,_), N1 is N-1, ad(N1,SG). | |
450 | ||
451 | ||
452 | ||
453 | add_nauty_graph_wo_check(SG) :- | |
454 | get_graph_info(SG, _Cols,AVLRange, | |
455 | TotalNrLabelCols,Nodes,AVLNodes,NrNodesPerLevel,TotalNodes,TSG),!, | |
456 | % print(get_graph_info(SG, Cols,AVLCols,TotalNrLabelCols,Nodes,NrNodesPerLevel,TotalNodes)),nl, | |
457 | prob_start_graph(TotalNodes), | |
458 | add_nodes(AVLRange,Nodes,AVLNodes,NrNodesPerLevel,TotalNrLabelCols,TSG). | |
459 | ||
460 | ||
461 | bench3 :- prob_free_storage, graphiso_init, prob_get_number_of_colours(16), | |
462 | statistics(runtime,[_,_]), | |
463 | addg(X1), | |
464 | addg(X2), | |
465 | statistics(runtime,[_,T1]), | |
466 | print(time(T1,X1,X2)),nl. | |
467 | ||
468 | addg(X) :- | |
469 | prob_start_graph(15), | |
470 | prob_set_colour_of_node(8,6), | |
471 | prob_add_edge(8,3), | |
472 | prob_add_edge(8,13), | |
473 | prob_add_edge(8,5), | |
474 | ||
475 | prob_set_colour_of_node(6,6), | |
476 | prob_add_edge(6,1), | |
477 | prob_add_edge(6,11), | |
478 | prob_add_edge(6,5), | |
479 | ||
480 | prob_set_colour_of_node(4,5), | |
481 | prob_add_edge(4,9), | |
482 | prob_add_edge(4,0), | |
483 | ||
484 | prob_set_colour_of_node(2,5), | |
485 | prob_add_edge(2,7), | |
486 | prob_add_edge(2,0), | |
487 | ||
488 | prob_set_colour_of_node(14,5), | |
489 | prob_add_edge(14,9), | |
490 | prob_add_edge(14,13), | |
491 | ||
492 | prob_set_colour_of_node(12,5), | |
493 | prob_add_edge(12,7), | |
494 | prob_add_edge(12,11), | |
495 | ||
496 | prob_set_colour_of_node(0,0), | |
497 | prob_set_colour_of_node(1,0), | |
498 | prob_set_colour_of_node(3,0), | |
499 | prob_set_colour_of_node(5,0), | |
500 | prob_set_colour_of_node(7,0), | |
501 | prob_set_colour_of_node(9,0), | |
502 | prob_set_colour_of_node(10,0), | |
503 | prob_set_colour_of_node(11,0), | |
504 | prob_set_colour_of_node(13,0), | |
505 | ||
506 | prob_exists_graph(X). | |
507 | ||
508 | */ | |
509 | ||
510 | ||
511 | ||
512 |