# plugins.
set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
+#-----------------------------------------------------------------------------#
+# Policies
+
+# Required for FindGLPK since it sets CMAKE_REQUIRED_LIBRARIES
+if(POLICY CMP0075)
+ cmake_policy(SET CMP0075 NEW)
+endif()
+
+#-----------------------------------------------------------------------------#
+# Tell CMake where to find our dependencies
+
+if(ABC_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${ABC_DIR}")
+endif()
+if(ANTLR_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${ANTLR_DIR}")
+endif()
+if(CADICAL_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${CADICAL_DIR}")
+endif()
+if(CRYPTOMINISAT_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${CRYPTOMINISAT_DIR}")
+endif()
+if(CXXTEST_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${CXXTEST_DIR}")
+endif()
+if(DRAT2ER_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${DRAT2ER_DIR}")
+endif()
+if(GLPK_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${GLPK_DIR}")
+endif()
+if(GMP_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${GMP_DIR}")
+endif()
+if(LFSC_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${LFSC_DIR}")
+endif()
+if(SYMFPU_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${SYMFPU_DIR}")
+endif()
+
+# By default the contrib/get-* scripts install dependencies to deps/install.
+list(APPEND CMAKE_PREFIX_PATH "${PROJECT_SOURCE_DIR}/deps/install")
+
#-----------------------------------------------------------------------------#
set(INCLUDE_INSTALL_DIR include)
find_package(PythonInterp REQUIRED)
endif()
-set(GMP_HOME ${GMP_DIR})
find_package(GMP REQUIRED)
if(ENABLE_ASAN)
endif()
if(USE_ABC)
- set(ABC_HOME "${ABC_DIR}")
find_package(ABC REQUIRED)
add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
endif()
if(USE_CADICAL)
- set(CaDiCaL_HOME ${CADICAL_DIR})
find_package(CaDiCaL REQUIRED)
add_definitions(-DCVC4_USE_CADICAL)
endif()
if(THREADS_HAVE_PTHREAD_ARG)
add_c_cxx_flag(-pthread)
endif()
- set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR})
find_package(CryptoMiniSat REQUIRED)
add_definitions(-DCVC4_USE_CRYPTOMINISAT)
endif()
if(USE_DRAT2ER)
- set(Drat2Er_HOME ${DRAT2ER_DIR})
find_package(Drat2Er REQUIRED)
add_definitions(-DCVC4_USE_DRAT2ER)
endif()
if(USE_GLPK)
set(GPL_LIBS "${GPL_LIBS} glpk")
- set(GLPK_HOME ${GLPK_DIR})
find_package(GLPK REQUIRED)
add_definitions(-DCVC4_USE_GLPK)
endif()
if(USE_LFSC)
set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
- set(LFSC_HOME ${LFSC_DIR})
find_package(LFSC REQUIRED)
add_definitions(-DCVC4_USE_LFSC)
endif()
endif()
if(USE_SYMFPU)
- set(SymFPU_HOME ${SYMFPU_DIR})
find_package(SymFPU REQUIRED)
add_definitions(-DCVC4_USE_SYMFPU)
set(CVC4_USE_SYMFPU 1)
# ABC_LIBRARIES - Libraries needed to use ABC
# ABC_ARCH_FLAGS - Platform specific compile flags
-
-# Check default location of ABC built with contrib/get-abc.
-if(NOT ABC_HOME)
- set(ABC_HOME ${PROJECT_SOURCE_DIR}/abc/alanmi-abc-53f39c11b58d)
-endif()
-
-# Note: We don't check the system version since ABC does not provide a default
-# install rule.
-find_path(ABC_INCLUDE_DIR
- NAMES base/abc/abc.h
- PATHS ${ABC_HOME}/src
- NO_DEFAULT_PATH)
-find_library(ABC_LIBRARIES
- NAMES abc
- PATHS ${ABC_HOME}
- NO_DEFAULT_PATH)
-find_program(ABC_ARCH_FLAGS_PROG
- NAMES arch_flags
- PATHS ${ABC_HOME}
- NO_DEFAULT_PATH)
+# Note: contrib/get-abc copies header files to deps/install/include/abc.
+# However, includes in ABC headers are not prefixed with "abc/" and therefore
+# we have to look for headers in include/abc instead of include/.
+find_path(ABC_INCLUDE_DIR NAMES base/abc/abc.h PATH_SUFFIXES abc)
+find_library(ABC_LIBRARIES NAMES abc)
+find_program(ABC_ARCH_FLAGS_PROG NAMES arch_flags)
if(ABC_ARCH_FLAGS_PROG)
execute_process(COMMAND ${ABC_ARCH_FLAGS_PROG}
# ANTLR_INCLUDE_DIR - the ANTLR include directory
# ANTLR_LIBRARIES - Libraries needed to use ANTLR
-
-# Check default location of ANTLR built with contrib/get-antlr-3.4.
-# If the user provides a directory we will not search the default paths and
-# fail if ANTLR was not found in the specified directory.
-if(NOT ANTLR_HOME)
- set(ANTLR_HOME ${PROJECT_SOURCE_DIR}/antlr-3.4)
- set(CHECK_SYSTEM_VERSION TRUE)
-endif()
-
-find_program(ANTLR_BINARY
- NAMES antlr3
- PATHS ${ANTLR_HOME}/bin
- NO_DEFAULT_PATH)
-find_path(ANTLR_INCLUDE_DIR
- NAMES antlr3.h
- PATHS ${ANTLR_HOME}/include
- NO_DEFAULT_PATH)
-find_library(ANTLR_LIBRARIES
- NAMES antlr3c antlr3c-static
- PATHS ${ANTLR_HOME}/lib
- NO_DEFAULT_PATH)
-
-if(CHECK_SYSTEM_VERSION)
- find_program(ANTLR_BINARY NAMES antlr3)
- find_path(ANTLR_INCLUDE_DIR NAMES antlr3.h)
- find_library(ANTLR_LIBRARIES NAMES antlr3c)
-endif()
+find_program(ANTLR_BINARY NAMES antlr3)
+find_path(ANTLR_INCLUDE_DIR NAMES antlr3.h)
+find_library(ANTLR_LIBRARIES NAMES antlr3c antlr3c-static)
# Check if antlr3FileStreamNew is available. If not we have to
# define CVC4_ANTLR3_OLD_INPUT_STREAM (src/parser/CMakeLists.txt).
# CaDiCaL_INCLUDE_DIR - the CaDiCaL include directory
# CaDiCaL_LIBRARIES - Libraries needed to use CaDiCaL
-
-# Check default location of CaDiCaL built with contrib/get-cadical.
-# If the user provides a directory we will not search the default paths and
-# fail if CaDiCaL was not found in the specified directory.
-if(NOT CaDiCaL_HOME)
- set(CaDiCaL_HOME ${PROJECT_SOURCE_DIR}/cadical)
- set(CHECK_SYSTEM_VERSION TRUE)
-endif()
-
-find_path(CaDiCaL_INCLUDE_DIR
- NAMES cadical.hpp
- PATHS ${CaDiCaL_HOME}/src
- NO_DEFAULT_PATH)
-find_library(CaDiCaL_LIBRARIES
- NAMES cadical
- PATHS ${CaDiCaL_HOME}/build
- NO_DEFAULT_PATH)
-
-if(CHECK_SYSTEM_VERSION)
- find_path(CaDiCaL_INCLUDE_DIR NAMES cadical.hpp)
- find_library(CaDiCaL_LIBRARIES NAMES cadical)
-endif()
+find_path(CaDiCaL_INCLUDE_DIR NAMES cadical.hpp)
+find_library(CaDiCaL_LIBRARIES NAMES cadical)
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(CaDiCaL
# CryptoMiniSat_LIBRARIES - Libraries needed to use CryptoMiniSat
-# Check default location of CryptoMiniSat built with contrib/get-cryptominisat.
-# If the user provides a directory we will not search the default paths and
-# fail if CryptoMiniSat was not found in the specified directory.
-if(NOT CryptoMiniSat_HOME)
- set(CryptoMiniSat_HOME ${PROJECT_SOURCE_DIR}/cryptominisat5/build)
- set(CHECK_SYSTEM_VERSION TRUE)
-endif()
-
-find_path(CryptoMiniSat_INCLUDE_DIR
- NAMES cryptominisat5/cryptominisat.h
- PATHS ${CryptoMiniSat_HOME}/include ${CryptoMiniSat_HOME}/cmsat5-src
- NO_DEFAULT_PATH)
-find_library(CryptoMiniSat_LIBRARIES
- NAMES cryptominisat5
- PATHS ${CryptoMiniSat_HOME}/lib
- NO_DEFAULT_PATH)
-
-if(CHECK_SYSTEM_VERSION)
- find_path(CryptoMiniSat_INCLUDE_DIR NAMES cryptominisat5/cryptominisat.h)
- find_library(CryptoMiniSat_LIBRARIES NAMES cryptominisat5)
-endif()
+find_path(CryptoMiniSat_INCLUDE_DIR NAMES cryptominisat5/cryptominisat.h)
+find_library(CryptoMiniSat_LIBRARIES NAMES cryptominisat5)
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(CryptoMiniSat
# Drat2Er_INCLUDE_DIR - the Drat2Er include directory
# Drat2Er_LIBRARIES - Libraries needed to use Drat2Er
-
-# Check default location of Drat2Er built with contrib/get-drat2er.
-# If the user provides a directory we will not search the default paths and
-# fail if Drat2Er was not found in the specified directory.
-if(NOT Drat2Er_HOME)
- set(Drat2Er_HOME ${PROJECT_SOURCE_DIR}/drat2er/build/install)
-endif()
-
-find_path(Drat2Er_INCLUDE_DIR
- NAMES drat2er.h
- PATHS ${Drat2Er_HOME}/include
- NO_DEFAULT_PATH)
-find_library(Drat2Er_LIBRARIES
- NAMES libdrat2er.a
- PATHS ${Drat2Er_HOME}/lib
- NO_DEFAULT_PATH)
-find_library(DratTrim_LIBRARIES
- NAMES libdrat-trim.a
- PATHS ${Drat2Er_HOME}/lib
- NO_DEFAULT_PATH)
+find_path(Drat2Er_INCLUDE_DIR NAMES drat2er.h)
+find_library(Drat2Er_LIBRARIES NAMES libdrat2er.a)
+find_library(DratTrim_LIBRARIES NAMES libdrat-trim.a)
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(Drat2Er
# GLPK_LIBRARIES - Libraries needed to use GLPK
-# Check default location of GLPK built with contrib/get-glpk-cut-log.
-# If the user provides a directory we will not search the default paths and
-# fail if GLPK was not found in the specified directory.
-if(NOT GLPK_HOME)
- set(GLPK_HOME ${PROJECT_SOURCE_DIR}/glpk-cut-log)
- set(CHECK_SYSTEM_VERSION TRUE)
-endif()
-
-find_path(GLPK_INCLUDE_DIR
- NAMES glpk.h
- PATHS ${GLPK_HOME}/include
- NO_DEFAULT_PATH)
-find_library(GLPK_LIBRARIES
- NAMES glpk
- PATHS ${GLPK_HOME}/lib
- NO_DEFAULT_PATH)
-
-if(CHECK_SYSTEM_VERSION)
- find_path(GLPK_INCLUDE_DIR NAMES glpk.h)
- find_library(GLPK_LIBRARIES NAMES glpk)
-endif()
+find_path(GLPK_INCLUDE_DIR NAMES glpk.h)
+find_library(GLPK_LIBRARIES NAMES glpk)
# Check if we really have GLPK-cut-log.
if(GLPK_INCLUDE_DIR)
# GMP_INCLUDE_DIR - the GMP include directory
# GMP_LIBRARIES - Libraries needed to use GMP
-
-# Check default location of GMP built with contrib/get-gmp.
-# If the user provides a directory we will not search the default paths and
-# fail if GMP was not found in the specified directory.
-if(NOT GMP_HOME)
- set(GMP_HOME ${PROJECT_SOURCE_DIR}/gmp-6.1.2)
- set(CHECK_SYSTEM_VERSION TRUE)
-endif()
-
-find_path(GMP_INCLUDE_DIR
- NAMES gmp.h gmpxx.h
- PATHS ${GMP_HOME}/include
- NO_DEFAULT_PATH)
-find_library(GMP_LIBRARIES
- NAMES gmp
- PATHS ${GMP_HOME}/lib
- NO_DEFAULT_PATH)
-
-if(CHECK_SYSTEM_VERSION)
- find_path(GMP_INCLUDE_DIR NAMES gmp.h gmpxx.h)
- find_library(GMP_LIBRARIES NAMES gmp)
-endif()
+find_path(GMP_INCLUDE_DIR NAMES gmp.h gmpxx.h)
+find_library(GMP_LIBRARIES NAMES gmp)
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES)
# LFSC_INCLUDE_DIR - the LFSC include directory
# LFSC_LIBRARIES - Libraries needed to use LFSC
-
-# Check default location of LFSC built with contrib/get-lfsc.
-# If the user provides a directory we will not search the default paths and
-# fail if LFSC was not found in the specified directory.
-if(NOT LFSC_HOME)
- set(LFSC_HOME ${PROJECT_SOURCE_DIR}/lfsc-checker/install)
- set(CHECK_SYSTEM_VERSION TRUE)
-endif()
-
-find_path(LFSC_INCLUDE_DIR
- NAMES lfscc.h
- PATHS ${LFSC_HOME}/include
- NO_DEFAULT_PATH)
-find_library(LFSC_LIBRARIES
- NAMES lfscc
- PATHS ${LFSC_HOME}/lib
- NO_DEFAULT_PATH)
-
-if(CHECK_SYSTEM_VERSION)
- find_path(LFSC_INCLUDE_DIR NAMES lfscc.h)
- find_library(LFSC_LIBRARIES NAMES lfscc)
-endif()
+find_path(LFSC_INCLUDE_DIR NAMES lfscc.h)
+find_library(LFSC_LIBRARIES NAMES lfscc)
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(LFSC
# SymFPU_FOUND - system has SymFPU lib
# SymFPU_INCLUDE_DIR - the SymFPU include directory
-
-# Check default location of SymFPU built with contrib/get-symfpu.
-# If the user provides a directory we will not search the default paths and
-# fail if SymFPU was not found in the specified directory.
-if(NOT SymFPU_HOME)
- set(SymFPU_HOME ${PROJECT_SOURCE_DIR}/symfpu-CVC4)
- set(CHECK_SYSTEM_VERSION TRUE)
-endif()
-
-find_path(SymFPU_INCLUDE_DIR
- NAMES symfpu/core/unpackedFloat.h
- PATHS ${SymFPU_HOME}
- NO_DEFAULT_PATH)
-
-if(CHECK_SYSTEM_VERSION)
- find_path(SymFPU_INCLUDE_DIR NAMES symfpu/core/unpackedFloat.h)
-endif()
+find_path(SymFPU_INCLUDE_DIR NAMES symfpu/core/unpackedFloat.h)
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(SymFPU DEFAULT_MSG SymFPU_INCLUDE_DIR)
#
source "$(dirname "$0")/get-script-header.sh"
-if [ -e abc ]; then
- echo 'error: file or directory "abc" exists; please move it out of the way.' >&2
- exit 1
-fi
-
+ABC_DIR="$DEPS_DIR/abc"
commit=53f39c11b58d
-mkdir abc
-cd abc
-webget https://bitbucket.org/alanmi/abc/get/$commit.tar.gz abc-$commit.tar.gz
-gunzip -f abc-$commit.tar.gz
-tar xfv abc-$commit.tar
-cd alanmi-abc-$commit
+check_dep_dir "$ABC_DIR"
+setup_dep "https://bitbucket.org/alanmi/abc/get/$commit.tar.gz" "$ABC_DIR"
+cd "$ABC_DIR"
# Strip out libSupport.c, it is in charge of loading extensions and we
# don't want different behavior based on ABC_LIB_PATH, or based on what
# These aren't necessary for our usage and we don't want the dependencies.
make -j$(nproc) libabc.a OPTFLAGS=-O ABC_USE_NO_READLINE=1 ABC_USE_NO_PTHREADS=1
mv libabc.a libabc-static.a
+install_lib libabc-static.a
make clean
+
make -j$(nproc) libabc.a OPTFLAGS='-O -fPIC' ABC_USE_NO_READLINE=1 ABC_USE_NO_PTHREADS=1
+install_lib libabc.a
+install_bin arch_flags
+
+# Copy headers and preserve subdirectories
+cd src
+mkdir -p "$INSTALL_INCLUDE_DIR/abc"
+cp --parents $(find . -name '*.h') "$INSTALL_INCLUDE_DIR/abc"
echo
echo ===================== Now configure CVC4 with =====================
#!/usr/bin/env bash
#
source "$(dirname "$0")/get-script-header.sh"
-ANTLR_HOME_DIR=antlr-3.4
+ANTLR_HOME_DIR="$DEPS_DIR/antlr-3.4"
if [ -z "${BUILD_TYPE}" ]; then
BUILD_TYPE="--disable-shared --enable-static"
fi
if [ -z "${MACHINE_TYPE}" ]; then
- CONFIG_GUESS_SCRIPT=$ANTLR_HOME_DIR/config.guess
- if ! [ -e ${CONFIG_GUESS_SCRIPT} ]; then
- mkdir -p $ANTLR_HOME_DIR
+ CONFIG_GUESS_SCRIPT="$ANTLR_HOME_DIR/config.guess"
+ if ! [ -e "${CONFIG_GUESS_SCRIPT}" ]; then
+ mkdir -p "$ANTLR_HOME_DIR"
# Attempt to download once
webget 'http://git.savannah.gnu.org/gitweb/?p=config.git;a=blob_plain;f=config.guess;hb=HEAD' $CONFIG_GUESS_SCRIPT
- if [ -e $CONFIG_GUESS_SCRIPT ]; then
- chmod +x $CONFIG_GUESS_SCRIPT
+ if [ -e "$CONFIG_GUESS_SCRIPT" ]; then
+ chmod +x "$CONFIG_GUESS_SCRIPT"
else
echo "$(basename $0): I need the file config/config.guess to tell MACHINE_TYPE" >&2
echo "Try running ./autogen.sh, or set the MACHINE_TYPE environment variable" >&2
MACHINE_TYPE=$(${CONFIG_GUESS_SCRIPT} | sed 's,-.*,,')
fi
-set -x
-mkdir -p $ANTLR_HOME_DIR/share/java
-mkdir -p $ANTLR_HOME_DIR/bin
-mkdir -p $ANTLR_HOME_DIR/src
-cd $ANTLR_HOME_DIR || exit 1
-webget https://www.antlr3.org/download/antlr-3.4-complete.jar share/java/antlr-3.4-complete.jar
-webget https://www.antlr3.org/download/C/libantlr3c-3.4.tar.gz src/libantlr3c-3.4.tar.gz
-tee bin/antlr3 <<EOF
+mkdir -p "$ANTLR_HOME_DIR/share/java"
+webget \
+ "https://www.antlr3.org/download/antlr-3.4-complete.jar" \
+ "$ANTLR_HOME_DIR/share/java/antlr-3.4-complete.jar"
+
+mkdir -p "$ANTLR_HOME_DIR/bin"
+tee "$ANTLR_HOME_DIR/bin/antlr3" <<EOF
#!/usr/bin/env bash
-export CLASSPATH=`pwd`/share/java/antlr-3.4-complete.jar:\$CLASSPATH
+export CLASSPATH=$ANTLR_HOME_DIR/share/java/antlr-3.4-complete.jar:\$CLASSPATH
exec java org.antlr.Tool "\$@"
EOF
-chmod a+x bin/antlr3
-cd src
-gunzip -f libantlr3c-3.4.tar.gz
-tar xfv libantlr3c-3.4.tar
-cd libantlr3c-3.4
+chmod a+x "$ANTLR_HOME_DIR/bin/antlr3"
+install_bin "$ANTLR_HOME_DIR/bin/antlr3"
-# Use an absolute path for the installation directory to avoid spurious libtool
-# warnings about the ANTLR library having moved
-PREFIX=$($PYTHON -c "import os; print(os.path.realpath('$(pwd)/../..'))")
+setup_dep \
+ "https://www.antlr3.org/download/C/libantlr3c-3.4.tar.gz" \
+ "$ANTLR_HOME_DIR/libantlr3c-3.4"
+cd "$ANTLR_HOME_DIR/libantlr3c-3.4"
# Make antlr3debughandlers.c empty to avoid unreferenced symbols
rm -rf src/antlr3debughandlers.c && touch src/antlr3debughandlers.c
-if [ ${MACHINE_TYPE} == 'x86_64' ]; then
+if [ "${MACHINE_TYPE}" == 'x86_64' ]; then
# 64-bit stuff here
- ./configure --enable-64bit --disable-antlrdebug --prefix="${PREFIX}" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
+ ./configure --enable-64bit --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
else
# 32-bit stuff here
- ./configure --disable-antlrdebug --prefix="${PREFIX}" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
+ ./configure --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
fi
cp Makefile Makefile.orig
exit 0
fi
-cd ../..
-mv lib/libantlr3c.a lib/libantlr3c-static.a
-
-cd src/libantlr3c-3.4
+mv "$INSTALL_LIB_DIR/libantlr3c.a" "$INSTALL_LIB_DIR/libantlr3c-static.a"
make clean
-if [ ${MACHINE_TYPE} == 'x86_64' ]; then
+if [ "${MACHINE_TYPE}" == 'x86_64' ]; then
# 64-bit stuff here
- ./configure --enable-64bit --with-pic --disable-antlrdebug --prefix="${PREFIX}" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
+ ./configure --enable-64bit --with-pic --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
else
# 32-bit stuff here
- ./configure --with-pic --disable-antlrdebug --prefix="${PREFIX}" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
+ ./configure --with-pic --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
fi
cp Makefile Makefile.orig
sed 's,^\(CFLAGS = .*\),\1 -fexceptions,' Makefile.orig > Makefile
make CFLAGS="${MAKE_CFLAGS}" CXXFLAGS="${MAKE_CXXFLAGS}" LDFLAGS="${MAKE_LDFLAGS}"
make install
-cd ../..
-mv lib/libantlr3c.la lib/libantlr3c.la.orig
-awk '/^old_library=/ {print "old_library='\''libantlr3c-static.a'\''"} /^library_names=/ {print "library_names='\''libantlr3c.a'\''"} !/^old_library=/ && !/^library_names=/ {print}' < lib/libantlr3c.la.orig > lib/libantlr3c.la
-set +x
-cd ..
+mv "$INSTALL_LIB_DIR/libantlr3c.la" "$INSTALL_LIB_DIR/libantlr3c.la.orig"
-# echo
-# echo Invalidating generated parsers..
-# touch src/parser/*/*.g
+awk '/^old_library=/ {print "old_library='\''libantlr3c-static.a'\''"} /^library_names=/ {print "library_names='\''libantlr3c.a'\''"} !/^old_library=/ && !/^library_names=/ {print}' < "$INSTALL_LIB_DIR/libantlr3c.la.orig" > "$INSTALL_LIB_DIR/libantlr3c.la"
+rm "$INSTALL_LIB_DIR/libantlr3c.la.orig"
-if [ ${MACHINE_TYPE} == 'x86_64' ]; then
+if [ "${MACHINE_TYPE}" == 'x86_64' ]; then
# 64-bit stuff here
echo ============== WARNING ====================
echo The script guessed that this machine is 64 bit.
else
# 32-bit stuff here
- echo ============== WARNING ====================
+ echo ============== WARNING ====================
echo The script guessed that this machine is 32 bit.
echo If antlr should be built as 64 bit \(i.e. -m64\),
echo please rerun the script as
#
source "$(dirname "$0")/get-script-header.sh"
-if [ -e cadical ]; then
- echo 'error: file or directory "cadical" exists; please move it out of the way.' >&2
- exit 1
-fi
-
+CADICAL_DIR="$DEPS_DIR/cadical"
version="rel-1.0.3"
-webget "https://github.com/arminbiere/cadical/archive/$version.tar.gz" "cadical-$version.tar.gz"
-tar xfvz "cadical-$version.tar.gz"
-rm "cadical-$version.tar.gz"
-mv "cadical-$version" cadical
-cd cadical
+check_dep_dir "$CADICAL_DIR"
+setup_dep \
+ "https://github.com/arminbiere/cadical/archive/$version.tar.gz" "$CADICAL_DIR"
+cd "$CADICAL_DIR"
CXXFLAGS="-fPIC" ./configure && make -j$(nproc)
+install_lib build/libcadical.a
+install_includes src/cadical.hpp
+
echo
-echo "Using CaDiCaL commit $commit"
+echo "Using CaDiCaL version $version"
echo
echo ===================== Now configure CVC4 with =====================
echo ./configure.sh --cadical
#
source "$(dirname "$0")/get-script-header.sh"
-if [ -e cryptominisat5 ]; then
- echo 'error: file or directory "cryptominisat5" exists; please move it out of the way.' >&2
- exit 1
-fi
-
+CMS_DIR="$DEPS_DIR/cryptominisat5"
version="5.6.3"
-webget https://github.com/msoos/cryptominisat/archive/$version.tar.gz cryptominisat-$version.tar.gz
-tar xfvz cryptominisat-$version.tar.gz
-rm cryptominisat-$version.tar.gz
-mv cryptominisat-$version cryptominisat5
+check_dep_dir "$CMS_DIR"
+setup_dep \
+ "https://github.com/msoos/cryptominisat/archive/$version.tar.gz" \
+ "$CMS_DIR"
+cd "$CMS_DIR"
-cd cryptominisat5
mkdir build
cd build
-
cmake -DENABLE_PYTHON_INTERFACE=OFF \
-DSTATICCOMPILE=ON \
-DNOM4RI=ON \
+ -DONLY_SIMPLE=ON \
+ -DCMAKE_INSTALL_PREFIX="$INSTALL_DIR" \
..
-make libcryptominisat5 -j$(nproc)
+make install -j$(nproc)
echo
echo ===================== Now configure CVC4 with =====================
#!/usr/bin/env bash
#
source "$(dirname "$0")/get-script-header.sh"
-if [ -e drat2er ]; then
- echo 'error: file or directory "drat2er" exists; please move it out of the way.' >&2
- exit 1
-fi
-git clone https://github.com/alex-ozdemir/drat2er.git
+DRAT2ER_DIR="$DEPS_DIR/drat2er"
+commit=521caf16149df3dfa46f700ec1fab56f8cc12a18
-cd drat2er
-
-git checkout api
+check_dep_dir "$DRAT2ER_DIR"
+setup_dep \
+ "https://github.com/alex-ozdemir/drat2er/archive/$commit.tar.gz" \
+ "$DRAT2ER_DIR"
+cd "$DRAT2ER_DIR"
mkdir build
-
cd build
-
-cmake .. -DCMAKE_INSTALL_PREFIX=$(pwd)/install
-
-make install
+cmake .. -DCMAKE_INSTALL_PREFIX="$INSTALL_DIR"
+make install -j$(nproc)
echo
echo ===================== Now configure CVC4 with =====================
#
source "$(dirname "$0")/get-script-header.sh"
+GLPK_DIR="$DEPS_DIR/glpk-cut-log"
commit=b420454e732f4b3d229c552ef7cd46fec75fe65c
-if [ -e glpk-cut-log ]; then
- echo 'error: file or directory "glpk-cut-log" exists; please move it out of the way.' >&2
- exit 1
-fi
-
-mkdir glpk-cut-log
-cd glpk-cut-log
-webget https://github.com/timothy-king/glpk-cut-log/archive/$commit.zip glpk-cut-log-$commit.zip
-unzip glpk-cut-log-$commit.zip
-cd glpk-cut-log-$commit
+check_dep_dir "$GLPK_DIR"
+setup_dep \
+ "https://github.com/timothy-king/glpk-cut-log/archive/$commit.tar.gz" \
+ "$GLPK_DIR"
+cd "$GLPK_DIR"
libtoolize
aclocal
autoheader
autoconf
automake --add-missing
-./configure --without-pic --prefix=`pwd`/.. --disable-shared --enable-static --disable-dependency-tracking
-make && make install
-mv `pwd`/../lib/libglpk.a `pwd`/../lib/libglpk-static.a
+
+./configure --without-pic --prefix="$INSTALL_DIR" --disable-shared --enable-static --disable-dependency-tracking
+make install -j$(nproc)
make distclean
-./configure --with-pic --prefix=`pwd`/.. --disable-shared --enable-static --disable-dependency-tracking
-make && make install
+mv "$INSTALL_LIB_DIR/libglpk.a" "$INSTALL_LIB_DIR/libglpk-static.a"
-cd ..
+./configure --with-pic --prefix="$INSTALL_DIR" --disable-shared --enable-static --disable-dependency-tracking
+make install -j$(nproc)
echo
echo ===================== Now configure CVC4 with =====================
[ -n "$HOST" ] && HOST="--host=$HOST"
[ -z "$GMPVERSION" ] && GMPVERSION=6.1.2
+GMP_DIR="$DEPS_DIR/gmp-$GMPVERSION"
+
+check_dep_dir "$GMP_DIR"
+
echo =============================================================================
echo
echo "Setting up GMP $GMPVERSION..."
echo
-( set -ex
- mkdir gmp-$GMPVERSION
- cd gmp-$GMPVERSION
- gmpprefix=`pwd` &&
- mkdir src &&
- cd src &&
- webget https://gmplib.org/download/gmp/gmp-$GMPVERSION.tar.bz2 gmp-$GMPVERSION.tar.bz2 &&
- tar xfj gmp-$GMPVERSION.tar.bz2 &&
- cd gmp-$GMPVERSION &&
- ./configure ${HOST} --prefix="$gmpprefix" --enable-cxx ${BUILD_TYPE} &&
- make CFLAGS="${MAKE_CFLAGS}" CXXFLAGS="${MAKE_CXXFLAGS}" LDFLAGS="${MAKE_LDFLAGS}" &&
- make install
-) || exit 1
+setup_dep "https://gmplib.org/download/gmp/gmp-$GMPVERSION.tar.bz2" "$GMP_DIR"
+cd "$GMP_DIR"
+./configure ${HOST} --prefix="$INSTALL_DIR" --enable-cxx ${BUILD_TYPE}
+make \
+ CFLAGS="${MAKE_CFLAGS}" \
+ CXXFLAGS="${MAKE_CXXFLAGS}" \
+ LDFLAGS="${MAKE_LDFLAGS}" \
+ -j$(nproc)
+make install
echo
#
source "$(dirname "$0")/get-script-header.sh"
-lfscrepo="https://github.com/CVC4/LFSC.git"
-dirname="lfsc-checker"
+LFSC_DIR="$DEPS_DIR/lfsc-checker"
+version="master"
-function gitclone {
- if [ -x "$(command -v git)" ]
- then
- git clone "$1" "$2"
- else
- echo "Need git to clone LFSC checker. Please install git." >&2
- exit 1
- fi
-}
+check_dep_dir "$LFSC_DIR"
+setup_dep "https://github.com/CVC4/LFSC/archive/$version.tar.gz" "$LFSC_DIR"
+cd "$LFSC_DIR"
-if [ -e lfsc-checker ]; then
- echo 'error: file or directory "lfsc-checker" already exists!' >&2
- exit 1
-fi
-
-mkdir $dirname
-cd $dirname
-
-LFSC_PATH=`pwd`
-
-gitclone $lfscrepo .
-mkdir install
mkdir build
cd build
-cmake -DCMAKE_INSTALL_PREFIX:PATH=$LFSC_PATH/install ..
-make install
-cd ..
+cmake -DCMAKE_INSTALL_PREFIX="$INSTALL_DIR" ..
+make install -j$(nproc)
echo
echo ===================== Now configure CVC4 with =====================
#
set -e -o pipefail
-cd "$(dirname "$0")/.."
+[ ! -d contrib ] && echo "$0 not called from base directory" && exit 1
+
+DEPS_DIR="$(pwd)/deps"
+INSTALL_DIR="$DEPS_DIR/install"
+INSTALL_LIB_DIR="$INSTALL_DIR/lib"
+INSTALL_INCLUDE_DIR="$INSTALL_DIR/include"
+INSTALL_BIN_DIR="$INSTALL_DIR/bin"
+
+mkdir -p "$DEPS_DIR"
if ! [ -e src/parser/cvc/Cvc.g ]; then
echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2
echo "Error: Couldn't find python, python2, or python3." >&2
exit 1
fi
+
+function setup_dep
+{
+ url="$1"
+ directory="$2"
+ echo "Setting up $directory ..."
+ mkdir -p "$directory"
+ cd "$directory"
+ webget "$url" archive
+ tar xf archive --strip 1 # Strip top-most directory
+ rm archive
+}
+
+function check_dep_dir
+{
+ if [ -e "$1" ]; then
+ echo "error: file or directory '$1' exists; please move it out of the way." >&2
+ exit 1
+ fi
+}
+
+
+# Some of our dependencies do not provide a make install rule. Use the
+# following helper functions to copy libraries/headers/binaries into the
+# corresponding directories in deps/install.
+
+function install_lib
+{
+ echo "Copying $1 to $INSTALL_LIB_DIR"
+ [ ! -d "$INSTALL_LIB_DIR" ] && mkdir -p "$INSTALL_LIB_DIR"
+ cp "$1" "$INSTALL_LIB_DIR"
+}
+
+function install_includes
+{
+ include="$1"
+ subdir="$2"
+ echo "Copying $1 to $INSTALL_INCLUDE_DIR/$subdir"
+ [ ! -d "$INSTALL_INCLUDE_DIR" ] && mkdir -p "$INSTALL_INCLUDE_DIR"
+ [ -n "$subdir" ] && [ ! -d "$INSTALL_INCLUDE_DIR/$subdir" ] && mkdir -p "$INSTALL_INCLUDE_DIR/$subdir"
+ cp -r "$include" "$INSTALL_INCLUDE_DIR/$subdir"
+}
+
+function install_bin
+{
+ echo "Copying $1 to $INSTALL_BIN_DIR"
+ [ ! -d "$INSTALL_BIN_DIR" ] && mkdir -p "$INSTALL_BIN_DIR"
+ cp "$1" "$INSTALL_BIN_DIR"
+}
#
source "$(dirname "$0")/get-script-header.sh"
-wdir="symfpu-CVC4"
-
-if [ -e $wdir ]; then
- echo "error: file or directory "$wdir" exists; please move it out of the way." >&2
- exit 1
-fi
-
+SYMFPU_DIR="$DEPS_DIR/symfpu-CVC4"
commit="8fbe139bf0071cbe0758d2f6690a546c69ff0053"
-mkdir $wdir
-cd $wdir
-git clone https://github.com/martin-cs/symfpu.git symfpu
-cd symfpu
-git checkout $commit
+check_dep_dir "$SYMFPU_DIR"
+setup_dep \
+ "https://github.com/martin-cs/symfpu/archive/$commit.tar.gz" "$SYMFPU_DIR"
+cd "$SYMFPU_DIR"
+install_includes core symfpu
+install_includes utils symfpu
echo
echo "Using symfpu commit $commit"
projects / cvc5.git / commitdiff