17
18
19
22
33
34
82
85
86
97
98abdemo(Gs,[HA,BA]) :-
99 init_gensym(t), first_d(D),
100 abdemo_top(Gs,[[[],[]],[[],[]]],[[HA,HC],[BA,BC]],[],N,D),
101 write_plan_len(HA,BA).
102
103abdemo_timed(Gs,[HA,BA]) :-
104 ticks(Z1),
105 abdemo(Gs,[HA,BA]),
106 write_plan(HA,BA),
107 ticks(Z2), Z is (Z2-Z1)/60, write('Total time taken '), writeYesln(Z).
108abdemo_top(Gs,R1,R3,N1,N3,D, _MaxDepth, _HighLevel) :-
109 must(nonvar(Gs)),
110 abdemo_id(Gs,R1,R2,N1,N2,D), !,
111 abdemo_cont(R2,R3,N2,N3).
112
118
119abdemo_cont([[HA,TC],RB],[[HA,TC],RB],N,N) :- all_executable(HA), !.
120
121abdemo_cont([[HA,HC],[BA,BC]],R2,N1,N3) :-
122 123 dbginfo('Abstract plan:'=[HA,BA]),
124 refine([[HA,HC],[BA,BC]],N1,Gs,R1,N2), action_count([[HA,HC],[BA,BC]],D),
125 abdemo_top(Gs,R1,R2,N2,N3,D).
126
127
129
130abdemo_id(Gs,R1,R2,N1,N2,D) :-
131 write(' D'), write(D), write(' '), ttyflush,
132 (abdemo(Gs,R1,R2,N1,N2,D)*-> true; (next_d(D,D2)->abdemo_id(Gs,R1,R2,N1,N2,D2))).
133
134
135
136all_executable(X):- \+ is_list(X),!,fail.
137all_executable([]).
138all_executable([H|R]) :- was_executable(H), all_executable(R).
139
140was_executable(H):- H = happens(A,_T1,_T2), must(executable(A)).
141
142
143general_interp:- true.
144
146
147
156
157
158
169abdemo([],R,R,N,N,D).
170abdemo([G|Gs],R1,R2,N1,N2,D):-
171 abdemo_cons(G,Gs,R1,R2,N1,N2,D).
172
173
174check_goals([]):-!.
175check_goals([H|T]):-check_goal(H),!,check_goals(T).
176check_goal(b(T1,T2)):- T1=@=T2,!,barf.
177check_goal(_).
178
179maybe_note_ab(Why,H,T,[[HA,TC1],[BA,TC2]],R,N1,N2,D) :-
180 Gs=[H|T],
181 setup_call_cleanup((notrace((
182 (( N1 \== [], Gs == [] ); ( N1 == [], Gs \== [] ); ( N1 \== [], Gs \== [] )),
183 184 dbginfo('Why'=Why),
185 186 dbginfo('Goals'=Gs),
187 dbginfo('Happens'=HA),
188 dbginfo('Befores'=BA),
189 dbginfo('Nafs'=N1),nl,nl,fail))),true,true),fail.
190
191:- discontiguous abdemo_cons/7. 192:- discontiguous abdemo_cons/7. 193
196
197abdemo_cons(b(X,Y),Gs1,R1,R3,N1,N2,D) :-
198 abresolve_b(b(X,Y),R1,Gs2,R2,B), append(Gs2,Gs1,Gs3),
199 notrace((iv_list_to_set(Gs3,Gs4),(((Gs3\==Gs4)-> (!,fail) ; true)))),
200 ignore(Gs3 = Gs4),!,
201 abdemo(Gs4,R2,R3,N1,N2,D).
202
203abresolve_b(b(X,Y),R1,[],R2,B) :- !, B = false,
204 skolemise_time(X), skolemise_time(Y),
205 ((R2=R1,demo_before(X,Y,R2)) -> true ;
206 (\+ demo_beq(Y,X,R1),
207 add_before(X,Y,R1,R2))).
208
209abdemo_cons(H,Gs, R1,R4,N1,N3,D):- maybe_note_ab(abdemo_cons, H,Gs,R1,R4,N1,N3,D),fail.
210abdemo_cons(H,Gs, R1,R4,N1,N3,D):- notrace((check_goals([H|Gs]),fail)).
211
212abdemo_cons(H,[HH|Gs],R1,R4,N1,N3,D):-
213 iv_list_to_set([H,HH|Gs],Set), Set\=@=[H,HH|Gs],!,
214 abdemo(Set,R1,R4,N1,N3,D).
215
216 217abdemo_cons(call(P),[H,I|Gs],R1,R4,N1,N3,D):- H\=call(_), !,
218 abdemo_cons(H,[I,call(P)|Gs],R1,R4,N1,N3,D).
220abdemo_cons((A;B),[H,I|Gs],R1,R4,N1,N3,D):- H\=(A;B), !,
221 abdemo_cons(H,[I,(A;B)|Gs],R1,R4,N1,N3,D).
223abdemo_cons(call(P),[H|Gs],R1,R4,N1,N3,D):- H\=call(_), !,
224 abdemo_cons(H,[call(P)|Gs],R1,R4,N1,N3,D).
225
226abdemo_cons(H,T,R1,R2,N1,N2,D):-
227 KEY = abdemo(H,T,R1,R2,N1,N2),
228 ((nb_current(last_call_abdemo,Was);Was=[])->
229 (((member(X,Was),X=@=KEY))
230 -> (!,fail);
231 ((nb_setval(last_call_abdemo,[KEY|Was]),fail)))).
232
233abdemo_cons(holds_at(F1,T),Gs1,R1,R3,N1,N3,D):- !,
234 abdemo_cons_holds_at(F1,T,Gs1,R1,R3,N1,N3,D).
235
236
252fill_in_tempargs(Pred, F1):- fill_in_tempargs_1(Pred, F1).
253fill_in_tempargs(Pred, neg(F1)):- fill_in_tempargs_1(Pred, F1).
254fill_in_tempargs_1(Pred, F1):- call(Pred,X),
255 functor(X,F,A),functor(F1,F,A),
256 fill_in_tempargs_each(X,F1).
257
258fill_in_tempargs_each(_,F1):- ground(F1),!.
259fill_in_tempargs_each(_,F1):- findall(F1,in_domain_db(F1),List),iv_list_to_set(List,Set),!,member(F1,Set).
260
261in_domain_db(F1):- user:ec_current_domain_db(axiom(Stuff,Body), _),sub_term(F1,Stuff+Body),ground(F1).
262
263abdemo_cons_holds_at(F1,T,Gs1,R1,R3,N1,N4,D):- var(F1),!,
264 fill_in_tempargs(fluent,F1), abdemo_cons_holds_at(F1,T,Gs1,R1,R3,N1,N4,D).
265abdemo_cons_holds_at(neg(F1),T,Gs1,R1,R3,N1,N4,D):- var(F1),!,
266 fill_in_tempargs(fluent,F1), abdemo_cons_holds_at(neg(F1),T,Gs1,R1,R3,N1,N4,D).
267
268abdemo_cons_holds_at(F1,T,Gs1,R1,R3,N1,N4,D) :-
269 F1 \= neg(_F2), abresolve(initially(F1),R1,Gs2,R1,B),
270 append(Gs2,Gs1,Gs3), add_neg_car(clipped(0,F1,T),N1,N2),
271 abdemo_naf_cons(clipped(0,F1,T),[],R1,R2,N2,N3,D),
272 abdemo(Gs3,R2,R3,N3,N4,D).
273
280
281abdemo_cons_holds_at(F1,T3,Gs1,R1,R6,N1,N5,D) :-
282 F1 \= neg(_F2), abresolve(initiates(A,F1,T1),R1,Gs2,R1,B1),
283 abresolve(happens(A,T1,T2),R1,[],R2,B2),
284 check_depth(R2,D),
285 abresolve(b(T2,T3),R2,[],R3,B3),
286 append(Gs2,Gs1,Gs3), check_nafs(B2,N1,R3,R4,N1,N2,D),
287 add_neg_car(clipped(T1,F1,T3),N2,N3),
288 abdemo_naf_cons(clipped(T1,F1,T3),[],R4,R5,N3,N4,D),
289 abdemo(Gs3,R5,R6,N4,N5,D).
290
301
302abdemo_cons_holds_at(neg(F),T,Gs1,R1,R3,N1,N4,D) :-
303 abresolve(initially(neg(F)),R1,Gs2,R1,B),
304 append(Gs2,Gs1,Gs3), add_neg_car(declipped(0,F,T),N1,N2),
305 abdemo_naf_cons(declipped(0,F,T),[],R1,R2,N2,N3,D),
306 abdemo(Gs3,R2,R3,N3,N4,D).
307
308abdemo_cons_holds_at(neg(F),T3,Gs1,R1,R6,N1,N5,D) :-
309 abresolve(terminates(A,F,T1),R1,Gs2,R1,B1),
310 abresolve(happens(A,T1,T2),R1,[],R2,B2),
311 check_depth(R2,D),
312 abresolve(b(T2,T3),R2,[],R3,B3),
313 append(Gs2,Gs1,Gs3), check_nafs(B2,N1,R3,R4,N1,N2,D),
314 add_neg_car(declipped(T1,F,T3),N2,N3),
315 abdemo_naf_cons(declipped(T1,F,T3),[],R4,R5,N3,N4,D),
316 abdemo(Gs3,R5,R6,N4,N5,D).
317
318abdemo_cons_holds_at(F1,T,Gs1,R1,R3,N1,N2,D) :-
319 G = holds_at(F1,T),
320 abresolve(G,R1,Gs2,R2,B), append(Gs2,Gs1,Gs3),
321 notrace((iv_list_to_set(Gs3,Gs4),(((Gs3\==Gs4)-> (!,fail) ; true)))),
322 ignore(Gs3 = Gs4),
323 abdemo(Gs4,R2,R3,N1,N2,D),
324 writeNoln('terminate action:'),
325 writeYesln(A),
326 writeNoln('precondition:'),
327 writeYesln(Gs2).
328
329
338
339abdemo_cons(happens(A,T1,T2),Gs,R1,R4,N1,N3,D) :- !,
340 abresolve(happens(A,T1,T2),R1,[],R2,B), check_depth(R2,D),
341 check_nafs(B,N1,R2,R3,N1,N2,D), abdemo(Gs,R3,R4,N2,N3,D).
342
343abdemo_cons(happens(A,T),Gs,R1,R4,N1,N3,D) :- !,
344 abresolve(happens(A,T),R1,[],R2,B), check_depth(R2,D),
345 check_nafs(B,N1,R2,R3,N1,N2,D), abdemo(Gs,R3,R4,N2,N3,D).
346
362
363abdemo_cons(expand([happens(A,T1,T2)|Bs]),Gs1,R1,R8,N1,N8,D) :- !,
364 axiom(happens(A,T1,T2),Gs2),
365 add_sub_actions(Gs2,R1,R2,N1,N2,D,Hs),
366 solve_befores(Bs,R2,R3,N2,N3,D),
367 abdemo_holds_ats(Gs2,R3,R4,N3,N4,D),
368 solve_other_goals(Gs2,R4,R5,N4,N5,D),
369 check_clipping(Gs2,R5,R6,N5,N6,D),
370 check_sub_action_nafs(Hs,N1,R6,R7,N6,N7,D),
371 abdemo(Gs1,R7,R8,N7,N8,D).
372
373
379
381
382abdemo_cons((G1;G2),Gs,R1,R3,N1,N4,D) :- general_interp, !,
383 (abdemo_cons(G1,Gs,R1,R3,N1,N4,D);
384 abdemo_cons(G2,Gs,R1,R3,N1,N4,D)).
385
386abdemo_cons((G,G0),Gs,R1,R2,N1,N2,D):- !,
387 abdemo_cons(G,[G0|Gs],R1,R2,N1,N2,D).
388
389abdemo_cons(not(G),Gs,R1,R3,N1,N4,D) :-
390 391 abdemo_naf_cons(G,[],R1,R2,N1,N2,D), add_neg_car(G,N2,N3),
392 abdemo(Gs,R2,R3,N3,N4,D).
393
394abdemo_cons(G,Gs1,R1,R3,N1,N2,D) :-
395 abresolve(G,R1,Gs2,R2,B), append(Gs2,Gs1,Gs3),
396 notrace((iv_list_to_set(Gs3,Gs4),(((Gs3\==Gs4)-> (!,fail) ; true)))),
397 ignore(Gs3 = Gs4),
398 abdemo(Gs4,R2,R3,N1,N2,D).
399check_depth(R,D):- check_depth(R,D,_L).
400
401check_depth(R,D,L) :- ec_trace(on,1),
402 action_count(R,L),
403 writeNoln('Actions:'),
404 writeYesln(R),
405 writeNoln('Action count:'), writeNoln(L), fail.
406
408check_depth(R,D,L) :- action_count(R,L), L =< D, D =< 1000.
409
411check_depth(R,D,L) :- ec_trace(on, 1), writeNoln('Maximum bound reached'),!, fail.
412
413
414
415
416
417action_count([[HA,TC],RB],L) :- length(HA,L).
418
419
420
421
423
424
426
427
428abdemo_holds_ats([],R,R,N,N,D).
429
430abdemo_holds_ats([holds_at(F,T)|Gs],R1,R3,N1,N3,D) :-
431 !, abdemo_cons_holds_at(F,T,[],R1,R2,N1,N2,D),
432 abdemo_holds_ats(Gs,R2,R3,N2,N3,D).
433
434abdemo_holds_ats([G|Gs],R1,R2,N1,N2,D) :-
435 abdemo_holds_ats(Gs,R1,R2,N1,N2,D).
436
437
438non_regular_goal(G):- \+ regular_goal(G).
439
440regular_goal(holds_at(_F, _T)).
441regular_goal(happens(_A, _T)).
442regular_goal(happens(_A, _T1, _T2)).
443regular_goal(b(_T1, _T2)).
444regular_goal(not(Clip)):- nonvar(Clip),
445 (Clip = clipped(_T1,_F,_T2) ; Clip = declipped(_DT1,_FD,_DT2)).
446
447solve_other_goals([],R,R,N,N,D).
448
449solve_other_goals([G|Gs],R1,R3,N1,N3,D) :-
450 non_regular_goal(G), !,
451 abdemo_cons(G,[],R1,R2,N1,N2,D),
452 solve_other_goals(Gs,R2,R3,N2,N3,D).
453
454solve_other_goals([G|Gs],R1,R2,N1,N2,D) :-
455 solve_other_goals(Gs,R1,R2,N1,N2,D).
456
463
464add_sub_actions([],R,R,N,N,D,[]).
465add_sub_actions([G|Gs],R1,R2,N1,N2,D,L):-
466 add_sub_actions_cons(G,Gs,R1,R2,N1,N2,D,L).
467
468add_sub_actions_cons(happens(A,T1,T2),Gs,R1,R3,N1,N3,D,Hs2) :-
469 !,
470 abresolve(happens(A,T1,T2),R1,[],R2,B), check_depth(R2,D),
471 add_sub_actions(Gs,R2,R3,N2,N3,D,Hs1), cond_add(B,happens(A,T1,T2),Hs1,Hs2).
472
473add_sub_actions_cons(happens(A,T),Gs,R1,R3,N1,N3,D,Hs2) :-
474 !, abresolve(happens(A,T),R1,[],R2,B), check_depth(R2,D),
475 add_sub_actions(Gs,R2,R3,N2,N3,D,Hs1), cond_add(B,happens(A,T,T),Hs1,Hs2).
476
477add_sub_actions_cons(b(T1,T2),Gs,R1,R3,N1,N3,D,Hs) :-
478 !, abresolve(b(T1,T2),R1,[],R2,B),
479 add_sub_actions(Gs,R2,R3,N2,N3,D,Hs).
480
481add_sub_actions_cons(G,Gs,R1,R2,N1,N2,D,Hs) :-
482 add_sub_actions(Gs,R1,R2,N1,N2,D,Hs).
483
484
485cond_add(false,H,Hs,Hs) :- !.
486
487cond_add(true,H,Hs,[H|Hs]).
488
489
490solve_befores([],R,R,N,N,D).
491
492solve_befores([b(T1,T2)|Gs],R1,R3,N1,N3,D) :-
493 !, abdemo_cons(b(T1,T2),[],R1,R2,N1,N2,D),
494 solve_befores(Gs,R2,R3,N2,N3,D).
495
496solve_befores([G|Gs],R1,R2,N1,N2,D) :-
497 solve_befores(Gs,R1,R2,N1,N2,D).
498
499
500check_sub_action_nafs([],N1,R,R,N2,N2,D) :- !.
501
502check_sub_action_nafs([happens(A,T1,T2)|Hs],N1,R1,R3,N2,N4,D) :-
503 check_nafs(A,T1,T2,N1,R1,R2,N2,N3,D),
504 check_sub_action_nafs(Hs,N1,R2,R3,N3,N4,D).
505
506
507check_clipping([],R,R,N,N,D) :- !.
508
509check_clipping([not(Clipped)|Gs],R1,R3,N1,N3,D) :-
510 511 (Clipped= clipped(T1,F,T2); Clipped=declipped(T1,F,T2)),
512 !, abdemo_naf_cons(Clipped,[],R1,R2,N1,N2,D),
513 check_clipping(Gs,R2,R3,N2,N3,D).
514
515check_clipping([G|Gs],R1,R2,N1,N2,D) :-
516 check_clipping(Gs,R1,R2,N1,N2,D).
517
518
519
520
521ammend_preconds4(A, T, Gs,Gss):-
522 findall(PrecondL, axiom_db(requires(A, T),PrecondL),PrecondLs),
523 append([Gs|PrecondLs],Gss).
524
525
527
528
537no_dbl_start(Gss):- \+ (member(b(start, Next),Gss), Next==start).
538
539abresolve(G,R1,Gs,R2,B):- notrace(var(G)),!,throw(var_abresolve(G,R1,Gs,R2,B)).
540
541abresolve(initially(A),R,Gss,R, False) :- !, abresolve(holds_at(A, start),R,Gss,R, False),
542 no_dbl_start(Gss).
543
544abresolve(terms_or_rels(A,F,T),R,Gss,R,false) :- axiom_db(releases(A,F,T),Gs), ammend_preconds4(A,T,Gs,Gss).
545abresolve(terms_or_rels(A,F,T),R,Gss,R,false) :- !, axiom_db(terminates(A,F,T),Gs), ammend_preconds4(A,T,Gs,Gss).
546
547abresolve(inits_or_rels(A,F,T),R,Gss,R,false) :- axiom_db(releases(A,F,T),Gs), ammend_preconds4(A,T,Gs,Gss).
548abresolve(inits_or_rels(A,F,T),R,Gss,R,false) :- !, axiom_db(initiates(A,F,T),Gs), ammend_preconds4(A,T,Gs,Gss).
549
550
564
565abresolve(happens(A,T),R1,Gs,R2,B) :- !, abresolve(happens(A,T,T),R1,Gs,R2,B).
566
567abresolve(happens(A,T1,T2),[[HA,TC],RB],[],[[HA,TC],RB],false) :-
568 member(happens(A,T1,T2),HA).
569
570abresolve(happens(A,T,T),[[HA,TC],RB],[],[[[happens(A,T,T)|HA],TC],RB],B) :-
571 into_db(executable(A)), !, B = true, skolemise_time(T).
572
573abresolve(happens(A,T1,T2),R1,[],R2,B) :- !, B = true,
574 skolemise_time(T1), skolemise_time(T2), add_happens(A,T1,T2,R1,R2).
575
580abresolve(b(X,Y),R1,Nil,R2,B):- !, abresolve_b(b(X,Y),R1,Nil,R2,B).
581
586
587abresolve(diff(X,Y),R,[],R,false) :- !, X \= Y.
588abresolve(ignore(_),R,[],R,false) :- !.
589abresolve(allDifferent(_),R,[],R,false) :- !.
590abresolve(is(X,Y),R,[],R,false) :- !, X is Y.
591abresolve(equals(X,Y),R,[],R,false) :- !, X = Y.
592abresolve(dif(X,Y),R,[],R,false) :- !, dif(X,Y).
593abresolve(call(G),R,[],R,false) :- !, into_db(call(G)).
594
596abresolve((G1;G2),ResidueIn,Goals,ResidueOut,Flag):- !,
597 (abresolve(G1,ResidueIn,Goals,ResidueOut,Flag);
598 abresolve(G2,ResidueIn,Goals,ResidueOut,Flag)).
599
600abresolve((G1,G2),ResidueIn,Goals,ResidueOut,Flag):- !,
601 (abresolve(G1,ResidueIn,Goals1,ResidueMid,Flag),
602 abresolve(G2,ResidueMid,Goals2,ResidueOut,Flag)),
603 append(Goals1,Goals2,Goals).
604
605
606
607abresolve(G,R,[],[G|R],false) :- quietly(into_db(abducible(G))).
608
609abresolve(G,R,Gs,R,false) :- axiom_db(G,Gs),re_constrain(G,Gs,Gss).
610
612re_constrain(B,B).
613
614re_constrain(G,[B|Bs],[BB|BBs]):- re_constrain(G,Bs,BBs), re_constrain(B,BB).
615re_constrain(_,Bs,Bs):-!.
616
618
619
638
639
640abdemo_nafs([],R,R,N,N,D).
641
642abdemo_nafs([N|Ns],R1,R3,N1,N3,D) :-
643 abdemo_naf(N,R1,R2,N1,N2,D), abdemo_nafs(Ns,R2,R3,N2,N3,D).
644
645
669
670abdemo_naf( [G|Gs1 ],R1,R2,N1,N2,D) :-
671 abdemo_naf_cons(G,Gs1,R1,R2,N1,N2,D).
672
673:- discontiguous abdemo_naf_cons/7. 674
675abdemo_naf_cons(H,Gs, R1,R4,N1,N3,D):- maybe_note_ab(abdemo_naf_cons, H,Gs,R1,R4,N1,N3,D),fail.
676
677abdemo_naf_cons(clipped(T1,F,T4),Gs1,R1,R2,N1,N2,D) :-
678 !, findall(Gs3,
679 (abresolve(terms_or_rels(A,F,T2),R1,Gs2,R1,false),
680 abresolve(happens(A,T2,T3),R1,[],R1,false),
681 append([b(T1,T3),b(T2,T4)|Gs2],Gs1,Gs3)),Gss),
682 abdemo_nafs(Gss,R1,R2,N1,N2,D).
683
684abdemo_naf_cons(declipped(T1,F,T4),Gs1,R1,R2,N1,N2,D) :-
685 !, findall(Gs3,
686 (abresolve(inits_or_rels(A,F,T2),R1,Gs2,R1,false),
687 abresolve(happens(A,T2,T3),R1,[],R1,false),
688 append([b(T1,T3),b(T2,T4)|Gs2],Gs1,Gs3)),Gss),
689 abdemo_nafs(Gss,R1,R2,N1,N2,D).
690
703
704abdemo_naf_cons(holds_at(F1,T),Gs1,R1,R3,N1,N3,D):- !,
705 abdemo_naf_cons_holds_at(F1,T,Gs1,R1,R3,N1,N3,D).
706
717abdemo_naf_cons_holds_at(F1,T,Gs1,R1,R3,N1,N3,D) :-
718 opposite(F1,F2),
719 (abdemo_cons_holds_at(F2,T,[],R1,R2,N1,N2,D), !,
720 (copy_term(Gs1,Gs2), abdemo_naf_cont(R1,Gs2,R2,R3,N1,N3,D))).
721
722abdemo_naf_cons_holds_at(_F,_T,Gs,R1,R3,N1,N3,D) :-
723 abdemo_naf(Gs,R1,R3,N1,N3,D).
724
734
735abdemo_naf_cons(b(X,Y),Gs,R,R,N,N,D) :- X == Y, !.
736
737abdemo_naf_cons(b(X,Y),Gs,R,R,N,N,D) :- demo_before(Y,X,R), !.
738
739abdemo_naf_cons(b(X,Y),Gs1,R1,R2,N1,N2,D) :-
740 !, append(Gs1,[postponed(b(X,Y))],Gs2),
741 abdemo_naf(Gs2,R1,R2,N1,N2,D).
742
749
750abdemo_naf_cons(postponed(b(X,Y)),Gs,R1,R2,N,N,D) :-
751 \+ demo_beq(X,Y,R1), add_before(Y,X,R1,R2).
752
753abdemo_naf_cons(postponed(b(X,Y)),Gs,R1,R2,N1,N2,D) :-
754 !, abdemo_naf(Gs,R1,R2,N1,N2,D).
755
761abdemo_naf_cons((G,G0),Gs,R1,R2,N1,N2,D):- !,
762 abdemo_naf_cons(G,[G0|Gs],R1,R2,N1,N2,D).
764abdemo_naf_cons((G1;G2),Gs,R1,R3,N1,N4,D) :- !,
765 (abdemo_naf_cons(G1,Gs,R1,R3,N1,N4,D);
766 abdemo_naf_cons(G2,Gs,R1,R3,N1,N4,D)).
767
768:- discontiguous(abdemo_naf_cons/7). 769
770
779abdemo_naf_cons_not(G,Gs1,R1,R3,N1,N3,D) :-
780 abdemo_cons(G,[],R1,R2,N1,N2,D) *->
781 (copy_term(Gs1,Gs2), abdemo_naf_cont(R1,Gs2,R2,R3,N1,N3,D)) ;
782 abdemo_naf(Gs,R1,R3,N1,N3,D).
783
784
785abdemo_naf_cons(not(G),Gs1,R1,R3,N1,N3,D):-
786 787 abdemo_naf_cons_not(G,Gs1,R1,R3,N1,N3,D),
788 !. 789
790abdemo_naf_cons(G,Gs1,R,R,N,N,D) :- \+ abresolve(G,R,Gs2,R,false), !.
791
792abdemo_naf_cons(G1,Gs1,R1,R2,N1,N2,D) :-
793 findall(Gs2,
794 (abresolve(G1,R1,Gs3,R1,false), append(Gs3,Gs1,Gs2)),
795 Gss),
796 abdemo_nafs(Gss,R1,R2,N1,N2,D).
797
798
805
806abdemo_naf_cont(R1,_Gs,R2,R2,N,N,D).
807
808abdemo_naf_cont(R1,Gs,R2,R3,N1,N2,D) :-
809 R1 \= R2, abdemo_naf(Gs,R1,R3,N1,N2,D).
810
811
823
824
825check_nafs(false,N1,R,R,N2,N2,D) :- !.
826
827check_nafs(true,N,[[[happens(A,T1,T2)|HA],TC],RB],R,N1,N2,D) :-
828 check_nafs(A,T1,T2,N,[[[happens(A,T1,T2)|HA],TC],RB],R,N1,N2,D).
829
830check_nafs(A,T1,T2,[],R,R,N,N,D).
831
832check_nafs(A,T1,T2,[N|Ns],R1,R3,N1,N3,D) :-
833 check_naf(A,T1,T2,N,R1,R2,N1,N2,D),
834 check_nafs(A,T1,T2,Ns,R2,R3,N2,N3,D).
835
836
837check_naf(A,T2,T3,[clipped(T1,F,T4)],R1,R2,N1,N2,D) :-
838 !, findall([b(T1,T3),b(T2,T4)|Gs],
839 (abresolve(terms_or_rels(A,F,T2),R1,Gs,R1,false)),Gss),
840 abdemo_nafs(Gss,R1,R2,N1,N2,D).
841
842check_naf(A,T2,T3,[declipped(T1,F,T4)],R1,R2,N1,N2,D) :-
843 !, findall([b(T1,T3),b(T2,T4)|Gs],
844 (abresolve(inits_or_rels(A,F,T2),R1,Gs,R1,false)),Gss),
845 abdemo_nafs(Gss,R1,R2,N1,N2,D).
846
847check_naf(A,T1,T2,N,R1,R2,N1,N2,D) :- abdemo_naf(N,R1,R2,N1,N2,D).
848
849
850
851
853
854
861
862demo_before(0,Y,R) :- !, Y \= 0.
863
864demo_before(X,Y,[RH,[BA,TC]]) :- member(b(X,Y),TC).
865
867
868demo_beq(X,Y,R) :- X == Y, !.
869
870demo_beq(X,Y,R) :- demo_before(X,Y,R), !.
871
872demo_beq(X,Y,[[HA,TC],RB]) :- member(beq(X,Y),TC).
873
874
881
882add_before(X,Y,[RH,[BA,TC]],[RH,[BA,TC]]) :- member(b(X,Y),TC), !.
883
884add_before(X,Y,[[HA,HC],[BA,BC1]],[[HA,HC],[[b(X,Y)|BA],BC2]]) :-
885 \+ demo_beq(Y,X,[[HA,HC],[BA,BC1]]), find_bef_connections(X,Y,BC1,C1,C2),
886 find_beq_connections(X,Y,HC,C3,C4), delete_abdemo(X,C3,C5), delete_abdemo(Y,C4,C6),
887 append(C5,C1,C7), append(C6,C2,C8),
888 cross_prod_bef(C7,C8,C9,BC1), append(C9,BC1,BC2).
889
897
898add_happens(A,T1,T2,[[HA,HC1],[BA,BC1]],[[[happens(A,T1,T2)|HA],HC2],[BA,BC2]]) :-
899 \+ demo_before(T2,T1,[[HA,HC1],[BA,BC1]]),
900 find_beq_connections(T1,T2,HC1,C1,C2), cross_prod_beq(C1,C2,C3,HC1),
901 append(C3,HC1,HC2), find_bef_connections(T1,T2,BC1,C4,C5),
902 cross_prod_bef(C4,C5,C6,BC1), delete_abdemo(b(T1,T2),C6,C7),
903 append(C7,BC1,BC2).
904
910
911find_bef_connections(X,Y,[],[X],[Y]).
912
913find_bef_connections(X,Y,[b(Z,X)|R],[Z|C1],C2) :-
914 !, find_bef_connections(X,Y,R,C1,C2).
915
916find_bef_connections(X,Y,[b(Y,Z)|R],C1,[Z|C2]) :-
917 !, find_bef_connections(X,Y,R,C1,C2).
918
919find_bef_connections(X,Y,[b(Z1,Z2)|R],C1,C2) :-
920 find_bef_connections(X,Y,R,C1,C2).
921
926
927find_beq_connections(X,Y,[],[X],[Y]).
928
929find_beq_connections(X,Y,[beq(Z,X)|R],[Z|C1],C2) :-
930 !, find_beq_connections(X,Y,R,C1,C2).
931
932find_beq_connections(X,Y,[beq(Y,Z)|R],C1,[Z|C2]) :-
933 !, find_beq_connections(X,Y,R,C1,C2).
934
935find_beq_connections(X,Y,[beq(Z1,Z2)|R],C1,C2) :-
936 find_beq_connections(X,Y,R,C1,C2).
937
938
939cross_prod_bef([],C,[],R).
940
941cross_prod_bef([X|C1],C2,R3,R) :-
942 cross_one_bef(X,C2,R1,R), cross_prod_bef(C1,C2,R2,R), append(R1,R2,R3).
943
944cross_one_bef(X,[],[],R).
945
946cross_one_bef(X,[Y|C],[b(X,Y)|R1],R) :-
947 \+ member(b(X,Y),R), !, cross_one_bef(X,C,R1,R).
948
949cross_one_bef(X,[Y|C],R1,R) :- cross_one_bef(X,C,R1,R).
950
951
952cross_prod_beq([],C,[],R).
953
954cross_prod_beq([X|C1],C2,R3,R) :-
955 cross_one_beq(X,C2,R1,R), cross_prod_beq(C1,C2,R2,R), append(R1,R2,R3).
956
957cross_one_beq(X,[],[],R).
958
959cross_one_beq(X,[Y|C],[beq(X,Y)|R1],R) :-
960 \+ member(beq(X,Y),R), !, cross_one_beq(X,C,R1,R).
961
962cross_one_beq(X,[Y|C],R1,R) :- cross_one_beq(X,C,R1,R).
963
964
965
966
968
969
998
999refine([[HA1,HC1],[BA1,BC1]],N1,Gs,[[HA2,HC2],[BA2,BC2]],N3) :-
1000 split_happens(HA1,[BA1,BC1],happens(A,T1,T2),HA2),
1001 split_beqs(HC1,T1,T2,T3,T4,HC3,HC2),
1002 split_befores(BA1,T1,T2,T3,T4,BA3,BA2),
1003 split_befores(BC1,T1,T2,T3,T4,BC3,BC2),
1004 split_nafs(N1,T1,T2,T3,T4,N2,N3),
1005 append([expand([happens(A,T3,T4)|BA3])],N2,Gs).
1006
1007
1013
1014split_happens([happens(A,T1,T2)],RB,happens(A,T1,T2),[]) :- !.
1015
1016split_happens([happens(A1,T1,T2)|RH1],RB,happens(A3,T5,T6),
1017 [happens(A4,T7,T8)|RH2]) :-
1018 split_happens(RH1,RB,happens(A2,T3,T4),RH2),
1019 order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
1020 happens(A3,T5,T6),happens(A4,T7,T8)).
1021
1022
1023order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
1024 happens(A1,T1,T2),happens(A2,T3,T4)) :-
1025 \+ executable(A1), executable(A2), !.
1026
1027order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
1028 happens(A2,T3,T4),happens(A1,T1,T2)) :-
1029 \+ executable(A2), executable(A1), !.
1030
1031order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
1032 happens(A1,T1,T2),happens(A2,T3,T4)) :-
1033 demo_before(T1,T3,[[],RB]), !.
1034
1035order(happens(A1,T1,T2),happens(A2,T3,T4),RB,happens(A2,T3,T4),happens(A1,T1,T2)).
1036
1037
1038split_befores([],T1,T2,T3,T4,[],[]).
1039
1040split_befores([b(T1,T2)|Bs1],T3,T4,T5,T6,Bs2,[b(T1,T2)|Bs3]) :-
1041 no_match(T1,T2,T3,T4), !, split_befores(Bs1,T3,T4,T5,T6,Bs2,Bs3).
1042
1043split_befores([b(T1,T2)|Bs1],T3,T4,T5,T6,[b(T7,T8)|Bs2],Bs3) :-
1044 substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
1045 split_befores(Bs1,T3,T4,T5,T6,Bs2,Bs3).
1046
1047
1048split_beqs([],T1,T2,T3,T4,[],[]).
1049
1050split_beqs([beq(T1,T2)|Bs1],T3,T4,T5,T6,Bs2,[beq(T1,T2)|Bs3]) :-
1051 no_match(T1,T2,T3,T4), !, split_beqs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
1052
1053split_beqs([beq(T1,T2)|Bs1],T3,T4,T5,T6,[beq(T7,T8)|Bs2],Bs3) :-
1054 substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
1055 split_beqs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
1056
1057
1058split_nafs([],T1,T2,T3,T4,[],[]).
1059
1060split_nafs([[ clipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,Bs2,[[clipped(T1,F,T2)]|Bs3]) :-
1061 no_match(T1,T2,T3,T4), !, split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
1062
1063split_nafs([[ clipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,
1064 [not(clipped(T7,F,T8))|Bs2],Bs3) :-
1065 !, substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
1066 split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
1067
1068split_nafs([[declipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,Bs2,
1069 [[declipped(T1,F,T2)]|Bs3]) :-
1070 no_match(T1,T2,T3,T4), !, split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
1071
1072split_nafs([[declipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,
1073 [not(declipped(T7,F,T8))|Bs2],Bs3) :-
1074 !, substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
1075 split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
1076
1077split_nafs([N|Bs1],T3,T4,T5,T6,Bs2,[N|Bs3]) :-
1078 substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
1079 split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
1080
1081
1082substitute_time(T1,T1,T2,T3,T4,T3) :- !.
1083substitute_time(T2,T1,T2,T3,T4,T4) :- !.
1084substitute_time(T1,T2,T3,T4,T5,T1).
1085
1086no_match(T1,T2,T3,T4) :- T1 \= T3, T2 \= T3, T1 \= T4, T2 \= T4.
1087
1088
1089
1090
1092
1093
1098
1099add_neg_car(N,Ns,Ns2):- add_neg([N],Ns,Ns2).
1100
1101add_neg(N,Ns,Ns) :- member(N,Ns), !.
1102add_neg(N,Ns,[N|Ns]).
1103
1104
1106
1107append_negs([],[],[]).
1108
1109append_negs([N|Ns1],Ns2,Ns4) :- add_neg(N,Ns2,Ns3), append(Ns1,Ns3,Ns4).
1110
1111
1112delete_abdemo(X,[],[]).
1113delete_abdemo(X,[X|L],L) :- !.
1114delete_abdemo(X,[Y|L1],[Y|L2]) :- delete_abdemo(X,L1,L2).
1115
1116
1117
1118
1119
1121
1122skolemise_time(T) :- notrace((ignore((var(T), gensym(t,T))))).
1123
1124
1125opposite(neg(F),F) :- !.
1126opposite(F,neg(F)).
1127
1128
1130
1131
1134axiom_db(H,B):- quietly(into_db(axiom(H,B))),no_dbl_start(B).
1135into_db(G):- call(G).
1136
1137
1138
1139:- fixup_exports.