Crate sylvan_sys 

This crate provides unsafe Rust bindings for the parallel multi-terminal binary decision diagram library Sylvan. At the moment, the bindings are based on version 1.6.1 available on Github. The crate compiles on Linux and MacOS, and if you can build sylvan with Visual Studio, it should work on Windows as well (the problem is mostly correctly linking the gmp library).

Keep in mind that you will need cmake and gmp (arbitrary precision numbers) to build Sylvan. Hopefully gmp will be soon optional, but for now it is necessary.

Since a lot of Sylvan’s functionality is defined using preprocessor macros, there is a small wrapper library (./wrapper/src) which exports each macro as a function (this can incur a small performance penalty which should be mostly mitigated by enabling link time optimizations). The wrapper also prefixes each function/macro with Sylvan_ so that they are clearly marked as part of Sylvan API. For documentation, see the original source code and tutorial.

Completeness: Most of the API should be fully reproduced here (including stuff like functions with callbacks). Some minor aspects (like the sylvan_stats struct or more advanced lace functionality) are missing, but if you need them, you can create an issues, and they can be added later.

Correctness: Unfortunately, Sylvan cannot be directly processed using bindgen, so the API was reproduced using a semi-automated method with a manual validation step (bunch of regexes that a human makes sure didn’t break anything ;)). As such, it is possible that there are some minor problems that need to be sorted out. Please file an issue if you see any unexpected behaviour or segfaults.

Modules

bdd

Wraps the sylvan_bdd.h declarations.

common

Wraps the sylvan_common.h declarations.

lace

Wrapper for the essential parts of the lace.h interface.

ldd

Wraps the sylvan_ldd.h declarations.

mt

Wraps the sylvan_mt.h declarations.

mtbdd

Wraps the sylvan_mtbdd.h declarations.

stats

Wraps the sylvan_stats.h declarations.

Constants

MTBDD_COMPLEMENT

MTBDD_FALSE

MTBDD_INVALID

MTBDD_TRUE

SYLVAN_COMPLEMENT

SYLVAN_FALSE

SYLVAN_INVALID

SYLVAN_TRUE

Type Aliases

BDD

BDDMAP

BDDSET

BDDVAR

MDD

MTBDD

MTBDDMAP