4
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 ).
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
116
117write_one_clause(Stream,Formula):-
118 build_clause(Formula,PrologClause),
119 writeclause(Stream,PrologClause).
120
132reorder((Conclusion :- Premise),Premises,Conclusions,Constraints):-
133 reorder(Premise,[],[],Premises,NewConstraints,p),
134 reorder(Conclusion,[],NewConstraints,Conclusions,Constraints,c).
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 ).
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
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
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 ].
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
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
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
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 ).
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