# Configuration

BINARIES=latin greek twl naive jr_test pp_sudoku sudoku jr twosat arrays

OCAMLC=ocamlc
OCAMLFLAGS=-I src

all: $(BINARIES) doc

%: src/dimacs.cmo src/kosaraju.cmo src/%.cmo
	$(OCAMLC) $(OCAMLFLAGS) $+ -o $@

%.cmo: %.ml
	$(OCAMLC) $(OCAMLFLAGS) -c $<

%.cmi: %.mli
	$(OCAMLC) $(OCAMLFLAGS) -c $<


# Exercises

N=10

test_latin: latin
	mkdir -p inputs outputs
	./latin p $(N) > inputs/latin-$(N).cnf
	minisat inputs/latin-$(N).cnf outputs/latin-$(N).model ; \
	  ./latin s $(N) < outputs/latin-$(N).model


test_greek: greek
	mkdir -p inputs outputs
	./greek p $(N) > inputs/greek-$(N).cnf
	minisat inputs/greek-$(N).cnf outputs/greek-$(N).model ; \
	  ./greek s $(N) < outputs/greek-$(N).model

GRID=530070000600195000098000060800060003400803001700020006060000280000419005000080079

test_sudoku: sudoku pp_sudoku
	mkdir -p inputs outputs
	./sudoku p $(GRID) > inputs/sudoku-$(GRID).cnf
	minisat inputs/sudoku-$(GRID).cnf outputs/sudoku-$(GRID).model ; \
	  ./sudoku s $(GRID) < outputs/sudoku-$(GRID).model | ./pp_sudoku

test_sudoku_plain: sudoku
	mkdir -p inputs outputs
	./sudoku p $(GRID) > inputs/sudoku-$(GRID).cnf
	minisat inputs/sudoku-$(GRID).cnf outputs/sudoku-$(GRID).model ; \
	  ./sudoku s $(GRID) < outputs/sudoku-$(GRID).model

CSV=problems/sudoku.csv

tests_sudoku: sudoku
	while read line ; do \
		pb=$$(echo $$line | head -c 81) ; \
		sol=$$(echo $$line | tail -c 82 | head -c 81) ; \
		echo "Testing grid $$pb $$sol" ; \
		(make GRID=$$pb test_sudoku_plain | grep $$sol | echo "Success") || \
			(echo "Failed"; exit 1) ; \
	done < $(CSV)

test_jr: jr jr_test
	mkdir -p inputs outputs
	./jr p $(N) > inputs/jr-$(N).cnf
	minisat inputs/jr-$(N).cnf outputs/jr-$(N).model ; \
	  ./jr s $(N) < outputs/jr-$(N).model | ./jr_test


2sat_test: all
	@for i in 2sat/SAT/* ; do \
	  echo -n "$$i... " ; \
	  ./twosat $$i outputs/output.sat ; \
	done
	@for i in 2sat/UNSAT/* ; do \
	  echo -n "$$i... " ; \
	  ./twosat $$i outputs/output.sat ; \
	done

# Project

PROVER=./arrays

in_test: all
	@for i in tests/SAT/* ; do \
	  echo -n "$$i... " ; \
	  $(PROVER) $$i outputs/output.sat ; \
	  grep -v UNSAT outputs/output.sat > /dev/null || exit 1 ; \
	done
	@for i in tests/UNSAT/* ; do \
	  echo -n "$$i... " ; \
	  $(PROVER) $$i outputs/output.sat ; \
	  grep UNSAT outputs/output.sat > /dev/null || exit 1 ; \
	done

test: all
	@echo Timing tests with minisat...
	@time --output=tests/minisat.time --format=%U \
	  make PROVER=minisat in_test > /dev/null
	@cat tests/minisat.time
	@echo Timing tests with $(PROVER)...
	@time --output=tests/prover.time --format=%U make in_test
	@cat tests/prover.time
	@m=`cat tests/minisat.time` ; p=`cat tests/prover.time` ; \
	  echo "Ratio: $$p / $$m" | bc

# clean and doc

clean:
	rm -f src/*.cmo src/*.cmi
	rm -f $(BINARIES)

doc:
	ocamldoc -d html/ -stars -html src/dimacs.mli src/kosaraju.mli


-include .depends
.depends: Makefile src/*.ml src/*.mli
	ocamldep -I src src/*.ml src/*.mli > .depends