00001 #ifndef DSD_OR_DECOMPOSE
00002 #define DSD_OR_DECOMPOSE
00003
00004 #include "DSDDecompose.h"
00005
00010 DSDNode* OR_Decomp(DSDManager* manager, DdNode* f, DdNode *top_func, DSDNode* T,DSDNode* E);
00011
00016 DSDNode *BDN_OR_VAR_EXP(DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *base);
00017
00022 DSDNode *BDN_NOR_VAR_EXP(DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *base);
00023
00028 DSDNode *BDN_OR_VAR_DEC(DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *base);
00029
00034 DSDNode *BDN_NOR_VAR_DEC(DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *base);
00035
00040 DSDNode *BDN_OR_DEC_ACTUALS(DSDManager *manager, DdNode *f, DSDNode *node, ActualNode *actuals);
00041
00046 DSDNode *BDN_NOR_DEC_ACTUALS(DSDManager *manager, DdNode *f, DSDNode *node, ActualNode *actuals);
00047
00051 DSDNode *BDN_OR_DEC_DEC(DSDManager *manager, DdNode *f, DSDNode *node1, DSDNode *node2);
00052
00056 DSDNode *BDN_NOR_DEC_DEC(DSDManager *manager, DdNode *f, DSDNode *node1, DSDNode *node2);
00057
00061 DSDNode *BDN_OR_ACTUALS(DSDManager *manager, DdNode *f, ActualNode *actuals);
00062
00066 DSDNode *BDN_NOR_ACTUALS(DSDManager *manager, DdNode *f, ActualNode *actuals);
00067
00072 DSDNode *BDN_BDD_OR_RESIDUE(DSDManager *manager, ActualNode *residue);
00073
00078 DSDNode *BDN_BDD_NOR_RESIDUE(DSDManager *manager, ActualNode *residue);
00079
00084 DSDNode *BDN_BDD_NOR_VAR_ACTUALS(DSDManager *manager, DdNode *top_func, ActualNode *residue);
00085
00090 DSDNode *BDN_BDD_NOR_VAR_DEC(DSDManager *manager, DdNode *top_func, DSDNode *node);
00091
00092 #endif
