% 02.11.05 : Changing definition of makearray. 
%            It now appends list of (arrayelement, CobVar) to VarMap in addition to 
%            just creating the array.
% 02.11.04 : Definition of conditional constraint changed

% This file contains efficient definition of index with cuts and 
% also the first 30 indices are sort of hard coded.
% Declarations of constant sized arrays are translated to makearray



index([X|_], 1.0, X) :- !.
index([_,X|_], 2.0, X) :- !.
index([_,_,X|_], 3.0, X) :- !.
index([_,_,_,X|_], 4.0, X) :- !.
index([_,_,_,_,X|_], 5.0, X) :- !.
index([_,_,_,_,_,X|_], 6.0, X) :- !.
index([_,_,_,_,_,_,X|_], 7.0, X) :- !.
index([_,_,_,_,_,_,_,X|_], 8.0, X) :- !.
index([_,_,_,_,_,_,_,_,X|_], 9.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,X|_], 10.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,X|_], 11.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,X|_], 12.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,X|_], 13.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 14.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 15.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 16.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 17.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 18.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 19.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 20.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 21.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 22.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 23.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 24.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 25.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 26.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 27.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 28.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 29.0, X) :- !.
index([_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,X|_], 30.0, X) :- !.

index(Array, Index, Value) :- 
   Index > 30, index(Array, 1, Index, Value).

index([X|_], I, I, X) :- !.
index([_|T], I, N, X) :- I1 is I + 1, index(T, I1, N, X).

output([]).
output([X|T]) :- print(X), nl, output(T).

% new definition of makearray to return ArrayVarMap.
makearray([N], V, NameofV, ArrayVarMap) :- 
   sizeofandmaparray(V, N, NameofV, ArrayVarMap), !.
makearray([N|Rest], V, NameofV, ArrayVarMap) :- 
   sizeofandmaparray(V, N, NameofV, ArrayVarMap1), 
   makearrayofeach(Rest,V, NameofV, N, ArrayVarMap2),
   append(ArrayVarMap1, ArrayVarMap2, ArrayVarMap).
makearray(_,_,_,_). % when array dimensions are left unspecified.

makearrayofeach(L,[V], NameofV, N, ArrayVarMap) :- 
   makearray(L, V, ind(NameofV,N), ArrayVarMap), !.
makearrayofeach(L, VList, NameofVList, N, ArrayVarMap) :- 
   last(VList, VLast), makearray(L, VLast, ind(NameofVList, N), ArrayVarMap1), 
   append(FrontVList, [VLast], VList), N1 is N - 1,
   makearrayofeach(L, FrontVList, NameofVList, N1, ArrayVarMap2),
   append(ArrayVarMap1, ArrayVarMap2, ArrayVarMap).

sizeofandmaparray([], 0.0, _NameofV, []) :- !.
sizeofandmaparray(Arr, N, NameofV, [(A, ind(NameofV, N))|ArrayVarMap]) :- 
   %order of predicates on next line is important.   
   N1 is N - 1, sizeofandmaparray(T, N1, NameofV, ArrayVarMap), append(T, [A], Arr). 

size([], 0) :- !.
size([_|T], N+1) :- sizeof(T, N).




min(X,Y,Z) :- ((nonvar(X), nonvar(Y))-> Z=min(X,Y); (nonvar(X)->Z=X; (nonvar(Y)-> Z=Y;true))).

max(X,Y,Z) :- ((nonvar(X), nonvar(Y))-> Z=max(X,Y); (nonvar(X)->Z=X; (nonvar(Y)-> Z=Y;true))).

makelistfromto(M, M, [M]) :- !.
makelistfromto(N, M, [N|NtoM]) :- N < M, N1 is N +1, makelistfromto(N1, M, NtoM).

%not complete : never forces \+(B)
conditionalConstr(A, _B, true) :- entailed(A), ! .
conditionalConstr(_A, B, callA) :- entailed(B), !.
conditionalConstr(_A, B, true) :- ground(B). % same as \+(B).
conditionalConstr(_A, _B, cannot_prove).


sizeof([],0).
sizeof([_X|T], N1):- sizeof(T, N), N1 is N + 1.