%% Version:  1.08  -  Date: 10/01/97  -  File: ncdp.pl
%%
%% Purpose: ncDP: A Non-Clausal Form Decision Procedure
%%
%% Author:  Jens Otten
%% Web:     www.leancop.de/ncdp/
%%
%% Usage:   prove(F).   % where F is a propositional formula
%%                      %  e.g. F=(((~a; ~b),c)=>(c,(a=> ~b)))
%%          dp(M).      % where M is a nested matrix
%%                      %  e.g. M=[[a,b],[-c],[c,[[-a],[-b]]]]
%%
%% Copyright: (c) 1997 by Jens Otten
%% License:   GNU General Public License


%%% equivalence, implication and negation operator declarations

:- op(1130,xfy,<=>).   :- op(1110,xfy,=>).   :- op(500,fy,'~').

%%% build matrix

bmatrix((~X),Pol,M)      :- !, Pol1 is (1-Pol), bmatrix(X,Pol1,M).
bmatrix((X1<=>X2),Pol,M) :- !, bmatrix(((X1=>X2),(X2=>X1)),Pol,M).
bmatrix(X,Pol,M3)        :- X=..[F,X1,X2], alpha(F,Pol,Pol1,Pol2), !,
                            bmatrix(X1,Pol1,M1), bmatrix(X2,Pol2,M2),
                            union(M1,M2,M3).
bmatrix(X,Pol,[M3])      :- X=..[F,X1,X2], beta(F,Pol,Pol1,Pol2), !,
                            bmatrix(X1,Pol1,M1), bmatrix(X2,Pol2,M2),
                            sim(M1,M4), sim(M2,M5), union(M4,M5,M3).
bmatrix(X,0,[[X]]).
bmatrix(X,1,[[-X]]).

sim([M],M) :- !. sim(M,[M]).

alpha(',',1,1,1):-!. alpha(';',0,0,0):-!. alpha((=>),0,1,0):-!.
beta(',',0,0,0):-!.  beta(';',1,1,1):-!.  beta((=>),1,0,1):-!.

%%% prove

prove(F) :- bmatrix(F,0,M), pure(M,M1), dp(M1).

%%% dp (non-clausal DP)

dp([]) :- !, fail.
dp(M)  :- member([],M), !.

% UNIT
dp(M)  :- member([L],M), ( atom(L), N= -L ; -N=L ), !,
          reduce(M,N,L,M1), dp(M1).

% Beta-Splitting
dp([[[C1|M],[C2|M2]|C]|M1])  :- !, 
   dp([[[C1|M]]|M1]), dp([[[C2|M2]]|M1]), dp([C|M1]).

% Splitting
dp(M)  :- selectLit(M,P,N),
          reduce(M,P,N,M1), dp(M1),
          reduce(M,N,P,M2), dp(M2).

%%% reduce MReduce/CReduce

reduce(L,L,_,[[]])   :- !.  %% true
reduce(N,_,N,[])     :- !.  %% false

reduce([C|M],L,N,M1) :- !,
 reduce(C,L,N,C1),             %% evaluate clauses/matrices
 (C1=[] -> M1=[[]] ;           %% matrix/clause elimination
 C1=[[]] -> reduce(M,L,N,M1) ; %% simplify
 reduce(M,L,N,M2),             %% evaluate remaining cl./mat.
 (M2=[[]] -> M1=[[]] ;         %% matrix/clause elimination
  M2=[], C1=[M3] -> M1=M3 ; M1=[C1|M2] )). 
  
reduce(A,_,_,A).

%% select literal
selectLit([M|_],A,An) :- !, selectLit(M,A,An).
selectLit(-A,-A,A)    :- !.
selectLit(A,A,-A).

%%% PURE
pure(M,M1) :- litM(M,LitM), pure(M,LitM,M1,LitM).

pure(M,[],M,_).
pure(M,[L|LitM],M1,LL) :- 
   (L= -N ; -L=N), !,
   (member(N,LL) -> M2=M ;
    reduce(M,N,L,M2)), pure(M2,LitM,M1,LL).

litM([],[])   :- !.
litM([H|T],L) :- !, litM(H,L1), litM(T,L2), union(L1,L2,L).
litM(A,[A]).