clingo_interface

add_b2asp_error(Msg,Args) :-
    write(user_error,Msg), write(user_error,Args), nl(user_error).

add_b2asp_warning(Msg,Args) :-
    add_b2asp_error(Msg,Args).

answer_nr_rest([X|T]) --> digit(X), !, answer_nr_rest(T).

answer_nr_rest([]) --> "".

anything --> [_],!,anything.

anything --> "".

clingo_answer_line(Nr) --> "Answer: ",clingo_number(Nr), anything.

clingo_args([A|T]) --> clingo_constant(A),!, clingo_args2(T).

clingo_args([(A,B)|T]) --> clingo_pair(A,B),!, clingo_args2(T).

clingo_args2(T) --> ",", clingo_args(T).

clingo_args2([]) --> "".

clingo_atom(Pred,Args) --> clingo_identifier(Pred), clingo_opt_args(Args).

clingo_constant(A) --> clingo_number(A).

clingo_constant(A) --> clingo_identifier(A).

clingo_cst_or_pair(A) --> clingo_constant(A),!.

clingo_cst_or_pair((A,B)) --> "(", clingo_cst_or_pair(A),",", clingo_cst_or_pair(B),")".

clingo_identifier(ID) --> letter(H), !, id2(T), {atom_codes(ID,[H|T])}.

clingo_model(M) --> " ", !, clingo_model(M).

clingo_model(Model) --> clingo_atom(Pred,Args),!,
    %{format(user_output,' model atom --> ~w ~w~n',[Pred,Args])},
    {(clingo_generated_id(Pred,_,_,_) -> Model = [Pred-Args|T] ; Model = T)},
    clingo_model(T).

clingo_model([]) --> "".

clingo_number(Nr) --> digit(X), !, answer_nr_rest(R), {number_codes(Nr,[X|R])}.

clingo_number(MinusNr) --> "-", digit(X), !, answer_nr_rest(R), {number_codes(Nr,[X|R]),MinusNr is -Nr}.

clingo_opt_args(Args) --> "(", !, clingo_args(Args),")".

clingo_opt_args([]) --> "". % for propositions without arguments

clingo_pair(A,B) --> "(", clingo_cst_or_pair(A),!, ",", clingo_cst_or_pair(B),")".

debug_format(_,FS,A) :- format(user_output,FS,A).

debug_mode(on).

digit(X) :- X >= 48, X =< 57.

digit(X) --> [X], {digit(X)}.

digit_or_letter(X) --> [X], {letter(X) ; digit(X)}.

get_clingo_generated_id_with_arity(Pred,Arity) :-
    clingo_generated_id(Pred,_Kind,_BaseType,_ID),
    if(clingo_clause_head_info(Pred,A),Arity=A,
    (add_b2asp_warning('No clingo clause generated for: ',Pred),fail)).

get_clingo_path('C:/Users/hhuri/Desktop/stage/clingo-5.4.0-win64/clingo.exe').

get_clingo_path('/opt/homebrew/bin/clingo').

get_nr_of_registered_strings(Nr) :- string_counter(Nr).

get_sol([Sol|T],R) :- !, member(R,[Sol|T]).

get_sol(L,R) :- add_b2asp_error('Unexpected clingo solution: ',L), R=[].

get_string_nr(String,Nr) :- var(String),!,
    add_internal_error('String must be ground: ',get_string_nr(String,Nr)),
    string2nr(String,Nr).

get_string_nr(String,Nr) :-
    (string2nr(String,R) -> Nr=R
    ; retract(string_counter(R)), N1 is R+1,
    assert(string_counter(N1)),
    assert(string2nr(String,N1)),
    assert(nr2string(N1,String)),
    debug_format(19,' Registered string ~w --> ~w~n',[String,N1]),
    Nr=N1
).

id2([H|T]) --> digit_or_letter(H),!, id2(T).

id2([95|T]) --> "_",!, id2(T).

id2([]) --> "".

letter(X) :- (X >= 97, X =< 122) ; (X >= 65, X=< 90). % underscore = 95, minus = 45

letter(X) --> [X], {letter(X)}.

nr2string(0,'dummy_string').

process_clingo_model_line([[0'\n]|T],Nr,Models) :- !, process_clingo_model_line(T,Nr,Models).

process_clingo_model_line([ModelLine|T],Nr,[BSolution|TM]) :- clingo_model(Model,ModelLine,[]), !,
    debug_format(19,'>>> ~s~n',[ModelLine]),
    add_to_profile_stats(clingo_models,1),
    length(Model,Len),
    add_to_profile_stats(clingo_model_atoms,Len),
    (debug_mode(on)
    -> length(ModelLine,LenLine),
    format('Parsed clingo model ~w (length ~w) with ~w relevant atoms~n',[Nr,LenLine,Len])
    ;
    format('Parsed clingo model ~w with ~w relevant atoms~n',[Nr,Len])
    ),
    sort(Model,SModel), % TODO: extract solution for registered identifiers
    keyclumped(SModel,Groups),
    %write(Groups),nl,
    translate_clingo_model_to_bindings(Groups,BSolution),
    %write(BSolution),nl,
    process_clingo_output(T,TM).

process_clingo_model_line(T,Nr,Models) :-
    add_b2asp_error('Could not parse clingo model answer: ',Nr),
    process_clingo_output(T,Models).

process_clingo_output([],[]).

process_clingo_output([[0'\n]|T],Models) :- !, process_clingo_output(T,Models).

process_clingo_output([Line|T],Models) :- debug_format(19,'>>> ~s~n',[Line]),
    clingo_answer_line(Nr,Line,[]), !,
    process_clingo_model_line(T,Nr,Models).

process_clingo_output([_|T],Models) :- process_clingo_output(T,Models).

read_all(S,Command,Pipe,Lines) :-
    call_cleanup(read_all1(S,Command,Pipe,Lines),
    close(S)).

read_all1(S,Command,Pipe,Lines) :-
    catch(read_all2(S,Lines), error(_,E), ( % E could be system_error('SPIO_E_ENCODING_INVALID')
    ajoin(['Error reading ',Pipe,' for "',Command,'" due to exception: '],Msg),
    add_error(system_call,Msg,E),
    fail
)).

read_all2(S,Text) :-
    read_line(S,Line),
    ( Line==end_of_file -> Text=[[]]
    ;
    Text = [Line, [0'\n] | Rest],
    %debug_format(19,'Read line on stream ~w: ~s~n',[S,Line]),
    read_all2(S,Rest)).

register_clause_head(Pred,ArgList) :- %format(user_output,'Registering clause head ~w ~w~n',[Pred,ArgList]),
    clingo_generated_id(Pred,_Kind,_BaseType,_ID), % comment out for more stringent checking of arities for all preds
    length(ArgList,Arity),
    \+ clingo_clause_head_info(Pred,Arity),!,
    (clingo_clause_head_info(Pred,Other)
    -> add_b2asp_warning('Multiple arities for clingo predicate: ',Pred/Other) ; true),
    assert(clingo_clause_head_info(Pred,Arity)).

register_clause_head(_,_).

register_clingo_generated_id(Pred,Kind,BaseType,ID) :-
    debug_format(5,'~n** Registering clingo predicate ~w for ~w~n',[Pred,ID]),
    assertz(clingo_generated_id(Pred,Kind,BaseType,ID)).

reset_clingo_interface :-
    retractall(string_counter(_)),
    retractall(string2nr(_,_)),
    retractall(nr2string(_,_)),
    debug_format(9,'Reset clingo interface~n',[]),
    assert(string2nr('dummy_string',0)),
    assert(nr2string(0,'dummy_string')),
    assert(string_counter(0)),
    retractall(clingo_clause_head_info(_,_)),
    retractall(clingo_generated_id(_,_,_,_)).

run_clingo(File,Result) :- run_clingo(File,1,-1,_,Result,_).

run_clingo(File,MaxNrModels,TimeoutSecs,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)),
    (TimeoutSecs >= 0
    -> ajoin(['--time-limit=',TimeoutSecs],TimeOpt), TOpt = [TimeOpt|DOpt]
    ; TOpt=DOpt),
    OtherOptions = [ModelsOpt|TOpt] , % =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),
    debug_format(4,' Created process ~w~n',[Options]),flush_output,
    read_all(JStdout,Clingo,stdout,OutLines), % read before process_wait; avoid blocking clingo
    read_all(JStderr,Clingo,stderr,ErrLines),
    debug_format(4,' process_wait ~w~n',[Process]),flush_output,
    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,
    start_ms_timer(T1),
    process_clingo_output(OutLines,Models),
    get_elapsed_walltime(T1,WT1),add_to_profile_stats(back_translation_time,WT1),
    stop_ms_timer_with_msg(T1,'translating clingo model back to B'),
    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]),
    show_stderr(ErrLines)),
    (format('Unrecognised exit code: ~w~n',[Exit]),
    show_stderr(ErrLines),
    Result=no_solution_found(Exit))
).

safe_process_create(Cmd,Args,Opts) :- process_create(Cmd,Args,Opts).

show_stderr([]) :- !.

show_stderr(ErrLines) :-
    append(ErrLines,ErrText),
    (ErrText = [] -> true
    ; format('--- CLINGO STDERR ----~n~s~n',[ErrText])).

string2nr('dummy_string',0).

string_counter(0).

translate_clingo_arg(BaseType,[ClingoVal],BVal) :- translate_clingo_scalar(BaseType,ClingoVal,BVal).

translate_clingo_exit_code(0,_,no_solution_found('E_UNKNOWN'),non_exhaustive).

translate_clingo_exit_code(1,_,no_solution_found('E_INTERRUPT'),non_exhaustive). % can be timeout

translate_clingo_exit_code(33,_,no_solution_found('E_MEMORY'),non_exhaustive).

translate_clingo_exit_code(65,_,no_solution_found('E_ERROR'),non_exhaustive). % is for syntax error and unsafe vars

translate_clingo_exit_code(128,_,no_solution_found('E_NO_RUN'),non_exhaustive).

translate_clingo_exit_code(20,_,contradiction_found,exhaustive). % UNSATISFIABLE (E_EXHAUST)

translate_clingo_exit_code(10,Sols,solution(Sol),non_exhaustive) :-
    get_sol(Sols,Sol). % E_SAT = 10, /*!< At least one model was found.

translate_clingo_exit_code(30,Sols,solution(Sol),exhaustive) :-
    get_sol(Sols,Sol). %all_solutions_found (E_EXHAUST)

translate_clingo_model_to_bindings(Model,Bindings) :-
    findall(expected(Pred,Kind,BaseType,BID),clingo_generated_id(Pred,Kind,BaseType,BID),ExpectedPreds),
    sort(ExpectedPreds,SExpectedPreds),
    translate_clingo_model_to_bindings3(Model,SExpectedPreds,Bindings).

translate_clingo_model_to_bindings3([],[],Sol) :- !, Sol=[].

translate_clingo_model_to_bindings3([Pred-ModelArgs|TM],[expected(Pred,Kind,BaseType,BID)|ET],
    [bind(BID,BVal)|BT]) :- !,
    translate_clingo_value(Kind,BaseType,ModelArgs,BVal),
    translate_clingo_model_to_bindings3(TM,ET,BT).

translate_clingo_model_to_bindings3(Model,[expected(Pred,Kind,_BaseType,BID)|ET],
    [bind(BID,BVal)|BT]) :- !,
    (Kind=set
    -> debug_format(19,'Setting set to empty: ~w (~w)~n',[Pred,BID]),
    BVal=[] % the clingo identifier represents a set, we have no facts meaning the set is empty
    ; add_b2asp_error('No value for clingo scalar in model: ',Pred),
    BVal=term(undefined)
    ),
    translate_clingo_model_to_bindings3(Model,ET,BT).

translate_clingo_scalar(integer,Nr,BV) :- integer(Nr),!, BV=int(Nr).

translate_clingo_scalar(interval(_,_),Nr,BV) :- integer(Nr),!, BV=int(Nr).

translate_clingo_scalar(integer_in_range(_,_,Type),Nr,BV) :- integer(Nr),
    ( Type = integer -> !, BV=int(Nr)
    ; Type = string, nr2string(Nr,String), !, BV=string(String)).

translate_clingo_scalar(boolean,pred_false,BV) :- !, BV=pred_false.

translate_clingo_scalar(boolean,pred_true,BV) :- !, BV=pred_true.

translate_clingo_scalar(couple(TA,TB),(CA,CB),(BA,BB)) :- !,
    translate_clingo_scalar(TA,CA,BA),
    translate_clingo_scalar(TB,CB,BB).

translate_clingo_scalar(global(GS),Nr,FDVAL) :- integer(Nr),!, FDVAL=fd(Nr,GS).

translate_clingo_scalar(string,Nr,S) :- integer(Nr),nr2string(Nr,String), !, S=string(String).

translate_clingo_scalar(T,V,term(V)) :- add_b2asp_warning('Unknown clingo scalar: ',T:V).

translate_clingo_value(scalar,BaseType,[[ClingoVal]],BVal) :- !,
    translate_clingo_scalar(BaseType,ClingoVal,BVal).

translate_clingo_value(scalar,BaseType,[Sol1|T],BVal) :- !,
    add_b2asp_warning('Unexpected multiple solutions for clingo scalar: ',[Sol1|T]),
    translate_clingo_scalar(BaseType,Sol1,BVal).

translate_clingo_value(set,BaseType,Sols,BValSetAsList) :- !,
    maplist(translate_clingo_arg(BaseType),Sols,BValSetAsList).

translate_clingo_value(Kind,_,_,_) :-
    add_b2asp_error('Unexpected Kind for Clingo ID: ',Kind), fail.

write_clingo_show_directive :-
    findall(Pred/Arity,get_clingo_generated_id_with_arity(Pred,Arity),List),
    maplist(write_show,List).

write_show(Pred/Arity) :- format('#show ~w/~w.~n',[Pred,Arity]).