From 1260d20cc05fe2d21088cc047c460e85ccdb3b14 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 5 Sep 2005 08:01:00 -0700 Subject: Version abc50905 --- src/sat/csat/csat_apis.c | 43 ++++++++++++++++++++++++++++++++++--------- 1 file changed, 34 insertions(+), 9 deletions(-) (limited to 'src/sat/csat') diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index 242de8e2..b030caef 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -28,8 +28,9 @@ struct CSAT_ManagerStruct_t { // information about the problem stmm_table * tName2Node; // the hash table mapping names to nodes + stmm_table * tNode2Name; // the hash table mapping nodes to names Abc_Ntk_t * pNtk; // the starting ABC network - Abc_Ntk_t * pTarget; // the AIG of the target + Abc_Ntk_t * pTarget; // the AIG representing the target char * pDumpFileName; // the name of the file to dump the target network // solving parameters int mode; // 0 = baseline; 1 = resource-aware fraiging @@ -44,6 +45,7 @@ struct CSAT_ManagerStruct_t static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars ); static void CSAT_TargetResFree( CSAT_Target_ResultT * p ); +static char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode ); // some external procedures extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); @@ -72,8 +74,9 @@ CSAT_Manager CSAT_InitManager() mng->pNtk = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_SOP ); mng->pNtk->pName = util_strsav("csat_network"); mng->tName2Node = stmm_init_table(strcmp, stmm_strhash); - mng->vNodes = Vec_PtrAlloc( 100 ); - mng->vValues = Vec_IntAlloc( 100 ); + mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash); + mng->vNodes = Vec_PtrAlloc( 100 ); + mng->vValues = Vec_IntAlloc( 100 ); return mng; } @@ -90,6 +93,7 @@ CSAT_Manager CSAT_InitManager() ***********************************************************************/ void CSAT_QuitManager( CSAT_Manager mng ) { + if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name ); if ( mng->tName2Node ) stmm_free_table( mng->tName2Node ); if ( mng->pNtk ) Abc_NtkDelete( mng->pNtk ); if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget ); @@ -151,7 +155,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c { printf( "CSAT_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; } // create the PI pObj = Abc_NtkCreatePi( mng->pNtk ); - pObj->pNext = (Abc_Obj_t *)name; + stmm_insert( mng->tNode2Name, (char *)pObj, name ); break; case CSAT_CONST: case CSAT_BAND: @@ -234,7 +238,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c { printf( "CSAT_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } // create the PO pObj = Abc_NtkCreatePo( mng->pNtk ); - pObj->pNext = (Abc_Obj_t *)name; + stmm_insert( mng->tNode2Name, (char *)pObj, name ); // connect to the PO fanin if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) ) { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; } @@ -270,13 +274,13 @@ int CSAT_Check_Integrity( CSAT_Manager mng ) // this procedure also finalizes construction of the ABC network Abc_NtkFixNonDrivenNets( pNtk ); Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext ); + Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) ); Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext ); + Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) ); assert( Abc_NtkLatchNum(pNtk) == 0 ); // make sure everything is okay with the network structure - if ( !Abc_NtkCheck( pNtk ) ) + if ( !Abc_NtkCheckRead( pNtk ) ) { printf( "CSAT_Check_Integrity: The internal network check has failed.\n" ); return 0; @@ -520,7 +524,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) // create the array of PI names and values for ( i = 0; i < mng->pResult->no_sig; i++ ) { - mng->pResult->names[i] = (char *)Abc_NtkCi(mng->pNtk, i)->pNext; // returns the same string that was given + mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given mng->pResult->values[i] = pModel[i]; } } @@ -623,6 +627,27 @@ void CSAT_TargetResFree( CSAT_Target_ResultT * p ) free( p ); } +/**Function************************************************************* + + Synopsis [Dumps the target AIG into the BENCH file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode ) +{ + char * pName = NULL; + if ( !stmm_lookup( mng->tNode2Name, (char *)pNode, (char **)&pName ) ) + { + assert( 0 ); + } + return pName; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3