diff options
| author | Hoang M. Le <hle@informatik.uni-bremen.de> | 2016-05-26 14:04:55 +0200 |
|---|---|---|
| committer | Hoang M. Le <hle@informatik.uni-bremen.de> | 2016-06-10 10:24:00 +0200 |
| commit | b30c06f9115bfcfea7a5d4d7609a25778adc573e (patch) | |
| tree | 10d65c6f2642ce25687b106e471956361a3366ee | |
| parent | 8a43b34c48d5d0507be51e3a7a1eac87fb60e0dc (diff) | |
| download | klee-b30c06f9115bfcfea7a5d4d7609a25778adc573e.tar.gz | |
update Makefile for metaSMT
| -rw-r--r-- | Makefile.common | 8 | ||||
| -rw-r--r-- | MetaSMT.mk | 16 | ||||
| -rwxr-xr-x | lib/Solver/Makefile | 10 |
3 files changed, 8 insertions, 26 deletions
diff --git a/Makefile.common b/Makefile.common index 9bc850ba..cf7bdcf7 100644 --- a/Makefile.common +++ b/Makefile.common @@ -78,11 +78,5 @@ ifeq ($(ENABLE_UCLIBC),1) endif # For metaSMT -ifeq ($(ENABLE_METASMT),1) - include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile - LD.Flags += -L$(METASMT_ROOT)/lib - CXX.Flags += -DBOOST_HAS_GCC_TR1 -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS - CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) - CXX.Flags += $(metaSMT_INCLUDES) -endif +include $(PROJ_SRC_ROOT)/MetaSMT.mk diff --git a/MetaSMT.mk b/MetaSMT.mk index 94dd398a..80f28a9b 100644 --- a/MetaSMT.mk +++ b/MetaSMT.mk @@ -1,17 +1,11 @@ # 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. +# Consume flags generated by metaSMT 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 + LD.Flags += $(metaSMT_LDFLAGS) + CXX.Flags += $(metaSMT_CXXFLAGS) + CXX.Flags += $(metaSMT_INCLUDES) CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) - LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lstp -lrt -lboolector -lminisat_core + LIBS += $(metaSMT_LDLIBS) endif diff --git a/lib/Solver/Makefile b/lib/Solver/Makefile index a44b4f6e..715f4b2d 100755 --- a/lib/Solver/Makefile +++ b/lib/Solver/Makefile @@ -16,11 +16,5 @@ NO_INSTALL=1 include $(LEVEL)/Makefile.common -ifeq ($(ENABLE_METASMT),1) - include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile - CXX.Flags += -DBOOST_HAS_GCC_TR1 - CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) - CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags)) - CXX.Flags += $(metaSMT_CXXFLAGS) - CXX.Flags += $(metaSMT_INCLUDES) -endif +include $(PROJ_SRC_ROOT)/MetaSMT.mk + |