%%% ActualCauses-Blocks_2022.pl - the blocks world domain (with One-Step Regression) 
%%% Copyright (c) 2020, 2022  Shakil Khan and Mikhail Soutchanski
%%% License: this source code is provided under the MIT License as stated at
%%%             https://opensource.org/license/MIT
%%%
%%% This is a preliminary, not optimized version of the reasoner about actual 
%%% causes as described in the ECAI 2020 paper
%%%    Shakil M. Khan, Mikhail Soutchanski 
%%%    Necessary and Sufficient Conditions for Actual Root Causes. 
%%%    Proc. of the 24th European Conference on Artificial Intelligence (ECAI)
%%% https://www.cs.ryerson.ca/~mes/publications/KhanSoutchanskiNecessarySufficientConditions4ActualRootCauses_ECAI-2020.pdf
%%% This implementation cannot handle quantified effects. 
%%%
%%% Implementation of regression is motivated by the implementation of holds(Formula,S)
%%% that is provided in the Golog interpreter posted at
%%%     https://www.cs.toronto.edu/cogrobo/kia/gologinterpreter
%%%  as part of online resources for Ray Reiter book "Knowledge in Action" at
%%%      https://www.cs.toronto.edu/cogrobo/kia/
%%% -------------------------------------------------------------------------


%:- style_check(-discontiguous).
%:- set_prolog_flag(optimise, true).

:- dynamic restoreSitArg/3.

:- op(250,xfx, 'eqlsTo'). 	% equality
:- op(300,fx,'neg').		% Negation
:- op(400,xfy,'and').		% Conjunction
:- op(500,xfy,'or').		% Disjunction
:- op(600,xfy,'implies').	% Implication
:- op(650,xfy,'iff').		% Equivalence

:- op(700,xfy,==>).  % Extra connective used in Simplification Rules. 
%+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

        /*      Domain specific axioms      */

/* restoreSitArg(+Situation_Suppressed_Formula,+Situation, -Formula_with_Situation).*/

restoreSitArg(poss(A),S,poss(A,S)).

restoreSitArg(onTable(X),S,onTable(X,S)). 
restoreSitArg(on(X,Y),S,on(X,Y,S)). 
restoreSitArg(clear(X),S,clear(X,S)). 

%%% INITIAL STATE AXIOMS %%%
/*
    a    p
    b    q    c   d  
  -------------------
*/
clear(a, []). clear(c, []). clear(d,[]).
on(a, b, []). 
on(p,q,[]).
onTable(b,[]). onTable(c,[]). onTable(d,[]). 
onTable(q,[]). 

%%% SUCCESSOR STATE AXIOMS %%%
/* In this implementation, all relational fluents are reified as terms 
   to facilitate manipulation of formulas. Syntax: 
   ssa( f(ObjArgs, [Act | Sit]), Condition),
where Condition can be the single element list [true], if Act makes fluent f
true in the situation that results from executing Act in Sit, or 
the single element list [false], if Act makes fluent false in the situation that
results from executing Act in Sit. Otherwise, Condition is a list of terms
representing conjunction of formulas characterizing when fluent f remains true
in situation  [Act | Sit], if it is true in Sit. 
   The following implementatio is motivated by the program provided at
    https://www.cs.toronto.edu/cogrobo/kia/simpleBlocksWorld   
*/
   
/* Action move block B from another block to the table makes fluent onTable(B) 
    true in the resulting situation */
ssa(onTable(B, [moveToTable(B,_)|_]), [true]).  

/* Action move block B from the table onto another block makes fluent onTable(B) 
    false in the resulting situation.  */
ssa(onTable(B, [moveFromTable(B,_)|_]), [false]).
ssa(onTable(B, [moveFromTable(X,_)|_]), [neg B eqlsTo X, onTable(B)]).
ssa(onTable(B, [A|_]), [neg Name eqlsTo moveFromTable, onTable(B)]):- A =.. [Name|_].

/* After moving block X from block Y to another block Z, represented as action
  move(X,Y,Z), fluent on(X,Z) becomes true, fluent on(X,Y) becomes false, fluent 
  clear(Y) becomes true, fluent clear(Z) becomes false, nothing else changes.*/
  
ssa(on(B1, B2, [move(B1,_,B2)|_]), [true]).
ssa(on(B1, B2, [moveFromTable(B1,B2)|_]), [true]).
ssa(on(B1, B2, [move(B1,B2,_)|_]), [false]).
ssa(on(B1, B2, [move(X,_,_)|_]), [neg B1 eqlsTo X, on(B1, B2)]).
ssa(on(B1, B2, [moveToTable(X,Y)|_]), [neg B1 eqlsTo X, neg B2 eqlsTo Y, on(B1, B2)]).
ssa(on(B1, B2, [A|_]), [neg Name eqlsTo move, neg Name eqlsTo moveToTable, on(B1, B2)]):- A =.. [Name|_].

ssa(clear(B, [move(_,B,_)|_]), [true]).
ssa(clear(B, [moveToTable(_,B)|_]), [true]).
ssa(clear(B, [move(_,_,B)|_]), [false]).
ssa(clear(B, [moveFromTable(_,B)|_]), [false]).
ssa(clear(B, [move(_,_,X)|_]), [neg B eqlsTo X, clear(B)]).
ssa(clear(B, [moveFromTable(_,X)|_]), [clear(B), neg B eqlsTo X]).
ssa(clear(B, [A|_]), [neg Name eqlsTo move, neg Name eqlsTo moveFromTable, clear(B)]):- A =.. [Name|_].

%%% PRECONDITION AXIOMS %%%

poss(move(B1,B2,B3), [clear(B1), clear(B3), B1 \= B3, on(B1,B2)]).

poss(moveToTable(B1,B2), [clear(B1), on(B1,B2)]).

poss(moveFromTable(B1,B2), [onTable(B1), clear(B1), clear(B2), B1 \= B2]).

%+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

/* primCause(+Effect, +Scenario, -Primary_Cause) */ 
/* Primary_Cause is a list such that the first item of the list is an action
   responsible for change in a given effect formula, while the rest of the list 
   represents situation where action was executed.
*/

primCause(_,[],[]).
/* Case 1: effect formula E is true after doing A in situation S, 
       but it was already true in S. In this case, A is not a primary cause.
       Consider remaining actions in S recursively.           */
primCause(E,[A|S],C) :- regress(E,[A|S],true), regress(E,S,true), 
                        primCause(E,S,C), !.
/* Case 2: effect formula E becomes true after doing A in situation S, 
       but previously it was false in S. In this case, A is a primary cause. */
primCause(E,[A|S],[A|S]) :- regress(E,[A|S],true), regress(E,S,false).

/* causalChain(+EffectFormula, +Scenario, -Causal_Chain) */
/* Causal_Chain is a list of the form [(A1,S1),(A2,S2),...,(An,Sn)], 
   where (A1,S1) is the primary cause, 
   (A2,S2) is the secondary cause, etc.
   As usual, each situation S here is a list of actions. 
*/ 
 
/* causalChain(true,_,[]). */ 
/* causalChain(_,[],[]).   */ 

causalChain(E,S,[]) :- primCause(E,S,[]),!. 

causalChain(E,[A],[ (ActCause,[]) ] ) :- primCause(E,[A],ActCause), 
                                        not ActCause = [ ], !.

causalChain(E,[A | S], [ (ActCause,Sit) | OtherCauses] ) :- 
    primCause(E,[A | S],[ActCause | Sit]), 
	rho(E,[ActCause | Sit],R1), rho(poss(ActCause),Sit,R2), 
	pack([R1,R2],X), simplify(X,Y), 
	causalChain(Y,Sit,OtherCauses).

%+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

/* pack(+List_of_Conjuncts, -Formula_Representing_the_Conjunction_of_the_Items_in_the_List */

pack([E],E).
pack([E|L],R):- pack(L,R2), R = E and R2.

%+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

/* regress(+Formula, +Situation, -Regressed_Formula) 
 Regression operator regress does not handle quantifiers. Implementation here is
 similar to the program provided at 
     https://www.cs.toronto.edu/cogrobo/kia/regressionTheoremProver
*/


regress(P and Q, S, R) :- regress(P,S,R1),
                     (R1 = false, !, R = false;
                      regress(Q,S,R2), simplify(R1 and R2,R),!).

regress(P or Q, S, R) :- regress(P,S,R1),
                     (R1 = true, !, R = true ;
                      regress(Q,S,R2), simplify(R1 or R2,R),!).

regress(P implies Q,S,R) :- regress(neg P or Q,S,R),!.

regress(P iff Q,S,R) :- regress((P implies Q) and (Q implies P),S,R),!.

regress(neg(neg P),S,R) :- regress(P,S,R),!.

regress(neg(P and Q),S,R) :- regress(neg P or neg Q,S,R),!.

regress(neg(P or Q),S,R) :- regress(neg P and neg Q,S,R),!.

regress(neg(P implies Q),S,R) :- regress( P and neg Q),S,R),!.

regress(neg(P iff Q),S,R) :- regress( (P and neg Q) or (Q and neg P),S,R),!.

regress(neg P,S,R) :- isAtom(P), regress(P,S,R1), simplify(neg R1,R),!.

/* Retrieve and regress the RHS of the APA. */
regress(poss(A),S,R) :- poss(A,L), pack(L,F), simplify(F,M), regress(M,S,R),!. 

regress(P eqlsTo Q,_,R):- (P=Q, R=true; P\=Q, R=false),!.

/* A is a defined atom. Retrieve and regress its definition. */
regress(A,[T|S],R) :- isAtom(A), restoreSitArg(A,[T|S],FluentWithSit), 
       ssa(FluentWithSit,W), % match with SSA for FluentWithSit
       pack(W,F),         % convert list W into conjunction of sub-formulas F
       simplify(F,X),     % do obvious simplification of F, if possible
       regress(X,S,R), !. % continue regressing recursively until the init sit

/* A is an atom, but it has no definition, so the regression is finished. */
regress(A,_,R) :- isAtom(A),
                not(ssa(A,_)),   
                (A = false, R = false, !;
                 restoreSitArg(A,[],F_init), F_init, R = true, !;
                 restoreSitArg(A,[],F_init), \+ F_init, R = false, !;
                 %% otherwise A is not fluent, but another atom: call it
                 \+ restoreSitArg(A,[],_), A, R = true, !;
                 \+ restoreSitArg(A,[],_), \+ A, R = false, !;		 
                 R = A).
 
%+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

/* rho(+Formula, +Situation, -Single_Step_Regressed_Formula) */
/* One-step regression operator rho does not handle quantifiers */

rho(P and Q, S,R) :- rho(P,S,R1),
                     (R1 = false, R = false, !;
                      rho(Q,S,R2), simplify(R1 and R2,R),!).

rho(P or Q, S,R) :- rho(P,S,R1),
                     (R1 = true, R = true, !;
                      rho(Q,S,R2), simplify(R1 or R2,R),!).

rho(P implies Q,S,R) :- rho(neg P or Q,S,R),!.

rho(P iff Q,S,R) :- rho((P implies Q) and (Q implies P),S,R),!.

rho(neg(neg P),S,R) :- rho(P,S,R),!.

rho(neg(P and Q),S,R) :- rho(neg P or neg Q,S,R),!.

rho(neg(P or Q),S,R) :- rho(neg P and neg Q,S,R),!.

rho(neg(P implies Q),S,R) :- rho(neg(neg P or Q),S,R),!.

rho(neg(P iff Q),S,R) :- rho(neg((P implies Q) and (Q implies P)),S,R),!.

rho(neg P,S,R) :- isAtom(P), rho(P,S,R1), simplify(neg R1,R),!.

/* Retrieve the RHS of the APA. */
rho(poss(A),_,R) :- poss(A,L), pack(L,F), simplify(F,R),!. 

rho(P eqlsTo Q,_,R):- (P=Q, R=true; P\=Q, R=false),!.

/* A is a defined atom. Retrieve its definition. */
rho(A,[T|S],R) :- isAtom(A), restoreSitArg(A,[T|S],A1), ssa(A1,W), pack(W,F),   
                simplify(F,R),!.

/* A is an atom, but it has no definition, so the regression is finished. */
rho(A,_,R) :- isAtom(A),
                not(ssa(A,_)),   
                (A = false, R = false, !;
                 restoreSitArg(A,[],Ai), Ai, R = true, !;
                 restoreSitArg(A,[],Ai), \+ Ai, R = false, !;
                 \+ restoreSitArg(A,[],_), A, R = true, !;
                 \+ restoreSitArg(A,[],_), \+ A, R = false, !;		 
                 R = A).
 
%+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
/*
Simplification rules in this program are similar to the rules provided at
    https://www.cs.toronto.edu/cogrobo/kia/primeImplicateCompiler
*/
simplify(W1 and W2,S) :- simplify(W1,S1), simplify(W2,S2),
                       simplify1(S1 and S2,S), !.
simplify(W1 or W2,S) :- simplify(W1,S1), simplify(W2,S2),
                       simplify1(S1 or S2,S), !.
simplify(neg W,S) :- simplify(W,S1), simplify1(neg S1,S), !.
simplify(A,S) :- simplify1(A,S).

simplify1(W,Simp) :- W ==> Simp, !.
simplify1(W,W).

%  Simplification Rules.

true and P ==> P.         P and true ==> P.       false and _P ==> false.
_P and false ==> false.    true or _P ==> true.    _P or true ==> true.
false or P ==> P.        P or false ==> P.      neg true ==> false.
neg false ==> true.        X eqlsTo X ==> true.
X eqlsTo Y ==> false :- not(X = Y).

%+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

/* sub(Name,New,Term1,Term2): Term2 is Term1 with Name replaced by New. 
   This predicate is implemented in the software provided at
    https://www.cs.toronto.edu/cogrobo/kia/gologinterpreter
*/

sub(_,_,T1,T2) :- var(T1), T2 = T1.
sub(X1,X2,T1,T2) :- \+ var(T1), T1 = X1, T2 = X2.
sub(X1,X2,T1,T2) :- \+ T1 = X1, T1 =..[F|L1], sub_list(X1,X2,L1,L2),
                    T2 =..[F|L2].
sub_list(_,_,[],[]).
sub_list(X1,X2,[T1|L1],[T2|L2]) :- sub(X1,X2,T1,T2), sub_list(X1,X2,L1,L2).

%+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

isAtom(A) :- not(A = neg W; A = (W1 and W2); A = (W1 or W2); 
                 A = (W1 implies W2); A = (W1 iff W2); 
                 A = W1 eqlsTo W2; A = exists(X,W); A = forall(X,W)).

%+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
%+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

/* Some test cases: */
/* The situation (trace) in the query should be written as cause(EffectFormula, Trace-in-reverse-order, Cause). 
   Thus, if the actions performed are S0->a1->a2->a3, i.e. <a1,a2,a3> starting 
   from S0, then the trace in the query is written as [a3,a2,a1] with the most 
   recent action a3 written as the head of the list. 
   It is recommended to test with queries that are difficult for other 
   approaches to actual causality. Namely, pre-emption examples and 
   over-determination examples are sometimes handled incorrectly by others.
*/

/* regress(clear(a),[],R). */
/* regress(clear(b), [moveToTable(a, b)],R). */
/* regress(clear(a), [moveFromTable(c, a)],R). */
/* regress(poss(moveToTable(a,b)),[moveFromTable(c,d)],R). */

/*
?- causalChain(onTable(p), [moveToTable(c,d), moveToTable(a,b), moveFromTable(c,d)], C).
No (0.00s cpu)
    - Note the query fails because the effect formula onTable(P) is false: 
    block p is not on the table initially, and none of the actions in the trace
    moved it to the table.
    
?- causalChain(onTable(q), [moveToTable(c, d), moveToTable(a, b), moveFromTable(c, d)], C).
C = []
Yes (0.00s cpu)
    - Note the query succeeds, but the list of actual causes is empty because 
      block q is initially on the table, and this fact has no actual causes.
*/

/* causalChain(clear(a),[moveFromTable(a, b), moveToTable(a, b), moveFromTable(c, d)],C). 
- causalChain(clear(a), [moveFromTable(a, b), moveToTable(a, b), moveFromTable(c, d)], C).
C = []
Yes (0.00s cpu)
Note that block a is clear initially and none of the actions changed this fluent.
Therefore, the list of actual causes for the effect formula  clear(a) is empty.
*/

/* causalChain(neg on(a,b),[moveToTable(a,b)],CC). 
    ?- causalChain(neg on(a, b), [moveToTable(a, b)], CC).
    CC = [([moveToTable(a, b)], [])]
    Yes (0.00s cpu)
A negated effect is answered correctly.
*/

/* causalChain(onTable(a),[moveToTable(c,d),moveToTable(a,b),moveFromTable(c,d)],C). 
?- causalChain(onTable(a), [moveToTable(c, d), moveToTable(a, b), moveFromTable(c, d)], C).
C = [(moveToTable(a, b), [moveFromTable(c, d)])]
Yes (0.00s cpu, solution 1, maybe more)
No (0.00s cpu)
The primary cause for effect onTable(a) is the 2nd action in the trace: moveToTable(a,b)
All other actions in the trace are irrelevant.
*/

/* causalChain(onTable(a),[moveFromTable(c,a),moveToTable(c,d),moveToTable(a,b),moveFromTable(c,d)],C). 
?- causalChain(onTable(a), [moveFromTable(c, a), moveToTable(c, d), moveToTable(a, b), moveFromTable(c, d)], C).
C = [(moveToTable(a, b), [moveFromTable(c, d)])]
Yes (0.00s cpu, solution 1, maybe more)
No (0.00s cpu)

?- causalChain(onTable(a), [moveFromTable(c, a), moveToTable(c, d), moveFromTable(c, d), moveToTable(a, b)], C).
C = [(moveToTable(a, b), [])]
Yes (0.00s cpu, solution 1, maybe more)
No (0.00s cpu)
*/
/* causalChain(onTable(a),[moveToTable(a,b),moveFromTable(a,b),moveToTable(a,b),moveFromTable(c,d)],C). 
?- causalChain(onTable(a), [moveToTable(a, b), moveFromTable(a, b), moveToTable(a, b), moveFromTable(c, d)], C).
C = [(moveToTable(a, b), [moveFromTable(a, b), moveToTable(a, b), moveFromTable(c, d)]), 
        (moveFromTable(a, b), [moveToTable(a, b), moveFromTable(c, d)]), 
            (moveToTable(a, b), [moveFromTable(c, d)])]
Note that the last action moveToTable(a,b) is the primary cause for effect onTable(a).
But this action is possible only if previously block a was not on the table.
This precondition is enabled by the secondary cause moveFromTable(a,b). However,
this action is possible if block a is on the table, and since it is not on
the table initially, there is an actual cause, action moveToTable(a,b), for
the latter precondition. This is the tertiary cause for the effect in query onTable(a).
Yes (0.00s cpu, solution 1, maybe more)
No (0.00s cpu)
*/

/*
Example with 27 actions, 2 relevant actions, and a conjunctive effect: 

causalChain(clear(b) and on(b,a),[moveFromTable(b,a),moveToTable(p,q),moveToTable(c,d),moveFromTable(c,d),moveToTable(c,d),moveFromTable(c,d),moveToTable(c,d),moveFromTable(c,d),moveToTable(c,d),moveFromTable(c,d),moveToTable(c,d),moveFromTable(c,d),moveToTable(c,d),moveFromTable(c,d),moveToTable(c,d),moveFromTable(c,d),moveToTable(c,d),moveFromTable(c,d),moveToTable(c,d),moveFromTable(c,d),moveToTable(c,d),moveFromTable(c,d),moveToTable(c,d),moveToTable(a,b),moveFromTable(c,d),moveToTable(c,d),moveFromTable(c,d)],CC).

In the above, only 2 acts are relevant: the last one, moveFromTable(b,a), and the 4th one, moveToTable(a,b).
All other irrelevant actions repeatedly move block c from the table to d, and then move c back to the table.
This example dmonstartes our program can deal with irrelevant actions correctly.

*/

