CC=gcc -W -Wall -O3 -DNDEBUG
LD=gcc
AR=ar

VPATH=../src:../test

# Add vpath for all subdirectories
vpath %.c ../src/core/cdcl:../src/core/conflict:../src/core/propagate:../src/core/simplify:../src/core/data:../src/core/main:../src/core/misc
vpath %.c ../src/util/data-structures:../src/util/inline:../src/util/io:../src/util/runtime:../src/util/kitten:../src/util/build:../src/util/misc

# Find all source files recursively in subdirectories
LIBSRT=$(shell find ../src -name '*.c' -type f | sort)
# Extract just the filename (not the path) - object files are flat
LIBSRC=$(notdir $(LIBSRT))
LIBSRC:=$(filter-out main.c $(APPSRC),$(LIBSRC))

APPSRC=application.c handle.c parse.c witness.c

TSTSRT=$(sort $(wildcard ../test/*.c))
TSTSUB=$(subst ../test/,,$(TSTSRT))
TSTSRC=$(filter-out test.c,$(TSTSUB))

APPOBJ=$(APPSRC:.c=.o)
LIBOBJ=$(LIBSRC:.c=.o)
TSTOBJ=$(APPOBJ) $(TSTSRC:.c=.o)

INCLUDES=-I. -I../src -I../src/core/cdcl -I../src/core/conflict -I../src/core/propagate -I../src/core/simplify -I../src/core/data -I../src/core/main -I../src/core/misc -I../src/util/data-structures -I../src/util/inline -I../src/util/io -I../src/util/runtime -I../src/util/kitten -I../src/util/build -I../src/util/misc

LIBS=libkissat.a

all: build.h libkissat.a kissat

build.h:
	../scripts/generate-build-header.sh > $@

test: all tissat
	./tissat

REMOVE=*.gcda *.gcno *.gcov gmon.out *~ *.proof

clean:
	rm -f kissat tissat kitten
	rm -f makefile build.h *.o *.a *.so
	rm -f $(REMOVE)
	cd ../src; rm -f $(REMOVE)
	cd ../test; rm -f $(REMOVE)

coverage:
	@gcov -o . $(shell find ../src -name '*.c' -o -name '*.h') 2>&1 | \
	../scripts/filter-coverage-output.sh
format:
	clang-format -i $(shell find ../src -name '*.c' -o -name '*.h')

kissat: main.o $(APPOBJ) libkissat.a makefile
	$(LD) -o $@ main.o $(APPOBJ) $(LIBS) -lm

tissat: test.o $(TSTOBJ) libkissat.a makefile
	$(LD) -o $@ test.o $(TSTOBJ) $(LIBS) -lm

kitten: kitten.c random.h stack.h makefile
	$(CC) $(CFLAGS) $(INCLUDES) -DSTAND_ALONE_KITTEN -o $@ ../src/util/kitten/kitten.c

collect.o: sort.c
dense.o: sort.c
propdense.o: assign.c
prophyper.o: assign.c
proprobe.o: assign.c
propsearch.o: assign.c
watch.o: sort.c

build.o: build.c build.h makefile
	$(CC) $(INCLUDES) -c $<

testkitten.o: testkitten.c makefile
	$(CC) $(INCLUDES) -c $<

test.o: test.c build.h makefile
	$(CC) $(INCLUDES) -c $<

libkissat.a: $(LIBOBJ) build.h makefile
	$(AR) rc $@ $(LIBOBJ)

libkissat.so: $(LIBOBJ) makefile
	$(LD) -shared -o $@ $(LIBOBJ)

# Generic pattern rule for object files (after explicit rules)
%.o: %.c build.h makefile
	$(CC) $(INCLUDES) -c $<

.PHONY: all clean coverage indent test build.h
