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 ++++++++++++++++++++++++++++++++++--------- src/sat/fraig/fraig.h | 6 ++++++ src/sat/fraig/fraigApi.c | 14 +++++++++++++- src/sat/fraig/fraigCanon.c | 2 +- src/sat/fraig/fraigInt.h | 2 -- src/sat/fraig/fraigMan.c | 3 ++- src/sat/fraig/fraigNode.c | 4 ++++ src/sat/fraig/fraigTable.c | 4 ++-- 8 files changed, 62 insertions(+), 16 deletions(-) (limited to 'src/sat') 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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index 39c6fae8..901bbac9 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -36,6 +36,7 @@ typedef struct Fraig_NodeStruct_t_ Fraig_Node_t; typedef struct Fraig_NodeVecStruct_t_ Fraig_NodeVec_t; typedef struct Fraig_HashTableStruct_t_ Fraig_HashTable_t; typedef struct Fraig_ParamsStruct_t_ Fraig_Params_t; +typedef struct Fraig_PatternsStruct_t_ Fraig_Patterns_t; struct Fraig_ParamsStruct_t_ { @@ -99,6 +100,9 @@ extern int Fraig_ManReadDoSparse( Fraig_Man_t * p ); extern int Fraig_ManReadChoicing( Fraig_Man_t * p ); extern int Fraig_ManReadVerbose( Fraig_Man_t * p ); extern int * Fraig_ManReadModel( Fraig_Man_t * p ); +extern int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p ); +extern int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ); +extern int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ); extern void Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed ); extern void Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack ); @@ -124,6 +128,8 @@ extern int Fraig_NodeReadNumRefs( Fraig_Node_t * p ); extern int Fraig_NodeReadNumFanouts( Fraig_Node_t * p ); extern int Fraig_NodeReadSimInv( Fraig_Node_t * p ); extern int Fraig_NodeReadNumOnes( Fraig_Node_t * p ); +extern unsigned * Fraig_NodeReadPatternsRandom( Fraig_Node_t * p ); +extern unsigned * Fraig_NodeReadPatternsDynamic( Fraig_Node_t * p ); extern void Fraig_NodeSetData0( Fraig_Node_t * p, Fraig_Node_t * pData ); extern void Fraig_NodeSetData1( Fraig_Node_t * p, Fraig_Node_t * pData ); diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c index c9e6960c..b92f6afd 100644 --- a/src/sat/fraig/fraigApi.c +++ b/src/sat/fraig/fraigApi.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [fraigAccess.c] + FileName [fraigApi.c] PackageName [FRAIG: Functionally reduced AND-INV graphs.] @@ -58,6 +58,12 @@ int Fraig_ManReadDoSparse( Fraig_Man_t * p ) { int Fraig_ManReadChoicing( Fraig_Man_t * p ) { return p->fChoicing; } int Fraig_ManReadVerbose( Fraig_Man_t * p ) { return p->fVerbose; } int * Fraig_ManReadModel( Fraig_Man_t * p ) { return p->pModel; } +// returns the number of patterns used for random simulation (this number is fixed for the FRAIG run) +int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p ) { return p->nWordsRand * 32; } +// returns the number of dynamic patterns accumulated at runtime (include SAT solver counter-examples and distance-1 patterns derived from them) +int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ) { return p->iWordStart * 32; } +// returns the number of dynamic patterns proved useful to distinquish some FRAIG nodes (this number is more than 0 after the first garbage collection of patterns) +int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ) { return p->iPatsPerm; } /**Function************************************************************* @@ -104,6 +110,12 @@ int Fraig_NodeReadNumRefs( Fraig_Node_t * p ) { retu int Fraig_NodeReadNumFanouts( Fraig_Node_t * p ) { return p->nFanouts; } int Fraig_NodeReadSimInv( Fraig_Node_t * p ) { return p->fInv; } int Fraig_NodeReadNumOnes( Fraig_Node_t * p ) { return p->nOnes; } +// returns the pointer to the random simulation patterns (their number is returned by Fraig_ManReadPatternNumRandom) +// memory pointed to by this and the following procedure is maintained by the FRAIG package and exists as long as the package runs +unsigned * Fraig_NodeReadPatternsRandom( Fraig_Node_t * p ) { return p->puSimR; } +// returns the pointer to the dynamic simulation patterns (their number is returned by Fraig_ManReadPatternNumDynamic or Fraig_ManReadPatternNumDynamicFiltered) +// if the number of patterns is not evenly divisible by 32, the patterns beyond the given number contain garbage +unsigned * Fraig_NodeReadPatternsDynamic( Fraig_Node_t * p ) { return p->puSimD; } /**Function************************************************************* diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c index ae20531d..5a7d0563 100644 --- a/src/sat/fraig/fraigCanon.c +++ b/src/sat/fraig/fraigCanon.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [fraigAnd.c] + FileName [fraigCanon.c] PackageName [FRAIG: Functionally reduced AND-INV graphs.] diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index 1c765c12..131b750c 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -259,8 +259,6 @@ struct Fraig_NodeStruct_t_ Fraig_Node_t * pRepr; // the canonical functional representative of the node // simulation data -// Fraig_Sims_t * pSimsR; // the random simulation info -// Fraig_Sims_t * pSimsD; // the systematic simulation info unsigned uHashR; // the hash value for random information unsigned uHashD; // the hash value for dynamic information unsigned * puSimR; // the simulation information (random) diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index cfdba619..e5979c93 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -53,7 +53,8 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ) pParams->fChoicing = 0; // enables recording structural choices pParams->fTryProve = 1; // tries to solve the final miter pParams->fVerbose = 0; // the verbosiness flag - pParams->fVerboseP = 0; + pParams->fVerboseP = 0; // the verbose flag for reporting the proof + pParams->fInternal = 0; // the flag indicates the internal run } /**Function************************************************************* diff --git a/src/sat/fraig/fraigNode.c b/src/sat/fraig/fraigNode.c index 9da9b88c..a6c1d5a6 100644 --- a/src/sat/fraig/fraigNode.c +++ b/src/sat/fraig/fraigNode.c @@ -113,6 +113,10 @@ clk = clock(); { // generate the simulation info pNode->puSimR[i] = FRAIG_RANDOM_UNSIGNED; + // for reasons that take very long to explain, it makes sense to have (0000000...) + // pattern in the set (this helps if we need to return the counter-examples) + if ( i == 0 ) + pNode->puSimR[i] <<= 1; // compute the hash key pNode->uHashR ^= pNode->puSimR[i] * s_FraigPrimes[i]; } diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c index 7a8af749..d0f22acd 100644 --- a/src/sat/fraig/fraigTable.c +++ b/src/sat/fraig/fraigTable.c @@ -355,7 +355,7 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor return 0; // check the simulation info for ( i = 0; i < iWordLast; i++ ) - if ( pNode1->puSimR[i] != pNode2->puSimR[i] ) + if ( pNode1->puSimR[i] != pNode2->puSimR[i] ) return 0; } else @@ -365,7 +365,7 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor return 0; // check the simulation info for ( i = 0; i < iWordLast; i++ ) - if ( pNode1->puSimD[i] != pNode2->puSimD[i] ) + if ( pNode1->puSimD[i] != pNode2->puSimD[i] ) return 0; } return 1; -- cgit v1.2.3