%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% computing the truth value of fluent formula
% a fluent formula is assigned a name
% which is declared by the predicate 
%     is_formula(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

is_formula(L):- literal(L).

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

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

% fluent formula

hf(N,T) :-
    time(T), is_formula(N), is_formula(N1), is_formula(N2), 
    isand(N, N1,N2), hf(N1,T), hf(N2,T). 

hf(N,T) :-
    time(T), is_formula(N), is_formula(N1), is_formula(N2), 
    isor(N, N1,N2), hf(N1,T).  

hf(N,T) :-
    time(T), is_formula(N), is_formula(N1), is_formula(N2), 
    isor(N, N1,N2), hf(N2,T). 

hf(N,T) :-
    time(T), is_formula(N), is_formula(N1), 
    isnegation(N, N1), not hf(N1,T). 

%%% syntactic sugar: exists -- could be used for disjunction 

hf(N, T) :- 
    time(T), is_formula(N), is_formula(N1), 
    exists(N, N1), hf(N1,T). 

% temporal formula 

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

hf(N, T) :- 
    time(T),
    until(N, N1, N2), 
    is_formula(N), is_formula(N1), is_formula(N2), 
    hf(N2, T).

hf(N, T) :- 
    time(T), is_formula(N), is_formula(N1), 
    always(N, N1), 
    hf_during(N1, T, length). 

hf(N, T) :- 
    time(T), time(T1), 
    is_formula(N), is_formula(N1), 
    eventually(N, N1),
    T <= T1, hf(N1, T1). 

hf(N, T) :- 
    time(T), is_formula(N), is_formula(N1), 
    next(N, N1), hf(N1, T+1).

hf_during(N,T,T) :- 
    time(T), is_formula(N), hf(N,T).  

hf_during(N,T,T1) :- 
    time(T), time(T1), T < T1,
    is_formula(N), hf(N,T), 
    hf_during(N,T+1,T1).

hide is_formula(F).
hide hf(F,T).
hide hf_during(F,T,T1).