sylvan_sys/
ldd.rs

1use crate::lace::{Task, WorkerP};
2use crate::MDD;
3use libc::{c_char, c_double, c_int, c_long, c_void, size_t, FILE};
4
5pub type LDDMC_ENUM_CB = extern "C" fn(*mut WorkerP, *mut Task, *mut u32, size_t, *mut c_void);
6pub type LDDMC_COLLECT_CB =
7    extern "C" fn(*mut WorkerP, *mut Task, *mut u32, size_t, *mut c_void) -> MDD;
8pub type LDDMC_VISIT_PRE_CB = extern "C" fn(*mut WorkerP, *mut Task, MDD, *mut c_void) -> c_int;
9pub type LDDMC_VISIT_POST_CB = extern "C" fn(*mut WorkerP, *mut Task, MDD, *mut c_void);
10pub type LDDMC_VISIT_INIT_CONTEXT_CB =
11    extern "C" fn(*mut WorkerP, *mut Task, *mut c_void, *mut c_void, c_int);
12pub type LDDMC_COMPOSE_CB = extern "C" fn(*mut WorkerP, *mut Task, MDD, *mut c_void) -> MDD;
13
14#[repr(C)]
15pub struct LDDMCCallbacks {
16    pub pre: LDDMC_VISIT_PRE_CB,
17    pub post: LDDMC_VISIT_POST_CB,
18    pub context: LDDMC_VISIT_INIT_CONTEXT_CB,
19}
20
21extern "C" {
22    pub fn Sylvan_init_ldd() -> c_void;
23    pub fn Sylvan_lddmc_makenode(value: u32, ifeq: MDD, ifneq: MDD) -> MDD;
24    pub fn Sylvan_lddmc_extendnode(mdd: MDD, value: u32, ifeq: MDD) -> MDD;
25    pub fn Sylvan_lddmc_getvalue(mdd: MDD) -> u32;
26    pub fn Sylvan_lddmc_getdown(mdd: MDD) -> MDD;
27    pub fn Sylvan_lddmc_getright(mdd: MDD) -> MDD;
28    pub fn Sylvan_lddmc_follow(mdd: MDD, value: u32) -> MDD;
29    pub fn Sylvan_lddmc_make_copynode(ifeq: MDD, ifneq: MDD) -> MDD;
30    pub fn Sylvan_lddmc_iscopy(mdd: MDD) -> c_int;
31    pub fn Sylvan_lddmc_followcopy(mdd: MDD) -> MDD;
32    pub fn Sylvan_lddmc_protect(ptr: *mut MDD) -> c_void;
33    pub fn Sylvan_lddmc_unprotect(ptr: *mut MDD) -> c_void;
34    pub fn Sylvan_lddmc_count_protected() -> size_t;
35    pub fn Sylvan_lddmc_ref(dd: MDD) -> MDD;
36    pub fn Sylvan_lddmc_deref(dd: MDD) -> c_void;
37    pub fn Sylvan_lddmc_count_refs() -> size_t;
38    pub fn Sylvan_lddmc_gc_mark_rec(mdd: MDD) -> c_void;
39    pub fn Sylvan_lddmc_union(a: MDD, b: MDD) -> MDD;
40    pub fn Sylvan_lddmc_minus(a: MDD, b: MDD) -> MDD;
41    pub fn Sylvan_lddmc_zip(a: MDD, b: MDD, res: *mut MDD) -> MDD;
42    pub fn Sylvan_lddmc_intersect(a: MDD, b: MDD) -> MDD;
43    pub fn Sylvan_lddmc_match(a: MDD, b: MDD, proj: MDD) -> MDD;
44    pub fn Sylvan_lddmc_union_cube(a: MDD, values: *mut u32, count: size_t) -> MDD;
45    pub fn Sylvan_lddmc_member_cube(a: MDD, values: *mut u32, count: size_t) -> c_int;
46    pub fn Sylvan_lddmc_cube(values: *mut u32, count: size_t) -> MDD;
47    pub fn Sylvan_lddmc_union_cube_copy(
48        a: MDD,
49        values: *mut u32,
50        copy: *mut c_int,
51        count: size_t,
52    ) -> MDD;
53    pub fn Sylvan_lddmc_member_cube_copy(
54        a: MDD,
55        values: *mut u32,
56        copy: *mut c_int,
57        count: size_t,
58    ) -> c_int;
59    pub fn Sylvan_lddmc_cube_copy(values: *mut u32, copy: *mut c_int, count: size_t) -> MDD;
60    pub fn Sylvan_lddmc_relprod(a: MDD, b: MDD, proj: MDD) -> MDD;
61    pub fn Sylvan_lddmc_relprod_union(a: MDD, b: MDD, meta: MDD, un: MDD) -> MDD;
62    pub fn Sylvan_lddmc_relprev(a: MDD, rel: MDD, proj: MDD, uni: MDD) -> MDD;
63    pub fn Sylvan_lddmc_project(mdd: MDD, proj: MDD) -> MDD;
64    pub fn Sylvan_lddmc_project_minus(mdd: MDD, proj: MDD, avoid: MDD) -> MDD;
65    pub fn Sylvan_lddmc_join(a: MDD, b: MDD, a_proj: MDD, b_proj: MDD) -> MDD;
66    pub fn Sylvan_lddmc_printdot(mdd: MDD) -> c_void;
67    pub fn Sylvan_lddmc_fprintdot(out: *mut FILE, mdd: MDD) -> c_void;
68    pub fn Sylvan_lddmc_fprint(out: *mut FILE, mdd: MDD) -> c_void;
69    pub fn Sylvan_lddmc_print(mdd: MDD) -> c_void;
70    pub fn Sylvan_lddmc_printsha(mdd: MDD) -> c_void;
71    pub fn Sylvan_lddmc_fprintsha(out: *mut FILE, mdd: MDD) -> c_void;
72    pub fn Sylvan_lddmc_getsha(mdd: MDD, target: *mut c_char) -> c_void;
73    pub fn Sylvan_lddmc_satcount_cached(mdd: MDD) -> c_double;
74    /*
75       Due to missing support in Rust, we can't really safely work with C-style f128 values.
76       pub fn Sylvan_lddmc_satcount(mdd: MDD) -> f128;
77    */
78    pub fn Sylvan_lddmc_sat_all_par(mdd: MDD, cb: LDDMC_ENUM_CB, context: *mut c_void) -> c_void;
79    pub fn Sylvan_lddmc_sat_all_nopar(mdd: MDD, cb: LDDMC_ENUM_CB, context: *mut c_void) -> c_void;
80    pub fn Sylvan_lddmc_collect(md: MDD, cb: LDDMC_COLLECT_CB, context: *mut c_void) -> MDD;
81    pub fn Sylvan_lddmc_match_sat_par(
82        mdd: MDD,
83        to_match: MDD,
84        proj: MDD,
85        cb: LDDMC_ENUM_CB,
86        context: *mut c_void,
87    ) -> c_void;
88    pub fn Sylvan_lddmc_sat_one(mdd: MDD, values: *mut u32, count: size_t) -> c_int;
89    pub fn Sylvan_lddmc_sat_one_mdd(mdd: MDD) -> MDD;
90    pub fn Sylvan_lddmc_pick_cube(mdd: MDD) -> MDD;
91    pub fn Sylvan_lddmc_visit_par(
92        mdd: MDD,
93        cbs: *mut LDDMCCallbacks,
94        ctx_size: size_t,
95        context: *mut c_void,
96    ) -> c_void;
97    pub fn Sylvan_lddmc_visit_seq(
98        mdd: MDD,
99        cbs: *mut LDDMCCallbacks,
100        ctx_size: size_t,
101        context: *mut c_void,
102    ) -> c_void;
103    pub fn Sylvan_lddmc_nodecount(mdd: MDD) -> size_t;
104    pub fn Sylvan_lddmc_nodecount_levels(mdd: MDD, variables: *mut size_t) -> c_void;
105    pub fn Sylvan_lddmc_compose(
106        mdd: MDD,
107        cb: LDDMC_COMPOSE_CB,
108        context: *mut c_void,
109        depth: c_int,
110    ) -> MDD;
111    pub fn Sylvan_lddmc_serialize_add(mdd: MDD) -> size_t;
112    pub fn Sylvan_lddmc_serialize_get(mdd: MDD) -> size_t;
113    pub fn Sylvan_lddmc_serialize_get_reversed(value: size_t) -> MDD;
114    pub fn Sylvan_lddmc_serialize_reset() -> c_void;
115    pub fn Sylvan_lddmc_serialize_totext(out: *mut FILE) -> c_void;
116    pub fn Sylvan_lddmc_serialize_tofile(out: *mut FILE) -> c_void;
117    pub fn Sylvan_lddmc_serialize_fromfile(input: *mut FILE) -> c_void;
118    pub fn Sylvan_lddmc_refs_pushptr(ptr: *const MDD) -> c_void;
119    pub fn Sylvan_lddmc_refs_popptr(amount: size_t) -> c_void;
120    pub fn Sylvan_lddmc_refs_push(dd: MDD) -> MDD;
121    pub fn Sylvan_lddmc_refs_pop(amount: c_long) -> c_void;
122    pub fn Sylvan_lddmc_refs_spawn(t: *mut Task) -> c_void;
123    pub fn Sylvan_lddmc_refs_sync(dd: MDD) -> MDD;
124}
sylvan_sys/ldd.rs

sylvan_sys/
ldd.rs
