Skip to content

Commit

Permalink
Use macro and directive to remove cvc4 dependency
Browse files Browse the repository at this point in the history
  • Loading branch information
Yue Zhao authored and yzhao30 committed Jun 8, 2017
1 parent bff9ed2 commit 4bf2d8a
Show file tree
Hide file tree
Showing 138 changed files with 50 additions and 29,212 deletions.
2 changes: 2 additions & 0 deletions .gitignore
Expand Up @@ -6,3 +6,5 @@ tags
.depend
.stoke_config
aliasing
.DS_Store

26 changes: 21 additions & 5 deletions Makefile
Expand Up @@ -74,6 +74,9 @@ ifndef EXT_TARGET
endif

#CXX_FLAGS are any extra flags the user might want to pass to the compiler
ifdef NOCVC4
CXX_FLAGS += -DNOCVC4=1
endif

WARNING_FLAGS=-Wall -Werror -Wextra -Wfatal-errors -Wno-deprecated -Wno-unused-parameter -Wno-unused-variable -Wno-vla -fdiagnostics-color=always
STOKE_CXX=ccache $(CXX) $(CXX_FLAGS) -std=c++14 $(WARNING_FLAGS)
Expand All @@ -83,8 +86,10 @@ INC_FOLDERS=\
src/ext/cpputil/ \
src/ext/x64asm \
src/ext/gtest-1.7.0/include \
src/ext/z3/src/api \
src/ext/cvc4-1.4-build/include
src/ext/z3/src/api
ifndef NOCVC4
INC_FOLDERS += src/ext/cvc4-1.4-build/include
endif

INC=$(addprefix -I./, $(INC_FOLDERS))

Expand All @@ -97,10 +102,17 @@ LIB=\
-lboost_filesystem -lboost_system -lboost_regex -lboost_thread \
-lcln \
-liml -lgmp \
-L src/ext/cvc4-1.4-build/lib -lcvc4 \
-lcblas -latlas \
-L src/ext/z3/build -lz3
ifndef NOCVC4
LIB += -L src/ext/cvc4-1.4-build/lib -lcvc4
endif

ifndef NOCVC4
LDFLAGS=-Wl,-rpath=\$$ORIGIN/../src/ext/z3/build:\$$ORIGIN/../src/ext/cvc4-1.4-build/lib,--enable-new-dtags
else
LDFLAGS=-Wl,-rpath=\$$ORIGIN/../src/ext/z3/build,--enable-new-dtags
endif

SRC_OBJ=\
src/cfg/cfg.o \
Expand All @@ -123,7 +135,6 @@ SRC_OBJ=\
src/search/search_state.o \
\
src/solver/z3solver.o \
src/solver/cvc4solver.o \
\
src/state/cpu_state.o \
src/state/cpu_states.o \
Expand Down Expand Up @@ -186,7 +197,12 @@ SRC_OBJ=\
\
src/verifier/hold_out.o


ifndef NOCVC4
SRC_OBJ += src/solver/cvc4solver.o
endif
#ifdef NOCVC4
#$(error NOCVC4 define)
#endif
TOOL_ARGS_OBJ=\
tools/args/benchmark.o \
tools/args/cost.o \
Expand Down
11 changes: 3 additions & 8 deletions configure.sh
Expand Up @@ -30,13 +30,12 @@ elif [ $AVX -eq 0 ]; then
PLATFORM="sandybridge"
else
echo "ERROR: STOKE is currently only supported on sandybridge or haswell machines. You appear to have an older CPU."
exit 1
exit 1
fi

## Now do some parsing, look for options

BUILD_TYPE="release"
NOCVC4=""

while :; do
case $1 in
Expand Down Expand Up @@ -81,12 +80,8 @@ echo "STOKE_PLATFORM=\"$PLATFORM\"" >> .stoke_config
echo "BUILD_TYPE=$BUILD_TYPE" >> .stoke_config
echo "MISC_OPTIONS=$MISC_OPTIONS" >> .stoke_config

if [ -z $NOCVC4 ]; then
cp -r scripts/tocopy/nocvc4/ .
echo ""
echo "Build without CVC4 solver"
else
cp -r scripts/tocopy/origin/ .
if [ ! -z $NOCVC4 ]; then
echo "NOCVC4=$NOCVC4" >> .stoke_config
fi


Expand Down

0 comments on commit 4bf2d8a

Please sign in to comment.