00001 #ifndef DSD_XOR_DECOMPOSE
00002 #define DSD_XOR_DECOMPOSE
00003
00004 #include "DSDDecompose.h"
00005
00010 DSDNode* XOR_Decomp(DSDManager* manager, DdNode* f, DdNode *top_func, DSDNode* T, DSDNode* E);
00011
00016 DSDNode *BDN_XOR_VAR_EXP(DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *base);
00017
00022 DSDNode *BDN_NXOR_VAR_EXP(DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *base);
00023
00028 DSDNode *BDN_XOR_VAR_DEC(DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *base);
00029
00034 DSDNode *BDN_NXOR_VAR_DEC(DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *base);
00035
00040 DSDNode *BDN_XOR_DEC_ACTUALS(DSDManager *manager, DdNode *f, DSDNode *node, ActualNode *actuals);
00041
00046 DSDNode *BDN_NXOR_DEC_ACTUALS(DSDManager *manager, DdNode *f, DSDNode *node, ActualNode *actuals);
00047
00048
00052 DSDNode *BDN_XOR_DEC_DEC(DSDManager *manager, DdNode *f, DSDNode *node1, DSDNode *node2);
00053
00057 DSDNode *BDN_NXOR_DEC_DEC(DSDManager *manager, DdNode *f, DSDNode *node1, DSDNode *node2);
00058
00062 DSDNode *BDN_XOR_ACTUALS(DSDManager *manager, DdNode *f, ActualNode *actuals);
00063
00067 DSDNode *BDN_NXOR_ACTUALS(DSDManager *manager, DdNode *f, ActualNode *actuals);
00068
00073 DSDNode *BDN_BDD_XOR_RESIDUE(DSDManager *manager, ActualNode *residue);
00074
00079 DSDNode *BDN_BDD_NXOR_RESIDUE(DSDManager *manager, ActualNode *residue);
00080
00081 #endif
