1		% (c) 2009-2023 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