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