1/*
    2% NomicMUD: A MUD server written in Prolog
    3%
    4% Some parts used Inform7, Guncho, PrologMUD and Marty's Prolog Adventure Prototype
    5% 
    6% July 10,1996 - John Eikenberry 
    7% Copyright (C) 2004 Marty White under the GNU GPL
    8% 
    9% Dec 13, 2035 - Douglas Miles
   10%
   11%
   12% Logicmoo Project changes:
   13%
   14% Main file.
   15%
   16*/
   17
   18
   19
   20%:- if((prolog_load_context(file,F),prolog_load_context(source,F))).
   21%:- style_check(-singleton).
   22
   23/*
   24
   25   ABDUCTIVE EVENT CALCULUS
   26
   27   MURRAY SHANAHAN
   28   Version 1.15
   29   July 1998
   30   Written for LPA MacProlog 32
   31
   32*/
   33
   34
   35/*
   36   This is an abductive meta-interpreter for abduction with negation-as-
   37   failure, with built-in features for handling event calculus queries.
   38   In effect this implements a partial-order planner. not(clipped) facts
   39   correspond to protected links. The planner will also perform
   40   hierarchical decomposition, given definitions of compound events
   41   (happens if happens clauses).
   42
   43   The form of queries is as follows.
   44
   45        abdemo(Goals,Residue)
   46
   47   Goals is a list of atoms. Residue is a pair of [RH,RB], where RH is a
   48   list of happens facts and RB is a list of temporal ordering facts.
   49   Negations is a list of lists of atoms.
   50
   51   Roughly speaking, the above formulae should hold if,
   52
   53        EC and CIRC[Domain] and CIRC[Residue] |= Goals
   54
   55   where EC is the event calculus axioms, CIRC[Domain] is the completion
   56   of initiates, terminates and  releases, and CIRC[Residue] is the
   57   completion of happens. (Note that completion isn't applied to temporal
   58   ordering facts.)
   59
   60   F is expected to be fully bound when we call abdemo(holds_at(F,T)).
   61   It's assumed that all primitive actions (two argument happens) are
   62   in the residue (ie: none are in the program).
   63
   64   Although the interpreter will work with any logic program, the axioms of
   65   the event calculus are compiled in to the meta-level.
   66
   67   The function symbol "neg" is introduced to represent classically
   68   negated fluents. holds_at(neg(F)) corresponds to not holds_at(F)
   69   (with classical "not"). terminates formulae play a role in clipping
   70   positive fluents and initiating negative fluents. Conversely,
   71   initiates formulae play a role in clipping negative fluents and
   72   initiating positive ones.
   73
   74   Computation interleaves search (abdemo) and refinement phases. After each
   75   step of the computation, where a step is an iteration of abdemo or a
   76   refinement, the residue so far plus the remaining goal list entail the goal
   77   state. In other words, these computational steps are also proof steps.
   78
   79   An iterative deepening search strategy is employed, where depth
   80   corresponds to length of plan.
   81*/
   82
   83% :- style_check(+discontiguous).
   84/* TOP LEVEL */
   85
   86
   87/*
   88   Top level calls to abdemo have to be transformed to the following form.
   89
   90        abdemo_top(Goals,ResidueIn,ResidueOut,NegationsIn,NegationsOut,DepthBound)
   91
   92   The residue has the form [[HA,HC],[BA,BC]], where HA is a list of happens
   93   atoms, HC is the transistive closure of the b-or-equal relation on times
   94   that follows from HA, BA is a list of before "b" atoms, and BC is the transitive
   95   closure of BA.
   96*/
   97
   98abdemo(Gs,[HA,BA]) :-
   99     init_gensym(t), first_d(D),
  100     abdemo_top(Gs,[[[],[]],[[],[]]],[[HA,HC],[BA,BC]],[],N,D),
  101     write_plan_len(HA,BA).
  102
  103abdemo_timed(Gs,[HA,BA]) :-
  104     ticks(Z1),
  105     abdemo(Gs,[HA,BA]),
  106     write_plan(HA,BA),
  107     ticks(Z2), Z is (Z2-Z1)/60, write('Total time taken '), writeYesln(Z).
  108abdemo_top(Gs,R1,R3,N1,N3,D, _MaxDepth, _HighLevel) :-
  109  must(nonvar(Gs)),
  110  abdemo_id(Gs,R1,R2,N1,N2,D), !, 
  111  abdemo_cont(R2,R3,N2,N3).
  112
  113/*
  114   abdemo_cont carries out one step of refinement, if necessary. It then
  115   resumes abdemo, but with an initial depth bound equal to the length of
  116   the plan so far. Obviously to start from 1 again would be pointless.
  117*/
  118
  119abdemo_cont([[HA,TC],RB],[[HA,TC],RB],N,N) :- all_executable(HA), !.
  120
  121abdemo_cont([[HA,HC],[BA,BC]],R2,N1,N3) :-
  122     %write('Abstract plan: '), write(HA), writeYesln(BA),
  123     dbginfo('Abstract plan:'=[HA,BA]),
  124     refine([[HA,HC],[BA,BC]],N1,Gs,R1,N2), action_count([[HA,HC],[BA,BC]],D),
  125     abdemo_top(Gs,R1,R2,N2,N3,D).
  126
  127
  128/* abdemo_id is an iterative deepening version of abdemo. */
  129
  130abdemo_id(Gs,R1,R2,N1,N2,D) :-
  131     write(' D'), write(D), write(' '), ttyflush, 
  132  (abdemo(Gs,R1,R2,N1,N2,D)*-> true; (next_d(D,D2)->abdemo_id(Gs,R1,R2,N1,N2,D2))).
  133
  134
  135
  136all_executable(X):- \+ is_list(X),!,fail.
  137all_executable([]).
  138all_executable([H|R]) :- was_executable(H), all_executable(R).
  139
  140was_executable(H):- H = happens(A,_T1,_T2), must(executable(A)).
  141
  142
  143general_interp:- true.
  144
  145/* ABDEMO */
  146
  147
  148/*
  149   abdemo/6 is a depth bounded abdemo. It fails if it can't generate a plan
  150   with DepthBound or fewer steps. Calls to abdemo/6 have the following form.
  151
  152        abdemo(Goals,ResidueIn,ResidueOut,
  153             NegationsIn,NegationsOut,DepthBound)
  154
  155*/
  156
  157
  158
  159/*
  160abdemo(Gs,[[HA,TC1],[BA,TC2]],R,N1,N2,D) :- 
  161    setup_call_cleanup((notrace((
  162    (( N1 \== [], Gs == [] ); ( N1 == [], Gs \== [] ); ( N1 \== [], Gs \== [] )),
  163     %is_dbginfo(trace=on), 
  164     dbginfo('Goals'=Gs),
  165     dbginfo('Happens'=HA),
  166     dbginfo('Befores'=BA),
  167     dbginfo('Nafs'=N1),nl,nl,fail))),true,true).
  168*/
  169abdemo([],R,R,N,N,D).
  170abdemo([G|Gs],R1,R2,N1,N2,D):- 
  171  abdemo_cons(G,Gs,R1,R2,N1,N2,D).
  172
  173
  174check_goals([]):-!.
  175check_goals([H|T]):-check_goal(H),!,check_goals(T).
  176check_goal(b(T1,T2)):- T1=@=T2,!,barf.
  177check_goal(_).
  178
  179maybe_note_ab(Why,H,T,[[HA,TC1],[BA,TC2]],R,N1,N2,D) :- 
  180    Gs=[H|T],
  181    setup_call_cleanup((notrace((
  182    (( N1 \== [], Gs == [] ); ( N1 == [], Gs \== [] ); ( N1 \== [], Gs \== [] )),
  183     %is_dbginfo(trace=on), 
  184     dbginfo('Why'=Why),
  185   %  dumpST,
  186     dbginfo('Goals'=Gs),
  187     dbginfo('Happens'=HA),
  188     dbginfo('Befores'=BA),     
  189     dbginfo('Nafs'=N1),nl,nl,fail))),true,true),fail.
  190
  191:- discontiguous abdemo_cons/7.  192:- discontiguous abdemo_cons/7.  193
  194% merge H
  195% abdemo_cons(H,[HH|Gs],R1,R4,N1,N3,D):- H=@=HH, !, abdemo_cons(H,Gs,R1,R4,N1,N3,D).
  196
  197abdemo_cons(b(X,Y),Gs1,R1,R3,N1,N2,D) :-
  198     abresolve_b(b(X,Y),R1,Gs2,R2,B), append(Gs2,Gs1,Gs3),
  199     notrace((iv_list_to_set(Gs3,Gs4),(((Gs3\==Gs4)-> (!,fail) ; true)))),
  200     ignore(Gs3 = Gs4),!,
  201     abdemo(Gs4,R2,R3,N1,N2,D).
  202
  203abresolve_b(b(X,Y),R1,[],R2,B) :- !, B = false, 
  204     skolemise_time(X), skolemise_time(Y), 
  205     ((R2=R1,demo_before(X,Y,R2)) -> true ; 
  206        (\+ demo_beq(Y,X,R1),
  207        add_before(X,Y,R1,R2))).
  208
  209abdemo_cons(H,Gs, R1,R4,N1,N3,D):- maybe_note_ab(abdemo_cons, H,Gs,R1,R4,N1,N3,D),fail.
  210abdemo_cons(H,Gs,     R1,R4,N1,N3,D):- notrace((check_goals([H|Gs]),fail)).
  211
  212abdemo_cons(H,[HH|Gs],R1,R4,N1,N3,D):- 
  213  iv_list_to_set([H,HH|Gs],Set), Set\=@=[H,HH|Gs],!,
  214  abdemo(Set,R1,R4,N1,N3,D).
  215
  216 % push call for later
  217abdemo_cons(call(P),[H,I|Gs],R1,R4,N1,N3,D):- H\=call(_), !,
  218 abdemo_cons(H,[I,call(P)|Gs],R1,R4,N1,N3,D).
  219% push call for later
  220abdemo_cons((A;B),[H,I|Gs],R1,R4,N1,N3,D):- H\=(A;B), !,
  221 abdemo_cons(H,[I,(A;B)|Gs],R1,R4,N1,N3,D).
  222% push call for later
  223abdemo_cons(call(P),[H|Gs],R1,R4,N1,N3,D):- H\=call(_), !,
  224 abdemo_cons(H,[call(P)|Gs],R1,R4,N1,N3,D).
  225
  226abdemo_cons(H,T,R1,R2,N1,N2,D):- 
  227 KEY = abdemo(H,T,R1,R2,N1,N2),
  228 ((nb_current(last_call_abdemo,Was);Was=[])->
  229 (((member(X,Was),X=@=KEY))
  230  -> (!,fail); 
  231  ((nb_setval(last_call_abdemo,[KEY|Was]),fail)))).
  232
  233abdemo_cons(holds_at(F1,T),Gs1,R1,R3,N1,N3,D):- !,
  234  abdemo_cons_holds_at(F1,T,Gs1,R1,R3,N1,N3,D).
  235
  236
  237/*
  238   Now we have two clauses which are meta-level representations of the two
  239   event calculus axioms for holds_at.
  240
  241        holds_at(F,T) <- initially(F) and not clipped(0,F,T)
  242
  243        holds_at(F,T3) <-
  244             happens(A,T1,T2) and T2 < T3 and
  245             initiates(A,F,T1) and not clipped(T1,F,T2)
  246
  247   Note the way the object-level axioms have been compiled into the
  248   meta-level. Note also that happens goals are not resolved against
  249   clauses in the object-level program. Instead, they're put straight into
  250   the residue. Resolving happens goals is the job of the refinement phase.
  251*/
  252fill_in_tempargs(Pred, F1):- fill_in_tempargs_1(Pred, F1).
  253fill_in_tempargs(Pred, neg(F1)):- fill_in_tempargs_1(Pred, F1).
  254fill_in_tempargs_1(Pred, F1):- call(Pred,X),
  255  functor(X,F,A),functor(F1,F,A),
  256  fill_in_tempargs_each(X,F1).
  257
  258fill_in_tempargs_each(_,F1):- ground(F1),!.
  259fill_in_tempargs_each(_,F1):- findall(F1,in_domain_db(F1),List),iv_list_to_set(List,Set),!,member(F1,Set).
  260
  261in_domain_db(F1):- user:ec_current_domain_db(axiom(Stuff,Body), _),sub_term(F1,Stuff+Body),ground(F1).
  262
  263abdemo_cons_holds_at(F1,T,Gs1,R1,R3,N1,N4,D):- var(F1),!,
  264  fill_in_tempargs(fluent,F1), abdemo_cons_holds_at(F1,T,Gs1,R1,R3,N1,N4,D).
  265abdemo_cons_holds_at(neg(F1),T,Gs1,R1,R3,N1,N4,D):- var(F1),!,
  266  fill_in_tempargs(fluent,F1), abdemo_cons_holds_at(neg(F1),T,Gs1,R1,R3,N1,N4,D).
  267
  268abdemo_cons_holds_at(F1,T,Gs1,R1,R3,N1,N4,D) :-
  269     F1 \= neg(_F2), abresolve(initially(F1),R1,Gs2,R1,B),
  270     append(Gs2,Gs1,Gs3), add_neg_car(clipped(0,F1,T),N1,N2),
  271     abdemo_naf_cons(clipped(0,F1,T),[],R1,R2,N2,N3,D),
  272     abdemo(Gs3,R2,R3,N3,N4,D).
  273
  274/*
  275   The order in which resolution steps are carried out in the next
  276   clause is crucial. We resolve initiates first in order to instantiate 
  277   A, but we don't want to proceed with sub-goals of initiates until
  278   we've added the corresponding happens and before "b" facts to the residue.
  279*/
  280
  281abdemo_cons_holds_at(F1,T3,Gs1,R1,R6,N1,N5,D) :-
  282     F1 \= neg(_F2), abresolve(initiates(A,F1,T1),R1,Gs2,R1,B1),
  283     abresolve(happens(A,T1,T2),R1,[],R2,B2),
  284     check_depth(R2,D),
  285     abresolve(b(T2,T3),R2,[],R3,B3),
  286     append(Gs2,Gs1,Gs3), check_nafs(B2,N1,R3,R4,N1,N2,D),
  287     add_neg_car(clipped(T1,F1,T3),N2,N3),
  288     abdemo_naf_cons(clipped(T1,F1,T3),[],R4,R5,N3,N4,D),
  289     abdemo(Gs3,R5,R6,N4,N5,D).
  290
  291/*
  292   The next two clauses are a meta-level representation of the two
  293   event calculus axioms for not holds_at.
  294
  295        not holds_at(F,T) <- initiallyn(F) and not declipped(0,F,T)
  296
  297        not holds_at(F,T3) <-
  298             happens(A,T1,T2) and T2 < T3 and
  299             terminates(A,F,T1) and not declipped(T1,F,T2)
  300*/
  301
  302abdemo_cons_holds_at(neg(F),T,Gs1,R1,R3,N1,N4,D) :-
  303     abresolve(initially(neg(F)),R1,Gs2,R1,B),
  304     append(Gs2,Gs1,Gs3), add_neg_car(declipped(0,F,T),N1,N2),
  305     abdemo_naf_cons(declipped(0,F,T),[],R1,R2,N2,N3,D),
  306     abdemo(Gs3,R2,R3,N3,N4,D).
  307
  308abdemo_cons_holds_at(neg(F),T3,Gs1,R1,R6,N1,N5,D) :-
  309     abresolve(terminates(A,F,T1),R1,Gs2,R1,B1),
  310     abresolve(happens(A,T1,T2),R1,[],R2,B2),
  311     check_depth(R2,D),
  312     abresolve(b(T2,T3),R2,[],R3,B3),
  313     append(Gs2,Gs1,Gs3), check_nafs(B2,N1,R3,R4,N1,N2,D),
  314     add_neg_car(declipped(T1,F,T3),N2,N3),
  315     abdemo_naf_cons(declipped(T1,F,T3),[],R4,R5,N3,N4,D),
  316     abdemo(Gs3,R5,R6,N4,N5,D).
  317
  318abdemo_cons_holds_at(F1,T,Gs1,R1,R3,N1,N2,D) :-
  319     G = holds_at(F1,T),
  320     abresolve(G,R1,Gs2,R2,B), append(Gs2,Gs1,Gs3),
  321     notrace((iv_list_to_set(Gs3,Gs4),(((Gs3\==Gs4)-> (!,fail) ; true)))),
  322     ignore(Gs3 = Gs4),
  323     abdemo(Gs4,R2,R3,N1,N2,D),
  324  writeNoln('terminate action:'),
  325  writeYesln(A),
  326  writeNoln('precondition:'),
  327  writeYesln(Gs2).
  328
  329
  330/*
  331   The next two clauses cater for happens goals.
  332
  333   Note that happens goals only appear either in the initial goal list or,
  334   in an "expand" goal, as a result of refinement. Note also that these
  335   clauses, because of the way abresolve(happens) works, will ensure sharing
  336   of sub-goals between compound events wherever possible.
  337*/
  338
  339abdemo_cons(happens(A,T1,T2),Gs,R1,R4,N1,N3,D) :- !,
  340     abresolve(happens(A,T1,T2),R1,[],R2,B), check_depth(R2,D),
  341     check_nafs(B,N1,R2,R3,N1,N2,D), abdemo(Gs,R3,R4,N2,N3,D).
  342
  343abdemo_cons(happens(A,T),Gs,R1,R4,N1,N3,D) :- !,
  344     abresolve(happens(A,T),R1,[],R2,B), check_depth(R2,D),
  345     check_nafs(B,N1,R2,R3,N1,N2,D), abdemo(Gs,R3,R4,N2,N3,D).
  346
  347/*
  348   The next clause deals with the expansion of compound actions. These appear
  349   as goals of the form expand([happens(A,T1,T2)|Bs]), where happens(A,T1,T2)
  350   is the compound action to be expanded and Bs is a list of "before" goals.
  351   These goals are placed in the goal list by calls to "refine". The various
  352   sub-goals generated by the expansion are treated in a careful order. First,
  353   the compound action's sub-actions are added to the residue. Then the "before"
  354   goals that "refine" took out of the residue are put back (with their newly
  355   skolemised time constants). The holds_at goals are solved next, on the
  356   assumption that they are either guards or supply context for the expansion.
  357   Then other, non event calculus goals are dealt with. Only then, with all the
  358   temporal ordering constraints sorted out, is it safe to tackle not(clipped)
  359   and not(declipped) goals, first those that are part of the compound action
  360   definition, then those recorded in the negations list.
  361*/
  362
  363abdemo_cons(expand([happens(A,T1,T2)|Bs]),Gs1,R1,R8,N1,N8,D) :- !,
  364     axiom(happens(A,T1,T2),Gs2),
  365     add_sub_actions(Gs2,R1,R2,N1,N2,D,Hs),
  366     solve_befores(Bs,R2,R3,N2,N3,D),
  367     abdemo_holds_ats(Gs2,R3,R4,N3,N4,D),
  368     solve_other_goals(Gs2,R4,R5,N4,N5,D),
  369     check_clipping(Gs2,R5,R6,N5,N6,D),
  370     check_sub_action_nafs(Hs,N1,R6,R7,N6,N7,D),
  371     abdemo(Gs1,R7,R8,N7,N8,D).
  372
  373
  374/*
  375   The next clauses cater for the general case (ie: goals other
  376   than holds_at and happens). They're also used to tackle domain
  377   constraints (ie: holds_at if holds_at clauses).
  378*/
  379
  380% INTERP-OR-AND    
  381
  382abdemo_cons((G1;G2),Gs,R1,R3,N1,N4,D) :- general_interp, !,
  383  (abdemo_cons(G1,Gs,R1,R3,N1,N4,D);
  384   abdemo_cons(G2,Gs,R1,R3,N1,N4,D)).
  385
  386abdemo_cons((G,G0),Gs,R1,R2,N1,N2,D):- !,
  387  abdemo_cons(G,[G0|Gs],R1,R2,N1,N2,D).
  388
  389abdemo_cons(not(G),Gs,R1,R3,N1,N4,D) :-
  390     % !, removed cut to allow negated axioms
  391     abdemo_naf_cons(G,[],R1,R2,N1,N2,D), add_neg_car(G,N2,N3),
  392     abdemo(Gs,R2,R3,N3,N4,D).
  393
  394abdemo_cons(G,Gs1,R1,R3,N1,N2,D) :-
  395     abresolve(G,R1,Gs2,R2,B), append(Gs2,Gs1,Gs3),
  396     notrace((iv_list_to_set(Gs3,Gs4),(((Gs3\==Gs4)-> (!,fail) ; true)))),
  397     ignore(Gs3 = Gs4),
  398     abdemo(Gs4,R2,R3,N1,N2,D).
  399check_depth(R,D):- check_depth(R,D,_L).
  400
  401check_depth(R,D,L) :- ec_trace(on,1), 
  402   action_count(R,L), 
  403   writeNoln('Actions:'),
  404   writeYesln(R),
  405   writeNoln('Action count:'), writeNoln(L), fail.
  406  
  407%Keep track of the current action depth
  408check_depth(R,D,L) :- action_count(R,L), L =< D, D =< 1000.
  409
  410% The action list is greater than the current Depth
  411check_depth(R,D,L) :- ec_trace(on, 1), writeNoln('Maximum bound reached'),!, fail.
  412
  413
  414
  415
  416
  417action_count([[HA,TC],RB],L) :- length(HA,L).
  418
  419
  420
  421
  422/* EXPANSION OF COMPOUND ACTIONS */
  423
  424
  425/* The following collection of predicates are called by abdemo(expand). */
  426
  427
  428abdemo_holds_ats([],R,R,N,N,D).
  429
  430abdemo_holds_ats([holds_at(F,T)|Gs],R1,R3,N1,N3,D) :-
  431     !, abdemo_cons_holds_at(F,T,[],R1,R2,N1,N2,D),
  432     abdemo_holds_ats(Gs,R2,R3,N2,N3,D).
  433
  434abdemo_holds_ats([G|Gs],R1,R2,N1,N2,D) :-
  435     abdemo_holds_ats(Gs,R1,R2,N1,N2,D).
  436
  437
  438non_regular_goal(G):- \+ regular_goal(G).
  439
  440regular_goal(holds_at(_F, _T)).
  441regular_goal(happens(_A, _T)).
  442regular_goal(happens(_A, _T1, _T2)).
  443regular_goal(b(_T1, _T2)).
  444regular_goal(not(Clip)):- nonvar(Clip), 
  445  (Clip = clipped(_T1,_F,_T2) ; Clip = declipped(_DT1,_FD,_DT2)).
  446
  447solve_other_goals([],R,R,N,N,D).
  448
  449solve_other_goals([G|Gs],R1,R3,N1,N3,D) :- 
  450     non_regular_goal(G), !,
  451     abdemo_cons(G,[],R1,R2,N1,N2,D),
  452     solve_other_goals(Gs,R2,R3,N2,N3,D).
  453
  454solve_other_goals([G|Gs],R1,R2,N1,N2,D) :-
  455     solve_other_goals(Gs,R1,R2,N1,N2,D).
  456
  457/*
  458   In its last argument, add_sub_actions accumulates a list of new actions
  459   added to the residue, so that subsequent re-checking of not(clipped) and
  460   not(declipped) goals can be done via check_nafs rather than the less
  461   efficient abdemo_nafs.
  462*/
  463
  464add_sub_actions([],R,R,N,N,D,[]).
  465add_sub_actions([G|Gs],R1,R2,N1,N2,D,L):-
  466  add_sub_actions_cons(G,Gs,R1,R2,N1,N2,D,L).
  467
  468add_sub_actions_cons(happens(A,T1,T2),Gs,R1,R3,N1,N3,D,Hs2) :-
  469     !, 
  470     abresolve(happens(A,T1,T2),R1,[],R2,B), check_depth(R2,D),
  471     add_sub_actions(Gs,R2,R3,N2,N3,D,Hs1), cond_add(B,happens(A,T1,T2),Hs1,Hs2).
  472
  473add_sub_actions_cons(happens(A,T),Gs,R1,R3,N1,N3,D,Hs2) :-
  474     !, abresolve(happens(A,T),R1,[],R2,B), check_depth(R2,D),
  475     add_sub_actions(Gs,R2,R3,N2,N3,D,Hs1), cond_add(B,happens(A,T,T),Hs1,Hs2).
  476
  477add_sub_actions_cons(b(T1,T2),Gs,R1,R3,N1,N3,D,Hs) :-
  478     !, abresolve(b(T1,T2),R1,[],R2,B),
  479     add_sub_actions(Gs,R2,R3,N2,N3,D,Hs).
  480
  481add_sub_actions_cons(G,Gs,R1,R2,N1,N2,D,Hs) :-
  482     add_sub_actions(Gs,R1,R2,N1,N2,D,Hs).
  483
  484
  485cond_add(false,H,Hs,Hs) :- !.
  486
  487cond_add(true,H,Hs,[H|Hs]).
  488
  489
  490solve_befores([],R,R,N,N,D).
  491
  492solve_befores([b(T1,T2)|Gs],R1,R3,N1,N3,D) :-
  493     !, abdemo_cons(b(T1,T2),[],R1,R2,N1,N2,D),
  494     solve_befores(Gs,R2,R3,N2,N3,D).
  495
  496solve_befores([G|Gs],R1,R2,N1,N2,D) :-
  497     solve_befores(Gs,R1,R2,N1,N2,D).
  498
  499
  500check_sub_action_nafs([],N1,R,R,N2,N2,D) :- !.
  501
  502check_sub_action_nafs([happens(A,T1,T2)|Hs],N1,R1,R3,N2,N4,D) :-
  503     check_nafs(A,T1,T2,N1,R1,R2,N2,N3,D),
  504     check_sub_action_nafs(Hs,N1,R2,R3,N3,N4,D).
  505
  506
  507check_clipping([],R,R,N,N,D) :- !.
  508
  509check_clipping([not(Clipped)|Gs],R1,R3,N1,N3,D) :- 
  510  % Dmiules asks:  Will we need copy_term ?
  511  (Clipped= clipped(T1,F,T2); Clipped=declipped(T1,F,T2)),
  512     !, abdemo_naf_cons(Clipped,[],R1,R2,N1,N2,D),
  513     check_clipping(Gs,R2,R3,N2,N3,D).
  514
  515check_clipping([G|Gs],R1,R2,N1,N2,D) :-
  516     check_clipping(Gs,R1,R2,N1,N2,D).
  517
  518
  519
  520
  521ammend_preconds4(A, T, Gs,Gss):- 
  522  findall(PrecondL, axiom_db(requires(A, T),PrecondL),PrecondLs), 
  523  append([Gs|PrecondLs],Gss).
  524
  525
  526/* ABRESOLVE */
  527
  528
  529/*
  530   The form of a call to abresolve is as follows.
  531
  532        abresolve(Goal,ResidueIn,Goals,ResidueOut,Flag)
  533
  534   where Goals is the body of clause resolved with, and Flag is set to true
  535   if a happens fact has been added to the residue.
  536*/
  537no_dbl_start(Gss):- \+ (member(b(start, Next),Gss), Next==start).
  538
  539abresolve(G,R1,Gs,R2,B):- notrace(var(G)),!,throw(var_abresolve(G,R1,Gs,R2,B)).
  540
  541abresolve(initially(A),R,Gss,R, False) :- !, abresolve(holds_at(A, start),R,Gss,R, False), 
  542  no_dbl_start(Gss).
  543
  544abresolve(terms_or_rels(A,F,T),R,Gss,R,false) :- axiom_db(releases(A,F,T),Gs), ammend_preconds4(A,T,Gs,Gss).
  545abresolve(terms_or_rels(A,F,T),R,Gss,R,false) :- !, axiom_db(terminates(A,F,T),Gs), ammend_preconds4(A,T,Gs,Gss).
  546
  547abresolve(inits_or_rels(A,F,T),R,Gss,R,false) :- axiom_db(releases(A,F,T),Gs), ammend_preconds4(A,T,Gs,Gss).
  548abresolve(inits_or_rels(A,F,T),R,Gss,R,false) :- !, axiom_db(initiates(A,F,T),Gs), ammend_preconds4(A,T,Gs,Gss).
  549
  550
  551/*
  552   happens goals get checked to see if they are already in the residue.
  553   This permits the re-use of actions already in the residue. However,
  554   this decision may lead to later failure, in which case we try adding
  555   a new action to the residue.
  556
  557   happens goals aren't resolved against object-level program clauses.
  558   Only goals that are marked as expand(goal) are resolved against
  559   program clauses, and this is done by abdemo.
  560
  561   Time variables get skolemised, but not action variables because
  562   they end up getting instantiated anyway.
  563*/
  564
  565abresolve(happens(A,T),R1,Gs,R2,B) :- !, abresolve(happens(A,T,T),R1,Gs,R2,B).
  566
  567abresolve(happens(A,T1,T2),[[HA,TC],RB],[],[[HA,TC],RB],false) :-
  568     member(happens(A,T1,T2),HA).
  569
  570abresolve(happens(A,T,T),[[HA,TC],RB],[],[[[happens(A,T,T)|HA],TC],RB],B) :-
  571     into_db(executable(A)), !, B = true, skolemise_time(T).
  572
  573abresolve(happens(A,T1,T2),R1,[],R2,B) :-  !, B = true, 
  574     skolemise_time(T1), skolemise_time(T2), add_happens(A,T1,T2,R1,R2).
  575
  576/*
  577   If either X or Y is not bound in a call to abresolve(b(X,Y)) then
  578   they get skolemised.
  579*/
  580abresolve(b(X,Y),R1,Nil,R2,B):- !, abresolve_b(b(X,Y),R1,Nil,R2,B).
  581
  582/*
  583   The predicates "diff" (meaning not equal) and "is" (for evaluating
  584   arithmetic expressions) are built in.
  585*/
  586
  587abresolve(diff(X,Y),R,[],R,false) :- !, X \= Y.
  588abresolve(ignore(_),R,[],R,false) :- !.
  589abresolve(allDifferent(_),R,[],R,false) :- !.
  590abresolve(is(X,Y),R,[],R,false) :- !, X is Y.
  591abresolve(equals(X,Y),R,[],R,false) :- !, X = Y.
  592abresolve(dif(X,Y),R,[],R,false) :- !, dif(X,Y).
  593abresolve(call(G),R,[],R,false) :- !, into_db(call(G)).
  594
  595% INTERP-OR-AND
  596abresolve((G1;G2),ResidueIn,Goals,ResidueOut,Flag):- !,
  597  (abresolve(G1,ResidueIn,Goals,ResidueOut,Flag);
  598   abresolve(G2,ResidueIn,Goals,ResidueOut,Flag)).
  599
  600abresolve((G1,G2),ResidueIn,Goals,ResidueOut,Flag):- !,
  601  (abresolve(G1,ResidueIn,Goals1,ResidueMid,Flag),
  602   abresolve(G2,ResidueMid,Goals2,ResidueOut,Flag)),
  603   append(Goals1,Goals2,Goals).
  604
  605
  606
  607abresolve(G,R,[],[G|R],false) :- quietly(into_db(abducible(G))).
  608
  609abresolve(G,R,Gs,R,false) :- axiom_db(G,Gs),re_constrain(G,Gs,Gss).
  610
  611% re_constrain(B,B):- B= b(T1,T2),!, dif(T1,T2).
  612re_constrain(B,B).
  613
  614re_constrain(G,[B|Bs],[BB|BBs]):- re_constrain(G,Bs,BBs), re_constrain(B,BB).
  615re_constrain(_,Bs,Bs):-!.
  616 
  617/*ABDEMO_NAFS and CHECK_NAFS */
  618
  619
  620/*
  621   abdemo_nafs([G1...Gn],R1,R2) demos not(G1) and ... and not(Gn).
  622
  623   Calls to abdemo_naf have the following form.
  624
  625        abdemo_nafs(Negations,ResidueIn,ResidueOut,
  626             NegationsIn,NegationsOut,DepthIn,DepthOut)
  627
  628   where Negations is the list of negations to be established, ResidueIn
  629   is the old residue, ResidueOut is the new residue (abdemo_nafs can add
  630   both before/"b" and happens facts, as well as other abducibles, to the
  631   residue), NegationsIn is the old list of negations (same as Negations
  632   for top-level call), and NegationsOut is the new list of negations
  633   (abdemo_nafs can add new clipped goals to NegationsIn).
  634
  635   DepthIn and DepthOut keep track of the number of sub-goals generated,
  636   for iterative deepening purposes.
  637*/
  638
  639
  640abdemo_nafs([],R,R,N,N,D).
  641
  642abdemo_nafs([N|Ns],R1,R3,N1,N3,D) :-
  643     abdemo_naf(N,R1,R2,N1,N2,D), abdemo_nafs(Ns,R2,R3,N2,N3,D).
  644
  645
  646/*
  647   abdemo_naf( [G1...Gn],R1,R2) demos not((G1) and ... and (Gn)).
  648
  649   As for abdemo, the main event calculus axioms are compiled into the
  650   meta-level in abdemo_naf. In addition to the two holds_at axioms, we
  651   have,
  652
  653        clipped(T1,F,T3) <-
  654             happens(A,T2) and T1 < T2 < T3 and
  655             [terminates(A,F,T2) or releases(A,F,T2)]
  656
  657        declipped(T1,F,T3) <-
  658             happens(A,T2) and T1 < T2 < T3 and
  659             [initiates(A,F,T2) or releases(A,F,T2)]
  660
  661   We have to use findall here, because all ways of achieving a goal
  662   have to fail for the goal itself to fail.
  663
  664   Note that only the two-argument version of happens is used, because
  665   the residue only contains instantaneous actions, and the effects of
  666   compound actions are assumed to match the effects of their
  667   component actions.
  668*/
  669
  670abdemo_naf( [G|Gs1 ],R1,R2,N1,N2,D) :-
  671  abdemo_naf_cons(G,Gs1,R1,R2,N1,N2,D).
  672
  673:- discontiguous abdemo_naf_cons/7.  674
  675abdemo_naf_cons(H,Gs, R1,R4,N1,N3,D):- maybe_note_ab(abdemo_naf_cons, H,Gs,R1,R4,N1,N3,D),fail.
  676
  677abdemo_naf_cons(clipped(T1,F,T4),Gs1,R1,R2,N1,N2,D) :-
  678     !, findall(Gs3,
  679          (abresolve(terms_or_rels(A,F,T2),R1,Gs2,R1,false),
  680           abresolve(happens(A,T2,T3),R1,[],R1,false),
  681          append([b(T1,T3),b(T2,T4)|Gs2],Gs1,Gs3)),Gss),
  682     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  683
  684abdemo_naf_cons(declipped(T1,F,T4),Gs1,R1,R2,N1,N2,D) :-
  685     !, findall(Gs3,
  686          (abresolve(inits_or_rels(A,F,T2),R1,Gs2,R1,false),
  687          abresolve(happens(A,T2,T3),R1,[],R1,false),
  688          append([b(T1,T3),b(T2,T4)|Gs2],Gs1,Gs3)),Gss),
  689     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  690
  691/*
  692   To show the classical negation of holds_at(F) (which is what we want), we
  693   have to show that holds_at(neg(F)). Conversely, to show the classical
  694   negation of holds_at(neg(F)) we have to show holds_at(F). Within a call
  695   to abdemo_naf, we can add both happens and before (and other abducibles)
  696   to the residue. This removes a potential source of incompleteness.
  697
  698   Note that F must be a ground term to preserve soundness and completeness.
  699   To guarantee this, all variables that occur in the body of an
  700   initiates, terminates or releases clause must occur in the fluent
  701   argument in its head.
  702*/
  703
  704abdemo_naf_cons(holds_at(F1,T),Gs1,R1,R3,N1,N3,D):- !,
  705  abdemo_naf_cons_holds_at(F1,T,Gs1,R1,R3,N1,N3,D).
  706
  707/* DANGER: Cut in next clause rules out other ways to solve holds_at(F2,T). */
  708/*
  709abdemo_naf_cons_holds_at(F1,T,Gs1,R1,R3,N1,N3,D) :-
  710     opposite(F1,F2), 
  711     abdemo_ cons_holds_at(F2,T,[],R1,R2,N1,N2,D), !,
  712     copy_ term(Gs1,Gs2), abdemo_naf_cont(R1,Gs2,R2,R3,N1,N3,D).
  713
  714abdemo_naf_cons_holds_at(_F,_T,Gs,R1,R3,N1,N3,D) :-
  715      abdemo_naf(Gs,R1,R3,N1,N3,D).
  716*/
  717abdemo_naf_cons_holds_at(F1,T,Gs1,R1,R3,N1,N3,D) :-
  718     opposite(F1,F2), 
  719     (abdemo_cons_holds_at(F2,T,[],R1,R2,N1,N2,D), !,
  720      (copy_term(Gs1,Gs2), abdemo_naf_cont(R1,Gs2,R2,R3,N1,N3,D))).
  721
  722abdemo_naf_cons_holds_at(_F,_T,Gs,R1,R3,N1,N3,D) :-
  723      abdemo_naf(Gs,R1,R3,N1,N3,D).
  724
  725/*
  726   Special facilities for handling temporal ordering facts are built in.
  727   We can add a before "b" fact to the residue to preserve the failure of
  728   a clipped goal. The failure of a before "b" goal does NOT mean that the
  729   negation of that goal is assumed to be true. (The Clark completion is
  730   not applicable to temporal ordering facts.) Rather, to make b(X,Y)
  731   fail, b(Y,X) has to follow. One way to achieve this is to add
  732   b(Y,X) to the residue.
  733*/
  734
  735abdemo_naf_cons(b(X,Y),Gs,R,R,N,N,D) :- X == Y, !.
  736
  737abdemo_naf_cons(b(X,Y),Gs,R,R,N,N,D) :- demo_before(Y,X,R), !.
  738
  739abdemo_naf_cons(b(X,Y),Gs1,R1,R2,N1,N2,D) :-
  740     !, append(Gs1,[postponed(b(X,Y))],Gs2),
  741     abdemo_naf(Gs2,R1,R2,N1,N2,D).
  742
  743/*
  744   A before "b" fact is only added to the residue as a last resort. Accordingly,
  745   if we encounter a b(X,Y) goal and cannot show b(Y,X), we
  746   postpone that goal until we've tried other possibilities. A postponed
  747   before "b" goal appears in the goal list as postponed(b(X,Y)).
  748*/
  749
  750abdemo_naf_cons(postponed(b(X,Y)),Gs,R1,R2,N,N,D) :-
  751     \+ demo_beq(X,Y,R1), add_before(Y,X,R1,R2).
  752
  753abdemo_naf_cons(postponed(b(X,Y)),Gs,R1,R2,N1,N2,D) :-
  754     !, abdemo_naf(Gs,R1,R2,N1,N2,D).
  755
  756/* 
  757   We drop through to the general case for goals other than special event
  758   calculus goals.
  759*/
  760% INTERP-OR-AND
  761abdemo_naf_cons((G,G0),Gs,R1,R2,N1,N2,D):- !,
  762  abdemo_naf_cons(G,[G0|Gs],R1,R2,N1,N2,D).
  763% INTERP-OR-AND 
  764abdemo_naf_cons((G1;G2),Gs,R1,R3,N1,N4,D) :- !,
  765  (abdemo_naf_cons(G1,Gs,R1,R3,N1,N4,D);
  766   abdemo_naf_cons(G2,Gs,R1,R3,N1,N4,D)).
  767
  768:-  discontiguous(abdemo_naf_cons/7).  769
  770
  771/* DANGER: Cut in next clause rules out other ways to solve G. */
  772/*
  773abdemo_naf_cons_not(G,Gs1,R1,R3,N1,N3,D) :-  
  774     abdemo_cons(G,[],R1,R2,N1,N2,D), !, 
  775     copy_term(Gs1,Gs2), abdemo_naf_cont(R1,Gs2,R2,R3,N1,N3,D).
  776abdemo_naf_cons_not(_G,Gs,R1,R3,N1,N3,D) :- 
  777     abdemo_naf(Gs,R1,R3,N1,N3,D).
  778*/
  779abdemo_naf_cons_not(G,Gs1,R1,R3,N1,N3,D) :-  
  780     abdemo_cons(G,[],R1,R2,N1,N2,D) *-> 
  781       (copy_term(Gs1,Gs2), abdemo_naf_cont(R1,Gs2,R2,R3,N1,N3,D)) ;
  782     abdemo_naf(Gs,R1,R3,N1,N3,D).
  783
  784
  785abdemo_naf_cons(not(G),Gs1,R1,R3,N1,N3,D):- 
  786    % !, removed cut to allow negated axioms
  787    abdemo_naf_cons_not(G,Gs1,R1,R3,N1,N3,D),
  788    !. % added cut
  789
  790abdemo_naf_cons(G,Gs1,R,R,N,N,D) :- \+ abresolve(G,R,Gs2,R,false), !.
  791
  792abdemo_naf_cons(G1,Gs1,R1,R2,N1,N2,D) :-
  793     findall(Gs2, 
  794            (abresolve(G1,R1,Gs3,R1,false), append(Gs3,Gs1,Gs2)),
  795             Gss),
  796     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  797
  798
  799/*
  800   abdemo_naf_cont gets an extra opportunity to succeed if the residue
  801   has been altered. This is determined by comparing R1 with R2. If
  802   a sub-goal has failed and the residue hasn't been altered, there's
  803   no need to look for other ways to prove the negation of the overall goal.
  804*/
  805
  806abdemo_naf_cont(R1,_Gs,R2,R2,N,N,D).
  807
  808abdemo_naf_cont(R1,Gs,R2,R3,N1,N2,D) :-
  809     R1 \= R2, abdemo_naf(Gs,R1,R3,N1,N2,D).
  810
  811
  812/*
  813   check_nafs is just like abdemo_nafs, except that it only checks
  814   negated clipped and declipped facts against the most recent event
  815   added to the residue. To check one of these negations, not only can
  816   we confine our attention to the most recent event, but we can ignore
  817   that event if it doesn't fall inside the interval covered by the
  818   clipped/declipped in question. Of course, the negated clipped/declipped
  819   fact might depend on other holds_at facts. But their preservation is
  820   ensured because the clipped/declipped negation they themselves depend
  821   on will also be checked.
  822*/
  823
  824
  825check_nafs(false,N1,R,R,N2,N2,D) :- !.
  826
  827check_nafs(true,N,[[[happens(A,T1,T2)|HA],TC],RB],R,N1,N2,D) :-
  828     check_nafs(A,T1,T2,N,[[[happens(A,T1,T2)|HA],TC],RB],R,N1,N2,D).
  829
  830check_nafs(A,T1,T2,[],R,R,N,N,D).
  831
  832check_nafs(A,T1,T2,[N|Ns],R1,R3,N1,N3,D) :-
  833     check_naf(A,T1,T2,N,R1,R2,N1,N2,D),
  834     check_nafs(A,T1,T2,Ns,R2,R3,N2,N3,D).
  835
  836
  837check_naf(A,T2,T3,[clipped(T1,F,T4)],R1,R2,N1,N2,D) :-
  838     !, findall([b(T1,T3),b(T2,T4)|Gs],
  839          (abresolve(terms_or_rels(A,F,T2),R1,Gs,R1,false)),Gss),
  840     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  841
  842check_naf(A,T2,T3,[declipped(T1,F,T4)],R1,R2,N1,N2,D) :-
  843     !, findall([b(T1,T3),b(T2,T4)|Gs],
  844          (abresolve(inits_or_rels(A,F,T2),R1,Gs,R1,false)),Gss),
  845     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  846
  847check_naf(A,T1,T2,N,R1,R2,N1,N2,D) :- abdemo_naf(N,R1,R2,N1,N2,D).
  848
  849
  850
  851
  852/* DEMO_BEFORE, ADD_BEFORE and ADD_HAPPENS */
  853
  854
  855/*
  856   demo_before simply checks membership of the transitive closure half of
  857   the temporal ordering part of the residue. Likewise demo_beq checks for
  858   demo_before or for membership of the transitive closure half of the
  859   happens part of the residue.
  860*/
  861
  862demo_before(0,Y,R) :- !, Y \= 0.
  863
  864demo_before(X,Y,[RH,[BA,TC]]) :- member(b(X,Y),TC).
  865
  866/* demo_beq is demo before or equal. */
  867
  868demo_beq(X,Y,R) :- X == Y, !.
  869
  870demo_beq(X,Y,R) :- demo_before(X,Y,R), !.
  871
  872demo_beq(X,Y,[[HA,TC],RB]) :- member(beq(X,Y),TC).
  873
  874
  875/*
  876   add_before(X,Y,R1,R2) adds b(X,Y) to the residue R1 giving R2.
  877   It does this by maintaining the transitive closure of the "b" and "beq"
  878   relations in R2, and assumes that R1 is already transitively closed.
  879   R1 and R2 are just the temporal ordering parts of the residue.
  880*/
  881
  882add_before(X,Y,[RH,[BA,TC]],[RH,[BA,TC]]) :- member(b(X,Y),TC), !.
  883
  884add_before(X,Y,[[HA,HC],[BA,BC1]],[[HA,HC],[[b(X,Y)|BA],BC2]]) :-
  885     \+ demo_beq(Y,X,[[HA,HC],[BA,BC1]]), find_bef_connections(X,Y,BC1,C1,C2),
  886     find_beq_connections(X,Y,HC,C3,C4), delete_abdemo(X,C3,C5), delete_abdemo(Y,C4,C6),
  887     append(C5,C1,C7), append(C6,C2,C8),
  888     cross_prod_bef(C7,C8,C9,BC1), append(C9,BC1,BC2).
  889
  890/*
  891   add_happens(A,T1,T2,R1,R2) adds happens(A,T1,T2) to the residue R1
  892   giving R2. Because happens(A,T1,T2) -> T1 <= T2, this necessitates
  893   updating the transitive closures of the before "b" and "beq" facts in the residue.
  894   Duplicates aren't checked for, as it's assumed this is done by the
  895   calling predicate.
  896*/
  897
  898add_happens(A,T1,T2,[[HA,HC1],[BA,BC1]],[[[happens(A,T1,T2)|HA],HC2],[BA,BC2]]) :-
  899     \+ demo_before(T2,T1,[[HA,HC1],[BA,BC1]]),
  900     find_beq_connections(T1,T2,HC1,C1,C2), cross_prod_beq(C1,C2,C3,HC1),
  901     append(C3,HC1,HC2), find_bef_connections(T1,T2,BC1,C4,C5),
  902     cross_prod_bef(C4,C5,C6,BC1), delete_abdemo(b(T1,T2),C6,C7),
  903     append(C7,BC1,BC2).
  904
  905/*
  906   find_bef_connections(X,Y,TC,C1,C2) creates two lists, C1 and C2,
  907   containing respectively all the time points before X and after
  908   Y according to TC, which is assumed to be transitively closed.
  909*/
  910
  911find_bef_connections(X,Y,[],[X],[Y]).
  912
  913find_bef_connections(X,Y,[b(Z,X)|R],[Z|C1],C2) :-
  914     !, find_bef_connections(X,Y,R,C1,C2).
  915
  916find_bef_connections(X,Y,[b(Y,Z)|R],C1,[Z|C2]) :-
  917     !, find_bef_connections(X,Y,R,C1,C2).
  918
  919find_bef_connections(X,Y,[b(Z1,Z2)|R],C1,C2) :-
  920     find_bef_connections(X,Y,R,C1,C2).
  921
  922/*
  923   find_beq_connections is like find_bef_connections, except that it works
  924   on the transtive closure of happens part of the residue.
  925*/
  926
  927find_beq_connections(X,Y,[],[X],[Y]).
  928
  929find_beq_connections(X,Y,[beq(Z,X)|R],[Z|C1],C2) :-
  930     !, find_beq_connections(X,Y,R,C1,C2).
  931
  932find_beq_connections(X,Y,[beq(Y,Z)|R],C1,[Z|C2]) :-
  933     !, find_beq_connections(X,Y,R,C1,C2).
  934
  935find_beq_connections(X,Y,[beq(Z1,Z2)|R],C1,C2) :-
  936     find_beq_connections(X,Y,R,C1,C2).
  937
  938
  939cross_prod_bef([],C,[],R).
  940
  941cross_prod_bef([X|C1],C2,R3,R) :-
  942     cross_one_bef(X,C2,R1,R), cross_prod_bef(C1,C2,R2,R), append(R1,R2,R3).
  943
  944cross_one_bef(X,[],[],R).
  945
  946cross_one_bef(X,[Y|C],[b(X,Y)|R1],R) :-
  947     \+ member(b(X,Y),R), !, cross_one_bef(X,C,R1,R).
  948
  949cross_one_bef(X,[Y|C],R1,R) :- cross_one_bef(X,C,R1,R).
  950
  951
  952cross_prod_beq([],C,[],R).
  953
  954cross_prod_beq([X|C1],C2,R3,R) :-
  955     cross_one_beq(X,C2,R1,R), cross_prod_beq(C1,C2,R2,R), append(R1,R2,R3).
  956
  957cross_one_beq(X,[],[],R).
  958
  959cross_one_beq(X,[Y|C],[beq(X,Y)|R1],R) :-
  960     \+ member(beq(X,Y),R), !, cross_one_beq(X,C,R1,R).
  961
  962cross_one_beq(X,[Y|C],R1,R) :- cross_one_beq(X,C,R1,R).
  963
  964
  965
  966
  967/* REFINE */
  968
  969
  970/*
  971   refine(R1,N1,Gs,R2,N2) takes the earliest compound action out of the residue
  972   R1 and puts it in the goal list Gs, along with all "before/b", not(clipped) and
  973   not(declipped) facts that refer to the same time points. These time points
  974   are unskolemised, so that they can be bound to existing time points in the
  975   residue, thus permitting sub-actions to be shared between abstract actions.
  976   This almost restores the state of computation to the state S before the chosen
  977   action was added to the residue in the first place. But not quite, because
  978   some derived before facts will be retained in the transitive closure part
  979   of the before part of the residue that weren't there in state S. This doesn't
  980   matter, however, because these derived facts will need to be there eventually
  981   anyway, when those before  facts that have been transferred from residue to goal
  982   list get put back in the residue.
  983
  984   The compound action extracted from the residue is marked for expansion by
  985   inserting it in the goal list in the form expand([happens(A,T1,T2)|Bs]),
  986   where Bs is the list of "before/b" facts taken out of the residue, as
  987   described above. When abdemo comes across a goal of this form, it will
  988   resolve the "happens" part against program clauses. The reason for
  989   not doing this resolution here is that we want to backtrack to alternative
  990   definitions of a compound goal inside the iterative deepening search, not
  991   outside it. This ensures the desired behaviour for compound actions which
  992   expand to one series of sub-actions given certain conditions but to another
  993   series of sub-actions given other conditions. Otherwise the check for these
  994   conditions, which will be a holds_at goal in the compound action definition,
  995   is in danger of being treated as a goal to be established instead of just
  996   checked.
  997*/
  998
  999refine([[HA1,HC1],[BA1,BC1]],N1,Gs,[[HA2,HC2],[BA2,BC2]],N3) :-
 1000     split_happens(HA1,[BA1,BC1],happens(A,T1,T2),HA2),
 1001     split_beqs(HC1,T1,T2,T3,T4,HC3,HC2),
 1002     split_befores(BA1,T1,T2,T3,T4,BA3,BA2),
 1003     split_befores(BC1,T1,T2,T3,T4,BC3,BC2),
 1004     split_nafs(N1,T1,T2,T3,T4,N2,N3),
 1005     append([expand([happens(A,T3,T4)|BA3])],N2,Gs).
 1006
 1007
 1008/*
 1009   split_happens(RH1,RB,H,RH2) holds if H is the earliest non-executable
 1010   (abstract) action in RH1 according to RB. The remainder of RH1 ends up in
 1011   RH2. If there are no non-executable actions, H is the earliest action.
 1012*/
 1013
 1014split_happens([happens(A,T1,T2)],RB,happens(A,T1,T2),[]) :- !.
 1015
 1016split_happens([happens(A1,T1,T2)|RH1],RB,happens(A3,T5,T6),
 1017          [happens(A4,T7,T8)|RH2]) :-
 1018     split_happens(RH1,RB,happens(A2,T3,T4),RH2),
 1019     order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
 1020          happens(A3,T5,T6),happens(A4,T7,T8)).
 1021
 1022
 1023order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
 1024          happens(A1,T1,T2),happens(A2,T3,T4)) :-
 1025     \+ executable(A1), executable(A2), !.
 1026
 1027order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
 1028          happens(A2,T3,T4),happens(A1,T1,T2)) :-
 1029     \+ executable(A2), executable(A1), !.
 1030
 1031order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
 1032          happens(A1,T1,T2),happens(A2,T3,T4)) :-
 1033     demo_before(T1,T3,[[],RB]), !.
 1034
 1035order(happens(A1,T1,T2),happens(A2,T3,T4),RB,happens(A2,T3,T4),happens(A1,T1,T2)).
 1036
 1037
 1038split_befores([],T1,T2,T3,T4,[],[]).
 1039
 1040split_befores([b(T1,T2)|Bs1],T3,T4,T5,T6,Bs2,[b(T1,T2)|Bs3]) :-
 1041     no_match(T1,T2,T3,T4), !, split_befores(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1042                                        
 1043split_befores([b(T1,T2)|Bs1],T3,T4,T5,T6,[b(T7,T8)|Bs2],Bs3) :-
 1044     substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
 1045     split_befores(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1046
 1047
 1048split_beqs([],T1,T2,T3,T4,[],[]).
 1049
 1050split_beqs([beq(T1,T2)|Bs1],T3,T4,T5,T6,Bs2,[beq(T1,T2)|Bs3]) :-
 1051     no_match(T1,T2,T3,T4), !, split_beqs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1052
 1053split_beqs([beq(T1,T2)|Bs1],T3,T4,T5,T6,[beq(T7,T8)|Bs2],Bs3) :-
 1054     substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
 1055     split_beqs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1056
 1057
 1058split_nafs([],T1,T2,T3,T4,[],[]).
 1059
 1060split_nafs([[  clipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,Bs2,[[clipped(T1,F,T2)]|Bs3]) :-
 1061     no_match(T1,T2,T3,T4), !, split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1062
 1063split_nafs([[  clipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,
 1064          [not(clipped(T7,F,T8))|Bs2],Bs3) :-
 1065     !, substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
 1066     split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1067
 1068split_nafs([[declipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,Bs2,
 1069          [[declipped(T1,F,T2)]|Bs3]) :-
 1070     no_match(T1,T2,T3,T4), !, split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1071
 1072split_nafs([[declipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,
 1073          [not(declipped(T7,F,T8))|Bs2],Bs3) :-
 1074     !, substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
 1075     split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1076
 1077split_nafs([N|Bs1],T3,T4,T5,T6,Bs2,[N|Bs3]) :-
 1078     substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
 1079     split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
 1080
 1081
 1082substitute_time(T1,T1,T2,T3,T4,T3) :- !.
 1083substitute_time(T2,T1,T2,T3,T4,T4) :- !.
 1084substitute_time(T1,T2,T3,T4,T5,T1).
 1085
 1086no_match(T1,T2,T3,T4) :- T1 \= T3, T2 \= T3, T1 \= T4, T2 \= T4.
 1087
 1088
 1089
 1090
 1091/* OTHER BITS AND PIECES */
 1092
 1093
 1094/*
 1095   add_neg(N,Ns1,Ns2) adds goal N to the list of (lists of) negations Ns1,
 1096   giving Ns2. Duplicates are ignored, but N must be fully bound.
 1097*/
 1098
 1099add_neg_car(N,Ns,Ns2):- add_neg([N],Ns,Ns2).
 1100
 1101add_neg(N,Ns,Ns) :- member(N,Ns), !.
 1102add_neg(N,Ns,[N|Ns]).
 1103
 1104
 1105/* append_negs is just append, but ignoring duplicates. */
 1106
 1107append_negs([],[],[]).
 1108
 1109append_negs([N|Ns1],Ns2,Ns4) :- add_neg(N,Ns2,Ns3), append(Ns1,Ns3,Ns4).
 1110
 1111
 1112delete_abdemo(X,[],[]).
 1113delete_abdemo(X,[X|L],L) :- !.
 1114delete_abdemo(X,[Y|L1],[Y|L2]) :- delete_abdemo(X,L1,L2).
 1115
 1116
 1117
 1118
 1119
 1120/* Skolemisation */
 1121
 1122skolemise_time(T) :- notrace((ignore((var(T), gensym(t,T))))).
 1123
 1124
 1125opposite(neg(F),F) :- !.
 1126opposite(F,neg(F)).
 1127
 1128
 1129%trace(off).
 1130
 1131
 1132%:- endif.
 1133%axiom_db(equals(X,Y),[call(X=Y)]).
 1134axiom_db(H,B):- quietly(into_db(axiom(H,B))),no_dbl_start(B).
 1135into_db(G):- call(G).
 1136
 1137
 1138
 1139:- fixup_exports.