This PR integrates the Biodivine/LibBDD library into BDD benchmark. Biodivine/LibBDD itself is written in Rust and does not come with a C FFI, hence I hacked a FFI on my own.
Some remarks:
I tested most of the benchmarks and they seem to work.
lib-bdd-ffi uses FetchContent in CMake and builds a library using cargo. Therefore, an internet connection is needed for the first time invoking cmake and make.
I did not monitor memory usage yet to see if the maximum node count is set in a meaningful way. AFAIK, LibBDD also does not provide any way to set the maximum apply cache size. They use a new HashMap for every apply operation, without any bounds on the size. lib-bdd-ffi checks that the cumulated node count of all BDDs belonging to a manager does not exceed some maximum value. This check happens after each apply operation only, i.e., the library might allocate too much memory in between.
I was a bit unsure whether to use lib_bdd, libbdd, or lib-bdd (the latter would only be applicable in executable names). In the end, I chose lib_bdd for the C++ interface to lib-bdd-ffi, but libbdd for all BDD Benchmark related things (e.g., libbdd_bdd_adapter, and executable names).
This PR integrates the Biodivine/LibBDD library into BDD benchmark. Biodivine/LibBDD itself is written in Rust and does not come with a C FFI, hence I hacked a FFI on my own.
Some remarks:
lib-bdd-ffi
usesFetchContent
in CMake and builds a library usingcargo
. Therefore, an internet connection is needed for the first time invokingcmake
andmake
.HashMap
for every apply operation, without any bounds on the size.lib-bdd-ffi
checks that the cumulated node count of all BDDs belonging to a manager does not exceed some maximum value. This check happens after each apply operation only, i.e., the library might allocate too much memory in between.lib_bdd
,libbdd
, orlib-bdd
(the latter would only be applicable in executable names). In the end, I choselib_bdd
for the C++ interface tolib-bdd-ffi
, butlibbdd
for all BDD Benchmark related things (e.g.,libbdd_bdd_adapter
, and executable names).