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