SRC = \
	AssemblyInfo.n \
        Grinder.n \
        ArrayTheory.n \
        SmtDumper.n \
	Rational.n \
	ExternalCNF.n \
	InternalCNF.n \
	QuantDPLLSolver.n \
	DPLLSolver.n \
	PatriciaTree.n \
	QuantLoop.n \
	SatSolver.n \
	Core.n \
	QAtom.n \
	Atom.n \
	ToCNF.n \
	Parser.n \
	FatalError.n \
	Term.n \
	Command.n \
	Theory.n \
	FreeFunTheory.n \
	UtvpiTheory.n \
	LinearTheory.n \
	TcTheory.n \
	Literal.n \
	Proof.n \
	Driver.n \
	Term.SubstLite.n \
	Term.SubTrigger.n \
	Term.Matcher.n \
	Term.Pool.n \
	CSV.n \
	

MACROS_SRC = UtilMacros.n
CSC = gmcs

NFLAGS = -g

ifeq ($(WINDIR),)
MINISAT_SO = minisat.so
else
MINISAT_SO = minisat.dll
endif

all: $(MINISAT_SO) MiniSatCS.dll fx7.exe

fx7.exe: $(SRC) Fx7.Macros.dll Fx7.BigInteger.dll
	ncc -bar+ -i $(NFLAGS) -o $@ $(SRC) -r:Fx7.Macros.dll -r:MiniSatCS.dll -r:Fx7.BigInteger.dll

MiniSatCS.dll: $(wildcard minisatcs/*.cs)
	$(MAKE) -C minisatcs
	cp -f minisatcs/MiniSatCS.dll* .

Fx7.BigInteger.dll: BigInteger.cs
	$(CSC) /t:library /out:$@ $^

Fx7.Macros.dll: $(MACROS_SRC)
	ncc -bar+ -t:library -r:Nemerle.Compiler -i $(NFLAGS) -o $@ $(MACROS_SRC)

minisat.so: minisat/Solver.C minisat/DotNet.C
	g++ -shared -o $@ -fno-strict-aliasing -fPIC -O3 -W -Wall -Iminisat $^

minisat.dll: minisat/Solver.C minisat/DotNet.C
	g++ -DNO_CYGWIN -Iminisat -mno-cygwin -c -O3 -W -Wall $^
	dllwrap -mno-cygwin --target i386-mingw32 --export-all-symbols \
		--dllname=$@ --driver-name=g++ Solver.o DotNet.o

clean:
	rm -f $(MINISAT_SO) fx7.exe Fx7.Macros.dll *.mdb *.pdb Fx7.BigInteger.dll

.PHONY: tests

t0: all
	time $(MAKE) do-t0

do-t0:
	./run    -n                               tests/custom
	./run -s -n                      -valid   tests/OrdersTest.sx
	./run -s -n -ax:tests/escv1.ax   -invalid tests/Examples.esc.invalid
	./run -s -n                      -valid   tests/PredTest.esc.valid
	./run -s -n                      -invalid tests/PredTest.esc.invalid
	./run -s -n -ax:tests/escv3.ax   -valid   tests/Examples.esc3.valid
	./run -s -n -ax:tests/necula1.ax -valid   tests/necula1.sx
	./run -s -n -ax:tests/saxe1.ax   -invalid tests/saxe1.input
	./run -s -n -ax:tests/escv1.ax   -valid   tests/Examples.esc.valid
	./run -s -n -ax:tests/def.ax     -valid   tests/Examples.valid
	./run -s -n -ax:tests/escv2.ax   -invalid tests/Examples.esc2.invalid
	./run -s -n -ax:tests/def.ax     -invalid tests/Examples.invalid

t1: all
	./run benchmarks/01_*

t2: all
	./run benchmarks/0[12]_*

t3: all
	./run benchmarks/0[123]_*

t4: all
	./run benchmarks/0[1234]_*

t5: all
	./run benchmarks/0[12345]_*

t6: all
	./run -t:600 benchmarks/0[123456]_*

t7: all
	./run -t:2500 benchmarks/0[1234567]_*

t9: all
	./run -t:2500 benchmarks/09_*

toq1: all
	./runesc -t:60 esc/q1/*

toq3: all
	./runesc -t:60 esc/q{1,2,3}/*

tq1: all
	./runesc -t:60 esc/qf1/* esc/q1/*

tq2: all
	./runesc -t:60 esc/qf1/* esc/q{1,2}/*

tq3: all
	./runesc -t:60 esc/qf1/* esc/q{1,2,3}/*

tql1: all
	./runesc -t:60 esc/ql1/*

tql2: all
	./runesc -t:60 esc/ql[12]/*

tql3: all
	./runesc -t:60 esc/ql[123]/*


t: all t0 t1

.PHONY: tags

tags:
	ctags *.n minisat/*.C minisat/*.h
	cd minisat; ctags *.C *.h

tgz:
	rm -rf fx7-bin
	mkdir fx7-bin
	cp MiniSatCS.dll fx7.exe Fx7.Macros.dll Fx7.BigInteger.dll minisat.so run ra fx7-bin/ 
	(echo "all:"; echo "	:") > fx7-bin/Makefile
	mkdir fx7-bin/logs
	cp /usr/lib/mono/nemerle/Nemerle.dll fx7-bin/
	tar zcf fx7-bin.tgz fx7-bin

# TODO include Nemerle.dll
# TODO include system desc
smtcomp: all
	rm -rf fx7-smtcomp
	mkdir fx7-smtcomp
	cp MiniSatCS.dll fx7.exe Fx7.Macros.dll Fx7.BigInteger.dll minisat.so fx7-smtcomp/
	cp /usr/bin/mono /usr/lib/lib{gthread-2.0.so.0,gmodule-2.0.so.0,glib-2.0.so.0,stdc++.so.6} fx7-smtcomp/
	svn export . fx7-smtcomp/source
	cp tests/SelectStore.ax smtcomp/* fx7-smtcomp/
	tar jcf fx7-smtcomp.tar.bz2 fx7-smtcomp