diff options
| -rw-r--r-- | CMakeLists.txt | 31 | ||||
| -rw-r--r-- | cmake/FindCryptoMiniSat.cmake | 18 |
2 files changed, 42 insertions, 7 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 624644fc4..355a315ff 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -106,14 +106,19 @@ message(STATUS "Building ${CMAKE_BUILD_TYPE} build") #-----------------------------------------------------------------------------# -option(USE_CLN "Use CLN instead of GMP" OFF) -option(ENABLE_PROOFS "Enable proof support" OFF) -option(USE_SYMFPU "Use SymFPU for floating point support" OFF) +option(ENABLE_PROOFS "Enable proof support" OFF) +option(USE_CLN "Use CLN instead of GMP" OFF) +option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver" OFF) +option(USE_SYMFPU "Use SymFPU for floating point support" OFF) #-----------------------------------------------------------------------------# find_package(PythonInterp REQUIRED) +find_package(ANTLR REQUIRED) +cvc4_link_library(${ANTLR_LIBRARIES}) +include_directories(${ANTLR_INCLUDE_DIR}) + find_package(GMP REQUIRED) cvc4_link_library(${GMP_LIBRARIES}) include_directories(${GMP_INCLUDE_DIR}) @@ -124,15 +129,23 @@ if(USE_CLN) include_directories(${CLN_INCLUDE_DIR}) endif() +if(USE_CRYPTOMINISAT) + # CryptoMiniSat requires pthreads support + set(THREADS_PREFER_PTHREAD_FLAG ON) + find_package(Threads REQUIRED) + if(THREADS_HAVE_PTHREAD_ARG) + add_c_cxx_flag(-pthread) + endif() + find_package(CryptoMiniSat REQUIRED) + cvc4_link_library(${CryptoMiniSat_LIBRARIES}) + include_directories(${CryptoMiniSat_INCLUDE_DIR}) +endif() + if(USE_SYMFPU) find_package(SymFPU REQUIRED) include_directories(${SymFPU_INCLUDE_DIR}) endif() -find_package(ANTLR REQUIRED) -cvc4_link_library(${ANTLR_LIBRARIES}) -include_directories(${ANTLR_INCLUDE_DIR}) - #-----------------------------------------------------------------------------# add_check_c_flag("-fexceptions") @@ -248,6 +261,10 @@ else() set(CVC4_USE_GMP_IMP 1) endif() +if(USE_CRYPTOMINISAT) + add_definitions(-DCVC4_USE_CRYPTOMINISAT) +endif() + if(USE_SYMFPU) add_definitions(-DCVC4_USE_SYMFPU) set(CVC4_USE_SYMFPU 1) diff --git a/cmake/FindCryptoMiniSat.cmake b/cmake/FindCryptoMiniSat.cmake new file mode 100644 index 000000000..1706efb9c --- /dev/null +++ b/cmake/FindCryptoMiniSat.cmake @@ -0,0 +1,18 @@ +# Find CryptoMiniSat +# CryptoMiniSat_FOUND - system has CryptoMiniSat lib +# CryptoMiniSat_INCLUDE_DIR - the CryptoMiniSat include directory +# CryptoMiniSat_LIBRARIES - Libraries needed to use CryptoMiniSat + +find_path(CryptoMiniSat_INCLUDE_DIR + NAMES cryptominisat5/cryptominisat.h + PATHS "${PROJECT_SOURCE_DIR}/cryptominisat5/install/include") +find_library(CryptoMiniSat_LIBRARIES + NAMES cryptominisat5 + PATHS "${PROJECT_SOURCE_DIR}/cryptominisat5/install/lib") + +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(CryptoMiniSat + DEFAULT_MSG + CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES) + +mark_as_advanced(CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES) |