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