Version abc61122

1 files changed, 0 insertions, 355 deletions

diff --git a/src/temp/aig/cudd2.c b/src/temp/aig/cudd2.c
deleted file mode 100644
index 3cc38260..00000000
--- a/src/temp/aig/cudd2.c
+++ /dev/null
@@ -1,355 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cudd2.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic And-Inverter Graph package.]
-
-  Synopsis    [Recording AIGs for the BDD operations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - October 3, 2006.]
-
-  Revision    [$Id: cudd2.c,v 1.00 2006/10/03 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-#include "st.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Aig_CuddMan_t_        Aig_CuddMan_t;
-struct Aig_CuddMan_t_
-{
-    Aig_Man_t *  pAig;   // internal AIG package
-    st_table *   pTable; // hash table mapping BDD nodes into AIG nodes
-};
-
-// static Cudd AIG manager used in this experiment
-static Aig_CuddMan_t * s_pCuddMan = NULL;
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Start AIG recording.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_Init( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd )
-{
-    int v;
-    // start the BDD-to-AIG manager when the first BDD manager is allocated
-    if ( s_pCuddMan != NULL )
-        return;
-    s_pCuddMan = ALLOC( Aig_CuddMan_t, 1 );
-    s_pCuddMan->pAig = Aig_ManStart();
-    s_pCuddMan->pTable = st_init_table( st_ptrcmp, st_ptrhash );
-    for ( v = 0; v < (int)numVars; v++ )
-        Aig_ObjCreatePi( s_pCuddMan->pAig );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops AIG recording.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_Quit( void * pCudd )
-{
-    assert( s_pCuddMan != NULL );
-    Aig_ManDumpBlif( s_pCuddMan->pAig, "aig_temp.blif" );
-    Aig_ManStop( s_pCuddMan->pAig );
-    st_free_table( s_pCuddMan->pTable );
-    free( s_pCuddMan );
-    s_pCuddMan = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Fetches AIG node corresponding to the BDD node from the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static Aig_Obj_t * Cudd2_GetArg( void * pArg )
-{
-    Aig_Obj_t * pNode;
-    assert( s_pCuddMan != NULL );
-    if ( !st_lookup( s_pCuddMan->pTable, (char *)Aig_Regular(pArg), (char **)&pNode ) )
-    {
-        printf( "Cudd2_GetArg(): An argument BDD is not in the hash table.\n" );
-        return NULL;
-    }
-    return Aig_NotCond( pNode, Aig_IsComplement(pArg) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts the AIG node corresponding to the BDD node into the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Cudd2_SetArg( Aig_Obj_t * pNode, void * pResult )
-{
-    assert( s_pCuddMan != NULL );
-    if ( st_is_member( s_pCuddMan->pTable, (char *)Aig_Regular(pResult) ) )
-        return;
-    pNode = Aig_NotCond( pNode,  Aig_IsComplement(pResult) );
-    st_insert( s_pCuddMan->pTable, (char *)Aig_Regular(pResult), (char *)pNode );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Registers constant 1 node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddOne( void * pCudd, void * pResult )
-{
-    Cudd2_SetArg( Aig_ManConst1(s_pCuddMan->pAig), pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds elementary variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddIthVar( void * pCudd, int iVar, void * pResult )
-{
-    int v;
-    assert( s_pCuddMan != NULL );
-    for ( v = Aig_ManPiNum(s_pCuddMan->pAig); v <= iVar; v++ )
-        Aig_ObjCreatePi( s_pCuddMan->pAig );
-    Cudd2_SetArg( Aig_ManPi(s_pCuddMan->pAig, iVar), pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddAnd( void * pCudd, void * pArg0, void * pArg1, void * pResult )
-{
-    Aig_Obj_t * pNode0, * pNode1, * pNode;
-    pNode0 = Cudd2_GetArg( pArg0 );
-    pNode1 = Cudd2_GetArg( pArg1 );
-    pNode  = Aig_And( s_pCuddMan->pAig, pNode0, pNode1 );
-    Cudd2_SetArg( pNode, pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddOr( void * pCudd, void * pArg0, void * pArg1, void * pResult )
-{
-    Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), Aig_Not(pResult) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddNand( void * pCudd, void * pArg0, void * pArg1, void * pResult )
-{
-    Cudd2_bddAnd( pCudd, pArg0, pArg1, Aig_Not(pResult) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddNor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
-{
-    Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddXor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
-{
-    Aig_Obj_t * pNode0, * pNode1, * pNode;
-    pNode0 = Cudd2_GetArg( pArg0 );
-    pNode1 = Cudd2_GetArg( pArg1 );
-    pNode  = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
-    Cudd2_SetArg( pNode, pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddXnor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
-{
-    Cudd2_bddXor( pCudd, pArg0, pArg1, Aig_Not(pResult) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddIte( void * pCudd, void * pArg0, void * pArg1, void * pArg2, void * pResult )
-{
-    Aig_Obj_t * pNode0, * pNode1, * pNode2, * pNode;
-    pNode0 = Cudd2_GetArg( pArg0 );
-    pNode1 = Cudd2_GetArg( pArg1 );
-    pNode2 = Cudd2_GetArg( pArg2 );
-    pNode  = Aig_Mux( s_pCuddMan->pAig, pNode0, pNode1, pNode2 );
-    Cudd2_SetArg( pNode, pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddCompose( void * pCudd, void * pArg0, void * pArg1, int v, void * pResult )
-{
-    Aig_Obj_t * pNode0, * pNode1, * pNode;
-    pNode0 = Cudd2_GetArg( pArg0 );
-    pNode1 = Cudd2_GetArg( pArg1 );
-    pNode  = Aig_Compose( s_pCuddMan->pAig, pNode0, pNode1, v );
-    Cudd2_SetArg( pNode, pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Should be called after each containment check.]
-
-  Description [Result should be 1 if Cudd2_bddLeq returned 1.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddLeq( void * pCudd, void * pArg0, void * pArg1, int Result )
-{
-    Aig_Obj_t * pNode0, * pNode1, * pNode;
-    pNode0 = Cudd2_GetArg( pArg0 );
-    pNode1 = Cudd2_GetArg( pArg1 );
-    pNode  = Aig_And( s_pCuddMan->pAig, pNode0, Aig_Not(pNode1) );
-    Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Should be called after each equality check.]
-
-  Description [Result should be 1 if they are equal.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddEqual( void * pCudd, void * pArg0, void * pArg1, int Result )
-{
-    Aig_Obj_t * pNode0, * pNode1, * pNode;
-    pNode0 = Cudd2_GetArg( pArg0 );
-    pNode1 = Cudd2_GetArg( pArg1 );
-    pNode  = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
-    Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-