%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \Pi_{sat}
% determining whether a basic formula \varphi 
% is satisfied or not 
% a basic desire is assigned a name
% which is declared by the predicate 
%     desire(Name)
% and then encoded using the two predicates 
%     isand(Name, FirstConjunct, SecondConjunct)
%     isor(Name, FirstDisjunct, SecondDisjunct)
%     isnegation(Name, NameOfTheNegatedFormula)
% (isand & isor are used instead of and & or, respectively, to avoid
% clash with smodels predefined predicates.)
% Temporal formulas are encoded using
%     until(Name, NameFirstFormula, NameSecondFormula)
%     always(Name, NameOfInsideFormula)
%     next(Name, NameOfInsideFormula)
%     eventually(Name, NameOfInsideFormula)    

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% declaring that every literal is a formula

desire(L):- literal(L).

% satisfy(L,T): formula L holds at the time T

% base case
satisfy(L,T) :-
    literal(L), time(T), holds(L,T). 

% fluent formula

satisfy(N,T) :-
    time(T), desire(N), desire(N1), desire(N2), 
    isand(N, N1,N2), satisfy(N1,T), satisfy(N2,T). 

satisfy(N,T) :-
    time(T), desire(N), desire(N1), desire(N2), 
    isor(N, N1,N2), satisfy(N1,T).  

satisfy(N,T) :-
    time(T), desire(N), desire(N1), desire(N2), 
    isor(N, N1,N2), satisfy(N2,T). 

satisfy(N,T) :-
    time(T), desire(N), desire(N1), 
    isnegation(N, N1), not satisfy(N1,T). 

% special formula (goal/occurrence)

satisfy(F,T):- 
    time(T), desire(F),
    goal(F),
    satisfy(F, length). 

satisfy(F,T):- 
    time(T), desire(F),
    happen(F, A), action(A), 
    occ(A, T). 

% temporal formula 

satisfy(N, T) :- 
    time(T), time(T1), 
    until(N, N1, N2), 
    desire(N), desire(N1), desire(N2), 
    T < T1, hf_during(N1, T, T1-1),
    satisfy(N2, T1).

satisfy(N, T) :- 
    time(T),
    until(N, N1, N2), 
    desire(N), desire(N1), desire(N2), 
    satisfy(N2, T).

satisfy(N, T) :- 
    time(T), desire(N), desire(N1), 
    always(N, N1), 
    during(N1, T, length). 

satisfy(N, T) :- 
    time(T), time(T1), 
    desire(N), desire(N1), 
    eventually(N, N1),
    T <= T1, satisfy(N1, T1). 

satisfy(N, T) :- 
    time(T), desire(N), desire(N1), 
    next(N, N1), satisfy(N1, T+1).

during(N,T,T) :- 
    time(T), desire(N), satisfy(N,T).  

during(N,T,T1) :- 
    time(T), time(T1), T < T1,
    desire(N), satisfy(N,T), 
    during(N,T+1,T1).

hide desire(F).
hide satisfy(F,T).
hide during(F,T,T1).
hide isand(N, N1, N2).
hide isor(N, N1, N2).
hide isnegation(N, N1).
hide happen(N, A).
hide always(N, N1).
hide eventually(N, N1).
hide until(N, N1, N2).
hide next(N, N1).