import configure script

The default solver is Boolector.  Switch to Z3 via --enable-z3.

.gitignore

@@ -0,0 +1,19 @@
+*~
+.DS_Store
+Makefile.in
+/aclocal.m4
+/autom4te.cache
+/build*
+/config.h.in
+/config.h
+/config.log
+/config.status
+/configure
+/m4
+/Makefile
+/tools/Makefile
+/lib/Makefile
+/src/Makefile
+/tests/Makefile
+/libtool
+/stamp-h1

Makefile.am

@@ -0,0 +1 @@
+SUBDIRS = lib src

configure.ac

@@ -0,0 +1,74 @@
+#                                               -*- Autoconf -*-
+# Process this file with autoconf to produce a configure script.
+
+AC_INIT([ksat],[0.1],[[email protected]])
+AC_CONFIG_AUX_DIR([build-aux])
+AC_CONFIG_TESTDIR([tests])
+AC_CONFIG_HEADERS([config.h])
+
+AM_INIT_AUTOMAKE([foreign -Wall -Werror])
+m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])])
+
+# Checks for programs.
+AM_PROG_CC_C_O
+AC_PROG_CXX
+AC_PROG_LN_S
+AC_PROG_MKDIR_P
+AC_PROG_SED
+AC_CHECK_PROG([CURL],[wget],[wget -O -],[curl])
+
+LT_INIT([disable-static pic-only])
+AC_PROG_LIBTOOL
+
+# Checks for OS.
+AM_CONDITIONAL(LINUX,false)
+AM_CONDITIONAL(DARWIN,false)
+case $build_os in
+  darwin*)
+	AM_CONDITIONAL(DARWIN,true)
+	;;
+  linux*)
+	AM_CONDITIONAL(LINUX,true)
+	;;
+  *)
+	AC_MSG_ERROR([platform not supported])
+	;;
+esac
+
+# Checks for SMT.
+AC_MSG_CHECKING([for SMT solver])
+AC_ARG_ENABLE([z3],
+	AS_HELP_STRING([--enable-z3],[Use Z3 as SMT solver]))
+if test "x$enable_z3" = "xyes"; then
+	SMT_LIB=libz3.a
+	SMT_LIBADD="-lz3 -lgomp -lgmp"
+	AC_DEFINE([HAVE_Z3],[1],[Use Z3 as SMT solver])
+	AC_MSG_RESULT([Z3])
+else
+	SMT_LIB=libboolector.a
+	SMT_LIBADD=-lboolector
+	AC_DEFINE([HAVE_BOOLECTOR],[1],[Use Boolector as SMT solver])
+	AC_MSG_RESULT([Boolector])
+	AC_SEARCH_LIBS([zlibVersion],[z],,[AC_MSG_FAILURE([zlib not found])])
+fi
+AC_SUBST([SMT_LIB])
+AC_SUBST([SMT_LIBADD])
+
+# Checks for libraries.
+if test "$SMT_LIB" = "libz3.a"; then
+	AC_CHECK_LIB([gmp],[__gmpz_init],,
+		[AC_MSG_ERROR([libgmp not found, required by Z3])])
+fi
+
+# Checks for header files.
+
+# Checks for typedefs, structures, and compiler characteristics.
+
+# Checks for library functions.
+
+AC_CONFIG_FILES([
+	Makefile
+	lib/Makefile
+	src/Makefile
+])
+AC_OUTPUT

lib/Makefile.am

@@ -0,0 +1,39 @@
+if LINUX
+Z3        = z3-x64-3.2
+endif
+if DARWIN
+Z3        = z3-osx-3.2.1
+endif
+BOOLECTOR = boolector-1.4.1-376e6b0-110304
+PICOSAT   = picosat-936
+PRECOSAT  = precosat-570-239dbbe-100801
+
+all-local: $(SMT_LIB)
+
+libz3.a:
+	$(CURL) 'http://research.microsoft.com/projects/z3/$(Z3).tar.gz' | tar xz
+	cp -f z3/include/*.h z3/lib/$@ .
+
+libboolector.a:
+	$(CURL) 'http://fmv.jku.at/picosat/$(PICOSAT).tar.gz' | tar xz
+	ln -f -s $(PICOSAT) picosat
+	sed -i -e "s/CFLAGS=/CFLAGS=-fPIC /" picosat/makefile.in
+	cd picosat && ./configure -O && make
+	$(CURL) 'http://fmv.jku.at/precosat/$(PRECOSAT).tar.gz' | tar xz
+	ln -f -s $(PRECOSAT) precosat
+	sed -i -e "s/;m32=yes//g" precosat/configure
+	sed -i -e "s/malloc.h/stdlib.h/g" precosat/precosat.cc
+	echo "#include <stddef.h>" > precosat/precosat.hh~
+	cat precosat/precosat.hh >> precosat/precosat.hh~
+	mv -f precosat/precosat.hh~ precosat/precosat.hh
+	sed -i -e "s/CXXFLAGS=/CXXFLAGS=-fPIC /" precosat/makefile.in
+	cd precosat && ./configure -O && make precosat.o precobnr.o
+	$(CURL) 'http://fmv.jku.at/boolector/$(BOOLECTOR).tar.gz' | tar xz
+	ln -f -s $(BOOLECTOR) boolector
+	sed -i -e "s/CFLAGS=/CFLAGS=-fPIC /" boolector/makefile.in
+	cd boolector && ./configure -precosat && make
+	ln -f -s boolector/libboolector.a
+
+libz3.so:
+	$(CURL) 'http://research.microsoft.com/projects/z3/$(Z3).tar.gz' | tar xz
+	cp -f z3/include/*.h z3/lib/$@ .