

% modal logic interpretation of ALC for SAT solving

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

m:- [modal].

% 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 = 
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,P),
	cWriteL(P),nl,
	to_dimacs_db(P,Q),
    tell('dimacs_file'),
	write_dimacs(Q),
    told.

test2:- F = and(all(eats,implies(veg,not(meat))),and(some(eats,veg),and(all(eats,and(some(drinks,wine),all(drinks,not(beer)))),all(eats,or(meat,some(drinks,beer)))))),
	write(F),
	rewrite(F,P),
	cWriteL(P),nl,
	to_dimacs_db(P,Q),
    tell('dimacs_file'),
	write_dimacs(Q),
    told.

% 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).
alc_dimacs(F,C):-rewrite(F,P), to_dimacs(P,C).
tancs_dimacs(F,C):- tancs_to_prolog(F,P),boxToALC(P,Q),rewrite(Q,R),to_dimacs(R,C).

rewrite(WFF,GCL):-
    retractall(dimacs_int(_,_)),
    retractall(e(_,_,_)),
    retractall(vb(_)),
    assertz(vb(0)),
    retractall(prop(_)),
    assertz(prop(0)),!,
    rewrite(WFF,[],[],CF,B),!,
% nl,writeL(CF),nl,writeL(B),
    length(CF,Len),nl,nl,write('no. non-ground clauses: '),write(Len),
    applyBindings(CF,B,GCL),!.

applyBindings(CL,B,GCL):-
	repBindings(B,VBL,BR),!,
	nl,write('vars unbound:'),write(BR),
	nl,write('vars bound:'),write(VBL),
	repApplyBindings(CL,VBL,GCL),!.

repApplyBindings([],_,[]):-!.
repApplyBindings([I|J],VBL,KK):-
	applyBC(I,VBL,II),!,        % apply bindings to each clause
	repApplyBindings(J,VBL,JJ),!,
	append(II,JJ,KK),!.
repApplyBindings([I|J],VBL,JJ):-    % ignore clauses where some var has no binding
%	nl,write('fail to transform: '),write(I),
	repApplyBindings(J,VBL,JJ).

applyBC(I,VBL,R):-
	repApplyBC(I,VBL,II),!,
	permute(II,R),!.

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


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

permute([[X,[]]|M],O):-
	permute(M,N),
	appendAll([X,[]],N,O),!.

permute([[X,[L]]|M],O):-!,
	permute(M,N),!,
	appendAll([X,L],N,O),!.

permute([[X,L]],O):-
	is_list(L),!,
	appendAll3(X,L,[],O),!.

permute([[X,L]|M],O):-
	is_list(L),!,
	permute(M,N),!,
	appendAll2(X,L,N,O),!.

permute([[X,I]|M],O):-
	permute(M,N),
	appendAll([X,I],N,O),!.

appendAll3(_,[],_,[]):-!.
appendAll3(I,[X|Y],L,[XX|YY]):-!,
	appendAll3([I,X],L,XX),
	appendAll3(I,Y,L,YY),!.

appendAll3(L,[],[L]):-!.
appendAll3(I,[X|Y],[XX|YY]):-!,
	append([I],X,XX),
	appendAll3(I,Y,YY),!.

appendAll2(_,[],_,[]):-!.
appendAll2(I,[X|Y],L,ZZ):-!,
	appendAll2([I,X],L,XX),
	appendAll2(I,Y,L,YY),!,
	append(XX,YY,ZZ),!.

appendAll2(_,[],[]):-!.
appendAll2(I,[X|Y],[XX|YY]):-!,
	append([I],X,XX),
	appendAll2(I,Y,YY),!.

appendAll(I,[],[[I]]):-!.
appendAll(I,[X],[[I|X]]):-!.
appendAll(I,[X|Y],[XX|YY]):-!,
	append([I],X,XX),
	appendAll(I,Y,YY),!.


repBindings([],[],[]):-!.
repBindings(BL,VBL1,BRR):- 
    getBindingsC([],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),!,
    not(IL = []),
    getBindingsC(C,B,Res,BR).
getBindingsC(C,[I|B],R,[I|BR]):-!,
    getBindingsC(C,B,R,BR).

gndTerm([]):-!.
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),
    not(IL = []),!,
    getBindingsV(B,VBL,Res,BR),!.
getBindingsV([e(C,Rln,v(V))|B],VBL,[[v(V),IL]|Res],BR):-
    integer(C),
    getBinding(C,Rln,IL),
    not(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).

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

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

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

rewrite(all(R, WFF),C,BI,CF,BO):- !,
    getVarBind(C,R,V,BI,BL),   % update the Binding set by e(C,R,v(V)), V may be new - e is functional
    rewrite(WFF,V,BL,CF,BO),!. % Context is now V

rewrite(some(R, WFF),C,BI,CF,BO):- !,
    next_int(E),
    assertz(e(C,R,E)),         % assert e(C,R,E) E is always new
    rewrite(WFF,E,BI,CF,BO),!. % Context is now E

rewrite(and(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite(WFF1,C,BI,CF1,BO1),!,
    rewrite(WFF2,C,BO1,CF2,BO),!,
    conj_cnf(CF1,CF2,CFR),!.
%    merge_set(BO1,BO2,BO).

rewrite(or(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite(WFF1,C,BI,CF1,BO1),!,
    rewrite(WFF2,C,BO1,CF2,BO),!,
    disj_cnf(CF1,CF2,CFR),!.
%    merge_set(BO1,BO2,BO).

rewrite(implies(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite_negated(WFF1,C,BI,CF1,BO1),!,
    rewrite(WFF2,C,BO1,CF2,BO),!,
    disj_cnf(CF1,CF2,CFR),!.
%    merge_set(BO1,BO2,BO).

rewrite(not(WFF),C,BI,CFR,BO):- rewrite_negated(WFF,C,BI,CFR,BO).

rewrite(WFF,C,BI,[[[WFF,C]]],BI):- !.



rewrite_negated(some(R, WFF),C,BI,CF,BO):- !,
    getVarBind(C,R,V,BI,BL),   % update the Binding set by e(C,R,v(V)), V may be new - e is functional
    rewrite_negated(WFF,V,BL,CF,BO),!. % Context is now V

rewrite_negated(all(R, WFF),C,BI,CF,BO):- !,
    next_int(E),
    assertz(e(C,R,E)),         % assert e(C,R,E) E is always new
    rewrite_negated(WFF,E,BI,CF,BO),!. % Context is now E

rewrite_negated(or(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite_negated(WFF1,C,BI,CF1,BO1),!,
    rewrite_negated(WFF2,C,BO1,CF2,BO),!,
    conj_cnf(CF1,CF2,CFR),!.
%    merge_set(BO1,BO2,BO).

rewrite_negated(and(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite_negated(WFF1,C,BI,CF1,BO1),!,
    rewrite_negated(WFF2,C,BO1,CF2,BO),!,
    disj_cnf(CF1,CF2,CFR),!.
%    merge_set(BO1,BO2,BO).

rewrite_negated(implies(WFF1, WFF2),C,BI,CFR,BO):- !,
    rewrite(WFF1,C,BI,CF1,BO1),!,
    rewrite_negated(WFF2,C,BO1,CF2,BO),!,
    conj_cnf(CF1,CF2,CFR),!.
%    merge_set(BO1,BO2,BO).

rewrite_negated(not(WFF),C,BI,CFR,BO):- rewrite(WFF,C,BI,CFR,BO).

rewrite_negated(WFF,C,BI,[[[not(WFF),C]]],BI):- !.

getVarBind(C,R,V,BI,BI):-
    member(e(C,R,V),BI),!.
getVarBind(C,R,v(V),BI,[e(C,R,v(V))|BI]):-
    next_var(V),!.


conj_cnf(A,B,C):- append(A,B,C).

disj_cnf(C,[],C).
disj_cnf([],_,[]).
disj_cnf([A|B],C,D):-
        list_to_set(A,AA),
        append_to_all(AA,C,D0),
        disj_cnf(B,C,D1),
        append(D0,D1,D).

append_to_all(_,[],[]).
append_to_all(A,[B|C],[D0|D1]):-
        append(A,B,D00),
        list_to_set(D00,D0),
        append_to_all(A,C,D1).

% 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

to_dimacs_db(A,B):-
	retractall(prop(_)),
	assertz(prop(0)),
	to_dimacs_db_rep(A,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):-
    prop(P),
    length(I,Len),
    write('c an ALC problem'),nl,
    write('p cnf '),write(P),write(' '),write(Len),nl,
    write_dimacs_list(I).
/*
    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),!.
