#!/usr/bin/make -f

# Uncomment this to turn on verbose mode.
# export DH_VERBOSE=1

export DEB_BUILD_MAINT_OPTIONS = hardening=+all

DEB_HOST_MULTIARCH ?= $(shell dpkg-architecture -qDEB_HOST_MULTIARCH)

ifneq (,$(shell dh_listpackages -a | grep libz3-cil))
    WITH_MONO ?= yes
else
    WITH_MONO ?= no
endif

ifneq (,$(shell dh_listpackages -a | grep libz3-jni))
    WITH_JAVA ?= yes
else
    WITH_JAVA ?= no
endif

%:
	if [ $(WITH_JAVA) = yes ]; then \
		if [ $(WITH_MONO) = yes ]; then \
			dh $@ --parallel --with python2,javahelper,ocaml,cli; \
		else \
			dh $@ --parallel --with python2,javahelper,ocaml; \
		fi; \
	else \
		dh $@ --parallel --with python2,ocaml; \
	fi

override_dh_auto_configure:
	if [ $(WITH_MONO) = yes ]; then \
		sed -i 's/^DOTNET_ENABLED=.*/DOTNET_ENABLED=True/' scripts/mk_util.py; \
	else \
		sed -i 's/^DOTNET_ENABLED=.*/DOTNET_ENABLED=False/' scripts/mk_util.py; \
	fi
	if [ $(WITH_JAVA) = yes ]; then \
		python scripts/mk_make.py --java --ml --prefix=$(CURDIR)/debian/tmp/usr; \
	else \
		python scripts/mk_make.py --ml --prefix=$(CURDIR)/debian/tmp/usr; \
	fi
	sed -i 's/^SLINK_FLAGS=/SLINK_FLAGS=$$(LDFLAGS) -fPIC /' build/config.mk
	echo 'libz3$$(SO_EXT): SLINK_FLAGS += -Wl,-soname,libz3.so.4' >> build/Makefile
	printf '%%:\n\t$$(MAKE) -C build $$@\n' > Makefile
	printf '\nall:\n\t$$(MAKE) -C build $$@\n' >> Makefile
	ln -s libz3.so build/libz3.dll
	# from T2 README, with fixes
	printf '<configuration>\n <dllmap dll="libz3.dll" target="/usr/lib/$(DEB_HOST_MULTIARCH)/libz3.so" os="linux"/>\n</configuration>\n' > build/Microsoft.Z3.dll.config

override_dh_clean:
	dh_clean
	sed -i 's/^DOTNET_ENABLED=.*/DOTNET_ENABLED=False/' scripts/mk_util.py
	$(RM) Makefile scripts/*.pyc
	$(RM) -r build
	$(RM) src/api/python/*.pyc
	$(RM) \
    src/api/api_commands.cpp \
    src/api/api_log_macros.cpp \
    src/api/api_log_macros.h \
    src/api/dll/gparams_register_modules.cpp \
    src/api/dll/install_tactic.cpp \
    src/api/dll/mem_initializer.cpp \
    src/api/dotnet/Enumerations.cs \
    src/api/dotnet/Native.cs \
    src/api/dotnet/Properties/AssemblyInfo.cs \
    src/api/python/z3consts.py \
    src/api/python/z3core.py \
    src/api/java/Native.cpp \
    src/api/java/Native.java \
    src/api/java/enumerations/Z3_ast_kind.java \
    src/api/java/enumerations/Z3_ast_print_mode.java \
    src/api/java/enumerations/Z3_decl_kind.java \
    src/api/java/enumerations/Z3_error_code.java \
    src/api/java/enumerations/Z3_goal_prec.java \
    src/api/java/enumerations/Z3_lbool.java \
    src/api/java/enumerations/Z3_param_kind.java \
    src/api/java/enumerations/Z3_parameter_kind.java \
    src/api/java/enumerations/Z3_sort_kind.java \
    src/api/java/enumerations/Z3_symbol_kind.java \
    src/api/ml/z3native.ml \
    src/api/ml/z3native.mli \
    src/api/ml/z3native_stubs.c \
    src/api/ml/z3enums.ml \
    src/api/ml/z3enums.mli \
    src/ast/fpa/fpa2bv_rewriter_params.hpp \
    src/ast/normal_forms/nnf_params.hpp \
    src/ast/pattern/database.h \
    src/ast/pattern/pattern_inference_params_helper.hpp \
    src/ast/pp_params.hpp \
    src/ast/rewriter/arith_rewriter_params.hpp \
    src/ast/rewriter/array_rewriter_params.hpp \
    src/ast/rewriter/bool_rewriter_params.hpp \
    src/ast/rewriter/bv_rewriter_params.hpp \
    src/ast/rewriter/fpa_rewriter_params.hpp \
    src/ast/rewriter/poly_rewriter_params.hpp \
    src/ast/rewriter/rewriter_params.hpp \
    src/ast/simplifier/arith_simplifier_params_helper.hpp \
    src/ast/simplifier/array_simplifier_params_helper.hpp \
    src/ast/simplifier/bv_simplifier_params_helper.hpp \
    src/interp/interp_params.hpp \
    src/math/polynomial/algebraic_params.hpp \
    src/math/realclosure/rcf_params.hpp \
    src/model/model_evaluator_params.hpp \
    src/model/model_params.hpp \
    src/muz/base/fixedpoint_params.hpp \
    src/nlsat/nlsat_params.hpp \
    src/parsers/util/parser_params.hpp \
    src/sat/sat_asymm_branch_params.hpp \
    src/sat/sat_params.hpp \
    src/sat/sat_scc_params.hpp \
    src/sat/sat_simplifier_params.hpp \
    src/shell/gparams_register_modules.cpp \
    src/shell/install_tactic.cpp \
    src/shell/mem_initializer.cpp \
    src/smt/params/smt_params_helper.hpp \
    src/solver/combined_solver_params.hpp \
    src/tactic/sls/sls_params.hpp \
    src/test/gparams_register_modules.cpp \
    src/test/install_tactic.cpp \
    src/test/mem_initializer.cpp \
    src/util/version.h \
    src/opt/opt_params.hpp


override_dh_auto_test:
	$(MAKE) test-z3
	build/test-z3 -a
	$(RM) interval_lemma_* trigo-lemmas.math

override_dh_auto_install:
	mkdir -p debian/tmp/usr/lib/python2.7/dist-packages/
	dh_auto_install
	$(RM) debian/tmp/usr/lib/python2.7/dist-packages/libz3.so
	ln -s ../../$(DEB_HOST_MULTIARCH)/libz3.so \
		debian/tmp/usr/lib/python2.7/dist-packages/libz3.so
	mv debian/tmp/usr/lib/libz3.so debian/tmp/usr/lib/libz3.so.4
	ln -s libz3.so.4 debian/tmp/usr/lib/libz3.so
	mkdir -p debian/tmp/usr/lib/$(DEB_HOST_MULTIARCH)/jni
	-mv debian/tmp/usr/lib/libz3java.so* \
		debian/tmp/usr/lib/$(DEB_HOST_MULTIARCH)/jni/
	mv debian/tmp/usr/lib/libz3.so* \
		debian/tmp/usr/lib/$(DEB_HOST_MULTIARCH)/

override_dh_install:
	dh_install
	-cp build/api/ml/*.cmxa debian/libz3-ocaml-dev/usr/lib/ocaml/z3/
	-cp build/api/ml/*.cmx debian/libz3-ocaml-dev/usr/lib/ocaml/z3/

override_dh_installchangelogs:
	dh_installchangelogs RELEASE_NOTES
	for p in python-z3 libz3-ocaml-dev libz3-cil libz3-java libz3-jni ; do \
		$(RM) -rf debian/$$p/usr/share/doc/$$p/ ; \
		ln -s libz3-dev debian/$$p/usr/share/doc/$$p || true ; \
	done

override_dh_clideps:
	# dh_clideps fails to find libz3.so automatically
	# So we have to depend on libz3-dev manually in d/control
	dh_clideps --exclude-moduleref=libz3