summaryrefslogtreecommitdiffstats
path: root/src/aig/gia/giaNf.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia/giaNf.c')
-rw-r--r--src/aig/gia/giaNf.c106
1 files changed, 60 insertions, 46 deletions
diff --git a/src/aig/gia/giaNf.c b/src/aig/gia/giaNf.c
index 29f8679c..510e7ddb 100644
--- a/src/aig/gia/giaNf.c
+++ b/src/aig/gia/giaNf.c
@@ -1895,7 +1895,8 @@ void Nf_ManResetMatches( Nf_Man_t * p, int Round )
else
{
assert( Round > 0 || (!pDc->fBest && !pAc->fBest) );
- if ( (p->pPars->fAreaOnly || (Round & 1)) && !pAc->fCompl )
+// if ( (p->pPars->fAreaOnly || (Round & 1)) && !pAc->fCompl )
+ if ( (Round & 1) && !pAc->fCompl )
ABC_SWAP( Nf_Mat_t, *pDc, *pAc );
pDc->fBest = 1;
pAc->fBest = 0;
@@ -2185,38 +2186,59 @@ void Nf_ManUpdateStats( Nf_Man_t * p )
Vec_Int_t * vCutGates; // gates (cut -> gate)
*/
-int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec_Wec_t * vObjCuts, Vec_Int_t * vSolCuts, Vec_Int_t * vCutGates, int StartVar )
+int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec_Wec_t * vObjCuts, Vec_Int_t * vSolCuts, Vec_Int_t * vCutGates, Vec_Wrd_t * vCutAreas, word * pInvArea, int StartVar, int nVars )
{
Nf_Man_t * p = (Nf_Man_t *)pMan;
int nInputs = Gia_ManCiNum(p->pGia);
+ int LitShift = 2*nInputs+2;
Gia_Obj_t * pObj;
int c, iObj;
- Vec_Int_t * vInvCuts = Vec_IntAlloc( Gia_ManAndNum(p->pGia) );
+ if ( 2*Gia_ManAndNum(p->pGia) + Gia_ManCiNum(p->pGia) > nVars )
+ {
+ printf( "The number of variables is too large: 2*%d + %d = %d > %d.\n", Gia_ManAndNum(p->pGia), Gia_ManCiNum(p->pGia), 2*Gia_ManAndNum(p->pGia) + Gia_ManCiNum(p->pGia), nVars );
+ return 0;
+ }
+ *pInvArea = p->InvAreaW;
// save roots
Vec_IntClear( vRoots );
Gia_ManForEachCo( p->pGia, pObj, c )
- Vec_IntPush( vRoots, Gia_ObjFaninLit0p(p->pGia, pObj)-2*nInputs-2 );
+ {
+ assert( !Gia_ObjIsCi(Gia_ObjFanin0(pObj)) );
+ Vec_IntPush( vRoots, Gia_ObjFaninLit0p(p->pGia, pObj)-LitShift );
+ }
// prepare
Vec_WecClear( vCuts );
Vec_WecClear( vObjCuts );
Vec_IntClear( vSolCuts );
Vec_IntClear( vCutGates );
+ Vec_WrdClear( vCutAreas );
// collect cuts for each node
Gia_ManForEachAndId( p->pGia, iObj )
{
- Vec_Int_t * vObj[2], * vCut;
+ Vec_Int_t * vObj[2], * vCutOne;
int iCut, * pCut, * pCutSet;
int iCutInv[2] = {-1, -1};
// get matches
- Nf_Mat_t * pM[2];
+ Nf_Mat_t * pM[2] = {NULL, NULL};
for ( c = 0; c < 2; c++ )
- pM[c] = Nf_ObjMapRefNum(p, iObj, c) ? Nf_ObjMatchBest(p, iObj, c) : NULL;
+ {
+ if ( Nf_ObjMapRefNum(p, iObj, c) == 0 )
+ continue;
+ if ( Nf_ObjMatchBest(p, iObj, c)->fCompl )
+ {
+ assert( iCutInv[c] == -1 );
+ iCutInv[c] = Vec_IntSize(vSolCuts);
+ Vec_IntPush( vSolCuts, -1 );
+ continue;
+ }
+ pM[c] = Nf_ObjMatchBest(p, iObj, c);
+ }
// start collecting cuts of pos-obj and neg-obj
- assert( Vec_WecSize(vObjCuts) == 2*(iObj-nInputs-1) );
+ assert( Vec_WecSize(vObjCuts) == 2*iObj-LitShift );
for ( c = 0; c < 2; c++ )
{
vObj[c] = Vec_WecPushLevel( vObjCuts );
- Vec_IntPush( vObj[c], Abc_Var2Lit(Abc_Var2Lit(iObj-nInputs-1, c), 1) );
+ Vec_IntPush( vObj[c], Abc_Var2Lit(Abc_Var2Lit(iObj, c)-LitShift, 1) );
}
// enumerate cuts
pCutSet = Nf_ObjCutSet( p, iObj );
@@ -2239,6 +2261,7 @@ int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec
Mio_Cell2_t*pC = Nf_ManCell( p, Info );
assert( nFans == (int)pC->nFanins );
Vec_IntPush( vCutGates, Info );
+ Vec_WrdPush( vCutAreas, pC->AreaW );
// to make comparison possible
Cfg.fCompl = 0;
// add solution cut
@@ -2246,31 +2269,26 @@ int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec
{
if ( pM[c] == NULL )
continue;
- if ( pM[c]->fCompl )
- {
- assert( iCutInv[c] == -1 );
- iCutInv[c] = Vec_IntSize(vSolCuts);
- Vec_IntPush( vSolCuts, -1 );
- printf( "adding inv for %d\n", Abc_Var2Lit(iObj-nInputs-1, c) );
- }
- else if ( (int)pM[c]->CutH == Nf_CutHandle(pCutSet, pCut) && (int)pM[c]->Gate == Info && Nf_Cfg2Int(pM[c]->Cfg) == Nf_Cfg2Int(Cfg) )
+ if ( (int)pM[c]->CutH == Nf_CutHandle(pCutSet, pCut) && (int)pM[c]->Gate == Info && Nf_Cfg2Int(pM[c]->Cfg) == Nf_Cfg2Int(Cfg) )
{
Vec_IntPush( vSolCuts, Vec_WecSize(vCuts) );
- printf( "adding solution for %d\n", Abc_Var2Lit(iObj-nInputs-1, c) );
+ //printf( "adding solution for %d\n", Abc_Var2Lit(iObj, c)-LitShift );
}
}
// add new cut
iCutLit = Abc_Var2Lit( StartVar + Vec_WecSize(vCuts), 0 );
- vCut = Vec_WecPushLevel( vCuts );
+ vCutOne = Vec_WecPushLevel( vCuts );
// add literals
- Vec_IntPush( vCut, Abc_Var2Lit(iObj, fCompl) );
+ Vec_IntPush( vCutOne, Abc_Var2Lit(iObj, fCompl) );
Vec_IntPush( vObj[fCompl], iCutLit );
Nf_CfgForEachVarCompl( Cfg, nFans, iFanin, fComplF, k )
- if ( pFans[iFanin] >= nInputs + 1 ) // and-node
+ if ( pFans[iFanin] >= nInputs + 1 ) // internal node
{
- Vec_IntPush( vCut, Abc_Var2Lit(pFans[iFanin], fComplF) );
- Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(pFans[iFanin]-nInputs-1, fComplF)), iCutLit );
+ Vec_IntPush( vCutOne, Abc_Var2Lit(pFans[iFanin], fComplF) );
+ //Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(pFans[iFanin], fComplF)-LitShift), iCutLit );
}
+ else if ( fComplF ) // complemented primary input
+ Vec_IntPush( vCutOne, Abc_Var2Lit(pFans[iFanin], 1) );
}
}
}
@@ -2280,29 +2298,27 @@ int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec
{
if ( iCutInv[c] != -1 )
Vec_IntWriteEntry( vSolCuts, iCutInv[c], Vec_WecSize(vCuts) );
- Vec_IntPush( vInvCuts, Abc_Var2Lit(StartVar + Vec_WecSize(vCuts), 0) );
- vCut = Vec_WecPushLevel( vCuts );
- Vec_IntPush( vCut, Abc_Var2Lit(iObj, c) );
- Vec_IntPush( vCut, Abc_Var2Lit(iObj, !c) );
+ // the obj-lit implies its cut
+ Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(iObj, c)-LitShift), Abc_Var2Lit(StartVar + Vec_WecSize(vCuts), 0) );
+ // the cut includes both literals
+ vCutOne = Vec_WecPushLevel( vCuts );
+ Vec_IntPush( vCutOne, Abc_Var2Lit(iObj, c) );
+ Vec_IntPush( vCutOne, Abc_Var2Lit(iObj, !c) );
Vec_IntPush( vCutGates, 3 );
+ Vec_WrdPush( vCutAreas, p->InvAreaW );
}
}
- assert( Vec_WecSize(vObjCuts) == Vec_IntSize(vInvCuts) );
- Gia_ManForEachAndId( p->pGia, iObj )
- {
- int iCutInv[2];
- for ( c = 0; c < 2; c++ )
- iCutInv[c] = Vec_IntEntry(vInvCuts, Abc_Var2Lit(iObj-nInputs-1, c));
- for ( c = 0; c < 2; c++ )
- {
- Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(iObj-nInputs-1, c)), iCutInv[0] );
- Vec_IntPush( Vec_WecEntry(vObjCuts, Abc_Var2Lit(iObj-nInputs-1, c)), iCutInv[1] );
- }
- }
- Vec_IntFree( vInvCuts );
+// for ( c = 0; c < p->nCells; c++ )
+// printf( "%d=%s ", c, p->pCells[c].pName );
+// printf( "\n" );
+ // add complemented inputs
+ Gia_ManForEachCiId( p->pGia, iObj, c )
+ if ( Nf_ObjMapRefNum(p, iObj, 1) )
+ Vec_IntPush( vSolCuts, -(2*Gia_ManAndNum(p->pGia)+c) );
assert( Vec_WecSize(vCuts) == Vec_IntSize(vCutGates) );
+ assert( Vec_WecSize(vCuts) == Vec_WrdSize(vCutAreas) );
assert( Vec_WecSize(vObjCuts) == 2*Gia_ManAndNum(p->pGia) );
- return 2*nInputs+2;
+ return nInputs;
}
/**Function*************************************************************
@@ -2390,13 +2406,11 @@ Gia_Man_t * Nf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
}
Nf_ManFixPoDrivers( p );
pNew = Nf_ManDeriveMapping( p );
-
- // experimental mapper
+ if ( pPars->fAreaOnly )
{
-// extern int Sbm_ManTestSat( void * p );
-// Sbm_ManTestSat( p );
+ int Sbm_ManTestSat( void * pMan );
+ Sbm_ManTestSat( p );
}
-
Nf_StoDelete( p );
return pNew;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-22 19:37:15 +0000