ladr-libtoolize.diff 41 KB

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