← Back to branch summary

~ubuntu-branches/ubuntu/saucy/ladr/saucy

« back to all changes in this revision

Viewing changes to .pc/01-libtoolise.patch/provers.src/Makefile

  • Committer: Package Import Robot
  • Author(s): Frank Lichtenheld
  • Date: 2013-05-25 11:43:32 UTC
  • mfrom: (5.1.5 sid)
  • Revision ID: package-import@ubuntu.com-20130525114332-lkzco1dti2hwrf7v
Tags: 0.0.200911a-2
* QA upload.
* Upload to unstable.
* Change maintainer to QA group.

Show diffs side-by-side

added added

removed removed

Lines of Context:
.pc/01-libtoolise.patch/provers.src/Makefile
 
1
# LADR/prover9.src
 
2
 
 
3
CC = gcc
 
4
 
 
5
# XFLAGS can be specified on the command line (see XFLAGS below)
 
6
 
 
7
CFLAGS = $(XFLAGS) -O -Wall
 
8
# CFLAGS = $(XFLAGS) -O6 -Wall
 
9
# CFLAGS = $(XFLAGS) -g  -O -Wall
 
10
# CFLAGS = $(XFLAGS) -g -O0 -Wall
 
11
# CFLAGS = $(XFLAGS) -pg -O -Wall
 
12
# CFLAGS = $(XFLAGS) -Wall -pedantic
 
13
 
 
14
PRVR_OBJ = index_lits.o forward_subsume.o demodulate.o\
 
15
           pred_elim.o unfold.o semantics.o\
 
16
           giv_select.o white_black.o actions.o\
 
17
           search.o\
 
18
           utilities.o\
 
19
           provers.o\
 
20
           foffer.o
 
21
 
 
22
OBJECTS = $(PRVR_OBJ)
 
23
 
 
24
# PROGRAMS = mprover iterate4
 
25
 
 
26
PROGRAMS = prover9 fof-prover9 autosketches4 newauto newsax\
 
27
           ladr_to_tptp tptp_to_ladr
 
28
 
 
29
##############################################################################
 
30
 
 
31
all: libs $(PROGRAMS) install clean
 
32
 
 
33
libs: ladr libmace4
 
34
 
 
35
ladr libladr:
 
36
        cd ../ladr && $(MAKE) libladr
 
37
        $(MAKE) clean
 
38
 
 
39
libmace libmace4:
 
40
        cd ../mace4.src && $(MAKE) libmace4
 
41
        $(MAKE) clean
 
42
 
 
43
install:
 
44
        /bin/cp -p $(PROGRAMS) ../bin
 
45
 
 
46
clean:
 
47
        /bin/rm -f *.o
 
48
 
 
49
realclean:
 
50
        /bin/rm -f *.o $(PROGRAMS)
 
51
 
 
52
protos:
 
53
        util/make_protos $(OBJECTS)
 
54
 
 
55
dep:
 
56
        util/make_dep $(OBJECTS)
 
57
 
 
58
tags:
 
59
        etags *.c ../ladr/*.c
 
60
 
 
61
prover:
 
62
        /bin/rm -f prover9
 
63
        $(MAKE) prover9
 
64
 
 
65
prover9: prover9.o $(OBJECTS)
 
66
        $(CC) $(CFLAGS) -lm -o prover9 prover9.o $(OBJECTS) ../ladr/libladr.a
 
67
 
 
68
fof-prover9: fof-prover9.o $(OBJECTS)
 
69
        $(CC) $(CFLAGS) -lm -o fof-prover9 fof-prover9.o $(OBJECTS) ../ladr/libladr.a
 
70
 
 
71
ladr_to_tptp: ladr_to_tptp.o $(OBJECTS)
 
72
        $(CC) $(CFLAGS) -lm -o ladr_to_tptp ladr_to_tptp.o $(OBJECTS) ../ladr/libladr.a
 
73
 
 
74
tptp_to_ladr: tptp_to_ladr.o $(OBJECTS)
 
75
        $(CC) $(CFLAGS) -lm -o tptp_to_ladr tptp_to_ladr.o $(OBJECTS) ../ladr/libladr.a
 
76
 
 
77
autosketches4: autosketches4.o $(OBJECTS)
 
78
        $(CC) $(CFLAGS) -lm -o autosketches4 autosketches4.o $(OBJECTS) ../ladr/libladr.a
 
79
 
 
80
newauto: newauto.o $(OBJECTS)
 
81
        $(CC) $(CFLAGS) -lm -o newauto newauto.o $(OBJECTS) ../ladr/libladr.a
 
82
 
 
83
newsax: newsax.o $(OBJECTS)
 
84
        $(CC) $(CFLAGS) -lm -o newsax newsax.o $(OBJECTS) ../ladr/libladr.a
 
85
 
 
86
cgrep: cgrep.o $(OBJECTS)
 
87
        $(CC) $(CFLAGS) -o cgrep cgrep.o $(OBJECTS) ../ladr/libladr.a
 
88
 
 
89
mprover: mprover.o $(OBJECTS)
 
90
        $(CC) $(CFLAGS) -o mprover mprover.o $(OBJECTS) ../ladr/libladr.a ../mace4.src/libmace4.a
 
91
 
 
92
iterate4: iterate4.o $(OBJECTS)
 
93
        $(CC) $(CFLAGS) -o iterate4 iterate4.o $(OBJECTS) ../ladr/libladr.a
 
94
 
 
95
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
 
96
 
 
97
# The rest of the file is generated automatically by util/make_dep
 
98
 
 
99
index_lits.o:           index_lits.h ../ladr/clock.h ../ladr/subsume.h ../ladr/di_tree.h
 
100
 
 
101
forward_subsume.o:      forward_subsume.h ../ladr/subsume.h ../ladr/clock.h
 
102
 
 
103
demodulate.o:           demodulate.h ../ladr/ladr.h
 
104
 
 
105
pred_elim.o:    pred_elim.h ../ladr/subsume.h ../ladr/resolve.h ../ladr/clauses.h ../ladr/clause_misc.h ../ladr/ioutil.h
 
106
 
 
107
unfold.o:       unfold.h ../ladr/parautil.h ../ladr/clist.h ../ladr/ioutil.h
 
108
 
 
109
semantics.o:    semantics.h ../ladr/interp.h ../ladr/ioutil.h
 
110
 
 
111
giv_select.o:           giv_select.h search-structures.h
 
112
 
 
113
white_black.o:          white_black.h search-structures.h
 
114
 
 
115
actions.o:      actions.h search-structures.h
 
116
 
 
117
search.o:       search.h search-structures.h semantics.h pred_elim.h demodulate.h index_lits.h forward_subsume.h unfold.h actions.h giv_select.h white_black.h utilities.h ../ladr/interp.h ../ladr/ioutil.h ../ladr/subsume.h ../ladr/resolve.h ../ladr/clauses.h ../ladr/clause_misc.h ../ladr/ioutil.h ../ladr/ladr.h ../ladr/clock.h ../ladr/subsume.h ../ladr/di_tree.h ../ladr/subsume.h ../ladr/clock.h ../ladr/parautil.h ../ladr/clist.h ../ladr/ioutil.h
 
118
 
 
119
utilities.o:    utilities.h search-structures.h
 
120
 
 
121
provers.o:      provers.h search.h search-structures.h semantics.h pred_elim.h demodulate.h index_lits.h forward_subsume.h unfold.h actions.h giv_select.h white_black.h utilities.h ../ladr/interp.h ../ladr/ioutil.h ../ladr/subsume.h ../ladr/resolve.h ../ladr/clauses.h ../ladr/clause_misc.h ../ladr/ioutil.h ../ladr/ladr.h ../ladr/clock.h ../ladr/subsume.h ../ladr/di_tree.h ../ladr/subsume.h ../ladr/clock.h ../ladr/parautil.h ../ladr/clist.h ../ladr/ioutil.h
 
122
 
 
123
foffer.o:       foffer.h search.h search-structures.h semantics.h pred_elim.h demodulate.h index_lits.h forward_subsume.h unfold.h actions.h giv_select.h white_black.h utilities.h ../ladr/interp.h ../ladr/ioutil.h ../ladr/subsume.h ../ladr/resolve.h ../ladr/clauses.h ../ladr/clause_misc.h ../ladr/ioutil.h ../ladr/ladr.h ../ladr/clock.h ../ladr/subsume.h ../ladr/di_tree.h ../ladr/subsume.h ../ladr/clock.h ../ladr/parautil.h ../ladr/clist.h ../ladr/ioutil.h