sylvan_sys/
bdd.rs

1use crate::lace::{Task, WorkerP};
2use crate::{BDD, BDDMAP, BDDSET, BDDVAR, MTBDD};
3use libc::{c_double, c_int, c_void, size_t, FILE};
4
5pub type ENUM_CB = extern "C" fn(*mut WorkerP, *mut Task, *mut c_void, *mut BDDVAR, *mut u8, c_int);
6pub type COLLECT_CB = extern "C" fn(*mut WorkerP, *mut Task, *mut c_void, *mut u8) -> BDD;
7
8extern "C" {
9
10    pub fn Sylvan_isconst(bdd: MTBDD) -> c_int;
11    pub fn Sylvan_isnode(bdd: MTBDD) -> c_int;
12    pub fn Sylvan_set_granularity(granularity: c_int) -> c_void;
13    pub fn Sylvan_get_granularity() -> c_int;
14    pub fn Sylvan_not(a: BDD) -> BDD;
15    pub fn Sylvan_ite(a: BDD, b: BDD, c: BDD) -> BDD;
16    pub fn Sylvan_and(a: BDD, b: BDD) -> BDD;
17    pub fn Sylvan_xor(a: BDD, b: BDD) -> BDD;
18    pub fn Sylvan_equiv(a: BDD, b: BDD) -> BDD;
19    pub fn Sylvan_or(a: BDD, b: BDD) -> BDD;
20    pub fn Sylvan_nand(a: BDD, b: BDD) -> BDD;
21    pub fn Sylvan_nor(a: BDD, b: BDD) -> BDD;
22    pub fn Sylvan_imp(a: BDD, b: BDD) -> BDD;
23    pub fn Sylvan_invimp(a: BDD, b: BDD) -> BDD;
24    pub fn Sylvan_biimp(a: BDD, b: BDD) -> BDD;
25    pub fn Sylvan_diff(a: BDD, b: BDD) -> BDD;
26    pub fn Sylvan_less(a: BDD, b: BDD) -> BDD;
27    pub fn Sylvan_nithvar(var: u32) -> BDD;
28    pub fn Sylvan_exists(a: BDD, vars: BDD) -> BDD;
29    pub fn Sylvan_forall(a: BDD, vars: BDD) -> BDD;
30    pub fn Sylvan_project(a: BDD, vars: BDD) -> BDD;
31    pub fn Sylvan_and_exists(a: BDD, b: BDD, vars: BDDSET) -> BDD;
32    pub fn Sylvan_and_project(a: BDD, b: BDD, vars: BDDSET) -> BDD;
33    pub fn Sylvan_relprev(a: BDD, b: BDD, vars: BDDSET) -> BDD;
34    pub fn Sylvan_relnext(a: BDD, b: BDD, vars: BDDSET) -> BDD;
35    pub fn Sylvan_closure(a: BDD) -> BDD;
36    pub fn Sylvan_constrain(f: BDD, c: BDD) -> BDD;
37    pub fn Sylvan_restrict(f: BDD, c: BDD) -> BDD;
38    pub fn Sylvan_compose(f: BDD, m: BDDMAP) -> BDD;
39    pub fn Sylvan_satcount(bdd: BDD, variables: BDDSET) -> c_double;
40    pub fn Sylvan_cube(variables: BDDSET, cube: *mut u8) -> BDD;
41    pub fn Sylvan_union_cube(bdd: BDD, variables: BDDSET, cube: *mut u8) -> BDD;
42    pub fn Sylvan_sat_one(bdd: BDD, variables: BDDSET, str: *mut u8) -> c_int;
43    pub fn Sylvan_sat_one_bdd(bdd: BDD) -> BDD;
44    pub fn Sylvan_pick_cube(bdd: BDD) -> BDD;
45    pub fn Sylvan_sat_single(bdd: BDD, vars: BDDSET) -> BDD;
46    pub fn Sylvan_pick_single_cube(bdd: BDD, vars: BDDSET) -> BDD;
47    pub fn Sylvan_enum(bdd: BDD, vars: BDDSET, cb: ENUM_CB, context: *mut c_void) -> c_void;
48    pub fn Sylvan_enum_par(bdd: BDD, vars: BDDSET, cb: ENUM_CB, context: *mut c_void) -> c_void;
49    pub fn Sylvan_collect(bdd: BDD, vars: BDDSET, cb: COLLECT_CB, context: *mut c_void) -> BDD;
50    pub fn Sylvan_pathcount(bdd: BDD) -> c_double;
51    pub fn Sylvan_serialize_add(bdd: BDD) -> size_t;
52    pub fn Sylvan_serialize_get(bdd: BDD) -> size_t;
53    pub fn Sylvan_serialize_get_reversed(value: size_t) -> BDD;
54    pub fn Sylvan_serialize_reset() -> c_void;
55    pub fn Sylvan_serialize_totext(out: *mut FILE) -> c_void;
56    pub fn Sylvan_serialize_tofile(out: *mut FILE) -> c_void;
57    pub fn Sylvan_serialize_fromfile(input: *mut FILE) -> c_void;
58    pub fn Sylvan_fprint(f: *mut FILE, bdd: BDD) -> c_void;
59    pub fn Sylvan_print(bdd: BDD) -> c_void;
60
61}
sylvan_sys/bdd.rs

sylvan_sys/
bdd.rs
