

% modal logic interpretation of ALC for SAT solving

:- dynamic prop/1, dimacs_int/2.


% 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(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,R):-
    rewrite(WFF,[0,0],R).

rewrite(all(R, WFF),[CX,_],CFR):- !,
    concat_test(CX,R,CXR),!,
    rewrite(WFF,[CXR,forall],CF),!,
    disj_cnf([[not(CXR)]],CF,CFR).

rewrite(some(R, WFF),[CX,_],CFR):- !,
    concat_test(CX,R,CXR),!,
    rewrite(WFF,[CXR,exists],CF),!,
    conj_cnf([[CXR]],CF,CFR).

rewrite(and(WFF1, WFF2),[CX,Q],CFR):- !,
    rewrite(WFF1,[CX,Q],CF1),!,
    rewrite(WFF2,[CX,Q],CF2),!,
    conj_cnf(CF1,CF2,CFR).

rewrite(or(WFF1, WFF2),[CX,Q],CFR):- !,
    rewrite(WFF1,[CX,Q],CF1),!,
    rewrite(WFF2,[CX,Q],CF2),!,
    disj_cnf(CF1,CF2,CFR).

rewrite(implies(WFF1, WFF2),[CX,Q],CFR):- !,
    rewrite_negated(WFF1,[CX,Q],CF1),!,
    rewrite(WFF2,[CX,Q],CF2),!,
    disj_cnf(CF1,CF2,CFR).

rewrite(not(WFF),L,R):- rewrite_negated(WFF,L,R).

rewrite(WFF,[CX,exists],[[Prop]]):- concat_test(WFF,CX,Prop),!.
rewrite(WFF,[CX,forall],[[Prop]]):- concat_test(WFF,CX,Prop),!.
rewrite(WFF,[0,0],[[WFF]]):-!.
rewrite(WFF,[CX,_],[[Prop]]):- concat_test(WFF,CX,Prop),!.


rewrite_negated(WFF,R):-
    rewrite_negated(WFF,[0,0],R).

rewrite_negated(all(R, WFF),[CX,_],CFR):- !,
    concat_test(CX,R,CXR),!,
    rewrite_negated(WFF,[CXR,exists],CF),!,
    conj_cnf([[CXR]],CF,CFR).

rewrite_negated(some(R, WFF),[CX,_],CFR):- !,
    concat_test(CX,R,CXR),!,
    rewrite_negated(WFF,[CXR,forall],CF),!,
    disj_cnf([[not(CXR)]],CF,CFR).

rewrite_negated(and(WFF1, WFF2),[CX,Q],CFR):- !,
    rewrite_negated(WFF1,[CX,Q],CF1),!,
    rewrite_negated(WFF2,[CX,Q],CF2),!,
    disj_cnf(CF1,CF2,CFR).

rewrite_negated(or(WFF1, WFF2),[CX,Q],CFR):- !,
    rewrite_negated(WFF1,[CX,Q],CF1),!,
    rewrite_negated(WFF2,[CX,Q],CF2),!,
    conj_cnf(CF1,CF2,CFR).

rewrite_negated(implies(WFF1, WFF2),[CX,Q],CFR):- !,
    rewrite(WFF1,[CX,Q],CF1),!,
    rewrite_negated(WFF2,[CX,Q],CF2),!,
    conj_cnf(CF1,CF2,CFR).

rewrite_negated(not(WFF),L,R):- rewrite(WFF,L,R),!.

rewrite_negated(WFF,[CX,exists],[[not(Prop)]]):- concat_test(WFF,CX,Prop),!.
rewrite_negated(WFF,[CX,forall],[[not(Prop)]]):- concat_test(WFF,CX,Prop),!.
rewrite_negated(WFF,[0,0],[[not(WFF)]]):-!.
rewrite_negated(WFF,[CX,_],[[not(Prop)]]):- concat_test(WFF,CX,Prop),!.


concat_test(X,0,X):-!.
concat_test(0,X,X):-!.
concat_test(X,Y,Z):- concat(X,'.',ZZ),concat(ZZ,Y,Z),!.


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(A,B):-
	retractall(prop(_)),
	assertz(prop(0)),
	to_dimacs(A,B,[]),!.

to_dimacs([],[],_):-!.
to_dimacs([A|B],[AA|BB],L):-
    to_dimacs_clause(A,AA,L,LL),
    to_dimacs(B,BB,LL).

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

to_dimacs_clause([not(A)|B],[not(AA)|BB],L,LL):-
	member([A,AA],L), %write(A),write(' '),write(AA),nl,
	delete(B,not(A),BC),
	to_dimacs_clause(BC,BB,L,LL).
	
to_dimacs_clause([A|B],[AA|BB],L,LL):-
	member([A,AA],L), %write(A),write(' '),write(AA),nl,
	delete(B,A,BC),
	to_dimacs_clause(BC,BB,L,LL).
	
to_dimacs_clause([not(A)|B],[not(I)|BB],L,LL):-
	next_int(I), %write(A),write(' '),write(I),nl,
	delete(B,not(A),BC),
	to_dimacs_clause(BC,BB,[[A,I]|L],LL).

to_dimacs_clause([A|B],[I|BB],L,LL):-
	next_int(I), %write(A),write(' '),write(I),nl,
	delete(B,A,BC),
	to_dimacs_clause(BC,BB,[[A,I]|L],LL).


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),B):-!,
	dimacs_int(A,_AA),!,
        member(not(A),B),!.

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

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

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

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

to_dimacs_clause([A|B],[I|BB]):-
	next_int(I),!,
        assertz(dimacs_int(A,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)).


