2:-ensure_loaded('genSymPatches.pl'). 3
5:-ensure_loaded('sortPlans.pl'). 6
8:-ensure_loaded('temporalOrderCleaner.pl'). 9
11:-ensure_loaded('mappingTotalOrderPlan.pl'). 12
14:-ensure_loaded('loopReduction.pl'). 15
16
18:-ensure_loaded('../htmlTyping/typing.pl'). 19
20
21:- include('../knowledgeBaseCGI.pl'). 22
23
24:-prolog_flag(compiling,_,profiledcode). 25
27:- prolog_flag(toplevel_print_options,_,[quoted(true),numbervars(true),portrayed(true)]).
28
30:- multifile valid_html_form/2. 31
32
65
66
114
115
116
117
119
120
137
138
139
141
142plan(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
153abdemo(Gs,[HA,BA], MaxDepth, HighLevel) :-
154 init_gensym(t),
155 abdemo_top(Gs,[[[],[]],[[],[]]],[[HA,HC],[BA,BC]],[],N,0, MaxDepth, HighLevel).
156
157
158abdemo_top(Gs,R1,R3,N1,N3,D, MaxDepth, HighLevel) :-
159
160 abdemo_id(Gs,R1,R2,N1,N2,D, MaxDepth),
161
162 163
164 abdemo_cont(R2,R3,N2,N3,MaxDepth,HighLevel).
165
171
172abdemo_cont([[HA,TC],RB],[[HA,TC],RB],N,N,MaxDepth,HighLevel) :- all_executable(HA, HighLevel), !.
173
174abdemo_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 180 181 182 183 !,
184
185 action_count([[HA,HC],[BA,BC]],D),
186
187 abdemo_top(Gs,R1,R2,N2,N3,D,MaxDepth, HighLevel)
188
189 190 .
191
192
194
198
199abdemo_id(Gs,R1,R2,N1,N2,D, MaxDepth) :-
200 D >= MaxDepth, writeNoln('No solution found within bound '), writeNoln(MaxDepth), fail. 201
202abdemo_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
216
217
218all_executable([], HighLevel).
219
220all_executable([happens(A,T1,T2)|R] ,HighLevel) :- (HighLevel =:= 0 ->
221 true
222 ;
223 executable(A), all_executable(R, HighLevel)
224 ).
225
226
227
229
230
239
240abdemo(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
247abdemo([],R,R,N,N,D).
248
264
265abdemo([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
279
280abdemo([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 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
311
312abdemo([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
320abdemo([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
346
347abdemo([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
352abdemo([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
372
373abdemo([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 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
399
400abdemo([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
405abdemo([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 410
411
413abdemo([G|Gs],R1,R3,N1,N4,D ) :- writeNoln( 'currently unknown information about(may be compound!):'), writeNoln(G),
414fail.
415
416
433
434
435action_count([[HA,TC],RB],L) :- length(HA,L).
436
437
438
439
441
442
444
445
446abdemo_holds_ats([],R,R,N,N,D).
447
448abdemo_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 453 !,
454
455
456 abdemo_holds_ats(Gs,R2,R3,N2,N3,D).
457
458abdemo_holds_ats([G|Gs],R1,R2,N1,N2,D) :-
459 abdemo_holds_ats(Gs,R1,R2,N1,N2,D).
460
461
462solve_other_goals([],R,R,N,N,D).
463
464solve_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
471solve_other_goals([G|Gs],R1,R2,N1,N2,D) :-
472 solve_other_goals(Gs,R1,R2,N1,N2,D).
473
474
475
478
479solve_other_goals([G|Gs],R1,R2,N1,N2,D) :- fail.
480
481
482
489
490add_sub_actions([],R,R,N,N,D,[]).
491
492add_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
499add_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
506add_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
510add_sub_actions([G|Gs],R1,R2,N1,N2,D,Hs) :-
511 add_sub_actions(Gs,R1,R2,N1,N2,D,Hs).
512
513
514cond_add(false,H,Hs,Hs) :- !.
515
516cond_add(true,H,Hs,[H|Hs]).
517
518
519solve_befores([],R,R,N,N,D).
520
521
522
523solve_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),!. 526
527solve_befores([G|Gs],R1,R2,N1,N2,D) :-
528 solve_befores(Gs,R1,R2,N1,N2,D),!. 529
530
531check_sub_action_nafs([],N1,R,R,N2,N2,D) :- !.
532
533check_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
538check_clipping([],R,R,N,N,D) :- !.
539
540check_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
544check_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
548check_clipping([G|Gs],R1,R2,N1,N2,D) :-
549 check_clipping(Gs,R1,R2,N1,N2,D).
550
551
552
553
555
556
565
566abresolve(terms_or_rels_or_imposs(A,F,T),R,Gs,R,false) :- axiom(releases(A,F,T),Gs).
567abresolve(terms_or_rels_or_imposs(A,F,T),R,Gs,R,false) :- axiom(terminates(A,F,T),Gs).
568
570abresolve(terms_or_rels_or_imposs(A,F,T),R,Gs,R,false) :- !, axiom(impossible(A,T),Gs).
571
572abresolve(inits_or_rels(A,F,T),R,Gs,R,false) :- axiom(releases(A,F,T),Gs).
573abresolve(inits_or_rels(A,F,T),R,Gs,R,false) :- !, axiom(initiates(A,F,T),Gs).
574
588
589abresolve(happens(A,T),R1,Gs,R2,B) :- !, abresolve(happens(A,T,T),R1,Gs,R2,B).
590
591abresolve(happens(A,T1,T2),[[HA,TC],RB],[],[[HA,TC],RB],false) :-
592 member(happens(A,T1,T2),HA),
593
594 595 596 597 !.
598
599abresolve(happens(A,T,T),[[HA,TC],RB],[],[[[happens(A,T,T)|HA],TC],RB],B) :-
600 executable(A), !, B = true, skolemise(T).
601
602abresolve(happens(A,T1,T2),R1,[],R2,B) :-
603 !, B = true, skolemise(T1), skolemise(T2), add_happens(A,T1,T2,R1,R2).
604
609
610abresolve(before(X,Y),R,[],R,false) :-
611 skolemise(X), skolemise(Y), demo_before(X,Y,R), !.
612
613abresolve(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
621
622abresolve(diff(X,Y),R,[],R,false) :- !, X \= Y.
623
624abresolve(is(X,Y),R,[],R,false) :- !, X is Y.
625
626
627
630
631abresolve(prolog(Code),R,[],R,false) :- !, Code.
632
633%Access Knowledge base
634abresolve(knowledgeBase(Username, GroupList),R,[],R,false) :- !, knowledgeDb :: lookupUserProlog(Username, Groups), !,listMember(GroupList, Groups),!.
635
637abresolve(valid_html_form(Type, Att),R,[],R,false):- !, valid_html_form(Type,Att).
638
640abresolve(valid_html_formChildren(Type, Children),R,[],R,false):- !, valid_html_formChildren(Type,Children).
641
642
643
644breakupResidual( [[X,Y],[Z,A]] , X).
645
646
648abresolve(notOccured(Action),R,[],R,false) :-
649 !,
650 breakupResidual(R,Actions),!,
651 \+ member(Action, Actions).
652
653abresolve(occured(Action),R,[],R,false) :-
654 !,
655 breakupResidual(R,Actions),!,
656 member(Action, Actions).
657
658
659
660
661abresolve(G,R,[],[G|R],false) :- abducible(G).
662
663abresolve(G,R,Gs,R,false) :- writeln('--------------------'), writeNoln(G),writeln('--------------------'), axiom(G,Gs).
664
665
666
667
669
670
689
690
691abdemo_nafs([],R,R,N,N,D).
692
693abdemo_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
724
725abdemo_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
732abdemo_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
751
753
754abdemo_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
759abdemo_naf([holds_at(F,T)|Gs],R1,R2,N1,N2,D) :-
760 !, abdemo_naf(Gs,R1,R2,N1,N2,D).
761
771
772abdemo_naf([before(X,Y)|Gs],R,R,N,N,D) :- X == Y, !.
773
774abdemo_naf([before(X,Y)|Gs],R,R,N,N,D) :- demo_before(Y,X,R), !.
775
776abdemo_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
786
787abdemo_naf([postponed(before(X,Y))|Gs],R1,R2,N,N,D) :-
788 \+ demo_beq(X,Y,R1), add_before(Y,X,R1,R2).
789
790abdemo_naf([postponed(before(X,Y))|Gs],R1,R2,N1,N2,D) :-
791 !, abdemo_naf(Gs,R1,R2,N1,N2,D).
792
797
799
800abdemo_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
804abdemo_naf([not(G)|Gs],R1,R2,N1,N2,D) :- !, abdemo_naf(Gs,R1,R2,N1,N2,D).
805
806abdemo_naf([G|Gs1],R,R,N,N,D) :- \+ abresolve(G,R,Gs2,R,false), !.
807
808abdemo_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
819
820abdemo_naf_cont(R1,Gs,R2,R2,N,N,D).
821
822abdemo_naf_cont(R1,Gs,R2,R3,N1,N2,D) :-
823 R1 \= R2, abdemo_naf(Gs,R1,R3,N1,N2,D).
824
825
837
838
839check_nafs(false,N1,R,R,N2,N2,D) :- !.
840
841check_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
844check_nafs(A,T1,T2,[],R,R,N,N,D).
845
846check_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
851check_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
856check_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
861check_naf(A,T1,T2,N,R1,R2,N1,N2,D) :- abdemo_naf(N,R1,R2,N1,N2,D).
862
863
864
865
867
868
875
876demo_before(0,Y,R) :- !, Y \= 0.
877
878demo_before(X,Y,[RH,[BA,TC]]) :- member(before(X,Y),TC).
879
881
882demo_beq(X,Y,R) :- X == Y, !.
883
884demo_beq(X,Y,R) :- demo_before(X,Y,R), !.
885
886demo_beq(X,Y,[[HA,TC],RB]) :- member(beq(X,Y),TC).
887
888
895
896add_before(X,Y,[RH,[BA,TC]],[RH,[BA,TC]]) :- member(before(X,Y),TC), !.
897
898add_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
911
912add_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
924
925find_bef_connections(X,Y,[],[X],[Y]).
926
927find_bef_connections(X,Y,[before(Z,X)|R],[Z|C1],C2) :-
928 !, find_bef_connections(X,Y,R,C1,C2).
929
930find_bef_connections(X,Y,[before(Y,Z)|R],C1,[Z|C2]) :-
931 !, find_bef_connections(X,Y,R,C1,C2).
932
933find_bef_connections(X,Y,[before(Z1,Z2)|R],C1,C2) :-
934 find_bef_connections(X,Y,R,C1,C2).
935
940
941find_beq_connections(X,Y,[],[X],[Y]).
942
943find_beq_connections(X,Y,[beq(Z,X)|R],[Z|C1],C2) :-
944 !, find_beq_connections(X,Y,R,C1,C2).
945
946find_beq_connections(X,Y,[beq(Y,Z)|R],C1,[Z|C2]) :-
947 !, find_beq_connections(X,Y,R,C1,C2).
948
949find_beq_connections(X,Y,[beq(Z1,Z2)|R],C1,C2) :-
950 find_beq_connections(X,Y,R,C1,C2).
951
952
953cross_prod_bef([],C,[],R).
954
955cross_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
958cross_one_bef(X,[],[],R).
959
960cross_one_bef(X,[Y|C],[before(X,Y)|R1],R) :-
961 \+ member(before(X,Y),R), !, cross_one_bef(X,C,R1,R).
962
963cross_one_bef(X,[Y|C],R1,R) :- cross_one_bef(X,C,R1,R).
964
965
966cross_prod_beq([],C,[],R).
967
968cross_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
971cross_one_beq(X,[],[],R).
972
973cross_one_beq(X,[Y|C],[beq(X,Y)|R1],R) :-
974 \+ member(beq(X,Y),R), !, cross_one_beq(X,C,R1,R).
975
976cross_one_beq(X,[Y|C],R1,R) :- cross_one_beq(X,C,R1,R).
977
978
979
980
982
983
1012
1013refine([[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
1027
1028split_happens([happens(A,T1,T2)],RB,happens(A,T1,T2),[]) :- !.
1029
1030split_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
1037order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
1038 happens(A1,T1,T2),happens(A2,T3,T4)) :-
1039 \+ executable(A1), executable(A2), !.
1040
1041order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
1042 happens(A2,T3,T4),happens(A1,T1,T2)) :-
1043 \+ executable(A2), executable(A1), !.
1044
1045order(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
1049order(happens(A1,T1,T2),happens(A2,T3,T4),RB,happens(A2,T3,T4),happens(A1,T1,T2)).
1050
1051
1052split_befores([],T1,T2,T3,T4,[],[]).
1053
1054split_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
1057split_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
1062split_beqs([],T1,T2,T3,T4,[],[]).
1063
1064split_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
1067split_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
1072split_nafs([],T1,T2,T3,T4,[],[]).
1073
1074split_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
1077split_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
1082split_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
1086split_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
1091split_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
1096substitute_time(T1,T1,T2,T3,T4,T3) :- !.
1097substitute_time(T2,T1,T2,T3,T4,T4) :- !.
1098substitute_time(T1,T2,T3,T4,T5,T1).
1099
1100no_match(T1,T2,T3,T4) :- T1 \= T3, T2 \= T3, T1 \= T4, T2 \= T4.
1101
1102
1103
1104
1106
1107
1112
1113add_neg(N,Ns,Ns) :- member(N,Ns), !.
1114add_neg(N,Ns,[N|Ns]).
1115
1116
1118
1119append_negs([],[],[]).
1120append_negs([N|Ns1],Ns2,Ns4) :- add_neg(N,Ns2,Ns3), append(Ns1,Ns3,Ns4).
1121
1122
1127
1129count([],Result, Result).
1130count([Head|Tail], Accum, Result) :-
1131 IncAccum is Accum+1,
1132 count(Tail,IncAccum,Result).
1133
1134listlength( [Head|Tail], Result ) :-
1135 count([Head|Tail],0,Result).
1136
1137
1139
1140skolemise(T) :- var(T), gensym(t,T), !.
1141skolemise(T).
1142
1143
1144opposite(neg(F),F) :- !.
1145opposite(F,neg(F)).
1146
1147trace(off,0).
1148trace(off,1)