1% A REGRESSION PLANNER FOR ACTIONS IN STRIPS NOTATION
    2% WITH LOOP DETECTION + HEURISTIC INFORMATION ON UNSATISFIABLE GOALS
    3
    4% solve(G,AS,NS,P) is true if P is a plan to solve goal G that uses 
    5% less than NS steps.
    6% G is a list of atomic subgoals. AS is the list of ancestor goal lists.
    7
    8solve(G,N,P) <-
    9   solve(G,[G],N,P).
   10
   11solve(G,_,_,init) <-
   12   solved(G).
   13
   14solve(G,AS,NAs,do(A,Pl)) <-
   15   NAs > 0 &
   16   satisfiable(G) &
   17   useful(G,A) &
   18   wp(G,A,G1) &
   19   ~ subgoal_loop(G1,AS) &
   20   NA1 is NAs-1 &
   21   solve(G1,[G1|AS],NA1,Pl).
   22
   23% subgoal_loop(G,AS) is true if we are in a loop of subgoals to solve.
   24% This occurs if G is a more difficult to solve goal than one of its ancestors
   25subgoal_loop(G1,AS) <- 
   26   grnd(G1)& member(An,AS)&  subset(An,G1).
   27
   28% solved(G) is true if goal list G is true initially
   29solved([]).
   30solved([G|R]) <-
   31   holds(G,init) &
   32   solved(R).
   33
   34% satisfiable(G) is true if (based on a priori information) it is possible for
   35%  goal list G to be true all at once.
   36satisfiable(G) <-
   37   ~ unsatisfiable(G).
   38
   39% useful(G,A) is true if action A is useful to solve a goal in goal list G
   40% we try first those subgoals that do not hold initially
   41useful([S|R],A) <-
   42   holds(S,init) &
   43   useful(R,A).
   44useful([S|_],A) <-
   45   achieves(A,S).
   46useful([S|R],A) <-
   47   ~ holds(S,init) &
   48   useful(R,A).
   49
   50% domain specific rule about what may be useful to solve even if it was true
   51%  initially. 
   52useful(G,A) <-
   53   member(S,G) &
   54   member(S,[handempty])& % handempty is the only such goal in this domain
   55   holds(S,init) &
   56   achieves(S,A).
   57
   58% wp(G,A,G0) is true if G0 is the weakest precondition that needs to hold
   59% immediately before action A to ensure that G is true immediately after A
   60wp([],A,G1) <-
   61   preconditions(A,G) &
   62   filter_derived(G,[],G1).
   63wp([S|R],A,G1) <-
   64   wp(R,A,G0) &
   65   regress(S,A,G0,G1).
   66
   67% regress(Cond,Act,SG0,SG1) is true if regressing Cond through Act
   68% starting with subgoals SG0 produces subgoals SG1
   69regress(S,A,G,G) <-
   70   achieves(A,S).
   71regress(S,A,G,G1) <-
   72   primitive(S) &
   73   ~ achieves(A,S) &
   74   ~ deletes(A,S) &
   75   insert(S,G,G1).
   76
   77filter_derived([],L,L).
   78filter_derived([G|R],L,[G|L1]) <-
   79   primitive(G) &
   80   filter_derived(R,L,L1).
   81filter_derived([A \= B | R],L,L1) <-
   82   dif(A,B) &
   83   filter_derived(R,L,L1).
   84filter_derived([G|R],L0,L2) <-
   85   (G <- B) &
   86   filter_derived(R,L0,L1) &
   87   filter_derived(B,L1,L2).
   88
   89regress_all([],_,G,G).
   90regress_all([S|R],A,G0,G2) <-
   91   regress(S,A,G0,G1) &
   92   regress_all(R,A,G1,G2).
   93
   94% =============================================================================
   95
   96% member(X,L) is true if X is a member of list L
   97member(X,[X|_]).
   98member(X,[_|L]) <-
   99   member(X,L).
  100
  101notin(_,[]).
  102notin(A,[B|C]) <-
  103   dif(A,B) &
  104   notin(A,C).
  105
  106% subset(L1,L2) is true if L1 is a subset of list L2
  107subset([],_).
  108subset([A|B],L) <-
  109   member(A,L) &
  110   subset(B,L).
  111
  112% insert(E,L0,L1) inserts E into list L0 producing list L1.
  113% If E is already a member it is not added.
  114insert(A,[],[A]).
  115insert(A,[B|L],[A|L]) <- A==B.
  116insert(A,[B|L],[B|R]) <-
  117   ~ A == B &
  118   insert(A,L,R).
  119grnd(G) <-
  120   numbervars(G,0,_).
  121
  122% =============================================================================
  123% DOMAIN SPECIFIC KNOWLEDGE
  124unsatisfiable(L) <-
  125   member(sitting_at(X1,Y1),L) &
  126   member(sitting_at(X2,Y2),L) &
  127   X1 == X2 &
  128   ~ (Y1=Y2).
  129unsatisfiable(L) <-
  130   member(sitting_at(X1,_),L) &
  131   member(carrying(_,Y2),L) &
  132   X1 == Y2.
  133unsatisfiable(L) <-
  134   member(carrying(X1,Y1),L) &
  135   member(carrying(X2,Y2),L) &
  136   Y1 == Y2 &
  137   (X1\=X2).
  138
  139% TRY THE FOLLOWING QUERIES with delrob_strips.pl:
  140% solve([carrying(rob,k1)],5,P).
  141% solve([sitting_at(k1,lab2)],8,P).
  142% solve([carrying(rob,parcel),sitting_at(rob,lab2)],10,P).
  143% solve([sitting_at(rob,lab2),carrying(rob,parcel)],10,P).