1 % (c) 2019-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 :- module(bliss_interface, [init_bliss_interface/0,
5 init_directed_graph/0,
6 init_undirected_graph/0,
7 add_node/2,
8 add_node/3,
9 add_edge/2,
10 find_automorphisms/1,
11 get_canonical_form/1,
12 graph_to_dot_file/1]).
13
14 :- use_module(library(random), [random/3]).
15
16 %% find_automorphisms(-PermGroup).
17 % Find graph automorphisms yielding a permutation group,
18 % each permutation in the group is given by a generator which is represented in cycle notation.
19
20 %% get_canonical_form(-CanonicalForm).
21 % Fetch the canonical labeling of the graph in cycle notation.
22
23 foreign_resource('bliss_interface', [init_directed_graph_wrapper,
24 init_undirected_graph_wrapper,
25 add_node_wrapper,
26 add_edge_wrapper,
27 find_automorphisms,
28 get_canonical_form]).
29
30 foreign(init_directed_graph_wrapper, c, init_directed_graph_wrapper).
31 foreign(init_undirected_graph_wrapper, c, init_undirected_graph_wrapper).
32 foreign(add_node_wrapper, c, add_node_wrapper(+integer, [-integer])).
33 foreign(add_edge_wrapper, c, add_edge_wrapper(+integer, +integer)).
34 foreign(find_automorphisms, c, find_automorphisms([-term])).
35 foreign(get_canonical_form, c, get_canonical_form([-term])).
36
37 :- dynamic is_initialised/0, amount_of_nodes/1, dot_edge_atom/1, is_directed_graph/0, node_color/2, node_label/2, color_code/2.
38 :- volatile is_initialised/0, amount_of_nodes/1, dot_edge_atom/1, is_directed_graph/0, node_color/2, node_label/2, color_code/2.
39
40 %% init_bliss_interface.
41 init_bliss_interface :-
42 \+ is_initialised,
43 reset_state,
44 !,
45 Error = '~n! Could not load ~w library!~n! Check that it is available in the lib folder of ProB.~n~n',
46 catch(load_foreign_resource(library(bliss_interface)),_,
47 (format(user_error, Error, [library(bliss_interface)]), fail)),
48 asserta(is_initialised).
49 init_bliss_interface.
50
51 %% init_directed_graph.
52 % Clear graph and start creating a directed graph.
53 init_directed_graph :-
54 reset_state,
55 asserta(is_directed_graph),
56 init_directed_graph_wrapper.
57
58 %% init_undirected_graph.
59 % Clear graph and start creating an undirected graph.
60 init_undirected_graph :-
61 reset_state,
62 init_undirected_graph_wrapper.
63
64 %% add_node(+Color, -Id).
65 % Create a new node with the given colour and return the id.
66 add_node(Color, Id) :-
67 inc_nodes,
68 add_node_wrapper(Color, Id),
69 asserta(node_color(Id,Color)).
70
71 %% add_node(+Label, +Color, -Id).
72 % Label is used for dot graph visualization.
73 add_node(Label, Color, Id) :-
74 add_node(Color, Id),
75 asserta(node_label(Id,Label)).
76
77 %% add_edge(+Id1, +Id2).
78 % Create an edge between two ids.
79 add_edge(Id1, Id2) :-
80 amount_of_nodes(Nodes),
81 Id1 >= 0,
82 Id2 >= 0,
83 Id1 < Nodes,
84 Id2 < Nodes,
85 add_dot_edge_atom(Id1, Id2),
86 add_edge_wrapper(Id1, Id2).
87
88 %% graph_to_dot_file(+FilePath).
89 graph_to_dot_file(FilePath) :-
90 open(FilePath, write, S, [encoding(utf8)]),
91 dot_file_header(S),
92 dot_node_attributes(S),
93 dot_file_edges(S),
94 write(S, '}'),
95 close(S).
96
97 inc_nodes :-
98 retract(amount_of_nodes(Old)),
99 New is Old + 1,
100 asserta(amount_of_nodes(New)).
101
102 add_dot_edge_atom(Id1, Id2) :-
103 number_to_atom(Id1, AId1),
104 number_to_atom(Id2, AId2),
105 atom_concat(AId1, ' -> ', T1),
106 atom_concat(T1, AId2, T2),
107 atom_concat(T2, ';', DotEdgeAtom),
108 ( dot_edge_atom(DotEdgeAtom)
109 -> true
110 ; asserta(dot_edge_atom(DotEdgeAtom))
111 ).
112
113 reset_state :-
114 retractall(is_directed_graph),
115 retractall(amount_of_nodes(_)),
116 retractall(node_color(_,_)),
117 retractall(node_label(_,_)),
118 retractall(dot_edge_atom(_)),
119 asserta(amount_of_nodes(0)).
120
121 dot_node_attributes(S) :-
122 findall((Id,Color), node_color(Id, Color), NodeColors),
123 retractall(color_code(_,_)),
124 dot_node_attributes(NodeColors, S).
125
126 dot_node_attributes([], _).
127 dot_node_attributes([(Id,Color)|T], S) :-
128 get_color_code_for_id(Id, Color, ColorCode),
129 number_to_atom(Id, AId),
130 atom_concat(AId, ' [style="filled" color="', T1),
131 atom_concat(T1, ColorCode, T2),
132 ( node_label(Id, Label)
133 -> atom_concat(T2, '" label="', T3),
134 atom_concat(T3, Label, T4),
135 atom_concat(T4, '"]', DotNodeColor)
136 ; atom_concat(T2, '"]', DotNodeColor)
137 ),
138 write(S, DotNodeColor),
139 nl(S),
140 dot_node_attributes(T, S).
141
142 get_color_code_for_id(Id, Color, ColorCode) :-
143 node_color(Id, Color),
144 ( color_code(Color, TColorCode)
145 -> ColorCode = TColorCode
146 ; random(100000, 999999, RGB),
147 number_to_atom(RGB, ARGB),
148 atom_concat('#', ARGB, ColorCode),
149 asserta(color_code(Color, ColorCode))
150 ).
151
152 number_to_atom(Number, Atom) :-
153 number_codes(Number, C),
154 atom_codes(Atom, C).
155
156 dot_file_edges(S) :-
157 findall(DotEdgeAtom, dot_edge_atom(DotEdgeAtom), DotEdgeAtoms),
158 dot_file_edges(DotEdgeAtoms, S).
159
160 dot_file_edges([], _).
161 dot_file_edges([DotEdgeAtom|T], S) :-
162 write(S, DotEdgeAtom),
163 nl(S),
164 dot_file_edges(T, S).
165
166 dot_file_header(S) :-
167 is_directed_graph,
168 !,
169 write(S, 'digraph bliss_graph {'),
170 nl(S).
171 dot_file_header(S) :-
172 write(S, 'graph bliss_graph {'),
173 nl(S).