MiniSAT Backend Support

.gitignore

@@ -1,7 +1,5 @@
 /wasi-sdk-*
 *.wasm
-/picosat-*
 /*-build
 /*-prefix
 /Toolchain-WASI.cmake
-!/picosat-version

.gitmodules

@@ -4,3 +4,6 @@
 [submodule "btor2tools"]
 	path = btor2tools-src
 	url = https://github.com/Boolector/btor2tools.git
+[submodule "minisat-src"]
+	path = minisat-src
+	url = https://github.com/agurfinkel/minisat

boolector.patch

@@ -1,89 +1,59 @@
-diff --git a/src/boolector.c b/src/boolector.c
-index 2df5bbe6..06c75490 100644
---- a/src/boolector.c
-+++ b/src/boolector.c
-@@ -293,8 +293,10 @@ boolector_delete (Btor *btor)
-   BTOR_TRAPI ("");
-   if (btor->close_apitrace == 1)
-     fclose (btor->apitrace);
-+#ifndef __wasm
-   else if (btor->close_apitrace == 2)
-     pclose (btor->apitrace);
-+#endif
- #ifndef NDEBUG
-   if (btor->clone) boolector_delete (btor->clone);
- #endif
-diff --git a/src/btormain.c b/src/btormain.c
-index 078bdc30..fde14230 100644
---- a/src/btormain.c
-+++ b/src/btormain.c
-@@ -21,7 +21,9 @@
-
- #include <assert.h>
- #include <limits.h>
-+#ifndef __wasm
- #include <signal.h>
-+#endif
- #include <stdarg.h>
- #include <stdio.h>
- #include <stdlib.h>
-@@ -1061,7 +1063,9 @@ boolector_main (int32_t argc, char **argv)
-       else if (btor_util_file_has_suffix (g_app->infile_name, ".zip"))
-         sprintf (cmd, "unzip -p %s", g_app->infile_name);
-
-+#ifndef __wasm
-       if ((g_app->infile = popen (cmd, "r"))) g_app->close_infile = 2;
-+#endif
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index 532c08e3..bd003e6a 100644
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -394,6 +394,8 @@ if(MiniSat_FOUND)
+     message(FATAL_ERROR "MiniSAT headers not found")
+   else()
+     add_definitions("-DBTOR_USE_MINISAT")
++    # Disable gzip dependency for new enough MiniSAT.
++    add_definitions("-DMINISAT_LIBRARY_ONLY")
+   endif()
+ endif()
 
-       BTOR_DELETEN (g_app->mm, cmd, len + 40);
-     }
-@@ -1595,8 +1599,10 @@ DONE:
+diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
+index b51e10a1..09b696d2 100644
+--- a/src/CMakeLists.txt
++++ b/src/CMakeLists.txt
+@@ -133,6 +133,9 @@ endif()
+ if(MiniSat_FOUND)
+   target_include_directories(boolector PRIVATE ${MiniSat_INCLUDE_DIR})
+   target_link_libraries(boolector ${MiniSat_LIBRARIES})
++  if(WASI)
++    target_link_libraries(boolector wasi-emulated-process-clocks wasi-emulated-signal)
++  endif()
+ endif()
 
-   if (g_app->close_infile == 1)
-     fclose (g_app->infile);
-+#ifndef __wasm
-   else if (g_app->close_infile == 2)
-     pclose (g_app->infile);
-+#endif
-   if (g_app->close_outfile) fclose (g_app->outfile);
-
-   if (!boolector_get_opt (btor, BTOR_OPT_EXIT_CODES))
-diff --git a/src/btormcmain.c b/src/btormcmain.c
-index e3c5ed3f..be549217 100644
---- a/src/btormcmain.c
-+++ b/src/btormcmain.c
-@@ -818,7 +818,9 @@ main (int32_t argc, char **argv)
-       else if (btor_util_file_has_suffix (infile_name, ".zip"))
-         sprintf (cmd, "unzip -p %s", infile_name);
+ install(TARGETS boolector
+diff --git a/src/sat/btorminisat.cc b/src/sat/btorminisat.cc
+index e37ee585..bc08d612 100644
+--- a/src/sat/btorminisat.cc
++++ b/src/sat/btorminisat.cc
+@@ -16,6 +16,10 @@
+ #define __STDC_FORMAT_MACROS
+ #endif
 
-+#ifndef __wasm
-       if ((infile = popen (cmd, "r"))) close_infile = 2;
++#if defined(__wasm)
++#include <typeinfo>
 +#endif
++
+ #include "minisat/simp/SimpSolver.h"
 
-       BTOR_DELETEN (mm, cmd, len + 40);
-     }
-@@ -956,8 +958,10 @@ main (int32_t argc, char **argv)
- DONE:
-   if (close_infile == 1)
-     fclose (infile);
-+#ifndef __wasm
-   else if (close_infile == 2)
-     pclose (infile);
-+#endif
-   boolector_mc_delete (mc);
-   while (!BTOR_EMPTY_STACK (opts))
-   {
-diff --git a/src/btortrapi.c b/src/btortrapi.c
-index 64308a4f..12c911a3 100644
---- a/src/btortrapi.c
-+++ b/src/btortrapi.c
-@@ -64,7 +64,9 @@ btor_trapi_open_trace (Btor *btor, const char *name)
-     len += 20;
-     BTOR_NEWN (btor->mm, cmd, len);
-     sprintf (cmd, "gzip -c > %s", name);
-+#ifndef __wasm
-     if ((file = popen (cmd, "w"))) btor->close_apitrace = 2;
+ #include <cassert>
+@@ -257,3 +261,16 @@ btor_sat_enable_minisat (BtorSATMgr* smgr)
+ }
+ };
+ #endif
++
++#if defined(__wasm)
++extern "C" {
++	// FIXME: WASI does not currently support exceptions.
++	void* __cxa_allocate_exception(size_t thrown_size) throw() {
++		return malloc(thrown_size);
++	}
++	bool __cxa_uncaught_exception() throw();
++	void __cxa_throw(void* thrown_exception, struct std::type_info * tinfo, void (*dest)(void*)) {
++		std::terminate();
++	}
++}
 +#endif
-     BTOR_DELETEN (btor->mm, cmd, len);
-   }
-   else

build.sh

@@ -9,10 +9,6 @@ WASI_SDK_URL=https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-
 if ! [ -d ${WASI_SDK} ]; then curl -L ${WASI_SDK_URL} | tar xzf -; fi
 WASI_SDK_PATH=$(pwd)/${WASI_SDK}
 
-PICOSAT_DIR=$(cat picosat-version)
-PICOSAT_URL=http://fmv.jku.at/picosat/${PICOSAT_DIR}.tar.gz
-if ! [ -d ${PICOSAT_DIR} ]; then curl -L ${PICOSAT_URL} | tar xzf -; fi
-
 WASI_TARGET="wasm32-wasi"
 WASI_SYSROOT="--sysroot ${WASI_SDK_PATH}/share/wasi-sysroot"
 WASI_CFLAGS="-flto"
@@ -49,17 +45,14 @@ set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY)
 set(CMAKE_FIND_ROOT_PATH_MODE_PACKAGE ONLY)
 END
 
-mkdir -p $(pwd)/picosat-prefix
-(cd $PICOSAT_DIR && CC="${CCACHE:-ccache} ${WASI_SDK_PATH}/bin/clang" \
-    CFLAGS="-DNGETRUSAGE -DNALLSIGNALS -DNDEBUG -O3" \
-    ./configure.sh)
-
-make -C $PICOSAT_DIR picosat.o version.o
-${WASI_SDK_PATH}/bin/ar rc $PICOSAT_DIR/libpicosat.a $PICOSAT_DIR/picosat.o $PICOSAT_DIR/version.o
-${WASI_SDK_PATH}/bin/ranlib $PICOSAT_DIR/libpicosat.a
-cp $PICOSAT_DIR/libpicosat.a $PICOSAT_DIR/picosat.h $(pwd)/picosat-prefix
+(cd minisat-src && git apply < ../minisat.patch || git apply --reverse --check < ../minisat.patch)
+cmake -B minisat-build -S minisat-src \
+  -DCMAKE_TOOLCHAIN_FILE=../Toolchain-WASI.cmake \
+  -DLIBRARY_ONLY=ON \
+  -DCMAKE_BUILD_TYPE="Release" \
+  -DCMAKE_INSTALL_PREFIX=$(pwd)/minisat-prefix
+make -C minisat-build install
 
-(cd btor2tools-src && git apply < ../btor2tools.patch || git apply --reverse --check < ../btor2tools.patch)
 cmake -B btor2tools-build -S btor2tools-src \
   -DCMAKE_TOOLCHAIN_FILE=../Toolchain-WASI.cmake \
   -DBUILD_SHARED_LIBS=OFF \
@@ -70,6 +63,6 @@ make -C btor2tools-build install
 (cd boolector-src && git apply < ../boolector.patch || git apply --reverse --check < ../boolector.patch)
 cmake -B boolector-build -S boolector-src \
     -DCMAKE_TOOLCHAIN_FILE=../Toolchain-WASI.cmake \
-    -DCMAKE_INCLUDE_PATH="$(pwd)/btor2tools-prefix/include;$(pwd)/picosat-prefix" \
-    -DCMAKE_LIBRARY_PATH="$(pwd)/btor2tools-prefix/lib;$(pwd)/picosat-prefix"
-cmake --build boolector-build -t boolector-bin
+    -DCMAKE_INCLUDE_PATH="$(pwd)/btor2tools-prefix/include;$(pwd)/minisat-prefix/include" \
+    -DCMAKE_LIBRARY_PATH="$(pwd)/btor2tools-prefix/lib;$(pwd)/minisat-prefix/lib"
+cmake --build boolector-build -v -t boolector-bin