From 6205eaaee3a840dd076f9baaac67720d85d6a680 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 13 Mar 2008 08:01:00 -0700 Subject: Version abc80313 --- src/aig/aig/aigInter.c | 111 ++++++++++++- src/aig/bdc/bdc.h | 2 +- src/aig/bdc/bdcCore.c | 128 +++++++++++---- src/aig/bdc/bdcDec.c | 407 ++++++++++++++++++++++++++++++++++------------- src/aig/bdc/bdcInt.h | 31 ++-- src/aig/bdc/bdcTable.c | 24 ++- src/aig/fra/fra.h | 1 + src/aig/fra/fraSim.c | 21 +++ src/base/abc/abcSop.c | 15 ++ src/base/abci/abc.c | 13 +- src/base/abci/abcDar.c | 32 +++- src/base/abci/abcIf.c | 87 ++++++++++ src/base/cmd/cmd.c | 19 ++- src/map/if/if.h | 1 + src/opt/mfs/mfsCore.c | 4 + src/opt/mfs/mfsInt.h | 2 + src/opt/mfs/mfsMan.c | 10 +- src/opt/mfs/mfsStrash.c | 81 ++++++++++ src/sat/bsat/satSolver.c | 7 + src/sat/bsat/satStore.c | 25 +++ 20 files changed, 852 insertions(+), 169 deletions(-) diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c index c5d0b39f..d6b724c7 100644 --- a/src/aig/aig/aigInter.c +++ b/src/aig/aig/aigInter.c @@ -34,6 +34,104 @@ extern int timeInt; /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose ) +{ + sat_solver * pSat; + Cnf_Dat_t * pCnfOn, * pCnfOff; + Aig_Obj_t * pObj, * pObj2; + int Lits[3], status, i; + int clk = clock(); + + assert( Aig_ManPiNum(pManOn) == Aig_ManPiNum(pManOff) ); + assert( Aig_ManPoNum(pManOn) == Aig_ManPoNum(pManOff) ); + + // derive CNFs + pManOn->nRegs = Aig_ManPoNum(pManOn); + pCnfOn = Cnf_Derive( pManOn, Aig_ManPoNum(pManOn) ); + pManOn->nRegs = 0; + + pManOff->nRegs = Aig_ManPoNum(pManOn); + pCnfOff = Cnf_Derive( pManOff, Aig_ManPoNum(pManOff) ); + pManOff->nRegs = 0; + +// pCnfOn = Cnf_DeriveSimple( pManOn, Aig_ManPoNum(pManOn) ); +// pCnfOff = Cnf_DeriveSimple( pManOff, Aig_ManPoNum(pManOn) ); + Cnf_DataLift( pCnfOff, pCnfOn->nVars ); + + // start the solver + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, pCnfOn->nVars + pCnfOff->nVars ); + + // add clauses of A + for ( i = 0; i < pCnfOn->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnfOn->pClauses[i], pCnfOn->pClauses[i+1] ) ) + { + Cnf_DataFree( pCnfOn ); + Cnf_DataFree( pCnfOff ); + sat_solver_delete( pSat ); + return; + } + } + + // add clauses of B + for ( i = 0; i < pCnfOff->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnfOff->pClauses[i], pCnfOff->pClauses[i+1] ) ) + { + Cnf_DataFree( pCnfOn ); + Cnf_DataFree( pCnfOff ); + sat_solver_delete( pSat ); + return; + } + } + + // add PI clauses + // collect the common variables + Aig_ManForEachPi( pManOn, pObj, i ) + { + pObj2 = Aig_ManPi( pManOff, i ); + + Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + status = sat_solver_simplify( pSat ); + assert( status != 0 ); + + // solve incremental SAT problems + Aig_ManForEachPo( pManOn, pObj, i ) + { + pObj2 = Aig_ManPo( pManOff, i ); + + Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 0 ); + status = sat_solver_solve( pSat, Lits, Lits+2, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); + if ( status != l_False ) + printf( "The incremental SAT problem is not UNSAT.\n" ); + } + Cnf_DataFree( pCnfOn ); + Cnf_DataFree( pCnfOff ); + sat_solver_delete( pSat ); +// PRT( "Fast interpolation time", clock() - clk ); +} + /**Function************************************************************* Synopsis [] @@ -48,7 +146,7 @@ extern int timeInt; Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose ) { void * pSatCnf = NULL; - Inta_Man_t * pManInter; + Inta_Man_t * pManInter; Aig_Man_t * pRes; sat_solver * pSat; Cnf_Dat_t * pCnfOn, * pCnfOff; @@ -56,6 +154,7 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose Aig_Obj_t * pObj, * pObj2; int Lits[3], status, i; int clk; + int iLast; assert( Aig_ManPiNum(pManOn) == Aig_ManPiNum(pManOff) ); @@ -87,6 +186,12 @@ clk = clock(); } sat_solver_store_mark_clauses_a( pSat ); + // update the last clause + { + extern int sat_solver_store_change_last( sat_solver * pSat ); +// iLast = sat_solver_store_change_last( pSat ); + } + // add clauses of B for ( i = 0; i < pCnfOff->nClauses; i++ ) { @@ -102,6 +207,8 @@ clk = clock(); // add PI clauses // collect the common variables vVarsAB = Vec_IntAlloc( Aig_ManPiNum(pManOn) ); +// Vec_IntPush( vVarsAB, iLast ); + Aig_ManForEachPi( pManOn, pObj, i ) { Vec_IntPush( vVarsAB, pCnfOn->pVarNums[pObj->Id] ); @@ -175,6 +282,8 @@ timeInt += clock() - clk; */ Vec_IntFree( vVarsAB ); Sto_ManFree( pSatCnf ); + +// Ioa_WriteAiger( pRes, "inter2.aig", 0, 0 ); return pRes; } diff --git a/src/aig/bdc/bdc.h b/src/aig/bdc/bdc.h index 71875edb..e0c35773 100644 --- a/src/aig/bdc/bdc.h +++ b/src/aig/bdc/bdc.h @@ -58,7 +58,7 @@ struct Bdc_Par_t_ /*=== bdcCore.c ==========================================================*/ extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ); extern void Bdc_ManFree( Bdc_Man_t * p ); -extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesLimit ); +extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax ); #ifdef __cplusplus diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c index 157927b1..f0b0f3bc 100644 --- a/src/aig/bdc/bdcCore.c +++ b/src/aig/bdc/bdcCore.c @@ -42,15 +42,12 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ) { Bdc_Man_t * p; - unsigned * pData; - int i, k, nBits; p = ALLOC( Bdc_Man_t, 1 ); memset( p, 0, sizeof(Bdc_Man_t) ); assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 ); p->pPars = pPars; p->nWords = Kit_TruthWordNum( pPars->nVarsMax ); p->nDivsLimit = 200; - p->nNodesLimit = 0; // will be set later // memory p->vMemory = Vec_IntStart( 1 << 16 ); // internal nodes @@ -62,22 +59,11 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars ) memset( p->pTable, 0, sizeof(Bdc_Fun_t *) * p->nTableSize ); p->vSpots = Vec_IntAlloc( 256 ); // truth tables - p->vTruths = Vec_PtrAllocSimInfo( pPars->nVarsMax + 5, p->nWords ); - // set elementary truth tables - nBits = (1 << pPars->nVarsMax); - Kit_TruthFill( Vec_PtrEntry(p->vTruths, 0), p->nVars ); - for ( k = 0; k < pPars->nVarsMax; k++ ) - { - pData = Vec_PtrEntry( p->vTruths, k+1 ); - Kit_TruthClear( pData, p->nVars ); - for ( i = 0; i < nBits; i++ ) - if ( i & (1 << k) ) - pData[i>>5] |= (1 << (i&31)); - } - p->puTemp1 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 1 ); - p->puTemp2 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 2 ); - p->puTemp3 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 3 ); - p->puTemp4 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 4 ); + p->vTruths = Vec_PtrAllocTruthTables( p->pPars->nVarsMax ); + p->puTemp1 = ALLOC( unsigned, 4 * p->nWords ); + p->puTemp2 = p->puTemp1 + p->nWords; + p->puTemp3 = p->puTemp2 + p->nWords; + p->puTemp4 = p->puTemp3 + p->nWords; // start the internal ISFs p->pIsfOL = &p->IsfOL; Bdc_IsfStart( p, p->pIsfOL ); p->pIsfOR = &p->IsfOR; Bdc_IsfStart( p, p->pIsfOR ); @@ -102,6 +88,7 @@ void Bdc_ManFree( Bdc_Man_t * p ) Vec_IntFree( p->vMemory ); Vec_IntFree( p->vSpots ); Vec_PtrFree( p->vTruths ); + free( p->puTemp1 ); free( p->pNodes ); free( p->pTable ); free( p ); @@ -126,16 +113,25 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs ) Bdc_TableClear( p ); Vec_IntClear( p->vMemory ); // add constant 1 and elementary vars - p->nNodes = p->nNodesNew = 0; - for ( i = 0; i <= p->pPars->nVarsMax; i++ ) + p->nNodes = 0; + p->nNodesNew = - 1 - p->nVars - (vDivs? Vec_PtrSize(vDivs) : 0); + // add constant 1 + pNode = Bdc_FunNew( p ); + pNode->Type = BDC_TYPE_CONST1; + pNode->puFunc = NULL; + pNode->uSupp = 0; + Bdc_TableAdd( p, pNode ); + // add variables + for ( i = 0; i < p->nVars; i++ ) { pNode = Bdc_FunNew( p ); pNode->Type = BDC_TYPE_PI; pNode->puFunc = Vec_PtrEntry( p->vTruths, i ); - pNode->uSupp = i? (1 << (i-1)) : 0; + pNode->uSupp = (1 << i); Bdc_TableAdd( p, pNode ); } // add the divisors + if ( vDivs ) Vec_PtrForEachEntry( vDivs, puTruth, i ) { pNode = Bdc_FunNew( p ); @@ -146,6 +142,40 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs ) if ( i == p->nDivsLimit ) break; } + assert( p->nNodesNew == 0 ); +} + +/**Function************************************************************* + + Synopsis [Clears the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bdc_ManDecPrint( Bdc_Man_t * p ) +{ + Bdc_Fun_t * pNode; + int i; + printf( " 0 : Const 1\n" ); + for ( i = 1; i < p->nNodes; i++ ) + { + printf( " %d : ", i ); + pNode = p->pNodes + i; + if ( pNode->Type == BDC_TYPE_PI ) + printf( "PI " ); + else + { + printf( "%s%d &", Bdc_IsComplement(pNode->pFan0)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) ); + printf( " %s%d ", Bdc_IsComplement(pNode->pFan1)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) ); + } + Extra_PrintBinary( stdout, pNode->puFunc, (1<nVars) ); + printf( "\n" ); + } + printf( "Root = %s%d.\n", Bdc_IsComplement(p->pRoot)? "-":"", Bdc_FunId(p,Bdc_Regular(p->pRoot)) ); } /**Function************************************************************* @@ -162,25 +192,67 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs ) int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax ) { Bdc_Isf_t Isf, * pIsf = &Isf; + assert( nVars <= p->pPars->nVarsMax ); // set current manager parameters p->nVars = nVars; p->nWords = Kit_TruthWordNum( nVars ); + p->nNodesMax = nNodesMax; Bdc_ManPrepare( p, vDivs ); - p->nNodesLimit = (p->nNodes + nNodesMax < p->nNodesAlloc)? p->nNodes + nNodesMax : p->nNodesAlloc; // copy the function Bdc_IsfStart( p, pIsf ); - Bdc_IsfClean( pIsf ); - pIsf->uSupp = Kit_TruthSupport( puFunc, p->nVars ) | Kit_TruthSupport( puCare, p->nVars ); - Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars ); - Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars ); - // call decomposition + if ( puCare ) + { + Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars ); + Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars ); + } + else + { + Kit_TruthCopy( pIsf->puOn, puFunc, p->nVars ); + Kit_TruthNot( pIsf->puOff, puFunc, p->nVars ); + } Bdc_SuppMinimize( p, pIsf ); + // call decomposition p->pRoot = Bdc_ManDecompose_rec( p, pIsf ); if ( p->pRoot == NULL ) return -1; return p->nNodesNew; } +/**Function************************************************************* + + Synopsis [Performs decomposition of one function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bdc_ManDecomposeTest( unsigned uTruth, int nVars ) +{ + static int Counter = 0; + static int Total = 0; + Bdc_Par_t Pars = {0}, * pPars = &Pars; + Bdc_Man_t * p; + int RetValue; +// unsigned uCare = ~0x888f888f; + unsigned uCare = ~0; +// unsigned uFunc = 0x88888888; +// unsigned uFunc = 0xf888f888; +// unsigned uFunc = 0x117e117e; +// unsigned uFunc = 0x018b018b; + unsigned uFunc = uTruth; + + pPars->nVarsMax = 8; + p = Bdc_ManAlloc( pPars ); + RetValue = Bdc_ManDecompose( p, &uFunc, &uCare, nVars, NULL, 1000 ); + Total += RetValue; + printf( "%5d : Nodes = %5d. Total = %8d.\n", ++Counter, RetValue, Total ); +// Bdc_ManDecPrint( p ); + Bdc_ManFree( p ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/bdc/bdcDec.c b/src/aig/bdc/bdcDec.c index 747fcb14..13a33196 100644 --- a/src/aig/bdc/bdcDec.c +++ b/src/aig/bdc/bdcDec.c @@ -24,73 +24,10 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR ); -static int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, unsigned * puTruth, Bdc_Type_t Type ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/**Function************************************************************* - - Synopsis [Performs one step of bi-decomposition.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) -{ - Bdc_Fun_t * pFunc; - Bdc_Isf_t IsfL, * pIsfL = &IsfL; - Bdc_Isf_t IsfB, * pIsfR = &IsfB; - // check computed results - if ( pFunc = Bdc_TableLookup( p, pIsf ) ) - return pFunc; - // decide on the decomposition type - pFunc = Bdc_FunNew( p ); - if ( pFunc == NULL ) - return NULL; - pFunc->Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR ); - // decompose the left branch - pFunc->pFan0 = Bdc_ManDecompose_rec( p, pIsfL ); - if ( pFunc->pFan0 == NULL ) - return NULL; - // decompose the right branch - if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc->pFan0->puFunc, pFunc->Type ) ) - { - p->nNodes--; - return pFunc->pFan0; - } - pFunc->pFan1 = Bdc_ManDecompose_rec( p, pIsfL ); - if ( pFunc->pFan1 == NULL ) - return NULL; - // compute the function of node - pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); - if ( pFunc->Type == BDC_TYPE_AND ) - Kit_TruthAnd( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars ); - else if ( pFunc->Type == BDC_TYPE_OR ) - Kit_TruthOr( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars ); - else - assert( 0 ); - // verify correctness - assert( Bdc_TableCheckContainment(p, pIsf, pFunc->puFunc) ); - // convert from OR to AND - if ( pFunc->Type == BDC_TYPE_OR ) - { - pFunc->Type = BDC_TYPE_AND; - pFunc->pFan0 = Bdc_Not(pFunc->pFan0); - pFunc->pFan1 = Bdc_Not(pFunc->pFan1); - Kit_TruthNot( pFunc->puFunc, pFunc->puFunc, p->nVars ); - pFunc = Bdc_Not(pFunc); - } - Bdc_TableAdd( p, Bdc_Regular(pFunc) ); - return pFunc; -} - /**Function************************************************************* Synopsis [Updates the ISF of the right after the left was decompoosed.] @@ -102,8 +39,15 @@ Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) SeeAlso [] ***********************************************************************/ -int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, unsigned * puTruth, Bdc_Type_t Type ) +int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, Bdc_Fun_t * pFunc0, Bdc_Type_t Type ) { + unsigned * puTruth = p->puTemp1; + // get the truth table of the left branch + if ( Bdc_IsComplement(pFunc0) ) + Kit_TruthNot( puTruth, Bdc_Regular(pFunc0)->puFunc, p->nVars ); + else + Kit_TruthCopy( puTruth, pFunc0->puFunc, p->nVars ); + // split into parts if ( Type == BDC_TYPE_OR ) { // Right.Q = bdd_appex( Q, CompSpecLeftF, bddop_diff, setRightRes ); @@ -118,8 +62,9 @@ int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL // return (int)( pR->Q == b0 ); Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars ); - Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp ); - Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp ); + Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uUniq ); + Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uUniq ); +// assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) ); assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) ); return Kit_TruthIsConst0(pIsfR->puOn, p->nVars); } @@ -136,11 +81,12 @@ int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL // assert( pR->Q != b0 ); // return (int)( pR->R == b0 ); - Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars ); - Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp ); - Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp ); - assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) ); - return Kit_TruthIsConst0(pIsfR->puOn, p->nVars); + Kit_TruthAnd( pIsfR->puOff, pIsf->puOff, puTruth, p->nVars ); + Kit_TruthExistSet( pIsfR->puOff, pIsfR->puOff, p->nVars, pIsfL->uUniq ); + Kit_TruthExistSet( pIsfR->puOn, pIsf->puOn, p->nVars, pIsfL->uUniq ); +// assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) ); + assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) ); + return Kit_TruthIsConst0(pIsfR->puOff, p->nVars); } return 0; } @@ -201,10 +147,8 @@ int Bdc_DecomposeFindInitialVarSet( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pVars[End] ); if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp1, p->puTemp2, p->nVars) ) { - pIsfL->uSupp = (1 << Beg); - pIsfR->uSupp = (1 << End); - pIsfL->Var = Beg; - pIsfR->Var = End; + pIsfL->uUniq = (1 << pVars[Beg]); + pIsfR->uUniq = (1 << pVars[End]); return 1; } } @@ -229,15 +173,17 @@ int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc for ( v = 0; v < p->nVars; v++ ) { - Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v ); + if ( (pIsf->uSupp & (1 << v)) == 0 ) + continue; // if ( (Q & !bdd_exist( R, VarSetXa )) != bddfalse ) // Exist = Cudd_bddExistAbstract( dd, pF->R, Var ); Cudd_Ref( Exist ); // if ( Cudd_bddIteConstant( dd, pF->Q, Cudd_Not(Exist), b0 ) != b0 ) + + Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v ); if ( !Kit_TruthIsImply( pIsf->puOn, p->puTemp1, p->nVars ) ) { // measure the cost of this variable // VarCost = bdd_satcountset( bdd_forall( Q, VarSetXa ), VarCube ); - // Univ = Cudd_bddUnivAbstract( dd, pF->Q, Var ); Cudd_Ref( Univ ); // VarCost = Kit_TruthCountOnes( Univ, p->nVars ); // Cudd_RecursiveDeref( dd, Univ ); @@ -258,7 +204,6 @@ int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc if ( VarCostBest ) { // funQLeftRes = Q & bdd_exist( R, setRightORweak ); - // Temp = Cudd_bddExistAbstract( dd, pF->R, VarBest ); Cudd_Ref( Temp ); // pL->Q = Cudd_bddAnd( dd, pF->Q, Temp ); Cudd_Ref( pL->Q ); // Cudd_RecursiveDeref( dd, Temp ); @@ -269,11 +214,13 @@ int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc // pL->R = pF->R; Cudd_Ref( pL->R ); // pL->V = VarBest; Cudd_Ref( pL->V ); Kit_TruthCopy( pIsfL->puOff, pIsf->puOff, p->nVars ); - pIsfL->Var = VarBest; + pIsfL->uUniq = (1 << VarBest); + pIsfR->uUniq = 0; // assert( pL->Q != b0 ); // assert( pL->R != b0 ); // assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 ); +// assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) ); // express cost in percents of the covered boolean space Cost = VarCostBest * BDC_SCALE / (1<nVars); @@ -297,23 +244,25 @@ int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc ***********************************************************************/ int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR ) { - unsigned uSuppRem; + unsigned uSupportRem; int v, nLeftVars = 1, nRightVars = 1; // clean the var sets - Bdc_IsfClean( pIsfL ); - Bdc_IsfClean( pIsfR ); + Bdc_IsfStart( p, pIsfL ); + Bdc_IsfStart( p, pIsfR ); + // check that the support is correct + assert( Kit_TruthSupport(pIsf->puOn, p->nVars) == Kit_TruthSupport(pIsf->puOff, p->nVars) ); + assert( pIsf->uSupp == Kit_TruthSupport(pIsf->puOn, p->nVars) ); // find initial variable sets if ( !Bdc_DecomposeFindInitialVarSet( p, pIsf, pIsfL, pIsfR ) ) return Bdc_DecomposeWeakOr( p, pIsf, pIsfL, pIsfR ); // prequantify the variables in the offset - Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->Var ); - Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->Var ); + Kit_TruthExistSet( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->uUniq ); + Kit_TruthExistSet( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->uUniq ); // go through the remaining variables - uSuppRem = pIsf->uSupp & ~pIsfL->uSupp & ~pIsfR->uSupp; - assert( Kit_WordCountOnes(uSuppRem) > 0 ); + uSupportRem = pIsf->uSupp & ~pIsfL->uUniq & ~pIsfR->uUniq; for ( v = 0; v < p->nVars; v++ ) { - if ( (uSuppRem & (1 << v)) == 0 ) + if ( (uSupportRem & (1 << v)) == 0 ) continue; // prequantify this variable Kit_TruthExistNew( p->puTemp3, p->puTemp1, p->nVars, v ); @@ -325,15 +274,17 @@ int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) ) { // pL->V &= VarNew; - pIsfL->uSupp |= (1 << v); + pIsfL->uUniq |= (1 << v); nLeftVars++; + Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars ); } // else if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse ) else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) ) { // pR->V &= VarNew; - pIsfR->uSupp |= (1 << v); + pIsfR->uUniq |= (1 << v); nRightVars++; + Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars ); } } else @@ -342,15 +293,17 @@ int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) ) { // pR->V &= VarNew; - pIsfR->uSupp |= (1 << v); + pIsfR->uUniq |= (1 << v); nRightVars++; + Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars ); } // else if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse ) else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) ) { // pL->V &= VarNew; - pIsfL->uSupp |= (1 << v); + pIsfL->uUniq |= (1 << v); nLeftVars++; + Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars ); } } } @@ -365,28 +318,32 @@ int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf // pL->R = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( pL->R ); Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars ); - Kit_TruthExistSet( pIsfL->puOn, pIsfL->puOn, p->nVars, pIsfR->uSupp ); + Kit_TruthExistSet( pIsfL->puOn, pIsfL->puOn, p->nVars, pIsfR->uUniq ); Kit_TruthCopy( pIsfL->puOff, p->puTemp2, p->nVars ); +// assert( pL->Q != b0 ); +// assert( pL->R != b0 ); +// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 ); + assert( !Kit_TruthIsConst0(pIsfL->puOn, p->nVars) ); + assert( !Kit_TruthIsConst0(pIsfL->puOff, p->nVars) ); +// assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) ); + // derive the functions Q and R for the right branch // Temp = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( Temp ); // pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pL->V ); Cudd_Ref( pR->Q ); // Cudd_RecursiveDeref( dd, Temp ); // pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R ); -/* Kit_TruthAnd( pIsfR->puOn, pIsf->puOn, p->puTemp2, p->nVars ); - Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp ); + Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uUniq ); Kit_TruthCopy( pIsfR->puOff, p->puTemp1, p->nVars ); -*/ -// assert( pL->Q != b0 ); -// assert( pL->R != b0 ); -// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 ); - assert( !Kit_TruthIsConst0(pIsfL->puOn, p->nVars) ); - assert( !Kit_TruthIsConst0(pIsfL->puOff, p->nVars) ); - assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) ); + assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) ); + assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) ); +// assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) ); + assert( pIsfL->uUniq ); + assert( pIsfR->uUniq ); return Bdc_DecomposeGetCost( p, nLeftVars, nRightVars ); } @@ -403,7 +360,7 @@ int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf ***********************************************************************/ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR ) { - int CostOr, CostAnd, CostOrL, CostOrR, CostAndL, CostAndR; + int WeightOr, WeightAnd, WeightOrL, WeightOrR, WeightAndL, WeightAndR; Bdc_IsfClean( p->pIsfOL ); Bdc_IsfClean( p->pIsfOR ); @@ -411,33 +368,61 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL Bdc_IsfClean( p->pIsfAR ); // perform OR decomposition - CostOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR ); + WeightOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR ); // perform AND decomposition Bdc_IsfNot( pIsf ); - CostAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR ); + WeightAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR ); Bdc_IsfNot( pIsf ); Bdc_IsfNot( p->pIsfAL ); Bdc_IsfNot( p->pIsfAR ); + // check the case when decomposition does not exist + if ( WeightOr == 0 && WeightAnd == 0 ) + { + Bdc_IsfCopy( pIsfL, p->pIsfOL ); + Bdc_IsfCopy( pIsfR, p->pIsfOR ); + return BDC_TYPE_MUX; + } // check the hash table - Bdc_SuppMinimize( p, p->pIsfOL ); - CostOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL); - Bdc_SuppMinimize( p, p->pIsfOR ); - CostOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL); - Bdc_SuppMinimize( p, p->pIsfAL ); - CostAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL); - Bdc_SuppMinimize( p, p->pIsfAR ); - CostAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL); + assert( WeightOr || WeightAnd ); + WeightOrL = WeightOrR = 0; + if ( WeightOr ) + { + if ( p->pIsfOL->uUniq ) + { + Bdc_SuppMinimize( p, p->pIsfOL ); + WeightOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL); + } + if ( p->pIsfOR->uUniq ) + { + Bdc_SuppMinimize( p, p->pIsfOR ); + WeightOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL); + } + } + WeightAndL = WeightAndR = 0; + if ( WeightAnd ) + { + if ( p->pIsfAL->uUniq ) + { + Bdc_SuppMinimize( p, p->pIsfAL ); + WeightAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL); + } + if ( p->pIsfAR->uUniq ) + { + Bdc_SuppMinimize( p, p->pIsfAR ); + WeightAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL); + } + } // check if there is any reuse for the components - if ( CostOrL + CostOrR < CostAndL + CostAndR ) + if ( WeightOrL + WeightOrR > WeightAndL + WeightAndR ) { Bdc_IsfCopy( pIsfL, p->pIsfOL ); Bdc_IsfCopy( pIsfR, p->pIsfOR ); return BDC_TYPE_OR; } - if ( CostOrL + CostOrR > CostAndL + CostAndR ) + if ( WeightOrL + WeightOrR < WeightAndL + WeightAndR ) { Bdc_IsfCopy( pIsfL, p->pIsfAL ); Bdc_IsfCopy( pIsfR, p->pIsfAR ); @@ -445,15 +430,207 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL } // compare the two-component costs - if ( CostOr < CostAnd ) + if ( WeightOr > WeightAnd ) { Bdc_IsfCopy( pIsfL, p->pIsfOL ); Bdc_IsfCopy( pIsfR, p->pIsfOR ); return BDC_TYPE_OR; } + Bdc_IsfCopy( pIsfL, p->pIsfAL ); + Bdc_IsfCopy( pIsfR, p->pIsfAR ); return BDC_TYPE_AND; } +/**Function************************************************************* + + Synopsis [Find variable that leads to minimum sum of support sizes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR ) +{ + int Var, VarMin, nSuppMin, nSuppCur; + unsigned uSupp0, uSupp1; + VarMin = -1; + nSuppMin = 1000; + for ( Var = 0; Var < p->nVars; Var++ ) + { + if ( (pIsf->uSupp & (1 << Var)) == 0 ) + continue; + Kit_TruthCofactor0New( pIsfL->puOn, pIsf->puOn, p->nVars, Var ); + Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, Var ); + Kit_TruthCofactor1New( pIsfR->puOn, pIsf->puOn, p->nVars, Var ); + Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, Var ); + uSupp0 = Kit_TruthSupport( pIsfL->puOn, p->nVars ) & Kit_TruthSupport( pIsfL->puOff, p->nVars ); + uSupp1 = Kit_TruthSupport( pIsfR->puOn, p->nVars ) & Kit_TruthSupport( pIsfR->puOff, p->nVars ); + nSuppCur = Kit_WordCountOnes(uSupp0) + Kit_WordCountOnes(uSupp1); + if ( nSuppMin > nSuppCur ) + { + nSuppMin = nSuppCur; + VarMin = Var; +// break; + } + } + if ( VarMin >= 0 ) + { + Kit_TruthCofactor0New( pIsfL->puOn, pIsf->puOn, p->nVars, VarMin ); + Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, VarMin ); + Kit_TruthCofactor1New( pIsfR->puOn, pIsf->puOn, p->nVars, VarMin ); + Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, VarMin ); + Bdc_SuppMinimize( p, pIsfL ); + Bdc_SuppMinimize( p, pIsfR ); + } + return VarMin; +} + +/**Function************************************************************* + + Synopsis [Creates gates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc ) +{ + unsigned * puTruth = p->puTemp1; + if ( Bdc_IsComplement(pFunc) ) + Kit_TruthNot( puTruth, Bdc_Regular(pFunc)->puFunc, p->nVars ); + else + Kit_TruthCopy( puTruth, pFunc->puFunc, p->nVars ); + return Bdc_TableCheckContainment( p, pIsf, puTruth ); +} + +/**Function************************************************************* + + Synopsis [Creates gates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Bdc_Fun_t * Bdc_ManCreateGate( Bdc_Man_t * p, Bdc_Fun_t * pFunc0, Bdc_Fun_t * pFunc1, Bdc_Type_t Type ) +{ + Bdc_Fun_t * pFunc; + pFunc = Bdc_FunNew( p ); + if ( pFunc == NULL ) + return NULL; + pFunc->Type = Type; + pFunc->pFan0 = pFunc0; + pFunc->pFan1 = pFunc1; + pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); + // get the truth table of the left branch + if ( Bdc_IsComplement(pFunc0) ) + Kit_TruthNot( p->puTemp1, Bdc_Regular(pFunc0)->puFunc, p->nVars ); + else + Kit_TruthCopy( p->puTemp1, pFunc0->puFunc, p->nVars ); + // get the truth table of the right branch + if ( Bdc_IsComplement(pFunc1) ) + Kit_TruthNot( p->puTemp2, Bdc_Regular(pFunc1)->puFunc, p->nVars ); + else + Kit_TruthCopy( p->puTemp2, pFunc1->puFunc, p->nVars ); + // compute the function of node + if ( pFunc->Type == BDC_TYPE_AND ) + { + Kit_TruthAnd( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars ); + } + else if ( pFunc->Type == BDC_TYPE_OR ) + { + Kit_TruthOr( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars ); + // transform to AND gate + pFunc->Type = BDC_TYPE_AND; + pFunc->pFan0 = Bdc_Not(pFunc->pFan0); + pFunc->pFan1 = Bdc_Not(pFunc->pFan1); + Kit_TruthNot( pFunc->puFunc, pFunc->puFunc, p->nVars ); + pFunc = Bdc_Not(pFunc); + } + else + assert( 0 ); + // add to table + Bdc_Regular(pFunc)->uSupp = Kit_TruthSupport( Bdc_Regular(pFunc)->puFunc, p->nVars ); + Bdc_TableAdd( p, Bdc_Regular(pFunc) ); + return pFunc; +} + +/**Function************************************************************* + + Synopsis [Performs one step of bi-decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) +{ + int static Counter = 0; + int LocalCounter = Counter++; + Bdc_Type_t Type; + Bdc_Fun_t * pFunc, * pFunc0, * pFunc1; + Bdc_Isf_t IsfL, * pIsfL = &IsfL; + Bdc_Isf_t IsfB, * pIsfR = &IsfB; +/* +printf( "Init function (%d):\n", LocalCounter ); +Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n"); +Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n"); +*/ + // check computed results + assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) ); + if ( pFunc = Bdc_TableLookup( p, pIsf ) ) + return pFunc; + // decide on the decomposition type + Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR ); + if ( Type == BDC_TYPE_MUX ) + { + int iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR ); + pFunc0 = Bdc_ManDecompose_rec( p, pIsfL ); + pFunc1 = Bdc_ManDecompose_rec( p, pIsfR ); + if ( pFunc0 == NULL || pFunc1 == NULL ) + return NULL; + pFunc = Bdc_FunWithId( p, iVar + 1 ); + pFunc0 = Bdc_ManCreateGate( p, Bdc_Not(pFunc), pFunc0, BDC_TYPE_AND ); + pFunc1 = Bdc_ManCreateGate( p, pFunc, pFunc1, BDC_TYPE_AND ); + if ( pFunc0 == NULL || pFunc1 == NULL ) + return NULL; + pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, BDC_TYPE_OR ); + } + else + { + pFunc0 = Bdc_ManDecompose_rec( p, pIsfL ); + if ( pFunc0 == NULL ) + return NULL; + // decompose the right branch + if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc0, Type ) ) + { + p->nNodesNew--; + return pFunc0; + } + Bdc_SuppMinimize( p, pIsfR ); + pFunc1 = Bdc_ManDecompose_rec( p, pIsfR ); + if ( pFunc1 == NULL ) + return NULL; + // create new gate + pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type ); + } + if ( pFunc == NULL ) + return NULL; + assert( Bdc_ManNodeVerify( p, pIsf, pFunc ) ); + return pFunc; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h index 5f7b1186..5fda4301 100644 --- a/src/aig/bdc/bdcInt.h +++ b/src/aig/bdc/bdcInt.h @@ -36,7 +36,7 @@ extern "C" { /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#define BDC_SCALE 100 // value used to compute the cost +#define BDC_SCALE 1000 // value used to compute the cost //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -47,11 +47,11 @@ typedef enum { BDC_TYPE_NONE = 0, // 0: unknown BDC_TYPE_CONST1, // 1: constant 1 BDC_TYPE_PI, // 2: primary input - BDC_TYPE_AND, // 4: AND-gate - BDC_TYPE_OR, // 5: OR-gate (temporary) - BDC_TYPE_XOR, // 6: XOR-gate - BDC_TYPE_MUX, // 7: MUX-gate - BDC_TYPE_OTHER // 8: unused + BDC_TYPE_AND, // 3: AND-gate + BDC_TYPE_OR, // 4: OR-gate (temporary) + BDC_TYPE_XOR, // 5: XOR-gate + BDC_TYPE_MUX, // 6: MUX-gate + BDC_TYPE_OTHER // 7: unused } Bdc_Type_t; typedef struct Bdc_Fun_t_ Bdc_Fun_t; @@ -60,7 +60,6 @@ struct Bdc_Fun_t_ int Type; // Const1, PI, AND, XOR, MUX Bdc_Fun_t * pFan0; // fanin of the given node Bdc_Fun_t * pFan1; // fanin of the given node - Bdc_Fun_t * pFan2; // fanin of the given node unsigned uSupp; // bit mask of current support unsigned * puFunc; // the function of the node Bdc_Fun_t * pNext; // next function with same support @@ -70,8 +69,8 @@ struct Bdc_Fun_t_ typedef struct Bdc_Isf_t_ Bdc_Isf_t; struct Bdc_Isf_t_ { - int Var; // the first variable assigned - unsigned uSupp; // the current support + unsigned uSupp; // the complete support of this component + unsigned uUniq; // the unique variables of this component unsigned * puOn; // on-set unsigned * puOff; // off-set }; @@ -82,13 +81,13 @@ struct Bdc_Man_t_ Bdc_Par_t * pPars; // parameter set int nVars; // the number of variables int nWords; // the number of words - int nNodesLimit; // the limit on the number of new nodes + int nNodesMax; // the limit on the number of new nodes int nDivsLimit; // the limit on the number of divisors // internal nodes Bdc_Fun_t * pNodes; // storage for decomposition nodes - int nNodes; // the number of nodes used - int nNodesNew; // the number of nodes used int nNodesAlloc; // the number of nodes allocated + int nNodes; // the number of all nodes created so far + int nNodesNew; // the number of new AND nodes created so far Bdc_Fun_t * pRoot; // the root node // resub candidates Bdc_Fun_t ** pTable; // hash table of candidates @@ -115,9 +114,11 @@ static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)01); } static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)(c!=0)); } -static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p ) { Bdc_Fun_t * pRes; if ( p->nNodes == p->nNodesLimit ) return NULL; pRes = p->pNodes + p->nNodes++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); p->nNodesNew++; return pRes; } -static inline void Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); } -static inline void Bdc_IsfClean( Bdc_Isf_t * p ) { p->uSupp = 0; p->Var = 0; } +static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p ) { Bdc_Fun_t * pRes; if ( p->nNodes >= p->nNodesAlloc || p->nNodesNew >= p->nNodesMax ) return NULL; pRes = p->pNodes + p->nNodes++; p->nNodesNew++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); return pRes; } +static inline Bdc_Fun_t * Bdc_FunWithId( Bdc_Man_t * p, int Id ) { assert( Id < p->nNodes ); return p->pNodes + Id; } +static inline int Bdc_FunId( Bdc_Man_t * p, Bdc_Fun_t * pFun ) { return pFun - p->pNodes; } +static inline void Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->uSupp = 0; pF->uUniq = 0; pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); } +static inline void Bdc_IsfClean( Bdc_Isf_t * p ) { p->uSupp = 0; p->uUniq = 0; } static inline void Bdc_IsfCopy( Bdc_Isf_t * p, Bdc_Isf_t * q ) { Bdc_Isf_t T = *p; *p = *q; *q = T; } static inline void Bdc_IsfNot( Bdc_Isf_t * p ) { unsigned * puT = p->puOn; p->puOn = p->puOff; p->puOff = puT; } diff --git a/src/aig/bdc/bdcTable.c b/src/aig/bdc/bdcTable.c index d86a938d..b7f10344 100644 --- a/src/aig/bdc/bdcTable.c +++ b/src/aig/bdc/bdcTable.c @@ -42,6 +42,9 @@ void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) { int v; + // compute support + pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) | + Kit_TruthSupport( pIsf->puOff, p->nVars ); // go through the support variables for ( v = 0; v < p->nVars; v++ ) { @@ -72,7 +75,7 @@ void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth ) { return Kit_TruthIsImply( pIsf->puOn, puTruth, p->nVars ) && - Kit_TruthIsDisjoint( pIsf->puOff, puTruth, p->nVars ); + Kit_TruthIsDisjoint( puTruth, pIsf->puOff, p->nVars ); } /**Function************************************************************* @@ -88,10 +91,29 @@ int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTru ***********************************************************************/ Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf ) { + int fDisableCache = 0; Bdc_Fun_t * pFunc; + if ( fDisableCache && Kit_WordCountOnes(pIsf->uSupp) > 1 ) + return NULL; + if ( pIsf->uSupp == 0 ) + { + assert( p->pTable[pIsf->uSupp] == p->pNodes ); + if ( Kit_TruthIsConst1( pIsf->puOn, p->nVars ) ) + return p->pNodes; + assert( Kit_TruthIsConst1( pIsf->puOff, p->nVars ) ); + return Bdc_Not(p->pNodes); + } for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext ) if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) ) return pFunc; + Bdc_IsfNot( pIsf ); + for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext ) + if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) ) + { + Bdc_IsfNot( pIsf ); + return Bdc_Not(pFunc); + } + Bdc_IsfNot( pIsf ); return NULL; } diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 48588eb2..e7583b4b 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -334,6 +334,7 @@ extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ); extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ); extern int Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); extern int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right ); +extern int Fra_SmlNodeCountOnes( Fra_Sml_t * p, Aig_Obj_t * pObj ); extern int Fra_SmlCheckOutput( Fra_Man_t * p ); extern void Fra_SmlSavePattern( Fra_Man_t * p ); extern void Fra_SmlSimulate( Fra_Man_t * p, int fInit ); diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index fe11ac36..b14dd5bd 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -159,6 +159,27 @@ int Fra_SmlNodeIsZero( Fra_Sml_t * p, Aig_Obj_t * pObj ) return 1; } +/**Function************************************************************* + + Synopsis [Counts the number of one's in the patten of the output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_SmlNodeCountOnes( Fra_Sml_t * p, Aig_Obj_t * pObj ) +{ + unsigned * pSims; + int i, Counter = 0; + pSims = Fra_ObjSim(p, pObj->Id); + for ( i = 0; i < p->nWordsTotal; i++ ) + Counter += Aig_WordCountOnes( pSims[i] ); + return Counter; +} + /**Function************************************************************* diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c index 106901ab..dc3595c1 100644 --- a/src/base/abc/abcSop.c +++ b/src/base/abc/abcSop.c @@ -931,6 +931,21 @@ char * Abc_SopFromTruthHex( char * pTruth ) pCube[nVars + 1] = '1'; pCube[nVars + 2] = '\n'; } +/* + // create TT representation + { + extern void Bdc_ManDecomposeTest( unsigned uTruth, int nVars ); + unsigned uTruth = 0; + int nVarsAll = 4; + assert( nVarsAll == 4 ); + assert( nVars <= nVarsAll ); + Vec_IntForEachEntry( vMints, Mint, i ) + uTruth |= (1 << Mint); +// uTruth = uTruth | (uTruth << 8) | (uTruth << 16) | (uTruth << 24); + uTruth = uTruth | (uTruth << 16); + Bdc_ManDecomposeTest( uTruth, nVarsAll ); + } +*/ Vec_IntFree( vMints ); return pSopCover; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f311686d..f366a612 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -391,6 +391,10 @@ void Abc_Init( Abc_Frame_t * pAbc ) extern void Dar_LibStart(); Dar_LibStart(); } + { + extern Bdc_ManDecomposeTest( unsigned uTruth, int nVars ); +// Bdc_ManDecomposeTest( 0x0f0f0f0f, 3 ); + } } /**Function************************************************************* @@ -10771,6 +10775,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fEdge = 0; pPars->fCutMin = 0; pPars->fSeqMap = 0; + pPars->fBidec = 0; pPars->fVerbose = 0; // internal parameters pPars->fTruth = 0; @@ -10782,7 +10787,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pFuncCost = NULL; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEpaflemrstvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEpaflemrstbvh" ) ) != EOF ) { switch ( c ) { @@ -10880,6 +10885,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': pPars->fLiftLeaves ^= 1; break; + case 'b': + pPars->fBidec ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -11008,7 +11016,7 @@ usage: sprintf( LutSize, "library" ); else sprintf( LutSize, "%d", pPars->nLutSize ); - fprintf( pErr, "usage: if [-KCFA num] [-DE float] [-parlemsvh]\n" ); + fprintf( pErr, "usage: if [-KCFA num] [-DE float] [-parlemsbvh]\n" ); fprintf( pErr, "\t performs FPGA technology mapping of the network\n" ); fprintf( pErr, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize ); fprintf( pErr, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); @@ -11025,6 +11033,7 @@ usage: fprintf( pErr, "\t-m : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" ); fprintf( pErr, "\t-s : toggles sequential mapping [default = %s]\n", pPars->fSeqMap? "yes": "no" ); // fprintf( pErr, "\t-t : toggles the use of true sequential cuts [default = %s]\n", pPars->fLiftLeaves? "yes": "no" ); + fprintf( pErr, "\t-b : toggles deriving local AIGs using bi-decomposition [default = %s]\n", pPars->fBidec? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : prints the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 012b74cf..adf1f6e6 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1567,6 +1567,32 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbo return pNtkAig; } +/**Function************************************************************* + + Synopsis [Fast interpolation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkInterFast( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose ) +{ + extern void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose ); + Aig_Man_t * pManOn, * pManOff; + // create internal AIGs + pManOn = Abc_NtkToDar( pNtkOn, 0 ); + if ( pManOn == NULL ) + return; + pManOff = Abc_NtkToDar( pNtkOff, 0 ); + if ( pManOff == NULL ) + return; + Aig_ManInterFast( pManOn, pManOff, fVerbose ); + Aig_ManStop( pManOn ); + Aig_ManStop( pManOff ); +} int timeCnf; int timeSat; @@ -1587,12 +1613,15 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose { Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter; Abc_Obj_t * pObj; - int i; + int i, clk = clock(); if ( Abc_NtkCoNum(pNtkOn) != Abc_NtkCoNum(pNtkOff) ) { printf( "Currently works only for networks with equal number of POs.\n" ); return NULL; } + // compute the fast interpolation time +// Abc_NtkInterFast( pNtkOn, pNtkOff, fVerbose ); + // consider the case of one output if ( Abc_NtkCoNum(pNtkOn) == 1 ) return Abc_NtkInterOne( pNtkOn, pNtkOff, fVerbose ); // start the new newtork @@ -1636,6 +1665,7 @@ timeInt = 0; // PRT( "CNF", timeCnf ); // PRT( "SAT", timeSat ); // PRT( "Int", timeInt ); +// PRT( "Slow interpolation time", clock() - clk ); // return the network if ( !Abc_NtkCheck( pNtkInter ) ) diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index bf351a47..a20925b2 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -34,6 +34,7 @@ static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_O static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk ); extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose ); +extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -84,6 +85,8 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ) if ( pNtkNew == NULL ) return NULL; If_ManStop( pIfMan ); + if ( pPars->fBidec && pPars->nLutSize <= 8 ) + Abc_NtkBidecResyn( pNtkNew ); // duplicate EXDC if ( pNtk->pExdc ) @@ -309,7 +312,9 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t Abc_NodeComplement( pNodeNew ); } else + { pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pIfObj ); + } If_ObjSetCopy( pIfObj, pNodeNew ); return pNodeNew; } @@ -545,6 +550,88 @@ Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk ) return vNodes; } + +#include "bdc.h" +#include "bdcInt.h" + +static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) ); } + +/**Function************************************************************* + + Synopsis [Resynthesizes nodes using bi-decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth ) +{ + unsigned * pTruth; + Bdc_Fun_t * pFunc; + int i; + // derive truth table + pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 ); + if ( Hop_IsComplement(pRoot) ) + Extra_TruthNot( pTruth, pTruth, nVars ); + // decompose truth table + Bdc_ManDecompose( p, pTruth, NULL, nVars, NULL, 1000 ); + // convert back into HOP + Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop ); + for ( i = 0; i < nVars; i++ ) + Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i ); + for ( i = nVars + 1; i < p->nNodes; i++ ) + { + pFunc = Bdc_FunWithId( p, i ); + pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) ); + } + return Bdc_FunCopyHop(p->pRoot); +} + +/**Function************************************************************* + + Synopsis [Resynthesizes nodes using bi-decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk ) +{ + Bdc_Par_t Pars = {0}, * pPars = &Pars; + Bdc_Man_t * p; + Abc_Obj_t * pObj; + Vec_Int_t * vTruth; + int i, nGainTotal = 0, nNodes1, nNodes2; + int clk = clock(); + pPars->nVarsMax = Abc_NtkGetFaninMax( pNtk ); + if ( pPars->nVarsMax > 8 ) + { + printf( "Resynthesis is not performed.\n" ); + return; + } + vTruth = Vec_IntAlloc( 0 ); + p = Bdc_ManAlloc( pPars ); + Abc_NtkForEachNode( pNtk, pObj, i ) + { + nNodes1 = Hop_DagSize(pObj->pData); + pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth ); + nNodes2 = Hop_DagSize(pObj->pData); + nGainTotal += nNodes1 - nNodes2; + } +// printf( "LUTs = %d. Total gain in AIG nodes = %d. ", Abc_NtkNodeNum(pNtk), nGainTotal ); +// PRT( "Time", clock() - clk ); + Bdc_ManFree( p ); + Vec_IntFree( vTruth ); +} + + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index fd57f430..316dd8ad 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -149,12 +149,17 @@ void Cmd_End( Abc_Frame_t * pAbc ) int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv ) { int c; + int fClear; + fClear = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) { switch ( c ) { + case 'c': + fClear ^= 1; + break; case 'h': goto usage; default: @@ -162,11 +167,19 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv ) } } + if ( fClear ) + { + pAbc->TimeTotal += pAbc->TimeCommand; + pAbc->TimeCommand = 0.0; + return 0; + } + if ( argc != globalUtilOptind ) { goto usage; } + pAbc->TimeTotal += pAbc->TimeCommand; fprintf( pAbc->Out, "elapse: %3.2f seconds, total: %3.2f seconds\n", pAbc->TimeCommand, pAbc->TimeTotal ); @@ -182,7 +195,9 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; usage: - fprintf( pAbc->Err, "usage: time [-h]\n" ); + fprintf( pAbc->Err, "usage: time [-ch]\n" ); + fprintf( pAbc->Err, " \t\tprint the runtime since the last call\n" ); + fprintf( pAbc->Err, " -c \t\tclears the elapsed time without printing it\n" ); fprintf( pAbc->Err, " -h \t\tprint the command usage\n" ); return 1; } diff --git a/src/map/if/if.h b/src/map/if/if.h index 6c33e03f..d42dd0af 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -90,6 +90,7 @@ struct If_Par_t_ int fEdge; // uses edge-based cut selection heuristics int fCutMin; // performs cut minimization by removing functionally reducdant variables int fSeqMap; // sequential mapping + int fBidec; // use bi-decomposition int fVerbose; // the verbosity flag // internal parameters int fAreaOnly; // area only mode diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 4a2e96e7..4e4f7490 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -110,6 +110,8 @@ clk = clock(); p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); p->timeWin += clock() - clk; + // count the number of patterns +// p->dTotalRatios += Abc_NtkConstraintRatio( p, pNode ); // construct AIG for the window clk = clock(); p->pAigWin = Abc_NtkConstructAig( p, pNode ); @@ -121,6 +123,8 @@ p->timeCnf += clock() - clk; // create the SAT problem clk = clock(); p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 ); + if ( p->pSat == NULL ) + return 0; // solve the SAT problem Abc_NtkMfsSolveSat( p, pNode ); p->timeSat += clock() - clk; diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index b7fa6ef0..91395d03 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -86,6 +86,7 @@ struct Mfs_Man_t_ int nTotalDivs; int nTimeOuts; int nDcMints; + double dTotalRatios; // node/edge stats int nTotalNodesBeg; int nTotalNodesEnd; @@ -132,6 +133,7 @@ extern int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode ) extern void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ); /*=== mfsStrash.c ==========================================================*/ extern Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ); +extern double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode ); /*=== mfsWin.c ==========================================================*/ extern Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit ); diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 5f947aeb..17ca40fc 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -126,9 +126,13 @@ void Mfs_ManPrint( Mfs_Man_t * p ) } else { - printf( "Nodes = %d. Care mints = %d. Total mints = %d. Ratio = %5.2f.\n", - p->nNodesTried, p->nMintsCare, p->nMintsTotal, 1.0 * p->nMintsCare / p->nMintsTotal ); + printf( "Nodes = %d. DC mints in local space = %d. Total mints = %d. Ratio = %5.2f.\n", + p->nNodesTried, p->nMintsTotal-p->nMintsCare, p->nMintsTotal, + 1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal ); +// printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", +// 1.0-(p->dTotalRatios/p->nNodesTried) ); } +/* PRTP( "Win", p->timeWin , p->timeTotal ); PRTP( "Div", p->timeDiv , p->timeTotal ); PRTP( "Aig", p->timeAig , p->timeTotal ); @@ -136,7 +140,7 @@ void Mfs_ManPrint( Mfs_Man_t * p ) PRTP( "Sat", p->timeSat-p->timeInt , p->timeTotal ); PRTP( "Int", p->timeInt , p->timeTotal ); PRTP( "ALL", p->timeTotal , p->timeTotal ); - +*/ } /**Function************************************************************* diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c index a3475752..88f7554c 100644 --- a/src/opt/mfs/mfsStrash.c +++ b/src/opt/mfs/mfsStrash.c @@ -255,6 +255,87 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ) return pMan; } +/**Function************************************************************* + + Synopsis [Creates AIG for the window with constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Abc_NtkAigForConstraints( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin; + Aig_Man_t * pMan; + Aig_Obj_t * pPi, * pPo, * pObjAig, * pObjRoot; + Vec_Int_t * vOuts; + int i, k, iOut; + if ( p->pCare == NULL ) + return NULL; + pMan = Aig_ManStart( 1000 ); + // mark the care set + Aig_ManIncrementTravId( p->pCare ); + Vec_PtrForEachEntry( p->vSupp, pFanin, i ) + { + pPi = Aig_ManPi( p->pCare, (int)pFanin->pData ); + Aig_ObjSetTravIdCurrent( p->pCare, pPi ); + pPi->pData = Aig_ObjCreatePi(pMan); + } + // construct the constraints + pObjRoot = Aig_ManConst1(pMan); + Vec_PtrForEachEntry( p->vSupp, pFanin, i ) + { + vOuts = Vec_PtrEntry( p->vSuppsInv, (int)pFanin->pData ); + Vec_IntForEachEntry( vOuts, iOut, k ) + { + pPo = Aig_ManPo( p->pCare, iOut ); + if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) ) + continue; + Aig_ObjSetTravIdCurrent( p->pCare, pPo ); + if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) ) + continue; + pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan ); + if ( pObjAig == NULL ) + continue; + pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) ); + pObjRoot = Aig_And( pMan, pObjRoot, pObjAig ); + } + } + Aig_ObjCreatePo( pMan, pObjRoot ); + Aig_ManCleanup( pMan ); + return pMan; +} + +#include "fra.h" + +/**Function************************************************************* + + Synopsis [Compute the ratio of don't-cares.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode ) +{ + int nSimWords = 256; + Aig_Man_t * pMan; + Fra_Sml_t * pSim; + int Counter; + pMan = Abc_NtkAigForConstraints( p, pNode ); + pSim = Fra_SmlSimulateComb( pMan, nSimWords ); + Counter = Fra_SmlNodeCountOnes( pSim, Aig_ManPo(pMan, 0) ); + Aig_ManStop( pMan ); + Fra_SmlStop( pSim ); + return 1.0 * Counter / (32 * nSimWords); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index a04921c9..6d517b8e 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1293,6 +1293,13 @@ void sat_solver_store_free( sat_solver * s ) if ( s->pStore ) Sto_ManFree( s->pStore ); s->pStore = NULL; } + +int sat_solver_store_change_last( sat_solver * s ) +{ + extern int Sto_ManChangeLastClause( void * p ); + if ( s->pStore ) return Sto_ManChangeLastClause( s->pStore ); + return -1; +} void sat_solver_store_mark_roots( sat_solver * s ) { diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c index f968162e..31fe92ca 100644 --- a/src/sat/bsat/satStore.c +++ b/src/sat/bsat/satStore.c @@ -260,6 +260,31 @@ void Sto_ManMarkClausesA( Sto_Man_t * p ) } } +/**Function************************************************************* + + Synopsis [Returns the literal of the last clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sto_ManChangeLastClause( Sto_Man_t * p ) +{ + Sto_Cls_t * pClause, * pPrev; + pPrev = NULL; + Sto_ManForEachClause( p, pClause ) + pPrev = pClause; + assert( pPrev != NULL ); + assert( pPrev->fA == 1 ); + assert( pPrev->nLits == 1 ); + p->nClausesA--; + pPrev->fA = 0; + return pPrev->pLits[0] >> 1; +} + /**Function************************************************************* -- cgit v1.2.3