Prolog ASLDICN Event Calculus Planner

23 Nov

The event calculus planner used within my thesis was based on Dr. Murray Shanahan’s ASLDICN (Abductive SLD with Integrity constraints and proof by Negation) planner with compound action support. This planner is an adaptation from one published in one of Dr. Shanahan’s research papers

http://casbah.ee.ic.ac.uk/%7Empsha/planners.html

The original planner only supports the generation of a single plan. I needed to support conditional planning. I wanted the planner to generate multiple plans representing the different ways of reaching the goal. The problem was how to convert the planner to generate all possible plans. Importantly ensuring that this does not cause infinite looping and no redundant plan solutions are generated.

My version of the planner add the following features:

  • Conditional Planning
  • Impossible Predicate
  • Occured And NotOccured predicates

Prolog Event Calculus Planner

Download eventCalculusPlanner.pl

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