1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%% $Id: tom_constraints.pl,v 1.3 1994/05/31 20:03:48 gerd Exp $
    3%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    4
    5/*%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    6
    7\chapter
    8[Die Datei {\tt tom\_constraints}]
    9{Die Datei {\Huge \tt tom\_constraints}}
   10
   11This file contains the particular predicates for the approach using
   12constraints and constraint handling.
   13
   14\PL*/
   15write_matrix(OutStream):-
   16	is_option('Tom:special_path_term',Value),
   17	( Value = off ->
   18	    true
   19	; concat_atom([Value,'.pl'],FullFileName),
   20	  compile(FullFileName)
   21	),
   22	!,
   23	( constraint(_AnyType, AFormula, matrix),
   24	  ( Value = off ->
   25	      NormalizedFormula = AFormula
   26	  ; Call_Normal_Formula =.. [Value, AFormula, NormalizedFormula],
   27	    call(Call_Normal_Formula)
   28	  ),
   29	  write_one_clause(OutStream,NormalizedFormula),
   30	  fail
   31	; true
   32	).
   33
   34write_extras(OutStream):-
   35	check_options(OutStream),
   36	writeclause(OutStream,# begin(constraint_theory)),
   37	!,
   38	( setof(Type,B ^ A ^ constraint(Type,A,B),ListOfTypes)
   39	; true
   40	),
   41	( member((Functor / Arity),ListOfTypes),
   42	  ( is_option('Tom:theory_optimization') ->
   43	      add_driver_clause(OutStream,Functor,Arity)
   44	  ; true
   45	  ),
   46	  constraint((Functor / Arity),AxiomClause,Sort),
   47	  ( Sort = transitive ->
   48	      optimize_transitive(AxiomClause,OptimizedAxiom)
   49	  ; Sort = interaction ->
   50	      optimize_interaction(AxiomClause,OptimizedAxiom)
   51	  ; is_option('Tom:theory_optimization') ->
   52	      optimize_axiom(AxiomClause,OptimizedAxiom)
   53	  ; OptimizedAxiom = AxiomClause
   54	  ),
   55	  writeclause(OutStream, OptimizedAxiom),
   56	  fail
   57	; true
   58	),
   59	( is_option('Tom:theory_optimization') ->
   60	    writeclause(OutStream,
   61	           {check_theory_depth(Depth,NewDepth):-  
   62	                  ( (Depth =< 0) ->
   63			     setval(depthq,1),
   64			     fail
   65			  ; NewDepth is Depth-1)})
   66	; true
   67	),
   68	writeclause(OutStream,# end(constraint_theory)),
   69	is_option('Tom:special_unification',Value),
   70	( Value = off ->
   71	    true
   72	; write_descriptors(Value)
   73	).
   74/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   75
   76\Predicate write_one_clause/2 (+OutStream, +Clause).
   77
   78This predicate organises the output of one clause |Clause| to the
   79output stream |OutStream|. We distinguish two cases here:
   80\begin{enumerate}
   81\item The usual case is an implication. As we are
   82dealing with some kind of Prolog notation and we want to write
   83implications, we write the conclusions at first followed by the
   84premises and finally the constraints. 
   85However, before we can print out the literals, we reorder the formula.
   86Any of the lists of literals (|Conclusions|, |Premises|, |Constraints|) may
   87be empty and the separators for formatting if printed depending on these lists.
   88
   89We were not able to use the built-in predicate |writeclause| because it doesn't
   90know the operator |//:|.
   91\end{enumerate}
   92\PL*/
   93write_one_clause(Stream,(Conclusion :- Premise)):-
   94	!,
   95	reorder((Conclusion :- Premise),Premises,Conclusions,Constraints),
   96	write_literals(Stream,Conclusions,";"),
   97	( Premises = [] -> true ; printf(Stream," :- ",[])),
   98	write_literals(Stream,Premises,","),
   99	( Constraints = [] -> true ; printf(Stream,"  //: ",[])),
  100	write_literals(Stream,Constraints,","),
  101	printf(Stream,".\n",[]).
  102
  103/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  104\begin{enumerate}
  105\addtocounter{enumi}{1}
  106\item The second clause of this predicate is treating the ordinary formulae. They
  107are translated into a Prolog format and printed using |writeclause|. We can
  108be sure that if the formula is not an implication that there won't be any
  109constraint predicates because they are introduced in an implication
  110or a conjunction only. However, implications are treated by the first clause
  111of the predicate and a conjunct with an auxiliary predicate has been put in
  112the constraint theory part.
  113\end{enumerate}
  114
  115\PL*/
  116
  117write_one_clause(Stream,Formula):-
  118	build_clause(Formula,PrologClause),
  119	writeclause(Stream,PrologClause).
  120
  121/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  122
  123\Predicate reorder/4 (+Formula, -Premises, -Conclusions, -Constraints).
  124
  125This predicate examines the formula tree and collects the literals
  126into the three lists |Premises|, |Conclusions|, and |Constraints|.
  127
  128The formula |Formula| is assumed to be an implication. At first, the premise
  129is treated and the conclusion afterwards.
  130
  131\PL*/
  132reorder((Conclusion :- Premise),Premises,Conclusions,Constraints):-
  133	reorder(Premise,[],[],Premises,NewConstraints,p),
  134	reorder(Conclusion,[],NewConstraints,Conclusions,Constraints,c).
  135/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  136
  137\Predicate reorder/6 (+Formula, +InLiterals, +InConstraints,
  138	              -OutLiterals, -OutConstraints, +Indicator).
  139
  140This predicates reorders formulae which are not implications. Due to the
  141construction of the algorithm, they are basically literals, conjunctions,
  142or disjunctions. The last two cases are covered by the first clause.
  143In case of disjunction and conjunction, we simply proceed on the disjuncts
  144and conjuncts respectively.
  145
  146If we have a negated formula, this formula must be a literal (we are working
  147with a negation normal form). Auxiliary predicates cannot be negated, hence,
  148we simply chuck it in the list of literals.
  149
  150In case we are dealing with a literal, it goes either into the list of literals
  151or into the list of constraints. If it goes into the list of constraints, we
  152have to take care of whether we are dealing with a premise or a conclusion
  153of an implication. Depending on that fact, we negate the literal or we don't.
  154For determining the fact just mentioned, we have introduced the additional
  155argument |Indicator| which can only take the values |p| and |c|, for premise
  156and conclusion respectively.
  157
  158\PL*/
  159reorder((P1 , P2),InLiterals,InConstraints,
  160	             OutLiterals,OutConstraints,Indicator):-
  161	!,
  162	reorder(P1,InLiterals,InConstraints,
  163	            NewLiterals,NewConstraints,Indicator),
  164	reorder(P2,NewLiterals,NewConstraints,
  165	            OutLiterals,OutConstraints,Indicator).
  166
  167reorder((P1 ; P2),InLiterals,InConstraints,
  168	             OutLiterals,OutConstraints,Indicator):-
  169	!,
  170	reorder(P1,InLiterals,InConstraints,
  171	            NewLiterals,NewConstraints,Indicator),
  172	reorder(P2,NewLiterals,NewConstraints,
  173	            OutLiterals,OutConstraints,Indicator).
  174
  175reorder(-(Formula), InLiterals, InConstraints, [- Formula | InLiterals],
  176	  InConstraints,_):-!.
  177
  178reorder(Formula,InLiterals,InConstraints,
  179	             OutLiterals,OutConstraints,Indicator):-
  180	Formula =.. [Functor | _Arguments],
  181	( name(Functor,[36, 82, 109, 111, 100 | _]) ->
  182	    ( Indicator = 'p' ->
  183		OutConstraints = [ Formula | InConstraints ]
  184	    ; OutConstraints = [ - Formula | InConstraints ]
  185	    ),
  186	    OutLiterals = InLiterals
  187	; OutConstraints = InConstraints,
  188	  OutLiterals = [ Formula | InLiterals]
  189	).
  190/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  191
  192\Predicate write_literals/3 (+Stream, +ListOfLiterals, +Separator).
  193
  194This predicate prints the literals from |ListOfLiterals| to |Stream|,
  195separating two of those by |Separator|. The predicate |printf| is used
  196for printing --- quick and dirty (well, kind of).
  197
  198\PL*/
  199
  200write_literals(_Stream,[],_Separator).
  201
  202write_literals(Stream,[H | T],Separator):-
  203	printf(Stream,"%vDQMw ",[H]),
  204	( T = [] ->
  205	  true
  206	; printf(Stream," %w ",[Separator]),
  207	  write_literals(Stream,T,Separator)
  208	).
  209
  210/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  211
  212\Predicate optimize_axiom/2 (+InAxiom, -OutAxiom).
  213
  214The optimization of any axiom basically means to append another argument to
  215each literal. This new argument expresses the depth of the theory inferences.
  216In order to do this, we analyse the structure of the clause to be
  217optimized. On the literal level, we add another argument to the
  218predicate symbol.
  219
  220This predicate simply generates the additional argument and the following
  221predicate |optimize_axiom/3| is called.
  222\PL*/
  223
  224optimize_axiom((Head :- Body),(OptHead :- OptBody)):-
  225	!,
  226	optimize_axiom(Head,OptHead,Depth),
  227	optimize_axiom(Body,OptBody,Depth).
  228
  229optimize_axiom(Literal, OptLiteral):-
  230	Literal =.. [ Functor | Arguments ],
  231	append(Arguments, [_Depth], NewArguments),
  232	OptLiteral =.. [ Functor | NewArguments ].
  233
  234/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  235
  236\Predicate optimize_axiom/3 (+InAxiom, -OutAxiom, +Depth).
  237
  238Here, we get down to the literal level and increase the arity of the
  239predicate symbol by one.
  240
  241\PL*/
  242
  243optimize_axiom((L1 ; L2),(OL1 ; OL2),Depth):-
  244	!,
  245	optimize_axiom(L1, OL1, Depth),
  246	optimize_axiom(L2, OL2, Depth).
  247
  248optimize_axiom((L1 , L2),(OL1 , OL2), Depth):-
  249	!,
  250	optimize_axiom(L1, OL1, Depth),
  251	optimize_axiom(L2, OL2, Depth).
  252
  253optimize_axiom( -(Literal), -(OptLiteral), Depth):-
  254	!,
  255	optimize_axiom(Literal, OptLiteral, Depth).
  256
  257optimize_axiom(Literal, OptLiteral, Depth):-
  258	Literal =.. [ Functor | Arguments ],
  259	append(Arguments, [Depth], NewArguments),
  260	OptLiteral =.. [ Functor | NewArguments ].
  261/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  262
  263\Predicate optimize_transitive/2 (+InAxiom, -OutAxiom).
  264
  265The axiom for transitivity has to be optimised in a special way. Most
  266other axioms are not self recursive, while the transitivity is. Hence,
  267we have to control the depth of inferences in the theory. This has been done
  268by including another predicate, into the optimised
  269axiom. This additional predicate is called |check_theory_depth|.
  270The Dollar sign has to be used because it will be stripped off
  271from the filter to follow (|constraints.pl|).
  272
  273\PL*/
  274
  275optimize_transitive((H :- C1,C2),
  276	            (OHead :- { check_theory_depth(X,Y),
  277		                nonvar(Argument),
  278		                Unification},
  279			      OC1, OC2)):-
  280	H =.. [HFunctor | [HArguments]],
  281	OHead =.. [HFunctor, Argument, X],
  282	C1 =.. C1List,
  283	append(C1List, [Y], NewC1),  
  284	OC1 =.. NewC1,
  285	C2 =.. C2List,
  286	append(C2List, [Y], NewC2),
  287	OC2 =.. NewC2,
  288	is_option('Tom:special_unification', Unificator),
  289	( Unificator = off ->
  290	    Unification = (Argument =  HArguments)
  291	; Unification =.. [Unificator, Argument, HArguments]
  292	).
  293
  294/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  295
  296\Predicate optimize_interaction/2 (+InAxiom, -OutAxiom).
  297
  298The axiom for interaction has to be optimised in a special way. We want to
  299ensure that the A1-unification is carried out on the first arguments only.
  300
  301\PL*/
  302
  303optimize_interaction((H :- T),
  304	            (OHead :- { nonvar(HA),
  305	                        Unification},
  306	                      OT)):-
  307	H =.. [HF, HA],
  308	OHead =.. [HF, HA, Depth],
  309	T =.. [TF,  TA],
  310	OT =.. [TF, TA, Depth],
  311	is_option('Tom:special_unification', Unificator),
  312	( Unificator = off ->
  313	    Unification = (HA = TA)
  314	; Unification =.. [Unificator, HA, TA]
  315	).
  316
  317/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  318
  319\Predicate add_driver_clause/3 (+OutStream, +Functor, + Arity).
  320
  321We add the driver clause for each different predicate symbol. This clause
  322simply adds another argument to the predicate which unifies with a counter
  323containing the depth.
  324\PL*/
  325
  326add_driver_clause(OutStream, Functor, Arity):-
  327	functor(Pred1, Functor, Arity),
  328	Pred1 =.. List,
  329	append(List, [Val], NewList),
  330	Pred2 =.. NewList,
  331	writeclause(OutStream,(Pred1 :- ({getval(current_depth,Val)},
  332	                                 Pred2))).
  333
  334/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  335
  336\Predicate check_options/1 (+Stream).
  337
  338This predicate simply checks the option |'Tom:theory_optimization'| and
  339acts accordingly to a simple strategy. If the flag is set to |off| and
  340there are ``dangerous'' axioms like transitivity, we set the flag to |on|
  341and proceed. Conversely, if the flag is set to |on| and there are no
  342self recursive clauses such as transitivity, we set the flag to |off| and
  343proceed. In all other cases, we simply go on. Thus, this predicate is merely
  344a case analysis. The messages about flag setting go to the respective streams
  345as Prolog comments.
  346
  347\PL*/
  348
  349check_options(Stream):-
  350	( ( \+ is_option('Tom:theory_optimization') ,
  351	     constraint((_AnyPredicate / _AnyArity),_AnyClause,transitive ) ->
  352	     set_option('Tom:theory_optimization' = on),
  353	     writeln(Stream,"
  354% I suggest to optimize the theory - changed the flag to on.")
  355	  )
  356	; ( is_option('Tom:theory_optimization') ,
  357	     \+ constraint((_APredicate / _AnArity) ,_AClause, transitive) ->
  358	       set_option('Tom:theory_optimization' = off),
  359	       writeln(Stream,"
  360% I don't believe it is necessary to optimize the theory - changed the flag to off.")
  361	  )
  362	; true
  363	).
  364/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  365
  366\Predicate write_descriptors/1(+Unificator).
  367
  368
  369\PL*/
  370
  371write_descriptors(Unificator):-
  372	open('tom_c_descriptors.pl',write,DStream),
  373	writeclause(DStream, :- module('tom_c_descriptors')),
  374	nl(DStream),
  375	writeclause(DStream, :- compile(library(capri))),
  376	writeclause(DStream, :- lib(matrix)),
  377	nl(DStream),
  378	concat_atom([Unificator,'.pl'],FullName),
  379	writeclause(DStream,force_option('ProCom::post_link',[[FullName]])),
  380	writeclause(DStream,force_option('ProCom::path',['path.pl'])),
  381	writeclause(DStream,force_option(equality,[off])),
  382	writeclause(DStream,force_option(remove_unreached_clauses,[off])),
  383	writeclause(DStream,force_option(find_all_connections,[on])),
  384	writeclause(DStream,force_option(connect_weak_unifyable,[off])),
  385	writeclause(DStream,force_option(reductions,[[]])),
  386	writeclause(DStream,force_option(search,[iterative_deepening(1, 1, 1)])),
  387	nl(DStream),
  388	writeclause(DStream,(make_pred(A, B, C) :-
  389	( A =.. [D, E],
  390	functor(E, F, G),
  391	functor(H, F, G),
  392	(
  393	    D = (--)
  394	->
  395	    I = (++)
  396	;
  397	    (
  398		D = (++)
  399	    ->
  400		I = (--)
  401	    )
  402	),
  403	C =.. [I, H],
  404	B =.. [D, H]))),
  405	nl(DStream),
  406	writeclause(DStream, look_for_entry(A, B, C, D) :-
  407	(make_pred(A, B, C),
  408	'Contrapositive'(C,_, D))),
  409	nl(DStream),
  410	Unification1 =.. [Unificator, K, M],
  411	writeclause(DStream, descriptor((proof(reduction(Index3,K -> L)),
  412	   template(K, goal),
  413	   call(make_pred(K,M,L)),
  414	   template(L, path(Index3)),
  415	   constructor(Unification1)))),
  416	nl(DStream),
  417	Unification2 =.. [Unificator, O, Q],
  418	writeclause(DStream, descriptor((proof(connection(Index4, O -> P)),
  419	   template(O, goal),
  420	   call(look_for_entry(O,Q,P,Index4)),
  421	   template(P, extension(Index4)),
  422	   constructor(Unification2)))),
  423	close(DStream),
  424	set_option(prover = procom(tom_c_descriptors)).
  425
  426
  427/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  428
  429\EndProlog */