1 % (c) 2025-2026 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(clingo_interface,[run_clingo/2, run_clingo/6,
6 reset_clingo_interface/0,
7 clingo_generated_id/4,
8 register_clingo_generated_id/4, register_clause_head/2,
9 write_clingo_show_directive/0,
10 get_string_nr/2, get_nr_of_registered_strings/1, register_fresh_strings/1]).
11
12 :- use_module(probsrc(module_information),[module_info/2]).
13 :- module_info(group,b2asp).
14 :- module_info(description,'Running clingo on a file and parsing model output.').
15
16 :- use_module(library(lists)).
17 :- use_module(library(between),[between/3]).
18 :- use_module(library(file_systems),[file_exists/1]).
19 :- use_module(library(process)).
20
21
22 :- use_module(probsrc(error_manager)).
23 :- use_module(probsrc(tools_strings),[ajoin/2]).
24 :- use_module(probsrc(debug)).
25 :- use_module(probsrc(preferences)).
26 :- use_module(probsrc(system_call),[safe_process_create_with_diagnostics/4]).
27 get_clingo_path(Path) :- get_preference(path_to_clingo,Path).
28 add_b2asp_error(Msg,Args) :- add_error(b2asp,Msg,Args).
29 add_b2asp_warning(Msg,Args) :- add_warning(b2asp,Msg,Args).
30
31
32 :- use_module(probsrc(tools),[start_ms_timer/1, stop_ms_timer_with_msg/2, get_elapsed_walltime/2]).
33 :- use_module(covsrc(hit_profiler),[add_to_profile_stats/2]).
34
35 run_clingo(File,Result) :- run_clingo(File,1,-1,_,Result,_).
36 run_clingo(File,MaxNrModels,TimeoutSecs,WT,Result,Exhaustive) :-
37 statistics(walltime,[Start,_]),
38 % without debugging we suppress clingo's warnings (e.g., "info: atom does not occur in any rule head");
39 % there can be many of them, and if they fill the stderr pipe while we read stdout, clingo and ProB block
40 (debug_mode(on) -> DOpt=['-V'] ; DOpt=['--warn=none']),
41 (MaxNrModels<2 -> ModelsOpt='--models=1' % so that code works without ajoin
42 ; ajoin(['--models=',MaxNrModels],ModelsOpt)),
43 (TimeoutSecs >= 0
44 -> ajoin(['--time-limit=',TimeoutSecs],TimeOpt), TOpt = [TimeOpt|DOpt]
45 ; TOpt=DOpt),
46 OtherOptions = [ModelsOpt|TOpt] , % =0 outputs all models
47 debug_format(19,' Running CLINGO on ~w (options=~w)~n',[File,OtherOptions]),flush_output,
48 Options = [process(Process),stdout(pipe(JStdout,[encoding(utf8)])),
49 stderr(pipe(JStderr,[encoding(utf8)]))],
50 (get_clingo_path(Clingo), file_exists(Clingo)-> true
51 ; get_clingo_path(Clingo) -> add_b2asp_error('Cannot find Clingo binary at (be sure to set path_to_clingo preference to point to clingo binary): ',Clingo),fail
52 ; add_b2asp_error('Cannot find Clingo binary (be sure to set path_to_clingo preference to point to clingo binary)',''),fail
53 ),
54 safe_process_create_with_diagnostics(clingo,Clingo, [File|OtherOptions], Options),
55 debug_format(4,' Created process ~w~n',[Options]),flush_output,
56 catch(read_clingo_output(Process,Clingo,JStdout,JStderr,OutLines,ErrLines,Exit),
57 E,
58 (kill_clingo(Process),
59 catch(close(JStdout),_,true), catch(close(JStderr),_,true),
60 throw(E))), % e.g., user interrupt or ProB time-out
61 % above almost corresponds to: system_call_with_options(Clingo,[File|OtherOptions],[],OutLines,ErrLines,ExitCode)
62 % except that here we do not call append/2 on OutLines and ErrLines
63 statistics(walltime,[Stop,_]), WT is Stop-Start,
64 format(' CLINGO walltime: ~w ms, ~w~n',[WT,Exit]),flush_output,
65 debug_format(19,'--- CLINGO OUTPUT ----~n',[]),flush_output,
66 start_ms_timer(T1),
67 process_clingo_output(OutLines,Models),
68 get_elapsed_walltime(T1,WT1),add_to_profile_stats(back_translation_time,WT1),
69 stop_ms_timer_with_msg(T1,'translating clingo model back to B'),
70 if((Exit=exit(Code),
71 % ErrLines = [], % clingo write debug info on stderr (parsed program, rewritten program)
72 translate_clingo_exit_code(Code,Models,Result,Exhaustive)
73 ),
74 (debug_format(19,'Clingo exit code = ~w -> ~w (~w)~n',[Code,Result,Exhaustive]),
75 show_stderr(ErrLines)),
76 (format('Unrecognised exit code: ~w~n',[Exit]),
77 show_stderr(ErrLines),
78 Result=no_solution_found(Exit))
79 ).
80
81 read_clingo_output(Process,Clingo,JStdout,JStderr,OutLines,ErrLines,Exit) :-
82 read_all(JStdout,Clingo,stdout,OutLines), % read before process_wait; avoid blocking clingo
83 read_all(JStderr,Clingo,stderr,ErrLines),
84 debug_format(4,' process_wait ~w~n',[Process]),flush_output,
85 process_wait(Process,Exit).
86
87 % kill a clingo process which is still running, and release its resources
88 kill_clingo(Process) :-
89 catch(process_kill(Process),_,true),
90 catch(process_wait(Process,_,[timeout(1)]),_,true).
91
92 show_stderr([]) :- !.
93 show_stderr(ErrLines) :-
94 append(ErrLines,ErrText),
95 (ErrText = [] -> true
96 ; format('--- CLINGO STDERR ----~n~s~n',[ErrText])).
97
98 % see https://github.com/potassco/clasp/issues/42#issuecomment-459981038%3E
99 translate_clingo_exit_code(0,_,no_solution_found('E_UNKNOWN'),non_exhaustive).
100 translate_clingo_exit_code(1,_,no_solution_found('E_INTERRUPT'),non_exhaustive). % can be timeout
101 translate_clingo_exit_code(33,_,no_solution_found('E_MEMORY'),non_exhaustive).
102 translate_clingo_exit_code(65,_,no_solution_found('E_ERROR'),non_exhaustive). % is for syntax error and unsafe vars
103 translate_clingo_exit_code(128,_,no_solution_found('E_NO_RUN'),non_exhaustive).
104 translate_clingo_exit_code(20,_,contradiction_found,exhaustive). % UNSATISFIABLE (E_EXHAUST)
105 translate_clingo_exit_code(10,Sols,solution(Sol),non_exhaustive) :-
106 get_sol(Sols,Sol). % E_SAT = 10, /*!< At least one model was found.
107 translate_clingo_exit_code(11,Sols,solution(Sol),non_exhaustive) :-
108 get_sol(Sols,Sol). % E_SAT + E_INTERRUPT: models were found, but the search was interrupted, e.g., by --time-limit
109 translate_clingo_exit_code(30,Sols,solution(Sol),exhaustive) :-
110 get_sol(Sols,Sol). %all_solutions_found (E_EXHAUST)
111
112 get_sol([Sol|T],R) :- !, member(R,[Sol|T]).
113 get_sol(L,R) :- add_b2asp_error('Unexpected clingo solution: ',L), R=[].
114
115 %get_first_sol([Sol|_],R) :- !, R=Sol.
116 %get_first_sol(L,R) :- add_b2asp_error('Unexpected clingo solution: ',L), R=[].
117
118 % process clingo output stream and extract answers (stable models)
119 process_clingo_output([],[]).
120 process_clingo_output([[0'\n]|T],Models) :- !, process_clingo_output(T,Models).
121 process_clingo_output([Line|T],Models) :- debug_format(19,'>>> ~s~n',[Line]),
122 clingo_answer_line(Nr,Line,[]), !,
123 process_clingo_model_line(T,Nr,Models).
124 process_clingo_output([_|T],Models) :- process_clingo_output(T,Models).
125
126 process_clingo_model_line([[0'\n]|T],Nr,Models) :- !, process_clingo_model_line(T,Nr,Models).
127 process_clingo_model_line([ModelLine|T],Nr,[BSolution|TM]) :- clingo_model(Model,ModelLine,[]), !,
128 debug_format(19,'>>> ~s~n',[ModelLine]),
129 add_to_profile_stats(clingo_models,1),
130 length(Model,Len),
131 add_to_profile_stats(clingo_model_atoms,Len),
132 (debug_mode(on)
133 -> length(ModelLine,LenLine),
134 format('Parsed clingo model ~w (length ~w) with ~w relevant atoms~n',[Nr,LenLine,Len])
135 ;
136 format('Parsed clingo model ~w with ~w relevant atoms~n',[Nr,Len])
137 ),
138 sort(Model,SModel),
139 keyclumped(SModel,Groups),
140 %write(Groups),nl,
141 translate_clingo_model_to_bindings(Groups,BSolution),
142 %write(BSolution),nl,
143 process_clingo_output(T,TM).
144 process_clingo_model_line(T,Nr,Models) :-
145 add_b2asp_error('Could not parse clingo model answer: ',Nr),
146 process_clingo_output(T,Models).
147
148 % TRANSLATING clingo model atoms back to B values
149 % -----------------------------------------------
150
151 translate_clingo_model_to_bindings(Model,Bindings) :-
152 findall(expected(Pred,Kind,BaseType,BID),clingo_generated_id(Pred,Kind,BaseType,BID),ExpectedPreds),
153 sort(ExpectedPreds,SExpectedPreds),
154 translate_clingo_model_to_bindings3(Model,SExpectedPreds,Bindings).
155
156 translate_clingo_model_to_bindings3([],[],Sol) :- !, Sol=[].
157 translate_clingo_model_to_bindings3([Pred-ModelArgs|TM],[expected(Pred,Kind,BaseType,BID)|ET],
158 [bind(BID,BVal)|BT]) :- !,
159 translate_clingo_value(Kind,BaseType,ModelArgs,BVal),
160 translate_clingo_model_to_bindings3(TM,ET,BT).
161 translate_clingo_model_to_bindings3(Model,[expected(Pred,Kind,_BaseType,BID)|ET],
162 [bind(BID,BVal)|BT]) :- !,
163 (Kind=set
164 -> debug_format(19,'Setting set to empty: ~w (~w)~n',[Pred,BID]),
165 BVal=[] % the clingo identifier represents a set, we have no facts meaning the set is empty
166 ; add_b2asp_error('No value for clingo scalar in model: ',Pred),
167 BVal=term(undefined)
168 ),
169 translate_clingo_model_to_bindings3(Model,ET,BT).
170
171 % translate a solution for a clingo identifier back to a B value
172 translate_clingo_value(scalar,BaseType,[[ClingoVal]],BVal) :- !,
173 translate_clingo_scalar(BaseType,ClingoVal,BVal).
174 translate_clingo_value(scalar,BaseType,[Sol1|T],BVal) :- !,
175 add_b2asp_warning('Unexpected multiple solutions for clingo scalar: ',[Sol1|T]),
176 translate_clingo_scalar(BaseType,Sol1,BVal).
177 translate_clingo_value(set,BaseType,Sols,BValSetAsList) :- !,
178 maplist(translate_clingo_arg(BaseType),Sols,BValSetAsList).
179 translate_clingo_value(Kind,_,_,_) :-
180 add_b2asp_error('Unexpected Kind for Clingo ID: ',Kind), fail.
181
182 translate_clingo_arg(BaseType,[ClingoVal],BVal) :- translate_clingo_scalar(BaseType,ClingoVal,BVal).
183 % translate_clingo_arg(BaseType,[ClingoVal1,ClingoVal2],BVal) :- ... convert to B pairs
184
185 % translate a solution for a clingo scalar back to a B value
186 %translate_clingo_scalar(A,ID,FDVAL) :- write(translate_clingo_scalar(A,ID,FDVAL)),nl,trace,fail.
187 translate_clingo_scalar(integer,Nr,BV) :- integer(Nr),!, BV=int(Nr).
188 translate_clingo_scalar(interval(_,_),Nr,BV) :- integer(Nr),!, BV=int(Nr).
189 translate_clingo_scalar(integer_in_range(_,_,Type),Nr,BV) :- integer(Nr),
190 ( Type = integer -> !, BV=int(Nr)
191 ; Type = string, nr2string(Nr,String), !, BV=string(String)).
192 translate_clingo_scalar(boolean,pred_false,BV) :- !, BV=pred_false.
193 translate_clingo_scalar(boolean,pred_true,BV) :- !, BV=pred_true.
194 translate_clingo_scalar(couple(TA,TB),(CA,CB),(BA,BB)) :- !,
195 translate_clingo_scalar(TA,CA,BA),
196 translate_clingo_scalar(TB,CB,BB).
197 translate_clingo_scalar(global(GS),Nr,FDVAL) :- integer(Nr),!, FDVAL=fd(Nr,GS).
198 translate_clingo_scalar(string,Nr,S) :- integer(Nr),nr2string(Nr,String), !, S=string(String).
199 translate_clingo_scalar(T,V,term(V)) :- add_b2asp_warning('Unknown clingo scalar: ',T:V).
200
201 % PARSING CODE for clingo OUTPUT
202 % ---------------------
203 % detect line like Answer: 1 (Time: 0.003s)
204 clingo_answer_line(Nr) --> "Answer: ",clingo_number(Nr), anything.
205
206 clingo_number(Nr) --> digit(X), !, answer_nr_rest(R), {number_codes(Nr,[X|R])}.
207 clingo_number(MinusNr) --> "-", digit(X), !, answer_nr_rest(R), {number_codes(Nr,[X|R]),MinusNr is -Nr}.
208 answer_nr_rest([X|T]) --> digit(X), !, answer_nr_rest(T).
209 answer_nr_rest([]) --> "".
210
211 anything --> [_],!,anything.
212 anything --> "".
213
214 % a clingo identifier (TODO check that this conforms to clingo syntax)
215 clingo_identifier(ID) --> letter(H), !, id2(T), {atom_codes(ID,[H|T])}.
216 id2([H|T]) --> digit_or_letter(H),!, id2(T).
217 id2([95|T]) --> "_",!, id2(T).
218 id2([]) --> "".
219
220 % a single stable model generated by clingo, a list of ground atoms separated by single whitespace
221 clingo_model(M) --> " ", !, clingo_model(M).
222 clingo_model(Model) --> clingo_atom(Pred,Args),!,
223 %{format(user_output,' model atom --> ~w ~w~n',[Pred,Args])},
224 {(clingo_generated_id(Pred,_,_,_) -> Model = [Pred-Args|T] ; Model = T)},
225 clingo_model(T).
226 clingo_model([]) --> "".
227 %clingo_model(In,_Out) :- format(user_error,'Cannot parse: ~s~n',[In]),fail.
228
229 % a single clingo atom either a ground predicate p(2), p((2,3)), or p(2,3) or a proposition p
230 clingo_atom(Pred,Args) --> clingo_identifier(Pred), clingo_opt_args(Args).
231 clingo_opt_args(Args) --> "(", !, clingo_args(Args),")".
232 clingo_opt_args([]) --> "". % for propositions without arguments
233 clingo_args([A|T]) --> clingo_constant(A),!, clingo_args2(T).
234 clingo_args([(A,B)|T]) --> clingo_pair(A,B),!, clingo_args2(T).
235
236 clingo_constant(A) --> clingo_number(A).
237 clingo_constant(A) --> clingo_identifier(A).
238
239 clingo_args2(T) --> ",", clingo_args(T).
240 clingo_args2([]) --> "".
241
242 clingo_pair(A,B) --> "(", clingo_cst_or_pair(A),!, ",", clingo_cst_or_pair(B),")".
243
244 clingo_cst_or_pair(A) --> clingo_constant(A),!.
245 clingo_cst_or_pair((A,B)) --> "(", clingo_cst_or_pair(A),",", clingo_cst_or_pair(B),")".
246
247 digit_or_letter(X) --> [X], {letter(X) ; digit(X)}.
248 letter(X) --> [X], {letter(X)}.
249 digit(X) --> [X], {digit(X)}.
250 letter(X) :- (X >= 97, X =< 122) ; (X >= 65, X=< 90). % underscore = 95, minus = 45
251 digit(X) :- X >= 48, X =< 57.
252
253 % ---------
254
255 % read all characters from a stream
256 read_all(S,Command,Pipe,Lines) :-
257 call_cleanup(read_all1(S,Command,Pipe,Lines),
258 close(S)).
259 read_all1(S,Command,Pipe,Lines) :-
260 catch(read_all2(S,Lines), error(_,E), ( % E could be system_error('SPIO_E_ENCODING_INVALID')
261 ajoin(['Error reading ',Pipe,' for "',Command,'" due to exception: '],Msg),
262 add_error(clingo_interface,Msg,E),
263 fail
264 )).
265 read_all2(S,Text) :-
266 read_line(S,Line),
267 ( Line==end_of_file -> Text=[[]]
268 ;
269 Text = [Line, [0'\n] | Rest],
270 %debug_format(19,'Read line on stream ~w: ~s~n',[S,Line]),
271 read_all2(S,Rest)).
272
273 % ------------
274
275
276 :- dynamic clingo_generated_id/4, clingo_clause_head_info/2.
277
278 % register that Clingo predicate Pred represents a solution for a B variable ID
279 % Kind is set or scalar, BaseType is B type term
280 register_clingo_generated_id(Pred,Kind,BaseType,ID) :-
281 debug_format(5,'~n** Registering clingo predicate ~w for ~w~n',[Pred,ID]),
282 assertz(clingo_generated_id(Pred,Kind,BaseType,ID)).
283
284 % register that a clause has been generated for this clingo predicate
285 register_clause_head(Pred,ArgList) :- %format(user_output,'Registering clause head ~w ~w~n',[Pred,ArgList]),
286 clingo_generated_id(Pred,_Kind,_BaseType,_ID), % comment out for more stringent checking of arities for all preds
287 length(ArgList,Arity),
288 \+ clingo_clause_head_info(Pred,Arity),!,
289 (clingo_clause_head_info(Pred,Other)
290 -> add_b2asp_warning('Multiple arities for clingo predicate: ',Pred/Other) ; true),
291 assert(clingo_clause_head_info(Pred,Arity)).
292 register_clause_head(_,_).
293
294 get_clingo_generated_id_with_arity(Pred,Arity) :-
295 clingo_generated_id(Pred,_Kind,_BaseType,_ID),
296 if(clingo_clause_head_info(Pred,A),Arity=A,
297 (add_b2asp_warning('No clingo clause generated for: ',Pred),fail)).
298
299 % The #show directive allows you to filter what atoms are shown in the output.
300 write_clingo_show_directive :-
301 findall(Pred/Arity,get_clingo_generated_id_with_arity(Pred,Arity),List),
302 maplist(write_show,List).
303
304 write_show(Pred/Arity) :- format('#show ~w/~w.~n',[Pred,Arity]).
305
306
307 :- dynamic string_counter/1, string2nr/2, nr2string/2.
308 string_counter(0).
309 string2nr('dummy_string',0).
310 nr2string(0,'dummy_string').
311
312 get_nr_of_registered_strings(Nr) :- string_counter(Nr).
313
314 get_string_nr(String,Nr) :- var(String),!,
315 add_internal_error('String must be ground: ',get_string_nr(String,Nr)),
316 string2nr(String,Nr).
317 get_string_nr(String,Nr) :-
318 (string2nr(String,R) -> Nr=R
319 ; retract(string_counter(R)), N1 is R+1,
320 assert(string_counter(N1)),
321 assert(string2nr(String,N1)),
322 assert(nr2string(N1,String)),
323 debug_format(19,' Registered string ~w --> ~w~n',[String,N1]),
324 Nr=N1
325 ).
326
327
328
329 % make sure that at least Nr fresh strings are registered, i.e., strings not occurring in the formula:
330 % dummy_string (number 0) and dummy_string2, dummy_string3, ...
331 register_fresh_strings(Nr) :-
332 (between(2,Nr,I), ajoin([dummy_string,I],S), get_string_nr(S,_), fail ; true).
333
334 reset_clingo_interface :-
335 retractall(string_counter(_)),
336 retractall(string2nr(_,_)),
337 retractall(nr2string(_,_)),
338 debug_format(9,'Reset clingo interface~n',[]),
339 assert(string2nr('dummy_string',0)),
340 assert(nr2string(0,'dummy_string')),
341 assert(string_counter(0)),
342 retractall(clingo_clause_head_info(_,_)),
343 retractall(clingo_generated_id(_,_,_,_)).