summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/aig/aigInter.c111
-rw-r--r--src/aig/bdc/bdc.h2
-rw-r--r--src/aig/bdc/bdcCore.c128
-rw-r--r--src/aig/bdc/bdcDec.c407
-rw-r--r--src/aig/bdc/bdcInt.h31
-rw-r--r--src/aig/bdc/bdcTable.c24
-rw-r--r--src/aig/fra/fra.h1
-rw-r--r--src/aig/fra/fraSim.c21
-rw-r--r--src/base/abc/abcSop.c15
-rw-r--r--src/base/abci/abc.c13
-rw-r--r--src/base/abci/abcDar.c32
-rw-r--r--src/base/abci/abcIf.c87
-rw-r--r--src/base/cmd/cmd.c19
-rw-r--r--src/map/if/if.h1
-rw-r--r--src/opt/mfs/mfsCore.c4
-rw-r--r--src/opt/mfs/mfsInt.h2
-rw-r--r--src/opt/mfs/mfsMan.c10
-rw-r--r--src/opt/mfs/mfsStrash.c81
-rw-r--r--src/sat/bsat/satSolver.c7
-rw-r--r--src/sat/bsat/satStore.c25
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
@@ -45,10 +45,108 @@ extern int timeInt;
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 []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
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<<p->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,75 +24,12 @@
/// 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.]
Description []
@@ -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<<p->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*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 10:57:51 +0000