Version abc80130

1 files changed, 0 insertions, 572 deletions

diff --git a/src/aig/kit/kitSop.c b/src/aig/kit/kitSop.c
deleted file mode 100644
index 20ad0651..00000000
--- a/src/aig/kit/kitSop.c
+++ /dev/null
@@ -1,572 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [kitSop.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Computation kit.]
-
-  Synopsis    [Procedures involving SOPs.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - Dec 6, 2006.]
-
-  Revision    [$Id: kitSop.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "kit.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates SOP from the cube array.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Kit_SopCreate( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory )
-{
-    unsigned uCube;
-    int i;
-    // start the cover
-    cResult->nCubes = 0;
-    cResult->pCubes = Vec_IntFetch( vMemory, Vec_IntSize(vInput) );
-    // add the cubes
-    Vec_IntForEachEntry( vInput, uCube, i )
-        Kit_SopPushCube( cResult, uCube );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates SOP from the cube array.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Kit_SopCreateInverse( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nLits, Vec_Int_t * vMemory )
-{
-    unsigned uCube, uMask = 0;
-    int i, nCubes = Vec_IntSize(vInput);
-    // start the cover
-    cResult->nCubes = 0;
-    cResult->pCubes = Vec_IntFetch( vMemory, nCubes );
-    // add the cubes
-//    Vec_IntForEachEntry( vInput, uCube, i )
-    for ( i = 0; i < nCubes; i++ )
-    {
-        uCube = Vec_IntEntry( vInput, i );
-        uMask = ((uCube | (uCube >> 1)) & 0x55555555);
-        uMask |= (uMask << 1);
-        Kit_SopPushCube( cResult, uCube ^ uMask );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates SOP.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Kit_SopDup( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory )
-{
-    unsigned uCube;
-    int i;
-    // start the cover
-    cResult->nCubes = 0;
-    cResult->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
-    // add the cubes
-    Kit_SopForEachCube( cSop, uCube, i )
-        Kit_SopPushCube( cResult, uCube );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the quotient of division by literal.]
-
-  Description [Reduces the cover to be equal to the result of
-  division of the given cover by the literal.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Kit_SopDivideByLiteralQuo( Kit_Sop_t * cSop, int iLit )
-{
-    unsigned uCube;
-    int i, k = 0;
-    Kit_SopForEachCube( cSop, uCube, i )
-    {
-        if ( Kit_CubeHasLit(uCube, iLit) )
-            Kit_SopWriteCube( cSop, Kit_CubeRemLit(uCube, iLit), k++ );
-    }
-    Kit_SopShrink( cSop, k );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Divides cover by one cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Kit_SopDivideByCube( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory )
-{
-    unsigned uCube, uDiv;
-    int i;
-    // get the only cube
-    assert( Kit_SopCubeNum(cDiv) == 1 );
-    uDiv = Kit_SopCube(cDiv, 0);
-    // allocate covers
-    vQuo->nCubes = 0;
-    vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
-    vRem->nCubes = 0;
-    vRem->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
-    // sort the cubes
-    Kit_SopForEachCube( cSop, uCube, i )
-    {
-        if ( Kit_CubeContains( uCube, uDiv ) )
-            Kit_SopPushCube( vQuo, Kit_CubeSharp(uCube, uDiv) );
-        else
-            Kit_SopPushCube( vRem, uCube );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Divides cover by one cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Kit_SopDivideInternal( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory )
-{
-    unsigned uCube, uDiv, uCube2, uDiv2, uQuo;
-    int i, i2, k, k2, nCubesRem;
-    assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) );
-    // consider special case
-    if ( Kit_SopCubeNum(cDiv) == 1 )
-    {
-        Kit_SopDivideByCube( cSop, cDiv, vQuo, vRem, vMemory );
-        return;
-    }
-    // allocate quotient
-    vQuo->nCubes = 0;
-    vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) / Kit_SopCubeNum(cDiv) );
-    // for each cube of the cover
-    // it either belongs to the quotient or to the remainder
-    Kit_SopForEachCube( cSop, uCube, i )
-    {
-        // skip taken cubes
-        if ( Kit_CubeIsMarked(uCube) )
-            continue;
-        // find a matching cube in the divisor
-        uDiv = ~0;
-        Kit_SopForEachCube( cDiv, uDiv, k )
-            if ( Kit_CubeContains( uCube, uDiv ) )
-                break;
-        // the cube is not found 
-        if ( k == Kit_SopCubeNum(cDiv) )
-            continue;
-        // the quotient cube exists
-        uQuo = Kit_CubeSharp( uCube, uDiv );
-        // find corresponding cubes for other cubes of the divisor
-        uDiv2 = ~0;
-        Kit_SopForEachCube( cDiv, uDiv2, k2 )
-        {
-            if ( k2 == k )
-                continue;
-            // find a matching cube
-            Kit_SopForEachCube( cSop, uCube2, i2 )
-            {
-                // skip taken cubes
-                if ( Kit_CubeIsMarked(uCube2) )
-                    continue;
-                // check if the cube can be used
-                if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
-                    break;
-            }
-            // the case when the cube is not found
-            if ( i2 == Kit_SopCubeNum(cSop) )
-                break;
-        }
-        // we did not find some cubes - continue looking at other cubes
-        if ( k2 != Kit_SopCubeNum(cDiv) )
-            continue;
-        // we found all cubes - add the quotient cube
-        Kit_SopPushCube( vQuo, uQuo );
-
-        // mark the first cube
-        Kit_SopWriteCube( cSop, Kit_CubeMark(uCube), i );
-        // mark other cubes that have this quotient
-        Kit_SopForEachCube( cDiv, uDiv2, k2 )
-        {
-            if ( k2 == k )
-                continue;
-            // find a matching cube
-            Kit_SopForEachCube( cSop, uCube2, i2 )
-            {
-                // skip taken cubes
-                if ( Kit_CubeIsMarked(uCube2) )
-                    continue;
-                // check if the cube can be used
-                if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
-                    break;
-            }
-            assert( i2 < Kit_SopCubeNum(cSop) );
-            // the cube is found, mark it 
-            // (later we will add all unmarked cubes to the remainder)
-            Kit_SopWriteCube( cSop, Kit_CubeMark(uCube2), i2 );
-        }
-    }
-    // determine the number of cubes in the remainder
-    nCubesRem = Kit_SopCubeNum(cSop) - Kit_SopCubeNum(vQuo) * Kit_SopCubeNum(cDiv);
-    // allocate remainder
-    vRem->nCubes = 0;
-    vRem->pCubes = Vec_IntFetch( vMemory, nCubesRem );
-    // finally add the remaining unmarked cubes to the remainder 
-    // and clean the marked cubes in the cover
-    Kit_SopForEachCube( cSop, uCube, i )
-    {
-        if ( !Kit_CubeIsMarked(uCube) )
-        {
-            Kit_SopPushCube( vRem, uCube );
-            continue;
-        }
-        Kit_SopWriteCube( cSop, Kit_CubeUnmark(uCube), i );
-    }
-    assert( nCubesRem == Kit_SopCubeNum(vRem) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the common cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline unsigned Kit_SopCommonCube( Kit_Sop_t * cSop )
-{
-    unsigned uMask, uCube;
-    int i;
-    uMask = ~(unsigned)0;
-    Kit_SopForEachCube( cSop, uCube, i )
-        uMask &= uCube;
-    return uMask;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Makes the cover cube-free.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Kit_SopMakeCubeFree( Kit_Sop_t * cSop )
-{
-    unsigned uMask, uCube;
-    int i;
-    uMask = Kit_SopCommonCube( cSop );
-    if ( uMask == 0 )
-        return;
-    // remove the common cube
-    Kit_SopForEachCube( cSop, uCube, i )
-        Kit_SopWriteCube( cSop, Kit_CubeSharp(uCube, uMask), i );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if the cover is cube-free.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Kit_SopIsCubeFree( Kit_Sop_t * cSop )
-{
-    return Kit_SopCommonCube( cSop ) == 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates SOP composes of the common cube of the given SOP.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Kit_SopCommonCubeCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory )
-{
-    assert( Kit_SopCubeNum(cSop) > 0 );
-    cResult->nCubes = 0;
-    cResult->pCubes = Vec_IntFetch( vMemory, 1 );
-    Kit_SopPushCube( cResult, Kit_SopCommonCube(cSop) );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Find any literal that occurs more than once.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Kit_SopAnyLiteral( Kit_Sop_t * cSop, int nLits )
-{
-    unsigned uCube;
-    int i, k, nLitsCur;
-    // go through each literal
-    for ( i = 0; i < nLits; i++ )
-    {
-        // go through all the cubes
-        nLitsCur = 0;
-        Kit_SopForEachCube( cSop, uCube, k )
-            if ( Kit_CubeHasLit(uCube, i) )
-                nLitsCur++;
-        if ( nLitsCur > 1 )
-            return i;
-    }
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Find the least often occurring literal.]
-
-  Description [Find the least often occurring literal among those
-  that occur more than once.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Kit_SopWorstLiteral( Kit_Sop_t * cSop, int nLits )
-{
-    unsigned uCube;
-    int i, k, iMin, nLitsMin, nLitsCur;
-    int fUseFirst = 1;
-
-    // go through each literal
-    iMin = -1;
-    nLitsMin = 1000000;
-    for ( i = 0; i < nLits; i++ )
-    {
-        // go through all the cubes
-        nLitsCur = 0;
-        Kit_SopForEachCube( cSop, uCube, k )
-            if ( Kit_CubeHasLit(uCube, i) )
-                nLitsCur++;
-        // skip the literal that does not occur or occurs once
-        if ( nLitsCur < 2 )
-            continue;
-        // check if this is the best literal
-        if ( fUseFirst )
-        {
-            if ( nLitsMin > nLitsCur )
-            {
-                nLitsMin = nLitsCur;
-                iMin = i;
-            }
-        }
-        else
-        {
-            if ( nLitsMin >= nLitsCur )
-            {
-                nLitsMin = nLitsCur;
-                iMin = i;
-            }
-        }
-    }
-    if ( nLitsMin < 1000000 )
-        return iMin;
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Find the least often occurring literal.]
-
-  Description [Find the least often occurring literal among those
-  that occur more than once.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Kit_SopBestLiteral( Kit_Sop_t * cSop, int nLits, unsigned uMask )
-{
-    unsigned uCube;
-    int i, k, iMax, nLitsMax, nLitsCur;
-    int fUseFirst = 1;
-
-    // go through each literal
-    iMax = -1;
-    nLitsMax = -1;
-    for ( i = 0; i < nLits; i++ )
-    {
-        if ( !Kit_CubeHasLit(uMask, i) )
-            continue;
-        // go through all the cubes
-        nLitsCur = 0;
-        Kit_SopForEachCube( cSop, uCube, k )
-            if ( Kit_CubeHasLit(uCube, i) )
-                nLitsCur++;
-        // skip the literal that does not occur or occurs once
-        if ( nLitsCur < 2 )
-            continue;
-        // check if this is the best literal
-        if ( fUseFirst )
-        {
-            if ( nLitsMax < nLitsCur )
-            {
-                nLitsMax = nLitsCur;
-                iMax = i;
-            }
-        }
-        else
-        {
-            if ( nLitsMax <= nLitsCur )
-            {
-                nLitsMax = nLitsCur;
-                iMax = i;
-            }
-        }
-    }
-    if ( nLitsMax >= 0 )
-        return iMax;
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes a level-zero kernel.]
-
-  Description [Modifies the cover to contain one level-zero kernel.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Kit_SopDivisorZeroKernel_rec( Kit_Sop_t * cSop, int nLits )
-{
-    int iLit;
-    // find any literal that occurs at least two times
-    iLit = Kit_SopWorstLiteral( cSop, nLits );
-    if ( iLit == -1 )
-        return;
-    // derive the cube-free quotient
-    Kit_SopDivideByLiteralQuo( cSop, iLit ); // the same cover
-    Kit_SopMakeCubeFree( cSop );             // the same cover
-    // call recursively
-    Kit_SopDivisorZeroKernel_rec( cSop, nLits );    // the same cover
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the quick divisor of the cover.]
-
-  Description [Returns 0, if there is no divisor other than trivial.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Kit_SopDivisor( Kit_Sop_t * cResult, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory )
-{
-    if ( Kit_SopCubeNum(cSop) <= 1 )
-        return 0;
-    if ( Kit_SopAnyLiteral( cSop, nLits ) == -1 )
-        return 0;
-    // duplicate the cover
-    Kit_SopDup( cResult, cSop, vMemory );
-    // perform the kerneling
-    Kit_SopDivisorZeroKernel_rec( cResult, nLits );
-    assert( Kit_SopCubeNum(cResult) > 0 );
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Create the one-literal cover with the best literal from cSop.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Kit_SopBestLiteralCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, unsigned uCube, int nLits, Vec_Int_t * vMemory )
-{
-    int iLitBest;
-    // get the best literal
-    iLitBest = Kit_SopBestLiteral( cSop, nLits, uCube );
-    // start the cover
-    cResult->nCubes = 0;
-    cResult->pCubes = Vec_IntFetch( vMemory, 1 );
-    // set the cube
-    Kit_SopPushCube( cResult, Kit_CubeSetLit(0, iLitBest) );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-