1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%%                                                                           %%
    3%%      Version:  1.00   Date: 15/03/98   File: xray_config.pl               %%
    4%% Last Version:                          File:                              %%
    5%% Changes:                                                                  %%
    6%% 15/03/98 Created                                                          %%
    7%%                                                                           %%
    8%% Purpose:                                                                  %%
    9%%                                                                           %%
   10%% Author:  Torsten Schaub                                                   %%
   11%%                                                                           %%
   12%% Usage:   prolog xray_config.pl                                            %%
   13%%                                                                           %%
   14%%                                                                           %%
   15%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   16
   17:- ensure_loaded(hooks).   18:- ensure_loaded(lemma).   19
   20:- no_hook_handling,hook_configuration.     % indicated by {pred|body}_hook_flag
   21
   22:- no_lemma_handling,lemma_configuration.   % indicated by lemma_handling_flag
   23
   24:- dynamic(delta_ordering/1).   25:- dynamic(verbose_flag/0).   26:- dynamic(compile_complete_search/0).   27
   28%%% ----------------------------------------------------------------------
   29%%% PTTP CONFIGURATION
   30
   31%%% complete search facilities are turned (during compile-time)
   32%%%  on by do_compile_complete_search,
   33%%% off by dont_compile_complete_search.
   34%%%
   35%%% do_compile_complete_search or dont_compile_complete_search *must* be
   36%%% executed before the problem is compiled.
   37
   38do_compile_complete_search :-
   39        retract(compile_complete_search),
   40        fail.
   41do_compile_complete_search :-
   42        assert(compile_complete_search).
   43
   44dont_compile_complete_search :-
   45        retract(compile_complete_search),
   46        fail.
   47dont_compile_complete_search.
   48
   49:- do_compile_complete_search.            % default is to compile complete search
   50
   51%%% Proof printing is (better) turned (during compile-time)
   52%%%  on by   do_compile_proof_printing (print_proof),
   53%%% off by dont_compile_proof_printing (dont_print_proof).
   54%%%
   55%%% do_compile_proof_printing or dont_compile_proof_printing *must* be
   56%%% executed before the problem is compiled.
   57
   58do_compile_proof_printing   :- print_proof.
   59dont_compile_proof_printing :- dont_print_proof.
   60
   61:- do_compile_proof_printing.            % default is to compile proof printing
   62
   63%%% Inference counting is turned
   64%%%  on by   do_compile_count_inferences (count_inferences),
   65%%% off by dont_compile_count_inferences (dont_count_inferences).
   66%%%
   67%%% Inferences are counted by retracting the current count
   68%%% and asserting the incremented count, so inference counting
   69%%% is very slow.
   70
   71do_compile_count_inferences   :- count_inferences.
   72dont_compile_count_inferences :- dont_count_inferences.
   73
   74:- dont_compile_count_inferences.   75
   76pttp_configuration :-
   77	nl,writeln('PTTP CONFIGURATION:'),nl,
   78	(count_inferences_pred(true) ->
   79	    writeln('PTTP counts no inferences.');
   80	    writeln('PTTP counts inferences!')),
   81        (trace_search_progress_pred(nop) ->
   82	    writeln('PTTP does not trace search progress.');
   83	    writeln('PTTP traces search progress!')),
   84	(compile_proof_printing ->
   85	    writeln('PTTP compiles proof printing!');
   86	    writeln('PTTP does not compile proof printing.')),
   87	(compile_complete_search ->
   88	    writeln('PTTP compiles complete search!');
   89	    writeln('PTTP does not compile complete search.')).
   90
   91:- pttp_configuration.   92
   93%%% ----------------------------------------------------------------------
   94%%% XRay CONFIGURATION
   95
   96xray_configuration :-
   97	nl,write('XRay CONFIGURATION:'),nl,nl,
   98	
   99	write(delta_ordering),
  100	write(' = '),
  101	(delta_ordering(O), write(O),write(' '),fail ; write('.')),
  102	nl,
  103	
  104	write(verbose_mode),
  105	write(' = '),
  106	(verbose_flag, write("on") ; write("off")),
  107	nl.
  108
  109%%% delta_ordering stears the order of admissibility 
  110%%% and compatibility checking in delta rules
  111%%% at compile-time
  112
  113switch_delta_ordering :-
  114	delta_ordering(compatibility>admissibility),
  115	admissibility_first.
  116switch_delta_ordering :-
  117	delta_ordering(admissibility>compatibility),
  118	compatibility_first.
  119
  120compatibility_first :-                      % check compatibility first
  121        retract(delta_ordering(_)),
  122        fail.
  123compatibility_first :-
  124        assert(delta_ordering(compatibility>admissibility)).
  125
  126admissibility_first :-                      % check admissibility first
  127        retract(delta_ordering(_)),
  128        fail.
  129admissibility_first :-
  130        assert(delta_ordering(admissibility>compatibility)).
  131
  132:- admissibility_first.                     % default is to check admissibility first
  133
  134
  135%%% Verbose proof printing is turned on by verbose_mode,
  136%%% off by dont_verbose_mode.
  137%%% works during compile- and run-time
  138
  139verbose_mode :-                          % enable proof printing
  140        retract(verbose_flag),
  141        fail.
  142verbose_mode :-
  143        assert(verbose_flag).
  144
  145no_verbose_mode :-                     % disable proof printing
  146        retract(verbose_flag),
  147        fail.
  148no_verbose_mode.
  149
  150:- verbose_mode.                         % default is to print proof
  151
  152%%% verbose predicate, chatting if verbose_mode is turned on
  153verbose(X) :-
  154	verbose_flag ->
  155	        write(X),nl;
  156	%true->
  157		true.
  158
  159%%% PRINT CONFIGURATION
  160%%%
  161
  162:- xray_configuration,nl.  163
  164configuration :-
  165	hook_configuration,
  166	lemma_configuration,
  167	pttp_configuration,
  168	xray_configuration