:- op(700,xfy,&).
:- op(650,yfx,=>).

% generation and output of a plan

plans(C,T) :- not(consistent(C,true)),!, nl,
	      write('*** impossible ***'),nl.
plans(C,T) :- plan(C,true,T,T1), nl, output(T1), nl.

output(Xs=>X) :- !, output1(Xs), write(X), write('.'), nl.

output1(Xs=>X) :- !, output1(Xs), write(X), write(' ;'), nl.
output1(X) :- write(X), write(' ;'), nl.

% top level of main recursive loop

plan(X&C,P,T,T2) :- !, solve(X,P,T,P1,T1), plan(C,P1,T1,T2).
plan(X,P,T,T1) :- solve(X,P,T,P1,T1).

% to solve a goal

solve(X,P,T,P,T) :- always(X) ; X.
solve(X,P,T,P1,T) :- holds(X,T), and(X,P,P1).
solve(X,P,T,X&P, T1) :- add(X,U), achieve(X,U,P,T,T1).

% methods of achieving an action
% 1} by extension

achieve(X,U,P,T,T1=>U) :- preserves(U,P),
			  can(U,C),
			  consistent(C,P),
			  plan(C,P,T,T1),
			  preserves(U,P).
% 2} by insertion

achieve(X,U,P,T=>V,T1=>V) :- preserved(X,V),
			     retrace(P,V,P1),
			     achieve(X,U,P1,T,T1),
			     preserved(X,V).

% check if a fact holds in given state

holds(X,T=>V) :- add(X,V).
holds(X,T=>V) :- !, preserved(X,V),
		 holds(X,T),
		 preserved(X,V).
holds(X,T) :- given(T,X).

% prove that an action preserves a fact

preserves(U,X&C) :- preserved(X,U), preserves(U,C).
preserves(_,true).

preserved(X,V) :- numbervars(X&V,0,N),
		  del(X,V), !, fail.
preserved(_,_).

% retracing an already achievedgoal

retrace(P,V,P2) :- can(V,C),
		   retrace1(P,V,C,P1),
		   append(C,P1,P2).
retrace1(X&P,V,C,P1) :- add(Y,V),
		        equiv(X,Y), !,
		        retrace1(P,V,C,P1).
retrace1(X&P,V,C,P1) :- elem(Y,C),
			equiv(X,Y), !,
			retrace1(P,V,C,P1).
retrace1(true,V,C,true).
retrace1(X&P,V,C,X&P1) :- retrace1(P,V,C,P1).

% consistency with a goal already achieved

consistent(C,P) :- numbervars(C&P,0,N),
		   imposs(S),
		   not(not(intersect(C,S))),
		   implied(S,C&P), !, fail.
consistent(_,_).

% utilities

and(X,P,P) :- elem(Y,P),
	      equiv(X,Y), !.
and(X,P,X&P).

append(X&C,P,X&P1) :- !, append(C,P,P1).
append(X,P,X&P).

elem(X,Y&C) :- elem(X,Y).
elem(X,Y&C) :- !, elem(X,C).
elem(X,X).

implied(S1&S2,C) :- !, implied(S1,C),
		    implied(S2,C).
implied(X,C) :- elem(X,C).
implied(X,C) :- X.

intersect(S1,S2) :- elem(X,S1),
		    elem(X,S2).

not_equal(X,Y) :- not(X=Y),
		  not(X='$VAR'(_)),
		  not(Y='$VAR'(_)).

equiv(X,Y) :- not(nonequiv(X,Y)).

nonequiv(X,Y) :- numbervars(X&Y,0,N),
		 X=Y, !,
		 fail.
nonequiv(_,_).