Version abc70930

1 files changed, 0 insertions, 231 deletions

diff --git a/src/aig/kit/kitBdd.c b/src/aig/kit/kitBdd.c
deleted file mode 100644
index 9c8d4f7a..00000000
--- a/src/aig/kit/kitBdd.c
+++ /dev/null
@@ -1,231 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [kitBdd.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Computation kit.]
-
-  Synopsis    [Procedures involving BDDs.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - Dec 6, 2006.]
-
-  Revision    [$Id: kitBdd.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "kit.h"
-#include "extra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the BDD for the given SOP.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars )
-{
-    DdNode * bSum, * bCube, * bTemp, * bVar;
-    unsigned uCube;
-    int Value, i, v;
-    assert( nVars < 16 );
-    // start the cover
-    bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
-   // check the logic function of the node
-    Kit_SopForEachCube( cSop, uCube, i )
-    {
-        bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
-        for ( v = 0; v < nVars; v++ )
-        {
-            Value = ((uCube >> 2*v) & 3);
-            if ( Value == 1 )
-                bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
-            else if ( Value == 2 )
-                bVar = Cudd_bddIthVar( dd, v );
-            else
-                continue;
-            bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
-            Cudd_RecursiveDeref( dd, bTemp );
-        }
-        bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   
-        Cudd_Ref( bSum );
-        Cudd_RecursiveDeref( dd, bTemp );
-        Cudd_RecursiveDeref( dd, bCube );
-    }
-    // complement the result if necessary
-    Cudd_Deref( bSum );
-    return bSum;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converts graph to BDD.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph )
-{
-    DdNode * bFunc, * bFunc0, * bFunc1;
-    Kit_Node_t * pNode;
-    int i;
-
-    // sanity checks
-    assert( Kit_GraphLeaveNum(pGraph) >= 0 );
-    assert( Kit_GraphLeaveNum(pGraph) <= pGraph->nSize );
-
-    // check for constant function
-    if ( Kit_GraphIsConst(pGraph) )
-        return Cudd_NotCond( b1, Kit_GraphIsComplement(pGraph) );
-    // check for a literal
-    if ( Kit_GraphIsVar(pGraph) )
-        return Cudd_NotCond( Cudd_bddIthVar(dd, Kit_GraphVarInt(pGraph)), Kit_GraphIsComplement(pGraph) );
-
-    // assign the elementary variables
-    Kit_GraphForEachLeaf( pGraph, pNode, i )
-        pNode->pFunc = Cudd_bddIthVar( dd, i );
-
-    // compute the function for each internal node
-    Kit_GraphForEachNode( pGraph, pNode, i )
-    {
-        bFunc0 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
-        bFunc1 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
-        pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( pNode->pFunc );
-    }
-
-    // deref the intermediate results
-    bFunc = pNode->pFunc;   Cudd_Ref( bFunc );
-    Kit_GraphForEachNode( pGraph, pNode, i )
-        Cudd_RecursiveDeref( dd, pNode->pFunc );
-    Cudd_Deref( bFunc );
-
-    // complement the result if necessary
-    return Cudd_NotCond( bFunc, Kit_GraphIsComplement(pGraph) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Kit_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nVars, int nVarsTotal, int fMSBonTop )
-{
-    DdNode * bF0, * bF1, * bF;
-    int Var;
-    if ( nVars <= 5 )
-    {
-        unsigned uTruth, uMask;
-        uMask = ((~(unsigned)0) >> (32 - (1<<nVars)));
-        uTruth = (pTruth[iBit>>5] >> (iBit&31)) & uMask;
-        if ( uTruth == 0 )
-            return b0;
-        if ( uTruth == uMask )
-            return b1;        
-    }
-    // find the variable to use
-    Var = fMSBonTop? nVarsTotal-nVars : nVars-1;
-    // other special cases can be added
-    bF0 = Kit_TruthToBdd_rec( dd, pTruth, iBit,                nVars-1, nVarsTotal, fMSBonTop );  Cudd_Ref( bF0 );
-    bF1 = Kit_TruthToBdd_rec( dd, pTruth, iBit+(1<<(nVars-1)), nVars-1, nVarsTotal, fMSBonTop );  Cudd_Ref( bF1 );
-    bF  = Cudd_bddIte( dd, dd->vars[Var], bF1, bF0 );                     Cudd_Ref( bF );
-    Cudd_RecursiveDeref( dd, bF0 );
-    Cudd_RecursiveDeref( dd, bF1 );
-    Cudd_Deref( bF );
-    return bF;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compute BDD corresponding to the truth table.]
-
-  Description [If truth table has N vars, the BDD depends on N topmost
-  variables of the BDD manager. The most significant variable of the table
-  is encoded by the topmost variable of the manager. BDD construction is 
-  efficient in this case because BDD is constructed one node at a time, 
-  by simply adding BDD nodes on top of existent BDD nodes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop )
-{
-    return Kit_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars, fMSBonTop );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Verifies that the factoring is correct.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Kit_SopFactorVerify( Vec_Int_t * vCover, Kit_Graph_t * pFForm, int nVars )
-{
-    static DdManager * dd = NULL;
-    Kit_Sop_t Sop, * cSop = &Sop;
-    DdNode * bFunc1, * bFunc2;
-    Vec_Int_t * vMemory;
-    int RetValue;
-    // get the manager
-    if ( dd == NULL )
-        dd = Cudd_Init( 16, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    // derive SOP
-    vMemory = Vec_IntAlloc( Vec_IntSize(vCover) );
-    Kit_SopCreate( cSop, vCover, nVars, vMemory );
-    // get the functions
-    bFunc1 = Kit_SopToBdd( dd, cSop, nVars );      Cudd_Ref( bFunc1 );
-    bFunc2 = Kit_GraphToBdd( dd, pFForm );         Cudd_Ref( bFunc2 );
-//Extra_bddPrint( dd, bFunc1 ); printf("\n");
-//Extra_bddPrint( dd, bFunc2 ); printf("\n");
-    RetValue = (bFunc1 == bFunc2);
-    if ( bFunc1 != bFunc2 )
-    {
-        int s;
-        Extra_bddPrint( dd, bFunc1 ); printf("\n");
-        Extra_bddPrint( dd, bFunc2 ); printf("\n");
-        s  = 0;
-    }
-    Cudd_RecursiveDeref( dd, bFunc1 );
-    Cudd_RecursiveDeref( dd, bFunc2 );
-    Vec_IntFree( vMemory );
-    return RetValue;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-