diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-05-22 06:41:50 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-22 08:41:50 -0500 |
commit | c531152e6a707b66b885e508ea61e2a67e195ccc (patch) | |
tree | a18a2d342b03db1700a963470f2064cf3ac8d086 /CMakeLists.txt | |
parent | ae33f11d0f4156b4d21b9e77f6df59ec0f9e8184 (diff) |
Add support for SAT solver Kissat. (#4514)
Diffstat (limited to 'CMakeLists.txt')
-rw-r--r-- | CMakeLists.txt | 56 |
1 files changed, 35 insertions, 21 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index c535890e1..d34d6ebfe 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -67,6 +67,9 @@ endif() if(GMP_DIR) list(APPEND CMAKE_PREFIX_PATH "${GMP_DIR}") endif() +if(KISSAT_DIR) + list(APPEND CMAKE_PREFIX_PATH "${KISSAT_DIR}") +endif() if(LFSC_DIR) list(APPEND CMAKE_PREFIX_PATH "${LFSC_DIR}") endif() @@ -143,8 +146,9 @@ option(ENABLE_PROFILING "Enable support for gprof profiling") cvc4_option(USE_ABC "Use ABC for AIG bit-blasting") cvc4_option(USE_CADICAL "Use CaDiCaL SAT solver") cvc4_option(USE_CLN "Use CLN instead of GMP") -cvc4_option(USE_GLPK "Use GLPK simplex solver") cvc4_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver") +cvc4_option(USE_GLPK "Use GLPK simplex solver") +cvc4_option(USE_KISSAT "Use Kissat SAT solver") cvc4_option(USE_READLINE "Use readline for better interactive support") # >> 2-valued: ON OFF # > for options where we don't need to detect if set by user (default: OFF) @@ -167,6 +171,7 @@ 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(KISSAT_DIR "" CACHE STRING "Set Kissat install directory") set(LFSC_DIR "" CACHE STRING "Set LFSC install directory") set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory") @@ -483,6 +488,11 @@ if(USE_GLPK) add_definitions(-DCVC4_USE_GLPK) endif() +if(USE_KISSAT) + find_package(Kissat REQUIRED) + add_definitions(-DCVC4_USE_KISSAT) +endif() + if(USE_LFSC) set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc) find_package(LFSC REQUIRED) @@ -587,9 +597,9 @@ string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}") message("CVC4 ${CVC4_RELEASE_STRING}") message("") if(ENABLE_COMP_INC_TRACK) - message("Build profile : ${CVC4_BUILD_PROFILE_STRING} (incremental)") + message("Build profile : ${CVC4_BUILD_PROFILE_STRING} (incremental)") else() - message("Build profile : ${CVC4_BUILD_PROFILE_STRING}") + message("Build profile : ${CVC4_BUILD_PROFILE_STRING}") endif() message("") print_config("GPL :" ENABLE_GPL) @@ -627,55 +637,59 @@ print_config("CaDiCaL :" USE_CADICAL) print_config("CryptoMiniSat :" USE_CRYPTOMINISAT) print_config("drat2er :" USE_DRAT2ER) print_config("GLPK :" USE_GLPK) +print_config("Kissat :" USE_KISSAT) print_config("LFSC :" USE_LFSC) if(CVC4_USE_CLN_IMP) - message("MP library : cln") + message("MP library : cln") else() - message("MP library : gmp") + message("MP library : gmp") endif() print_config("Readline :" ${USE_READLINE}) print_config("SymFPU :" ${USE_SYMFPU}) message("") if(ABC_DIR) - message("ABC dir : ${ABC_DIR}") + message("ABC dir : ${ABC_DIR}") endif() if(ANTLR_DIR) - message("ANTLR dir : ${ANTLR_DIR}") + message("ANTLR dir : ${ANTLR_DIR}") endif() if(CADICAL_DIR) - message("CADICAL dir : ${CADICAL_DIR}") + message("CADICAL dir : ${CADICAL_DIR}") endif() if(CRYPTOMINISAT_DIR) - message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}") + message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}") endif() if(DRAT2ER_DIR) - message("DRAT2ER dir : ${DRAT2ER_DIR}") + message("DRAT2ER dir : ${DRAT2ER_DIR}") endif() if(GLPK_DIR) - message("GLPK dir : ${GLPK_DIR}") + message("GLPK dir : ${GLPK_DIR}") endif() if(GMP_DIR) - message("GMP dir : ${GMP_DIR}") + message("GMP dir : ${GMP_DIR}") +endif() +if(KISSAT_DIR) + message("KISSAT dir : ${KISSAT_DIR}") endif() if(LFSC_DIR) - message("LFSC dir : ${LFSC_DIR}") + message("LFSC dir : ${LFSC_DIR}") endif() if(SYMFPU_DIR) - message("SYMFPU dir : ${SYMFPU_DIR}") + message("SYMFPU dir : ${SYMFPU_DIR}") endif() message("") -message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}") -message("CXXFLAGS : ${CMAKE_CXX_FLAGS}") -message("CFLAGS : ${CMAKE_C_FLAGS}") -message("Linker flags : ${CMAKE_EXE_LINKER_FLAGS}") +message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}") +message("CXXFLAGS : ${CMAKE_CXX_FLAGS}") +message("CFLAGS : ${CMAKE_C_FLAGS}") +message("Linker flags : ${CMAKE_EXE_LINKER_FLAGS}") message("") -message("Install prefix : ${CMAKE_INSTALL_PREFIX}") +message("Install prefix : ${CMAKE_INSTALL_PREFIX}") message("") if(GPL_LIBS) message( - "CVC4 license : GPLv3 (due to optional libraries; see below)" + "CVC4 license : GPLv3 (due to optional libraries; see below)" "\n" "\n" "Please note that CVC4 will be built against the following GPLed libraries:" @@ -692,7 +706,7 @@ if(GPL_LIBS) ) else() message( - "CVC4 license : modified BSD" + "CVC4 license : modified BSD" "\n" "\n" "Note that this configuration is NOT built against any GPL'ed libraries, so" |