%%--------------------------------------------------------------------------------
%% Auxiliary Predicate: append(X,Y,Z) - Z is the list that results from
%% appending list Y to list X.
%%--------------------------------------------------------------------------------

append([], T, T).
append([H | T], T1, [H | T2]) :- append(T, T1, T2).

%%--------------------------------------------------------------------------------
%% Auxiliary Predicate: flatten(X,Y) - Y is the list that results from
%% flattening the list X.
%%--------------------------------------------------------------------------------

flatten([], []).
flatten([Head], [Head])   :- atomic(Head), !.
flatten([Head], [Head])   :- var(Head), !.
flatten([Head], Y)        :- flatten(Head, Y), !.
flatten([Head | Tail], Y) :- flatten([Head], Y1),
                             flatten(Tail, Y2),
                             append(Y1, Y2, Y).

%%--------------------------------------------------------------------------------
%% Auxiliary Predicate: variablesInTerm(X,Y) - Y is the list of all
%% variables in the term X.
%%--------------------------------------------------------------------------------

variablesInTerm(X,[])      :- ground(X), !.
variablesInTerm(X,[X])     :- var(X), !.
variablesInTerm(X,VarList) :- X =.. [F | P],
                              variables([F | P], VarList).

%%--------------------------------------------------------------------------------
%% Auxiliary Predicate variables(X,Y) - Y is the list of all variables
%% in the list of terms X.
%%--------------------------------------------------------------------------------

variables([],[]).
variables([Head | Tail], VarList) :- variablesInTerm(Head, VarsInTerm),
                                     variables(Tail, VarsInTail),
                                     append(VarsInTerm, VarsInTail, VarList).
									 
%%--------------------------------------------------------------------------------
%% Auxiliary Predicate: cardinality(X,Y) - Y is the number of elements in the
%% list X.
%%--------------------------------------------------------------------------------

cardinality([], 0).
cardinality([_ | Tail], X) :- cardinality(Tail, Y),
                              X is Y + 1.

%%--------------------------------------------------------------------------------
%% Query Definitions
%%--------------------------------------------------------------------------------

answer(sometimes, Query, yes) :- ground(Query), model(I),
                                 Query =.. [F | P],
                                 NewGoal =.. [F | [I|P]],
                                 call(NewGoal), !.
				
answer(sometimes, Query, no)  :- ground(Query).
				
answer(sometimes, Query, S)   :- \+ ground(Query),
                                 Query =.. [F | P],
                                 variables(P, VarList),
                                 NewQuery =.. [F | [I|VarList]],
                                 setof(VarList, I^NewQuery, S), !.

answer(always, Query, no)     :- ground(Query), model(I),
                                 Query =.. [F | P],
                                 NewGoal =.. [F | [I|P]],
                                 \+ call(NewGoal), !.

answer(always, Query, yes)    :- ground(Query).

answer(always, Query, S)      :- \+ ground(Query),
                                 Query =.. [F | P],
                                 variables(P, VarList),
                                 NewQuery =.. [F | [I|VarList]],
                                 numberOfModels(N),
                                 setof(VarList, setof(I,NewQuery,S1), S),
                                 cardinality(S1, N1),
                                 N1 == N.