run_clingo(File,MaxNrModels,WT,Result,Exhaustive) :-
statistics(walltime,[Start,_]),
(debug_mode(on) -> DOpt=['-V'] ; DOpt=[]),
(MaxNrModels<2 -> ModelsOpt='--models=1' % so that code works without ajoin
; ajoin(['--models=',MaxNrModels],ModelsOpt)),
OtherOptions = [ModelsOpt|DOpt] , % =0 outputs all models
debug_format(19,' Running CLINGO on ~w (options=~w)~n',[File,OtherOptions]),flush_output,
Options = [process(Process),stdout(pipe(JStdout,[encoding(utf8)])),
stderr(pipe(JStderr,[encoding(utf8)]))],
(get_clingo_path(Clingo), file_exists(Clingo)-> true
; 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
; add_b2asp_error('Cannot find Clingo binary (be sure to set path_to_clingo preference to point to clingo binary)',''),fail
),
safe_process_create(Clingo, [File|OtherOptions], Options),
read_all(JStdout,Clingo,stdout,OutLines), % read before process_wait; avoid blocking clingo
read_all(JStderr,Clingo,stderr,ErrLines),
process_wait(Process,Exit),
% above almost corresponds to: system_call_with_options(Clingo,[File|OtherOptions],[],OutLines,ErrLines,ExitCode)
% except that here we do not call append/2 on OutLines and ErrLines
statistics(walltime,[Stop,_]), WT is Stop-Start,
format(' CLINGO walltime: ~w ms, ~w~n',[WT,Exit]),flush_output,
debug_format(19,'--- CLINGO OUTPUT ----~n',[]),flush_output,
process_clingo_output(OutLines,Models),
if((Exit=exit(Code),
% ErrLines = [], % clingo write debug info on stderr (parsed program, rewritten program)
translate_clingo_exit_code(Code,Models,Result,Exhaustive)),
debug_format(19,'Clingo exit code = ~w -> ~w (~w)~n',[Code,Result,Exhaustive]),
(append(ErrLines,ErrText),
format('STD-ERROR (~w):~n~s~n',[Exit,ErrText]),
Result=no_solution_found(Exit))
).