|
Defines |
| #define | bdd_relprod(a, b, var) bdd_appex((a),(b),bddop_and,(var)) |
| | Relational product.
|
Functions |
| BDD | bdd_buildcube (int value, int width, BDD *var) |
| | Build a cube from an array of variables specified by a BDD array.
|
| BDD | bdd_ibuildcube (int value, int width, int *var) |
| | Build a cube from an array of variables.
|
| BDD | bdd_not (BDD r) |
| | Negates a bdd.
|
| BDD | bdd_apply (BDD l, BDD r, int op) |
| | Basic bdd operations.
|
| BDD | bdd_and (BDD l, BDD r) |
| | The logical 'and' of two bdds.
|
| BDD | bdd_or (BDD l, BDD r) |
| | The logical 'or' of two bdds.
|
| BDD | bdd_xor (BDD l, BDD r) |
| | The logical 'xor' of two bdds.
|
| BDD | bdd_imp (BDD l, BDD r) |
| | The logical 'implication' between two bdds.
|
| BDD | bdd_biimp (BDD l, BDD r) |
| | The logical 'bi-implication' between two bdds.
|
| BDD | bdd_ite (BDD f, BDD g, BDD h) |
| | If-then-else operator.
|
| BDD | bdd_restrict (BDD r, BDD var) |
| | Restric a set of variables to constant values.
|
| BDD | bdd_constrain (BDD f, BDD c) |
| | Generalized cofactor.
|
| BDD | bdd_replace (BDD r, bddPair *pair) |
| | Replaces variables with other variables.
|
| BDD | bdd_compose (BDD f, BDD g, BDD v) |
| | Functional composition.
|
| BDD | bdd_veccompose (BDD g, bddPair *pair) |
| | Simultaneous functional composition.
|
| BDD | bdd_simplify (BDD f, BDD d) |
| | Coudert and madre's restrict function.
|
| BDD | bdd_exist (BDD r, BDD var) |
| | Existential quantification of variables.
|
| BDD | bdd_forall (BDD r, BDD var) |
| | Universal quantification of variables.
|
| BDD | bdd_unique (BDD, BDD) |
| | Unique quantification of variables.
|
| BDD | bdd_appex (BDD l, BDD r, int opr, BDD var) |
| | Apply operation and existential quantification.
|
| BDD | bdd_appall (BDD l, BDD r, int opr, BDD var) |
| | Apply operation and universal quantification.
|
| BDD | bdd_appuni (BDD l, BDD r, int opr, BDD var) |
| | Apply operation and unique quantification.
|
| BDD | bdd_satone (BDD r) |
| | Finds one satisfying variable assignment.
|
| BDD | bdd_satoneset (BDD r, BDD var, BDD pol) |
| | Finds one satisfying variable assignment.
|
| BDD | bdd_fullsatone (BDD r) |
| | Finds one satisfying variable assignment.
|
| void | bdd_allsat (BDD r, bddallsathandler handler) |
| | Finds all satisfying variable assignments.
|
