22
24
25:-public write_tree/1, answer/1. 26
27:-mode write_tree(+). 28:-mode wt(+,+). 29:-mode header(+). 30:-mode decomp(+,-,-). 31:-mode complex(+). 32:-mode othervars(+,-,-). 33
34write_tree(T):-
35 numbervars(T,0,_),
36 wt(T,0),
37 fail.
38write_tree(_).
39
40wt((P:-Q),L) :- !, L1 is L+3,
41 write(P), tab(1), write((:-)), nl,
42 tab(L1), wt(Q,L1).
43wt((P,Q),L) :- !, L1 is L-2,
44 wt(P,L), nl,
45 tab(L1), put("&"), tab(1), wt(Q,L).
46wt({P},L) :- complex(P), !, L1 is L+2,
47 put("{"), tab(1), wt(P,L1), tab(1), put("}").
48wt(E,L) :- decomp(E,H,P), !, L1 is L+2,
49 header(H), nl,
50 tab(L1), wt(P,L1).
51wt(E,_) :- write(E).
52
([]).
54header([X|H]) :- write(X), tab(1), header(H).
55
56decomp(setof(X,P,S),[S,=,setof,X],P).
57decomp(\+(P),[\+],P) :- complex(P).
58decomp(numberof(X,P,N),[N,=,numberof,X],P).
59decomp(X^P,[exists,X|XX],P1) :- othervars(P,XX,P1).
60
61othervars(X^P,[X|XX],P1) :- !, othervars(P,XX,P1).
62othervars(P,[],P).
63
64complex((_,_)).
65complex({_}).
66complex(setof(_,_,_)).
67complex(numberof(_,_,_)).
68complex(_^_).
69complex(\+P) :- complex(P).
70
72
73:-mode respond(?). 74:-mode holds(+,?). 75:-mode answer(+). 76:-mode yesno(+). :-mode replies(+). 77:-mode reply(+). 78:-mode seto(?,+,-). 79:-mode satisfy(+). 80:-mode pickargs(+,+,+). 81:-mode pick(+,?). 82
83respond([]) :- display('Nothing satisfies your question.'), nl.
84respond([A|L]) :- reply(A), replies(L).
85
86answer((answer([]):-E)) :- !, holds(E,B), yesno(B).
87answer((answer([X]):-E)) :- !, seto(X,E,S), respond(S).
88answer((answer(X):-E)) :- seto(X,E,S), respond(S).
89
90seto(X,E,S) :-
92 phrase(satisfy(E,G),Vars),
94 ( setof(X,Vars^G,S)
95 -> true
96 ; S = []
97 ).
98
99holds(E,True) :-
100 phrase(satisfy(E, G), _),
101 ( G
102 -> True = true
103 ; True = false
104 ).
105
106yesno(true) :- display('Yes.').
107yesno(false) :- display('No.').
108
109replies([]) :- display('.').
110replies([A]) :- display(' and '), reply(A), display('.').
111replies([A|X]) :- display(', '), reply(A), replies(X).
112
113reply(N--U) :- !, write(N), display(' '), write(U).
114reply(X) :- write(X).
123satisfy((P0,Q0), (P,Q)) --> !, satisfy(P0, P), satisfy(Q0, Q).
124satisfy({P0}, (P->true)) --> !, satisfy(P0, P).
125satisfy(X^P0, P) --> !, satisfy(P0, P), [X].
126satisfy(\+P0, \+P) --> !, satisfy(P0, P).
127satisfy(numberof(X,P0,N), (setof(X,Vars^P,S),length(S,N))) --> !,
128 { phrase(satisfy(P0,P),Vars) },
129 [S], Vars. 130satisfy(setof(X,P0,S), setof(X,Vars^P,S)) --> !,
131 { phrase(satisfy(P0,P),Vars) },
132 Vars.
133satisfy(+P0, \+ exceptionto(P)) --> !,
134 satisfy(P0, P).
135satisfy(X<Y, X<Y) --> !.
136satisfy(X=<Y, X=<Y) --> !.
137satisfy(X>=Y, X>=Y) --> !.
138satisfy(X>Y, X>Y) --> !.
139satisfy(P, database(P)) --> [].
140
141exceptionto(P) :-
142 functor(P,F,N), functor(P1,F,N),
143 pickargs(N,P,P1),
144 exception(P1).
145
146exception(P) :- database(P), !, fail.
147exception(_P).
148
149pickargs(0,_,_) :- !.
150pickargs(N,P,P1) :- N1 is N-1,
151 arg(N,P,S),
152 pick(S,X),
153 arg(N,P1,X),
154 pickargs(N1,P,P1).
155
156pick([X|_],X).
157pick([_|S],X) :- !, pick(S,X).
158pick([],_) :- !, fail.
159pick(X,X)