-
Notifications
You must be signed in to change notification settings - Fork 1
/
boolector.patch
60 lines (56 loc) · 1.6 KB
/
boolector.patch
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
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()
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()
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,11 @@
#define __STDC_FORMAT_MACROS
#endif
+#if defined(__wasm)
+#include <typeinfo>
+#include <exception>
+#endif
+
#include "minisat/simp/SimpSolver.h"
#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