From 52e5b91cbbfe587bae80984bb3672e4c1a70203c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 4 Dec 2006 08:01:00 -0800 Subject: Version abc61204 --- src/aig/ivy/ivyFactor.c | 833 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 833 insertions(+) create mode 100644 src/aig/ivy/ivyFactor.c (limited to 'src/aig/ivy') diff --git a/src/aig/ivy/ivyFactor.c b/src/aig/ivy/ivyFactor.c new file mode 100644 index 00000000..d8323931 --- /dev/null +++ b/src/aig/ivy/ivyFactor.c @@ -0,0 +1,833 @@ +/**CFile**************************************************************** + + FileName [ivyFactor.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Factoring the cover up to 16 inputs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyFactor.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" +#include "dec.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars ); +extern Dec_Edge_t Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars, Vec_Int_t * vSimple ); +extern Dec_Edge_t Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars ); +extern Dec_Edge_t Dec_Factor32TrivialCube( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits ); +extern Dec_Edge_t Dec_Factor32TrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr ); +extern Vec_Int_t * Dec_Factor32Divisor( Vec_Int_t * vCover, int nVars ); +extern void Dec_Factor32DivisorZeroKernel( Vec_Int_t * vCover, int nVars ); +extern int Dec_Factor32WorstLiteral( Vec_Int_t * vCover, int nVars ); + +extern Vec_Int_t * Mvc_CoverCommonCubeCover( Vec_Int_t * vCover ); + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Factors the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Dec_Factor32( Vec_Int_t * vCover, int nVars ) +{ + Dec_Graph_t * pFForm; + Dec_Edge_t eRoot; + + // check for trivial functions + if ( Vec_IntSize(vCover) == 0 ) + return Dec_GraphCreateConst0(); + if ( Vec_IntSize(vCover) == 1 && /* tautology */ ) + return Dec_GraphCreateConst1(); + + // perform CST + Mvc_CoverInverse( vCover ); // CST + // start the factored form + pFForm = Dec_GraphCreate( Abc_SopGetVarNum(pSop) ); + // factor the cover + eRoot = Dec_Factor32_rec( pFForm, vCover, nVars ); + // finalize the factored form + Dec_GraphSetRoot( pFForm, eRoot ); + // verify the factored form +// if ( !Dec_Factor32Verify( pSop, pFForm ) ) +// printf( "Verification has failed.\n" ); +// Mvc_CoverInverse( vCover ); // undo CST + return pFForm; +} + +/**Function************************************************************* + + Synopsis [Internal recursive factoring procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars ) +{ + Vec_Int_t * vDiv, * vQuo, * vRem, * vCom; + Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem; + Dec_Edge_t eNodeAnd, eNode; + + // make sure the cover contains some cubes + assert( Vec_IntSize(vCover) ); + + // get the divisor + vDiv = Dec_Factor32Divisor( vCover, nVars ); + if ( vDiv == NULL ) + return Dec_Factor32Trivial( pFForm, vCover, nVars ); + + // divide the cover by the divisor + Mvc_CoverDivideInternal( vCover, nVars, vDiv, &vQuo, &vRem ); + assert( Vec_IntSize(vQuo) ); + + Vec_IntFree( vDiv ); + Vec_IntFree( vRem ); + + // check the trivial case + if ( Vec_IntSize(vQuo) == 1 ) + { + eNode = Dec_Factor32LF_rec( pFForm, vCover, nVars, vQuo ); + Vec_IntFree( vQuo ); + return eNode; + } + + // make the quotient cube free + Mvc_CoverMakeCubeFree( vQuo ); + + // divide the cover by the quotient + Mvc_CoverDivideInternal( vCover, nVars, vQuo, &vDiv, &vRem ); + + // check the trivial case + if ( Mvc_CoverIsCubeFree( vDiv ) ) + { + eNodeDiv = Dec_Factor32_rec( pFForm, vDiv ); + eNodeQuo = Dec_Factor32_rec( pFForm, vQuo ); + Vec_IntFree( vDiv ); + Vec_IntFree( vQuo ); + eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo ); + if ( Vec_IntSize(vRem) == 0 ) + { + Vec_IntFree( vRem ); + return eNodeAnd; + } + else + { + eNodeRem = Dec_Factor32_rec( pFForm, vRem ); + Vec_IntFree( vRem ); + return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem ); + } + } + + // get the common cube + vCom = Mvc_CoverCommonCubeCover( vDiv ); + Vec_IntFree( vDiv ); + Vec_IntFree( vQuo ); + Vec_IntFree( vRem ); + + // solve the simple problem + eNode = Dec_Factor32LF_rec( pFForm, vCover, nVars, vCom ); + Vec_IntFree( vCom ); + return eNode; +} + + +/**Function************************************************************* + + Synopsis [Internal recursive factoring procedure for the leaf case.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars, Vec_Int_t * vSimple ) +{ + Dec_Man_t * pManDec = Abc_FrameReadManDec(); + Vec_Int_t * vEdgeLits = pManDec->vLits; + Vec_Int_t * vDiv, * vQuo, * vRem; + Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem; + Dec_Edge_t eNodeAnd; + + // get the most often occurring literal + vDiv = Mvc_CoverBestLiteralCover( vCover, nVars, vSimple ); + // divide the cover by the literal + Mvc_CoverDivideByLiteral( vCover, nVars, vDiv, &vQuo, &vRem ); + // get the node pointer for the literal + eNodeDiv = Dec_Factor32TrivialCube( pFForm, vDiv, Mvc_CoverReadCubeHead(vDiv), vEdgeLits ); + Vec_IntFree( vDiv ); + // factor the quotient and remainder + eNodeQuo = Dec_Factor32_rec( pFForm, vQuo ); + Vec_IntFree( vQuo ); + eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo ); + if ( Vec_IntSize(vRem) == 0 ) + { + Vec_IntFree( vRem ); + return eNodeAnd; + } + else + { + eNodeRem = Dec_Factor32_rec( pFForm, vRem ); + Vec_IntFree( vRem ); + return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem ); + } +} + + + +/**Function************************************************************* + + Synopsis [Factoring the cover, which has no algebraic divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars ) +{ + Dec_Man_t * pManDec = Abc_FrameReadManDec(); + Vec_Int_t * vEdgeCubes = pManDec->vCubes; + Vec_Int_t * vEdgeLits = pManDec->vLits; + Mvc_Manager_t * pMem = pManDec->pMvcMem; + Dec_Edge_t eNode; + Mvc_Cube_t * pCube; + int i; + // create the factored form for each cube + Vec_IntClear( vEdgeCubes ); + Mvc_CoverForEachCube( vCover, pCube ) + { + eNode = Dec_Factor32TrivialCube( pFForm, vCover, nVars, pCube, vEdgeLits ); + Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) ); + } + // balance the factored forms + return Dec_Factor32TrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeCubes->pArray, vEdgeCubes->nSize, 1 ); +} + +/**Function************************************************************* + + Synopsis [Factoring the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_Factor32TrivialCube( Dec_Graph_t * pFForm, Vec_Int_t * vCover, Mvc_Cube_t * pCube, int nVars, Vec_Int_t * vEdgeLits ) +{ + Dec_Edge_t eNode; + int iBit, Value; + // create the factored form for each literal + Vec_IntClear( vEdgeLits ); + Mvc_CubeForEachBit( vCover, pCube, iBit, Value ) + if ( Value ) + { + eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST + Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) ); + } + // balance the factored forms + return Dec_Factor32TrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 ); +} + +/**Function************************************************************* + + Synopsis [Create the well-balanced tree of nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_Factor32TrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr ) +{ + Dec_Edge_t eNode1, eNode2; + int nNodes1, nNodes2; + + if ( nNodes == 1 ) + return peNodes[0]; + + // split the nodes into two parts + nNodes1 = nNodes/2; + nNodes2 = nNodes - nNodes1; +// nNodes2 = nNodes/2; +// nNodes1 = nNodes - nNodes2; + + // recursively construct the tree for the parts + eNode1 = Dec_Factor32TrivialTree_rec( pFForm, peNodes, nNodes1, fNodeOr ); + eNode2 = Dec_Factor32TrivialTree_rec( pFForm, peNodes + nNodes1, nNodes2, fNodeOr ); + + if ( fNodeOr ) + return Dec_GraphAddNodeOr( pFForm, eNode1, eNode2 ); + else + return Dec_GraphAddNodeAnd( pFForm, eNode1, eNode2 ); +} + +/**Function************************************************************* + + Synopsis [Returns the quick divisor of the cover.] + + Description [Returns NULL, if there is not divisor other than + trivial.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Dec_Factor32Divisor( Vec_Int_t * vCover, int nVars ) +{ + Vec_Int_t * pKernel; + if ( Vec_IntSize(vCover) <= 1 ) + return NULL; + // allocate the literal array and count literals + if ( Mvc_CoverAnyLiteral( vCover, NULL ) == -1 ) + return NULL; + // duplicate the cover + pKernel = Mvc_CoverDup(vCover); + // perform the kerneling + Dec_Factor32DivisorZeroKernel( pKernel ); + assert( Vec_IntSize(pKernel) ); + return pKernel; +} + +/**Function************************************************************* + + Synopsis [Computes a level-zero kernel.] + + Description [Modifies the cover to contain one level-zero kernel.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dec_Factor32DivisorZeroKernel( Vec_Int_t * vCover, int nVars ) +{ + int iLit; + // find any literal that occurs at least two times +// iLit = Mvc_CoverAnyLiteral( vCover, NULL ); + iLit = Dec_Factor32WorstLiteral( vCover, NULL ); +// iLit = Mvc_CoverBestLiteral( vCover, NULL ); + if ( iLit == -1 ) + return; + // derive the cube-free quotient + Mvc_CoverDivideByLiteralQuo( vCover, iLit ); // the same cover + Mvc_CoverMakeCubeFree( vCover ); // the same cover + // call recursively + Dec_Factor32DivisorZeroKernel( vCover ); // the same cover +} + +/**Function************************************************************* + + Synopsis [Find the most often occurring literal.] + + Description [Find the most often occurring literal among those + that occur more than once.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dec_Factor32WorstLiteral( Vec_Int_t * vCover, int nVars ) +{ + Mvc_Cube_t * pCube; + int nWord, nBit; + int i, iMin, nLitsMin, nLitsCur; + int fUseFirst = 1; + + // go through each literal + iMin = -1; + nLitsMin = 1000000; + for ( i = 0; i < vCover->nBits; i++ ) + { + // get the word and bit of this literal + nWord = Mvc_CubeWhichWord(i); + nBit = Mvc_CubeWhichBit(i); + // go through all the cubes + nLitsCur = 0; + Mvc_CoverForEachCube( vCover, pCube ) + if ( pCube->pData[nWord] & (1< nLitsCur ) + { + nLitsMin = nLitsCur; + iMin = i; + } + } + else + { + if ( nLitsMin >= nLitsCur ) + { + nLitsMin = nLitsCur; + iMin = i; + } + } + } + + if ( nLitsMin < 1000000 ) + return iMin; + return -1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Mvc_CoverCommonCubeCover( Vec_Int_t * vCover ) +{ + Vec_Int_t * vRes; + unsigned uTemp, uCube; + int i; + uCube = ~(unsigned)0; + Vec_IntForEachEntry( vCover, uTemp, i ) + uCube &= uTemp; + vRes = Vec_IntAlloc( 1 ); + Vec_IntPush( vRes, uCube ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the support of cover2 is contained in the support of cover1.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mvc_CoverCheckSuppContainment( Vec_Int_t * vCover1, Vec_Int_t * vCover2 ) +{ + unsigned uTemp, uSupp1, uSupp2; + int i; + // set the supports + uSupp1 = 0; + Vec_IntForEachEntry( vCover1, uTemp, i ) + uSupp1 |= uTemp; + uSupp2 = 0; + Vec_IntForEachEntry( vCover2, uTemp, i ) + uSupp2 |= uTemp; + // return containment + return uSupp1 & !uSupp2; +// Mvc_CubeBitNotImpl( Result, vCover2->pMask, vCover1->pMask ); +// return !Result; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverDivide( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem ) +{ + // check the number of cubes + if ( Vec_IntSize( vCover ) < Vec_IntSize( vDiv ) ) + { + *pvQuo = NULL; + *pvRem = NULL; + return; + } + + // make sure that support of vCover contains that of vDiv + if ( !Mvc_CoverCheckSuppContainment( vCover, vDiv ) ) + { + *pvQuo = NULL; + *pvRem = NULL; + return; + } + + // perform the general division + Mvc_CoverDivideInternal( vCover, vDiv, pvQuo, pvRem ); +} + + +/**Function************************************************************* + + Synopsis [Merge the cubes inside the groups.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverDivideInternal( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem ) +{ + Vec_Int_t * vQuo, * vRem; + Mvc_Cube_t * pCubeC, * pCubeD, * pCubeCopy; + Mvc_Cube_t * pCube1, * pCube2; + int * pGroups, nGroups; // the cube groups + int nCubesC, nCubesD, nMerges, iCubeC, iCubeD, iMerge; + int fSkipG, GroupSize, g, c, RetValue; + int nCubes; + + // get cover sizes + nCubesD = Vec_IntSize( vDiv ); + nCubesC = Vec_IntSize( vCover ); + + // check trivial cases + if ( nCubesD == 1 ) + { + if ( Mvc_CoverIsOneLiteral( vDiv ) ) + Mvc_CoverDivideByLiteral( vCover, vDiv, pvQuo, pvRem ); + else + Mvc_CoverDivideByCube( vCover, vDiv, pvQuo, pvRem ); + return; + } + + // create the divisor and the remainder + vQuo = Mvc_CoverAlloc( vCover->pMem, vCover->nBits ); + vRem = Mvc_CoverAlloc( vCover->pMem, vCover->nBits ); + + // get the support of the divisor + Mvc_CoverAllocateMask( vDiv ); + Mvc_CoverSupport( vDiv, vDiv->pMask ); + + // sort the cubes of the divisor + Mvc_CoverSort( vDiv, NULL, Mvc_CubeCompareInt ); + // sort the cubes of the cover + Mvc_CoverSort( vCover, vDiv->pMask, Mvc_CubeCompareIntOutsideAndUnderMask ); + + // allocate storage for cube groups + pGroups = MEM_ALLOC( vCover->pMem, int, nCubesC + 1 ); + + // mask contains variables in the support of Div + // split the cubes into groups using the mask + Mvc_CoverList2Array( vCover ); + Mvc_CoverList2Array( vDiv ); + pGroups[0] = 0; + nGroups = 1; + for ( c = 1; c < nCubesC; c++ ) + { + // get the cubes + pCube1 = vCover->pCubes[c-1]; + pCube2 = vCover->pCubes[c ]; + // compare the cubes + Mvc_CubeBitEqualOutsideMask( RetValue, pCube1, pCube2, vDiv->pMask ); + if ( !RetValue ) + pGroups[nGroups++] = c; + } + // finish off the last group + pGroups[nGroups] = nCubesC; + + // consider each group separately and decide + // whether it can produce a quotient cube + nCubes = 0; + for ( g = 0; g < nGroups; g++ ) + { + // if the group has less than nCubesD cubes, + // there is no way it can produce the quotient cube + // copy the cubes to the remainder + GroupSize = pGroups[g+1] - pGroups[g]; + if ( GroupSize < nCubesD ) + { + for ( c = pGroups[g]; c < pGroups[g+1]; c++ ) + { + pCubeCopy = Mvc_CubeDup( vRem, vCover->pCubes[c] ); + Mvc_CoverAddCubeTail( vRem, pCubeCopy ); + nCubes++; + } + continue; + } + + // mark the cubes as those that should be added to the remainder + for ( c = pGroups[g]; c < pGroups[g+1]; c++ ) + Mvc_CubeSetSize( vCover->pCubes[c], 1 ); + + // go through the cubes in the group and at the same time + // go through the cubes in the divisor + iCubeD = 0; + iCubeC = 0; + pCubeD = vDiv->pCubes[iCubeD++]; + pCubeC = vCover->pCubes[pGroups[g]+iCubeC++]; + fSkipG = 0; + nMerges = 0; + + while ( 1 ) + { + // compare the topmost cubes in F and in D + RetValue = Mvc_CubeCompareIntUnderMask( pCubeC, pCubeD, vDiv->pMask ); + // cube are ordered in increasing order of their int value + if ( RetValue == -1 ) // pCubeC is above pCubeD + { // cube in C should be added to the remainder + // check that there is enough cubes in the group + if ( GroupSize - iCubeC < nCubesD - nMerges ) + { + fSkipG = 1; + break; + } + // get the next cube in the cover + pCubeC = vCover->pCubes[pGroups[g]+iCubeC++]; + continue; + } + if ( RetValue == 1 ) // pCubeD is above pCubeC + { // given cube in D does not have a corresponding cube in the cover + fSkipG = 1; + break; + } + // mark the cube as the one that should NOT be added to the remainder + Mvc_CubeSetSize( pCubeC, 0 ); + // remember this merged cube + iMerge = iCubeC-1; + nMerges++; + + // stop if we considered the last cube of the group + if ( iCubeD == nCubesD ) + break; + + // advance the cube of the divisor + assert( iCubeD < nCubesD ); + pCubeD = vDiv->pCubes[iCubeD++]; + + // advance the cube of the group + assert( pGroups[g]+iCubeC < nCubesC ); + pCubeC = vCover->pCubes[pGroups[g]+iCubeC++]; + } + + if ( fSkipG ) + { + // the group has failed, add all the cubes to the remainder + for ( c = pGroups[g]; c < pGroups[g+1]; c++ ) + { + pCubeCopy = Mvc_CubeDup( vRem, vCover->pCubes[c] ); + Mvc_CoverAddCubeTail( vRem, pCubeCopy ); + nCubes++; + } + continue; + } + + // the group has worked, add left-over cubes to the remainder + for ( c = pGroups[g]; c < pGroups[g+1]; c++ ) + { + pCubeC = vCover->pCubes[c]; + if ( Mvc_CubeReadSize(pCubeC) ) + { + pCubeCopy = Mvc_CubeDup( vRem, pCubeC ); + Mvc_CoverAddCubeTail( vRem, pCubeCopy ); + nCubes++; + } + } + + // create the quotient cube + pCube1 = Mvc_CubeAlloc( vQuo ); + Mvc_CubeBitSharp( pCube1, vCover->pCubes[pGroups[g]+iMerge], vDiv->pMask ); + // add the cube to the quotient + Mvc_CoverAddCubeTail( vQuo, pCube1 ); + nCubes += nCubesD; + } + assert( nCubes == nCubesC ); + + // deallocate the memory + MEM_FREE( vCover->pMem, int, nCubesC + 1, pGroups ); + + // return the results + *pvRem = vRem; + *pvQuo = vQuo; +// Mvc_CoverVerifyDivision( vCover, vDiv, vQuo, vRem ); +} + + +/**Function************************************************************* + + Synopsis [Divides the cover by a cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverDivideByCube( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem ) +{ + Vec_Int_t * vQuo, * vRem; + Mvc_Cube_t * pCubeC, * pCubeD, * pCubeCopy; + int ComvResult; + + // get the only cube of D + assert( Vec_IntSize(vDiv) == 1 ); + + // start the quotient and the remainder + vQuo = Mvc_CoverAlloc( vCover->pMem, vCover->nBits ); + vRem = Mvc_CoverAlloc( vCover->pMem, vCover->nBits ); + + // get the first and only cube of the divisor + pCubeD = Mvc_CoverReadCubeHead( vDiv ); + + // iterate through the cubes in the cover + Mvc_CoverForEachCube( vCover, pCubeC ) + { + // check the containment of literals from pCubeD in pCube + Mvc_Cube2BitNotImpl( ComvResult, pCubeD, pCubeC ); + if ( !ComvResult ) + { // this cube belongs to the quotient + // alloc the cube + pCubeCopy = Mvc_CubeAlloc( vQuo ); + // clean the support of D + Mvc_CubeBitSharp( pCubeCopy, pCubeC, pCubeD ); + // add the cube to the quotient + Mvc_CoverAddCubeTail( vQuo, pCubeCopy ); + } + else + { + // copy the cube + pCubeCopy = Mvc_CubeDup( vRem, pCubeC ); + // add the cube to the remainder + Mvc_CoverAddCubeTail( vRem, pCubeCopy ); + } + } + // return the results + *pvRem = vRem; + *pvQuo = vQuo; +} + +/**Function************************************************************* + + Synopsis [Divides the cover by a literal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverDivideByLiteral( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem ) +{ + Vec_Int_t * vQuo, * vRem; + Mvc_Cube_t * pCubeC, * pCubeCopy; + int iLit; + + // get the only cube of D + assert( Vec_IntSize(vDiv) == 1 ); + + // start the quotient and the remainder + vQuo = Mvc_CoverAlloc( vCover->pMem, vCover->nBits ); + vRem = Mvc_CoverAlloc( vCover->pMem, vCover->nBits ); + + // get the first and only literal in the divisor cube + iLit = Mvc_CoverFirstCubeFirstLit( vDiv ); + + // iterate through the cubes in the cover + Mvc_CoverForEachCube( vCover, pCubeC ) + { + // copy the cube + pCubeCopy = Mvc_CubeDup( vCover, pCubeC ); + // add the cube to the quotient or to the remainder depending on the literal + if ( Mvc_CubeBitValue( pCubeCopy, iLit ) ) + { // remove the literal + Mvc_CubeBitRemove( pCubeCopy, iLit ); + // add the cube ot the quotient + Mvc_CoverAddCubeTail( vQuo, pCubeCopy ); + } + else + { // add the cube ot the remainder + Mvc_CoverAddCubeTail( vRem, pCubeCopy ); + } + } + // return the results + *pvRem = vRem; + *pvQuo = vQuo; +} + + +/**Function************************************************************* + + Synopsis [Derives the quotient of division by literal.] + + Description [Reduces the cover to be the equal to the result of + division of the given cover by the literal.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverDivideByLiteralQuo( Vec_Int_t * vCover, int iLit ) +{ + Mvc_Cube_t * pCube, * pCube2, * pPrev; + // delete those cubes that do not have this literal + // remove this literal from other cubes + pPrev = NULL; + Mvc_CoverForEachCubeSafe( vCover, pCube, pCube2 ) + { + if ( Mvc_CubeBitValue( pCube, iLit ) == 0 ) + { // delete the cube from the cover + Mvc_CoverDeleteCube( vCover, pPrev, pCube ); + Mvc_CubeFree( vCover, pCube ); + // don't update the previous cube + } + else + { // delete this literal from the cube + Mvc_CubeBitRemove( pCube, iLit ); + // update the previous cube + pPrev = pCube; + } + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3