/*************************************************************************

         name: foTabl.pl
      version: July 2002
  description: Predicates for First Order Tableaux
      authors: Aljoscha Burchardt, Stephan Walter
 
*************************************************************************/

:- use_module(signature,[newconst/1]).
:- use_module(substitute,[subst/3]).
:- use_module(comsemLib,[hbaseList/2]).

:- ensure_loaded(comsemOperators).

/*=====================================================
  tabl/6 -- Propositional Clauses --
======================================================*/

tabl(true(A & B),InBranch,OutBranch,QuantsIn,QuantsOut,Qdepth) :-
	!,tabl(true(A),InBranch,K,QuantsIn,QuantsOut1,Qdepth), 
	tabl(true(B),K,L,QuantsOut1,QuantsOut,Qdepth),
 	list_to_set(L,OutBranch).

tabl(false( A & _),InBranch,H,QuantsIn,QuantsOut,Qdepth) :- 
	tabl(false(A),InBranch,H,QuantsIn,QuantsOut,Qdepth).

tabl(false( _ & B),InBranch,H,QuantsIn,QuantsOut,Qdepth) :- 
	!,tabl(false(B),InBranch,H,QuantsIn,QuantsOut,Qdepth).

tabl(true(~A),InBranch,H,QuantsIn,QuantsOut,Qdepth) :- 
	!,tabl(false(A),InBranch,H,QuantsIn,QuantsOut,Qdepth).

tabl(false(~A),InBranch,H,QuantsIn,QuantsOut,Qdepth) :- 
	!,tabl(true(A),InBranch,H,QuantsIn,QuantsOut,Qdepth).

/*=====================================================
  tabl/6 -- Quantifier Clauses --
======================================================*/

% Instantiate existentially quantif. formula with new individual
tabl(false(forall(X,Scope)),InBranch,OutBranch,QuantsIn,QuantsOut,Qdepth) :-
	!,newconst(NewConst),
	subst([X:NewConst],Scope,NewFormula),
	tabl(false(NewFormula),InBranch,OutBranch,QuantsIn,QuantsOut,Qdepth).

% apply univ. quant once and store
tabl(true(forall(X,Scope)),InBranch,OutBranch,QuantsIn,QuantsOut,Qdepth) :-
	!,hbaseList(InBranch,HBase),
	member(Ind,HBase),
	subst([X:Ind],Scope,NewInstantiation),
	tabl(true(NewInstantiation),InBranch,OutBranch,[(forall(X,Scope),[Ind])|QuantsIn],QuantsOut,Qdepth).

/*=====================================================
  tabl/6 -- "Base" Clauses --
======================================================*/

% a: clash
tabl(F,InBranch,OutBranch,_,_,_) :- 
	OutBranch = [F|InBranch],
	clash(OutBranch),!,fail.

clash(List) :- 
	member(true(A),List),
	member(false(A),List).


% b: instantiate quant
tabl(F,InBranch,OutBranch,[(forall(X,Scope),SoFarInds)|RestQuants],QuantsOut,Qdepth) :-
	length(SoFarInds,LengthInds),
	LengthInds =< Qdepth,
	hbaseList([F|InBranch],HBase),
	member(Ind,HBase),
	\+ member(Ind,SoFarInds),!,
	subst([X:Ind],Scope,NewInstantiation),
	append(RestQuants,[(forall(X,Scope),[Ind|SoFarInds])],NewQuants),
	tabl(true(NewInstantiation),[F|InBranch],OutBranch,NewQuants,QuantsOut,Qdepth).

% c: no clash, no instantiation possible: pass on quants
% is impossible at a leaf (since Quants is required to be [] at the end of the day (branch))
tabl(F,InBranch,[F|InBranch],Quants,Quants,_) :- !.

% d: at a leaf: skip one quant (all inds are used or Qdepth exceeded)
tabl(F,InBranch,OutBranch,[_|RestQuants],QuantsOut,Qdepth) :-
	tabl(F,InBranch,OutBranch,RestQuants,QuantsOut,Qdepth).




