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