From fac9c3be139b3bb8895f78d5815684487fb007de Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Sun, 25 Aug 2024 20:20:53 +0000 Subject: [PATCH] Fix compiling multiple backend --- src/Makefile | 11 +++-------- src/makefile.include | 5 +++++ src/reach/Makefile | 40 +++++++++++++++++++++++----------------- 3 files changed, 31 insertions(+), 25 deletions(-) diff --git a/src/Makefile b/src/Makefile index 0d9a905..c6847e3 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,8 +1,3 @@ -#ENABLE_Y2 := 0 -#ENABLE_M5 := 0 -#ENABLE_BT := 0 -#ENABLE_Z3 := 0 - REA_LOC = reach DPA_LOC = dpa VWN_LOC = vwn @@ -10,9 +5,9 @@ VWN_LOC = vwn all: $(MAKE) vw $(MAKE) da - ENABLE_Y2=1 $(MAKE) re - ENABLE_BT=1 $(MAKE) re -# ENABLE_M5=1 $(MAKE) re + CONFIG_Y2=1 $(MAKE) re + CONFIG_BT=1 $(MAKE) re + CONFIG_M5=1 $(MAKE) re clean: $(MAKE) vwc diff --git a/src/makefile.include b/src/makefile.include index 912c2d6..edd40be 100644 --- a/src/makefile.include +++ b/src/makefile.include @@ -3,6 +3,11 @@ STATIC_MODE := 0 ENABLE_VMT := 1 ENABLE_BTOR2 := 1 +ENABLE_Y2 := 1 +ENABLE_BT := 1 +ENABLE_M5 := 1 +ENABLE_Z3 := 0 + CURR_DIR = $(shell pwd) BIN_DIR = $(CURR_DIR)/../../build/bin DEPS = $(CURR_DIR)/../../deps diff --git a/src/reach/Makefile b/src/reach/Makefile index 0433c90..b3dcca2 100644 --- a/src/reach/Makefile +++ b/src/reach/Makefile @@ -10,34 +10,40 @@ else LINK_FLAGS += -pthread -lgmpxx -lgmp -lrt -ldl endif -Y2_DIR = $(DEPS)/yices2 -Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a -INCLUDE += -I$(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/include -LINKLIBS += $(Y2_LIB) -CFLAGS += -D_Y2 ifeq ($(ENABLE_Y2), 1) + Y2_DIR = $(DEPS)/yices2 + Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a + INCLUDE += -I$(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/include + LINKLIBS += $(Y2_LIB) + CFLAGS += -D_Y2 +endif +ifeq ($(CONFIG_Y2), 1) CFLAGS += -DBACKEND_Y2 REACH_SUFFIX = y2 endif ifeq ($(ENABLE_BT), 1) - BT_DIR = $(DEPS)/boolector - BT_LIB = $(BT_DIR)/build/lib/libboolector.a - BT_LIB += $(BT_DIR)/deps/btor2tools/build/lib/libbtor2parser.a - BT_LIB += $(BT_DIR)/deps/cadical/build/libcadical.a - INCLUDE += -I$(BT_DIR)/src - LINKLIBS += $(BT_LIB) - CFLAGS += -D_BT + BT_DIR = $(DEPS)/boolector + BT_LIB = $(BT_DIR)/build/lib/libboolector.a + BT_LIB += $(BT_DIR)/deps/btor2tools/build/lib/libbtor2parser.a + BT_LIB += $(BT_DIR)/deps/cadical/build/libcadical.a + INCLUDE += -I$(BT_DIR)/src + LINKLIBS += $(BT_LIB) + CFLAGS += -D_BT +endif +ifeq ($(CONFIG_BT), 1) CFLAGS += -DBACKEND_BT REACH_SUFFIX = bt endif ifeq ($(ENABLE_M5), 1) - MSAT_DIR = $(DEPS)/mathsat - MSAT_LIB = $(MSAT_DIR)/lib/libmathsat.a $(STATIC_GMPXX) $(STATIC_GMP) - INCLUDE += -I$(MSAT_DIR)/include - LINKLIBS += $(MSAT_LIB) - CFLAGS += -D_M5 + MSAT_DIR = $(DEPS)/mathsat + MSAT_LIB = $(MSAT_DIR)/lib/libmathsat.a # $(STATIC_GMPXX) $(STATIC_GMP) + INCLUDE += -I$(MSAT_DIR)/include + LINKLIBS += $(MSAT_LIB) + CFLAGS += -D_M5 +endif +ifeq ($(CONFIG_M5), 1) CFLAGS += -DBACKEND_M5 REACH_SUFFIX = m5 endif