Skip to content

Commit

Permalink
Use same cadical library for cvc5 and boolector
Browse files Browse the repository at this point in the history
  • Loading branch information
CyanoKobalamyne committed Jul 3, 2024
1 parent 341f51c commit 2390b00
Show file tree
Hide file tree
Showing 5 changed files with 11 additions and 9 deletions.
2 changes: 1 addition & 1 deletion CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ set(INCLUDE_DIRS
"${PROJECT_SOURCE_DIR}/include")

# add to search path for find_package
list(APPEND CMAKE_PREFIX_PATH "${PROJECT_SOURCE_DIR}/deps")
list(APPEND CMAKE_PREFIX_PATH "${PROJECT_SOURCE_DIR}/deps/install")

if (NOT SMT_SWITCH_LIB_TYPE)
set(SMT_SWITCH_LIB_TYPE SHARED)
Expand Down
4 changes: 2 additions & 2 deletions btor/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ target_include_directories (smt-switch-btor PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/
target_include_directories (smt-switch-btor PUBLIC "${BTOR_HOME}/src")

target_link_libraries(smt-switch-btor "${BTOR_HOME}/build/lib/libboolector.a")
target_link_libraries(smt-switch-btor "${BTOR_HOME}/deps/cadical/build/libcadical.a")
target_link_libraries(smt-switch-btor "${PROJECT_SOURCE_DIR}/deps/install/lib/libcadical.a")
target_link_libraries(smt-switch-btor "${BTOR_HOME}/deps/btor2tools/build/lib/libbtor2parser.a")
target_link_libraries(smt-switch-btor smt-switch)
target_link_libraries(smt-switch-btor pthread)
Expand All @@ -29,7 +29,7 @@ if (SMT_SWITCH_LIB_TYPE STREQUAL STATIC)
COMMAND
mkdir smt-switch-btor && cd smt-switch-btor && ar -x "../$<TARGET_FILE_NAME:smt-switch-btor>" && cd ../ &&
mkdir boolector && cd boolector && ar -x "${BTOR_HOME}/build/lib/libboolector.a" &&
ar -x "${BTOR_HOME}/deps/cadical/build/libcadical.a" &&
ar -x "${PROJECT_SOURCE_DIR}/deps/install/lib/libcadical.a" &&
ar -x "${BTOR_HOME}/deps/btor2tools/build/lib/libbtor2parser.a" && cd ../ &&
ar -qc "$<TARGET_FILE_NAME:smt-switch-btor>" ./boolector/*.o ./smt-switch-btor/*.o &&
# now clean up
Expand Down
6 changes: 3 additions & 3 deletions contrib/setup-btor.sh
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ else
NUM_CORES=1
fi

$DIR/setup-cadical.sh

if [ ! -d "$DEPS/boolector" ]; then
cd $DEPS
Expand All @@ -23,16 +24,15 @@ if [ ! -d "$DEPS/boolector" ]; then
cd boolector
git checkout -f $BTOR_VERSION
CFLAGS="" ./contrib/setup-btor2tools.sh
./contrib/setup-cadical.sh
./configure.sh --only-cadical -fPIC
./configure.sh --only-cadical -fPIC --path "$DEPS/install"
cd build
make -j$NUM_CORES
cd $DIR
else
echo "$DEPS/boolector already exists. If you want to rebuild, please remove it manually."
fi

if [ -f $DEPS/boolector/build/lib/libboolector.a ] && [ -f $DEPS/boolector/deps/cadical/build/libcadical.a ] && [ -f $DEPS/boolector/deps/btor2tools/build/lib/libbtor2parser.a ] ; then \
if [ -f $DEPS/boolector/build/lib/libboolector.a ] && [ -f $DEPS/install/lib/libcadical.a ] && [ -f $DEPS/boolector/deps/btor2tools/build/lib/libbtor2parser.a ] ; then \
echo "It appears boolector was setup successfully into $DEPS/boolector."
echo "You may now install it with make ./configure.sh --btor && cd build && make"
else
Expand Down
6 changes: 4 additions & 2 deletions contrib/setup-cvc5.sh
Original file line number Diff line number Diff line change
Expand Up @@ -16,21 +16,23 @@ else
NUM_CORES=1
fi

$DIR/setup-cadical.sh

if [ ! -d "$DEPS/cvc5" ]; then
cd $DEPS
git clone https://github.com/cvc5/cvc5.git
chmod -R 777 cvc5
cd cvc5
git checkout -f ${CVC5_VERSION}
CXXFLAGS=-fPIC CFLAGS=-fPIC ./configure.sh --static --auto-download
CXXFLAGS=-fPIC CFLAGS=-fPIC ./configure.sh --static --auto-download --dep-path="$DEPS/install"
cd build
make -j$NUM_CORES
cd $DIR
else
echo "$DEPS/cvc5 already exists. If you want to rebuild, please remove it manually."
fi

if [ -f $DEPS/cvc5/build/src/libcvc5.a ] && [ -f $DEPS/cvc5/build/src/parser/libcvc5parser.a ]; then
if [ -f $DEPS/cvc5/build/src/libcvc5.a ] && [ -f $DEPS/cvc5/build/src/parser/libcvc5parser.a ] && [ -f $DEPS/install/lib/libcadical.a ]; then
echo "It appears cvc5 was setup successfully into $DEPS/cvc5."
echo "You may now install it with make ./configure.sh --cvc5 && cd build && make"
else
Expand Down
2 changes: 1 addition & 1 deletion cvc5/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ find_library(POLYLIBXX REQUIRED

find_library(CADICAL REQUIRED
NAMES libcadical.a libcadical.so libcadical.dylib
PATHS "${CVC5_HOME}/build/deps/lib")
)

target_link_libraries(smt-switch-cvc5 "${CVC5_HOME}/build/src/libcvc5.a")
target_link_libraries(smt-switch-cvc5 "${CVC5_HOME}/build/src/parser/libcvc5parser.a")
Expand Down

0 comments on commit 2390b00

Please sign in to comment.