From 92e7cda9c323b0e8acef90d4a109b29f33b4fccb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=81ron=20Ricardo=20Perez-Lopez?= Date: Sat, 31 Aug 2024 06:44:55 -0400 Subject: [PATCH] Switch default solver to Bitwuzla (#348) --- CMakeLists.txt | 29 +++++++++++++++-------------- README.md | 2 +- configure.sh | 10 +++++----- contrib/setup-smt-switch.sh | 18 +++++++++--------- options/options.h | 2 +- smt/available_solvers.cpp | 22 +++++++++++----------- 6 files changed, 42 insertions(+), 41 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 581922b7..28302bdb 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -28,8 +28,8 @@ else() set(SHARED_LIB_EXT "so") endif() -if (WITH_BITWUZLA) - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DWITH_BITWUZLA") +if (WITH_BOOLECTOR) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DWITH_BOOLECTOR") endif() if (WITH_MSAT) @@ -69,10 +69,13 @@ set(SMT_SWITCH_DIR "${PROJECT_SOURCE_DIR}/deps/smt-switch") set(CMAKE_MODULE_PATH ${SMT_SWITCH_DIR}/cmake) find_package(GMP REQUIRED) +find_package(PkgConfig REQUIRED) # Check that dependencies are there list(APPEND CMAKE_PREFIX_PATH "${SMT_SWITCH_DIR}/deps/install") +pkg_check_modules(BITWUZLA REQUIRED bitwuzla) + if (NOT EXISTS "${SMT_SWITCH_DIR}/local/include/smt-switch/smt.h") message(FATAL_ERROR "Missing smt-switch headers -- try running ./contrib/setup-smt-switch.sh") endif() @@ -81,19 +84,17 @@ if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch.a") message(FATAL_ERROR "Missing smt-switch library -- try running ./contrib/setup-smt-switch.sh") endif() -if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-btor.a") - message(FATAL_ERROR "Missing smt-switch boolector library -- try running ./contrib/setup-smt-switch.sh") +if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-bitwuzla.a") + message(FATAL_ERROR "Missing smt-switch Bitwuzla library -- try running ./contrib/setup-smt-switch.sh") endif() if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-cvc5.a") - message(FATAL_ERROR "Missing smt-switch cvc5 library -- try running ./contrib/setup-smt-switch.sh --with-cvc5") + message(FATAL_ERROR "Missing smt-switch cvc5 library -- try running ./contrib/setup-smt-switch.sh") endif() -if (WITH_BITWUZLA) - find_package(PkgConfig REQUIRED) - pkg_check_modules(BITWUZLA REQUIRED bitwuzla) - if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-bitwuzla.a") - message(FATAL_ERROR "Missing smt-switch bitwuzla library -- try running ./contrib/setup-smt-switch.sh --with-bitwuzla") +if (WITH_BOOLECTOR) + if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-btor.a") + message(FATAL_ERROR "Missing smt-switch Boolector library -- try running ./contrib/setup-smt-switch.sh --with-btor") endif() endif() @@ -234,12 +235,11 @@ if (BUILD_PYTHON_BINDINGS) add_subdirectory(python) endif() -target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-btor.a") +target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-bitwuzla.a") target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-cvc5.a") -if (WITH_BITWUZLA) - target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-bitwuzla.a") - target_link_libraries(pono-lib PUBLIC ${BITWUZLA_LDFLAGS}) +if (WITH_BOOLECTOR) + target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-btor.a") endif() if (WITH_MSAT) @@ -277,6 +277,7 @@ endif() target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch.a") target_link_libraries(pono-lib PUBLIC "${PROJECT_SOURCE_DIR}/deps/btor2tools/build/lib/libbtor2parser.a") +target_link_libraries(pono-lib PUBLIC "${BITWUZLA_LDFLAGS}") target_link_libraries(pono-lib PUBLIC "${GMPXX_LIBRARIES}") target_link_libraries(pono-lib PUBLIC "${GMP_LIBRARIES}") target_link_libraries(pono-lib PUBLIC pthread) diff --git a/README.md b/README.md index b679b894..d8ce06d5 100644 --- a/README.md +++ b/README.md @@ -22,7 +22,7 @@ Pono was awarded the Oski Award under its original name _cosa2_ at [HWMCC'19](ht * [optional] Install bison and flex * If you don't have bison and flex installed globally, run `./contrib/setup-bison.sh` and `./contrib/setup-flex.sh` * Even if you do have bison, you might get errors about not being able to load `-ly`. In such a case, run the bison setup script. -* Run `./contrib/setup-smt-switch.sh` -- it will build smt-switch with boolector +* Run `./contrib/setup-smt-switch.sh` -- it will build smt-switch with Bitwuzla * [optional] to build with MathSAT (required for interpolant-based model checking) you need to obtain the libraries yourself * note that MathSAT is under a custom non-BSD compliant license and you must assume all responsibility for meeting the conditions * download the solver from https://mathsat.fbk.eu/download.html, unpack it and rename the directory to `./deps/mathsat` diff --git a/configure.sh b/configure.sh index 3cb00b94..5aaff701 100755 --- a/configure.sh +++ b/configure.sh @@ -13,7 +13,7 @@ Configures the CMAKE build environment. -h, --help display this message and exit --prefix=STR install directory (default: /usr/local/) --build-dir=STR custom build directory (default: build) ---with-bitwuzla build with Bitwuzla (default: off) +--with-btor build with Boolector (default: off) --with-msat build with MathSAT which has a custom non-BSD compliant license. (default : off) Required for interpolant based model checking --with-msat-ic3ia build with the open-source IC3IA implementation as a backend. (default: off) @@ -37,7 +37,7 @@ die () { build_dir=build install_prefix=default build_type=default -with_bitwuzla=default +with_boolector=default with_msat=default with_msat_ic3ia=default with_coreir=default @@ -75,7 +75,7 @@ do *) build_dir=$(pwd)/$build_dir ;; # make absolute path esac ;; - --with-bitwuzla) with_bitwuzla=ON;; + --with-btor) with_boolector=ON;; --with-msat) with_msat=ON;; --with-msat-ic3ia) with_msat_ic3ia=ON;; --with-coreir) with_coreir=ON;; @@ -109,8 +109,8 @@ cmake_opts="-DCMAKE_BUILD_TYPE=$buildtype -DPONO_LIB_TYPE=${lib_type} -DPONO_STA [ $install_prefix != default ] \ && cmake_opts="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix" -[ $with_bitwuzla != default ] \ - && cmake_opts="$cmake_opts -DWITH_BITWUZLA=$with_bitwuzla" +[ $with_boolector != default ] \ + && cmake_opts="$cmake_opts -DWITH_BOOLECTOR=$with_boolector" [ $with_msat != default ] \ && cmake_opts="$cmake_opts -DWITH_MSAT=$with_msat" diff --git a/contrib/setup-smt-switch.sh b/contrib/setup-smt-switch.sh index 73fd38e0..8e60b986 100755 --- a/contrib/setup-smt-switch.sh +++ b/contrib/setup-smt-switch.sh @@ -13,7 +13,7 @@ Usage: $0 [