sylvan_sys/
lib.rs

1//! This crate provides unsafe Rust bindings for the parallel multi-terminal binary decision
2//! diagram library Sylvan. At the moment, the bindings are based on version `1.6.1` available
3//! [on Github](https://github.com/trolando/sylvan). The crate compiles on Linux and MacOS, and
4//! if you can build `sylvan` with Visual Studio, it should work on Windows as well (the problem
5//! is mostly correctly linking the `gmp` library).
6//!
7//! > Keep in mind that you will need `cmake` and `gmp` (arbitrary precision numbers) to build
8//! Sylvan. Hopefully `gmp` will be soon optional, but for now it is necessary.
9//!
10//! Since a lot of Sylvan's functionality is defined using preprocessor macros, there is a small
11//! wrapper library (`./wrapper/src`) which exports each macro as a function (this can incur
12//! a small performance penalty which should be mostly mitigated by enabling link time
13//! optimizations). The wrapper also prefixes each function/macro with `Sylvan_` so that they are
14//! clearly marked as part of Sylvan API. For documentation, see the original source
15//! code and [tutorial](https://trolando.github.io/sylvan/).
16//!
17//! **Completeness:** Most of the API should be fully reproduced here (including stuff like
18//! functions with callbacks). Some minor aspects (like the `sylvan_stats` struct or more advanced
19//! lace functionality) are missing, but if you need them, you can create an issues, and they can
20//! be added later.
21//!
22//! **Correctness:** Unfortunately, Sylvan cannot be directly processed using `bindgen`, so the API
23//! was reproduced using a semi-automated method with a manual validation step (bunch of regexes
24//! that a human makes sure didn't break anything ;)). As such, it is possible that there are some
25//! minor problems that need to be sorted out. Please file an issue if you see any unexpected
26//! behaviour or segfaults.
27
28// Allow non-idiomatic names in the whole crate.
29#![allow(non_camel_case_types)]
30#![allow(non_snake_case)]
31extern crate libc;
32
33/// Wraps the `sylvan_bdd.h` declarations.
34pub mod bdd;
35/// Wraps the `sylvan_common.h` declarations.
36pub mod common;
37/// Wrapper for the essential parts of the `lace.h` interface.
38pub mod lace;
39/// Wraps the `sylvan_ldd.h` declarations.
40pub mod ldd;
41/// Wraps the `sylvan_mt.h` declarations.
42pub mod mt;
43/// Wraps the `sylvan_mtbdd.h` declarations.
44pub mod mtbdd;
45/// Wraps the `sylvan_stats.h` declarations.
46pub mod stats;
47
48#[cfg(test)]
49mod test;
50
51pub type MDD = u64;
52pub type MTBDD = u64;
53pub type BDDVAR = u32;
54
55pub type MTBDDMAP = MTBDD;
56pub type BDD = MTBDD;
57pub type BDDMAP = MTBDD;
58pub type BDDSET = MTBDD;
59
60pub const MTBDD_COMPLEMENT: MTBDD = 0x8000000000000000;
61pub const MTBDD_FALSE: MTBDD = 0;
62pub const MTBDD_TRUE: MTBDD = 0x8000000000000000;
63pub const MTBDD_INVALID: MTBDD = 0xffffffffffffffff;
64
65pub const SYLVAN_COMPLEMENT: MTBDD = MTBDD_COMPLEMENT;
66pub const SYLVAN_FALSE: MTBDD = MTBDD_FALSE;
67pub const SYLVAN_TRUE: MTBDD = MTBDD_TRUE;
68pub const SYLVAN_INVALID: MTBDD = MTBDD_INVALID;
sylvan_sys/lib.rs

sylvan_sys/
lib.rs
