18:-ensure_loaded('iwfms/genSymPatches.pl'). 19
21:-ensure_loaded('iwfms/sortPlans.pl'). 22
24:-ensure_loaded('iwfms/temporalOrderCleaner.pl'). 25
27:-ensure_loaded('iwfms/mappingTotalOrderPlan.pl'). 28
30:-ensure_loaded('iwfms/loopReduction.pl'). 31
32
35
36
38
40
41:- prolog_flag(compiling,_,profiledcode). 42
44:- prolog_flag(toplevel_print_options,_,[quoted(true),numbervars(true),portrayed(true)]).
45
47:- multifile valid_html_form/2. 48
49
82
83
131
134
135
152
153
154
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 176 abdemo_cont(R2,R3,N2,N3,MaxDepth,HighLevel).
177
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 190 191 192 193 !,
194 action_count([[HA,HC],[BA,BC]],D),
195 abdemo_top(Gs,R1,R2,N2,N3,D,MaxDepth, HighLevel)
196
197 198 .
199
200
202
206
207abdemo_id(Gs,R1,R2,N1,N2,D, MaxDepth) :-
208 D >= MaxDepth, writeNoln('No solution found within bound '), writeNoln(MaxDepth), fail. 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
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
234
235
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
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
290should_swap_goals(diff(_,_),_,NotDif,_):- NotDif \= diff(_,_).
291should_swap_goals(_R1,[_|Vs1],_R2,[]).
292
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 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
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
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
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 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
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
416
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
440
441
442
443
444
445action_count([[HA,TC],RB],L) :- length(HA,L).
446
447
448
449
451
452
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 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
493
495
496
497
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),!. 539
540solve_befores([G|Gs],R1,R2,N1,N2,D) :-
541 solve_befores(Gs,R1,R2,N1,N2,D),!. 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
568
569
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
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
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 607 608 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
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
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
645
646abresolve(prolog(Code),R,[],R,false) :- !, Code.
647abresolve(call(Code),R,[],R,false) :- !, Code.
648
663
664:- discontiguous ec:abresolve/5.
665
666breakupResidual( [[X,Y],[Z,A]] , X).
667
668
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
698
699
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
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
780
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
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
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
826
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
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
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
896
897
904
905demo_before(0,Y,R) :- !, Y \= 0.
906
907demo_before(X,Y,[RH,[BA,TC]]) :- member(b(X,Y),TC).
908
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
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
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
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
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
1011
1012
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
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
1135
1136
1141
1142add_neg(N,Ns,Ns) :- member(N,Ns), !.
1143add_neg(N,Ns,[N|Ns]).
1144
1145
1147
1148append_negs([],[],[]).
1149append_negs([N|Ns1],Ns2,Ns4) :- add_neg(N,Ns2,Ns3), append(Ns1,Ns3,Ns4).
1150
1151
1153delete_abdemo(X,[],[]).
1154delete_abdemo(X,[X|L],L) :- !.
1155delete_abdemo(X,[Y|L1],[Y|L2]) :- delete_abdemo(X,L1,L2).
1156
1157
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
1169
1170skolemise_time(T) :- notrace((ignore((var(T), gensym(t,T))))).
1171
1172
1173opposite(neg(F),F) :- !.
1174opposite(F,neg(F))