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