00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00041 #ifndef _FDD_H
00042 #define _FDD_H
00043
00044 #include "bdd.h"
00045
00046
00047 #ifdef CPLUSPLUS
00048 extern "C" {
00049 #endif
00050
00051
00052
00071 extern int fdd_extdomain(int*, int);
00072
00073
00089 extern int fdd_overlapdomain(int, int);
00090
00091
00100 extern void fdd_clearall(void);
00101
00102
00112 extern int fdd_domainnum(void);
00113
00114
00124 extern int fdd_domainsize(int);
00125
00126
00136 extern int fdd_varnum(int);
00137
00138
00151 extern int* fdd_vars(int);
00152
00153
00166 extern BDD fdd_ithvar(int, int);
00167
00168
00180 extern int fdd_scanvar(BDD, int);
00181
00182
00194 extern int* fdd_scanallvar(BDD);
00195
00196
00207 extern BDD fdd_ithset(int);
00208
00209
00220 extern BDD fdd_domain(int);
00221
00222
00232 extern BDD fdd_equals(int, int);
00233
00234
00259 extern bddfilehandler fdd_file_hook(bddfilehandler);
00260 #ifdef CPLUSPLUS
00261 extern bddstrmhandler fdd_strm_hook(bddstrmhandler);
00262 #endif
00263
00264
00276 extern void fdd_printset(BDD);
00277
00278
00290 extern void fdd_fprintset(FILE*, BDD);
00291
00292
00304 extern int fdd_scanset(BDD, int**, int*);
00305
00306
00317 extern BDD fdd_makeset(int*, int);
00318
00319
00330 extern int fdd_intaddvarblock(int, int, int);
00331
00332
00344 extern int fdd_setpair(bddPair*, int, int);
00345
00346
00358 extern int fdd_setpairs(bddPair*, int*, int*, int);
00359
00360 #ifdef CPLUSPLUS
00361 }
00362 #endif
00363
00364
00365
00366
00367
00368 #ifdef CPLUSPLUS
00369
00370
00371
00372 inline bdd fdd_ithvarpp(int var, int val)
00373 { return fdd_ithvar(var, val); }
00374
00375 inline bdd fdd_ithsetpp(int var)
00376 { return fdd_ithset(var); }
00377
00378 inline bdd fdd_domainpp(int var)
00379 { return fdd_domain(var); }
00380
00381 inline int fdd_scanvar(const bdd &r, int var)
00382 { return fdd_scanvar(r.root, var); }
00383
00384 inline int* fdd_scanallvar(const bdd &r)
00385 { return fdd_scanallvar(r.root); }
00386
00387 inline bdd fdd_equalspp(int left, int right)
00388 { return fdd_equals(left, right); }
00389
00390 inline void fdd_printset(const bdd &r)
00391 { fdd_printset(r.root); }
00392
00393 inline void fdd_fprintset(FILE* ofile, const bdd &r)
00394 { fdd_fprintset(ofile, r.root); }
00395
00396 inline int fdd_scanset(const bdd &r, int *&v, int &n)
00397 { return fdd_scanset(r.root, &v, &n); }
00398
00399 inline bdd fdd_makesetpp(int *v, int n)
00400 { return fdd_makeset(v,n); }
00401
00402 #if 0
00403 inline bdd* fdd_conpp(int bitnum, int var)
00404 { return fdd_transfer( bitnum, fdd_con(bitnum, var) ); }
00405
00406 inline bdd* fdd_varpp(int bitnum, int var)
00407 { return fdd_transfer( bitnum, fdd_var(bitnum, var) ); }
00408
00409 extern int fdd_isconst(int bitnum, bdd *e);
00410 extern int fdd_val(int bitnum, bdd *e);
00411
00412 inline bdd* fdd_add(int bitnum, bdd *left, bdd *right)
00413 { return fdd_termopr(bitnum, left, right,bdd::fddAdd); }
00414
00415 inline bdd* fdd_sub(int bitnum, bdd *left, bdd *right)
00416 { return fdd_termopr(bitnum, left, right,bdd::fddSub); }
00417
00418 inline bdd* fdd_shl(int bitnum, bdd *expr, bdd c)
00419 { return fdd_shift(bitnum, expr, c, bdd::fddShl); }
00420
00421 inline bdd* fdd_shr(int bitnum, bdd *expr, bdd c)
00422 { return fdd_shift(bitnum, expr, c, bdd::fddShr); }
00423
00424 inline bdd fdd_lth(int bitnum, bdd *left, bdd *right)
00425 { return fdd_relopr(bitnum, left, right, bdd::fddLth); }
00426
00427 inline bdd fdd_lte(int bitnum, bdd *left, bdd *right)
00428 { return fdd_relopr(bitnum, left, right, bdd::fddLte); }
00429
00430 inline bdd fdd_gth(int bitnum, bdd *left, bdd *right)
00431 { return fdd_relopr(bitnum, left, right, bdd::fddGth); }
00432
00433 inline bdd fdd_gte(int bitnum, bdd *left, bdd *right)
00434 { return fdd_relopr(bitnum, left, right, bdd::fddGte); }
00435
00436 inline bdd fdd_equ(int bitnum, bdd *left, bdd *right)
00437 { return fdd_relopr(bitnum, left, right, bdd::fddEqu); }
00438
00439 inline bdd fdd_neq(int bitnum, bdd *left, bdd *right)
00440 { return fdd_relopr(bitnum, left, right, bdd::fddNeq); }
00441 #endif
00442
00443
00444 #define fdd_ithvar fdd_ithvarpp
00445 #define fdd_ithset fdd_ithsetpp
00446 #define fdd_domain fdd_domainpp
00447 #define fdd_equals fdd_equalspp
00448 #define fdd_makeset fdd_makesetpp
00449 #define fdd_con fdd_conpp
00450 #define fdd_var fdd_varpp
00451
00452
00453 #endif
00454
00455 #endif
00456
00457
00458