diff options
| -rw-r--r-- | CMakeLists.txt | 12 | ||||
| -rw-r--r-- | cmake/FindDrat2Er.cmake | 31 | ||||
| -rwxr-xr-x | configure.sh | 14 | ||||
| -rwxr-xr-x | contrib/get-drat2er | 25 | ||||
| -rw-r--r-- | src/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | src/base/configuration_private.h | 6 |
6 files changed, 92 insertions, 0 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 099fc00fa..3265830cc 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -93,6 +93,7 @@ cvc4_option(USE_READLINE "Use readline for better interactive support") # > for options where we don't need to detect if set by user (default: OFF) option(USE_CADICAL "Use CaDiCaL SAT solver") option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver") +option(USE_DRAT2ER "Include drat2er for making eager BV proofs") option(USE_LFSC "Use LFSC proof checker") option(USE_SYMFPU "Use SymFPU for floating point support") option(USE_PYTHON2 "Prefer using Python 2 (for Python bindings)") @@ -108,6 +109,7 @@ set(ANTLR_DIR "" CACHE STRING "Set ANTLR3 install directory") set(CADICAL_DIR "" CACHE STRING "Set CaDiCaL install directory") set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory") set(CXXTEST_DIR "" CACHE STRING "Set CxxTest install directory") +set(DRAT2ER_DIR "" CACHE STRING "Set drat2er install directory") set(GLPK_DIR "" CACHE STRING "Set GLPK install directory") set(GMP_DIR "" CACHE STRING "Set GMP install directory") set(LFSC_DIR "" CACHE STRING "Set LFSC install directory") @@ -410,6 +412,12 @@ if(USE_CRYPTOMINISAT) 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}) @@ -523,6 +531,7 @@ message("") print_config("ABC :" USE_ABC) print_config("CaDiCaL :" USE_CADICAL) print_config("CryptoMiniSat :" USE_CRYPTOMINISAT) +print_config("drat2er :" USE_DRAT2ER) print_config("GLPK :" USE_GLPK) print_config("LFSC :" USE_LFSC) @@ -546,6 +555,9 @@ endif() if(CRYPTOMINISAT_DIR) message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}") endif() +if(DRAT2ER_DIR) + message("DRAT2ER dir : ${DRAT2ER_DIR}") +endif() if(GLPK_DIR) message("GLPK dir : ${GLPK_DIR}") endif() diff --git a/cmake/FindDrat2Er.cmake b/cmake/FindDrat2Er.cmake new file mode 100644 index 000000000..e0bc8d446 --- /dev/null +++ b/cmake/FindDrat2Er.cmake @@ -0,0 +1,31 @@ +# Find drat2er +# Drat2Er_FOUND - system has Drat2Er lib +# 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) + +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(Drat2Er + DEFAULT_MSG + Drat2Er_INCLUDE_DIR Drat2Er_LIBRARIES) + +mark_as_advanced(Drat2Er_INCLUDE_DIR Drat2Er_LIBRARIES) +if(Drat2Er_LIBRARIES) + message(STATUS "Found Drat2Er libs: ${Drat2Er_LIBRARIES}") +endif() diff --git a/configure.sh b/configure.sh index 7fa842f70..e53d8caa7 100755 --- a/configure.sh +++ b/configure.sh @@ -55,6 +55,7 @@ The following flags enable optional packages (disable with --no-<option name>). --abc use the ABC AIG library --cadical use the CaDiCaL SAT solver --cryptominisat use the CryptoMiniSat SAT solver + --drat2er use drat2er (required for eager BV proofs) --lfsc use the LFSC proof checker --symfpu use SymFPU for floating point solver --portfolio build the multithreaded portfolio version of CVC4 @@ -66,6 +67,7 @@ Optional Path to Optional Packages: --antlr-dir=PATH path to ANTLR C headers and libraries --cadical-dir=PATH path to top level of CaDiCaL source tree --cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree + --drat2er-dir=PATH path to the top level of the drat2er installation --cxxtest-dir=PATH path to CxxTest installation --glpk-dir=PATH path to top level of GLPK installation --gmp-dir=PATH path to top level of GMP installation @@ -112,6 +114,7 @@ coverage=default cryptominisat=default debug_symbols=default debug_context_mm=default +drat2er=default dumping=default gpl=default win64=default @@ -141,6 +144,7 @@ abc_dir=default antlr_dir=default cadical_dir=default cryptominisat_dir=default +drat2er_dir=default cxxtest_dir=default glpk_dir=default gmp_dir=default @@ -202,6 +206,9 @@ do --debug-context-mm) debug_context_mm=ON;; --no-debug-context-mm) debug_context_mm=OFF;; + --drat2er) drat2er=ON;; + --no-drat2er) drat2er=OFF;; + --dumping) dumping=ON;; --no-dumping) dumping=OFF;; @@ -297,6 +304,9 @@ do --cxxtest-dir) die "missing argument to $1 (try -h)" ;; --cxxtest-dir=*) cxxtest_dir=${1##*=} ;; + --drat2er-dir) die "missing argument to $1 (try -h)" ;; + --drat2er-dir=*) drat2er_dir=${1##*=} ;; + --glpk-dir) die "missing argument to $1 (try -h)" ;; --glpk-dir=*) glpk_dir=${1##*=} ;; @@ -386,6 +396,8 @@ cmake_opts="" && cmake_opts="$cmake_opts -DUSE_CLN=$cln" [ $cryptominisat != default ] \ && cmake_opts="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat" +[ $drat2er != default ] \ + && cmake_opts="$cmake_opts -DUSE_DRAT2ER=$drat2er" [ $glpk != default ] \ && cmake_opts="$cmake_opts -DUSE_GLPK=$glpk" [ $lfsc != default ] \ @@ -408,6 +420,8 @@ cmake_opts="" && cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir" [ "$cxxtest_dir" != default ] \ && cmake_opts="$cmake_opts -DCXXTEST_DIR=$cxxtest_dir" +[ "$drat2er_dir" != default ] \ + && cmake_opts="$cmake_opts -DDRAT2ER_DIR=$drat2er_dir" [ "$glpk_dir" != default ] \ && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir" [ "$gmp_dir" != default ] \ diff --git a/contrib/get-drat2er b/contrib/get-drat2er new file mode 100755 index 000000000..e465ab3d4 --- /dev/null +++ b/contrib/get-drat2er @@ -0,0 +1,25 @@ +#!/bin/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 + +cd drat2er + +git checkout api + +mkdir build + +cd build + +cmake .. -DCMAKE_INSTALL_PREFIX=$(pwd)/install + +make install + +echo +echo ===================== Now configure CVC4 with ===================== +echo ./configure.sh --drat2er diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7ecee2dee..889260045 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -739,6 +739,10 @@ if(USE_CRYPTOMINISAT) target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES}) target_include_directories(cvc4 PUBLIC ${CryptoMiniSat_INCLUDE_DIR}) endif() +if(USE_DRAT2ER) + target_link_libraries(cvc4 ${Drat2Er_LIBRARIES}) + target_include_directories(cvc4 PUBLIC ${Drat2Er_INCLUDE_DIR}) +endif() if(USE_GLPK) target_link_libraries(cvc4 ${GLPK_LIBRARIES}) target_include_directories(cvc4 PUBLIC ${GLPK_INCLUDE_DIR}) diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 5164d46bc..77f3f5e77 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -126,6 +126,12 @@ namespace CVC4 { # define IS_CRYPTOMINISAT_BUILD false #endif /* CVC4_USE_CRYPTOMINISAT */ +#if CVC4_USE_DRAT2ER +# define IS_DRAT2ER_BUILD true +#else /* CVC4_USE_DRAT2ER */ +# define IS_DRAT2ER_BUILD false +#endif /* CVC4_USE_DRAT2ER */ + #if CVC4_USE_LFSC #define IS_LFSC_BUILD true #else /* CVC4_USE_LFSC */ |