sylvan_sys/
mtbdd.rs

1use crate::lace::{Task, WorkerP};
2use crate::{MTBDD, MTBDDMAP};
3use libc::{c_char, c_double, c_int, c_long, c_void, size_t, FILE};
4use std::marker::{PhantomData, PhantomPinned};
5
6pub type MTBDD_APPLY_OP = extern "C" fn(*mut WorkerP, *mut Task, *mut MTBDD, *mut MTBDD) -> MTBDD;
7pub type MTBDD_APPLYP_OP =
8    extern "C" fn(*mut WorkerP, *mut Task, *mut MTBDD, *mut MTBDD, size_t) -> MTBDD;
9pub type MTBDD_UAPPLY_OP = extern "C" fn(*mut WorkerP, *mut Task, MTBDD, size_t) -> MTBDD;
10pub type MTBDD_ABSTRACT_OP = extern "C" fn(*mut WorkerP, *mut Task, MTBDD, MTBDD, c_int) -> MTBDD;
11pub type MTBDD_ENUM_CB =
12    extern "C" fn(*mut WorkerP, *mut Task, *mut MTBDDEnumTrace, MTBDD, *mut c_void);
13pub type MTBDD_EVAL_COMPOSE_CB = extern "C" fn(*mut WorkerP, *mut Task, MTBDD) -> MTBDD;
14pub type MTBDD_VISIT_PRE_CB = extern "C" fn(*mut WorkerP, *mut Task, MTBDD, *mut c_void) -> c_int;
15pub type MTBDD_VISIT_POST_CB = extern "C" fn(*mut WorkerP, *mut Task, MTBDD, *mut c_void);
16pub type MTBDD_ENUM_FILTER_CB = extern "C" fn(MTBDD) -> c_int;
17
18#[repr(C)]
19pub struct MTBDDEnumTrace {
20    pub prev: *mut MTBDDEnumTrace,
21    pub var: u32,
22    pub val: c_int,
23}
24
25/// An opaque C struct representing a skip list used during serialisation.
26#[repr(C)]
27pub struct SkipList {
28    _data: [u8; 0],
29    _marker: PhantomData<(*mut u8, PhantomPinned)>,
30}
31
32pub type SkipListPtr = *mut SkipList;
33
34extern "C" {
35    pub fn Sylvan_init_mtbdd() -> c_void;
36    pub fn Sylvan_init_bdd() -> c_void;
37    pub fn Sylvan_mtbdd_makeleaf(leaf_type: u32, value: u64) -> MTBDD;
38    pub fn Sylvan_mtbdd_makenode(var: u32, low: MTBDD, high: MTBDD) -> MTBDD;
39    pub fn Sylvan_makenode(var: u32, low: MTBDD, high: MTBDD) -> MTBDD;
40    pub fn Sylvan_mtbdd_isleaf(mtbdd: MTBDD) -> c_int;
41    pub fn Sylvan_mtbdd_isnode(mtbdd: MTBDD) -> c_int;
42    pub fn Sylvan_mtbdd_gettype(leaf: MTBDD) -> u32;
43    pub fn Sylvan_mtbdd_getvalue(leaf: MTBDD) -> u64;
44    pub fn Sylvan_mtbdd_getvar(node: MTBDD) -> u32;
45    pub fn Sylvan_var(node: MTBDD) -> u32;
46    pub fn Sylvan_mtbdd_getlow(node: MTBDD) -> MTBDD;
47    pub fn Sylvan_low(node: MTBDD) -> MTBDD;
48    pub fn Sylvan_mtbdd_gethigh(node: MTBDD) -> MTBDD;
49    pub fn Sylvan_high(node: MTBDD) -> MTBDD;
50    pub fn Sylvan_mtbdd_hascomp(dd: MTBDD) -> c_int;
51    pub fn Sylvan_mtbdd_comp(dd: MTBDD) -> MTBDD;
52    pub fn Sylvan_mtbdd_not(dd: MTBDD) -> MTBDD;
53    pub fn Sylvan_mtbdd_int64(value: i64) -> MTBDD;
54    pub fn Sylvan_mtbdd_double(value: c_double) -> MTBDD;
55    pub fn Sylvan_mtbdd_fraction(numer: i64, denom: u64) -> MTBDD;
56    pub fn Sylvan_mtbdd_getint64(terminal: MTBDD) -> i64;
57    pub fn Sylvan_mtbdd_getdouble(terminal: MTBDD) -> c_double;
58    pub fn Sylvan_mtbdd_getnumer(terminal: MTBDD) -> i32;
59    pub fn Sylvan_mtbdd_getdenom(terminal: MTBDD) -> u32;
60    pub fn Sylvan_mtbdd_ithvar(var: u32) -> MTBDD;
61    pub fn Sylvan_ithvar(var: u32) -> MTBDD;
62    pub fn Sylvan_mtbdd_set_empty() -> MTBDD;
63    pub fn Sylvan_set_empty() -> MTBDD;
64    pub fn Sylvan_mtbdd_set_isempty(set: MTBDD) -> c_int;
65    pub fn Sylvan_set_isempty(set: MTBDD) -> c_int;
66    pub fn Sylvan_mtbdd_set_first(set: MTBDD) -> u32;
67    pub fn Sylvan_set_first(set: MTBDD) -> u32;
68    pub fn Sylvan_mtbdd_set_next(set: MTBDD) -> MTBDD;
69    pub fn Sylvan_set_next(set: MTBDD) -> MTBDD;
70    pub fn Sylvan_mtbdd_set_from_array(arr: *mut u32, length: size_t) -> MTBDD;
71    pub fn Sylvan_mtbdd_fromarray(arr: *mut u32, length: size_t) -> MTBDD;
72    pub fn Sylvan_mtbdd_set_fromarray(arr: *mut u32, length: size_t) -> MTBDD;
73    pub fn Sylvan_set_fromarray(arr: *mut u32, length: size_t) -> MTBDD;
74    pub fn Sylvan_mtbdd_set_to_array(set: MTBDD, arr: *mut u32) -> c_void;
75    pub fn Sylvan_mtbdd_set_toarray(set: MTBDD, arr: *mut u32) -> c_void;
76    pub fn Sylvan_set_toarray(set: MTBDD, arr: *mut u32) -> c_void;
77    pub fn Sylvan_mtbdd_set_count(set: MTBDD) -> size_t;
78    pub fn Sylvan_set_count(set: MTBDD) -> size_t;
79    pub fn Sylvan_mtbdd_set_union(set1: MTBDD, set2: MTBDD) -> MTBDD;
80    pub fn Sylvan_mtbdd_set_addall(set1: MTBDD, set2: MTBDD) -> MTBDD;
81    pub fn Sylvan_set_addall(set1: MTBDD, set2: MTBDD) -> MTBDD;
82    pub fn Sylvan_mtbdd_set_minus(set1: MTBDD, set2: MTBDD) -> MTBDD;
83    pub fn Sylvan_mtbdd_set_removeall(set1: MTBDD, set2: MTBDD) -> MTBDD;
84    pub fn Sylvan_set_removeall(set1: MTBDD, set2: MTBDD) -> MTBDD;
85    pub fn Sylvan_mtbdd_set_contains(set: MTBDD, var: u32) -> c_int;
86    pub fn Sylvan_mtbdd_set_in(set: MTBDD, var: u32) -> c_int;
87    pub fn Sylvan_set_in(set: MTBDD, var: u32) -> c_int;
88    pub fn Sylvan_mtbdd_set_add(set: MTBDD, var: u32) -> MTBDD;
89    pub fn Sylvan_set_add(set: MTBDD, var: u32) -> MTBDD;
90    pub fn Sylvan_mtbdd_set_remove(set: MTBDD, var: u32) -> MTBDD;
91    pub fn Sylvan_set_remove(set: MTBDD, var: u32) -> MTBDD;
92    pub fn Sylvan_mtbdd_test_isset(set: MTBDD) -> c_void;
93    pub fn Sylvan_test_isset(set: MTBDD) -> c_void;
94    pub fn Sylvan_mtbdd_cube(variables: MTBDD, cube: *mut u8, terminal: MTBDD) -> MTBDD;
95    pub fn Sylvan_mtbdd_union_cube(
96        mtbdd: MTBDD,
97        variables: MTBDD,
98        cube: *mut u8,
99        terminal: MTBDD,
100    ) -> MTBDD;
101    pub fn Sylvan_mtbdd_satcount(dd: MTBDD, nvars: size_t) -> c_double;
102    pub fn Sylvan_mtbdd_leafcount_more(mtbdds: *const MTBDD, count: size_t) -> size_t;
103    pub fn Sylvan_mtbdd_leafcount(dd: MTBDD) -> size_t;
104    pub fn Sylvan_mtbdd_nodecount_more(mtbdds: *const MTBDD, count: size_t) -> size_t;
105    pub fn Sylvan_mtbdd_nodecount(dd: MTBDD) -> size_t;
106    pub fn Sylvan_nodecount(dd: MTBDD) -> size_t;
107    pub fn Sylvan_mtbdd_apply(a: MTBDD, b: MTBDD, op: MTBDD_APPLY_OP) -> MTBDD;
108    pub fn Sylvan_mtbdd_applyp(
109        a: MTBDD,
110        b: MTBDD,
111        p: size_t,
112        op: MTBDD_APPLYP_OP,
113        opid: u64,
114    ) -> MTBDD;
115    pub fn Sylvan_mtbdd_uapply(dd: MTBDD, op: MTBDD_UAPPLY_OP, param: size_t) -> MTBDD;
116    pub fn Sylvan_mtbdd_abstract(a: MTBDD, v: MTBDD, op: MTBDD_ABSTRACT_OP) -> MTBDD;
117    pub fn Sylvan_mtbdd_negate(a: MTBDD) -> MTBDD;
118    pub fn Sylvan_mtbdd_cmpl(a: MTBDD) -> MTBDD;
119    pub fn Sylvan_mtbdd_plus(a: MTBDD, b: MTBDD) -> MTBDD;
120    pub fn Sylvan_mtbdd_minus(a: MTBDD, b: MTBDD) -> MTBDD;
121    pub fn Sylvan_mtbdd_times(a: MTBDD, b: MTBDD) -> MTBDD;
122    pub fn Sylvan_mtbdd_min(a: MTBDD, b: MTBDD) -> MTBDD;
123    pub fn Sylvan_mtbdd_max(a: MTBDD, b: MTBDD) -> MTBDD;
124    pub fn Sylvan_mtbdd_abstract_plus(dd: MTBDD, v: MTBDD) -> MTBDD;
125    pub fn Sylvan_mtbdd_abstract_times(dd: MTBDD, v: MTBDD) -> MTBDD;
126    pub fn Sylvan_mtbdd_abstract_min(dd: MTBDD, v: MTBDD) -> MTBDD;
127    pub fn Sylvan_mtbdd_abstract_max(dd: MTBDD, v: MTBDD) -> MTBDD;
128    pub fn Sylvan_mtbdd_ite(f: MTBDD, g: MTBDD, h: MTBDD) -> MTBDD;
129    pub fn Sylvan_mtbdd_and_abstract_plus(a: MTBDD, b: MTBDD, vars: MTBDD) -> MTBDD;
130    pub fn Sylvan_mtbdd_and_exists(a: MTBDD, b: MTBDD, vars: MTBDD) -> MTBDD;
131    pub fn Sylvan_mtbdd_and_abstract_max(a: MTBDD, b: MTBDD, vars: MTBDD) -> MTBDD;
132    pub fn Sylvan_mtbdd_threshold_double(dd: MTBDD, value: c_double) -> MTBDD;
133    pub fn Sylvan_mtbdd_strict_threshold_double(dd: MTBDD, value: c_double) -> MTBDD;
134    pub fn Sylvan_mtbdd_equal_norm_d(a: MTBDD, b: MTBDD, epsilon: c_double) -> MTBDD;
135    pub fn Sylvan_mtbdd_equal_norm_rel_d(a: MTBDD, b: MTBDD, epsilon: c_double) -> MTBDD;
136    pub fn Sylvan_mtbdd_leq(a: MTBDD, b: MTBDD) -> MTBDD;
137    pub fn Sylvan_mtbdd_less(a: MTBDD, b: MTBDD) -> MTBDD;
138    pub fn Sylvan_mtbdd_geq(a: MTBDD, b: MTBDD) -> MTBDD;
139    pub fn Sylvan_mtbdd_greater(a: MTBDD, b: MTBDD) -> MTBDD;
140    pub fn Sylvan_mtbdd_support(dd: MTBDD) -> MTBDD;
141    pub fn Sylvan_support(dd: MTBDD) -> MTBDD;
142    pub fn Sylvan_mtbdd_compose(dd: MTBDD, map: MTBDDMAP) -> MTBDD;
143    pub fn Sylvan_mtbdd_minimum(dd: MTBDD) -> MTBDD;
144    pub fn Sylvan_mtbdd_maximum(dd: MTBDD) -> MTBDD;
145    pub fn Sylvan_mtbdd_enum_first(
146        dd: MTBDD,
147        variables: MTBDD,
148        arr: *mut u8,
149        filter_cb: MTBDD_ENUM_FILTER_CB,
150    ) -> MTBDD;
151    pub fn Sylvan_mtbdd_enum_next(
152        dd: MTBDD,
153        variables: MTBDD,
154        arr: *mut u8,
155        filter_cb: MTBDD_ENUM_FILTER_CB,
156    ) -> MTBDD;
157    pub fn Sylvan_mtbdd_enum_all_first(
158        dd: MTBDD,
159        variables: MTBDD,
160        arr: *mut u8,
161        filter_cb: MTBDD_ENUM_FILTER_CB,
162    ) -> MTBDD;
163    pub fn Sylvan_mtbdd_enum_all_next(
164        dd: MTBDD,
165        variables: MTBDD,
166        arr: *mut u8,
167        filter_cb: MTBDD_ENUM_FILTER_CB,
168    ) -> MTBDD;
169    pub fn Sylvan_mtbdd_enum_par(dd: MTBDD, cb: MTBDD_ENUM_CB, context: *mut c_void) -> c_void;
170    pub fn Sylvan_mtbdd_eval_compose(dd: MTBDD, vars: MTBDD, cb: MTBDD_EVAL_COMPOSE_CB) -> MTBDD;
171    pub fn Sylvan_mtbdd_test_isvalid(mtbdd: MTBDD) -> c_int;
172    pub fn Sylvan_test_isbdd(mtbdd: MTBDD) -> c_int;
173    pub fn Sylvan_mtbdd_fprintdot(out: *mut FILE, mtbdd: MTBDD) -> c_void;
174    pub fn Sylvan_fprintdot(out: *mut FILE, mtbdd: MTBDD) -> c_void;
175    pub fn Sylvan_mtbdd_printdot(mtbdd: MTBDD) -> c_void;
176    pub fn Sylvan_printdot(mtbdd: MTBDD) -> c_void;
177    pub fn Sylvan_mtbdd_fprintdot_nc(out: *mut FILE, mtbdd: MTBDD) -> c_void;
178    pub fn Sylvan_mtbdd_printdot_nc(mtbdd: MTBDD) -> c_void;
179    pub fn Sylvan_mtbdd_fprint_leaf(out: *mut FILE, leaf: MTBDD) -> c_void;
180    pub fn Sylvan_mtbdd_print_leaf(leaf: MTBDD) -> c_void;
181    pub fn Sylvan_mtbdd_leaf_to_str(leaf: MTBDD, buf: *mut c_char, buflen: size_t) -> *mut c_char;
182    pub fn Sylvan_mtbdd_printsha(dd: MTBDD) -> c_void;
183    pub fn Sylvan_printsha(dd: MTBDD) -> c_void;
184    pub fn Sylvan_mtbdd_fprintsha(f: *mut FILE, dd: MTBDD) -> c_void;
185    pub fn Sylvan_fprintsha(f: *mut FILE, dd: MTBDD) -> c_void;
186    pub fn Sylvan_mtbdd_getsha(dd: MTBDD, target: *mut c_char) -> c_void;
187    pub fn Sylvan_getsha(dd: MTBDD, target: *mut c_char) -> c_void;
188    pub fn Sylvan_mtbdd_visit_seq(
189        dd: MTBDD,
190        pre: MTBDD_VISIT_PRE_CB,
191        post: MTBDD_VISIT_POST_CB,
192        context: *mut c_void,
193    ) -> c_void;
194    pub fn Sylvan_mtbdd_visit_par(
195        dd: MTBDD,
196        pre: MTBDD_VISIT_PRE_CB,
197        post: MTBDD_VISIT_POST_CB,
198        context: *mut c_void,
199    ) -> c_void;
200    pub fn Sylvan_mtbdd_writer_tobinary(file: *mut FILE, dds: *mut MTBDD, count: c_int) -> c_void;
201    pub fn Sylvan_mtbdd_writer_totext(file: *mut FILE, dds: *mut MTBDD, count: c_int) -> c_void;
202    pub fn Sylvan_mtbdd_writer_start() -> SkipListPtr;
203    pub fn Sylvan_mtbdd_writer_add(sl: SkipListPtr, dd: MTBDD) -> c_void;
204    pub fn Sylvan_mtbdd_writer_writebinary(out: *mut FILE, sl: SkipListPtr) -> c_void;
205    pub fn Sylvan_mtbdd_writer_get(sl: SkipListPtr, dd: MTBDD) -> u64;
206    pub fn Sylvan_mtbdd_writer_end(sl: SkipListPtr) -> c_void;
207    pub fn Sylvan_mtbdd_reader_frombinary(file: *mut FILE, dds: *mut MTBDD, count: c_int) -> c_int;
208    pub fn Sylvan_mtbdd_reader_readbinary(file: *mut FILE) -> *mut u64;
209    pub fn Sylvan_mtbdd_reader_get(arr: *mut u64, identifier: u64) -> MTBDD;
210    pub fn Sylvan_mtbdd_reader_end(arr: *mut u64) -> c_void;
211    pub fn Sylvan_mtbdd_map_empty() -> MTBDD;
212    pub fn Sylvan_map_empty() -> MTBDD;
213    pub fn Sylvan_mtbdd_map_isempty(map: MTBDD) -> c_int;
214    pub fn Sylvan_map_isempty(map: MTBDD) -> c_int;
215    pub fn Sylvan_mtbdd_map_key(map: MTBDD) -> u32;
216    pub fn Sylvan_map_key(map: MTBDD) -> u32;
217    pub fn Sylvan_mtbdd_map_value(map: MTBDD) -> MTBDD;
218    pub fn Sylvan_map_value(map: MTBDD) -> MTBDD;
219    pub fn Sylvan_mtbdd_map_next(map: MTBDD) -> MTBDD;
220    pub fn Sylvan_map_next(map: MTBDD) -> MTBDD;
221    pub fn Sylvan_mtbdd_map_contains(map: MTBDDMAP, key: u32) -> c_int;
222    pub fn Sylvan_map_contains(map: MTBDDMAP, key: u32) -> c_int;
223    pub fn Sylvan_mtbdd_map_count(map: MTBDDMAP) -> size_t;
224    pub fn Sylvan_map_count(map: MTBDDMAP) -> size_t;
225    pub fn Sylvan_mtbdd_map_add(map: MTBDDMAP, key: u32, value: MTBDD) -> MTBDDMAP;
226    pub fn Sylvan_map_add(map: MTBDDMAP, key: u32, value: MTBDD) -> MTBDDMAP;
227    pub fn Sylvan_mtbdd_map_update(map1: MTBDDMAP, map2: MTBDDMAP) -> MTBDDMAP;
228    pub fn Sylvan_mtbdd_map_addall(map1: MTBDDMAP, map2: MTBDDMAP) -> MTBDDMAP;
229    pub fn Sylvan_map_addall(map1: MTBDDMAP, map2: MTBDDMAP) -> MTBDDMAP;
230    pub fn Sylvan_mtbdd_map_remove(map: MTBDDMAP, key: u32) -> MTBDDMAP;
231    pub fn Sylvan_map_remove(map: MTBDDMAP, key: u32) -> MTBDDMAP;
232    pub fn Sylvan_mtbdd_map_removeall(map: MTBDDMAP, variables: MTBDD) -> MTBDDMAP;
233    pub fn Sylvan_map_removeall(map: MTBDDMAP, variables: MTBDD) -> MTBDDMAP;
234    pub fn Sylvan_mtbdd_gc_mark_rec(mtbdd: MTBDD) -> c_void;
235    pub fn Sylvan_gc_mark_rec(mtbdd: MTBDD) -> c_void;
236    pub fn Sylvan_mtbdd_protect(ptr: *mut MTBDD) -> c_void;
237    pub fn Sylvan_protect(ptr: *mut MTBDD) -> c_void;
238    pub fn Sylvan_mtbdd_unprotect(ptr: *mut MTBDD) -> c_void;
239    pub fn Sylvan_unprotect(ptr: *mut MTBDD) -> c_void;
240    pub fn Sylvan_mtbdd_count_protected() -> size_t;
241    pub fn Sylvan_count_protected() -> size_t;
242    pub fn Sylvan_mtbdd_ref(dd: MTBDD) -> MTBDD;
243    pub fn Sylvan_ref(dd: MTBDD) -> MTBDD;
244    pub fn Sylvan_mtbdd_deref(dd: MTBDD) -> c_void;
245    pub fn Sylvan_deref(dd: MTBDD) -> c_void;
246    pub fn Sylvan_mtbdd_count_refs() -> size_t;
247    pub fn Sylvan_count_refs() -> size_t;
248    pub fn Sylvan_mtbdd_refs_pushptr(ptr: *const MTBDD) -> c_void;
249    pub fn Sylvan_refs_pushptr(ptr: *const MTBDD) -> c_void;
250    pub fn Sylvan_mtbdd_refs_popptr(amount: size_t) -> c_void;
251    pub fn Sylvan_refs_popptr(amount: size_t) -> c_void;
252    pub fn Sylvan_mtbdd_refs_push(mtbdd: MTBDD) -> MTBDD;
253    pub fn Sylvan_refs_push(mtbdd: MTBDD) -> MTBDD;
254    pub fn Sylvan_mtbdd_refs_pop(amount: c_long) -> c_void;
255    pub fn Sylvan_refs_pop(amount: c_long) -> c_void;
256    pub fn Sylvan_mtbdd_refs_spawn(t: *mut Task) -> c_void;
257    pub fn Sylvan_refs_spawn(t: *mut Task) -> c_void;
258    pub fn Sylvan_mtbdd_refs_sync(mtbdd: MTBDD) -> MTBDD;
259    pub fn Sylvan_refs_sync(mtbdd: MTBDD) -> MTBDD;
260}
sylvan_sys/mtbdd.rs

sylvan_sys/
mtbdd.rs
