# Environnment variables.
CC = g++
INCLUDES=
LIBS = -L/opt/local/lib/

# This part is for supporting MacOS.
# Currently this is not very felxible since paths
# follows the standard macport installation.
# One should note that
UNAME_S := $(shell uname -s)
ifeq ($(UNAME_S),Darwin)
	CC = xcrun g++-mp-10
	INCLUDES = -I/opt/local/include/
	LIBS = -L/opt/local/lib/
endif

SRCS := $(shell find ./src -name "*.cc")

OBJS := $(addsuffix .o, $(basename $(SRCS)))

EXEC = bmctool

CXXFLAGS = -Wall -Wextra  -ansi -std=c++17 -O3

LDFLAGS = -L./painless/lib -llgl \
          -L./painless/lib -l_standard \
          -L./painless/lib -lpainless \
          -L./NuSMV-2.6.0/NuSMV/lib -lnusmv \
          -L./painless/lib -lperiplolibrary  \
          -L./painless/lib -lperiplo  \
          -L./painless/lib -lapi  \
          -L./painless/lib -lsatsolvers  \
          -L./painless/lib -ldesat  \
          -lxml2 -lpthread -lz -lreadline \
          -lm -lgmpxx -lgmp -fopenmp $(LIBS)

CXXFLAGS += -I./painless/lingeling \
            -I./painless/mapleCOMSPS \
	    -I./painless/desat/Desat -I./painless/desat/Desat/libExpression \
            -I./painless/periplo \
            -I./painless \
            -I./src \
            -I./NuSMV-2.6.0/NuSMV/code \
            -I./NuSMV-2.6.0/NuSMV/build/build-cudd/include \
            -I./NuSMV-2.6.0/NuSMV/build \
            -I./painless/periplo/src/  \
            -I./painless/periplo/src/api/ \
            -I./painless/periplo/src/cnfizers/ \
            -I./painless/periplo/src/common/ \
            -I./painless/periplo/src/egraph/ \
            -I./painless/periplo/src/minisat/ \
            -I./painless/periplo/src/proof/ \
            -I./painless/periplo/src/satsolvers/ \
            -I./painless/periplo/src/simplifiers/ \
            -I./painless/periplo/src/sorts/ \
             -DPRODUCE_PROOF $(INCLUDES)
            #  #-DFULL_LABELING

all: build-nusmv build-painless build
	echo Compilation done.

build: $(EXEC)

check:
	./tests/test.sh

$(EXEC): bmctool.o $(OBJS)
	$(CC) -o $@ $^ $(CXXFLAGS) $(LDFLAGS)

%.o: %.cc
	$(CC) -o $@ -c $< $(CXXFLAGS) $(LDFLAGS)

build-nusmv:
	cd NuSMV-2.6.0/NuSMV && mkdir -p build    		 	&& \
	cd build                                                 	&& \
	cmake .. -DPYTHON_EXECUTABLE:FILEPATH=/usr/bin/python2.7 	&& \
	make                                                     	&& \
	cd .. 							 	&& \
	mkdir -p lib						 	&& \
	$(CC) -shared -o lib/libnusmv.so -lxml2 -lpthread    	           \
	-lz -lreadline  -lm -lgmpxx $(LIBS) -lgmp               	   \
	`find ./build/code/nusmv/shell/cmd/ ./build/code/nusmv/addons_core -type f -wholename "*.o"`   `find ./build/code/nusmv/core   -type f -wholename "*.o"` ./build/build-cudd/lib/*.a `find ./build/build-MiniSat/ -type f -wholename "*.a"`


build-painless:
	cd painless                                               && \
	make                                                      && \
	sh libpainless.sh


build-docker:
	docker build --no-cache -t gitlab-registry.lrde.epita.fr/akheireddine/bmctool .

run-docker:
	docker run --rm -it gitlab-registry.lrde.epita.fr/akheireddine/bmctool

push-docker:
	docker push gitlab-registry.lrde.epita.fr/akheireddine/bmctool

pull-docker:
	docker pull gitlab-registry.lrde.epita.fr/akheireddine/bmctool

clean:
	rm -f $(OBJS) bmctool.o $(EXEC)

cleanall: clean
	cd  NuSMV-2.6.0/NuSMV/build && make clean && cd .. && rm -Rf lib

mrproper: clean
	rm -rf $(EXEC) bmctool.o

.PHONY: clean mrproper