
% main.pl
:- dynamic inputformula/3.
:-[modal_naive],[parse],[database],[read]. %[parse_tancs].

l:-[main].



t:- translate('test.alc',alc,dimacs).
q:- translate('galen-kris-1.alc',alc,dimacs).
r:- translate('p-qbf-cnfSSS-K4-C10-V16-D4.1',tancs,dimacs).
s:- translate('p-qbf-cnfSSS-K4-C40-V16-D6.8',tancs,dimacs).

solver(o,'/home/stuart/AKT/ALC-SAT/sato4.1/sato').
solver(z,'/home/stuart/AKT/ALC-SAT/SAT/zchaff.2001.2.17.linux').
%solver(z,'/home/stuart/AKT/ALC-SAT/zchaff/zchaff').

rand:-
    [tests],
    cd('./RAND'),
    repRand(1,501),
    cd.

repRand(X,X):-!.
repRand(X,Y):-
    nl,nl,write('Problem '),write(X),
    rtest(X),!,
    try_solve(o,X),!,
    XX is X + 1,
    repRand(XX,Y).

try_solve(O,I):-
    solver(O,S),
    concat_list([S,' dimacs_file',I,' > ',result,I],Cmd),
    shell(Cmd).
try_solve(_,_).

ttSATo(F,E):- 
    translate(F,tancs,dimacs,'dimacs_file',RewriteTime1,RewriteTime2,ConJ),!,
    try_solve(o),
    concat_list(['echo ttSAT file: ',F,' conjecture: ',ConJ,' > temp3'],Cmd0),
    shell(Cmd0),
    concat_list(['echo ttSAT rewrite time: ',RewriteTime1,' dimacs: ',RewriteTime2,' > temp2'],Cmd1),
    shell(Cmd1),
    concat_list(['cat temp3 temp2 temp1 > ',F,E],Cmd2),
    shell(Cmd2),
    shell('rm dimacs_file temp1 temp2 temp3'),!.

ttLWBo(F,E):- 
    translate(F,hAndS,dimacs,'dimacs_file',RewriteTime1,RewriteTime2,ConJ),!,
    try_solve(o),
    concat_list(['echo ttSAT file: ',F,' conjecture: ',ConJ,' > temp3'],Cmd0),
    shell(Cmd0),
    concat_list(['echo ttSAT rewrite time: ',RewriteTime1,' dimacs: ',RewriteTime2,' > temp2'],Cmd1),
    shell(Cmd1),
    concat_list(['cat temp3 temp2 temp1 > ',F,E],Cmd2),
    shell(Cmd2),
    shell('rm dimacs_file temp1 temp2 temp3'),!.

try_solve(O):-
    solver(O,S),
    concat_list([S,' dimacs_file > ',temp1],Cmd),
    shell(Cmd).
% sato fails, and leaves the file unfinish when problem is SAT
try_solve(_):- shell('rm unfinish'). 

try_solve(_).

ttSATz(F,E):-
    translate(F,tancs,dimacs,'dimacs_file',RewriteTime1,RewriteTime2,ConJ),!,
    solver(z,S),
    concat_list([S,' dimacs_file > ',temp1],Cmd),
    shell(Cmd),
    concat_list(['echo ttSAT file: ',F,' conjecture: ',ConJ,' > temp3'],Cmd0),
    shell(Cmd0),
    concat_list(['echo ttSAT rewrite time: ',RewriteTime1,' dimacs: ',RewriteTime2,' > temp2'],Cmd1),
    shell(Cmd1),
    concat_list(['cat temp3 temp2 temp1 > ',F,E],Cmd2),
    shell(Cmd2),
    shell('rm dimacs_file temp1 temp2 temp3'),!.

ttLWBz(F,E):-
    translate(F,hAndS,dimacs,'dimacs_file',RewriteTime1,RewriteTime2,ConJ),!,
    solver(z,S),
    concat_list([S,' dimacs_file > ',temp1],Cmd),
    shell(Cmd),
    concat_list(['echo ttSAT file: ',F,' conjecture: ',ConJ,' > temp3'],Cmd0),
    shell(Cmd0),
    concat_list(['echo ttSAT rewrite time: ',RewriteTime1,' dimacs: ',RewriteTime2,' > temp2'],Cmd1),
    shell(Cmd1),
    concat_list(['cat temp3 temp2 temp1 > ',F,E],Cmd2),
    shell(Cmd2),
    shell('rm dimacs_file temp1 temp2 temp3'),!.


translate(F,alc,dimacs):-
    retractall(defconcept(_,_)),retractall(defprimconcept(_,_)),retractall(prop(_)),
    retractall(dimacs_int(_,_)),
    read_alc_defs(F,Defs),!,          % Defs is ['(...)','(...)'...]
    repLispProlog(Defs,PDefs),!,      % convert defs to prolog terms
    assertDefs(PDefs),!,              % assert
    statistics(runtime,_),
    expandCDefs(PDefs,XConDefs),!,    % expand defconcepts (requires internal db of assertions)
    expandPDefs(PDefs,XPrimDefs),!,   % expand defprimconcepts (requires internal db of assertions)
    %write(XConDefs),nl,
    %write(XPrimDefs),
    append(XPrimDefs,XConDefs,XDefs),
    conjuctDefs(XDefs,Conj),!,        % make all defs into a conjunction; primitive defs => RHS; concept defs <= RHS
    rewrite(Conj,ClauseForm),!,       % convert to CF
    to_dimacs_db(ClauseForm,DIMACS),!,   % convert to DIMACS format
    write('c file is: '),write(F),nl,
    write_dimacs(DIMACS).


translate(F,tancs,dimacs,OPFile,Time1,Time2,CJ):-
    retractall(inputformula(_,_,_)),
    retractall(dimacs_int(_,_)),
    concat('../',tancs,OPS),
    [OPS],
    [F],                            % consult the tancs file, having made the wff into ''
    findall(I,inputformula(_,hypothesis,I),IL),!,
    get_conjecture(CJ),  % negate the conjecture - refutation proof
    repModalToALC(IL,ALCList),!,
    conjuctDefsTANCS(ALCList,Conj),!,
    statistics(runtime,_),   % time from here
    rewrite(Conj,ClauseForm),!,     % convert to CF
    statistics(runtime,[_,TimeMS1]),
    to_dimacs_db(ClauseForm,DIMACS),!, % convert to DIMACS format
    statistics(runtime,[_,TimeMS2]),
    Time1 is TimeMS1/1000,
    Time2 is TimeMS2/1000,
    tell(OPFile),
    write('c file is: '),write(F),nl,
    write('c conjecture is '),write(CJ),nl,
    write_dimacs(DIMACS),
    told.

translate(F,hAndS,dimacs,OPFile,Time1,Time2,CJ):-
    retractall(inputformula(_,_,_)),
    retractall(dimacs_int(_,_)),
    concat('../',hAndS,OPS),
    [OPS],
    [F],                            % consult the H and S file, having made the wff into ''
    inputformula(_,hypothesis,ConjH),
    inputformula(_,conjecture,CJ),  
    diaToALC(ConjH,Conj),!,
    %nl,nl,write(Conj),
    statistics(runtime,_),   % time from here naive rewrite opens the file....etc
    rewrite(not(Conj),OPFile),!,     % negate, convert to CF
    statistics(runtime,[_,TimeMS1]),
    Time1 is TimeMS1/1000,
    Time2  = Time1,!. %is TimeMS2/1000.

get_conjecture(I):-
    inputformula(_,conjecture,I),!.
get_conjecture(none).

% tancs - dimacs translation
repModalToALC([],[]):-!.
repModalToALC([I|J],[A|R]):-
    boxToALC(I,A),!,
    repModalToALC(J,R).
repModalToALC([I|_],_):-write('problem with this:'),write(I),nl,!,fail.

% tancs - dimacs translation
repHandSToALC([],[]):-!.
repHandSToALC([I|J],[A|R]):-
    diaToALC(I,A),!,
    repHandSToALC(J,R).
repHandSToALC([I|_],_):-write('problem with this:'),write(I),nl,!,fail.

boxToALC(K,all(R,FF)):-
    K =.. [box,L],
    L =.. [':',R,F],
    boxToALC(F,FF).
boxToALC(K,some(R,FF)):-
    K =.. [pos,L],
    L =.. [':',R,F],
    boxToALC(F,FF).
boxToALC(K,and(AA,BB)):-
    K =.. ['&',A,B],
    boxToALC(A,AA),
    boxToALC(B,BB).
boxToALC(K,or(AA,BB)):-
    K =.. ['|',A,B],
    boxToALC(A,AA),
    boxToALC(B,BB).
boxToALC(K,implies(AA,BB)):-
    K =.. ['=>',A,B],
    boxToALC(A,AA),
    boxToALC(B,BB).
boxToALC(K,not(AA)):-
    K =.. ['~',A],
    boxToALC(A,AA).

boxToALC(A,A).


diaToALC(K,all(r,FF)):-
    K =.. [box,F],
    diaToALC(F,FF).
diaToALC(K,some(r,FF)):-
    K =.. [dia,F],
    diaToALC(F,FF).
diaToALC(K,and(AA,BB)):-
    K =.. ['&',A,B],
    diaToALC(A,AA),
    diaToALC(B,BB).
diaToALC(K,or(AA,BB)):-
    K =.. ['v',A,B],
    diaToALC(A,AA),
    diaToALC(B,BB).
diaToALC(K,implies(AA,BB)):-
    K =.. ['->',A,B],
    diaToALC(A,AA),
    diaToALC(B,BB).
diaToALC(K,not(AA)):-
    K =.. ['~',A],
    diaToALC(A,AA).
diaToALC(A,A).

conjuctDefsTANCS([I],I):-!.
conjuctDefsTANCS([I|J],and(I,R)):-
    conjuctDefsTANCS(J,R).

% alc - dimacs translation

repLispProlog([],[]):-!.
repLispProlog([I|J],[P|R]):-
    lisp_to_prolog(I,P),
    repLispProlog(J,R).
repLispProlog([_|J],R):-
    repLispProlog(J,R).

assertDefs([]):-!.
assertDefs([defconcept(A,B)|J]):-!,
    assertz(defconcept(A,B)),
    assertDefs(J).
assertDefs([defprimconcept(A,B)|J]):-!,
    assertz(defprimconcept(A,B)),
    assertDefs(J).
assertDefs([_|J]):-
    assertDefs(J).

expandCDefs([],[]):-!.
expandCDefs([defconcept(A,Def)|J],[defconcept(A,NewDEF)|R]):-
    expand_definition(A,Def,NewDEF),
    test_assert(A,Def,NewDEF),
    expandCDefs(J,R).
expandCDefs([_|J],R):- % ignore everything else
    expandCDefs(J,R).

expandPDefs([],[]):-!.
expandPDefs([defprimconcept(A,Def)|J],[defprimconcept(A,NewDEF)|R]):-
    expand_definition(A,Def,NewDEF),
    expandPDefs(J,R).
expandPDefs([_|J],R):- % ignore everything else
    expandPDefs(J,R).
    
test_assert(_,Def,Def):-!.
test_assert(A,Def,NewDEF):-
    retract(defconcept(A,Def)),
    assertz(defconcept(A,NewDEF)).
    
% defprimconcept A B ::= A & (A  => B)
%     defconcept A B ::= A & (A <=> B)
%                    ::= A & (A <=  B)  & expand all defs A=>B

conjuctDefs([defprimconcept(A,B)],  and(A,implies(A,B))):-!.
conjuctDefs([defconcept(A,B)],      and(A,implies(B,A))):-!.
conjuctDefs([defprimconcept(A,B)|J],and(A,and(implies(A,B),P))):-
    conjuctDefs(J,P).
conjuctDefs([defconcept(A,B)|J],    and(A,and(implies(B,A),P))):-
    conjuctDefs(J,P).

concat_list([I],I):-!.
concat_list([I|J],S):-
    concat_list(J,R),
    concat(I,R,S).
