diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-01 13:43:33 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-01 13:43:33 -0700 |
commit | 99e8ef14cbff5e53daf37ff8206bba1c17758970 (patch) | |
tree | f4de60afce4ff8b6d0543efd8b28416fc90d29e3 /src | |
parent | e7ddde3f5a92e75496a7bd5d95315ef8cce7bd18 (diff) | |
download | abc-99e8ef14cbff5e53daf37ff8206bba1c17758970.tar.gz abc-99e8ef14cbff5e53daf37ff8206bba1c17758970.tar.bz2 abc-99e8ef14cbff5e53daf37ff8206bba1c17758970.zip |
Scalable gate-level abstraction.
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaAbsGla2.c | 338 | ||||
-rw-r--r-- | src/aig/gia/giaUtil.c | 2 |
2 files changed, 267 insertions, 73 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index d82bd609..fc5d2962 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -102,7 +102,7 @@ static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) // inserts literal of this object static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Lit ) { - assert( Lit > 1 ); +// assert( Lit > 1 ); assert( Ga2_ObjFindLit(p, pObj, f) == -1 ); Vec_IntSetEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj), Lit ); } @@ -115,7 +115,7 @@ static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) Lit = toLitCond( p->nSatVars++, 0 ); Ga2_ObjAddLit( p, pObj, f, Lit ); } - assert( Lit > 1 ); +// assert( Lit > 1 ); return Lit; } @@ -235,6 +235,7 @@ void Ga2_ManCollectLeaves_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLea } int Ga2_ManMarkup( Gia_Man_t * p, int N ) { + int fSimple = 1; static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; clock_t clk = clock(); Vec_Int_t * vLeaves; @@ -243,45 +244,50 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N ) vLeaves = Vec_IntAlloc( 100 ); - // label nodes with multiple fanouts and inputs MUXes - Gia_ManForEachObj( p, pObj, i ) + if ( fSimple ) { - pObj->Value = 0; - if ( !Gia_ObjIsAnd(pObj) ) - continue; - Gia_ObjFanin0(pObj)->Value++; - Gia_ObjFanin1(pObj)->Value++; - if ( !Gia_ObjIsMuxType(pObj) ) - continue; - Gia_ObjFanin0(Gia_ObjFanin0(pObj))->Value++; - Gia_ObjFanin1(Gia_ObjFanin0(pObj))->Value++; - Gia_ObjFanin0(Gia_ObjFanin1(pObj))->Value++; - Gia_ObjFanin1(Gia_ObjFanin1(pObj))->Value++; + Gia_ManForEachObj( p, pObj, i ) + pObj->fPhase = !Gia_ObjIsCo(pObj); } - Gia_ManForEachObj( p, pObj, i ) - { - pObj->fPhase = 0; - if ( Gia_ObjIsAnd(pObj) ) - pObj->fPhase = (pObj->Value > 1); - else if ( Gia_ObjIsCo(pObj) ) - Gia_ObjFanin0(pObj)->fPhase = 1; - else - pObj->fPhase = 1; - } - // add marks when needed - Gia_ManForEachAnd( p, pObj, i ) + else { - if ( !pObj->fPhase ) - continue; - Vec_IntClear( vLeaves ); - Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 ); - if ( Vec_IntSize(vLeaves) > N ) - Ga2_ManBreakTree_rec( p, pObj, 1, N ); + // label nodes with multiple fanouts and inputs MUXes + Gia_ManForEachObj( p, pObj, i ) + { + pObj->Value = 0; + if ( !Gia_ObjIsAnd(pObj) ) + continue; + Gia_ObjFanin0(pObj)->Value++; + Gia_ObjFanin1(pObj)->Value++; + if ( !Gia_ObjIsMuxType(pObj) ) + continue; + Gia_ObjFanin0(Gia_ObjFanin0(pObj))->Value++; + Gia_ObjFanin1(Gia_ObjFanin0(pObj))->Value++; + Gia_ObjFanin0(Gia_ObjFanin1(pObj))->Value++; + Gia_ObjFanin1(Gia_ObjFanin1(pObj))->Value++; + } + Gia_ManForEachObj( p, pObj, i ) + { + pObj->fPhase = 0; + if ( Gia_ObjIsAnd(pObj) ) + pObj->fPhase = (pObj->Value > 1); + else if ( Gia_ObjIsCo(pObj) ) + Gia_ObjFanin0(pObj)->fPhase = 1; + else + pObj->fPhase = 1; + } + // add marks when needed + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !pObj->fPhase ) + continue; + Vec_IntClear( vLeaves ); + Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 ); + if ( Vec_IntSize(vLeaves) > N ) + Ga2_ManBreakTree_rec( p, pObj, 1, N ); + } } -// Gia_ManForEachObj( p, pObj, i ) -// pObj->fPhase = !Gia_ObjIsCo(pObj); - // verify that the tree is split correctly Vec_IntFreeP( &p->vMapping ); p->vMapping = Vec_IntStart( Gia_ManObjNum(p) ); @@ -464,22 +470,59 @@ static inline unsigned Ga2_ObjTruthDepends( unsigned t, int v ) } unsigned Ga2_ObjComputeTruthSpecial( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vLits ) { + int fVerbose = 0; static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + unsigned Res, uLeaves[5]; Gia_Obj_t * pObj; - int i, Entry; - unsigned Res; + int i, k, Lit, Entry, pMap[5]; + int Id = Gia_ObjId(p, pRoot); + assert( Gia_ObjIsAnd(pRoot) ); + if ( 4948 == Id ) + { + int s = 0; + } + + if ( fVerbose ) + printf( "Object %d.\n", Gia_ObjId(p, pRoot) ); + // assign elementary truth tables Gia_ManForEachObjVec( vLeaves, p, pObj, i ) { + pMap[i] = i; Entry = Vec_IntEntry( vLits, i ); assert( Entry >= 0 ); if ( Entry == 0 ) - pObj->Value = 0; + pObj->Value = uLeaves[i] = 0; else if ( Entry == 1 ) - pObj->Value = ~0; + pObj->Value = uLeaves[i] = ~0; else // non-trivial literal - pObj->Value = uTruth5[i]; + { + pObj->Value = uLeaves[i] = uTruth5[i]; + // check if this literal already encountered + Vec_IntForEachEntryStop( vLits, Lit, k, i ) + if ( Abc_Lit2Var(Lit) == Abc_Lit2Var(Entry) ) + { + if ( Lit == Entry ) + pObj->Value = uLeaves[i] = uLeaves[k]; + else if ( Lit == Abc_LitNot(Entry) ) + pObj->Value = uLeaves[i] = ~uLeaves[k]; + else assert( 0 ); + pMap[i] = k; + break; + } + } + + if ( fVerbose ) + printf( "%d ", Entry ); } + + if ( fVerbose ) + { + Res = Ga2_ObjTruth( p, pRoot ); + Kit_DsdPrintFromTruth( &Res, Vec_IntSize(vLeaves) ); + printf( "\n" ); + } + // compute truth table Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 ); if ( Res != 0 && Res != ~0 ) @@ -495,16 +538,32 @@ unsigned Ga2_ObjComputeTruthSpecial( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t assert( Vec_IntEntry(vLits, pUsed[0]) <= Vec_IntEntry(vLits, pUsed[nUsed-1]) ); // assign elementary truth tables to the leaves Gia_ManForEachObjVec( vLeaves, p, pObj, i ) - pObj->Value = 0; + { + Entry = Vec_IntEntry( vLits, i ); + assert( Entry >= 0 ); + if ( Entry == 0 ) + pObj->Value = 0; + else if ( Entry == 1 ) + pObj->Value = ~0; + else // non-trivial literal + pObj->Value = 0xDEADCAFE; // not important + } for ( i = 0; i < nUsed; i++ ) { Entry = Vec_IntEntry( vLits, pUsed[i] ); assert( Entry > 1 ); pObj = Gia_ManObj( p, Vec_IntEntry(vLeaves, pUsed[i]) ); pObj->Value = Abc_LitIsCompl(Entry) ? ~uTruth5[i] : uTruth5[i]; +// pObj->Value = uTruth5[i]; // remember this literal pUsed[i] = Abc_LitRegular(Entry); +// pUsed[i] = Entry; } + // update using the map + Gia_ManForEachObjVec( vLeaves, p, pObj, i ) + if ( pMap[i] != i ) + pObj->Value = Gia_ManObj( p, Vec_IntEntry(vLeaves, pMap[i]) )->Value; + // compute truth table Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 ); // reload the literals @@ -513,10 +572,29 @@ unsigned Ga2_ObjComputeTruthSpecial( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t { Vec_IntPush( vLits, pUsed[i] ); assert( Ga2_ObjTruthDepends(Res, i) ); + if ( fVerbose ) + printf( "%d ", pUsed[i] ); } + for ( ; i < 5; i++ ) + assert( !Ga2_ObjTruthDepends(Res, i) ); + +if ( fVerbose ) +{ + Kit_DsdPrintFromTruth( &Res, nUsed ); + printf( "\n" ); +} + } else - Vec_IntClear( vLits ); + { + +if ( fVerbose ) +{ + Vec_IntClear( vLits ); + printf( "Const %d\n", Res > 0 ); +} + + } return Res; } @@ -554,10 +632,14 @@ Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover ) SeeAlso [] ***********************************************************************/ -static inline void Ga2_ManCnfAddDynamic( Ga2_Man_t * p, int uTruth, int Lits[], int iLitOut ) +static inline void Ga2_ManCnfAddDynamic( Ga2_Man_t * p, int uTruth, int Lits[], int iLitOut, int ProofId ) { int i, k, b, Cube, nClaLits, ClaLits[6]; - assert( uTruth > 0 && uTruth < 0xffff ); +// assert( uTruth > 0 && uTruth < 0xffff ); + if ( uTruth == 0 ) + { + int s = 0; + } // write positive/negative polarity for ( i = 0; i < 2; i++ ) { @@ -583,7 +665,7 @@ static inline void Ga2_ManCnfAddDynamic( Ga2_Man_t * p, int uTruth, int Lits[], } Cube = Cube / 3; } - sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, -1 ); + sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, ProofId ); } } } @@ -608,13 +690,13 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In if ( Literal == 1 ) // value 0 --> add positive literal { // pCube[b] = '0'; - assert( Lits[b] > 1 ); +// assert( Lits[b] > 1 ); ClaLits[nClaLits++] = Lits[b]; } else if ( Literal == 2 ) // value 1 --> add negative literal { // pCube[b] = '1'; - assert( Lits[b] > 1 ); +// assert( Lits[b] > 1 ); ClaLits[nClaLits++] = lit_neg(Lits[b]); } else if ( Literal != 0 ) @@ -626,7 +708,6 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, ProofId ); } } - b = 0; } @@ -641,7 +722,7 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In SeeAlso [] ***********************************************************************/ -void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs ) +static inline void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs ) { unsigned uTruth; int nLeaves; @@ -674,47 +755,152 @@ void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs ) Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(~uTruth, nLeaves, p->vIsopMem) ); } -void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) +static inline void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) { Vec_Int_t * vLeaves; - Gia_Obj_t * pFanin; - int k, iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f ); - assert( !Gia_ObjIsConst0(pObj) ); + Gia_Obj_t * pLeaf; + int k, Lit, iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f ); assert( iLitOut > 1 ); - assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) ); - if ( f == 0 && Gia_ObjIsRo(p->pGia, pObj) ) + assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) ); + if ( Gia_ObjIsConst0(pObj) || (f == 0 && Gia_ObjIsRo(p->pGia, pObj)) ) { iLitOut = Abc_LitNot( iLitOut ); sat_solver2_addclause( p->pSat, &iLitOut, &iLitOut + 1, Gia_ObjId(p->pGia, pObj) ); } else { + int fUseStatic = 1; + Vec_IntClear( p->vLits ); vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); + Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k ) + { + Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f - Gia_ObjIsRo(p->pGia, pObj) ); + Vec_IntPush( p->vLits, Lit ); + if ( Lit < 2 ) + fUseStatic = 0; + } + if ( fUseStatic || Gia_ObjIsRo(p->pGia, pObj) ) + Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) ); + else + { + unsigned uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits ); + Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) ); + } + } +} +static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) +{ + int Id = Gia_ObjId(p->pGia, pObj); + Vec_Int_t * vLeaves; + Gia_Obj_t * pLeaf; + unsigned uTruth; + int i, Lit; + assert( Ga2_ObjIsAbs0(p, pObj) ); + assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) ); + if ( Gia_ObjIsConst0(pObj) || (f == 0 && Gia_ObjIsRo(p->pGia, pObj)) ) + { + Ga2_ObjAddLit( p, pObj, f, 0 ); + } + else if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + // if flop is included in the abstraction, but its driver is not + // flop input driver has no variable assigned -- we assign it here + pLeaf = Gia_ObjRoToRi( p->pGia, pObj ); + Lit = Ga2_ObjFindOrAddLit( p, Gia_ObjFanin0(pLeaf), f-1 ); + assert( Lit >= 0 ); + Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(pLeaf) ); + Ga2_ObjAddLit( p, pObj, f, Lit ); + } + else + { + int pLits[5]; + assert( Gia_ObjIsAnd(pObj) ); Vec_IntClear( p->vLits ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) - Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f - Gia_ObjIsRo(p->pGia, pObj) ) ); - Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) ); + vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); + Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, i ) + { + if ( Ga2_ObjIsAbs0(p, pLeaf) ) // belongs to original abstraction + { + Lit = Ga2_ObjFindLit( p, pLeaf, f ); + assert( Lit >= 0 ); + } + else if ( Ga2_ObjIsLeaf0(p, pLeaf) ) // belongs to original PPIs + { +// Lit = Ga2_ObjFindLit( p, pLeaf, f ); + Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f ); + if ( Lit == -1 ) + { + Lit = GA2_BIG_NUM + i; + assert( 0 ); + } + } + else assert( 0 ); + Vec_IntPush( p->vLits, (pLits[i] = Lit) ); + } + + // minimize truth table + uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits ); + if ( uTruth == 0 || uTruth == ~0 ) // const 0 / 1 + { + Lit = (uTruth > 0); + Ga2_ObjAddLit( p, pObj, f, Lit ); + } + else if ( uTruth == 0xAAAAAAAA || uTruth == 0x55555555 ) // buffer / inverter + { + Lit = Vec_IntEntry( p->vLits, 0 ); + if ( Lit >= GA2_BIG_NUM ) + { + pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit-GA2_BIG_NUM) ); + Lit = Ga2_ObjFindLit( p, pLeaf, f ); + assert( Lit == -1 ); + Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f ); + } + assert( Lit >= 0 ); + Lit = Abc_LitNotCond( Lit, uTruth == 0x55555555 ); + Ga2_ObjAddLit( p, pObj, f, Lit ); + } + else + { + assert( Vec_IntSize(p->vLits) > 1 && Vec_IntSize(p->vLits) < 6 ); + // replace literals + Vec_IntForEachEntry( p->vLits, Lit, i ) + { + if ( Lit >= GA2_BIG_NUM ) + { + pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit-GA2_BIG_NUM) ); + Lit = Ga2_ObjFindLit( p, pLeaf, f ); + assert( Lit == -1 ); + Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f ); + Vec_IntWriteEntry( p->vLits, i, Lit ); + } + } + // perform structural hashing here!!! + + + // add new nodes + Lit = Ga2_ObjFindOrAddLit(p, pObj, f); + if ( Vec_IntSize(p->vLits) == 5 ) + Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), pLits, Lit, -1 ); + else + Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), Lit, -1 ); + } } } void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f ) { - int fSimple = 1; + int fSimple = 0; Gia_Obj_t * pObj; - int i, Lit; - if ( fSimple ) - { - Lit = Ga2_ObjFindOrAddLit( p, Gia_ManConst0(p->pGia), f ); - Lit = Abc_LitNot( Lit ); - sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, -1 ); - } + int i; // add variables for the leaves Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i ) { - if ( !i ) continue; if ( i == p->LimAbs ) break; - Ga2_ManAddToAbsOneStatic( p, pObj, f ); + if ( fSimple ) + Ga2_ManAddToAbsOneStatic( p, pObj, f ); + else + Ga2_ManAddToAbsOneDynamic( p, pObj, f ); } Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i ) if ( i >= p->LimAbs ) @@ -825,6 +1011,7 @@ Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p ) Vec_IntWriteEntry( vGateClasses, Gia_ObjId(p->pGia, pObj), 1 ); else if ( !Gia_ObjIsConst0(pObj) ) assert( 0 ); +// Gia_ObjPrint( p->pGia, pObj ); } return vGateClasses; } @@ -882,6 +1069,7 @@ void Ga2_ManRestart( Ga2_Man_t * p ) SeeAlso [] ***********************************************************************/ +/* int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) { int fSimple = 1; @@ -977,7 +1165,7 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) } return Lit; } - +*/ /**Function************************************************************* Synopsis [] @@ -1016,6 +1204,8 @@ static inline int Ga2_ObjSatValue( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) assert( !Gia_ObjIsConst0(pObj) ); if ( Lit == -1 ) return 0; + if ( Abc_Lit2Var(Lit) >= p->pSat->size ) + return 0; return Abc_LitIsCompl(Lit) ^ sat_solver2_var_value( p->pSat, Abc_Lit2Var(Lit) ); } void Ga2_GlaPrepareCexAndMap( Ga2_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pvMaps ) @@ -1153,7 +1343,7 @@ void Ga2_ManAbsPrintFrame( Ga2_Man_t * p, int nFrames, int nConfls, int nCexes, Abc_PrintInt( sat_solver2_nlearnts(p->pSat) ); Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC ); Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) ); - Abc_Print( 1, "%s", fFinal ? "\n" : "\n" ); + Abc_Print( 1, "%s", (fFinal && nCexes) ? "\n" : "\r" ); fflush( stdout ); } @@ -1237,7 +1427,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(Gia_ManPo(pAig,0)), f ); assert( Lit >= 0 ); Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(Gia_ManPo(pAig,0)) ); + if ( Lit == 0 ) + continue; + assert( Lit > 1 ); // check for counter-examples + sat_solver2_setnvars( p->pSat, p->nSatVars ); nVarsOld = p->nSatVars; for ( c = 0; ; c++ ) { @@ -1319,7 +1513,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { Vec_IntFreeP( &pAig->vGateClasses ); pAig->vGateClasses = Ga2_ManAbsTranslate( p ); - printf( "\n" ); +// printf( "\n" ); break; // temporary } } diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 01e2b1bd..72fdf307 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1125,7 +1125,7 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ) else if ( Gia_ObjIsPo(p, pObj) ) printf( "PO( %4d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") ); else if ( Gia_ObjIsCi(pObj) ) - printf( "RO" ); + printf( "RO( %4d%s )", Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)), (Gia_ObjFaninC0(Gia_ObjRoToRi(p, pObj))? "\'" : " ") ); else if ( Gia_ObjIsCo(pObj) ) printf( "RI( %4d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") ); // else if ( Gia_ObjIsBuf(pObj) ) |