Update Bitwuzla code for new API (#347)

stanford-centaur · Jun 18, 2024 · 2da835b · 2da835b
1 parent b099b2d
commit 2da835b
Show file tree

Hide file tree

Showing 14 changed files with 487 additions and 619 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -9,6 +9,7 @@ jobs:
         name:
           [
             btor,
+            bitwuzla,
             cvc5,
             msat,
             yices2,
@@ -35,6 +36,7 @@ jobs:
             cmake \
             gperf \
             libgmp-dev \
+            ninja-build \
             openjdk-8-jdk
 
       - name: Install Packages (macOS)
@@ -44,6 +46,7 @@ jobs:
           brew install \
             gmp \
             gperf \
+            ninja \
             ${{ matrix.extra_macos_packages }}
           echo "LDFLAGS=-L$(brew --prefix)/lib $LDFLAGS" >> "$GITHUB_ENV"
           echo "CFLAGS=-I$(brew --prefix)/include $CFLAGS" >> "$GITHUB_ENV"
@@ -55,7 +58,12 @@ jobs:
           python3 -m venv ./.venv
           source ./.venv/bin/activate
           python3 -m pip install Cython==0.29.*
-          python3 -m pip install pytest scikit-build toml pyparsing
+          python3 -m pip install \
+            pytest \
+            scikit-build \
+            toml \
+            pyparsing \
+            meson
           echo "$PWD/.venv/bin" >> $GITHUB_PATH
 
       - name: Install Bison

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -150,14 +150,15 @@ endif (BUILD_BTOR)
 option (BUILD_BITWUZLA
   "Should we build the libraries for bitwuzla" OFF)
 if (BUILD_BITWUZLA)
-  if (NOT DEFINED BITWUZLA_HOME)
-    set(BITWUZLA_HOME "${PROJECT_SOURCE_DIR}/deps/bitwuzla")
+  if (NOT DEFINED BITWUZLA_DIR)
+    # default location if using contrib/setup-bitwuzla.sh
+    # will also search global paths
+    set (BITWUZLA_DIR "${PROJECT_SOURCE_DIR}/deps/install")
   endif()
   add_subdirectory (bitwuzla)
   set (SOLVER_BACKEND_LIBS ${SOLVER_BACKEND_LIBS} smt-switch-bitwuzla)
 
   add_definitions(-DBUILD_BITWUZLA)
-  add_definitions(-DBITWUZLA_HOME=${BITWUZLA_HOME})
 endif (BUILD_BITWUZLA)
 
 

diff --git a/bitwuzla/CMakeLists.txt b/bitwuzla/CMakeLists.txt
@@ -1,5 +1,10 @@
 set(CMAKE_POSITION_INDEPENDENT_CODE ON)
 
+# Find Bitwuzla installation
+list(PREPEND CMAKE_PREFIX_PATH "${BITWUZLA_DIR}")
+find_package(PkgConfig REQUIRED)
+pkg_check_modules(BITWUZLA REQUIRED bitwuzla)
+
 add_library(smt-switch-bitwuzla "${SMT_SWITCH_LIB_TYPE}"
   "${CMAKE_CURRENT_SOURCE_DIR}/src/bitwuzla_factory.cpp"
   "${CMAKE_CURRENT_SOURCE_DIR}/src/bitwuzla_solver.cpp"
@@ -8,37 +13,11 @@ add_library(smt-switch-bitwuzla "${SMT_SWITCH_LIB_TYPE}"
   )
 
 target_include_directories (smt-switch-bitwuzla PUBLIC "${PROJECT_SOURCE_DIR}/include")
-target_include_directories (smt-switch-bitwuzla PUBLIC "${PROJECT_SOURCE_DIR}/contrib/memstream-0.1/")
 target_include_directories (smt-switch-bitwuzla PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/include")
-target_include_directories (smt-switch-bitwuzla PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/bitwuzla/include")
-target_include_directories (smt-switch-bitwuzla PUBLIC "${BITWUZLA_HOME}/src/api/c")
-target_include_directories (smt-switch-bitwuzla PUBLIC ${GMP_INCLUDE_DIR})
+target_include_directories (smt-switch-bitwuzla PUBLIC ${BITWUZLA_INCLUDE_DIRS})
 
-target_link_libraries(smt-switch-bitwuzla "${BITWUZLA_HOME}/build/lib/libbitwuzla.a")
-target_link_libraries(smt-switch-bitwuzla "${BITWUZLA_HOME}/deps/cadical/build/libcadical.a")
-target_link_libraries(smt-switch-bitwuzla "${BITWUZLA_HOME}/deps/btor2tools/build/lib/libbtor2parser.a")
 target_link_libraries(smt-switch-bitwuzla smt-switch)
-target_link_libraries(smt-switch-bitwuzla pthread)
-target_link_libraries(smt-switch-bitwuzla m)
-target_link_libraries(smt-switch-bitwuzla ${GMP_LIBRARIES})
-
-if (SMT_SWITCH_LIB_TYPE STREQUAL STATIC)
-  # we want the static library to include the bitwuzla source
-  # we need to unpack and repack the libraries
-  add_custom_target(repack-bitwuzla-static-lib
-    ALL
-    COMMAND
-      mkdir smt-switch-bitwuzla && cd smt-switch-bitwuzla && ar -x "../$<TARGET_FILE_NAME:smt-switch-bitwuzla>" && cd ../ &&
-      mkdir bitwuzla && cd bitwuzla && ar -x "${BITWUZLA_HOME}/build/lib/libbitwuzla.a" &&
-      ar -x "${BITWUZLA_HOME}/deps/cadical/build/libcadical.a" &&
-      ar -x "${BITWUZLA_HOME}/deps/btor2tools/build/lib/libbtor2parser.a" && cd ../ &&
-      ar -qc "$<TARGET_FILE_NAME:smt-switch-bitwuzla>" ./bitwuzla/*.o ./smt-switch-bitwuzla/*.o &&
-      # now clean up
-      rm -rf smt-switch-bitwuzla bitwuzla
-    DEPENDS
-      smt-switch-bitwuzla
-    )
-endif()
+target_link_libraries(smt-switch-bitwuzla ${BITWUZLA_LDFLAGS})
 
 install(TARGETS smt-switch-bitwuzla DESTINATION lib)
 # install headers -- for expert use only

diff --git a/bitwuzla/include/bitwuzla_solver.h b/bitwuzla/include/bitwuzla_solver.h
@@ -16,20 +16,17 @@
 
 #pragma once
 
-#include <signal.h>
-#include <unistd.h>
-
+#include <cstdint>
 #include <memory>
 #include <string>
-#include <unordered_set>
+#include <unordered_map>
 #include <vector>
 
-#include "bitwuzla_sort.h"
+#include "bitwuzla/cpp/bitwuzla.h"
 #include "bitwuzla_term.h"
-#include "exceptions.h"
 #include "result.h"
 #include "smt.h"
-#include "sort.h"
+#include "utils.h"
 
 namespace smt {
 
@@ -41,37 +38,18 @@ class BzlaSolver : public AbsSmtSolver
  public:
   BzlaSolver()
       : AbsSmtSolver(BZLA),
-        bzla(bitwuzla_new()),
-        context_level(0),
-        time_limit(0),
-        terminate_bzla(false)
-  {
-    // set termination function -- throw an exception
-    auto throw_exception = [](const char * msg) -> void {
-      throw InternalSolverException(msg);
-    };
-    bitwuzla_set_abort_callback(throw_exception);
-
-    // this termination callback is used to support a time limit option
-    // used in conjunction with C alarm function. See timelimit_start()
-    // and timelimit_end() helper functions
-    auto terminate = [](void * state) -> int32_t {
-      bool terminate_bzla = *reinterpret_cast<bool *>(state);
-      if (terminate_bzla)
-      {
-        return 1;
-      }
-      return 0;
-    };
-    bitwuzla_set_termination_callback(bzla, terminate, &terminate_bzla);
-  };
+        options(),
+        tm(new bitwuzla::TermManager()),
+        bzla(nullptr),
+        context_level(0){};
   BzlaSolver(const BzlaSolver &) = delete;
   BzlaSolver & operator=(const BzlaSolver &) = delete;
   ~BzlaSolver()
   {
     // need to destruct all stored terms in symbol_table
     symbol_table.clear();
-    bitwuzla_delete(bzla);
+    delete bzla;
+    delete tm;
   };
   void set_opt(const std::string option, const std::string value) override;
   void set_logic(const std::string logic) override;
@@ -80,16 +58,16 @@ class BzlaSolver : public AbsSmtSolver
   Result check_sat_assuming(const TermVec & assumptions) override;
   Result check_sat_assuming_list(const TermList & assumptions) override;
   Result check_sat_assuming_set(const UnorderedTermSet & assumptions) override;
-  void push(uint64_t num = 1) override;
-  void pop(uint64_t num = 1) override;
-  uint64_t get_context_level() const override;
+  void push(std::uint64_t num = 1) override;
+  void pop(std::uint64_t num = 1) override;
+  std::uint64_t get_context_level() const override;
   Term get_value(const Term & t) const override;
   UnorderedTermMap get_array_values(const Term & arr,
                                     Term & out_const_base) const override;
   void get_unsat_assumptions(UnorderedTermSet & out) override;
-  Sort make_sort(const std::string name, uint64_t arity) const override;
+  Sort make_sort(const std::string name, std::uint64_t arity) const override;
   Sort make_sort(SortKind sk) const override;
-  Sort make_sort(SortKind sk, uint64_t size) const override;
+  Sort make_sort(SortKind sk, std::uint64_t size) const override;
   Sort make_sort(SortKind sk, const Sort & sort1) const override;
   Sort make_sort(SortKind sk,
                  const Sort & sort1,
@@ -119,10 +97,10 @@ class BzlaSolver : public AbsSmtSolver
                     std::string name) const override;
 
   Term make_term(bool b) const override;
-  Term make_term(int64_t i, const Sort & sort) const override;
+  Term make_term(std::int64_t i, const Sort & sort) const override;
   Term make_term(const std::string val,
                  const Sort & sort,
-                 uint64_t base = 10) const override;
+                 std::uint64_t base = 10) const override;
   Term make_term(const Term & val, const Sort & sort) const override;
   Term make_symbol(const std::string name, const Sort & sort) override;
   Term get_symbol(const std::string & name) override;
@@ -146,63 +124,59 @@ class BzlaSolver : public AbsSmtSolver
 
   // getters for solver-specific objects
   // for interacting with third-party Bitwuzla-specific software
-
-  Bitwuzla * get_bitwuzla() const { return bzla; };
+  bitwuzla::Bitwuzla * get_bitwuzla() const
+  {
+    if (bzla == nullptr)
+    {
+      bzla = new bitwuzla::Bitwuzla(*tm, options);
+    }
+    return bzla;
+  }
 
  protected:
-  Bitwuzla * bzla;
+  bitwuzla::Options options;
+  bitwuzla::TermManager * tm;
+  mutable bitwuzla::Bitwuzla * bzla;
 
   std::unordered_map<std::string, Term> symbol_table;
-
-  uint64_t context_level;
-
-  uint64_t time_limit;
-  bool terminate_bzla;  ///< used if time limit is reached
+  std::uint64_t context_level;
 
   // helper functions
-  template <class I>
-  inline Result check_sat_assuming_internal(I it, const I & end)
+  template <class T>
+  inline Result check_sat_assuming_internal(T container)
   {
     std::shared_ptr<BzlaTerm> bt;
-    while (it != end)
+    std::vector<bitwuzla::Term> assumptions;
+    for (auto && t : container)
     {
-      bt = std::static_pointer_cast<BzlaTerm>(*it);
-      bitwuzla_assume(bzla, bt->term);
-      ++it;
+      bt = std::static_pointer_cast<BzlaTerm>(t);
+      assumptions.push_back(bt->term);
     }
 
-    timelimit_start();
-    BitwuzlaResult res = bitwuzla_check_sat(bzla);
-    bool tl_triggered = timelimit_end();
-    if (res == BITWUZLA_SAT)
+    bitwuzla::Result res;
+    try
     {
-      return Result(SAT);
+      res = get_bitwuzla()->check_sat(assumptions);
     }
-    else if (res == BITWUZLA_UNSAT)
+    catch (std::exception & e)
     {
-      return Result(UNSAT);
+      throw InternalSolverException(e.what());
+    }
+
+    if (res == bitwuzla::Result::SAT)
+    {
+      return Result(SAT);
     }
-    else if (tl_triggered)
+    else if (res == bitwuzla::Result::UNSAT)
     {
-      return Result(UNKNOWN, "Time limit reached.");
+      return Result(UNSAT);
     }
     else
     {
+      Assert(res == bitwuzla::Result::UNKNOWN);
       return Result(UNKNOWN);
     }
   }
-
-  /** Helper function for managing time limits (if one is set)
-   *  Registers a signal handler to use with alarm
-   *  and a termination callback function.
-   */
-  void timelimit_start();
-
-  /** Helper function for managing time limits (if one is set)
-   *  Returns true iff the query was terminated due to the
-   *  time limit.
-   */
-  bool timelimit_end();
 };
 
 }  // namespace smt
diff --git a/bitwuzla/include/bitwuzla_sort.h b/bitwuzla/include/bitwuzla_sort.h
@@ -16,10 +16,12 @@
 
 #pragma once
 
-#include "bitwuzla.h"
-#include "exceptions.h"
-#include "sort.h"
-#include "utils.h"
+#include <cstddef>
+#include <cstdint>
+#include <string>
+
+#include "bitwuzla/cpp/bitwuzla.h"
+#include "smt.h"
 
 namespace smt {
 
@@ -29,16 +31,16 @@ class BzlaSolver;
 class BzlaSort : public AbsSort
 {
  public:
-  BzlaSort(const BitwuzlaSort * s) : sort(s){};
+  BzlaSort(const bitwuzla::Sort s) : sort(s){};
   virtual ~BzlaSort();
   std::size_t hash() const override;
-  uint64_t get_width() const override;
+  std::uint64_t get_width() const override;
   Sort get_indexsort() const override;
   Sort get_elemsort() const override;
   SortVec get_domain_sorts() const override;
   Sort get_codomain_sort() const override;
   std::string get_uninterpreted_name() const override;
-  size_t get_arity() const override;
+  std::size_t get_arity() const override;
   SortVec get_uninterpreted_param_sorts() const override;
   Datatype get_datatype() const override;
   bool compare(const Sort & s) const override;
@@ -47,11 +49,11 @@ class BzlaSort : public AbsSort
   // getters for solver-specific objects
   // for interacting with third-party Bitwuzla-specific software
 
-  const BitwuzlaSort * get_bitwuzla_sort() const { return sort; };
+  const bitwuzla::Sort get_bitwuzla_sort() const { return sort; };
 
  protected:
   // objects from Bitwuzla API
-  const BitwuzlaSort * sort;
+  const bitwuzla::Sort sort;
 
   friend class BzlaSolver;
 };