diff options
Diffstat (limited to 'abc70930/src/sat/fraig/fraigUtil.c')
| -rw-r--r-- | abc70930/src/sat/fraig/fraigUtil.c | 1034 |
1 files changed, 1034 insertions, 0 deletions
diff --git a/abc70930/src/sat/fraig/fraigUtil.c b/abc70930/src/sat/fraig/fraigUtil.c new file mode 100644 index 00000000..342a7111 --- /dev/null +++ b/abc70930/src/sat/fraig/fraigUtil.c @@ -0,0 +1,1034 @@ +/**CFile**************************************************************** + + FileName [fraigUtil.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Various utilities.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - October 1, 2004] + + Revision [$Id: fraigUtil.c,v 1.15 2005/07/08 01:01:34 alanmi Exp $] + +***********************************************************************/ + +#include "fraigInt.h" +#include <limits.h> + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int bit_count[256] = { + 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 +}; + +static void Fraig_Dfs_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vNodes, int fEquiv ); +static int Fraig_CheckTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_Node_t * pOld ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes the DFS ordering of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv ) +{ + Fraig_NodeVec_t * vNodes; + int i; + pMan->nTravIds++; + vNodes = Fraig_NodeVecAlloc( 100 ); + for ( i = 0; i < pMan->vOutputs->nSize; i++ ) + Fraig_Dfs_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), vNodes, fEquiv ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Computes the DFS ordering of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_DfsOne( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fEquiv ) +{ + Fraig_NodeVec_t * vNodes; + pMan->nTravIds++; + vNodes = Fraig_NodeVecAlloc( 100 ); + Fraig_Dfs_rec( pMan, Fraig_Regular(pNode), vNodes, fEquiv ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Computes the DFS ordering of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_DfsNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppNodes, int nNodes, int fEquiv ) +{ + Fraig_NodeVec_t * vNodes; + int i; + pMan->nTravIds++; + vNodes = Fraig_NodeVecAlloc( 100 ); + for ( i = 0; i < nNodes; i++ ) + Fraig_Dfs_rec( pMan, Fraig_Regular(ppNodes[i]), vNodes, fEquiv ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Recursively computes the DFS ordering of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_Dfs_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vNodes, int fEquiv ) +{ + assert( !Fraig_IsComplement(pNode) ); + // skip the visited node + if ( pNode->TravId == pMan->nTravIds ) + return; + pNode->TravId = pMan->nTravIds; + // visit the transitive fanin + if ( Fraig_NodeIsAnd(pNode) ) + { + Fraig_Dfs_rec( pMan, Fraig_Regular(pNode->p1), vNodes, fEquiv ); + Fraig_Dfs_rec( pMan, Fraig_Regular(pNode->p2), vNodes, fEquiv ); + } + if ( fEquiv && pNode->pNextE ) + Fraig_Dfs_rec( pMan, pNode->pNextE, vNodes, fEquiv ); + // save the node + Fraig_NodeVecPush( vNodes, pNode ); +} + +/**Function************************************************************* + + Synopsis [Computes the DFS ordering of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_CountNodes( Fraig_Man_t * pMan, int fEquiv ) +{ + Fraig_NodeVec_t * vNodes; + int RetValue; + vNodes = Fraig_Dfs( pMan, fEquiv ); + RetValue = vNodes->nSize; + Fraig_NodeVecFree( vNodes ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + assert( !Fraig_IsComplement(pOld) ); + assert( !Fraig_IsComplement(pNew) ); + pMan->nTravIds++; + return Fraig_CheckTfi_rec( pMan, pNew, pOld ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_CheckTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_Node_t * pOld ) +{ + // check the trivial cases + if ( pNode == NULL ) + return 0; + if ( pNode->Num < pOld->Num && !pMan->fChoicing ) + return 0; + if ( pNode == pOld ) + return 1; + // skip the visited node + if ( pNode->TravId == pMan->nTravIds ) + return 0; + pNode->TravId = pMan->nTravIds; + // check the children + if ( Fraig_CheckTfi_rec( pMan, Fraig_Regular(pNode->p1), pOld ) ) + return 1; + if ( Fraig_CheckTfi_rec( pMan, Fraig_Regular(pNode->p2), pOld ) ) + return 1; + // check equivalent nodes + return Fraig_CheckTfi_rec( pMan, pNode->pNextE, pOld ); +} + + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_CheckTfi2( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + Fraig_NodeVec_t * vNodes; + int RetValue; + vNodes = Fraig_DfsOne( pMan, pNew, 1 ); + RetValue = (pOld->TravId == pMan->nTravIds); + Fraig_NodeVecFree( vNodes ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Sets the number of fanouts (none, one, or many).] + + Description [This procedure collects the nodes reachable from + the POs of the AIG and sets the type of fanout counter (none, one, + or many) for each node. This procedure is useful to determine + fanout-free cones of AND-nodes, which is helpful for rebalancing + the AIG (see procedure Fraig_ManRebalance, or something like that).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManMarkRealFanouts( Fraig_Man_t * p ) +{ + Fraig_NodeVec_t * vNodes; + Fraig_Node_t * pNodeR; + int i; + // collect the nodes reachable + vNodes = Fraig_Dfs( p, 0 ); + // clean the fanouts field + for ( i = 0; i < vNodes->nSize; i++ ) + { + vNodes->pArray[i]->nFanouts = 0; + vNodes->pArray[i]->pData0 = NULL; + } + // mark reachable nodes by setting the two-bit counter pNode->nFans + for ( i = 0; i < vNodes->nSize; i++ ) + { + pNodeR = Fraig_Regular(vNodes->pArray[i]->p1); + if ( pNodeR && ++pNodeR->nFanouts == 3 ) + pNodeR->nFanouts = 2; + pNodeR = Fraig_Regular(vNodes->pArray[i]->p2); + if ( pNodeR && ++pNodeR->nFanouts == 3 ) + pNodeR->nFanouts = 2; + } + Fraig_NodeVecFree( vNodes ); +} + +/**Function************************************************************* + + Synopsis [Creates the constant 1 node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_BitStringCountOnes( unsigned * pString, int nWords ) +{ + unsigned char * pSuppBytes = (unsigned char *)pString; + int i, nOnes, nBytes = sizeof(unsigned) * nWords; + // count the number of ones in the simulation vector + for ( i = nOnes = 0; i < nBytes; i++ ) + nOnes += bit_count[pSuppBytes[i]]; + return nOnes; +} + +/**Function************************************************************* + + Synopsis [Verify one useful property.] + + Description [This procedure verifies one useful property. After + the FRAIG construction with choice nodes is over, each primary node + should have fanins that are primary nodes. The primary nodes is the + one that does not have pNode->pRepr set to point to another node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManCheckConsistency( Fraig_Man_t * p ) +{ + Fraig_Node_t * pNode; + Fraig_NodeVec_t * pVec; + int i; + pVec = Fraig_Dfs( p, 0 ); + for ( i = 0; i < pVec->nSize; i++ ) + { + pNode = pVec->pArray[i]; + if ( Fraig_NodeIsVar(pNode) ) + { + if ( pNode->pRepr ) + printf( "Primary input %d is a secondary node.\n", pNode->Num ); + } + else if ( Fraig_NodeIsConst(pNode) ) + { + if ( pNode->pRepr ) + printf( "Constant 1 %d is a secondary node.\n", pNode->Num ); + } + else + { + if ( pNode->pRepr ) + printf( "Internal node %d is a secondary node.\n", pNode->Num ); + if ( Fraig_Regular(pNode->p1)->pRepr ) + printf( "Internal node %d has first fanin %d that is a secondary node.\n", + pNode->Num, Fraig_Regular(pNode->p1)->Num ); + if ( Fraig_Regular(pNode->p2)->pRepr ) + printf( "Internal node %d has second fanin %d that is a secondary node.\n", + pNode->Num, Fraig_Regular(pNode->p2)->Num ); + } + } + Fraig_NodeVecFree( pVec ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Prints the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_PrintNode( Fraig_Man_t * p, Fraig_Node_t * pNode ) +{ + Fraig_NodeVec_t * vNodes; + Fraig_Node_t * pTemp; + int fCompl1, fCompl2, i; + + vNodes = Fraig_DfsOne( p, pNode, 0 ); + for ( i = 0; i < vNodes->nSize; i++ ) + { + pTemp = vNodes->pArray[i]; + if ( Fraig_NodeIsVar(pTemp) ) + { + printf( "%3d : PI ", pTemp->Num ); + Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimR, 20 ); + printf( " " ); + Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimD, 20 ); + printf( " %d\n", pTemp->fInv ); + continue; + } + + fCompl1 = Fraig_IsComplement(pTemp->p1); + fCompl2 = Fraig_IsComplement(pTemp->p2); + printf( "%3d : %c%3d %c%3d ", pTemp->Num, + (fCompl1? '-':'+'), Fraig_Regular(pTemp->p1)->Num, + (fCompl2? '-':'+'), Fraig_Regular(pTemp->p2)->Num ); + Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimR, 20 ); + printf( " " ); + Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimD, 20 ); + printf( " %d\n", pTemp->fInv ); + } + Fraig_NodeVecFree( vNodes ); +} + +/**Function************************************************************* + + Synopsis [Prints the bit string.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_PrintBinary( FILE * pFile, unsigned * pSign, int nBits ) +{ + int Remainder, nWords; + int w, i; + + Remainder = (nBits%(sizeof(unsigned)*8)); + nWords = (nBits/(sizeof(unsigned)*8)) + (Remainder>0); + + for ( w = nWords-1; w >= 0; w-- ) + for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- ) + fprintf( pFile, "%c", '0' + (int)((pSign[w] & (1<<i)) > 0) ); + +// fprintf( pFile, "\n" ); +} + +/**Function************************************************************* + + Synopsis [Sets up the mask.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_GetMaxLevel( Fraig_Man_t * pMan ) +{ + int nLevelMax, i; + nLevelMax = 0; + for ( i = 0; i < pMan->vOutputs->nSize; i++ ) + nLevelMax = nLevelMax > Fraig_Regular(pMan->vOutputs->pArray[i])->Level? + nLevelMax : Fraig_Regular(pMan->vOutputs->pArray[i])->Level; + return nLevelMax; +} + +/**Function************************************************************* + + Synopsis [Analyses choice nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_MappingUpdateLevel_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fMaximum ) +{ + Fraig_Node_t * pTemp; + int Level1, Level2, LevelE; + assert( !Fraig_IsComplement(pNode) ); + if ( !Fraig_NodeIsAnd(pNode) ) + return pNode->Level; + // skip the visited node + if ( pNode->TravId == pMan->nTravIds ) + return pNode->Level; + pNode->TravId = pMan->nTravIds; + // compute levels of the children nodes + Level1 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p1), fMaximum ); + Level2 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p2), fMaximum ); + pNode->Level = 1 + FRAIG_MAX( Level1, Level2 ); + if ( pNode->pNextE ) + { + LevelE = Fraig_MappingUpdateLevel_rec( pMan, pNode->pNextE, fMaximum ); + if ( fMaximum ) + { + if ( pNode->Level < LevelE ) + pNode->Level = LevelE; + } + else + { + if ( pNode->Level > LevelE ) + pNode->Level = LevelE; + } + // set the level of all equivalent nodes to be the same minimum + if ( pNode->pRepr == NULL ) // the primary node + for ( pTemp = pNode->pNextE; pTemp; pTemp = pTemp->pNextE ) + pTemp->Level = pNode->Level; + } + return pNode->Level; +} + +/**Function************************************************************* + + Synopsis [Resets the levels of the nodes in the choice graph.] + + Description [Makes the level of the choice nodes to be equal to the + maximum of the level of the nodes in the equivalence class. This way + sorting by level leads to the reverse topological order, which is + needed for the required time computation.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_MappingSetChoiceLevels( Fraig_Man_t * pMan, int fMaximum ) +{ + int i; + pMan->nTravIds++; + for ( i = 0; i < pMan->vOutputs->nSize; i++ ) + Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), fMaximum ); +} + +/**Function************************************************************* + + Synopsis [Reports statistics on choice nodes.] + + Description [The number of choice nodes is the number of primary nodes, + which has pNextE set to a pointer. The number of choices is the number + of entries in the equivalent-node lists of the primary nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManReportChoices( Fraig_Man_t * pMan ) +{ + Fraig_Node_t * pNode, * pTemp; + int nChoiceNodes, nChoices; + int i, LevelMax1, LevelMax2; + + // report the number of levels + LevelMax1 = Fraig_GetMaxLevel( pMan ); + Fraig_MappingSetChoiceLevels( pMan, 0 ); + LevelMax2 = Fraig_GetMaxLevel( pMan ); + + // report statistics about choices + nChoiceNodes = nChoices = 0; + for ( i = 0; i < pMan->vNodes->nSize; i++ ) + { + pNode = pMan->vNodes->pArray[i]; + if ( pNode->pRepr == NULL && pNode->pNextE != NULL ) + { // this is a choice node = the primary node that has equivalent nodes + nChoiceNodes++; + for ( pTemp = pNode; pTemp; pTemp = pTemp->pNextE ) + nChoices++; + } + } + printf( "Maximum level: Original = %d. Reduced due to choices = %d.\n", LevelMax1, LevelMax2 ); + printf( "Choice stats: Choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node is the root of EXOR/NEXOR gate.] + + Description [The node can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsExorType( Fraig_Node_t * pNode ) +{ + Fraig_Node_t * pNode1, * pNode2; + // make the node regular (it does not matter for EXOR/NEXOR) + pNode = Fraig_Regular(pNode); + // if the node or its children are not ANDs or not compl, this cannot be EXOR type + if ( !Fraig_NodeIsAnd(pNode) ) + return 0; + if ( !Fraig_NodeIsAnd(pNode->p1) || !Fraig_IsComplement(pNode->p1) ) + return 0; + if ( !Fraig_NodeIsAnd(pNode->p2) || !Fraig_IsComplement(pNode->p2) ) + return 0; + + // get children + pNode1 = Fraig_Regular(pNode->p1); + pNode2 = Fraig_Regular(pNode->p2); + assert( pNode1->Num < pNode2->Num ); + + // compare grandchildren + return pNode1->p1 == Fraig_Not(pNode2->p1) && pNode1->p2 == Fraig_Not(pNode2->p2); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] + + Description [The node can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsMuxType( Fraig_Node_t * pNode ) +{ + Fraig_Node_t * pNode1, * pNode2; + + // make the node regular (it does not matter for EXOR/NEXOR) + pNode = Fraig_Regular(pNode); + // if the node or its children are not ANDs or not compl, this cannot be EXOR type + if ( !Fraig_NodeIsAnd(pNode) ) + return 0; + if ( !Fraig_NodeIsAnd(pNode->p1) || !Fraig_IsComplement(pNode->p1) ) + return 0; + if ( !Fraig_NodeIsAnd(pNode->p2) || !Fraig_IsComplement(pNode->p2) ) + return 0; + + // get children + pNode1 = Fraig_Regular(pNode->p1); + pNode2 = Fraig_Regular(pNode->p2); + assert( pNode1->Num < pNode2->Num ); + + // compare grandchildren + // node is an EXOR/NEXOR + if ( pNode1->p1 == Fraig_Not(pNode2->p1) && pNode1->p2 == Fraig_Not(pNode2->p2) ) + return 1; + + // otherwise the node is MUX iff it has a pair of equal grandchildren + return pNode1->p1 == Fraig_Not(pNode2->p1) || + pNode1->p1 == Fraig_Not(pNode2->p2) || + pNode1->p2 == Fraig_Not(pNode2->p1) || + pNode1->p2 == Fraig_Not(pNode2->p2); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node is EXOR, 0 if it is NEXOR.] + + Description [The node should be EXOR type and not complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsExor( Fraig_Node_t * pNode ) +{ + Fraig_Node_t * pNode1; + assert( !Fraig_IsComplement(pNode) ); + assert( Fraig_NodeIsExorType(pNode) ); + assert( Fraig_IsComplement(pNode->p1) ); + // get children + pNode1 = Fraig_Regular(pNode->p1); + return Fraig_IsComplement(pNode1->p1) == Fraig_IsComplement(pNode1->p2); +} + +/**Function************************************************************* + + Synopsis [Recognizes what nodes are control and data inputs of a MUX.] + + Description [If the node is a MUX, returns the control variable C. + Assigns nodes T and E to be the then and else variables of the MUX. + Node C is never complemented. Nodes T and E can be complemented. + This function also recognizes EXOR/NEXOR gates as MUXes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Fraig_NodeRecognizeMux( Fraig_Node_t * pNode, Fraig_Node_t ** ppNodeT, Fraig_Node_t ** ppNodeE ) +{ + Fraig_Node_t * pNode1, * pNode2; + assert( !Fraig_IsComplement(pNode) ); + assert( Fraig_NodeIsMuxType(pNode) ); + // get children + pNode1 = Fraig_Regular(pNode->p1); + pNode2 = Fraig_Regular(pNode->p2); + // find the control variable + if ( pNode1->p1 == Fraig_Not(pNode2->p1) ) + { + if ( Fraig_IsComplement(pNode1->p1) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Fraig_Not(pNode2->p2); + *ppNodeE = Fraig_Not(pNode1->p2); + return pNode2->p1; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Fraig_Not(pNode1->p2); + *ppNodeE = Fraig_Not(pNode2->p2); + return pNode1->p1; + } + } + else if ( pNode1->p1 == Fraig_Not(pNode2->p2) ) + { + if ( Fraig_IsComplement(pNode1->p1) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Fraig_Not(pNode2->p1); + *ppNodeE = Fraig_Not(pNode1->p2); + return pNode2->p2; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Fraig_Not(pNode1->p2); + *ppNodeE = Fraig_Not(pNode2->p1); + return pNode1->p1; + } + } + else if ( pNode1->p2 == Fraig_Not(pNode2->p1) ) + { + if ( Fraig_IsComplement(pNode1->p2) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Fraig_Not(pNode2->p2); + *ppNodeE = Fraig_Not(pNode1->p1); + return pNode2->p1; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Fraig_Not(pNode1->p1); + *ppNodeE = Fraig_Not(pNode2->p2); + return pNode1->p2; + } + } + else if ( pNode1->p2 == Fraig_Not(pNode2->p2) ) + { + if ( Fraig_IsComplement(pNode1->p2) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Fraig_Not(pNode2->p1); + *ppNodeE = Fraig_Not(pNode1->p1); + return pNode2->p2; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Fraig_Not(pNode1->p1); + *ppNodeE = Fraig_Not(pNode2->p1); + return pNode1->p2; + } + } + assert( 0 ); // this is not MUX + return NULL; +} + +/**Function************************************************************* + + Synopsis [Counts the number of EXOR type nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManCountExors( Fraig_Man_t * pMan ) +{ + int i, nExors; + nExors = 0; + for ( i = 0; i < pMan->vNodes->nSize; i++ ) + nExors += Fraig_NodeIsExorType( pMan->vNodes->pArray[i] ); + return nExors; + +} + +/**Function************************************************************* + + Synopsis [Counts the number of EXOR type nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManCountMuxes( Fraig_Man_t * pMan ) +{ + int i, nMuxes; + nMuxes = 0; + for ( i = 0; i < pMan->vNodes->nSize; i++ ) + nMuxes += Fraig_NodeIsMuxType( pMan->vNodes->pArray[i] ); + return nMuxes; + +} + +/**Function************************************************************* + + Synopsis [Returns 1 if siminfo of Node1 is contained in siminfo of Node2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeSimsContained( Fraig_Man_t * pMan, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 ) +{ + unsigned * pUnsigned1, * pUnsigned2; + int i; + + // compare random siminfo + pUnsigned1 = pNode1->puSimR; + pUnsigned2 = pNode2->puSimR; + for ( i = 0; i < pMan->nWordsRand; i++ ) + if ( pUnsigned1[i] & ~pUnsigned2[i] ) + return 0; + + // compare systematic siminfo + pUnsigned1 = pNode1->puSimD; + pUnsigned2 = pNode2->puSimD; + for ( i = 0; i < pMan->iWordStart; i++ ) + if ( pUnsigned1[i] & ~pUnsigned2[i] ) + return 0; + + return 1; +} + +/**Function************************************************************* + + Synopsis [Count the number of PI variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_CountPis( Fraig_Man_t * p, Msat_IntVec_t * vVarNums ) +{ + int * pVars, nVars, i, Counter; + + nVars = Msat_IntVecReadSize(vVarNums); + pVars = Msat_IntVecReadArray(vVarNums); + Counter = 0; + for ( i = 0; i < nVars; i++ ) + Counter += Fraig_NodeIsVar( p->vNodes->pArray[pVars[i]] ); + return Counter; +} + + + +/**Function************************************************************* + + Synopsis [Counts the number of EXOR type nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManPrintRefs( Fraig_Man_t * pMan ) +{ + Fraig_NodeVec_t * vPivots; + Fraig_Node_t * pNode, * pNode2; + int i, k, Counter, nProved; + int clk; + + vPivots = Fraig_NodeVecAlloc( 1000 ); + for ( i = 0; i < pMan->vNodes->nSize; i++ ) + { + pNode = pMan->vNodes->pArray[i]; + + if ( pNode->nOnes == 0 || pNode->nOnes == (unsigned)pMan->nWordsRand * 32 ) + continue; + + if ( pNode->nRefs > 5 ) + { + Fraig_NodeVecPush( vPivots, pNode ); +// printf( "Node %6d : nRefs = %2d Level = %3d.\n", pNode->Num, pNode->nRefs, pNode->Level ); + } + } + printf( "Total nodes = %d. Referenced nodes = %d.\n", pMan->vNodes->nSize, vPivots->nSize ); + +clk = clock(); + // count implications + Counter = nProved = 0; + for ( i = 0; i < vPivots->nSize; i++ ) + for ( k = i+1; k < vPivots->nSize; k++ ) + { + pNode = vPivots->pArray[i]; + pNode2 = vPivots->pArray[k]; + if ( Fraig_NodeSimsContained( pMan, pNode, pNode2 ) ) + { + if ( Fraig_NodeIsImplication( pMan, pNode, pNode2, -1 ) ) + nProved++; + Counter++; + } + else if ( Fraig_NodeSimsContained( pMan, pNode2, pNode ) ) + { + if ( Fraig_NodeIsImplication( pMan, pNode2, pNode, -1 ) ) + nProved++; + Counter++; + } + } + printf( "Number of candidate pairs = %d. Proved = %d.\n", Counter, nProved ); +PRT( "Time", clock() - clk ); + return 0; +} + + +/**Function************************************************************* + + Synopsis [Checks if pNew exists among the implication fanins of pOld.] + + Description [If pNew is an implication fanin of pOld, returns 1. + If Fraig_Not(pNew) is an implication fanin of pOld, return -1. + Otherwise returns 0.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsInSupergate( Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + int RetValue1, RetValue2; + if ( Fraig_Regular(pOld) == Fraig_Regular(pNew) ) + return (pOld == pNew)? 1 : -1; + if ( Fraig_IsComplement(pOld) || Fraig_NodeIsVar(pOld) ) + return 0; + RetValue1 = Fraig_NodeIsInSupergate( pOld->p1, pNew ); + RetValue2 = Fraig_NodeIsInSupergate( pOld->p2, pNew ); + if ( RetValue1 == -1 || RetValue2 == -1 ) + return -1; + if ( RetValue1 == 1 || RetValue2 == 1 ) + return 1; + return 0; +} + + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_CollectSupergate_rec( Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper, int fFirst, int fStopAtMux ) +{ + // if the new node is complemented or a PI, another gate begins +// if ( Fraig_IsComplement(pNode) || Fraig_NodeIsVar(pNode) || Fraig_NodeIsMuxType(pNode) ) + if ( (!fFirst && Fraig_Regular(pNode)->nRefs > 1) || + Fraig_IsComplement(pNode) || Fraig_NodeIsVar(pNode) || + (fStopAtMux && Fraig_NodeIsMuxType(pNode)) ) + { + Fraig_NodeVecPushUnique( vSuper, pNode ); + return; + } + // go through the branches + Fraig_CollectSupergate_rec( pNode->p1, vSuper, 0, fStopAtMux ); + Fraig_CollectSupergate_rec( pNode->p2, vSuper, 0, fStopAtMux ); +} + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux ) +{ + Fraig_NodeVec_t * vSuper; + vSuper = Fraig_NodeVecAlloc( 8 ); + Fraig_CollectSupergate_rec( pNode, vSuper, 1, fStopAtMux ); + return vSuper; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManIncrementTravId( Fraig_Man_t * pMan ) +{ + pMan->nTravIds2++; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + pNode->TravId2 = pMan->nTravIds2; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + return pNode->TravId2 == pMan->nTravIds2; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + return pNode->TravId2 == pMan->nTravIds2 - 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |