Switch default solver to Bitwuzla

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,6 +69,9 @@ 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)
+
+pkg_check_modules(BITWUZLA REQUIRED bitwuzla)
 
 # Check that dependencies are there
 list(APPEND CMAKE_PREFIX_PATH "${SMT_SWITCH_DIR}/deps/install")
@@ -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,12 @@ 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 ${BITWUZLA_LDFLAGS})
+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)

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`

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"

contrib/setup-smt-switch.sh

@@ -13,7 +13,7 @@ Usage: $0 [<option> ...]
 Sets up the smt-switch API for interfacing with SMT solvers through a C++ API.
 
 -h, --help display this message and exit
---with-bitwuzla include Bitwuzla (default: off)
+--with-btor  include Boolector (default: off)
 --with-msat include MathSAT which is under a custom non-BSD compliant license (default: off)
 --cvc5-home use an already downloaded version of cvc5
 --python build python bindings (default: off)
@@ -26,7 +26,7 @@ die () {
  exit 1
 }
 
-WITH_BITWUZLA=default
+WITH_BOOLECOR=default
 WITH_MSAT=default
 CONF_OPTS=""
 WITH_PYTHON=default
@@ -39,9 +39,9 @@ do
  --with-msat)
  WITH_MSAT=ON
  CONF_OPTS="$CONF_OPTS --msat --msat-home=../mathsat";;
- --with-bitwuzla)
- WITH_BITWUZLA=ON
- CONF_OPTS="$CONF_OPTS --bitwuzla";;
+ --with-btor)
+ WITH_BOOLECTOR=ON
+ CONF_OPTS="$CONF_OPTS --btor";;
  --python)
  WITH_PYTHON=YES
  CONF_OPTS="$CONF_OPTS --python";;
@@ -68,15 +68,15 @@ if [ ! -d "$DEPS/smt-switch" ]; then
  git clone https://github.com/stanford-centaur/smt-switch
  cd smt-switch
  git checkout -f $SMT_SWITCH_VERSION
- ./contrib/setup-btor.sh
+ ./contrib/setup-bitwuzla.sh
  if [ $cvc5_home = default ]; then
  ./contrib/setup-cvc5.sh
  fi
- if [ $WITH_BITWUZLA = ON ]; then
- ./contrib/setup-bitwuzla.sh
+ if [ $WITH_BOOLECTOR = ON ]; then
+ ./contrib/setup-btor.sh
  fi
  # pass bison/flex directories from smt-switch perspective
- ./configure.sh --btor --cvc5 $CONF_OPTS --prefix=local --static --smtlib-reader --bison-dir=../bison/bison-install --flex-dir=../flex/flex-install
+ ./configure.sh --bitwuzla --cvc5 $CONF_OPTS --prefix=local --static --smtlib-reader --bison-dir=../bison/bison-install --flex-dir=../flex/flex-install
  cd build
  make -j$(nproc)
  make test

smt/available_solvers.cpp

@@ -26,11 +26,11 @@
 #include "smt-switch/printing_solver.h"
 
 // these two always included
-#include "smt-switch/boolector_factory.h"
+#include "smt-switch/bitwuzla_factory.h"
 #include "smt-switch/cvc5_factory.h"
 
-#if WITH_BITWUZLA
-#include "smt-switch/bitwuzla_factory.h"
+#if WITH_BOOLECTOR
+#include "smt-switch/boolector_factory.h"
 #endif
 
 #if WITH_MSAT
@@ -52,10 +52,10 @@ namespace pono {
 
 // list of regular (non-interpolator) solver enums
 const std::vector<SolverEnum> solver_enums({
- BTOR, CVC5,
+ BZLA, CVC5,
 
-#if WITH_BITWUZLA
- BZLA,
+#if WITH_BOOLECTOR
+ BTOR,
 #endif
 
 #if WITH_MSAT
@@ -74,18 +74,18 @@ SmtSolver create_solver_base(SolverEnum se, bool logging, bool printing = false)
  SmtSolver s;
  auto printing_style = smt::PrintingStyleEnum::DEFAULT_STYLE;
  switch (se) {
- case BTOR: {
- s = BoolectorSolverFactory::create(logging);
+ case BZLA: {
+ s = BitwuzlaSolverFactory::create(logging);
  break;
  }
  case CVC5: {
  s = Cvc5SolverFactory::create(logging);
  printing_style = smt::PrintingStyleEnum::CVC5_STYLE;
  break;
  }
-#if WITH_BITWUZLA
- case BZLA: {
- s = BitwuzlaSolverFactory::create(logging);
+#if WITH_BOOLECTOR
+ case BTOR: {
+ s = BoolectorSolverFactory::create(logging);
  break;
  }
 #endif