Use common Cadical dependency for various solvers (#350)

* Add setup script for Cadical

* Use same cadical library for cvc5 and boolector

* Add symlink to setup-cadical.sh in ci-scripts

* Make install command macOS-compatible

* Install cadical headers

CMakeLists.txt

@@ -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)

btor/CMakeLists.txt

@@ -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)
@@ -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

ci-scripts/setup-cadical.sh

@@ -0,0 +1 @@
+../contrib/setup-cadical.sh

contrib/setup-btor.sh

@@ -15,6 +15,7 @@ else
     NUM_CORES=1
 fi
 
+$DIR/setup-cadical.sh
 
 if [ ! -d "$DEPS/boolector" ]; then
     cd $DEPS
@@ -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

contrib/setup-cadical.sh

@@ -0,0 +1,35 @@
+#!/bin/bash
+set -o errexit
+set -o pipefail
+set -o nounset
+
+CADICAL_VERSION=rel-1.7.4
+
+SCRIPT_NAME="$(basename "${BASH_SOURCE[0]}")"
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+ROOT_DIR="$(cd "$SCRIPT_DIR/.." && pwd)"
+DEPS_DIR="$ROOT_DIR/deps"
+
+# Download
+mkdir -p "$DEPS_DIR"
+cd $DEPS_DIR
+if [[ ! -d "cadical" ]]; then
+    git clone https://github.com/arminbiere/cadical
+fi
+
+# Build
+cd cadical
+git checkout $CADICAL_VERSION
+if [[ -d "build" ]]; then
+    echo "$SCRIPT_NAME: $DEPS_DIR/cadical/build exists, skipping configure step"
+else
+    CXXFLAGS=-fPIC ./configure
+fi
+make
+
+# Install
+mkdir -p "$DEPS_DIR/install/lib"
+install -m644 "build/libcadical.a" "$DEPS_DIR/install/lib"
+mkdir -p "$DEPS_DIR/install/include"
+install -m644 "src/ccadical.h" "$DEPS_DIR/install/include"
+install -m644 "src/cadical.hpp" "$DEPS_DIR/install/include"

contrib/setup-cvc5.sh

@@ -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

cvc5/CMakeLists.txt

@@ -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")