From cece05cadf6a624afd188e81720ae7701736a703 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 14 Jan 2016 12:21:48 +0000
Subject: Refactor the MetaSMT makefile commands into its own file which can be
 included by tools that needs to link against MetaSMT. Apart from making the
 Makefile code cleaner this allowed the Solver unit test linking to succeed
 when not building with STP support.

Unfortunately when using MetaSMT as the core solver the Solver unit
tests do not pass. Clearly no one tried this before... :(
---
 MetaSMT.mk                | 17 +++++++++++++++++
 tools/kleaver/Makefile    | 12 +-----------
 tools/klee/Makefile       | 12 +-----------
 unittests/Solver/Makefile |  2 ++
 4 files changed, 21 insertions(+), 22 deletions(-)
 create mode 100644 MetaSMT.mk

diff --git a/MetaSMT.mk b/MetaSMT.mk
new file mode 100644
index 00000000..94dd398a
--- /dev/null
+++ b/MetaSMT.mk
@@ -0,0 +1,17 @@
+# This file contains common code for linking against MetaSMT
+#
+# FIXME: This is a horribly fragile hack.
+# Instead the detection of what solvers the build of MetaSMT supports should be
+# done by the configure script and then the appropriate compiler flags should
+# be emitted to Makefile.config for consumption here.
+ifeq ($(ENABLE_METASMT),1)
+  include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
+  LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \
+              -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \
+              -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \
+              -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib \
+              -L$(METASMT_ROOT)/../../deps/stp-svn/lib
+  CXX.Flags += -DBOOST_HAS_GCC_TR1
+  CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
+  LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lstp -lrt -lboolector -lminisat_core
+endif
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index 287aeb38..ece2b799 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -23,14 +23,4 @@ ifneq ($(ENABLE_STP),0)
   LIBS += $(STP_LDFLAGS)
 endif
 
-ifeq ($(ENABLE_METASMT),1)
-  include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
-  LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \
-              -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \
-              -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \
-              -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib \
-              -L$(METASMT_ROOT)/../../deps/stp-svn/lib
-  CXX.Flags += -DBOOST_HAS_GCC_TR1
-  CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
-  LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lstp -lrt -lboolector -lminisat_core
-endif
+include $(PROJ_SRC_ROOT)/MetaSMT.mk
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index f8824fe7..d807350d 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -24,14 +24,4 @@ ifneq ($(ENABLE_STP),0)
   LIBS += $(STP_LDFLAGS)
 endif
 
-ifeq ($(ENABLE_METASMT),1)
-  include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
-  LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \
-              -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \
-              -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \
-              -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib \
-              -L$(METASMT_ROOT)/../../deps/stp-svn/lib
-  CXX.Flags += -DBOOST_HAS_GCC_TR1
-  CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
-  LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lstp -lrt -lboolector -lminisat_core
-endif
+include $(PROJ_SRC_ROOT)/MetaSMT.mk
diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile
index 65edbe7a..1d3d609e 100644
--- a/unittests/Solver/Makefile
+++ b/unittests/Solver/Makefile
@@ -12,3 +12,5 @@ include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 ifneq ($(ENABLE_STP),0)
   LIBS += $(STP_LDFLAGS)
 endif
+
+include $(PROJ_SRC_ROOT)/MetaSMT.mk
-- 
cgit 1.4.1