

% 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).
test:- F = 
not(implies(and(true, not(all(r, all(r, implies(all(r, implies(all(r, implies(p0, all(r, p0))), p0)), implies(some(r, all(r, p0)), p0)))))), or(some(r, some(r, not(and(and(and(implies(all(r, implies(all(r, implies(p0, all(r, p0))), p0)), all(r, all(r, implies(all(r, implies(p0, all(r, p0))), p0)))), all(r, implies(all(r, p0), all(r, all(r, p0))))), implies(all(r, implies(all(r, implies(p0, all(r, p0))), p0)), implies(some(r, all(r, p0)), or(p0, all(r, p0))))), implies(all(r, implies(all(r, implies(implies(p0, all(r, p0)), all(r, implies(p0, all(r, p0))))), implies(p0, all(r, p0)))), implies(some(r, all(r, implies(p0, all(r, p0)))), or(implies(p0, all(r, p0)), all(r, implies(p0, all(r, p0)))))))))), false))),
	write(F),
	rewrite(F,'dimacs_file').

test1:- F = and(all(r,all(r,or(p,q))),and(some(r,all(r,or(s,t))),and(some(r,some(r,or(u,v))),all(r,some(r,or(a,b)))))),
	write(F),
	rewrite(F,'dimacs_file').

test2:- F = and(all(eats,implies(veg,not(meat))),and(some(eats,veg),and(all(eats,and(some(drinks,wine),all(drinks,not(beer)))),some(eats,or(all(eats,meat),some(drinks,beer)))))),
	write(F),
	rewrite(F,'dimacs_file').

% 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,
    rewrite(WFF,0,[],CF,B),!,
%%%% nl,writeL(CF),nl,writeL(B),
%    length(CF,Len),nl,write('no. non-ground clauses: '),write(Len),
%    tell('dimacs_file_cl'),
    applyBindings(CF,B,CountCL),!,
%    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),
    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):-trace,
	repBindings(B,VBL,_BR),!,
	%nl,write('vars unbound:'),write(BR),
	%nl,write('vars bound:'),write(VBL),
        swapVbInt,
        setup_dimacs,
	repApplyBindings(CL,VBL,CountCL),!.

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

repBindings([],[],[]):-!.
repBindings(BL,VBL1,BRR):- 
    getBindingsC(0,BL,VBL,BR),!,
    getBindingsLevel(BR,VBL,VBL1,BRR),!.


getBindingsLevel(BL,VBL,VBL3,BLRR):-
    getBindingsVCheck(BL,VBL,VBL1,BLR),!,
    getBindingsLevel(BLR,VBL1,VBL2,BLRR),!,
    append(VBL,VBL2,VBL3),!.
getBindingsLevel(BLR,VBL,VBL,BLR):-!.

getBindingsC(_,[],[],[]):-!.
getBindingsC(C,[e(C,Rln,v(V))|B],[[v(V),IL]|Res],BR):-
    gndTerm(C),
    getBinding(C,Rln,IL),
    getBindingsC(C,B,Res,BR).
getBindingsC(C,[I|B],R,[I|BR]):-!,
    getBindingsC(C,B,R,BR).

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


getBindingsVCheck(BL,VBL,VBL1,BLR):-
    getBindingsV(BL,VBL,VBL1,BLR),!,
    not(VBL = VBL1),!.


getBindingsV([],_,[],[]):-!.
getBindingsV([e(v(V),Rln,v(W))|B],VBL,[[v(W),IL]|Res],BR):-
    memberCut([v(V),L],VBL),
    getBindingL([v(V)|L],Rln,IL),
    getBindingsV(B,VBL,Res,BR),!.
getBindingsV([e(C,Rln,v(V))|B],VBL,[[v(V),IL]|Res],BR):-
    gndTerm(C),
    getBinding(C,Rln,IL),
    getBindingsV(B,VBL,Res,BR).

%getBindingsV([I|J],VBL,Res,[I|BR]):-!,
%    getBindingsV(J,VBL,Res,BR).
    
getBindingL(L,R,IL):-!,
    findall(I,const(L,R,I),IL).

const(L,R,I):-
    member(C,L),
    e(C,R,I).

getBinding(C,R,IL):-
    findall(I,e(C,R,I),IL),!.

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

repApplyBindings([],_,0):-!.
repApplyBindings([I|J],VBL,ResO):-
	applyBC(I,VBL,II),!,        % apply bindings to each clause
        length(II,LenII),
%        write(II),
        to_dimacs_db(II),           % reduce memory overhead - write dimacs here
	repApplyBindings(J,VBL,Res),!,
        ResO is LenII + Res,!.
repApplyBindings([I|_J],_VBL,_Res):-    % ignore clauses where some var has no binding
	nl,told,write('fail to transform: '),write(I),!,fail.
%	repApplyBindings(J,VBL,Res).

applyBC(I,VBL,R):-
	getClVars(I,VBL,II),!,
	subst(I,II,R),!.

% for each literal, replace v(V) with the corresonding list
getClVars([],_,[]):-!.
getClVars([[X,v(V)]|C],VBL,[[v(V),LL]|R]):-
	member([v(V),L],VBL),!,
        checkVBLNil(L,LL),!,
	getClVars(C,VBL,R),!.
getClVars([[_X,_Y]|C],VBL,R):-
	getClVars(C,VBL,R),!.

checkVBLNil([],I):-!,next_var(I).
checkVBLNil(I,I):-!.
    



% 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),!.
