3
4cilog_version('0.14').
5
9
14
30get_runtime(T,U) :- catch((statistics(cputime,T),U=secs),_,
31 (statistics(runtime,[T,_]),U=ms)). 32
33
36mywhen(C,G) :-
37 C -> G
38 ; writeallonline(['Warning: ',C,' failing. Delaying not implemented.']),
39 fail.
40
43
44differ(X,Y) :- dif(X,Y). 46
47mywrite(T) :- write_term(T,[numbervars(true),portray(true)]). 48mywrite(T) :- write(T). 49
56
58:- op(1150, xfx, <- ). 61:- op(1120, xfx, <= ). 63:- op(950,xfy, &). 65:- op(900,fy,~). 67:- op(700,xfx,\=). 68
69:- op(1170, fx, tell). 70:- op(1170, fx, ask). 71:- op(1170, fx, whynot). 72:- op(1170, fx, how). 73:- op(1170,fx,load). 74:- op(1170,fx,prload). 75:- op(1170,fx,bound). 76:- op(1170,fx,stats). 77:- op(1170,fx,listing). 78:- op(1170,fx,clear). 79:- op(1170,fx,askable). 80:- op(1170,fx,assumable). 81:- op(1170,fx,deterministic). 82
83:- dynamic (<-)/2. 84:- dynamic failed/1. 85:- dynamic depth_bound/1. 86:- dynamic askabl/1. 87:- dynamic assumabl/1. 88:- dynamic asked/2. 89:- dynamic debugging_failure/0. 90:- dynamic answer_found/0. 91:- dynamic checking_runtime/0. 92:- dynamic lastruntime/1. 93:- dynamic deter/1. 94
95depth_bound(30).
96
100
101help_message(['
102CILOG Help','
103
104A clause is of the form','
105 Head <- Body','
106 Head','
107Head is an atom.','
108Body is an expression made up of','
109 Atom','
110 ~ B1 negation as finite failure','
111 B1 & B2 conjunction B1 and B2','
112where B1 and B2 are expressions.','
113 bagof(A,Q,L) true if L is the list of A''s where Q is true.','
114
115***** Basic commands:','
116
117tell CLAUSE. add the clause to the knowledge base','
118askable Atom. makes Atom askable.','
119assumable Atom. makes atom assumable.','
120
121ask QUERY. ask if expression QUERY is a consequence of the KB','
122whynot QUERY. find out why QEURY failed.','
123
124bound N. set search depth-bound to N (default=30)','
125listing. list all clauses in the knowledge base.','
126listing H. list clauses in the knowledge base with head H.','
127askables. list all askables.','
128assumables. list all assumables.','
129clear. clear the knowledge base','
130check. check the knowledge base for undefined predicates','
131clear H. clear clauses with head H from knowledge base','
132help. print this help message','
133stats runtime. give runtime statistics','
134quit. quit cilog','
135prolog. exit to Prolog. Type "start." to start cilog again.','
136
137***** Input/Output','
138
139load ''Filename''. load the clauses in file Filename','
140prload ''Filename''. load the clauses in Filename, using Prolog''s syntax.']).
141
145
146interpret(help) :- !,
147 help_message(Help),
148 writeallonline(Help).
149
150interpret((tell _ :- _)) :- !,
151 writeallonline(['Illegal rule: ":-" is not a legal implication. Use "<-".']).
152interpret((tell C)) :- !,
153 tell_clause(C).
154
155interpret((ask Q)) :- !,
156 retractall(debugging_failure),
157 retractall(answer_found),
158 depth_bound(DB),
159 askq(Q,DB).
160
161interpret((whynot Q)) :- !,
162 depth_bound(DB),
163 whynotb(Q,DB,_,[],_).
164
165interpret((clear H)) :- !,
166 retractall((H <- _)),
167 retractall(assumabl(H)),
168 retractall(askabl(H)),
169 retractall(asked(H,_)).
170
171interpret((stats Cmd)) :- !,
172 stats_command(Cmd).
173
174interpret(clear) :- !,
175 interpret((clear _)).
176
177interpret((prload File)) :- !,
178 prolog_load(File).
179
180interpret((load File)) :- !,
181 ci_load(File).
182
183interpret((bound)) :- !,
184 depth_bound(N),
185 writeallonline(['Current depth bound is ',N]).
186
187interpret((bound N)) :- !,
188 (integer(N) ->
189 retract(depth_bound(_)),
190 asserta(depth_bound(N))
191 ; writeallonline(['Depth bound must be an integer'])).
192
193interpret(quit) :-
194 throw(quit).
195
196interpret(check) :- !,
197 check.
198
199interpret((askable G)) :- !,
200 assertz(askabl(G)).
201
202interpret((assumable G)) :- !,
203 assertz(assumabl(G)).
204
205interpret((deterministic G)) :- !,
206 assertz(deter(G)).
207
208interpret(askables) :-
209 askabl(G),
210 writeallonline(['askable ',G,'.']),
211 fail.
212interpret(askables) :- !.
213
214interpret(assumables) :-
215 assumabl(G),
216 writeallonline(['assumable ',G,'.']),
217 fail.
218interpret(assumables) :- !.
219
220interpret((listing)) :- !,
221 interpret((listing _)),
222 interpret(askables),
223 interpret(assumables).
224
225interpret((listing H)) :-
226 (H <- B),
227 (B = true
228 -> writeallonline([H,'.'])
229 ; writeallonline([H,' <- ',B,'.'])
230 ),
231 fail.
232interpret((listing _)) :- !.
233
234interpret((A <- B)) :- !,
235 writeallonline(['Illegal command, ',(A <- B),'. You have to "tell" a clause.']).
236
237interpret(C) :-
238 writeallonline(['Unknown Command, ',C,'. Type "help." for help.']).
239
240
244
245askq(Q,_) :-
246 illegal_body(Q,Why),!,
247 writeallonline(['Illegal query: '|Why]).
248askq(Q,DB) :-
249 retractall(failed(_)),
250 assert(failed(naturally)),
251 reset_runtime,
252 solve(Q,DB,Res,[wrule(yes,true,Q,true)],[],Ass),
253 (answer_found -> true ; assert(answer_found)),
255 report(Q,Res,Ass).
256askq(Q,_) :-
257 failed(naturally),!,
258 (answer_found
259 -> writeallonline(['No more answers.'])
260 ; writeallonline(['No. ',Q,' doesn''t follow from the knowledge base.'])),
261 report_runtime.
262askq(Q,DB) :- !,
263 ask_failing(Q,DB).
264
265ask_failing(Q,DB) :-
266 writeallonline(['Query failed due to depth-bound ',DB,'.']),
267 report_runtime,
268 writel([' [New-depth-bound,where,ok,help]: ']),
269 flush_and_read(Comm),
270 interpret_failing_question(Comm,Q,DB).
271
273interpret_failing_question(help,Q,DB) :- !,
274 writeallonline([
275 ' Give one of the following commands:',nl,
276 ' an integer > ',DB,' to use this depth bound.',nl,
277 ' (use "bound N." to set it permanently).',nl,
278 ' where. to explore the proof tree where the depth-bound was reached.',nl,
279 ' ok. to return to the cilog prompt.',nl,
280 ' help. to print this message.']),
281 ask_failing(Q,DB).
282interpret_failing_question(end_of_file,_,_) :- !.
283interpret_failing_question(ok,_,_) :- !.
284interpret_failing_question(where,Q,DB) :-
285 assert(debugging_failure),
286 askq(Q,DB).
287interpret_failing_question(Comm,Q,_) :-
288 integer(Comm),!,
289 askq(Q,Comm).
290interpret_failing_question(Comm,Q,DB) :-
291 writeallonline([' Unknown command, ',Comm,' type "help." for help.']),
292 ask_failing(Q,DB).
293
297
298tell_clause((~ H <- B)) :- !,
299 writeallonline(['Illegal rule: ~',H,' <- ',B,'.',nl,
300 'You cannot have negation in the head of a clause.']).
301tell_clause((H1 & H2 <- B)) :- !,
302 writeallonline(['Illegal rule: ',H1 & H2,' <- ',B,'.',nl,
303 'You cannot have a conjunction in the head of a clause.']).
304tell_clause((H1 , H2 <- B)) :- !,
305 writeallonline(['Illegal rule: ',H1 ,',', H2,' <- ',B,'.',nl,
306 'You cannot have a "," in the head of a clause.']).
307tell_clause((H <- B)) :-
308 !,
309 ( builtin(H,_) ->
310 writeallonline([H,' is built-in. It cannot be redefined.'])
311 ; illegal_body(B,Why) ->
312 writeallonline(['Illegal rule: ',H,'<-',B,'. '|Why])
313 ; assertz((H <- B))).
314tell_clause((H :- B)) :-
315 !,
316 writeallonline(['Illegal rule: ',H,':-',B,'. ":-" is not a legal implication. Use "<-".']).
317tell_clause((A, B)) :-
318 !,
319 writeallonline(['Error: ',(A,B),' is not a valid clause.']).
320tell_clause((A & B)) :-
321 !,
322 writeallonline(['Error: ',(A&B),' is not a valid clause.']).
323tell_clause((~A)) :-
324 !,
325 writeallonline(['Error: ',~A,' is not a valid clause.']).
326tell_clause(H) :-
327 builtin(H,_),!,
328 writeallonline([H,' is built-in. It cannot be redefined.']).
329tell_clause(H) :-
330 !,
331 assertz((H <- true)).
332
333illegal_body(X,['Variables cannot be atoms. Use call(',X,').']) :- var(X).
334illegal_body((_,_),[' "," is not a legal conjunction. Use "&".']).
335illegal_body((\+ _),[' "\\+" is not a legal negation. Use "~".']).
336illegal_body(!,[' "!" is not supported.']).
337illegal_body([_|_],[' Lists cannot be atoms.']).
338
339illegal_body((A&_),Why) :-
340 illegal_body(A,Why).
341illegal_body((_&A),Why) :-
342 illegal_body(A,Why).
343illegal_body((A;_),Why) :-
344 illegal_body(A,Why).
345illegal_body((_;A),Why) :-
346 illegal_body(A,Why).
347illegal_body((~A),Why) :-
348 illegal_body(A,Why).
349
353
357solve(true,_,true,_,Ass,Ass) :- !.
358solve((A&B),N,(AT&BT),[wrule(H,LT,_,RB)|WT],A0,A2) :- !,
359 solve(A,N,AT,[wrule(H,LT,A,(B&RB))|WT],A0,A1),
360 solve(B,N,BT,[wrule(H,(LT&AT),B,RB)|WT],A1,A2).
361solve(A \= B,_,if(A \= B,builtin),_,A0,A0) :- !,
362 differ(A,B).
363solve(call(G),_,_,WT,_,_) :-
364 var(G),!,
365 writeallonline(['Error: the argument to call must be bound when evaluated.']),
366 why_question(WT,_),
367 writeallonline(['Failing the call with unbound argument.']),!,
368 fail.
369solve(call(G),N,T,WT,A0,A1) :- !,
370 solve(G,N,T,WT,A0,A1).
371solve((~ G),N,if(~G,naf),WT,A0,A0) :- !,
372 mywhen( ground(G), failtoprove(G,N,WT)).
373solve(bagof(E,Q,L),N,BagTrees,WT,A0,A1) :- !,
374 solvebag(bagof(E,Q,L),N,BagTrees,WT,A0,A1).
375solve(G,_,if(G,assumed),_,A0,A1) :-
376 assumabl(G),
377 insert(G,A0,A1).
378solve(G,_,if(G,asked),WT,A0,A0) :-
379 askabl(G),
380 ask_user(G,WT,Ans),
381 Ans \== unknown,!, 382 Ans=yes.
383solve(H,_,if(H,builtin),WT,A0,A0) :-
384 builtin(H,C),!,
385 (C -> catch(H,_,debugging_builtin_error(H,WT))
386 ; writeallonline(['Error: "',H,'" can''t be called in this form, as ',C,' isn''t true.']),
387 debugging_builtin_error(H,WT)
388 ).
389solve(H,N0,if(H,BT),WT,A0,A1) :-
390 N0 > 0,
391 deter(H),
392 N1 is N0-1,
393 (H <- B),
394 solve(B,N1,BT,[wrule(H,true,B,true)|WT],A0,A1), !.
395solve(H,N0,if(H,BT),WT,A0,A1) :-
396 N0 > 0,
397 N1 is N0-1,
398 (H <- B),
399 solve(B,N1,BT,[wrule(H,true,B,true)|WT],A0,A1).
400solve(H,0,if(H,asked),WT,A0,A0) :-
401 debugging_failure,!,
402 debugging_failure_goal(H,WT).
403solve(_,0,_,_,_,_) :-
404 retractall(failed(_)),
405 assert(failed(unnaturally)),
406 fail.
407
408report(Q,Res,[]) :- !,
409 writeallonline(['Answer: ',Q,'.']),
410 report_runtime,
411 writel([' [ok,more,how,help]: ']),
412 flush_and_read(Comm),
413 interpret_report(Comm,Q,Res,[]).
414report(Q,Res,Ass) :-
415 writeallonline(['Answer: ',Q,'.']),
416 writeallonline(['Assuming: ',Ass,'.']),
417 report_runtime,
418 writel([' [more,ok,how,help]: ']),
419 flush_and_read(Comm),
420 interpret_report(Comm,Q,Res,Ass).
421
423interpret_report(ok,_,_,_) :- !.
424interpret_report(more,_,_,_) :- !,
425 reset_runtime,fail.
426interpret_report(end_of_file,_,_,_) :- !,
427 writeallonline(['^D']).
428interpret_report(how,Q,Res,Ass) :- !,
429 traverse(Res,Rep),
430 ( (Rep = top; Rep=up)
431 -> report(Q,Res,Ass)
432 ; Rep= retry
433 -> reset_runtime,fail
434 ; Rep=prompt
435 -> true
436 ; writeallonline(['This shouldn''t occur. Traverse reported ',Rep])
437 ).
438interpret_report(help,Q,Res,Ass) :- !,
439 writeallonline([
440 ' The system has proven an instance of your query.',nl,
441 ' You can give the following commands:',nl,
442 ' more. for more answers',nl,
443 ' ok. for no more answers',nl,
444 ' how. to enter a dialog to determine how the goal was proved.']),
445 report(Q,Res,Ass).
446interpret_report(Comm,Q,Res,Ass) :-
447 Comm \== more,
448 writeallonline(['Unknown command; ',Comm,'. Type "help." if you need help.']),
449 report(Q,Res,Ass).
450
452debugging_failure_goal(H,WT) :-
453 writeallonline([' Depth-bound reached. Current subgoal: ',H,'.']),
454 writel([' [fail,succeed,proceed,why,ok,help]: ']),
455 flush_and_read(Comm),
456 interpret_debugging_failure_command(Comm,H,WT).
457
458interpret_debugging_failure_command(help,H,WT) :- !,
459 writeallonline([
460 ' The system has reached the depth bound.',nl,
461 ' You can give the following commands:',nl,
462 ' fail. fail this subgoal.',nl,
463 ' succeed. make this subgoal succeed.',nl,
464 ' proceed. fail and don''t stop any more at failing subgoals.',nl,
465 ' why. determine why this subgoal was called.',nl,
466 ' ok. return to cilog prompt.',nl,
467 ' help. print this message.']),
468 debugging_failure_goal(H,WT).
469interpret_debugging_failure_command(fail,_,_) :- !,
470 retractall(failed(_)),
471 assert(failed(unnaturally)),
472 fail.
473interpret_debugging_failure_command(succeed,_,_) :- !.
474interpret_debugging_failure_command(proceed,_,_) :- !,
475 retractall(debugging_failure),
476 retractall(failed(_)),
477 assert(failed(unnaturally)),
478 fail.
479interpret_debugging_failure_command(ok,_,_) :- !,
480 throw(prompt).
481interpret_debugging_failure_command(end_of_file,_,_) :- !,
482 throw(prompt).
483interpret_debugging_failure_command(why,H,WT) :- !,
484 \+ \+ (numbervars(WT,0,_),why_question(WT,_)),
485 debugging_failure_goal(H,WT).
486interpret_debugging_failure_command(Comm,H,WT) :- !,
487 writeallonline([' Unknown command: ',Comm,'. Type "help." for help.']),
488 debugging_failure_goal(H,WT).
489
490
494builtin((A =< B), ground((A =< B))).
495builtin((A >= B), ground((A >= B))).
496builtin((A =\= B), ground((A =\= B))).
497builtin((A < B), ground((A<B))).
498builtin((A > B), ground((A>B))).
499builtin((_ is E),ground(E)).
500builtin(number(E),ground(E)).
501
503debugging_builtin_error(H,WT) :-
504 writeallonline([' Error in built-in predicate: ',H,'.']),
505 writel([' [fail,succeed,why,ok,help]: ']),
506 flush_and_read(Comm),
507 interpret_builtin_error_command(Comm,H,WT).
508
509interpret_builtin_error_command(help,H,WT) :- !,
510 writeallonline([
511 ' There is an error in a built-in predicate.',nl,
512 ' You can give the following commands:',nl,
513 ' fail. fail this subgoal.',nl,
514 ' succeed. make this subgoal succeed.',nl,
515 ' why. determine why this subgoal was called.',nl,
516 ' ok. return to cilog prompt.',nl,
517 ' help. print this message.']),
518 debugging_failure_goal(H,WT).
519interpret_builtin_error_command(fail,_,_) :- !,
520 fail.
521interpret_builtin_error_command(succeed,_,_) :- !.
522interpret_builtin_error_command(ok,_,_) :- !,
523 throw(prompt).
524interpret_builtin_error_command(end_of_file,_,_) :- !,
525 throw(prompt).
526interpret_builtin_error_command(why,H,WT) :- !,
527 \+ \+ (numbervars(WT,0,_),why_question(WT,_)),
528 debugging_builtin_error(H,WT).
529interpret_builtin_error_command(Comm,H,WT) :- !,
530 writeallonline([' Unknown command: ',Comm,'. Type "help." for help.']),
531 debugging_builtin_error(H,WT).
532
536
541ask_user(G,_,Ans) :-
542 ground(G),
543 asked(G,Ans1),!,Ans=Ans1.
544
545ask_user(G,WT,Ans) :-
546 ground(G),!,
547 writel(['Is ',G,' true? [yes,no,unknown,why,help]: ']),
548 flush_and_read(Rep),
549 interpret_ask_answer(Rep,G,WT,Ans).
550ask_user(G,WT,fail) :-
551 writeallonline([' Error: Askables with free variables not implemented.',nl,
552 ' The system wanted to ask ',G,'.',nl,
553 ' Entering why interation.']),
554 numbervars(WT,0,_),
555 why_question(WT,_),
556 writeallonline([' Askable subgoal ',G,' failing due to free variables.']).
557
558
560interpret_ask_answer(help,G,WT,Rep) :- !,
561 writeallonline([' The system is asking whether ',G,' is true or not. Give one of:',nl,
562 ' "yes." if ',G,' is known to be true.',nl,
563 ' "no." if ',G,' is known to be false.',nl,
564 ' "unknown." if ',G,' is unknown (so applicable clauses can be used).',nl,
565 ' "fail." to fail the subgoal (but not record an answer).',nl,
566 ' "why." to see why the system was asking this question.',nl,
567 ' "prompt." to return to the cilog prompt.',nl,
568 ' "help." to print this message.']),
569 ask_user(G,WT,Rep).
570interpret_ask_answer(yes,G,_,yes) :- !,
571 assertz(asked(G,yes)).
572interpret_ask_answer(no,G,_,no) :- !,
573 assertz(asked(G,no)).
574interpret_ask_answer(unknown,G,_,unknown) :- !,
575 assertz(asked(G,unknown)).
576interpret_ask_answer(fail,_,_,fail) :- !.
577interpret_ask_answer(prompt,_,_,_) :- !,
578 throw(prompt).
579interpret_ask_answer(end_of_file,_,_,_) :- !,
580 writeallonline(['^D']),
581 throw(prompt).
582
583interpret_ask_answer(why,G,WT,Rep) :- !,
584 \+ \+ ( numbervars(WT,0,_),why_question(WT,Rep),Rep \== prompt),
585 ask_user(G,WT,Rep).
586interpret_ask_answer(Ans,G,WT,Rep) :-
587 Ans \== fail,
588 writeallonline([' Unknown response "',Ans,'". For help type "help.".']),
589 ask_user(G,WT,Rep).
590
591
598why_question([wrule(H,LT,C,RB)|WT],Rep) :-
599 writeallonline([' ',C,' is used in the rule ']),
600 writeallonline([' ',H,' <-']),
601 print_tree_body(LT,1,Max),
602 writeallonline([' ** ',Max,': ',C]),
603 M1 is Max+1,
604 print_body(RB,M1,_),
605 writel([' [Number,why,help,ok]: ']),
606 flush_and_read(Comm),
607 interpret_why_ans(Comm,Max,[wrule(H,LT,C,RB)|WT],Rep).
608why_question([],down) :-
609 writeallonline([' This was the original query.']).
610
612interpret_why_ans(help,Max,[wrule(H,LT,C,RB)|WT],Rep) :- !,
613 writeallonline([
614' You can taverse the proof for a subgoal using following commands:',nl,
615' how i. show how element i (i<',Max,') of the body was proved.',nl,
616' how ',Max,'. show the rule being considered for ',C,'.',nl,
617' why. show why ',H,' is being proved.',nl,
618' prompt. return to the cilog prompt.',nl,
619' help. print this message.']),
620 why_question([wrule(H,LT,C,RB)|WT],Rep).
621interpret_why_ans(up,_,WT,Rep) :- !,
622 interpret_why_ans(why,_,WT,Rep).
623interpret_why_ans(why,_,[WR|WT],Rep) :- !,
624 why_question(WT,Rep1),
625 (Rep1 = down
626 -> why_question([WR|WT],Rep)
627 ; Rep=Rep1).
628interpret_why_ans((how N),Max,[wrule(H,LT,C,RB)|WT],Rep) :-
629 integer(N),!,
630 interpret_why_ans(N,Max,[wrule(H,LT,C,RB)|WT],Rep).
631interpret_why_ans(N,Max,[wrule(H,LT,C,RB)|WT],Rep) :-
632 integer(N),
633 N > 0,
634 N < Max, !,
635 nth(LT,1,_,N,E),
636 traverse(E,Rep1),
637 (Rep1=up -> why_question([wrule(H,LT,C,RB)|WT],Rep) ;
638 Rep1=top -> Rep=bottom ;
639 Rep1=retry
640 -> writeallonline([' retry doesn''t make sense here.']),
641 why_question([wrule(H,LT,C,RB)|WT],Rep) ;
642 Rep=Rep1).
643interpret_why_ans(Max,Max,_,down) :- !.
644interpret_why_ans(N,Max,WT,Rep) :-
645 integer(N),
646 N > Max, !,
647 writeallonline(['You can''t trace this, as it hasn''t been proved.']),
648 why_question(WT,Rep).
649interpret_why_ans(end_of_file,_,_,_) :- !,
650 writeallonline(['^D']),
651 throw(prompt).
652interpret_why_ans(prompt,_,_,_) :- !,
653 throw(prompt).
654interpret_why_ans(ok,_,_,bottom) :- !.
655
656interpret_why_ans(Comm,_,WT,Rep) :- !,
657 writeallonline(['Unknown command: ',Comm,'. Type "help." for help.']),
658 why_question(WT,Rep).
659
660
663print_body(true,N,N) :- !.
664print_body((A&B),N0,N2) :- !,
665 print_body(A,N0,N1),
666 print_body(B,N1,N2).
667print_body(H,N,N1) :-
668 writeallonline([' ',N,': ',H]),
669 N1 is N+1.
670
671
672
676
679
680failtoprove(G,N,WT) :-
681 (failed(naturally) ->
682 (solve(G,N,_,WT,[],_) ->
683 retract(failed(unnaturally)), asserta(failed(naturally)),fail
684 685 ; failed(naturally)
686 )
687 ; retract(failed(_)),
688 assert(failed(naturally)),
689 (solve(G,N,_,WT,[],_) ->
690 retract(failed(naturally)), asserta(failed(unnaturally)),fail
691 ; retract(failed(naturally)), asserta(failed(unnaturally))
692 693 )).
694
698
699solvebag(bagof(E,Q,L),N,bag(E,Q,BL),WT,A0,A1) :-
700 retract(failed(How)),
701 assert(failed(naturally)),
702 extractExistVars(Q,EVs,QR),
703 bagof(anstree(E,T),EVs^solve(QR,N,T,WT,A0,A1),BL), 704 ( failed(naturally) ->
705 firstOfAnstree(BL,L),
706 retract(failed(naturally)),
707 assert(failed(How))
708 ;
709 fail
710 ).
711
712firstOfAnstree([],[]).
713firstOfAnstree([anstree(E,_)|L],[E|R]) :-
714 firstOfAnstree(L,R).
715
(A^B^C,A^Vs,Q) :- !,
717 extractExistVars(B^C,Vs,Q).
718extractExistVars((A^Q&R),A,(Q&R)) :- !.
719extractExistVars(A^Q,A,Q) :- !.
720extractExistVars(Q,none,Q) :- !.
721
725
733traverse((A&B),Rep) :-
734 traverse(if(yes,(A&B)),Rep).
735traverse(if(H,true),up) :- !,
736 writeallonline([' ',H,' is a fact']).
737traverse(if(H,builtin),up) :- !,
738 writeallonline([' ',H,' is built-in.']).
739traverse(if(H,asked),up) :- !,
740 writeallonline([' You told me ',H,' is true.']).
741traverse(if(H,assumed),up) :- !,
742 writeallonline([' ',H,' is assumed.']).
743traverse(if(~G,naf),Rep) :- !,
744 writeallonline([' ',G,' finitely failed. You can examine the search space.']),
745 depth_bound(DB),
746 whynotb(G,DB,Rep,[],_).
747traverse(if(H,B),Rep) :-
748 writeallonline([' ',H,' <-']),
749 print_tree_body(B,1,Max),
750 writel([' How? [Number,up,retry,ok,prompt,help]: ']),
751 flush_and_read(Comm),
752 interpretcommand(Comm,B,Max,if(H,B),Rep).
753traverse(bag(E,Q,BL),Rep) :-
754 howbag(E,Q,BL,Rep).
755
758print_tree_body(true,N,N).
759print_tree_body((A&B),N0,N2) :-
760 print_tree_body(A,N0,N1),
761 print_tree_body(B,N1,N2).
762print_tree_body(if(H,_),N,N1) :-
763 writeallonline([' ',N,': ',H]),
764 N1 is N+1.
765print_tree_body(bag(E,Q,BL),N,N1) :-
766 firstOfAnstree(BL,L),
767 writeallonline([' ',N,': ',bagof(E,Q,L)]),
768 N1 is N+1.
769
771interpretcommand(help,_,Max,G,Rep) :- !,
772 writeallonline([
773 ' Give either (end each command with a period):',nl,
774 ' how i. explain how subgoal i (i<',Max,') was proved.',nl,
775 ' up. go up the proof tree one level.',nl,
776 ' retry. find another proof.',nl,
777 ' ok. stop traversing the proof tree.',nl,
778 ' prompt. return to the cilog prompt.',nl,
779 ' help. to print this message.']),
780 traverse(G,Rep).
781interpretcommand((how N),B,Max,G,Rep) :-
782 integer(N),
783 interpretcommand(N,B,Max,G,Rep).
784interpretcommand(N,B,Max,G,Rep) :-
785 integer(N),
786 N > 0,
787 N < Max,!,
788 nth(B,1,_,N,E),
789 traverse(E,Rep1),
790 ( Rep1= up
791 -> traverse(G,Rep)
792 ; Rep=Rep1
793 ).
794interpretcommand(N,_,Max,G,Rep) :-
795 integer(N),!,
796 797 M1 is Max-1,
798 writeallonline(['Number out of range: ',N,'. Use number in range: [1,',M1,'].']),
799 traverse(G,Rep).
800interpretcommand(up,_,_,_,up) :-!.
801interpretcommand(why,_,_,_,up) :-!.
802interpretcommand(ok,_,_,_,top) :-!.
803interpretcommand(prompt,_,_,_,_) :-!,
804 throw(prompt).
805interpretcommand(retry,_,_,_,retry) :-!.
806interpretcommand(end_of_file,_,_,_,prompt) :-!,
807 writeallonline(['^D']).
808interpretcommand(C,_,_,G,Rep) :-
809 writeallonline(['Illegal Command: ',C,' Type "help." for help.']),
810 traverse(G,Rep).
811
813nth((A&B),N0,N2,N,E) :- !,
814 nth(A,N0,N1,N,E),
815 nth(B,N1,N2,N,E).
816nth(true,N0,N0,_,_) :- !.
817nth(A,N,N1,N,A) :- !,
818 N1 is N+1.
819nth(_,N0,N1,_,_) :-
820 N1 is N0+1.
821
824howbag(E,Q,BL,Rep) :-
825 writeallonline([' The call ',bagof(E,Q,V),' returned with ',V,' containing']),
826 displaybaglist(BL,0,BLLen),
827 writel([' How? [Number,up,whynot,ok,prompt,help]: ']),
828 flush_and_read(Comm),
829 interpret_how_bag_command(Comm,E,Q,BL,BLLen,Rep).
830
832displaybaglist([],0,0) :- !,
833 writeallonline(['no elements.']).
834displaybaglist([],N,N) :- !.
835displaybaglist([anstree(E,_)|R],N,NN) :-
836 N1 is N+1,
837 writeallonline([' ',N1,': ',E]),
838 displaybaglist(R,N1,NN).
839
840interpret_how_bag_command(up,_,_,_,_,up) :- !.
841interpret_how_bag_command(ok,_,_,_,_,top) :- !.
842interpret_how_bag_command(prompt,_,_,_,_,_) :- !,
843 throw(prompt).
844interpret_how_bag_command(end_of_file,_,_,_,_,_) :- !,
845 writeallonline(['^D']),
846 throw(prompt).
847
848interpret_how_bag_command(help,E,Q,BL,Max,Rep) :- !,
849 writeallonline([
850 ' Give either (end each command with a period):',nl,
851 ' how i. explain how element i (i=<',Max,') was proved.',nl,
852 ' up. go up the proof tree one level.',nl,
853 ' retry. find another proof.',nl,
854 ' ok. stop traversing the proof tree.',nl,
855 ' prompt. return to the cilog prompt.',nl,
856 ' help. to print this message.']),
857 howbag(E,Q,BL,Rep).
858interpret_how_bag_command(N,E,Q,BL,BLLen,Rep) :-
859 integer(N),!,
860 ( N >= 0, N =< BLLen ->
861 nthList(N,BL,anstree(_,ET)),
862 traverse(ET,Repl),
863 ( Repl = up
864 -> howbag(E,Q,BL,Rep)
865 ; Rep=Repl
866 )
867 ; writeallonline([' Error: ',N,' must be in range ',[1,BLLen]]),
868 howbag(E,Q,BL,Rep)
869 ).
870interpret_how_bag_command((how N),E,Q,BL,BLLen,Rep) :- !,
871 interpret_how_bag_command(N,E,Q,BL,BLLen,Rep).
872
873interpret_how_bag_command(Comm,E,Q,BL,_,Rep) :- !,
874 writeallonline(['Unknown command ',Comm,' type "help." for help.']),
875 howbag(E,Q,BL,Rep).
876
878nthList(1,[E|_],E) :- !.
879nthList(N,[_|R],E) :-
880 N>1,
881 N1 is N-1,
882 nthList(N1,R,E).
883
887
895
896whynotb((A & B),DB,Rep,Ass0,Ass2) :-
897 retractall(failed(_)),
898 assert(failed(naturally)),
899 solve(A,DB,Res,[whynot],Ass0,Ass1),
900 report_whynot_conj(A,Res,B,DB,Rep,Ass1,Ass2).
901whynotb((A & _),DB,Rep,Ass0,Ass1) :- !,
902 whynotb(A,DB,Rep,Ass0,Ass1).
903
904whynotb(call(A),DB,Rep,Ass0,Ass1) :- !,
905 whynotb(A,DB,Rep,Ass0,Ass1).
906whynotb((~ A),DB,Rep,Ass0,Ass0) :- !,
907 retractall(failed(_)),
908 assert(failed(naturally)),
909 ( solve(A,DB,Res,[whynot],[],_) ->
910 writeallonline([' ',~A,' failed as ',A,' suceeded. Here is how:']),
911 traverse(Res,Rep)
912 ; failed(unnaturally) ->
913 writeallonline([' ',~A,' failed because of the depth-bound.']),
914 whynotb(A,DB,Rep,[],_)
915 ; writeallonline([' ',~A,' succeeds, as ',A,' finitely fails.']),
916 Rep=up
917 ).
918
919whynotb(A,_,up,Ass0,Ass0) :-
920 builtin(A,C),!,
921 (call(C)
922 -> (call(A)
923 -> writeallonline([' ',A,' is built-in and succeeds.'])
924 ; writeallonline([' ',A,' is built-in and fails.']))
925 ; writeallonline([' ',A,' is built-in and is insufficiently instanciated.'])).
926
927whynotb((A \= B),_,up,Ass0,Ass0) :-
928 ?=(A,B),!,
929 (A \== B
930 -> writeallonline([' ',(A \= B),' succeeds as they can never unify.'])
931 ; writeallonline([' ',(A \= B),' fails as they are identical.'])).
932whynotb((A \= B),_,up,Ass0,Ass0) :-
933 writeallonline([' ',(A \= B),' cannot be resolved. It is delayed.']),
934 when(?=(A,B),
935 (A \== B
936 -> writeallonline([' Resolving delayed ',(A \= B),'. It succeeded.'])
937 ; writeallonline([' Failure due to delayed constraint, ',(A \= B),'.']),
938 fail)).
939
940whynotb(Q,0,up,Ass0,Ass0) :- !,
941 writeallonline([' ',Q,' fails because of the depth-bound.']).
942
943whynotb(Q,DB,up,Ass0,Ass0) :-
944 DB > 0,
945 (Q <- true),!,
946 writeallonline([' ',Q,' is a fact. It doesn''t fail.']).
947
948whynotb(Q,DB,Rep,Ass0,Ass1) :-
949 DB > 0,
950 (Q <- B),
951 whynotrule(Q,B,DB,Rep,Ass0,Ass1).
952whynotb(Q,_,up,Ass0,Ass0) :-
953 writeallonline([' There is no applicable rule for ',Q,'.']).
954
955whynotrule(Q,B,DB,Rep,Ass0,Ass1) :-
956 writeallonline([' ',Q,' <- ',B,'.']),
957 writel([' Trace this rule? [yes,no,up,help]: ']),
958 flush_and_read(Comm),
959 whynotruleinterpret(Comm,Q,B,DB,Rep,Ass0,Ass1).
960
961whynotruleinterpret(yes,Q,B,DB,Rep,Ass0,Ass1) :- !,
962 DB1 is DB-1,
963 whynotb(B,DB1,Rep1,Ass0,Ass1),
964 (Rep1 = up
965 -> whynotrule(Q,B,DB,Rep,Ass0,Ass1)
966 ; Rep=Rep1).
967whynotruleinterpret(no,_,_,_,_,_,_) :- !,
968 fail.
969whynotruleinterpret(up,_,_,_,up,Ass0,Ass0) :- !.
970whynotruleinterpret(end_of_file,_,_,_,prompt,_,_) :- !,
971 writeallonline(['^D']).
972whynotruleinterpret(ok,_,_,_,prompt,_,_) :- !.
973whynotruleinterpret(help,Q,B,DB,Rep,Ass0,Ass1) :- !,
974 writeallonline([
975 ' Do you want to examine why this rule failed?',nl,
976 ' yes. look at this rule',nl,
977 ' no. try another rule',nl,
978 ' up. go back to the rule this rule was called from',nl,
979 ' ok. go to top-level prompt']),
980 whynotrule(Q,B,DB,Rep,Ass0,Ass1).
981whynotruleinterpret(Comm,Q,B,DB,Rep,Ass0,Ass1) :-
982 writeallonline([' Unknown command: ',Comm,'. Type "help." for help.']),
983 whynotrule(Q,B,DB,Rep,Ass0,Ass1).
984
985
986report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1) :-
987 writeallonline([' The proof for ',A,' succeeded.']),
988 writel([' Should this answer lead to a successful proof? [yes,no,debug,help]: ']),
989 flush_and_read(Comm),
990 why_not_conj_interpret(Comm,A,Res,B,DB,Rep,Ass0,Ass1).
991
992why_not_conj_interpret(debug,A,Res,B,DB,Rep,Ass0,Ass1) :- !,
993 traverse(Res,Rep1),
994 (Rep1 = up
995 -> report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1)
996 ; Rep=Rep1).
997why_not_conj_interpret(yes,_,_,B,DB,Rep,Ass0,Ass1) :- !,
998 whynotb(B,DB,Rep,Ass0,Ass1).
999why_not_conj_interpret(no,_,_,_,_,_,_,_) :- !,
1000 fail. 1001
1002why_not_conj_interpret(end_of_file,_,_,_,_,prompt,_,_) :- !,
1003 writeallonline(['^D']).
1004why_not_conj_interpret(ok,_,_,_,_,prompt,_,_) :- !,
1005 writeallonline(['^D']).
1006why_not_conj_interpret(help,A,Res,B,DB,Rep,Ass0,Ass1) :- !,
1007 writeallonline([
1008 ' yes. this instance should have made the body succeed.',nl,
1009 ' no. this instance should lead to a failure of the body.',nl,
1010 ' debug. this instance is false, debug it.',nl,
1011 ' ok. I''ve had enough. Go to the prompt.',nl,
1012 ' help. print this message.']),
1013 report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1).
1014why_not_conj_interpret(Comm,A,Res,B,DB,Rep,Ass0,Ass1) :-
1015 writeallonline([' Unknown command: ',Comm,'. Type "help." for help.']),
1016 report_whynot_conj(A,Res,B,DB,Rep,Ass0,Ass1).
1017
1018
1022
1023flush_and_read(T) :-
1024 flush_output,
1025 read(T).
1026
1027with_file(File,Read,Input,Goal):-
1028 setup_call_cleanup(
1029 open(File,Read,Input),
1030 Goal,
1031 close(Input)).
1032
1033
1034with_input(Input,Goal):-
1035 current_input(OldFile),
1036 setup_call_cleanup(set_input(Input),
1037 Goal,
1038 set_input(OldFile)).
1039
1040ci_load(File) :-
1041 with_file(File,read,Input,
1042 with_input(Input,and_read_all)),
1043 writeallonline(['CILOG theory ',File,' loaded.']).
1044
1045and_read_all:-
1046 flush_and_read(T),
1047 read_all(T).
1048read_all(end_of_file) :- !.
1049read_all((askable G)) :- !,
1050 assertz(askabl(G)),
1051 and_read_all.
1052
1053read_all((assumable G)) :- !,
1054 assertz(assumabl(G)),
1055 and_read_all.
1056read_all((H :- B)) :- !,
1057 writeallonline(['Error: Illegal Implication: ',H,' :- ',B,'. Use <- or prload.']).
1058read_all(T) :-
1059 tell_clause(T),
1060 and_read_all.
1061
1062prolog_load(File) :-
1063 with_file(File,read,Input,
1064 with_input(Input,and_prread_all)),
1065 writeallonline(['CILOG theory ',File,' consulted.']).
1066
1067and_prread_all:-
1068 flush_and_read(T),
1069 prread_all(T).
1070prread_all(end_of_file) :- !.
1071prread_all(T) :-
1072 prillegal(T,Mesg),!,
1073 writeallonline(Mesg).
1074prread_all(T) :-
1075 prtell(T),
1076 and_prread_all.
1077
1080prillegal((H <- B),['Error. Illegal Implication: ',H,' <- ',B,
1081 '. Use :- in prload.']) :- !.
1082prillegal((:- B),['Error. Commands not allowed. ":- ',B,'."']) :- !.
1083prillegal((_ :- B),Mesg) :- !,
1084 prillbody(B,Mesg).
1085prillbody((A,_),Mesg) :-
1086 prillbody(A,Mesg).
1087prillbody((_,B),Mesg) :-
1088 prillbody(B,Mesg).
1089prillbody((_;_),['Prolog rules assume disjunction ";". Define it before loading.']) :-
1090 \+ ((_;_) <- _).
1091prillbody((A;_),Mesg) :-
1092 prillbody(A,Mesg).
1093prillbody((_;B),Mesg) :-
1094 prillbody(B,Mesg).
1095prillbody((_&_),['Error. Illegal conjunction in Prolog rules: &']):- !.
1096prillbody(!,['Error. Cut (!) not allowed.']) :- !.
1097prillbody((_ -> _ ; _),['Error. "->" is not implemented.']) :- !.
1098
1100prtell((H :- B)) :- !,
1101 convert_body(B,B1),
1102 assertz((H <- B1)).
1103prtell(H) :-
1104 assertz((H <- true)).
1105
1107convert_body((A,B),(A1&B1)) :- !,
1108 convert_body(A,A1),
1109 convert_body(B,B1).
1110convert_body((A;B),(A1;B1)) :- !,
1111 convert_body(A,A1),
1112 convert_body(B,B1).
1113convert_body((\+ A),(~ A1)) :- !,
1114 convert_body(A,A1).
1115convert_body(A,A).
1116
1117
1121
1122start :-
1123 cilog_version(V),
1124 writeallonline([nl,
1125 'CILOG Version ',V,'. Copyright 1998-2004, David Poole.',nl,
1126 'CILOG comes with absolutely no warranty.',nl,
1127 'All inputs end with a period. Type "help." for help.']),
1128 start1.
1129
1130start1 :-
1131 catch(cilog,Exc,handle_exception(Exc)). 1133 1134go:- cilog.
1135cilog :-
1136 writel(['cilog: ']),
1137 flush_and_read(T),
1138 (T == prolog ->
1139 writeallonline(['Returning to Prolog. Type "start." to start cilog.'])
1140 ; T == end_of_file ->
1141 writeallonline(['^D']),
1142 writeallonline(['Returning to Prolog. Type "start." to start cilog.'])
1143 ; interpret(T),
1144 !,
1145 cilog).
1146
1147handle_exception(prompt) :- !, start1.
1148handle_exception(quit) :- halt.
1149handle_exception(Exc) :-
1150 writeallonline(['Error: ',Exc]),
1151 start1.
1152
1156
1160check :-
1161 (H <- B),
1162 body_elt_undefined(B,H,B).
1163check.
1164
1165body_elt_undefined(true,_,_) :- !,fail.
1166body_elt_undefined((A&_),H,B) :-
1167 body_elt_undefined(A,H,B).
1168body_elt_undefined((_&A),H,B) :- !,
1169 body_elt_undefined(A,H,B).
1170body_elt_undefined((~ A),H,B) :- !,
1171 body_elt_undefined(A,H,B).
1172body_elt_undefined((A;_),H,B) :-
1173 body_elt_undefined(A,H,B).
1174body_elt_undefined((_;A),H,B) :- !,
1175 body_elt_undefined(A,H,B).
1176body_elt_undefined(call(A),H,B) :- !,
1177 body_elt_undefined(A,H,B).
1178body_elt_undefined(_ \= _,_,_) :- !,fail.
1179body_elt_undefined(A,_,_) :-
1180 askabl(A),!,fail.
1181body_elt_undefined(A,_,_) :-
1182 assumabl(A),!,fail.
1183body_elt_undefined(A,_,_) :-
1184 builtin(A,_),!,fail.
1185body_elt_undefined(A,_,_) :-
1186 (A <- _),!,fail.
1187body_elt_undefined(A,H,B) :-
1188 writeallonline(['Warning: no clauses for ',A,' in rule ',(H <- B),'.']),!,fail.
1189
1193
1195checking_runtime.
1196
1198stats_command(runtime) :- !,
1199 retractall(checking_runtime),
1200 asserta(checking_runtime),
1201 writeallonline(['Runtime report turned on. Type "stats none." to turn it off.']).
1202stats_command(none) :- !,
1203 retractall(checking_runtime).
1204stats_command(_) :-
1205 writeallonline(['The stats commands implemented are:']),
1206 writeallonline([' stats runtime. turn on report of runtime.']),
1207 writeallonline([' stats none. turn off report of runtime.']).
1208
1212
1213reset_runtime :-
1214 checking_runtime,
1215 retractall(lastruntime(_)),
1216 get_runtime(T,_),
1217 asserta(lastruntime(T)),!.
1218reset_runtime :-
1219 checking_runtime ->
1220 writeallonline([' Problem with runtime checking.'])
1221 ; true.
1222
1223report_runtime :-
1224 checking_runtime,
1225 lastruntime(T),
1226 get_runtime(T1,Units),
1227 RT is T1 - T,
1228 writeallonline([' Runtime since last report: ',RT,' ',Units,'.']),!.
1229report_runtime :-
1230 checking_runtime ->
1231 writeallonline([' Problem with runtime reporting.'])
1232 ; true.
1233
1234
1238
1240writeallonline(L) :-
1241 \+ \+ (numbervars(L,0,_),writel0(L)),
1242 nl.
1244writel(L) :-
1245 \+ \+ (numbervars(L,0,_),writel0(L)).
1246
1248writel0([]) :- !.
1249writel0([nl|T]) :- !,
1250 nl,
1251 writel0(T).
1252writel0([H|T]) :-
1253 mywrite(H),
1254 writel0(T).
1255
1256insert(A,[],[A]).
1257insert(A,[A1|R],[A|R]) :- A == A1,!.
1258insert(A,[B|R],[B|R1]) :-
1259 insert(A,R,R1).
1260
1261
1263different(X,Y) :-
1264 \+ (X=Y),!.
1265different(X,Y) :-
1266 X \== Y,
1267 writeallonline(['Warning: ',X\=Y,' failing. Delaying not implemented.']),!,
1268 fail.
1269
1270:- initialization(start).