1include Makefile.local
2
3# The list of Makefiles and other important script sources which must
4# be included in any distribution.
5DISTFILES = \
6Makefile \
7Makefile.std \
8Makefile.local.in \
9configure.ac \
10configure \
11config.guess \
12config.sub \
13install-sh \
14INSTALL \
15LICENSE.in \
16PEOPLE \
17README \
18VERSION \
19bin/unpack.in \
20bin/run_tests.in \
21bin/cvc2smt.in \
22doc/Doxyfile.in \
23doc/Makefile.in \
24doc/devel.dox \
25doc/mainpage.dox \
26doc/userdoc.dox \
27doc/theory_api.dox \
28doc/theory_api_flow.fig \
29src/Makefile \
30src/cvc3.pc.in \
31test/Makefile \
32test/george.h \
33test/george.cpp \
34test/main.cpp \
35testc/Makefile \
36testc/main.c \
37emacs/cvc-mode.el
38
39all:	build
40
41.PHONY: build
42
43build:
44	cd $(TOP)/src; $(MAKE) $(TARGET) VERSION=$(VERSION)
45ifeq ($(BUILD_JAVA),1)
46	cd $(TOP)/java; $(MAKE) $(TARGET) VERSION=$(VERSION)
47endif
48ifeq ($(CYGWIN),)
49ifndef TARGET
50	find $(TOP)/src '(' -name "*.h" -o -name "*.cpp" -o       \
51	                           -name "*.y" ')'       \
52                                ! -name "lexPL.cpp" ! -name "parsePL.cpp" \
53				-print  > FILES
54ifdef ETAGS
55	sed -e s/^/\'/ -e s/$$/\'/ FILES | xargs etags
56endif
57ifdef EBROWSE
58	ebrowse --files=FILES
59endif
60endif
61endif
62
63#Standard make targets
64.PHONY: depend spotty install
65
66depend:
67	$(MAKE) TARGET=depend
68
69spotty:
70	$(MAKE) TARGET=spotty
71
72install:
73	$(MAKE) TARGET=install
74
75# Special make targets for top Makefile
76.PHONY: update-web update-web-doc doc dist dist_src dist_bin ld_sh ld_csh
77
78update-web:
79	cp $(TOP)/webpage/*.html $(WEBDIR)
80	cp $(TOP)/webpage/*.jpg $(WEBDIR)
81	cp $(TOP)/webpage/*.css $(WEBDIR)
82
83update-web-doc: doc
84	cd $(TOP)/doc/html/; tar cvBf - . | (cd $(WEBDIR)/doc/; tar xvpBf -)
85
86doc:
87	cd $(TOP)/doc; $(MAKE)
88
89dist: dist_src
90# dist: dist_src dist_bin
91
92TMPFILE=$(TOP)/filelist.tmp
93TARDIR=cvc3-$(VERSION)
94TARFILE=$(TARDIR).tar.gz
95DISTTMPDIR=$(TOP)/dist-bak
96
97dist_src:
98	@mkdir -p $(DISTTMPDIR)
99ifndef DPLL_BASIC
100	@mv configure.ac configure $(DISTTMPDIR)
101	@cat $(DISTTMPDIR)/configure.ac | sed '/#BEGIN/,/#END/ d' > $(TOP)/configure.ac
102	@autoconf
103endif
104	@rm -rf $(TMPFILE); touch $(TMPFILE)
105	echo "Collecting top-level script files"
106	@echo $(DISTFILES) >> $(TMPFILE)
107	cd $(TOP)/src; $(MAKE) print_src FILELIST=$(TMPFILE)
108	cd $(TOP)/java; $(MAKE) print_src FILELIST=$(TMPFILE)
109	echo "Building " $(TARFILE)
110	@mkdir -p $(TARDIR)
111	@tar cf - `cat $(TMPFILE)` | (cd $(TARDIR); tar xf -)
112	@echo "$(VERSION)" > $(TARDIR)/VERSION
113	@tar zcfv $(TARFILE) $(TARDIR)
114ifndef DPLL_BASIC
115	@rm -f configure.ac configure
116	@mv $(DISTTMPDIR)/configure* $(TOP)
117endif
118	rm -rf $(TMPFILE) $(TARDIR) $(DISTTMPDIR)
119
120dist_bin:
121	echo "Sorry, binary distribution is not implemented yet"
122	exit 1
123
124# Generate LD_LIBRARY_PATH assignments for various shells.
125# When CVC is compiled with dynamic libraries, run
126#   `make ld_sh` or `make ld_tcsh`
127# before running cvc executable.
128
129ld_sh:
130	@echo "export LD_LIBRARY_PATH=$(TOP)/lib"
131ld_csh:
132	@echo "setenv LD_LIBRARY_PATH $(TOP)/lib"
133
134.PHONY: clean clean_gcov superclean_gcov clean_gprof distclean
135
136# Clean up all the files generated by gcov (including *.cpp.gcov)
137clean_gcov:
138	find src -name "*.da" -exec rm -f {} \;
139superclean_gcov: clean_gcov
140	find src -name "*.gcov" -exec rm -f {} \;
141	find src -name "*.bb" -exec rm -f {} \;
142	find src -name "*.bbg" -exec rm -f {} \;
143
144clean_gprof:
145	rm -f gmon.out
146
147clean:  superclean_gcov clean_gprof
148	$(MAKE) TARGET=clean
149	@rm -f $(REGRESS_LOG)
150	@rm -f $(TOP)/.test*
151
152distclean:
153	cd $(TOP)/src; $(MAKE) distclean
154	cd $(TOP)/doc; $(MAKE) distclean
155	cd $(TOP)/test; $(MAKE) distclean
156	cd $(TOP)/java; $(MAKE) distclean
157	rm -rf $(TOP)/test/bin $(TOP)/test/obj
158	cd $(TOP)/testc; $(MAKE) distclean
159	rm -rf $(TOP)/testc/bin $(TOP)/testc/obj
160	@rm -rf $(DISTTMPDIR)
161	@mkdir -p $(DISTTMPDIR)
162	@mv $(TOP)/bin/*.in $(DISTTMPDIR)
163	@-mv $(TOP)/bin/CVS $(DISTTMPDIR)
164	@-mv $(TOP)/bin/.cvsignore $(DISTTMPDIR)
165	rm -rf $(TOP)/bin
166	@mv $(DISTTMPDIR) $(TOP)/bin
167	@rm -rf $(DISTTMPDIR)
168	rm -f TAGS BROWSE FILES LICENSE Makefile.local
169	rm -rf $(TOP)/autom4te.cache
170	rm -f config.log config.status $(LICENSE_INFO_FILE)
171	rm -f $(REGRESS_LOG)
172	@rm -f $(TOP)/.test*
173	rm -rf $(TOP)/lib $(TOP)/obj
174
175# Regression tests: both for internal and presentation languages.
176.PHONY: regress regress0 regress1 regress2 regress3 regress4
177.PHONY: regressonly regressonly0 regressonly1 regressonly2 regressonly3 regressonly4
178
179REGRESS_LOG=regressions.log
180
181# The higher the level, the more tests are run (4 = all)
182REGRESS_TESTS0 = benchmarks
183REGRESS_TESTS1 = $(REGRESS_TESTS0)
184REGRESS_TESTS2 = $(REGRESS_TESTS1)
185REGRESS_TESTS3 = $(REGRESS_TESTS2)
186REGRESS_TESTS4 = $(REGRESS_TESTS3)
187REGRESS_TESTS = $(REGRESS_TESTS0)
188REGRESS_LEVEL=0
189# Program name
190PROGNAME=$(TOP)/bin/cvc3
191# Addiional options for run_tests script
192ifndef RUN_TESTS_OPTIONS
193ifeq ($(OPTIMIZED),1)
194  RUN_TESTS_OPTIONS=+rt
195endif
196endif
197# Define to max. number of seconds to run each executable.
198# 0 = no limit
199TIME_LIMIT=1200
200# Additional options
201CVC_OPTIONS=+stats
202ALL_OPTIONS= -l $(REGRESS_LEVEL) -vc $(PROGNAME) $(RUN_TESTS_OPTIONS) \
203             -t $(TIME_LIMIT) $(REGRESS_TESTS) -- $(CVC_OPTIONS)
204regress: build
205	cd $(TOP)/test; $(MAKE)
206	cd $(TOP)/testc; $(MAKE)
207	@echo "*********************************************************" \
208          | tee -a $(REGRESS_LOG)
209	@echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
210	@echo "C++ API test" | tee -a $(REGRESS_LOG)
211	@echo "*********************************************************" \
212          | tee -a $(REGRESS_LOG)
213	$(TOP)/test/bin/test $(REGRESS_LEVEL) 2>&1 \
214	  | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
215	@echo "*********************************************************" \
216          | tee -a $(REGRESS_LOG)
217	@echo "C API test" | tee -a $(REGRESS_LOG)
218	@echo "*********************************************************" \
219          | tee -a $(REGRESS_LOG)
220	$(TOP)/testc/bin/testc $(REGRESS_LEVEL)  2>&1 \
221	  | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
222	@rm -f $(TOP)/.test*
223ifeq ($(BUILD_JAVA),1)
224	@echo "*********************************************************" \
225          | tee -a $(REGRESS_LOG)
226	@echo "Java API test" | tee -a $(REGRESS_LOG)
227	@echo "*********************************************************" \
228          | tee -a $(REGRESS_LOG)
229	$(MAKE) -C java test 2>&1 \
230	  | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
231endif
232	@echo "*********************************************************" \
233          | tee -a $(REGRESS_LOG)
234	@echo "Regression tests" | tee -a $(REGRESS_LOG)
235	@echo "*********************************************************" \
236          | tee -a $(REGRESS_LOG)
237	$(TOP)/bin/run_tests $(ALL_OPTIONS)  2>&1 \
238	  | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
239	@echo "*********************************************************" \
240          | tee -a $(REGRESS_LOG)
241	@echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
242	@echo "*********************************************************" \
243          | tee -a $(REGRESS_LOG)
244
245regress0:
246	$(MAKE) regress REGRESS_LEVEL=0
247regress1:
248	$(MAKE) regress REGRESS_LEVEL=1 REGRESS_TESTS="$(REGRESS_TESTS1)"
249regress2:
250	$(MAKE) regress REGRESS_LEVEL=2 REGRESS_TESTS="$(REGRESS_TESTS2)"
251regress3:
252	$(MAKE) regress REGRESS_LEVEL=3 REGRESS_TESTS="$(REGRESS_TESTS3)" TIME_LIMIT=1500
253regress4:
254	$(MAKE) regress REGRESS_LEVEL=4 REGRESS_TESTS="$(REGRESS_TESTS4)" TIME_LIMIT=0
255
256regressonly: build
257	@echo "*********************************************************" \
258          | tee -a $(REGRESS_LOG)
259	@echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
260	@echo "*********************************************************" \
261          | tee -a $(REGRESS_LOG)
262	@echo "Regression tests" | tee -a $(REGRESS_LOG)
263	@echo "*********************************************************" \
264          | tee -a $(REGRESS_LOG)
265	$(TOP)/bin/run_tests $(ALL_OPTIONS)  2>&1 \
266	  | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
267	@echo "*********************************************************" \
268          | tee -a $(REGRESS_LOG)
269	@echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
270	@echo "*********************************************************" \
271          | tee -a $(REGRESS_LOG)
272
273regressonly0:
274	$(MAKE) regressonly REGRESS_LEVEL=0
275regressonly1:
276	$(MAKE) regressonly REGRESS_LEVEL=1 REGRESS_TESTS="$(REGRESS_TESTS1)"
277regressonly2:
278	$(MAKE) regressonly REGRESS_LEVEL=2 REGRESS_TESTS="$(REGRESS_TESTS2)"
279regressonly3:
280	$(MAKE) regressonly REGRESS_LEVEL=3 REGRESS_TESTS="$(REGRESS_TESTS3)" TIME_LIMIT=1500
281regressonly4:
282	$(MAKE) regressonly REGRESS_LEVEL=4 REGRESS_TESTS="$(REGRESS_TESTS4)" TIME_LIMIT=0
283