:- use_module(library(readutil)).
:- [parser]. % provides input2formula/2
:- [tableau_fitting]. % provides valid/2, unsat/2

?-op(140,fy, [~, ?, !, neg]).
?-op(180, yfx, [&, and, or]).
?-op(180, yfx, '!=').
?-op(200, xfy, [imp, =>]).
:-op(200, xfy, [bimp, <=>]).
?-op(160, xfy, :).

/* prove(Fml,UnExp,Lits,FreeV,VarLim) <-- implements a lean tableau prover, cf Beckert and Posegga 
   based on Fitting's language; Fml is a formula in NNF, UnExp denotes the not yet expanded subformulas, 
   Lits (FreeV) is the list of literals (free variables) in the current branch and Varlim denotes the
   maximal number of free variables
*/

prove(and(A,B),UnExp,Lits,FreeV,VarLim) :- !,
    prove(A,[B|UnExp],Lits,FreeV,VarLim).
prove(or(A,B),UnExp,Lits,FreeV,VarLim) :- !,
    prove(A,UnExp,Lits,FreeV,VarLim),
    prove(B,UnExp,Lits,FreeV,VarLim).
prove(all(X,Fml),UnExp,Lits,FreeV,VarLim) :- !,
    \+ length(FreeV,VarLim),
    copy_term((X,Fml,FreeV),(X1,Fml1,FreeV)),
    append(UnExp,[all(X,Fml)],UnExp1),
    prove(Fml1,UnExp1,Lits,[X1|FreeV],VarLim).
prove(Lit,_UnExp,[L|Lits],_FreeV,_VarLim) :- !,
    (Lit = neg Neg; neg Lit = Neg) ->
	(unify_with_occurs_check(Neg,L); prove(Lit,[],Lits,_FreeV0,_VarLim0)).						 
prove(Lit,[Next|UnExp],Lits,FreeV,VarLim) :- !,
    prove(Next,UnExp,[Lit|Lits],FreeV,VarLim).

inc_prove(Fml,VarLim) :-
    prove(Fml,[],[],[],VarLim).
inc_prove(Fml,VarLim) :-
    NewVarLim is VarLim + 1,
    inc_prove(Fml,NewVarLim).

:- inc_prove(and(p,neg p),0).

inc_prove(Fml) :-
    inc_prove(Fml,0).

/* nnf(Fml,FreeV,NNF,Paths) <-- tranforms Fml with unique bound variables into NNF, 
   where FreeV is the list of free variables in Fml and Path is the number of disjunctive 
   path in Fml (resp. NNF)
*/

nnf(Fml,FreeV,NNF,Paths) :-
    (Fml = neg neg A -> Fml1 = A;
     Fml = neg all(X,F) -> Fml1 = some(X,neg F);
     Fml = neg some(X,F) -> Fml1 = all(X,neg F);
     Fml = neg (A or B) -> Fml1 = neg A and neg B;
     Fml = neg (A and B) -> Fml1 = neg A or neg B;
     Fml = A imp B -> Fml1 = neg A or B;
     Fml = neg (A imp B) -> Fml1 = A and neg B;
     Fml = A bimp B -> Fml1 = (A and B) or (neg A and neg B);
     Fml = neg (A bimp B) -> Fml1= (A and neg B) or (neg A and B)), !,
    nnf(Fml1,FreeV,NNF,Paths).
nnf(all(X,Fml),FreeV,all(X,NNF),Paths) :- !,
    nnf(Fml,[X|FreeV],NNF,Paths).
nnf(some(X,Fml),FreeV,NNF,Paths) :- !,
    copy_term((X,Fml,FreeV),(Fml,Fml1,FreeV)),
    copy_term((X,Fml1,FreeV),(ex,Fml2,FreeV)),
    nnf(Fml2,FreeV,NNF,Paths).
nnf(A and B,FreeV,and(NNF1,NNF2),Paths) :- !,
    nnf(A,FreeV,NNF1,Paths1),
    nnf(B,FreeV,NNF2,Paths2),
    Paths is Paths1 * Paths2.
nnf(A or B,FreeV,NNF,Paths) :- !,
    nnf(A,FreeV,NNF1,Paths1),
    nnf(B,FreeV,NNF2,Paths2),
    Paths is Paths1 + Paths2,
    (Paths1 > Paths2 -> NNF = or(NNF2,NNF1);
     NNF = or(NNF1,NNF2)).
nnf(Lit,_FreeV,Lit,1).

fm2nnf(Fml,NNF) :-
    nnf(Fml,_FreeV,NNF,_Paths).

:- fm2nnf(neg or(neg p,p),_NNF).
:- fm2nnf(neg (some(W,all(X,r(X,W,f(X,W)))) imp some(W,all(X,some(Y,r(X,W,Y)))) ),_NNF).
:- fm2nnf(neg (some(W,all(X,r(X,W,f(X,W)))) imp some(W,all(X,some(Y,r(X,W,Y)))) ),_NNF).
:- fm2nnf(neg (some(X,all(Y,r(X,Y))) imp all(Y,some(X,r(X,Y))) ),_NNF).
:- fm2nnf(neg (all(X,some(Y,r(X,Y))) imp some(Y,all(X,r(X,Y))) ),_NNF).
:- fm2nnf(neg (some(X,p(X) imp all(Y,p(Y))) ),_NNF).
:- fm2nnf(neg (some(X,(p(X) or q(X))) imp (some(X,p(X)) or some(X,q(X))) ),_NNF). 
:- \+ fm2nnf(some(X,(p(X) and q(X)) imp (some(X,p(X)) and some(X,q(X))) ),_NNF). % fails, due to restricted Skolemisation
:- fm2nnf(neg (some(X,(p(X) and q(X)) imp (some(Y,p(Y)) and some(Z,q(Z)))) ),_NNF). % requires different bound variables
:- fm2nnf(neg ((some(X,p(X)) and some(X,q(X))) imp some(X,(p(X) and q(X))) ),_NNF).
:- fm2nnf(neg (all(X,(p(X) or q(X))) imp (some(X,p(X)) or (all(X,q(X)))) ),_NNF).
:- fm2nnf(neg (((a or b) and (a or c) and (a or d) and (a or e) and (b or c) and (c or d) and (d or e)) or neg (((a or b) and (a or c) and (a or d) and (a or e) and (b or c) and (c or d) and e) )),_NNF).

:- fm2nnf(neg or(neg p,p),NNF), inc_prove(NNF).
:- fm2nnf(neg (some(W,all(X,r(X,W,f(X,W)))) imp some(W,all(X,some(Y,r(X,W,Y)))) ),NNF), inc_prove(NNF).
:- fm2nnf(neg (some(W,all(X,r(X,W,f(X,W)))) imp some(W,all(X,some(Y,r(X,W,Y)))) ),NNF), inc_prove(NNF).
:- fm2nnf(neg (some(X,all(Y,r(X,Y))) imp all(Y,some(X,r(X,Y))) ),NNF), inc_prove(NNF).
:- fm2nnf(neg (some(X,p(X) imp all(Y,p(Y))) ),NNF), inc_prove(NNF).
:- fm2nnf(neg (some(X,(p(X) or q(X))) imp (some(X,p(X)) or some(X,q(X))) ),NNF), inc_prove(NNF).
:- fm2nnf(neg (some(X,(p(X) and q(X)) imp (some(Y,p(Y)) and some(Z,q(Z)))) ),NNF), inc_prove(NNF).
:- fm2nnf(neg (all(X,(p(X) or q(X))) imp (some(X,p(X)) or (all(X,q(X)))) ),NNF), inc_prove(NNF).
:- fm2nnf(neg (((a or b) and (a or c) and (a or d) and (a or e) and (b or c) and (c or d) and (d or e)) or neg (((a or b) and (a or c) and (a or d) and (a or e) and (b or c) and (c or d) and e) )),NNF), inc_prove(NNF).

valid_leantap(F) :-
    fm2nnf(neg F,NNF),
    inc_prove(NNF,0).

unsat_leantap(F) :-
    fm2nnf(F,NNF),
    inc_prove(NNF,0).

/* apply theorem provers on SYN047 */

:- input2formula('SYN047+1.p',F), unsat(F,0).
:- input2formula('SYN047+1.p',F), unsat_leantap(F).

/* performance */

:- time(valid(((a or b) and (a or c) and (a or d) and (a or e) and (b or c) and (c or d) and (d or e)) or neg (((a or b) and (a or c) and (a or d) and (a or e) and (b or c) and (c or d) and e)),0)).
:- time(valid_leantap(((a or b) and (a or c) and (a or d) and (a or e) and (b or c) and (c or d) and (d or e)) or neg (((a or b) and (a or c) and (a or d) and (a or e) and (b or c) and (c or d) and e) ))).
:- input2formula('SYN047+1.p',F), time(unsat(F,0)).
:- input2formula('SYN047+1.p',F), time(unsat_leantap(F)).