|
| 1 | +diff --git a/include/bitwuzla/c/bitwuzla.h b/include/bitwuzla/c/bitwuzla.h |
| 2 | +index 2870e868..007f9d58 100644 |
| 3 | +--- a/include/bitwuzla/c/bitwuzla.h |
| 4 | ++++ b/include/bitwuzla/c/bitwuzla.h |
| 5 | +@@ -2007,6 +2007,14 @@ void bitwuzla_substitute_terms(size_t terms_size, |
| 6 | + |
| 7 | + /** @} */ |
| 8 | + |
| 9 | ++void bitwuzla_sort_dec_ref(BitwuzlaSort sort_id); |
| 10 | ++ |
| 11 | ++void bitwuzla_term_dec_ref(BitwuzlaTerm term_id); |
| 12 | ++ |
| 13 | ++uint64_t bitwuzla_bv_value_uint64(BitwuzlaTerm term); |
| 14 | ++ |
| 15 | ++const char *bitwuzla_bv_value_str(BitwuzlaTerm term, uint32_t base); |
| 16 | ++ |
| 17 | + #if __cplusplus |
| 18 | + } |
| 19 | + #endif |
| 20 | +diff --git a/src/api/c/bitwuzla.cpp b/src/api/c/bitwuzla.cpp |
| 21 | +index ece639cc..5c3175f7 100644 |
| 22 | +--- a/src/api/c/bitwuzla.cpp |
| 23 | ++++ b/src/api/c/bitwuzla.cpp |
| 24 | +@@ -2069,3 +2069,56 @@ bitwuzla_term_print_fmt(BitwuzlaTerm term, FILE *file, uint8_t base) |
| 25 | + } |
| 26 | + |
| 27 | + /* -------------------------------------------------------------------------- */ |
| 28 | ++ |
| 29 | ++#include "node/node.h" |
| 30 | ++#include "bv/bitvector.h" |
| 31 | ++ |
| 32 | ++namespace bitwuzla { |
| 33 | ++ template<> |
| 34 | ++ bzla::BitVector |
| 35 | ++ Term::value(uint8_t base) const { |
| 36 | ++ (void) base; |
| 37 | ++ BITWUZLA_CHECK_NOT_NULL(d_node); |
| 38 | ++ BITWUZLA_CHECK_TERM_IS_BV_VALUE(*this); |
| 39 | ++ return d_node->value<bzla::BitVector>(); |
| 40 | ++ } |
| 41 | ++} |
| 42 | ++ |
| 43 | ++void bitwuzla_sort_dec_ref(BitwuzlaSort sort_id) { |
| 44 | ++ Bitwuzla::SortMap &sort_map = Bitwuzla::sort_map(); |
| 45 | ++ const auto it = sort_map.find(sort_id); |
| 46 | ++ it->second.second -= 1; |
| 47 | ++ if (it->second.second == 0) { |
| 48 | ++ it->second.first.reset(); |
| 49 | ++ sort_map.erase(it); |
| 50 | ++ } |
| 51 | ++} |
| 52 | ++ |
| 53 | ++void bitwuzla_term_dec_ref(BitwuzlaTerm term_id) { |
| 54 | ++ Bitwuzla::TermMap &term_map = Bitwuzla::term_map(); |
| 55 | ++ const auto it = term_map.find(term_id); |
| 56 | ++ it->second.second -= 1; |
| 57 | ++ if (it->second.second == 0) { |
| 58 | ++ it->second.first.reset(); |
| 59 | ++ term_map.erase(it); |
| 60 | ++ } |
| 61 | ++} |
| 62 | ++ |
| 63 | ++uint64_t bitwuzla_bv_value_uint64(BitwuzlaTerm term) { |
| 64 | ++ uint64_t res = false; |
| 65 | ++ BITWUZLA_TRY_CATCH_BEGIN; |
| 66 | ++ BITWUZLA_CHECK_TERM_ID(term); |
| 67 | ++ bzla::BitVector bv = import_term(term).value<bzla::BitVector>(); |
| 68 | ++ res = bv.to_uint64(); |
| 69 | ++ BITWUZLA_TRY_CATCH_END; |
| 70 | ++ return res; |
| 71 | ++} |
| 72 | ++ |
| 73 | ++const char *bitwuzla_bv_value_str(BitwuzlaTerm term, uint32_t base) { |
| 74 | ++ static thread_local std::string res; |
| 75 | ++ BITWUZLA_TRY_CATCH_BEGIN; |
| 76 | ++ BITWUZLA_CHECK_TERM_ID(term); |
| 77 | ++ res = import_term(term).value<bzla::BitVector>().str(base); |
| 78 | ++ BITWUZLA_TRY_CATCH_END; |
| 79 | ++ return res.c_str(); |
| 80 | ++} |
| 81 | +diff --git a/src/api/c/checks.h b/src/api/c/checks.h |
| 82 | +index 63a26fff..60be3ed8 100644 |
| 83 | +--- a/src/api/c/checks.h |
| 84 | ++++ b/src/api/c/checks.h |
| 85 | +@@ -47,7 +47,7 @@ class BitwuzlaAbortStream |
| 86 | + { |
| 87 | + stream() << msg_prefix << " "; |
| 88 | + } |
| 89 | +- ~BitwuzlaAbortStream() |
| 90 | ++ ~BitwuzlaAbortStream() noexcept(false) |
| 91 | + { |
| 92 | + flush(); |
| 93 | + bitwuzla_abort(d_stream.str().c_str()); |
| 94 | +diff --git a/src/lib/meson.build b/src/lib/meson.build |
| 95 | +index 7380e24c..38fcb022 100644 |
| 96 | +--- a/src/lib/meson.build |
| 97 | ++++ b/src/lib/meson.build |
| 98 | +@@ -32,19 +32,19 @@ rng_lib = static_library('bzlarng', |
| 99 | + dependencies: gmp_dep) |
| 100 | + |
| 101 | + # Bitwuzla bit-vector, bit-blast and local search libraries |
| 102 | +-bitvector_lib = library('bitwuzlabv', |
| 103 | ++bitvector_lib = static_library('bitwuzlabv', |
| 104 | + sources: bv_sources, |
| 105 | + link_whole: rng_lib, |
| 106 | + dependencies: gmp_dep, |
| 107 | + install_rpath: install_rpath, |
| 108 | + install: true) |
| 109 | +-bitblast_lib = library('bitwuzlabb', |
| 110 | ++bitblast_lib = static_library('bitwuzlabb', |
| 111 | + sources: bb_sources, |
| 112 | + link_with: bitvector_lib, |
| 113 | + dependencies: gmp_dep, |
| 114 | + install_rpath: install_rpath, |
| 115 | + install: true) |
| 116 | +-local_search_lib = library('bitwuzlals', |
| 117 | ++local_search_lib = static_library('bitwuzlals', |
| 118 | + sources: ls_sources, |
| 119 | + link_with: [bitvector_lib], |
| 120 | + link_whole: rng_lib, |
| 121 | +diff --git a/src/meson.build b/src/meson.build |
| 122 | +index ddabc8e8..2260419b 100644 |
| 123 | +--- a/src/meson.build |
| 124 | ++++ b/src/meson.build |
| 125 | +@@ -9,7 +9,7 @@ cpp_compiler = meson.get_compiler('cpp') |
| 126 | + gmp_dep = dependency('gmp', |
| 127 | + version: '>=6.1', |
| 128 | + required: true, |
| 129 | +- static: build_static) |
| 130 | ++ static: true) |
| 131 | + |
| 132 | + |
| 133 | + # Subproject dependencies |
| 134 | +@@ -195,15 +195,23 @@ endif |
| 135 | + # Public header include directory |
| 136 | + bitwuzla_inc = include_directories('../include', 'lib') |
| 137 | + |
| 138 | ++ |
| 139 | ++link_args = [] |
| 140 | ++if host_machine.system() == 'windows' |
| 141 | ++ link_args += ['-static-libstdc++', '-static-libgcc', '-Wl,-Bstatic', '-lstdc++', '-lpthread', '-Wl,-Bdynamic'] |
| 142 | ++endif |
| 143 | ++ |
| 144 | + bitwuzla_lib = library('bitwuzla', |
| 145 | + sources, |
| 146 | + include_directories: bitwuzla_inc, |
| 147 | + link_with: support_libs, |
| 148 | + dependencies: dependencies, |
| 149 | +- soversion: bitwuzla_lib_soversion, |
| 150 | ++ #soversion: bitwuzla_lib_soversion, |
| 151 | + install_rpath: install_rpath, |
| 152 | + install: true, |
| 153 | +- cpp_args: cpp_args) |
| 154 | ++ cpp_args: cpp_args, |
| 155 | ++ link_args: link_args |
| 156 | ++ ) |
| 157 | + |
| 158 | + # Create library dependency |
| 159 | + bitwuzla_dep = declare_dependency(include_directories: bitwuzla_inc, |
0 commit comments