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
|
include Makefile.local
# The list of Makefiles and other important script sources which must
# be included in any distribution.
DISTFILES = \
Makefile \
Makefile.std \
Makefile.local.in \
configure.ac \
configure \
config.guess \
config.sub \
install-sh \
INSTALL \
LICENSE.in \
PEOPLE \
README \
VERSION \
bin/unpack.in \
bin/run_tests.in \
bin/cvc2smt.in \
doc/Doxyfile.in \
doc/Makefile.in \
doc/devel.dox \
doc/mainpage.dox \
doc/userdoc.dox \
doc/theory_api.dox \
doc/theory_api_flow.fig \
src/Makefile \
src/cvc3.pc.in \
test/Makefile \
test/george.h \
test/george.cpp \
test/main.cpp \
testc/Makefile \
testc/main.c \
emacs/cvc-mode.el
all: build
.PHONY: build
build:
cd $(TOP)/src; $(MAKE) $(TARGET) VERSION=$(VERSION)
ifeq ($(BUILD_JAVA),1)
cd $(TOP)/java; $(MAKE) $(TARGET) VERSION=$(VERSION)
endif
ifeq ($(CYGWIN),)
ifndef TARGET
find $(TOP)/src '(' -name "*.h" -o -name "*.cpp" -o \
-name "*.y" ')' \
! -name "lexPL.cpp" ! -name "parsePL.cpp" \
-print > FILES
ifdef ETAGS
sed -e s/^/\'/ -e s/$$/\'/ FILES | xargs etags
endif
ifdef EBROWSE
ebrowse --files=FILES
endif
endif
endif
#Standard make targets
.PHONY: depend spotty install
depend:
$(MAKE) TARGET=depend
spotty:
$(MAKE) TARGET=spotty
install:
$(MAKE) TARGET=install
# Special make targets for top Makefile
.PHONY: update-web update-web-doc doc dist dist_src dist_bin ld_sh ld_csh
update-web:
cp $(TOP)/webpage/*.html $(WEBDIR)
cp $(TOP)/webpage/*.jpg $(WEBDIR)
cp $(TOP)/webpage/*.css $(WEBDIR)
update-web-doc: doc
cd $(TOP)/doc/html/; tar cvBf - . | (cd $(WEBDIR)/doc/; tar xvpBf -)
doc:
cd $(TOP)/doc; $(MAKE)
dist: dist_src
# dist: dist_src dist_bin
TMPFILE=$(TOP)/filelist.tmp
TARDIR=cvc3-$(VERSION)
TARFILE=$(TARDIR).tar.gz
DISTTMPDIR=$(TOP)/dist-bak
dist_src:
@mkdir -p $(DISTTMPDIR)
ifndef DPLL_BASIC
@mv configure.ac configure $(DISTTMPDIR)
@cat $(DISTTMPDIR)/configure.ac | sed '/#BEGIN/,/#END/ d' > $(TOP)/configure.ac
@autoconf
endif
@rm -rf $(TMPFILE); touch $(TMPFILE)
echo "Collecting top-level script files"
@echo $(DISTFILES) >> $(TMPFILE)
cd $(TOP)/src; $(MAKE) print_src FILELIST=$(TMPFILE)
cd $(TOP)/java; $(MAKE) print_src FILELIST=$(TMPFILE)
echo "Building " $(TARFILE)
@mkdir -p $(TARDIR)
@tar cf - `cat $(TMPFILE)` | (cd $(TARDIR); tar xf -)
@echo "$(VERSION)" > $(TARDIR)/VERSION
@tar zcfv $(TARFILE) $(TARDIR)
ifndef DPLL_BASIC
@rm -f configure.ac configure
@mv $(DISTTMPDIR)/configure* $(TOP)
endif
rm -rf $(TMPFILE) $(TARDIR) $(DISTTMPDIR)
dist_bin:
echo "Sorry, binary distribution is not implemented yet"
exit 1
# Generate LD_LIBRARY_PATH assignments for various shells.
# When CVC is compiled with dynamic libraries, run
# `make ld_sh` or `make ld_tcsh`
# before running cvc executable.
ld_sh:
@echo "export LD_LIBRARY_PATH=$(TOP)/lib"
ld_csh:
@echo "setenv LD_LIBRARY_PATH $(TOP)/lib"
.PHONY: clean clean_gcov superclean_gcov clean_gprof distclean
# Clean up all the files generated by gcov (including *.cpp.gcov)
clean_gcov:
find src -name "*.da" -exec rm -f {} \;
superclean_gcov: clean_gcov
find src -name "*.gcov" -exec rm -f {} \;
find src -name "*.bb" -exec rm -f {} \;
find src -name "*.bbg" -exec rm -f {} \;
clean_gprof:
rm -f gmon.out
clean: superclean_gcov clean_gprof
$(MAKE) TARGET=clean
@rm -f $(REGRESS_LOG)
@rm -f $(TOP)/.test*
distclean:
cd $(TOP)/src; $(MAKE) distclean
cd $(TOP)/doc; $(MAKE) distclean
cd $(TOP)/test; $(MAKE) distclean
cd $(TOP)/java; $(MAKE) distclean
rm -rf $(TOP)/test/bin $(TOP)/test/obj
cd $(TOP)/testc; $(MAKE) distclean
rm -rf $(TOP)/testc/bin $(TOP)/testc/obj
@rm -rf $(DISTTMPDIR)
@mkdir -p $(DISTTMPDIR)
@mv $(TOP)/bin/*.in $(DISTTMPDIR)
@-mv $(TOP)/bin/CVS $(DISTTMPDIR)
@-mv $(TOP)/bin/.cvsignore $(DISTTMPDIR)
rm -rf $(TOP)/bin
@mv $(DISTTMPDIR) $(TOP)/bin
@rm -rf $(DISTTMPDIR)
rm -f TAGS BROWSE FILES LICENSE Makefile.local
rm -rf $(TOP)/autom4te.cache
rm -f config.log config.status $(LICENSE_INFO_FILE)
rm -f $(REGRESS_LOG)
@rm -f $(TOP)/.test*
rm -rf $(TOP)/lib $(TOP)/obj
# Regression tests: both for internal and presentation languages.
.PHONY: regress regress0 regress1 regress2 regress3 regress4
.PHONY: regressonly regressonly0 regressonly1 regressonly2 regressonly3 regressonly4
REGRESS_LOG=regressions.log
# The higher the level, the more tests are run (4 = all)
REGRESS_TESTS0 = benchmarks
REGRESS_TESTS1 = $(REGRESS_TESTS0)
REGRESS_TESTS2 = $(REGRESS_TESTS1)
REGRESS_TESTS3 = $(REGRESS_TESTS2)
REGRESS_TESTS4 = $(REGRESS_TESTS3)
REGRESS_TESTS = $(REGRESS_TESTS0)
REGRESS_LEVEL=0
# Program name
PROGNAME=$(TOP)/bin/cvc3
# Addiional options for run_tests script
ifndef RUN_TESTS_OPTIONS
ifeq ($(OPTIMIZED),1)
RUN_TESTS_OPTIONS=+rt
endif
endif
# Define to max. number of seconds to run each executable.
# 0 = no limit
TIME_LIMIT=1200
# Additional options
CVC_OPTIONS=+stats
ALL_OPTIONS= -l $(REGRESS_LEVEL) -vc $(PROGNAME) $(RUN_TESTS_OPTIONS) \
-t $(TIME_LIMIT) $(REGRESS_TESTS) -- $(CVC_OPTIONS)
regress: build
cd $(TOP)/test; $(MAKE)
cd $(TOP)/testc; $(MAKE)
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
@echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
@echo "C++ API test" | tee -a $(REGRESS_LOG)
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
$(TOP)/test/bin/test $(REGRESS_LEVEL) 2>&1 \
| tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
@echo "C API test" | tee -a $(REGRESS_LOG)
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
$(TOP)/testc/bin/testc $(REGRESS_LEVEL) 2>&1 \
| tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
@rm -f $(TOP)/.test*
ifeq ($(BUILD_JAVA),1)
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
@echo "Java API test" | tee -a $(REGRESS_LOG)
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
$(MAKE) -C java test 2>&1 \
| tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
endif
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
@echo "Regression tests" | tee -a $(REGRESS_LOG)
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
$(TOP)/bin/run_tests $(ALL_OPTIONS) 2>&1 \
| tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
@echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
regress0:
$(MAKE) regress REGRESS_LEVEL=0
regress1:
$(MAKE) regress REGRESS_LEVEL=1 REGRESS_TESTS="$(REGRESS_TESTS1)"
regress2:
$(MAKE) regress REGRESS_LEVEL=2 REGRESS_TESTS="$(REGRESS_TESTS2)"
regress3:
$(MAKE) regress REGRESS_LEVEL=3 REGRESS_TESTS="$(REGRESS_TESTS3)" TIME_LIMIT=1500
regress4:
$(MAKE) regress REGRESS_LEVEL=4 REGRESS_TESTS="$(REGRESS_TESTS4)" TIME_LIMIT=0
regressonly: build
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
@echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
@echo "Regression tests" | tee -a $(REGRESS_LOG)
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
$(TOP)/bin/run_tests $(ALL_OPTIONS) 2>&1 \
| tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
@echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
@echo "*********************************************************" \
| tee -a $(REGRESS_LOG)
regressonly0:
$(MAKE) regressonly REGRESS_LEVEL=0
regressonly1:
$(MAKE) regressonly REGRESS_LEVEL=1 REGRESS_TESTS="$(REGRESS_TESTS1)"
regressonly2:
$(MAKE) regressonly REGRESS_LEVEL=2 REGRESS_TESTS="$(REGRESS_TESTS2)"
regressonly3:
$(MAKE) regressonly REGRESS_LEVEL=3 REGRESS_TESTS="$(REGRESS_TESTS3)" TIME_LIMIT=1500
regressonly4:
$(MAKE) regressonly REGRESS_LEVEL=4 REGRESS_TESTS="$(REGRESS_TESTS4)" TIME_LIMIT=0
|
