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