00001 #ifndef DSD_PRIME_DECOMPOSE
00002 #define DSD_PRIME_DECOMPOSE
00003
00004 #include "DSDDecompose.h"
00005
00010 DSDNode* Prime_Decomp(DSDManager* manager, DdNode* f, DdNode *top_func, DSDNode* T, DSDNode* E);
00011
00016 DSDNode *BDN_MUX_VAR_DEC_DEC(DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *E, DSDNode *T);
00017
00023 DSDNode *BDN_BDD_MUX_VAR_DEC_DEC(DSDManager *manager, DdNode *top_func, DSDNode *E, DSDNode *T);
00024
00025
00030 DSDNode *BDN_BDD_PRIME_SUB(DSDManager *manager, DdNode *f, DdNode *top_func, ActualNode *conflict_residue, DSDNode *node);
00031
00036 DSDNode *BDN_BDD_PRIME_XOR_SUB(DSDManager *manager, DdNode *f, DdNode *top_func, ActualNode *conflict_residue, DSDNode *node);
00037
00042 DSDNode *BDN_BDD_PRIME_MUX_SUB(DSDManager *manager, DdNode *f, DdNode *top_func, ActualNode *conflict_residue, DSDNode *node);
00043
00048 ActualNode *cofactor_container_node_equivalence(DSDManager *manager, DSDNode *container, DSDNode *child);
00049
00054 ActualNode *cofactor_cofactor_equivalence(DSDManager *manager, DSDNode *container, DSDNode *child, int *switch_them);
00055
00060 ActualNode *cofactor_equivalence(DSDManager *manager, DSDNode *container, DSDNode *child);
00061
00066 DSDNode *cofactor_elem_BDN_BDD_PRIME_SUB_ELEM(DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *node1, DSDNode *node2);
00067
00071 int symbolic_finder_builder(DSDManager *manager, DSDNode *node1, DSDNode *node2);
00072
00076 int symbolic_finder_builder_incomplete(DSDManager *manager, DSDNode *node1, DSDNode *node2);
00077
00078
00079
00080
00081 #endif
