

% modal logic interpretation of ALC for SAT solving
% naive version - actually convert m,n,o variables in a clause into m * n * o clauses
% but move dimacs conversion into rewriting...

:- dynamic prop/1, vb/1, e/3, dimacs_int/2.

:- [modal_rewrite].
m:- [modal_naive].

% ALC: WFF = all(R, WFF); some(R,WFF); and(WFF,WFF); or(WFF,WFF); implies(WFF,WFF)
%      WFF = A,B,...
% 
% rewrite(ALC-WFF,Clause-Form)
% to_dimacs(Clause-Form,DIMACS-Clause-Form)
% write_dimacs(DIMACS-Clause-Form)
% rewrite(and(all(eats,animal),and(some(eats,veg),all(eats,or(meat,some(swims,river))))),P).
% rewrite(and(animal,all(eats,meat)),P), to_dimacs(P,Q),write_dimacs(Q).
% tancs_to_prolog('(box r1 : p)',P),boxToALC(P,Q),rewrite(Q,R),to_dimacs(R,S).
tancs_dimacs(F):- tancs_to_prolog(F,P),boxToALC(P,Q),rewrite(Q).

rewrite(WFF,OPF):-
    clean_db,
%trace,
    rewrite(WFF,0,[],CF,B),!,
    length(CF,Len),nl,write('no. non-ground clauses: '),write(Len),
    tell('dimacs_file_cl'),
    applyBindings(CF,B,CountCL,VBLLen,XLen),!,
    told,
    tell('dimacs_file_h'),
    write_header(CountCL),
    told,
    nl,write('no. ground clauses: '),write(CountCL),
    prop(Vars),
    nl,write('no. dimacs variables: '),write(Vars),
    nl,write('sets of bindings: '),write(VBLLen),
    nl,write('modal variables: '),write(XLen),
    concat('cat dimacs_file_h dimacs_file_cl > ',OPF,CMD),
    shell(CMD),
    shell('rm dimacs_file_h dimacs_file_cl'),!.

clean_db:-
	retractall(dimacs_int(_,_)),
	retractall(e(_,_,_)),
	retractall(vb(_)),
	assertz(vb(0)),
	retractall(prop(_)),
	assertz(prop(0)),!.

applyBindings(CL,B,CountCL,VBLLen,XLen):- %trace,
	getBind(B,VBL),
        swapVbInt,
        setup_dimacs,
	expand_Bindings(VBL,VBLL),
%	writeL(VBL),nl,writeL(VBLL),
	length(VBLL,VBLLen),
	member(X,VBLL),length(X,XLen),
	repApplyBindings(CL,VBLL,CountCL),!.

swapVbInt:-  % use vb to make new contexts
	retract(prop(I)),
	retractall(vb(_)),
	assertz(vb(I)),!.

getBind(BEL,VBL):-
	getFront(0,BEL,FR0),
	list_to_set(FR0,FR),
	getBdns(FR,FR,B1),
	list_to_set(B1,B2),
	expandFront(FR,BEL,B2,VBL),!.

expandFront([],_,R,R):-!.
expandFront(FR0,BEL,VBL,VBLR):-
	list_to_set(FR0,FR),
	getFrontTerms(FR,FRT),
	getFrontList(FRT,VBL,BEL,FR1),
	getBdns(FR1,FR1,B1),
	list_to_set(B1,B2),
	append(B2,VBL,VBL1),
	expandFront(FR1,BEL,VBL1,VBLR),!.
	
getFrontTerms([],[]):-!.
getFrontTerms([[T,_]|J],[T|Res]):-!,
	getFrontTerms(J,Res).

getFront(_,[],[]):-!.
getFront(C,[e(C,R,T)|J],[[T,R]|Res]):-
	getFront(C,J,Res),!.
getFront(C,[_|J],Res):-
	getFront(C,J,Res),!.

getFront(_,_,[],[]):-!.
getFront(C,VBL,[e(C,R,T)|J],[[T,R]|Res]):-
	getFront(C,VBL,J,Res),!.
getFront(C,VBL,[_|J],Res):-
	getFront(C,VBL,J,Res),!.


getFrontList([],_,_,[]):-!.
getFrontList([I|J],VBL,BEL,Res):-
	getFront(I,VBL,BEL,FR1),
	list_to_set(FR1,FR2),
	getFrontList(J,VBL,BEL,FR3),!,
	append(FR2,FR3,Res),!.

getBdns([],_,[]):-!.
getBdns([[v(V),R]|J],L,[[v(V),BL]|Res]):-
	repGetBdns(R,L,BL),
	getBdns(J,L,Res),!.
getBdns([_|J],L,Res):-
	getBdns(J,L,Res),!.

repGetBdns(_,[],[]):-!.
repGetBdns(R,[[v(_),_]|J],Res):-
	repGetBdns(R,J,Res),!.
repGetBdns(R,[[T,R]|J],[T|Res]):-!,
	repGetBdns(R,J,Res),!.
repGetBdns(R,[_|J],Res):-
	repGetBdns(R,J,Res),!.

eTerm(e(I,J,K)):-
	e(I,J,K).

gndTerm([]):-!.
gndTerm(f(_I,J)):- !,gndTerm(J),!.
gndTerm(I):- integer(I),!.


memberCut([v(V),L],VBL):-
	member([v(V),L],VBL),!.


expand_Bindings(VBL,VBLL):-
	splitGnd(VBL,CBL,VBLR),!,
	expandBindings(VBLR,CBL,VBLL),!.


splitGnd([],[],[]):-!.
splitGnd([[v(_V),[]]|VBL],G,NG):-!,
	splitGnd(VBL,G,NG),!.
splitGnd([[v(V),[L]]|VBL],[[v(V),L]|G],NG):-
	gndTerm(L),!,
	splitGnd(VBL,G,NG),!.
splitGnd([[v(V),L]|VBL],G,[[v(V),L]|NG]):-!,
	splitGnd(VBL,G,NG),!.
	
expandBindings([],R,[R]):-!.

expandBindings([[v(V),[I]]|VBL],CBL,VBLL):-
	makeGnd(I,CBL,II),!,
%	write(v(V)),write('='),write(II),nl,
	expandBindings(VBL,[[v(V),II]|CBL],VBLL),!.

expandBindings([[v(V),[I]]|VBL],CBL,VBLL):-
	append(VBL,[[v(V),[I]]],VBL1),
	expandBindings(VBL1,CBL,VBLL),!.
	
expandBindings([[v(V),L]|VBL],CBL,VBLL):-
	repExpandBindings(VBL,v(V),L,CBL,VBLL),!.

repExpandBindings(_,_,[],_,[]):-!.
repExpandBindings(VBL,v(V),[I|J],CBL,VBLL):-
	expandBindings([[v(V),[I]]|VBL],CBL,VBLL0),
	repExpandBindings(VBL,v(V),J,CBL,VBLL1),!,
	append(VBLL0,VBLL1,VBLL),!.

makeGnd(I,_,I):-
	gndTerm(I),!.
makeGnd(v(V),CBL,I):-
	member([v(V),I],CBL),!.
makeGnd(f(X,T),CBL,f(X,I)):-
	makeGnd(T,CBL,I),!.

gndListList([],[]):-!.
gndListList([I|J],[I|R]):- gndList(I),!,gndListList(J,R),!.
gndListList([_I|J],R):- 
%	write('free var in: '),write(I),nl,
	gndListList(J,R),!.

gndList([]):-!.
gndList([[_,I]|J]):-!,
    gndTerm(I),!,
    gndList(J).
gndList([I|J]):-
    gndTerm(I),!,
    gndList(J).

repApplyBindings([],_,0):-!.
repApplyBindings([I|J],VBLL,ResO):- 
	subVBLL(VBLL,I,I1),!,        % apply bindings to each clause
	list_to_set(I1,I2),!,
	gndListList(I2,I3),!,
        length(I3,LenII),
%        writeL(I3),nl,
        to_dimacs_db(I3),!,           % reduce memory overhead - write dimacs here
	repApplyBindings(J,VBLL,Res),!,
        ResO is LenII + Res,!.


subVBLL([],_,[]):-!.
subVBLL([SL|VBLL],CL,[CLL|R]):-
	repSubVBL(SL,CL,CLL),!,
	subVBLL(VBLL,CL,R),!.

repSubVBL([],R,R):-!.
repSubVBL([[V,T]|L],CL,CLR):-
	sub(T,V,CL,CL0),!,
	repSubVBL(L,CL0,CLR),!.


sub(_,_,[],[]):-!.
sub(I,V,[[P,T]|L],[[P,TT]|R]):-
	matches(I,V,T,TT),!,
	sub(I,V,L,R).
sub(I,V,[[P,X]|L],[[P,X]|R]):-!,
    sub(I,V,L,R).

matches(I,v(V),v(V),I):-!.
matches(I,v(V),f(X,T),f(X,TT)):-
	matches(I,v(V),T,TT),!.


% convert from symbolic propositional cnf to integer format
% i.e. each prop is an integer 1...prop(I)
% incidently, delete duplicate literals from a clause

setup_dimacs:-
	retractall(prop(_)),
	assertz(prop(0)),!.
    

to_dimacs_db(A):-
	to_dimacs_db_rep(A,B),!,
        write_dimacs(B),!.

to_dimacs_db_rep([],[]):-!.
to_dimacs_db_rep([A|B],[AA|BB]):-
    to_dimacs_clause(A,AA),
    to_dimacs_db_rep(B,BB).


dimacs_lookup([not(A),X],B):-!,
	dimacs_int([A,X],_AA),!,
        member([not(A),X],B),!.

dimacs_lookup([A,X],B):-!,
	dimacs_int([A,X],_AA),!,
        member([A,X],B),!.

to_dimacs_clause([],[]):-!.

to_dimacs_clause([A|B],BB):-
	dimacs_lookup(A,B),!, % there is a dimacs int and A occurs in B
	to_dimacs_clause(B,BB).

to_dimacs_clause([[not(A),X]|B],[not(AA)|BB]):-
	dimacs_int([A,X],AA),!,
	to_dimacs_clause(B,BB).
	
to_dimacs_clause([[A,X]|B],[AA|BB]):-
	dimacs_int([A,X],AA),!,
	to_dimacs_clause(B,BB).
	
to_dimacs_clause([[not(A),X]|B],[not(I)|BB]):-
	next_int(I),!,
        assertz(dimacs_int([A,X],I)),
	to_dimacs_clause(B,BB).

to_dimacs_clause([[A,X]|B],[I|BB]):-
	next_int(I),!,
        assertz(dimacs_int([A,X],I)),
	to_dimacs_clause(B,BB).


write_dimacs(I):-
    write_dimacs_list(I).

write_header(CountCL):-
    prop(P),
    write('c an ALC problem'),nl,
    write('p cnf '),write(P),write(' '),write(CountCL),nl.

/*
    write_dimacs_list(I,_Sum).
    nl,nl,
    write('no. clauses:    '), write(Len),nl,
    write('no. variables:  '), write(P),nl,
    Ave is Sum/Len,
    write('ave. var/clause:'), write(Ave),nl.
	*/

write_dimacs_list([]):-!.
write_dimacs_list([I|J]):-
    write_dimacs_clause(I),
    write_dimacs_list(J).

write_dimacs_list([],0):-!.
write_dimacs_list([I|J],S):-
    write_dimacs_clause(I),
    write_dimacs_list(J,T),
    length(I,Len),
    S is Len + T.

write_dimacs_clause([]):-write('0'),nl,!.
write_dimacs_clause([not(I)|J]):-
	write('-'),write(I),write(' '),
	write_dimacs_clause(J).
write_dimacs_clause([I|J]):-
	write(I),write(' '),
	write_dimacs_clause(J).

	


next_int(J):-
	prop(I),
	retract(prop(I)),
	J is I + 1,
	assertz(prop(J)).



next_var(J):-
	vb(I),
	retract(vb(I)),
	J is I + 1,
	assertz(vb(J)).

writeL([]).
writeL([I|J]):- nl,write(I),writeL(J).

cWriteL(L):- length(L,M),M < 51,writeL(L),nl,nl,write('no. clauses: '),write(M),!.
cWriteL(L):- length(L,M),nl,nl,write('no. clauses: '),write(M),!.
