1:-module(alpprolog,[]). 2
3:- expects_dialect(eclipse).
8:- use_module(wumpus_world_big). 9
10%:-lib(lists).
11
12:-export execute/1.
13:-export holds/1.
14:-export init/0.
15:-export state/1.
16
17:- local(variable(current_units)). 18:- local(variable(current_clauses)). 19
20
21
27
28init :-
29 initial_state(S),
30 normalize_formula(S,S1),
31 setval(actions,0),
32 set_state(S1),
33 set_sit(s0).
34
35%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
36%% %%
37%% Store States and Situations %%
38%% %%
39%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
40
41:-local reference(state).
42:-local variable(sit).
43
44state(State) :-
45 getval(state,State).
46
47set_state(NewState) :-
48 setval(state,NewState).
49
50sit(Sit) :-
51 getval(sit,Sit).
52
53set_sit(Action) :-
54 getval(sit,Sit),
55 setval(sit,did(Action,Sit)).
56
57
58
68
69
75
76normalize_formula(FormulaIn,FormulaOut) :-
77 split_clauses(FormulaIn,Units,Clauses),
78 ( foreach(Clause,Clauses),
79 foreach(Clause1,Clauses1) do
80 sort(Clause,Clause1) ),
81 sort(Clauses1,Clauses2),
82 sort(Units,Units1),
83 append(Units1,Clauses2,FormulaOut).
84
90
91negate_literal(Lit,Neg) :-
92 ( Lit = neg(Atom) ->
93 Neg = Atom
94 ;
95 Neg = neg(Lit) ).
96
102
103tautology(Clause) :-
104 ( restmember(Lit,Clause,Rest),
105 negate_literal(Lit,Neg),
106 omemberchk(Neg,Rest) ->
107 true
108 ;
109 fail ).
110
116
117primpls_to_primpls(PI1,PI2,PI) :-
118
119 split_clauses(PI1,U1,C1),
120 split_clauses(PI2,U2,C2),
121
122 append(U1,U2,U3),
123 sort(U3,U),
124 setval(current_units,U),
125
126 remove_clauses_subsumed_by_units(C1,U2,C3),
127 remove_clauses_subsumed_by_units(C2,U1,C4),
128
129 append(C3,C4,C5),
130 sort(C5,C),
131 setval(current_clauses,C),
132
133 resolve_units_clauses(U2,C3,NU1,NC1),
134 resolve_units_clauses(U1,C4,NU2,NC2),
135
136 append(NU1,NU2,NU3),
137 append(NU3,U,U4),
138 sort(U4,NU),
139 setval(current_units,NU),
140
141 remove_clauses_subsumed_by_units(NC1,NU,NC3),
142 remove_clauses_subsumed_by_units(NC2,NU,NC4),
143
144 remove_subsumed_clauses(NC3,NC4,NC5),
145 getval(current_clauses,NC6),
146 append(NC5,NC6,NC7),
147 sort(NC7,NC),
148
149 clause_set_to_prime_implicates(NU,NC,PI).
150
151
152
153clause_set_to_prime_implicates([],[],PIs) :-
154 !,
155 getval(current_units,Units),
156 getval(current_clauses,Clauses),
157 append(Units,Clauses,PIs).
158
159
160clause_set_to_prime_implicates(Units,Clauses,PIs) :-
161
162 getval(current_clauses,Clauses1),
163
164 resolve_units_clauses(Units,Clauses,NU1,NC1),
165
166 resolve_units_clauses(Units,Clauses1,NU2,NC2),
167
168 resolve_all_clauses(Clauses,NU3,NC3),
169
170 resolve_all_clauses(Clauses,Clauses1,NU4,NC4),
171
172 append(NU1,NU2,NU5),
173 append(NU3,NU4,NU6),
174 append(NU5,NU6,NU),
175
176 append(NC1,NC2,NC5),
177 append(NC3,NC4,NC6),
178 append(NC5,NC6,NC),
179
180 clause_set_to_prime_implicates(NU,NC,PIs).
181
182
183
184
185
191
192remove_subsumed_clauses(C1,C2,C) :-
193 ( foreach(C,C1),
194 fromto(C3,Out,In,[]),
195 param(C2) do
196 ( member(D,C2),
197 subset(D,C) ->
198 Out = In
199 ;
200 Out = [C|In] ) ),
201
202 ( foreach(E,C2),
203 fromto(C4,Out,In,[]),
204 param(C3) do
205 ( member(F,C3),
206 subset(F,E) ->
207 Out = In
208 ;
209 Out = [E|In] ) ),
210
211 append(C3,C4,C5),
212 sort(C5,C).
213
214
215
221
222resolve_units_clauses([],_Clauses,[],[]) :-
223 !.
224
225resolve_units_clauses(_Units,[],[],[]) :-
226 !.
227
228resolve_units_clauses(Units,Clauses,NewUnits,NewClauses) :-
229 resolve_units_clauses1(Units,Clauses,[],NewUnits1,NewClauses1),
230 sort(NewUnits1,NewUnits),
231 sort(NewClauses1,NewClauses).
232
233
234resolve_units_clauses1([Unit],Clauses,KeptUnits,NewUnits,NewClauses) :-
235 !,
236 ( foreach(Clause,Clauses),
237 fromto(NewUnits1,Out1,In1,[]),
238 fromto(NewClauses,Out2,In2,[]),
239 param(Unit) do
240 ( resolve_unit_clause(Unit,Clause,NewClause) ->
241 ( NewClause = [Single] ->
242 Out1 = [Single|In1],
243 Out2 = In2
244 ;
245 Out1 = In1,
246 Out2 = [NewClause|In2] )
247 ;
248 Out1 = In1,
249 Out2 = [Clause|In2] ) ),
250 append(NewUnits1,KeptUnits,NewUnits).
251
252
253resolve_units_clauses1([Unit|Units],Clauses,KeptUnits,NewUnits,NewClauses) :-
254 ( foreach(Clause,Clauses),
255 fromto(NewUnits1,Out1,In1,[]),
256 fromto(NewClauses1,Out2,In2,[]),
257 param(Unit) do
258 ( resolve_unit_clause(Unit,Clause,NewClause) ->
259 ( NewClause = [Single] ->
260 Out1 = [Single|In1],
261 Out2 = In2
262 ;
263 Out1 = In1,
264 Out2 = [NewClause|In2] )
265 ;
266 Out1 = In1,
267 Out2 = [Clause|In2] ) ),
268 append(NewUnits1,KeptUnits,KeptUnits1),
269 resolve_units_clauses1(Units,NewClauses1,KeptUnits1,NewUnits,NewClauses).
270
271
272resolve_unit_clause(Unit,Clause,NewClause) :-
273 negate_literal(Unit,Neg),
274 orestmemberchk(Neg,Clause,NewClause1),
275
276 reduce(NewClause1,NewClause2),
277
278 ( NewClause2 = [] ->
279 fail
280 ;
281 NewClause2 = NewClause ).
282
283
284
285
291
292
293reduce(C1,C2) :-
294
295 getval(current_units,U),
296 getval(current_clauses,C),
297
298 ( C1 = [Single] ->
299 ( memberchk(Single,U) ->
300 C2 = []
301 ;
302 remove_clauses_subsumed_by_units(C,C1,NC),
303 append(C1,U,NU1),
304 sort(NU1,NU),
305 setval(current_units,NU),
306 setval(current_clauses,NC),
307 C2 = C1)
308 ;
309 ( tautology(C1) ->
310 C2 = []
311 ;
312 append(U,C,Cs),
313 ( holds(Cs,[C1]) ->
314 C2 = []
315 ;
316 ( foreach(D,C),
317 fromto(NC,Out,In,[]),
318 param(C1) do
319 ( subset(C1,D) ->
320 Out = In
321 ;
322 Out = [D|In] ) ),
323 append([C1],NC,NC1),
324 sort(NC1,NC2),
325 setval(current_clauses,NC2),
326 C2 = C1 ) ) ).
327
328
329
338resolve_all_clauses([],_Clauses,[],[]) :-
339 !.
340
341resolve_all_clauses(_Clauses,[],[],[]) :-
342 !.
343
344resolve_all_clauses(ClauseSet1,ClauseSet2,NewUnits,NewClauses) :-
345 cartesian(ClauseSet1,ClauseSet2,Pairs),
346 ( foreach(Clause1-Clause2,Pairs),
347 fromto([],In1,Out1,NewUnits2),
348 fromto([],In2,Out2,NewClauses2) do
349 resolve_all_clauses([Clause1,Clause2],NewUnits1,
350 NewClauses1),
351 append(NewUnits1,In1,Out1),
352 append(NewClauses1,In2,Out2) ),
353 sort(NewUnits2,NewUnits),
354 sort(NewClauses2,NewClauses).
359resolve_all_clauses([],[],[]) :-
360 !.
361
362resolve_all_clauses([_Single],[],[]) :-
363 !.
364
365resolve_all_clauses([Clause1,Clause2],NewUnits,NewClauses) :-
366 !,
367 resolve_clause_all_clauses(Clause1,[Clause2],NewUnits,NewClauses).
368
369resolve_all_clauses(Clauses,NewUnits,NewClauses) :-
370 restmemberchk(Clause,Clauses,Rest),
371 resolve_clause_all_clauses(Clause,Rest,NewUnits1,NewClauses1),
372 resolve_all_clauses(Rest,NewUnits2,NewClauses2),
373 append(NewUnits1,NewUnits2,NewUnits),
374 append(NewClauses1,NewClauses2,NewClauses).
375
376resolve_clause_all_clauses(Clause1,[Clause2],NewUnits,NewClauses) :-
377
378 !,
379
380 ( resolve_clauses(Clause1,Clause2,Resolvent) ->
381
382 ( Resolvent = [_Single] ->
383 NewUnits = Resolvent,
384 NewClauses = []
385 ;
386 NewUnits = [],
387 NewClauses = [Resolvent] )
388
389 ;
390
391 NewUnits = [],
392 NewClauses = [] ).
393
394
395resolve_clause_all_clauses(Clause1,[Clause2|Clauses],NewUnits,NewClauses) :-
396
397 ( resolve_clauses(Clause1,Clause2,Resolvent) ->
398
399 ( Resolvent = [Single] ->
400 NewUnits = [Single|NewUnits1],
401 NewClauses = NewClauses1
402 ;
403 NewUnits = NewUnits1,
404 NewClauses = [Resolvent|NewClauses1] )
405 ;
406 NewUnits = NewUnits1,
407 NewClauses = NewClauses1 ),
408
409 resolve_clause_all_clauses(Clause1,Clauses,NewUnits1,NewClauses1).
410
411resolve_clauses(Clause1,Clause2,NewClause) :-
412 restmember(Lit1,Clause1,Rest1),
413 negate_literal(Lit1,Neg),
414 restmember(Neg,Clause2,Rest2),
415 append(Rest1,Rest2,NewClause1),
416 sort(NewClause1,NewClause2),
417 reduce(NewClause2,NewClause3),
418 ( NewClause3 = [] ->
419 fail
420 ;
421 NewClause = NewClause2 ).
422
428
429remove_clauses_subsumed_by_units([Clause|Clauses],Units,Clauses1) :-
430 member(Lit,Clause),
431 omemberchk(Lit,Units),
432 !,
433 remove_clauses_subsumed_by_units(Clauses,Units,Clauses1).
434
435
436remove_clauses_subsumed_by_units([Clause|Clauses],Units,[Clause|Clauses1]) :-
437 !,
438 remove_clauses_subsumed_by_units(Clauses,Units,Clauses1).
439
440remove_clauses_subsumed_by_units([],_,[]).
448split_clauses([El|Rest],[El|Units],Clauses) :-
449 El \= .(_,_),
450 !,
451 split_clauses(Rest,Units,Clauses).
452
453split_clauses([],[],[]) :-
454 !.
455
456split_clauses([El|Rest],[],[El|Rest]) :-
457 El = .(_,_).
458
459
460
470
476
477execute(Action) :-
478 action(Action,Pre,Eff),
479 holds(Pre),
480 update(Eff),
481 set_sit(Action).
482
483update(Update) :-
484 state(State),
485 update(State,Update,NewState),
486 !,
487 set_state(NewState).
488
489update(State,Update,NewState) :-
490 ( foreach(El,State),
491 fromto(NewState1,Out,In,[]),
492 param(Update) do
493 ( El = .(_,_) ->
494 ( affected_clause(El,Update) ->
495 Out = In
496 ;
497 Out = [El|In] )
498 ;
499 ( affected_literal(El,Update) ->
500 Out = In
501 ;
502 Out = [El|In] ) ) ),
503 append(Update,NewState1,NewState2),
504 normalize_formula(NewState2,NewState).
505
506
507affected_literal(El,Update) :-
508 ( memberchk(El,Update) ->
509 true
510 ;
511 ( negate_literal(El,Neg),
512 memberchk(Neg,Update) ->
513 true
514 ;
515 false ) ).
516
517affected_clause(Clause,Update) :-
518 ( member(El,Clause),
519 affected_literal(El,Update) ->
520 true
521 ;
522 false ).
523
524
534
540
541holds(Formula) :-
542 ( Formula = [Lit],
543 sensor(Lit) ->
544 sense(Lit)
545 ;
546 state(State),
547 normalize_formula(Formula,Formula1),
548 holds(State,Formula1) ).
549
550holds(State,Formula) :-
551 ( ground(Formula) ->
552 ground_holds(State,Formula)
553 ;
554 instantiate(State,Formula) ).
555
561
562ground_holds(State,Formula) :-
563 ( foreach(El,Formula),
564 param(State) do
565 ( El = .(_,_) ->
566 ground_holds_clause(State,El)
567 ;
568 ground_holds_literal(State,El) ) ).
569
570ground_holds_literal(State,Lit) :-
571 ( aux1(Lit) ->
572 Lit
573 ;
574 memberchk(Lit,State) ).
575
576ground_holds_clause(State,Clause) :-
577 aux_fluent(Clause,Aux,Fluent),
578 ( member(Lit,Aux),
579 Lit ->
580 true
581 ;
582 ( member(Lit,Fluent),
583 omemberchk(Lit,State) ->
584 true
585 ;
586 ( member(El,State),
587 El = .(_,_),
588 subset(Fluent,El) ->
589 true
590 ;
591 false ) ) ).
592
593
603instantiate(State,Formula) :-
604 ( foreach(El,Formula),
605 param(State) do
606 ( El = .(_,_) ->
607 instantiate_clause(State,El)
608 ;
609 instantiate_literal(State,El) ) ).
610
611instantiate_literal(State,Lit) :-
612 ( aux1(Lit) ->
613 Lit
614 ;
615 member(Lit,State) ).
616
617instantiate_clause(State,Clause) :-
618 aux_fluent(Clause,Aux,Fluent),
619 i1(Aux,Fluent,State).
620
621i1(Aux,_Fluent,_State) :-
622 member(Lit,Aux),
623 Lit.
624
625i1(_Aux,Fluent,State) :-
626 member(Lit,Fluent),
627 member(Lit,State).
628
629i1(_Aux,Fluent,State) :-
630 member(El,State),
631 El = .(_,_),
632 subset(Fluent,El).
633
634
640
641aux_fluent(Clause,Aux,Fluent) :-
642 ( foreach(Lit,Clause),
643 fromto(Aux,Out1,In1,[]),
644 fromto(Fluent,Out2,In2,[]) do
645 ( aux1(Lit) ->
646 Out1 = [Lit|In1],
647 Out2 = In2
648 ;
649 Out1 = In1,
650 Out2 = [Lit|In2] ) ).
651
657
658
659aux1(Lit) :-
660 Lit =.. [P|_],
661 aux(Aux),
662 memberchk(P,Aux).
663
664sensor(Lit) :-
665 sensors(Sensors),
666 Lit =.. [P|_],
667 memberchk(P,Sensors).
668
669
679
685
686sense(Lit) :-
687 sensor_axiom(Lit,Vals),
688 sense_val(Lit,Assig),
689 memberchk(Assig-Index-Meaning,Vals),
690 ( Index = [] ->
691 ( foreach(Var-Val,Assig) do
692 Var = Val ),
693 state(State),
694 primpls_to_primpls(State,Meaning,PIs),
695 set_state(PIs)
696 ;
697 holds(Index),
698 ( foreach(Var-Val,Assig) do
699 Var = Val ),
700 state(State),
701 primpls_to_primpls(State,Meaning,PIs),
702 !,
703 set_state(PIs) ).
704
705
706sense_val(Lit,Assig) :-
707 real_world(World),
708 ( Lit = glitter(X) ->
709 holds([at(agent,Y)]),
710 ( memberchk(at(gold,Y),World) ->
711 Assig = [X-true]
712 ;
713 Assig = [X-false] )
714 ;
715 ( Lit = breeze(X) ->
716 holds([at(agent,Y)]),
717 ( adjacent(Y,Z),
718 memberchk(pit(Z),World) ->
719 Assig = [X-true]
720 ;
721 Assig = [X-false] )
722 ;
723 Lit = stench(X),
724 holds([at(agent,Y)]),
725 ( adjacent(Y,Z),
726 memberchk(at(wumpus,Z),World) ->
727 Assig = [X-true]
728 ;
729 Assig = [X-false] ) ) ).
730
740
746
747restmemberchk(H,[H|T],T) :- !.
748restmemberchk(H,[H1|T],[H1|T1]) :-
749 restmemberchk(H,T,T1).
750
751restmember(H,[H|T],T) :-
752 (T = [] ->
753 !
754 ;
755 true ).
756restmember(H,[H1|T],[H1|T1]) :-
757 restmember(H,T,T1).
758
759
765
766orestmemberchk(H,[H|T],T) :- !.
767orestmemberchk(H,[H1|T],[H1|T1]) :-
768 ( H1 @< H ->
769 orestmemberchk(H,T,T1)
770 ;
771 fail ).
772
773orestmember(H,[H|T],T) :-
774 !.
775orestmember(H,[H1|T],[H1|T1]) :-
776 ground(H),
777 !,
778 ( H1 @< H ->
779 orestmember(H,T,T1)
780 ;
781 fail).
782orestmember(in(X,CR1),[in(Is,CR2)|T],[in(Is,CR2)|T1]) :-
783 ( CR2 @< CR1 ->
784 orestmember(in(X,CR1),T,T1)
785 ;
786 fail ).
787
788
794
795omemberchk(H,[H|_T]) :- !.
796omemberchk(H,[H1|T]) :-
797 ( H1 @< H ->
798 omemberchk(H,T)
799 ;
800 fail ).
801
802omember(H,[H|_T]) :-
803 !.
804omember(H,[H1|T]) :-
805 ground(H),
806 !,
807 ( H1 @< H ->
808 omember(H,T)
809 ;
810 fail).
811omember(in(X,CR1),[in(_Is,CR2)|T]) :-
812 ( CR2 @< CR1 ->
813 omember(in(X,CR1),T)
814 ;
815 fail ).
816
817
823
824cartesian(L,K,Res):-
825 (foreach(X,L),
826 fromto([],In,Out,Res),
827 param(K) do
828 (foreach(Y,K),
829 fromto(In,In1,[X-Y|In1],Out),
830 param(X) do
831 true ))