#**************************************************************
#* ********************************************************** *
#* *                                                        * *
#* *                Makefile                                * *
#* *                                                        * *
#* *                                                        * *
#* *                                                        * *
#* *  Copyright (C) 2020                                    * *
#* *  MPI fuer Informatik                                   * *
#* *                                                        * *
#* *  This program is protected software; any modification, * *
#* *  redistributtion etc. without approval is forbidden    * *
#* *                                                        * *
#* *  This program is distributed in the hope that it will  * *
#* *  be useful, but WITHOUT ANY WARRANTY; without even     * *
#* *  the implied warranty of MERCHANTABILITY or FITNESS    * *
#* *  FOR A PARTICULAR PURPOSE.  See the LICENCE file       * *
#* *  for more details.                                     * *
#* *                                                        * *
#* *                                                        * *
#* *                                                        * *
#* *             Contact:                                   * *
#* *             Christoph Weidenbach                       * *
#* *             Saarland Informatics Campus E1 4           * *
#* *             66123 Saarbruecken                         * *
#* *             Email: weidenbach@mpi-inf.mpg.de           * *
#* *             Germany                                    * *
#* *                                                        * *
#* ********************************************************** *
#**************************************************************

SHELL = /bin/bash

# Set the Compiler version flags. This allows including the git commit hash in --version output
VERSION_FLAGS := -DGIT_HASH=\"$(shell git rev-parse --short HEAD)\"

# FLINT Flags: compile link -lflint -lmpfr -lpthread code: -DSPASS_FLINT=1

STATIC     := # -static

ifdef SPASSDEBUG
    CFLAGS := -Wextra -Wimplicit-fallthrough=3 -Wall -g -fno-inline -Wno-unused # -DHM_DEBUGPRINT=1 #(to activate gcov) -fprofile-arcs -ftest-coverage
else
   ifdef SPASSANALYZE
      CFLAGS := -O2 -pg -no-pie -Wno-unused
   else
      CFLAGS := -O2 -Winline  #-fprofile-use # -fprofile-generate # # 
   endif
endif

ifdef SPASSSANITIZE
    CFLAGS += -fsanitize=undefined -fsanitize=address -fno-sanitize-recover=undefined
    NO_MEMORY_MANAGEMENT := 1
    STATIC := 
endif

ifdef SPASSCHECK
    CFLAGS += -DSPASS_CHECK=$(SPASSCHECK)
endif

ifdef WIN
    CFLAGS += -DSPASS_WIN=1
endif

ifdef NO_MEMORY_MANAGEMENT    
    CFLAGS += -DSPASS_NO_MEMORY_MANAGEMENT=1
endif

ifdef SPASSDRAT
    CFLAGS    += -DSPASS_DRAT=1
endif

# Enables catching of some common signals (segmentation fault ...)


WARNINGS = -pedantic -Wall -Wshadow -Wpointer-arith -Wwrite-strings -std=c99 #-Wconversion  
# Turn off some warnings for scanner files
SCANNERFLAGS=-Wno-implicit -Wno-uninitialized

CC		:= gcc
CFLAGS		:= -I ../../Source  -I ../../CNF/Source/ -I ../../SAT/Source/ $(WARNINGS) $(CFLAGS) $(VERSION_FLAGS)
VPATH		:= ../../Source/
VPATHCNF 	:= ../../CNF/Source/
VPATHSAT 	:= ../../SAT/Source/
RM		:= /bin/rm -f

PROGRAM		:= SPASS-SCL-FOL

BASE	    	:= fredund state trail inst twfo instset prlits abstract order distrn csolver congrbs groundgen fcnf lmodel condense subsume meta hlmodgrow hlcl ntwfo
SHARED		:= tptp tptp_parser misc memory array folsubst list strings term symbol fol clause ohash sorting ohash_functions pathidx kbo sharing upqueue bqueue flags clock
SHAREDCNF	:= cnf sharedterm
SHAREDSAT       := psolver pclause pindex preduce pstate mark var wlist
SHARED		:= $(addprefix $(VPATH), $(SHARED))
SHAREDCNF	:= $(addprefix $(VPATHCNF), $(SHAREDCNF))
SHAREDSAT	:= $(addprefix $(VPATHSAT), $(SHAREDSAT))

PROGRAMMAIN     := top.o

$(PROGRAM)	: $(addsuffix .o, $(SHARED)) $(addsuffix .o, $(SHAREDCNF)) $(addsuffix .o, $(SHAREDSAT)) $(addsuffix .o, $(BASE)) $(PROGRAMMAIN)
	$(CC) $(CFLAGS) $(addsuffix .o, $(SHARED)) $(addsuffix .o, $(SHAREDCNF)) $(addsuffix .o, $(SHAREDSAT))  $(addsuffix .o, $(BASE)) $(PROGRAMMAIN) $(STATIC)  -lm -o $(PROGRAM)

.PHONY		: all depend clean archive starexec-archive scripts tags


depend		: 
	$(RM)  .depend
	$(CC) $(CFLAGS) -MM *.c $(addsuffix .c, $(SHARED))  $(addsuffix .c, $(SHAREDCNF)) $(addsuffix .c, $(SHAREDSAT)) > .depend 

tags		:
	etags *.[ch] $(VPATH)/*.[ch]  $(VPATHCNF)/*.[ch] $(VPATHSAT)/*.[ch]
	cd $(VPATH); etags *.[ch];
	cd $(VPATHLA); etags *.[ch];
	cd $(VPATHCNF); etags *.[ch];
	cd $(VPATHSAT); etags *.[ch];	

clean		:
	$(RM) $(addsuffix .o, $(SHARED)) $(addsuffix .o, $(SHAREDCNF)) $(addsuffix .o, $(BASE)) $(addsuffix .o, $(SHAREDSAT)) $(PROGRAMBASE) $(PROGRAMMAIN) $(PROGRAM) *~ $(VPATH)*~ 

upd		:
	$(RM) $(addsuffix .o, $(SHARED)) $(addsuffix .o, $(SHAREDCNF)) $(addsuffix .o, $(BASE)) $(addsuffix .o, $(SHAREDSAT)) $(PROGRAMBASE) $(PROGRAMMAIN) $(PROGRAM) *~ $(VPATH)*~  TAGS .depend
	$(CC) $(CFLAGS) -MM *.c $(addsuffix .c, $(SHARED))  $(addsuffix .c, $(SHAREDCNF)) $(addsuffix .c, $(SHAREDSAT)) > .depend
	etags *.[ch] $(VPATH)/*.[ch]  $(VPATHCNF)/*.[ch] $(VPATHCNF)/*.[ch] $(VPATHSAT)/*.[ch]
	cd $(VPATH); etags *.[ch];
	cd $(VPATHLA); etags *.[ch];
	cd $(VPATHCNF); etags *.[ch];
	cd $(VPATHSAT); etags *.[ch];

opt   :  
	$(CC) $(CFLAGS) -O3 -fwhole-program -flto $(addsuffix .c, $(SHARED)) $(addsuffix .c, $(SHAREDCNF)) $(addsuffix .c, $(SHAREDSAT)) $(addsuffix .c, $(BASE)) top.c -lm -o $(PROGRAM)

sdis   :  $(PROGRAM)
	tar -zcf superlog.tgz  $(PROGRAM) README grammar.txt unittest.ftcnf isola.ftcnf

all       :
	make opt

archive:
	@tmp=$$(mktemp -d); out=$$(pwd)/$(PROGRAM)-src.tgz; \
	trap 'rm -rf "$$tmp"' EXIT; \
	mkdir -p "$$tmp/Trunk/FOL/Source" "$$tmp/Trunk/Source"; \
	cp Makefile "$$tmp/Trunk/FOL/Source/Makefile"; \
	for f in $$($(CC) $(CFLAGS) -MM $(addsuffix .c,$(BASE)) top.c \
		$(addsuffix .c,$(SHARED)) | sed 's/^[^:]*://;s/\\$$//' | \
		tr ' \\\n\t' '\n' | sort -u); do \
		case "$$f" in \
			../../Source/*.[ch]) dst="$$tmp/Trunk/Source/$${f##*/}" ;; \
			*/*) continue ;; \
			*.[ch]) dst="$$tmp/Trunk/FOL/Source/$${f##*/}" ;; \
			*) continue ;; \
		esac; \
		$(CC) -fpreprocessed -dD -E -P "$$f" -o "$$dst"; \
	done; \
	tar -C "$$tmp" -czf "$$out" Trunk; \
	echo "Created $$out"

starexec-archive:
	$(MAKE) clean
	$(MAKE) CC="zig cc -target x86_64-linux-gnu.2.17" opt
	mkdir -p bin
	$(RM) bin/$(PROGRAM)
	cp $(PROGRAM) bin/
	$(RM) SPASS-SCL.tgz
	tar -czf SPASS-SCL.tgz bin/

# Below this line the dependencies are included.
-include .depend
