21
23
24:-op(500,xfy,--). 25:-op(359,xf,ject). 26
27write_tree(T):-
28 numbervars80(T,1,_),
29 wt(T,0),
30 fail.
31write_tree(_).
32
33wt(T,D):- tab(D),fmt(T),!.
34
35wt((P:-Q),L) :- !, L1 is L+3,
36 write(P), tab(1), write((:-)), nl,
37 tab(L1), wt(Q,L1).
38wt((P,Q),L) :- !, L1 is L-2,
39 wt(P,L), nl,
40 tab(L1), put("&"), tab(1), wt(Q,L).
41wt({P},L) :- complex(P), !, L1 is L+2,
42 put("{"), tab(1), wt(P,L1), tab(1), put("}").
43wt(E,L) :- decomp(E,H,P), !, L1 is L+2,
44 header80(H), nl,
45 tab(L1), wt(P,L1).
46wt(E,_) :- write(E).
47
([]).
49header80([X|H]) :- reply(X), tab(1), header80(H).
50
51decomp(setof(X,P,S),[S,=,setof,X],P).
52decomp(\+(P),[\+],P) :- complex(P).
53decomp(numberof(X,P,N),[N,=,numberof,X],P).
54decomp(X^P,[exists,X|XX],P1) :- othervars(P,XX,P1).
55
56othervars(X^P,[X|XX],P1) :- !, othervars(P,XX,P1).
57othervars(P,[],P).
58
59complex((_,_)).
60complex({_}).
61complex(setof(_,_,_)).
62complex(numberof(_,_,_)).
63complex(_^_).
64complex(\+P) :- complex(P).
65
67
68respond([]) :- reply('Nothing satisfies your question.'), nl.
69respond([A|L]) :- reply(A), replies(L).
70
71answer80(S1):- answer802(S1,S),respond(S).
72
73answer802((answer80([]):-E),[B]) :- !, holds_truthvalue(E,B).
74answer802((answer80([X]):-E),S) :- !, seto(X,E,S).
75answer802((answer80(X):-E),S) :- seto(X,E,S).
76
77seto(X,E,S) :- setof(X,satisfy(E),S), !.
78seto(_X,_E,[]).
79
80holds_truthvalue(E,true) :- satisfy(E), !.
81holds_truthvalue(_E,false).
82
83yesno(true):-reply(' Yes. ').
84yesno(false):-reply(' No.').
85
86replies([]) :- reply('.').
87replies([A]) :- reply(' and '), reply(A), reply('.').
88replies([A|X]) :- reply(', '), reply(A), replies(X).
89
90reply(N--U) :- !, write(N), write(' '), write(U).
91reply(X) :- write(X).
92
93satisfy((P,Q)) :- !, satisfy(P), satisfy(Q).
94satisfy((P;Q)) :- !, satisfy(P) ; satisfy(Q).
97satisfy({P}) :- !, satisfy(P), !.
98satisfy(_X^P) :- !, satisfy(P).
99satisfy(\+P) :- satisfy(P), !, fail.
100satisfy(\+_P) :- !.
101satisfy(setof(X,P,S)) :- !, setof(X,satisfy(P),S).
102satisfy(numberof(X,P,N)) :- !, numberof(X,P,N).
103satisfy(X<Y) :- !, X<Y.
104satisfy(X=<Y) :- !, X=<Y.
105satisfy(X>=Y) :- !, X>=Y.
106satisfy(X>Y) :- !, X>Y.
107satisfy(P) :- call_u(P).
108
109
110^(_X,P) :- !, satisfy(P).
111
112+P :-!, satisfy_0(+P).
113
114satisfy_0(+P) :- exceptionto(P), !, fail.
115satisfy_0(+_P) :- !.
116
117numberof(X,P,N) :- setof(X,satisfy(P),S), length(S,N).
118
119exceptionto(P) :-
120 functor(P,F,N), functor(P1,F,N),
121 pickargs(N,P,P1),
122 exception(P1).
123
124exception(P) :- P, !, fail.
125exception(_P).
126
127pickargs(0,_,_) :- !.
128pickargs(N,P,P1) :- N1 is N-1,
129 arg(N,P,S),
130 pick(S,X),
131 arg(N,P1,X),
132 pickargs(N1,P,P1).
133
134pick([X|_S],X).
135pick([_|S],X) :- !, pick(S,X).
136pick([],_) :- !, fail.
137pick(X,X)