new bitwuzla version

emsec · Jul 15, 2023 · 9c709e3 · 9c709e3
1 parent ac9536d
commit 9c709e3
Show file tree

Hide file tree

Showing 3 changed files with 43 additions and 26 deletions.
diff --git a/cmake/detect_dependencies.cmake b/cmake/detect_dependencies.cmake
@@ -27,11 +27,22 @@ find_package(Sanitizers REQUIRED)
 # ###############################
 # ####   Bitwuzla
 # ###############################
-find_package(Bitwuzla)
+pkg_check_modules(BITWUZLA REQUIRED bitwuzla)
+
+# find_package(Bitwuzla)
+
+if(BITWUZLA_FOUND)
+    message(STATUS "Found BITWUZLA")
+    message(STATUS "    BITWUZLA_LIBRARIES: ${BITWUZLA_LIBRARIES}")
+    message(STATUS "    BITWUZLA_LINK_LIBRARIES: ${BITWUZLA_LINK_LIBRARIES}")
+    message(STATUS "    BITWUZLA_INCLUDE_DIRS: ${BITWUZLA_INCLUDE_DIRS}")
+else()
+    set(BITWUZLA_LIBRARY "")
+    set(BITWUZLA_INCLUDE_DIRS "")
+
+    message(STATUS "Bitwuzla not found, but this is optional...")
+endif(BITWUZLA_FOUND)
 
-if(Bitwuzla_FOUND)
-    set(BITWUZLA_LIBRARY Bitwuzla::bitwuzla)
-endif()
 
 # ###############################
 # ####   OpenMP

diff --git a/src/netlist/CMakeLists.txt b/src/netlist/CMakeLists.txt
@@ -5,9 +5,9 @@ add_library(netlist SHARED ${NETLIST_LIB_INCLUDE} ${NETLIST_LIB_SOURCE} ${CMAKE_
 set_target_properties(netlist PROPERTIES OUTPUT_NAME "hal_netlist")
 add_library(hal::netlist ALIAS netlist)
 
-if(Bitwuzla_FOUND)
+if(BITWUZLA_FOUND)
     add_compile_definitions(BITWUZLA_LIBRARY)
-    message(STATUS "found bitwuzla, adding define for solver query to bitwuzla library")
+    message(STATUS "found bitwuzla, adding define for solver query to bitwuzla library")    
 endif()
 
 
@@ -18,10 +18,11 @@ target_include_directories(netlist
                            $<INSTALL_INTERFACE:${CMAKE_INSTALL_INCLUDEDIR}>
                            ${Z3_INCLUDE_DIRS}
                            ${RAPIDJSON_INCLUDEDIR}
+                           ${BITWUZLA_INCLUDE_DIRS}
                            )
 
 target_compile_options(netlist
-                       PUBLIC ${COMPILE_OPTIONS_PUBLIC}
+                       PUBLIC ${COMPILE_OPTIONS_PUBLIC} ${BITWUZLA_CFLAGS_OTHER}
                        PRIVATE ${COMPILE_OPTIONS_PRIVATE}
                        INTERFACE ${COMPILE_OPTIONS_INTERFACE})
 set_target_properties(PROPERTIES DEFINE_SYMBOL BUILDING_CORE)
@@ -37,7 +38,7 @@ target_link_libraries(netlist
                         RapidJSON::RapidJSON
                         ${Z3_LIBRARIES}
                         ${ABC_LIBRARY}
-                        ${BITWUZLA_LIBRARY}
+                        ${BITWUZLA_LIBRARIES}
                       )
 
 install(TARGETS netlist

diff --git a/src/netlist/boolean_function/solver.cpp b/src/netlist/boolean_function/solver.cpp
@@ -8,7 +8,8 @@
 #include <set>
 
 #ifdef BITWUZLA_LIBRARY
-#include "bitwuzla/bitwuzla.h"
+#include "bitwuzla/cpp/bitwuzla.h"
+#include "bitwuzla/cpp/parser.h"
 #endif
 
 namespace hal
@@ -233,38 +234,42 @@ namespace hal
             Result<std::tuple<bool, std::string>> query_library(std::string& input, const QueryConfig& config)
             {
 #ifdef BITWUZLA_LIBRARY
-                auto bzla = bitwuzla_new();
 
+                // First, create a Bitwuzla options instance.
+                bitwuzla::Options options;
+                // We will parse example file `smt2/quickstart.smt2`.
+                // Create parser instance.
+                // We expect no error to occur.
                 const char* smt2_char_string = input.c_str();
 
-                char* out;
-                size_t out_len = {};
-
-                auto in_stream  = fmemopen((void*)smt2_char_string, strlen(smt2_char_string), "r");
-                auto out_stream = open_memstream(&out, &out_len);
-
-                BitwuzlaResult _r;
-                char* error;
+                auto in_stream = fmemopen((void*)smt2_char_string, strlen(smt2_char_string), "r");
 
                 if (config.generate_model)
                 {
-                    bitwuzla_set_option(bzla, BITWUZLA_OPT_PRODUCE_MODELS, 1);
+                    options.set(bitwuzla::Option::PRODUCE_MODELS, true);
                 }
 
-                auto res = bitwuzla_parse_format(bzla, "smt2", in_stream, "VIRTUAL FILE", out_stream, &error, &_r);
-                fflush(out_stream);
+                bitwuzla::parser::Parser parser(options, "VIRTUAL_FILE", in_stream, "smt2");
+                // Now parse the input file.
+                std::string err_msg = parser.parse(true);
 
-                if (error != nullptr)
+                if (!err_msg.empty())
                 {
-                    return ERR("failed to solve provided smt2 solver with bitwuzla: " + std::string(error));
+                    return ERR("failed to parse input file: " + err_msg);
                 }
 
                 fclose(in_stream);
-                fclose(out_stream);
 
-                bitwuzla_delete(bzla);
+                auto bitwuzla           = parser.bitwuzla();
+                bitwuzla::Result result = bitwuzla->check_sat();
+
+                std::stringbuf result_string;
+                std::ostream output_stream(&result_string);
+
+                bitwuzla->print_formula(output_stream, "smt2");
+
+                std ::string output(result_string.str());
 
-                std::string output(out);
 
                 return OK({false, output});
 #else