include Makefile.config

INSTALL = install

# cf. trick from GNU make manual sec 8.1 2006/04
empty  :=

# substitute space characters in path name to build CPATH
PWD     = $(shell pwd)
OSNAME  = $(shell uname)
BASEDIR = $(subst $(empty) $(empty),*,${PWD})
LINKER  = ${CC}

LIBDIR  += ${BASEDIR}/extern/libreduce
LIB     += reduce
MODULES += nla
CFLAGS  += -DNLA

EXTERN += gmp
LIBDIR += ${BASEDIR}/extern/gmp/lib
LIBDIR += ${BASEDIR}/extern/gmp/include
LIB    += gmp

ifneq "$(wildcard ${BASEDIR}/extern/permlib)" ""
  EXTERN  += permlib
  LIBDIR  += ${BASEDIR}/extern/permlib/lib
  LIB     += permlib
  CFLAGS  += -DSYMSIMP
  LINKER   = g++
endif

ifeq ($(PROOF_PRODUCTION),YES)
  CFLAGS += -DPROOF
endif

#parsers/smtlib2 parsers/dimacs ATP congruence symbolic utils SAT
MODULES    += arith bool congruence number symbolic symmetry parsers/smtlib2 parsers/dimacs pre proof utils SAT .
LIBDIRFLAGS = $(subst *,\$(empty) $(empty),$(foreach DIR,${LIBDIR},-L${DIR}))
LIBFLAGS    = $(foreach LIB,${LIB},-l${LIB})
LDFLAGS     = ${LIBDIRFLAGS} ${LIBFLAGS}

SUBDIRS     = $(foreach EXT,${EXTERN},extern/${EXT}) \
	      $(foreach MOD,${MODULES},src/${MOD})

CPATH = $(subst *,$(empty) $(empty),.:$(subst $(empty) $(empty),:,$(foreach MOD, ${MODULES},${BASEDIR}/src/${MOD}))):$(subst *,$(empty) $(empty),.:$(subst $(empty) $(empty),:,${LIBDIR}))

#parsers
LEX         = flex
LFLAGS      = -P yy2
YACC        = bison
YFLAGS      = -d -p yy2

export CFLAGS
export CPATH
export YFLAGS
export LFLAGS

.DEFAULT_GOAL := all

#coverage variant of all
coverage: CFLAGS += -fprofile-arcs -ftest-coverage
coverage: all

#debug mem variant of debug
debug_mem : CFLAGS += -DMEM
debug_mem : debug

#source code inclusion
debug : CFLAGS += -g -g3 -gdwarf-2 # -Wshorten-64-to-32
prof : CFLAGS += -g -g3 -gdwarf-2

#debugging code inclusion
all prof: CFLAGS += -DNDEBUG
debug pedantic: CFLAGS += -DDEBUG

#optimization level
all: CFLAGS += -O3
debug pedantic prof: CFLAGS += -O0

#inlining
all: CFLAGS += -finline-limit=1000000 -fomit-frame-pointer
debug pedantic prof: CFLAGS += -Dinline=""

#specifics
debug : CFLAGS += -ftrapv
prof : CFLAGS += -pg

#compiler verbosity
all: CFLAGS +=
debug prof: CFLAGS += -std=c99 -Wall
pedantic: CFLAGS += -std=c99 -Wall -Wextra -pedantic -DPEDANTIC -Wconversion \
	-Wdeclaration-after-statement -Wmissing-prototypes

#parsing
debug: YFLAGS +=--debug -v
#debug: CFLAGS += -DDEBUG_PARSER
debug: LFLAGS +=#-d

all debug pedantic prof: ${SUBDIRS} ${PROGRAM}

src/SAT: CFLAGS += -DINSIDE_VERIT

.PHONY: ${SUBDIRS}
${SUBDIRS}:
	${MAKE} -C $@ all

.PHONY: libreduce
libreduce: extern/reduce
	sh install-reduce.sh

extern/reduce:
	svn export svn://svn.code.sf.net/p/reduce-algebra/code/trunk extern/reduce

.PHONY: ${PROGRAM}
${PROGRAM}: libreduce
${PROGRAM}: OBJMODULES = $(foreach MOD,${MODULES},$(wildcard src/${MOD}/*.o))

${PROGRAM}:
	${LINKER} ${CFLAGS} ${OBJMODULES} ${LDFLAGS} -o ${PROGRAM}

install: all
	${INSTALL} $(PROGRAM) ${PREFIX_BIN}

clean veryclean:
	for I in ${SUBDIRS}; do ${MAKE} -C $$I $@ || exit 1; done
	rm -fr extern/reduce
	rm -f *~ $(PROGRAM)

doc-user:
	mkdir -p doc/user
	doxygen doc/Doxyfile.libveriT.user
	doxygen doc/Doxyfile.veriT.user

doc-dev:
	mkdir -p doc/dev
	doxygen doc/Doxyfile.dev

doc: doc-dev doc-user

tags:
	for F in `find src -name "*.[ch]" -print`; do etags -a $$F; done

.PHONY: doc tags
