Version abc80130

1 files changed, 0 insertions, 339 deletions

diff --git a/src/aig/kit/kitFactor.c b/src/aig/kit/kitFactor.c
deleted file mode 100644
index f596d9a8..00000000
--- a/src/aig/kit/kitFactor.c
+++ /dev/null
@@ -1,339 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [kitFactor.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Computation kit.]
-
-  Synopsis    [Algebraic factoring.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - Dec 6, 2006.]
-
-  Revision    [$Id: kitFactor.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "kit.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// factoring fails if intermediate memory usage exceed this limit
-#define KIT_FACTOR_MEM_LIMIT  (1<<16)
-
-static Kit_Edge_t  Kit_SopFactor_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory );
-static Kit_Edge_t  Kit_SopFactorLF_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, Kit_Sop_t * cSimple, int nLits, Vec_Int_t * vMemory );
-static Kit_Edge_t  Kit_SopFactorTrivial( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits );
-static Kit_Edge_t  Kit_SopFactorTrivialCube( Kit_Graph_t * pFForm, unsigned uCube, int nLits );
-
-extern int         Kit_SopFactorVerify( Vec_Int_t * cSop, Kit_Graph_t * pFForm, int nVars );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Factors the cover.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory )
-{
-    Kit_Sop_t Sop, * cSop = &Sop;
-    Kit_Graph_t * pFForm;
-    Kit_Edge_t eRoot;
-//    int nCubes;
-
-    // works for up to 15 variables because division procedure
-    // used the last bit for marking the cubes going to the remainder
-    assert( nVars < 16 );
-
-    // check for trivial functions
-    if ( Vec_IntSize(vCover) == 0 )
-        return Kit_GraphCreateConst0();
-    if ( Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0 )
-        return Kit_GraphCreateConst1();
-
-    // prepare memory manager
-//    Vec_IntClear( vMemory );
-    Vec_IntGrow( vMemory, KIT_FACTOR_MEM_LIMIT );
-
-    // perform CST
-    Kit_SopCreateInverse( cSop, vCover, 2 * nVars, vMemory ); // CST
-
-    // start the factored form
-    pFForm = Kit_GraphCreate( nVars );
-    // factor the cover
-    eRoot = Kit_SopFactor_rec( pFForm, cSop, 2 * nVars, vMemory );
-    // finalize the factored form
-    Kit_GraphSetRoot( pFForm, eRoot );
-    if ( fCompl )
-        Kit_GraphComplement( pFForm );
-
-    // verify the factored form
-//    nCubes = Vec_IntSize(vCover);
-//    Vec_IntShrink( vCover, nCubes );
-//    if ( !Kit_SopFactorVerify( vCover, pFForm, nVars ) )
-//        printf( "Verification has failed.\n" );
-    return pFForm;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursive factoring procedure.]
-
-  Description [For the pseudo-code, see Hachtel/Somenzi, 
-  Logic synthesis and verification algorithms, Kluwer, 1996, p. 432.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Kit_Edge_t Kit_SopFactor_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory )
-{
-    Kit_Sop_t Div, Quo, Rem, Com;
-    Kit_Sop_t * cDiv = &Div, * cQuo = &Quo, * cRem = &Rem, * cCom = &Com;
-    Kit_Edge_t eNodeDiv, eNodeQuo, eNodeRem, eNodeAnd;
-
-    // make sure the cover contains some cubes
-    assert( Kit_SopCubeNum(cSop) > 0 );
-
-    // get the divisor
-    if ( !Kit_SopDivisor(cDiv, cSop, nLits, vMemory) )
-        return Kit_SopFactorTrivial( pFForm, cSop, nLits );
-
-    // divide the cover by the divisor
-    Kit_SopDivideInternal( cSop, cDiv, cQuo, cRem, vMemory );
-
-    // check the trivial case
-    assert( Kit_SopCubeNum(cQuo) > 0 );
-    if ( Kit_SopCubeNum(cQuo) == 1 )
-        return Kit_SopFactorLF_rec( pFForm, cSop, cQuo, nLits, vMemory );
-
-    // make the quotient cube free
-    Kit_SopMakeCubeFree( cQuo );
-
-    // divide the cover by the quotient
-    Kit_SopDivideInternal( cSop, cQuo, cDiv, cRem, vMemory );
-
-    // check the trivial case
-    if ( Kit_SopIsCubeFree( cDiv ) )
-    {
-        eNodeDiv = Kit_SopFactor_rec( pFForm, cDiv, nLits, vMemory );
-        eNodeQuo = Kit_SopFactor_rec( pFForm, cQuo, nLits, vMemory );
-        eNodeAnd = Kit_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
-        if ( Kit_SopCubeNum(cRem) == 0 )
-            return eNodeAnd;
-        eNodeRem = Kit_SopFactor_rec( pFForm, cRem, nLits, vMemory );
-        return Kit_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
-    }
-
-    // get the common cube
-    Kit_SopCommonCubeCover( cCom, cDiv, vMemory );
-
-    // solve the simple problem
-    return Kit_SopFactorLF_rec( pFForm, cSop, cCom, nLits, vMemory );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Internal recursive factoring procedure for the leaf case.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Kit_Edge_t Kit_SopFactorLF_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, Kit_Sop_t * cSimple, int nLits, Vec_Int_t * vMemory )
-{
-    Kit_Sop_t Div, Quo, Rem;
-    Kit_Sop_t * cDiv = &Div, * cQuo = &Quo, * cRem = &Rem;
-    Kit_Edge_t eNodeDiv, eNodeQuo, eNodeRem, eNodeAnd;
-    assert( Kit_SopCubeNum(cSimple) == 1 );
-    // get the most often occurring literal
-    Kit_SopBestLiteralCover( cDiv, cSop, Kit_SopCube(cSimple, 0), nLits, vMemory );
-    // divide the cover by the literal
-    Kit_SopDivideByCube( cSop, cDiv, cQuo, cRem, vMemory );
-    // get the node pointer for the literal
-    eNodeDiv = Kit_SopFactorTrivialCube( pFForm, Kit_SopCube(cDiv, 0), nLits );
-    // factor the quotient and remainder
-    eNodeQuo = Kit_SopFactor_rec( pFForm, cQuo, nLits, vMemory );
-    eNodeAnd = Kit_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
-    if ( Kit_SopCubeNum(cRem) == 0 )
-        return eNodeAnd;
-    eNodeRem = Kit_SopFactor_rec( pFForm, cRem, nLits, vMemory );
-    return Kit_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Kit_Edge_t Kit_SopFactorTrivialCube_rec( Kit_Graph_t * pFForm, unsigned uCube, int nStart, int nFinish )
-{
-    Kit_Edge_t eNode1, eNode2;
-    int i, iLit = -1, nLits, nLits1, nLits2;
-    assert( uCube );
-    // count the number of literals in this interval
-    nLits = 0;
-    for ( i = nStart; i < nFinish; i++ )
-        if ( Kit_CubeHasLit(uCube, i) )
-        {
-            iLit = i;
-            nLits++;
-        }
-    assert( iLit != -1 );
-    // quit if there is only one literal        
-    if ( nLits == 1 )
-        return Kit_EdgeCreate( iLit/2, iLit%2 ); // CST
-    // split the literals into two parts
-    nLits1 = nLits/2;
-    nLits2 = nLits - nLits1;
-//    nLits2 = nLits/2;
-//    nLits1 = nLits - nLits2;
-    // find the splitting point
-    nLits = 0;
-    for ( i = nStart; i < nFinish; i++ )
-        if ( Kit_CubeHasLit(uCube, i) )
-        {
-            if ( nLits == nLits1 )
-                break;
-            nLits++;
-        }
-    // recursively construct the tree for the parts
-    eNode1 = Kit_SopFactorTrivialCube_rec( pFForm, uCube, nStart, i  );
-    eNode2 = Kit_SopFactorTrivialCube_rec( pFForm, uCube, i, nFinish );
-    return Kit_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring cube.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Kit_Edge_t Kit_SopFactorTrivialCube( Kit_Graph_t * pFForm, unsigned uCube, int nLits )
-{
-    return Kit_SopFactorTrivialCube_rec( pFForm, uCube, 0, nLits );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring SOP.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Kit_Edge_t Kit_SopFactorTrivial_rec( Kit_Graph_t * pFForm, unsigned * pCubes, int nCubes, int nLits )
-{
-    Kit_Edge_t eNode1, eNode2;
-    int nCubes1, nCubes2;
-    if ( nCubes == 1 )
-        return Kit_SopFactorTrivialCube_rec( pFForm, pCubes[0], 0, nLits );
-    // split the cubes into two parts
-    nCubes1 = nCubes/2;
-    nCubes2 = nCubes - nCubes1;
-//    nCubes2 = nCubes/2;
-//    nCubes1 = nCubes - nCubes2;
-    // recursively construct the tree for the parts
-    eNode1 = Kit_SopFactorTrivial_rec( pFForm, pCubes,           nCubes1, nLits );
-    eNode2 = Kit_SopFactorTrivial_rec( pFForm, pCubes + nCubes1, nCubes2, nLits );
-    return Kit_GraphAddNodeOr( pFForm, eNode1, eNode2 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Factoring the cover, which has no algebraic divisors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Kit_Edge_t Kit_SopFactorTrivial( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits )
-{
-    return Kit_SopFactorTrivial_rec( pFForm, cSop->pCubes, cSop->nCubes, nLits );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Testing procedure for the factoring code.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Kit_FactorTest( unsigned * pTruth, int nVars )
-{
-    Vec_Int_t * vCover, * vMemory;
-    Kit_Graph_t * pGraph;
-//    unsigned uTruthRes;
-    int RetValue;
-
-    // derive SOP
-    vCover = Vec_IntAlloc( 0 );
-    RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 );
-    assert( RetValue == 0 );
-
-    // derive factored form
-    vMemory = Vec_IntAlloc( 0 );
-    pGraph = Kit_SopFactor( vCover, 0, nVars, vMemory );
-/*
-    // derive truth table
-    assert( nVars <= 5 );
-    uTruthRes = Kit_GraphToTruth( pGraph );
-    if ( uTruthRes != pTruth[0] )
-        printf( "Verification failed!" );
-*/
-    printf( "Vars = %2d. Cubes = %3d. FFNodes = %3d. FF_memory = %3d.\n",
-        nVars, Vec_IntSize(vCover), Kit_GraphNodeNum(pGraph), Vec_IntSize(vMemory) );
-
-    Vec_IntFree( vMemory );
-    Vec_IntFree( vCover );
-    Kit_GraphFree( pGraph );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-