1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
|
diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/Makefile LADR-2009-11A/Makefile
--- LADR-2009-11A.orig/Makefile 2007-10-22 23:33:12.000000000 +0200
+++ LADR-2009-11A/Makefile 2009-12-26 13:50:32.285406118 +0100
@@ -2,7 +2,7 @@
@echo See README.make
all:
- cd ladr && $(MAKE) lib
+ cd ladr && $(MAKE) lib XFLAGS+=-D_REENTRANT
cd mace4.src && $(MAKE) all
cd provers.src && $(MAKE) all
cd apps.src && $(MAKE) all
@@ -12,7 +12,7 @@
@echo ""
ladr lib:
- cd ladr && $(MAKE) lib
+ cd ladr && $(MAKE) lib XFLAGS+=-D_REENTRANT
test1:
bin/prover9 -f prover9.examples/x2.in | bin/prooftrans parents_only
diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/apps.src/Makefile LADR-2009-11A/apps.src/Makefile
--- LADR-2009-11A.orig/apps.src/Makefile 2009-04-17 16:46:39.000000000 +0200
+++ LADR-2009-11A/apps.src/Makefile 2009-12-26 13:50:32.335405804 +0100
@@ -16,16 +16,16 @@
all: ladr apps install realclean
ladr:
- cd ../ladr && $(MAKE) libladr.a
+ cd ../ladr && $(MAKE) libladr.la
clean:
- /bin/rm -f *.o
+ libtool --mode=clean /bin/rm -f *.o
realclean:
- /bin/rm -f *.o $(PROGRAMS)
+ libtool --mode=clean /bin/rm -f *.o $(PROGRAMS)
install:
- /bin/mv $(PROGRAMS) ../bin
+ libtool --mode=install /bin/cp $(PROGRAMS) `pwd`/../bin
tags:
etags *.c ../ladr/*.c
@@ -33,85 +33,85 @@
apps: $(PROGRAMS)
test: test.o
- $(CC) $(CFLAGS) -o test test.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o test test.o ../ladr/libladr.la
interpformat: interpformat.o
- $(CC) $(CFLAGS) -o interpformat interpformat.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o interpformat interpformat.o ../ladr/libladr.la
prooftrans: prooftrans.o
- $(CC) $(CFLAGS) -o prooftrans prooftrans.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o prooftrans prooftrans.o ../ladr/libladr.la
directproof: directproof.o
- $(CC) $(CFLAGS) -o directproof directproof.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o directproof directproof.o ../ladr/libladr.la
test_clause_eval: test_clause_eval.o
- $(CC) $(CFLAGS) -o test_clause_eval test_clause_eval.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o test_clause_eval test_clause_eval.o ../ladr/libladr.la
test_complex: test_complex.o
- $(CC) $(CFLAGS) -o test_complex test_complex.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o test_complex test_complex.o ../ladr/libladr.la
complex: complex.o
- $(CC) $(CFLAGS) -o complex complex.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o complex complex.o ../ladr/libladr.la
latfilter: latfilter.o
- $(CC) $(CFLAGS) -o latfilter latfilter.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o latfilter latfilter.o ../ladr/libladr.la
olfilter: olfilter.o
- $(CC) $(CFLAGS) -o olfilter olfilter.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o olfilter olfilter.o ../ladr/libladr.la
unfast: unfast.o
- $(CC) $(CFLAGS) -o unfast unfast.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o unfast unfast.o ../ladr/libladr.la
upper-covers: upper-covers.o
- $(CC) $(CFLAGS) -o upper-covers upper-covers.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o upper-covers upper-covers.o ../ladr/libladr.la
miniscope: miniscope.o
- $(CC) $(CFLAGS) -o miniscope miniscope.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o miniscope miniscope.o ../ladr/libladr.la
isofilter0: isofilter0.o
- $(CC) $(CFLAGS) -o isofilter0 isofilter0.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o isofilter0 isofilter0.o ../ladr/libladr.la
isofilter: isofilter.o
- $(CC) $(CFLAGS) -o isofilter isofilter.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o isofilter isofilter.o ../ladr/libladr.la
isofilter2: isofilter2.o
- $(CC) $(CFLAGS) -o isofilter2 isofilter2.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o isofilter2 isofilter2.o ../ladr/libladr.la
dprofiles: dprofiles.o
- $(CC) $(CFLAGS) -o dprofiles dprofiles.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o dprofiles dprofiles.o ../ladr/libladr.la
renamer: renamer.o
- $(CC) $(CFLAGS) -o renamer renamer.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o renamer renamer.o ../ladr/libladr.la
rewriter: rewriter.o
- $(CC) $(CFLAGS) -o rewriter rewriter.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o rewriter rewriter.o ../ladr/libladr.la
idfilter: idfilter.o
- $(CC) $(CFLAGS) -o idfilter idfilter.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o idfilter idfilter.o ../ladr/libladr.la
clausefilter: clausefilter.o
- $(CC) $(CFLAGS) -o clausefilter clausefilter.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o clausefilter clausefilter.o ../ladr/libladr.la
interpfilter: interpfilter.o
- $(CC) $(CFLAGS) -o interpfilter interpfilter.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o interpfilter interpfilter.o ../ladr/libladr.la
clausetester: clausetester.o
- $(CC) $(CFLAGS) -o clausetester clausetester.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o clausetester clausetester.o ../ladr/libladr.la
mirror-flip: mirror-flip.o
- $(CC) $(CFLAGS) -o mirror-flip mirror-flip.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o mirror-flip mirror-flip.o ../ladr/libladr.la
perm3: perm3.o
- $(CC) $(CFLAGS) -o perm3 perm3.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o perm3 perm3.o ../ladr/libladr.la
sigtest: sigtest.o
- $(CC) $(CFLAGS) -o sigtest sigtest.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o sigtest sigtest.o ../ladr/libladr.la
rewriter2: rewriter2.o
- $(CC) $(CFLAGS) -o rewriter2 rewriter2.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o rewriter2 rewriter2.o ../ladr/libladr.la
gen_trc_defs: gen_trc_defs.o
- $(CC) $(CFLAGS) -o gen_trc_defs gen_trc_defs.o ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o gen_trc_defs gen_trc_defs.o ../ladr/libladr.la
diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/ladr/Makefile LADR-2009-11A/ladr/Makefile
--- LADR-2009-11A.orig/ladr/Makefile 2009-10-28 15:22:04.000000000 +0100
+++ LADR-2009-11A/ladr/Makefile 2009-12-26 13:50:32.453408456 +0100
@@ -11,46 +11,49 @@
# CFLAGS = $(XFLAGS) -pg -O -Wall
# CFLAGS = $(XFLAGS) -Wall -pedantic
-BASE_OBJ = order.o clock.o nonport.o\
- fatal.o ibuffer.o memory.o hash.o string.o strbuf.o\
- glist.o options.o symbols.o avltree.o
-TERM_OBJ = term.o termflag.o listterm.o tlist.o flatterm.o multiset.o\
- termorder.o parse.o accanon.o
-UNIF_OBJ = unify.o fpalist.o fpa.o discrim.o discrimb.o discrimw.o\
- dioph.o btu.o btm.o mindex.o basic.o attrib.o
-CLAS_OBJ = formula.o definitions.o literals.o topform.o clist.o\
- clauseid.o clauses.o\
- just.o cnf.o clausify.o parautil.o\
- pindex.o compress.o\
- maximal.o lindex.o weight.o weight2.o\
- int_code.o features.o di_tree.o fastparse.o\
- random.o subsume.o clause_misc.o clause_eval.o complex.o
-INFE_OBJ = dollar.o flatdemod.o demod.o clash.o resolve.o paramod.o\
- backdemod.o\
- hints.o ac_redun.o xproofs.o ivy.o
-MODL_OBJ = interp.o
-MISC_OBJ = std_options.o banner.o ioutil.o tptp_trans.o top_input.o
+BASE_OBJ = order.lo clock.lo nonport.lo\
+ fatal.lo ibuffer.lo memory.lo hash.lo string.lo strbuf.lo\
+ glist.lo options.lo symbols.lo avltree.lo
+TERM_OBJ = term.lo termflag.lo listterm.lo tlist.lo flatterm.lo multiset.lo\
+ termorder.lo parse.lo accanon.lo
+UNIF_OBJ = unify.lo fpalist.lo fpa.lo discrim.lo discrimb.lo discrimw.lo\
+ dioph.lo btu.lo btm.lo mindex.lo basic.lo attrib.lo
+CLAS_OBJ = formula.lo definitions.lo literals.lo topform.lo clist.lo\
+ clauseid.lo clauses.lo\
+ just.lo cnf.lo clausify.lo parautil.lo\
+ pindex.lo compress.lo\
+ maximal.lo lindex.lo weight.lo weight2.lo\
+ int_code.lo features.lo di_tree.lo fastparse.lo\
+ random.lo subsume.lo clause_misc.lo clause_eval.lo complex.lo
+INFE_OBJ = dollar.lo flatdemod.lo demod.lo clash.lo resolve.lo paramod.lo\
+ backdemod.lo\
+ hints.lo ac_redun.lo xproofs.lo ivy.lo
+MODL_OBJ = interp.lo
+MISC_OBJ = std_options.lo banner.lo ioutil.lo tptp_trans.lo top_input.lo
OBJECTS = $(BASE_OBJ) $(TERM_OBJ) $(UNIF_OBJ) $(CLAS_OBJ)\
$(INFE_OBJ) $(MODL_OBJ) $(MISC_OBJ)
-libladr.a: $(OBJECTS)
- $(AR) rs libladr.a $(OBJECTS)
+libladr.la: $(OBJECTS)
+ libtool --mode=link gcc -shared -rpath /usr/lib -version-info 4:0:0 -o libladr.la $(OBJECTS) -lm
+
+%.lo: %.c
+ libtool --mode=compile gcc -c $(CFLAGS) $(XFLAGS) -o $@ $<
##############################################################################
lib ladr libladr:
- $(MAKE) libladr.a
+ $(MAKE) libladr.la
dep:
util/make_dep $(OBJECTS)
clean:
- /bin/rm -f *.o
+ libtool --mode=clean /bin/rm -f *.lo
realclean:
- /bin/rm -f *.o *.a
+ libtool --mode=clean /bin/rm -f *.lo *.la
protos:
util/make_protos $(OBJECTS)
@@ -67,156 +70,156 @@
# The rest of the file is generated automatically by util/make_dep
-order.o: order.h
+order.lo: order.h
-clock.o: clock.h string.h memory.h fatal.h header.h
+clock.lo: clock.h string.h memory.h fatal.h header.h
-nonport.o: nonport.h
+nonport.lo: nonport.h
-fatal.o: fatal.h header.h
+fatal.lo: fatal.h header.h
-ibuffer.o: ibuffer.h fatal.h header.h
+ibuffer.lo: ibuffer.h fatal.h header.h
-memory.o: memory.h fatal.h header.h
+memory.lo: memory.h fatal.h header.h
-hash.o: hash.h memory.h fatal.h header.h
+hash.lo: hash.h memory.h fatal.h header.h
-string.o: string.h memory.h fatal.h header.h
+string.lo: string.h memory.h fatal.h header.h
-strbuf.o: strbuf.h string.h memory.h fatal.h header.h
+strbuf.lo: strbuf.h string.h memory.h fatal.h header.h
-glist.o: glist.h order.h string.h memory.h fatal.h header.h
+glist.lo: glist.h order.h string.h memory.h fatal.h header.h
-options.o: options.h string.h memory.h fatal.h header.h
+options.lo: options.h string.h memory.h fatal.h header.h
-symbols.o: symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+symbols.lo: symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-avltree.o: avltree.h memory.h order.h fatal.h header.h
+avltree.lo: avltree.h memory.h order.h fatal.h header.h
-term.o: term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+term.lo: term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-termflag.o: termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+termflag.lo: termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-listterm.o: listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+listterm.lo: listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-tlist.o: tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+tlist.lo: tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-flatterm.o: flatterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+flatterm.lo: flatterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-multiset.o: multiset.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+multiset.lo: multiset.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-termorder.o: termorder.h flatterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+termorder.lo: termorder.h flatterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-parse.o: parse.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+parse.lo: parse.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-accanon.o: accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+accanon.lo: accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
-unify.o: unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+unify.lo: unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-fpalist.o: fpalist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+fpalist.lo: fpalist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-fpa.o: fpa.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+fpa.lo: fpa.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-discrim.o: discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+discrim.lo: discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-discrimb.o: discrimb.h discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+discrimb.lo: discrimb.h discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-discrimw.o: discrimw.h discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+discrimw.lo: discrimw.h discrim.h unify.h index.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-dioph.o: dioph.h
+dioph.lo: dioph.h
-btu.o: btu.h dioph.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+btu.lo: btu.h dioph.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-btm.o: btm.h unify.h accanon.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h termorder.h flatterm.h
+btm.lo: btm.h unify.h accanon.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h termorder.h flatterm.h
-mindex.o: mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
+mindex.lo: mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
-basic.o: basic.h unify.h termflag.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+basic.lo: basic.h unify.h termflag.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-attrib.o: attrib.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+attrib.lo: attrib.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-formula.o: formula.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+formula.lo: formula.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
-definitions.o: definitions.h formula.h topform.h clauseid.h just.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h literals.h maximal.h parse.h
+definitions.lo: definitions.h formula.h topform.h clauseid.h just.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h literals.h maximal.h parse.h
-literals.o: literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+literals.lo: literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-topform.o: topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+topform.lo: topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
-clist.o: clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+clist.lo: clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
-clauseid.o: clauseid.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+clauseid.lo: clauseid.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
-clauses.o: clauses.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+clauses.lo: clauses.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
-just.o: just.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+just.lo: just.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
-cnf.o: cnf.h formula.h clock.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+cnf.lo: cnf.h formula.h clock.h attrib.h tlist.h termorder.h hash.h unify.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
-clausify.o: clausify.h topform.h cnf.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clock.h
+clausify.lo: clausify.h topform.h cnf.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clock.h
-parautil.o: parautil.h
+parautil.lo: parautil.h
-pindex.o: pindex.h clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+pindex.lo: pindex.h clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
-compress.o: compress.h parautil.h
+compress.lo: compress.h parautil.h
-maximal.o: maximal.h literals.h termorder.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+maximal.lo: maximal.h literals.h termorder.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
-lindex.o: lindex.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
+lindex.lo: lindex.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
-weight.o: weight.h literals.h unify.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h listterm.h
+weight.lo: weight.h literals.h unify.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h listterm.h
-weight2.o: weight2.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+weight2.lo: weight2.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-int_code.o: int_code.h just.h ibuffer.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+int_code.lo: int_code.h just.h ibuffer.h clauseid.h parse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
-features.o: features.h literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
+features.lo: features.h literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h
-di_tree.o: di_tree.h features.h topform.h literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h attrib.h formula.h maximal.h unify.h listterm.h termorder.h hash.h flatterm.h
+di_tree.lo: di_tree.h features.h topform.h literals.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h attrib.h formula.h maximal.h unify.h listterm.h termorder.h hash.h flatterm.h
-fastparse.o: fastparse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+fastparse.lo: fastparse.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
-random.o: random.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+random.lo: random.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
-subsume.o: subsume.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
+subsume.lo: subsume.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h
-clause_misc.o: clause_misc.h clist.h mindex.h just.h basic.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h
+clause_misc.lo: clause_misc.h clist.h mindex.h just.h basic.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h
-clause_eval.o: clause_eval.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+clause_eval.lo: clause_eval.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
-complex.o: complex.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+complex.lo: complex.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
-dollar.o: dollar.h clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
+dollar.lo: dollar.h clist.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h
-flatdemod.o: flatdemod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
+flatdemod.lo: flatdemod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
-demod.o: demod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
+demod.lo: demod.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
-clash.o: clash.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
+clash.lo: clash.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h
-resolve.o: resolve.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
+resolve.lo: resolve.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
-paramod.o: paramod.h resolve.h basic.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
+paramod.lo: paramod.h resolve.h basic.h clash.h lindex.h mindex.h parautil.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h maximal.h topform.h literals.h tlist.h attrib.h formula.h hash.h
-backdemod.o: backdemod.h demod.h clist.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h topform.h literals.h attrib.h formula.h maximal.h tlist.h hash.h
+backdemod.lo: backdemod.h demod.h clist.h parautil.h mindex.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h topform.h literals.h attrib.h formula.h maximal.h tlist.h hash.h
-hints.o: hints.h subsume.h clist.h backdemod.h resolve.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h demod.h clash.h
+hints.lo: hints.h subsume.h clist.h backdemod.h resolve.h parautil.h lindex.h features.h mindex.h maximal.h topform.h fpa.h discrimb.h discrimw.h btu.h btm.h unify.h index.h fpalist.h listterm.h termflag.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h discrim.h dioph.h accanon.h termorder.h flatterm.h literals.h tlist.h attrib.h formula.h hash.h demod.h clash.h
-ac_redun.o: ac_redun.h parautil.h accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
+ac_redun.lo: ac_redun.h parautil.h accanon.h termflag.h termorder.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h flatterm.h
-xproofs.o: xproofs.h clauses.h clause_misc.h paramod.h subsume.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h resolve.h clash.h lindex.h parautil.h features.h
+xproofs.lo: xproofs.h clauses.h clause_misc.h paramod.h subsume.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h resolve.h clash.h lindex.h parautil.h features.h
-ivy.o: ivy.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h resolve.h clash.h lindex.h parautil.h features.h
+ivy.lo: ivy.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h unify.h listterm.h termorder.h hash.h flatterm.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h parse.h resolve.h clash.h lindex.h parautil.h features.h
-interp.o: interp.h parse.h topform.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h
+interp.lo: interp.h parse.h topform.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h
-std_options.o: std_options.h options.h symbols.h clock.h string.h memory.h fatal.h header.h strbuf.h glist.h order.h
+std_options.lo: std_options.h options.h symbols.h clock.h string.h memory.h fatal.h header.h strbuf.h glist.h order.h
-banner.o: banner.h nonport.h clock.h string.h memory.h fatal.h header.h
+banner.lo: banner.h nonport.h clock.h string.h memory.h fatal.h header.h
-ioutil.o: ioutil.h parse.h fastparse.h ivy.h clausify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h
+ioutil.lo: ioutil.h parse.h fastparse.h ivy.h clausify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h
-tptp_trans.o: tptp_trans.h ioutil.h clausify.h parse.h fastparse.h ivy.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h
+tptp_trans.lo: tptp_trans.h ioutil.h clausify.h parse.h fastparse.h ivy.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h
-top_input.o: top_input.h ioutil.h std_options.h tptp_trans.h parse.h fastparse.h ivy.h clausify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h options.h
+top_input.lo: top_input.h ioutil.h std_options.h tptp_trans.h parse.h fastparse.h ivy.h clausify.h listterm.h term.h symbols.h strbuf.h glist.h string.h memory.h fatal.h header.h order.h topform.h literals.h attrib.h formula.h maximal.h termflag.h tlist.h unify.h termorder.h hash.h flatterm.h xproofs.h clauses.h clause_misc.h paramod.h subsume.h clist.h mindex.h just.h basic.h fpa.h discrimb.h discrimw.h btu.h btm.h index.h fpalist.h discrim.h dioph.h accanon.h clauseid.h resolve.h clash.h lindex.h parautil.h features.h cnf.h clock.h options.h
diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/mace4.src/Makefile LADR-2009-11A/mace4.src/Makefile
--- LADR-2009-11A.orig/mace4.src/Makefile 2009-04-17 16:46:46.000000000 +0200
+++ LADR-2009-11A/mace4.src/Makefile 2009-12-26 13:50:32.373406096 +0100
@@ -26,11 +26,11 @@
$(MAKE) libmace4.a
ladr:
- cd ../ladr && $(MAKE) libladr.a
+ cd ../ladr && $(MAKE) libladr.la
$(MAKE) clean
mace4: libmace4.a mace4.o $(OBJECTS)
- $(CC) $(CFLAGS) -o mace4 mace4.o libmace4.a ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o mace4 mace4.o libmace4.a ../ladr/libladr.la
$(OBJECTS): estack.h syms.h ground.h propagate.h mstate.h msearch.h
@@ -38,10 +38,10 @@
etags *.c ../ladr/*.c
clean:
- /bin/rm -f *.o
+ libtool --mode=clean /bin/rm -f *.o
realclean:
- /bin/rm -f *.o *.a mace4
+ libtool --mode=clean /bin/rm -f *.o *.a mace4
install:
- /bin/mv mace4 ../bin
+ libtool --mode=install /bin/cp mace4 `pwd`/../bin
diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/provers.src/Makefile LADR-2009-11A/provers.src/Makefile
--- LADR-2009-11A.orig/provers.src/Makefile 2009-10-28 15:22:15.000000000 +0100
+++ LADR-2009-11A/provers.src/Makefile 2009-12-26 13:50:32.420530288 +0100
@@ -41,13 +41,13 @@
$(MAKE) clean
install:
- /bin/cp -p $(PROGRAMS) ../bin
+ libtool --mode=install /bin/cp -p $(PROGRAMS) `pwd`/../bin
clean:
- /bin/rm -f *.o
+ libtool --mode=clean /bin/rm -f *.o
realclean:
- /bin/rm -f *.o $(PROGRAMS)
+ libtool --mode=clean /bin/rm -f *.o $(PROGRAMS)
protos:
util/make_protos $(OBJECTS)
@@ -63,34 +63,34 @@
$(MAKE) prover9
prover9: prover9.o $(OBJECTS)
- $(CC) $(CFLAGS) -lm -o prover9 prover9.o $(OBJECTS) ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o prover9 prover9.o $(OBJECTS) ../ladr/libladr.la
fof-prover9: fof-prover9.o $(OBJECTS)
- $(CC) $(CFLAGS) -lm -o fof-prover9 fof-prover9.o $(OBJECTS) ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o fof-prover9 fof-prover9.o $(OBJECTS) ../ladr/libladr.la
ladr_to_tptp: ladr_to_tptp.o $(OBJECTS)
- $(CC) $(CFLAGS) -lm -o ladr_to_tptp ladr_to_tptp.o $(OBJECTS) ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o ladr_to_tptp ladr_to_tptp.o $(OBJECTS) ../ladr/libladr.la
tptp_to_ladr: tptp_to_ladr.o $(OBJECTS)
- $(CC) $(CFLAGS) -lm -o tptp_to_ladr tptp_to_ladr.o $(OBJECTS) ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o tptp_to_ladr tptp_to_ladr.o $(OBJECTS) ../ladr/libladr.la
autosketches4: autosketches4.o $(OBJECTS)
- $(CC) $(CFLAGS) -lm -o autosketches4 autosketches4.o $(OBJECTS) ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o autosketches4 autosketches4.o $(OBJECTS) ../ladr/libladr.la
newauto: newauto.o $(OBJECTS)
- $(CC) $(CFLAGS) -lm -o newauto newauto.o $(OBJECTS) ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o newauto newauto.o $(OBJECTS) ../ladr/libladr.la
newsax: newsax.o $(OBJECTS)
- $(CC) $(CFLAGS) -lm -o newsax newsax.o $(OBJECTS) ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o newsax newsax.o $(OBJECTS) ../ladr/libladr.la
cgrep: cgrep.o $(OBJECTS)
- $(CC) $(CFLAGS) -o cgrep cgrep.o $(OBJECTS) ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o cgrep cgrep.o $(OBJECTS) ../ladr/libladr.la
mprover: mprover.o $(OBJECTS)
- $(CC) $(CFLAGS) -o mprover mprover.o $(OBJECTS) ../ladr/libladr.a ../mace4.src/libmace4.a
+ libtool --mode=link $(CC) $(CFLAGS) -o mprover mprover.o $(OBJECTS) ../ladr/libladr.la ../mace4.src/libmace4.la
iterate4: iterate4.o $(OBJECTS)
- $(CC) $(CFLAGS) -o iterate4 iterate4.o $(OBJECTS) ../ladr/libladr.a
+ libtool --mode=link $(CC) $(CFLAGS) -o iterate4 iterate4.o $(OBJECTS) ../ladr/libladr.la
prover9.o mprover.o iterate4.o autosketches4.o fof-prover9.o: search.h utilities.h forward_subsume.h giv_select.h white_black.h demodulate.h actions.h index_lits.h pred_elim.h unfold.h provers.h
diff -U 3 -H -b -E -d -r -N -- LADR-2009-11A.orig/test.src/Makefile LADR-2009-11A/test.src/Makefile
--- LADR-2009-11A.orig/test.src/Makefile 2007-03-06 21:27:59.000000000 +0100
+++ LADR-2009-11A/test.src/Makefile 2009-12-26 13:50:32.416531165 +0100
@@ -17,13 +17,13 @@
ladr:
make clean
- cd ../ladr && $(MAKE) libladr.a
+ cd ../ladr && $(MAKE) libladr.la
clean:
- /bin/rm -f *.o
+ libtool --mode=clean /bin/rm -f *.o
realclean:
- /bin/rm -f *.o $(PROGRAMS)
+ libtool --mode=clean /bin/rm -f *.o $(PROGRAMS)
tags:
etags *.c ../ladr/*.c
@@ -31,8 +31,8 @@
apps: $(PROGRAMS)
avltest: avltest.o
- $(CC) $(CFLAGS) -o avltest avltest.o ../ladr/libladr.a -lm
+ libtool --mode=link $(CC) $(CFLAGS) -o avltest avltest.o ../ladr/libladr.la -lm
tptp_test: tptp_test.o
- $(CC) $(CFLAGS) -o tptp_test tptp_test.o ../ladr/libladr.a -lm
+ libtool --mode=link $(CC) $(CFLAGS) -o tptp_test tptp_test.o ../ladr/libladr.la -lm
|
