:- use_module(library(lists), [member/2]).

index((H:-B),Index) :-
	count((B,H),Nlit,Narg,Ndisj,Niff,Neq,Neckcut,Ncut,MaxDepth),
	Index is Nlit + 7*Narg + 2*Neq + 3*Ndisj + Niff
	         + Neckcut + 12*Ncut + MaxDepth.

count(Body,Nlit,Narg,Ndisj,Niff,Neq,Neckcut,Ncut,MaxDepth) :-
	var(Body), !,
	(Nlit,Narg,Ndisj,Niff,Neq,Neckcut,Ncut,MaxDepth) =
	(   1,   0,    0,   0,  0,      0,   0,       0).
count(Body,Nlit,Narg,Ndisj,Niff,Neq,Neckcut,Ncut,MaxDepth) :-
	control_construct(Body,A,B,PlusDisj,PlusIff), !,
	count(A,Nlit1,Narg1,Ndisj1,Niff1,Neq1,Neckcut,Ncut1,MaxDepth1),
	count(B,Nlit2,Narg2,Ndisj2,Niff2,Neq2,      _,Ncut2,MaxDepth2),
	Nlit is Nlit1 + Nlit2,
	Narg is Narg1 + Narg2,
	Ndisj is Ndisj1 + Ndisj2 + PlusDisj,
	Niff is Niff1 + Niff2 + PlusIff,
	Neq is Neq1 + Neq2,
	Ncut is Ncut1 + Ncut2,
	MaxDepth is max(MaxDepth1,MaxDepth2).
count(Goal,Nlit,Narg,Ndisj,Niff,Neq,Neckcut,Ncut,MaxDepth) :-
	Goal = (_ = _), !,
	(Nlit,Narg,Ndisj,Niff,Neq,Neckcut,Ncut) =
	(   1,   2,    0,   0,  1,      0,   0),
	max_depth(Goal,MaxDepth).
count(!,Nlit,Narg,Ndisj,Niff,Neq,Neckcut,Ncut,MaxDepth) :- !,
	(Nlit,Narg,Ndisj,Niff,Neq,Neckcut,Ncut) =
	(   1,   0,    0,   0,  0,      1,   1),
        MaxDepth = 0.
count(Goal,Nlit,Narg,Ndisj,Niff,Neq,Neckcut,Ncut,MaxDepth) :-
	functor(Goal,_,Narg),
	(Nlit,Narg,Ndisj,Niff,Neq,Neckcut,Ncut) =
	(   1,Narg,    0,   0,  0,      0,   0),
	max_depth(Goal,MaxDepth).

control_construct((A,B),A,B,0,0).
control_construct((A;B),A,B,1,0).
control_construct((A->B),A,B,0,1).





max_depth(Term,MaxDepth) :-
	atomic(Term), !,
	MaxDepth = 0.
max_depth(Term,MaxDepth) :-
	setof(D,depth(Term,D),[M|_]),
	MaxDepth is -M - 1.

depth(Term,Depth) :-
	compound(Term), !,
	Term =.. [_|L],
	member(X,L),
	depth(X,Depth1),
	Depth is Depth1 - 1.
depth(_,0).