cudd_sys/
dddmp.rs

1use crate::{DdManager, DdNode};
2use libc::{FILE, c_char, c_int};
3
4/// Version of DDDMP format.
5pub const DDDMP_VERSION: &str = "DDDMP-2.0";
6
7/// Returned by functions when failed.
8pub const DDDMP_FAILURE: c_int = 0;
9
10/// Returned by functions when succeeded.
11pub const DDDMP_SUCCESS: c_int = 1;
12
13/// Text formatting mode.
14pub const DDDMP_MODE_TEXT: c_int = 'A' as c_int;
15
16/// Binary formatting mode.
17pub const DDDMP_MODE_BINARY: c_int = 'B' as c_int;
18
19/// Default formatting mode.
20pub const DDDMP_MODE_DEFAULT: c_int = 'D' as c_int;
21
22#[repr(C)]
23pub enum Dddmp_DecompCnfStoreType {
24    DDDMP_CNF_MODE_NODE,
25    DDDMP_CNF_MODE_MAXTERM,
26    DDDMP_CNF_MODE_BEST,
27}
28
29#[repr(C)]
30pub enum Dddmp_DecompCnfLoadType {
31    DDDMP_CNF_MODE_NO_CONJ,
32    DDDMP_CNF_MODE_NO_QUANT,
33    DDDMP_CNF_MODE_CONJ_QUANT,
34}
35
36#[repr(C)]
37pub enum Dddmp_DecompType {
38    DDDMP_BDD,
39    DDDMP_ADD,
40    DDDMP_CNF,
41    DDDMP_NONE,
42}
43
44#[repr(C)]
45pub enum Dddmp_VarInfoType {
46    DDDMP_VARIDS,
47    DDDMP_VARPERMIDS,
48    DDDMP_VARAUXIDS,
49    DDDMP_VARNAMES,
50    DDDMP_VARDEFAULT,
51}
52
53#[repr(C)]
54pub enum Dddmp_VarMatchType {
55    DDDMP_VAR_MATCHIDS,
56    DDDMP_VAR_MATCHPERMIDS,
57    DDDMP_VAR_MATCHAUXIDS,
58    DDDMP_VAR_MATCHNAMES,
59    DDDMP_VAR_COMPOSEIDS,
60}
61
62#[repr(C)]
63pub enum Dddmp_RootMatchType {
64    DDDMP_ROOT_MATCHNAMES,
65    DDDMP_ROOT_MATCHLIST,
66}
67
68unsafe extern "C" {
69    pub fn Dddmp_Text2Bin(filein: *mut c_char, fileout: *mut c_char) -> c_int;
70    pub fn Dddmp_Bin2Text(filein: *mut c_char, fileout: *mut c_char) -> c_int;
71    pub fn Dddmp_cuddBddDisplayBinary(fileIn: *mut c_char, fileOut: *mut c_char) -> c_int;
72    pub fn Dddmp_cuddBddLoad(
73        ddMgr: *mut DdManager,
74        varMatchMode: Dddmp_VarMatchType,
75        varmatchnames: *mut *mut c_char,
76        varmatchauxids: *mut c_int,
77        varcomposeids: *mut c_int,
78        mode: c_int,
79        file: *mut c_char,
80        fp: *mut FILE,
81    ) -> *mut DdNode;
82    pub fn Dddmp_cuddBddArrayLoad(
83        ddMgr: *mut DdManager,
84        rootMatchMode: Dddmp_RootMatchType,
85        rootmatchnames: *mut *mut c_char,
86        varMatchMode: Dddmp_VarMatchType,
87        varmatchnames: *mut *mut c_char,
88        varmatchauxids: *mut c_int,
89        varcomposeids: *mut c_int,
90        mode: c_int,
91        file: *mut c_char,
92        fp: *mut FILE,
93        pproots: *mut *mut *mut DdNode,
94    ) -> c_int;
95    pub fn Dddmp_cuddAddLoad(
96        ddMgr: *mut DdManager,
97        varMatchMode: Dddmp_VarMatchType,
98        varmatchnames: *mut *mut c_char,
99        varmatchauxids: *mut c_int,
100        varcomposeids: *mut c_int,
101        mode: c_int,
102        file: *mut c_char,
103        fp: *mut FILE,
104    ) -> *mut DdNode;
105    pub fn Dddmp_cuddAddArrayLoad(
106        ddMgr: *mut DdManager,
107        rootMatchMode: Dddmp_RootMatchType,
108        rootmatchnames: *mut *mut c_char,
109        varMatchMode: Dddmp_VarMatchType,
110        varmatchnames: *mut *mut c_char,
111        varmatchauxids: *mut c_int,
112        varcomposeids: *mut c_int,
113        mode: c_int,
114        file: *mut c_char,
115        fp: *mut FILE,
116        pproots: *mut *mut *mut DdNode,
117    ) -> c_int;
118    pub fn Dddmp_cuddHeaderLoad(
119        ddType: *mut Dddmp_DecompType,
120        nVars: *mut c_int,
121        nsuppvars: *mut c_int,
122        suppVarNames: *mut *mut *mut c_char,
123        orderedVarNames: *mut *mut *mut c_char,
124        varIds: *mut *mut c_int,
125        composeIds: *mut *mut c_int,
126        auxIds: *mut *mut c_int,
127        nRoots: *mut c_int,
128        file: *mut c_char,
129        fp: *mut FILE,
130    ) -> c_int;
131    pub fn Dddmp_cuddBddLoadCnf(
132        ddMgr: *mut DdManager,
133        varmatchmode: Dddmp_VarMatchType,
134        varmatchnames: *mut *mut c_char,
135        varmatchauxids: *mut c_int,
136        varcomposeids: *mut c_int,
137        mode: c_int,
138        file: *mut c_char,
139        fp: *mut FILE,
140        rootsPtrPtr: *mut *mut *mut DdNode,
141        nRoots: *mut c_int,
142    ) -> c_int;
143    pub fn Dddmp_cuddBddArrayLoadCnf(
144        ddMgr: *mut DdManager,
145        rootmatchmode: Dddmp_RootMatchType,
146        rootmatchnames: *mut *mut c_char,
147        varmatchmode: Dddmp_VarMatchType,
148        varmatchnames: *mut *mut c_char,
149        varmatchauxids: *mut c_int,
150        varcomposeids: *mut c_int,
151        mode: c_int,
152        file: *mut c_char,
153        fp: *mut FILE,
154        rootsPtrPtr: *mut *mut *mut DdNode,
155        nRoots: *mut c_int,
156    ) -> c_int;
157    pub fn Dddmp_cuddHeaderLoadCnf(
158        nVars: *mut c_int,
159        nsuppvars: *mut c_int,
160        suppVarNames: *mut *mut *mut c_char,
161        orderedVarNames: *mut *mut *mut c_char,
162        varIds: *mut *mut c_int,
163        composeIds: *mut *mut c_int,
164        auxIds: *mut *mut c_int,
165        nRoots: *mut c_int,
166        file: *mut c_char,
167        fp: *mut FILE,
168    ) -> c_int;
169    pub fn Dddmp_cuddAddStore(
170        ddMgr: *mut DdManager,
171        ddname: *mut c_char,
172        f: *mut DdNode,
173        varnames: *mut *mut c_char,
174        auxids: *mut c_int,
175        mode: c_int,
176        varinfo: Dddmp_VarInfoType,
177        fname: *mut c_char,
178        fp: *mut FILE,
179    ) -> c_int;
180    pub fn Dddmp_cuddAddArrayStore(
181        ddMgr: *mut DdManager,
182        ddname: *mut c_char,
183        nRoots: c_int,
184        f: *mut *mut DdNode,
185        rootnames: *mut *mut c_char,
186        varnames: *mut *mut c_char,
187        auxids: *mut c_int,
188        mode: c_int,
189        varinfo: Dddmp_VarInfoType,
190        fname: *mut c_char,
191        fp: *mut FILE,
192    ) -> c_int;
193    pub fn Dddmp_cuddBddStore(
194        ddMgr: *mut DdManager,
195        ddname: *mut c_char,
196        f: *mut DdNode,
197        varnames: *mut *mut c_char,
198        auxids: *mut c_int,
199        mode: c_int,
200        varinfo: Dddmp_VarInfoType,
201        fname: *mut c_char,
202        fp: *mut FILE,
203    ) -> c_int;
204    pub fn Dddmp_cuddBddArrayStore(
205        ddMgr: *mut DdManager,
206        ddname: *mut c_char,
207        nRoots: c_int,
208        f: *mut *mut DdNode,
209        rootnames: *mut *mut c_char,
210        varnames: *mut *mut c_char,
211        auxids: *mut c_int,
212        mode: c_int,
213        varinfo: Dddmp_VarInfoType,
214        fname: *mut c_char,
215        fp: *mut FILE,
216    ) -> c_int;
217    pub fn Dddmp_cuddBddStoreCnf(
218        ddMgr: *mut DdManager,
219        f: *mut DdNode,
220        mode: Dddmp_DecompCnfStoreType,
221        noHeader: c_int,
222        varNames: *mut *mut c_char,
223        bddIds: *mut c_int,
224        bddAuxIds: *mut c_int,
225        cnfIds: *mut c_int,
226        idInitial: c_int,
227        edgeInTh: c_int,
228        pathLengthTh: c_int,
229        fname: *mut c_char,
230        fp: *mut FILE,
231        clauseNPtr: *mut c_int,
232        varNewNPtr: *mut c_int,
233    ) -> c_int;
234    pub fn Dddmp_cuddBddArrayStoreCnf(
235        ddMgr: *mut DdManager,
236        f: *mut *mut DdNode,
237        rootN: c_int,
238        mode: Dddmp_DecompCnfStoreType,
239        noHeader: c_int,
240        varNames: *mut *mut c_char,
241        bddIds: *mut c_int,
242        bddAuxIds: *mut c_int,
243        cnfIds: *mut c_int,
244        idInitial: c_int,
245        edgeInTh: c_int,
246        pathLengthTh: c_int,
247        fname: *mut c_char,
248        fp: *mut FILE,
249        clauseNPtr: *mut c_int,
250        varNewNPtr: *mut c_int,
251    ) -> c_int;
252    pub fn Dddmp_cuddBddStorePrefix(
253        ddMgr: *mut DdManager,
254        nRoots: c_int,
255        f: *mut DdNode,
256        inputNames: *mut *mut c_char,
257        outputNames: *mut *mut c_char,
258        modelName: *mut c_char,
259        fileName: *mut c_char,
260        fp: *mut FILE,
261    ) -> c_int;
262    pub fn Dddmp_cuddBddArrayStorePrefix(
263        ddMgr: *mut DdManager,
264        nroots: c_int,
265        f: *mut *mut DdNode,
266        inputNames: *mut *mut c_char,
267        outputNames: *mut *mut c_char,
268        modelName: *mut c_char,
269        fname: *mut c_char,
270        fp: *mut FILE,
271    ) -> c_int;
272    pub fn Dddmp_cuddBddStoreBlif(
273        ddMgr: *mut DdManager,
274        nRoots: c_int,
275        f: *mut DdNode,
276        inputNames: *mut *mut c_char,
277        outputNames: *mut *mut c_char,
278        modelName: *mut c_char,
279        fileName: *mut c_char,
280        fp: *mut FILE,
281    ) -> c_int;
282    pub fn Dddmp_cuddBddArrayStoreBlif(
283        ddMgr: *mut DdManager,
284        nroots: c_int,
285        f: *mut *mut DdNode,
286        inputNames: *mut *mut c_char,
287        outputNames: *mut *mut c_char,
288        modelName: *mut c_char,
289        fname: *mut c_char,
290        fp: *mut FILE,
291    ) -> c_int;
292    pub fn Dddmp_cuddBddStoreSmv(
293        ddMgr: *mut DdManager,
294        nRoots: c_int,
295        f: *mut DdNode,
296        inputNames: *mut *mut c_char,
297        outputNames: *mut *mut c_char,
298        modelName: *mut c_char,
299        fileName: *mut c_char,
300        fp: *mut FILE,
301    ) -> c_int;
302    pub fn Dddmp_cuddBddArrayStoreSmv(
303        ddMgr: *mut DdManager,
304        nroots: c_int,
305        f: *mut *mut DdNode,
306        inputNames: *mut *mut c_char,
307        outputNames: *mut *mut c_char,
308        modelName: *mut c_char,
309        fname: *mut c_char,
310        fp: *mut FILE,
311    ) -> c_int;
312}
cudd_sys/dddmp.rs

cudd_sys/
dddmp.rs
