contrib: Setup all dependencies in deps/ directory. (#3534)

20 files changed, 237 insertions, 358 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index c2ce3e6ac..7d8b6d9ab 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -33,6 +33,51 @@ set(CMAKE_CXX_EXTENSIONS OFF)
 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)
 set(LIBRARY_INSTALL_DIR lib)
@@ -286,7 +331,6 @@ else()
   find_package(PythonInterp REQUIRED)
 endif()
 
-set(GMP_HOME ${GMP_DIR})
 find_package(GMP REQUIRED)
 
 if(ENABLE_ASAN)
@@ -383,13 +427,11 @@ if(ENABLE_VALGRIND)
 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()
@@ -411,27 +453,23 @@ if(USE_CRYPTOMINISAT)
   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()
@@ -446,7 +484,6 @@ if(USE_READLINE)
 endif()
 
 if(USE_SYMFPU)
-  set(SymFPU_HOME ${SYMFPU_DIR})
   find_package(SymFPU REQUIRED)
   add_definitions(-DCVC4_USE_SYMFPU)
   set(CVC4_USE_SYMFPU 1)
diff --git a/cmake/FindABC.cmake b/cmake/FindABC.cmake
index c44019739..a6f182654 100644
--- a/cmake/FindABC.cmake
+++ b/cmake/FindABC.cmake
@@ -4,26 +4,12 @@
 # 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}
diff --git a/cmake/FindANTLR.cmake b/cmake/FindANTLR.cmake
index 5f574247b..e12af826a 100644
--- a/cmake/FindANTLR.cmake
+++ b/cmake/FindANTLR.cmake
@@ -4,33 +4,9 @@
 # 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).
diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake
index bd7de319a..5ca7ce7b0 100644
--- a/cmake/FindCaDiCaL.cmake
+++ b/cmake/FindCaDiCaL.cmake
@@ -3,28 +3,8 @@
 # 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
diff --git a/cmake/FindCryptoMiniSat.cmake b/cmake/FindCryptoMiniSat.cmake
index d96c54eb3..44b30ba7e 100644
--- a/cmake/FindCryptoMiniSat.cmake
+++ b/cmake/FindCryptoMiniSat.cmake
@@ -4,27 +4,8 @@
 # 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
diff --git a/cmake/FindDrat2Er.cmake b/cmake/FindDrat2Er.cmake
index a7c2538a5..dc6f2a9b0 100644
--- a/cmake/FindDrat2Er.cmake
+++ b/cmake/FindDrat2Er.cmake
@@ -3,26 +3,9 @@
 # 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
diff --git a/cmake/FindGLPK.cmake b/cmake/FindGLPK.cmake
index 1587ca821..390992639 100644
--- a/cmake/FindGLPK.cmake
+++ b/cmake/FindGLPK.cmake
@@ -4,27 +4,8 @@
 # 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)
diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake
index 8125a583b..08cee9690 100644
--- a/cmake/FindGMP.cmake
+++ b/cmake/FindGMP.cmake
@@ -3,28 +3,8 @@
 # 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)
diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake
index 7a666839b..6135c7891 100644
--- a/cmake/FindLFSC.cmake
+++ b/cmake/FindLFSC.cmake
@@ -3,28 +3,8 @@
 # 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
diff --git a/cmake/FindSymFPU.cmake b/cmake/FindSymFPU.cmake
index f0f9ebf0f..dd9dbe113 100644
--- a/cmake/FindSymFPU.cmake
+++ b/cmake/FindSymFPU.cmake
@@ -2,23 +2,7 @@
 # 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)
diff --git a/contrib/get-abc b/contrib/get-abc
index 5d3f32fb5..d69af9ef8 100755
--- a/contrib/get-abc
+++ b/contrib/get-abc
@@ -2,19 +2,12 @@
 #
 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
@@ -28,8 +21,17 @@ sed 's,\( *\)\(.*Libs_Init(\),\1//\2,;s,\( *\)\(.*Libs_End(\),\1//\2,' src/base/
 # 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 =====================
diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4
index ecc92d998..9ab0695b7 100755
--- a/contrib/get-antlr-3.4
+++ b/contrib/get-antlr-3.4
@@ -1,20 +1,20 @@
 #!/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
@@ -26,36 +26,33 @@ if [ -z "${MACHINE_TYPE}" ]; then
   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
@@ -67,35 +64,27 @@ if [[ $WINDOWS_BUILD == "yes" ]]; then
   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.
@@ -105,7 +94,7 @@ if [ ${MACHINE_TYPE} == 'x86_64' ]; then
 
 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
diff --git a/contrib/get-cadical b/contrib/get-cadical
index 6cc1208c6..8c512ad28 100755
--- a/contrib/get-cadical
+++ b/contrib/get-cadical
@@ -2,23 +2,21 @@
 #
 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
diff --git a/contrib/get-cryptominisat b/contrib/get-cryptominisat
index 379d75df1..2b85e1a91 100755
--- a/contrib/get-cryptominisat
+++ b/contrib/get-cryptominisat
@@ -2,28 +2,25 @@
 #
 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 =====================
diff --git a/contrib/get-drat2er b/contrib/get-drat2er
index 52c663ab3..f04365890 100755
--- a/contrib/get-drat2er
+++ b/contrib/get-drat2er
@@ -1,24 +1,20 @@
 #!/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 =====================
diff --git a/contrib/get-glpk-cut-log b/contrib/get-glpk-cut-log
index 85ea643a9..16acf97ae 100755
--- a/contrib/get-glpk-cut-log
+++ b/contrib/get-glpk-cut-log
@@ -2,32 +2,28 @@
 #
 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 =====================
diff --git a/contrib/get-gmp b/contrib/get-gmp
index aec125185..678103cf4 100755
--- a/contrib/get-gmp
+++ b/contrib/get-gmp
@@ -15,21 +15,21 @@ source "$(dirname "$0")/get-script-header.sh"
 [ -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
diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker
index 953d05d18..e7bee86c0 100755
--- a/contrib/get-lfsc-checker
+++ b/contrib/get-lfsc-checker
@@ -2,36 +2,17 @@
 #
 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 =====================
diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh
index 4e2a133b3..7a88b3be2 100644
--- a/contrib/get-script-header.sh
+++ b/contrib/get-script-header.sh
@@ -2,7 +2,15 @@
 #
 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
@@ -36,3 +44,52 @@ if [ -z "$PYTHON" ]; then
   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"
+}
diff --git a/contrib/get-symfpu b/contrib/get-symfpu
index b17c00299..885bad62e 100755
--- a/contrib/get-symfpu
+++ b/contrib/get-symfpu
@@ -2,20 +2,15 @@
 #
 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"