abc/src/opt/dsc/dsc.c
/**
 * This method implements the paper proposed by V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
 * entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis", presented at ICCD 2015.
 * pTruth: pointer for the truth table representing the target function.
 * nVarsInit: the number of variables of the truth table of the target function.
 * pRes: pointer for storing the resulting decomposition, whenever a decomposition can be found.
 * pool: NULL or a pointer for with a capacity of storing 3*nVars truth-tables. IF NULL, the function will allocate and free the memory of each call.
 * (the results presented on ICCD paper are running this method with NULL for the memory pool).
 * The method returns 0 if a full decomposition was found and a negative value otherwise.
 */
This method implements the paper proposed by V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis", presented at ICCD 2015.
pTruth: pointer for the truth table representing the target function.
nVarsInit: the number of variables of the truth table of the target function.
pRes: pointer for storing the resulting decomposition, whenever a decomposition can be found.
pool: NULL or a pointer for with a capacity of storing 3*nVars truth-tables. IF NULL, the function will allocate and free the memory of each call.
(the results presented on ICCD paper are running this method with NULL for the memory pool).
The method returns 0 if a full decomposition was found and a negative value otherwise.
This method implements the paper proposed by V . Callegaro F . S . Marranghello M . G . A . Martins R . P . Ribas and A . I . Reis entitled " Bottom - up disjoint - support decomposition based on cofactor and boolean difference analysis " presented at ICCD 2015 . pTruth : pointer for the truth table representing the target function . nVarsInit : the number of variables of the truth table of the target function . pRes : pointer for storing the resulting decomposition whenever a decomposition can be found . pool : NULL or a pointer for with a capacity of storing 3 * nVars truth - tables . IF NULL the function will allocate and free the memory of each call . ( the results presented on ICCD paper are running this method with NULL for the memory pool ) . The method returns 0 if a full decomposition was found and a negative value otherwise .
extern int Dsc_Decompose(word * pTruth, const int nVarsInit, char * const pRes, word *pool) {
    const int TRUTH_WORDS = Abc_TtWordNum(nVarsInit);
    const int NEED_POOL_ALLOC = (pool == NULL);
    Dsc_node_t nodes[DSC_MAX_VAR];
    Dsc_node_t *newNodes[DSC_MAX_VAR];
    Dsc_node_t *oldNodes[DSC_MAX_VAR];
    Dsc_node_t freeNodes[DSC_MAX_VAR]; 
    int f = 0; 
    int o = 0; 
    int n = 0; 
    pRes[0] = '\0';
    pRes[1] = '\0';
    if (NEED_POOL_ALLOC)
        pool = ABC_ALLOC(word, 3 * TRUTH_WORDS * nVarsInit);
    {
        word *pNextTruth = pool;
        int iVar;
        for (iVar = 0; iVar < nVarsInit; iVar++) {
            Abc_TtCofactor0p(pNextTruth, pTruth, TRUTH_WORDS, iVar);
            if (!Abc_TtEqual(pNextTruth, pTruth, TRUTH_WORDS)) {
                Dsc_node_t *node = &nodes[iVar];
                node->pNegCof = pNextTruth;
                pNextTruth += TRUTH_WORDS;
                node->pPosCof = pNextTruth;
                Abc_TtCofactor1p(node->pPosCof, pTruth, TRUTH_WORDS, iVar);
                pNextTruth += TRUTH_WORDS;
                node->pBoolDiff = pNextTruth;
                Abc_TtXor(node->pBoolDiff, node->pNegCof, node->pPosCof, TRUTH_WORDS, 0);
                pNextTruth += TRUTH_WORDS;
                node->on[0] = 1; node->on[1] = (iVar << 1) | 1u; 
                node->off[0] = 1; node->off[1] = iVar << 1;
                node->exp[0] = 'a'+iVar; 
                node->exp[1] = '\0';
                newNodes[n++] = node;
            }
        }
    }
    if (n == 0) {
        if (NEED_POOL_ALLOC)
            ABC_FREE(pool);
        if (Abc_TtIsConst0(pTruth, TRUTH_WORDS)) {
            { if ( pRes ) pRes[0] = '0', pRes[1] = '\0'; }
            return 0;
        } else if (Abc_TtIsConst1(pTruth, TRUTH_WORDS)) {
            { if ( pRes ) pRes[0] = '1', pRes[1] = '\0'; }
            return 0;
        } else {
            Abc_Print(-1, "ERROR. No variable in the support of f, but f isn't constant!\n");
            return -1;
        }
    }
    while (n > 0) {
        int tempN = 0;
        int i, j, iPolarity, jPolarity;
        Dsc_node_t *ni, *nj, *newNode = NULL;
        for (i = 0; i < n; i++) {
            ni = newNodes[i];
            newNode = NULL;
            j = 0;
            while (j < o) {
                nj = oldNodes[j];
                if (dsc_and_test(ni, nj, TRUTH_WORDS, &iPolarity, &jPolarity)) {
                    newNode = &freeNodes[f++];
                    dsc_and_group(newNode, ni, iPolarity, nj, jPolarity, nVarsInit, TRUTH_WORDS);
                }
                if ((newNode == NULL)  && (dsc_xor_test(ni, nj, TRUTH_WORDS))) {
                    newNode = &freeNodes[f++];
                    dsc_xor_group(newNode, ni, nj, nVarsInit, TRUTH_WORDS);
                }
                if (newNode != NULL) {
                    oldNodes[j] = oldNodes[--o];
                    break;
                } else {
                    j++;
                }
            }
            if (newNode != NULL) {
                newNodes[tempN++] = newNode;
            } else {
                oldNodes[o++] = ni;
            }
        }
        n = tempN;
    }
    if (o == 1) {
        Dsc_node_t * solution = oldNodes[0];
        if (Abc_TtIsConst0(solution->pNegCof, TRUTH_WORDS) && Abc_TtIsConst1(solution->pPosCof, TRUTH_WORDS)) {
            if ( pRes )
                strcpy( pRes, solution->exp);
            if (NEED_POOL_ALLOC)
                ABC_FREE(pool);
            return 0;
        } else if (Abc_TtIsConst1(solution->pNegCof, TRUTH_WORDS) && Abc_TtIsConst0(solution->pPosCof, TRUTH_WORDS)) {
            if ( pRes ) {
                pRes[0] = '!';
                strcpy( &pRes[1], solution->exp);
            }
            if (NEED_POOL_ALLOC)
                ABC_FREE(pool);
            return 0;
        } else {
            printf("DSC ERROR: Final DSC node found, but differs from target function.\n");
            if (NEED_POOL_ALLOC)
                ABC_FREE(pool);
            return -1;
        }
    }
    if (NEED_POOL_ALLOC)
        ABC_FREE(pool);
    return -1;
}
extern int Dsc_Decompose ( word * pTruth , const int nVarsInit , char * const pRes , word * pool ) { const int TRUTH_WORDS = Abc_TtWordNum ( nVarsInit ) ; const int NEED_POOL_ALLOC = ( pool == NULL ) ; Dsc_node_t nodes [ DSC_MAX_VAR ] ; Dsc_node_t * newNodes [ DSC_MAX_VAR ] ; Dsc_node_t * oldNodes [ DSC_MAX_VAR ] ; Dsc_node_t freeNodes [ DSC_MAX_VAR ] ; int f = 0 ; int o = 0 ; int n = 0 ; pRes [ 0 ] = ' \0 ' ; pRes [ 1 ] = ' \0 ' ; if ( NEED_POOL_ALLOC ) pool = ABC_ALLOC ( word , 3 * TRUTH_WORDS * nVarsInit ) ; { word * pNextTruth = pool ; int iVar ; for ( iVar = 0 ; iVar < nVarsInit ; iVar ++ ) { Abc_TtCofactor0p ( pNextTruth , pTruth , TRUTH_WORDS , iVar ) ; if ( ! Abc_TtEqual ( pNextTruth , pTruth , TRUTH_WORDS ) ) { Dsc_node_t * node = & nodes [ iVar ] ; node -> pNegCof = pNextTruth ; pNextTruth += TRUTH_WORDS ; node -> pPosCof = pNextTruth ; Abc_TtCofactor1p ( node -> pPosCof , pTruth , TRUTH_WORDS , iVar ) ; pNextTruth += TRUTH_WORDS ; node -> pBoolDiff = pNextTruth ; Abc_TtXor ( node -> pBoolDiff , node -> pNegCof , node -> pPosCof , TRUTH_WORDS , 0 ) ; pNextTruth += TRUTH_WORDS ; node -> on [ 0 ] = 1 ; node -> on [ 1 ] = ( iVar << 1 ) | 1u ; node -> off [ 0 ] = 1 ; node -> off [ 1 ] = iVar << 1 ; node -> exp [ 0 ] = ' ' + iVar ; node -> exp [ 1 ] = ' \0 ' ; newNodes [ n ++ ] = node ; } } } if ( n == 0 ) { if ( NEED_POOL_ALLOC ) ABC_FREE ( pool ) ; if ( Abc_TtIsConst0 ( pTruth , TRUTH_WORDS ) ) { { if ( pRes ) pRes [ 0 ] = ' ' , pRes [ 1 ] = ' \0 ' ; } return 0 ; } else if ( Abc_TtIsConst1 ( pTruth , TRUTH_WORDS ) ) { { if ( pRes ) pRes [ 0 ] = ' ' , pRes [ 1 ] = ' \0 ' ; } return 0 ; } else { Abc_Print ( -1 , " \n " ) ; return -1 ; } } while ( n > 0 ) { int tempN = 0 ; int i , j , iPolarity , jPolarity ; Dsc_node_t * ni , * nj , * newNode = NULL ; for ( i = 0 ; i < n ; i ++ ) { ni = newNodes [ i ] ; newNode = NULL ; j = 0 ; while ( j < o ) { nj = oldNodes [ j ] ; if ( dsc_and_test ( ni , nj , TRUTH_WORDS , & iPolarity , & jPolarity ) ) { newNode = & freeNodes [ f ++ ] ; dsc_and_group ( newNode , ni , iPolarity , nj , jPolarity , nVarsInit , TRUTH_WORDS ) ; } if ( ( newNode == NULL ) && ( dsc_xor_test ( ni , nj , TRUTH_WORDS ) ) ) { newNode = & freeNodes [ f ++ ] ; dsc_xor_group ( newNode , ni , nj , nVarsInit , TRUTH_WORDS ) ; } if ( newNode != NULL ) { oldNodes [ j ] = oldNodes [ -- o ] ; break ; } else { j ++ ; } } if ( newNode != NULL ) { newNodes [ tempN ++ ] = newNode ; } else { oldNodes [ o ++ ] = ni ; } } n = tempN ; } if ( o == 1 ) { Dsc_node_t * solution = oldNodes [ 0 ] ; if ( Abc_TtIsConst0 ( solution -> pNegCof , TRUTH_WORDS ) && Abc_TtIsConst1 ( solution -> pPosCof , TRUTH_WORDS ) ) { if ( pRes ) strcpy ( pRes , solution -> exp ) ; if ( NEED_POOL_ALLOC ) ABC_FREE ( pool ) ; return 0 ; } else if ( Abc_TtIsConst1 ( solution -> pNegCof , TRUTH_WORDS ) && Abc_TtIsConst0 ( solution -> pPosCof , TRUTH_WORDS ) ) { if ( pRes ) { pRes [ 0 ] = ' ' ; strcpy ( & pRes [ 1 ] , solution -> exp ) ; } if ( NEED_POOL_ALLOC ) ABC_FREE ( pool ) ; return 0 ; } else { printf ( " \n " ) ; if ( NEED_POOL_ALLOC ) ABC_FREE ( pool ) ; return -1 ; } } if ( NEED_POOL_ALLOC ) ABC_FREE ( pool ) ; return -1 ; }
This method implements the paper proposed by V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
 entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis", presented at ICCD 2015.
 pTruth: pointer for the truth table representing the target function.
This method implements the paper proposed by V . Callegaro F . S . Marranghello M . G . A . Martins R . P . Ribas and A . I . Reis entitled " Bottom - up disjoint - support decomposition based on cofactor and boolean difference analysis " presented at ICCD 2015 . pTruth : pointer for the truth table representing the target function .
// N is the maximum number of possible groups. // f represent the next free position in the freeNodes array // o stands for the number of already tested nodes // n will represent the number of current nodes (i.e. support) // block for the node data allocation // pointer for the next free truth word // negative cofactor // dont care test // increment next truth pointer // positive cofactor // increment next truth pointer // boolean difference // increment next truth pointer // define on spec - // lit = i*2+1, when polarity=true // define off spec // lit=i*2 otherwise // store the node expression // TODO fix the variable names // add the node to the newNodes array //const int initialSupport = n; // XOR test // Direct solution found // Complementary solution found