From 93c785e80250f4e7f4637d3d9317a5cf2e278b69 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 3 Jun 2016 13:22:24 -0700 Subject: Small changes for today's experiments. --- src/aig/gia/giaDup.c | 2 +- src/aig/gia/giaHash.c | 10 +++++----- src/aig/gia/giaShow.c | 11 ++++++++++- src/base/abci/abc.c | 6 ++++++ src/base/wlc/wlcBlast.c | 19 +++++++++++++++++++ src/proof/acec/acecPolyn.c | 4 ++-- 6 files changed, 43 insertions(+), 9 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 3ffb948e..a2277294 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -2949,7 +2949,7 @@ Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ) // start the new manager // Gia_ManFillValue( p ); - pNew = Gia_ManStart( Vec_PtrSize(vLeaves) + Vec_PtrSize(vNodes) + Vec_PtrSize(vRoots) + 1); + pNew = Gia_ManStart( (fTrimPis ? Vec_PtrSize(vLeaves) : Gia_ManCiNum(p)) + Vec_PtrSize(vNodes) + Vec_PtrSize(vRoots) + 1 ); pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pSpec = Abc_UtilStrsav( p->pSpec ); // map the constant node diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c index d4a47ac5..c80f9e07 100644 --- a/src/aig/gia/giaHash.c +++ b/src/aig/gia/giaHash.c @@ -575,11 +575,6 @@ int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 ) ***********************************************************************/ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 ) { - if ( p->fGiaSimple ) - { - assert( p->nHTable == 0 ); - return Gia_ManAppendAnd( p, iLit0, iLit1 ); - } if ( iLit0 < 2 ) return iLit0 ? iLit1 : 0; if ( iLit1 < 2 ) @@ -588,6 +583,11 @@ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 ) return iLit1; if ( iLit0 == Abc_LitNot(iLit1) ) return 0; + if ( p->fGiaSimple ) + { + assert( p->nHTable == 0 ); + return Gia_ManAppendAnd( p, iLit0, iLit1 ); + } if ( (p->nObjs & 0xFF) == 0 && 2 * p->nHTable < Gia_ManAndNum(p) ) Gia_ManHashResize( p ); if ( p->fAddStrash ) diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c index 9cf79ccf..039931b2 100644 --- a/src/aig/gia/giaShow.c +++ b/src/aig/gia/giaShow.c @@ -362,20 +362,29 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int fprintf( pFile, " Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id, Gia_Regular(pNode->pEquiv)->Id, Gia_IsComplement(pNode->pEquiv)? "\'":"" ); */ - fprintf( pFile, " Node%d [label = \"%d\"", i, i ); if ( vMarks && Vec_IntEntry(vMarks, i) > 0 ) { + fprintf( pFile, " Node%d [label = \"%d_%d\"", i, Vec_IntFind(vRemap, i), i ); if ( Abc_Lit2Att2(Vec_IntEntry(vMarks, i)) == 2 ) fprintf( pFile, ", shape = doubleoctagon" ); else fprintf( pFile, ", shape = octagon" ); } else if ( Gia_ObjIsXor(pNode) ) + { + fprintf( pFile, " Node%d [label = \"%d\"", i, i ); fprintf( pFile, ", shape = doublecircle" ); + } else if ( Gia_ObjIsMux(pMan, pNode) ) + { + fprintf( pFile, " Node%d [label = \"%d\"", i, i ); fprintf( pFile, ", shape = trapezium" ); + } else + { + fprintf( pFile, " Node%d [label = \"%d\"", i, i ); fprintf( pFile, ", shape = ellipse" ); + } if ( pNode->fMark0 ) fprintf( pFile, ", style = filled" ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9d21bc72..270101b7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -6878,6 +6878,12 @@ int Abc_CommandRr( Abc_Frame_t * pAbc, int argc, char ** argv ) } } + printf( "This command is obsolete." ); + printf( "To perform pure redudancy removal, try \"mfs -r\".\n" ); + printf( "To perform something a little stronger try \"mfs2\"\n" ); + printf( "When working with an AIG, use \"logic\" before and \"strash\" after this command.\n" ); + return 0; + if ( pNtk == NULL ) { Abc_Print( -1, "Empty network.\n" ); diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index f6cd9310..826dbfa1 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -1344,6 +1344,25 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple assert( Vec_PtrSize(pNew->vNamesOut) == Gia_ManCoNum(pNew) ); */ pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName ); + // dump the miter parts + if ( 0 ) + { + char pFileName0[1000], pFileName1[1000]; + char * pNameGeneric = Extra_FileNameGeneric( p->pSpec ); + Vec_Int_t * vOrder = Vec_IntStartNatural( Gia_ManPoNum(pNew) ); + Gia_Man_t * pGia0 = Gia_ManDupCones( pNew, Vec_IntArray(vOrder), Vec_IntSize(vOrder)/2, 0 ); + Gia_Man_t * pGia1 = Gia_ManDupCones( pNew, Vec_IntArray(vOrder) + Vec_IntSize(vOrder)/2, Vec_IntSize(vOrder)/2, 0 ); + assert( Gia_ManPoNum(pNew) % 2 == 0 ); + sprintf( pFileName0, "%s_lhs_.aig", pNameGeneric ); + sprintf( pFileName1, "%s_rhs_.aig", pNameGeneric ); + Gia_AigerWrite( pGia0, pFileName0, 0, 0 ); + Gia_AigerWrite( pGia1, pFileName1, 0, 0 ); + Gia_ManStop( pGia0 ); + Gia_ManStop( pGia1 ); + Vec_IntFree( vOrder ); + ABC_FREE( pNameGeneric ); + printf( "Dumped two parts of the miter into files \"%s\" and \"%s\".\n", pFileName0, pFileName1 ); + } return pNew; } diff --git a/src/proof/acec/acecPolyn.c b/src/proof/acec/acecPolyn.c index 2f98df73..be601405 100644 --- a/src/proof/acec/acecPolyn.c +++ b/src/proof/acec/acecPolyn.c @@ -311,8 +311,8 @@ void Gia_PolynBuildOne( Pln_Man_t * p, int iMono ) Vec_IntAppendMinus( p->vTempC[0], vConst, 0 ); Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[2] ); // C * y - //if ( !p->pGia->vXors || Vec_IntFind(p->pGia->vXors, iDriver) > 0 ) - { + //if ( !p->pGia->vXors || Vec_IntFind(p->pGia->vXors, iDriver) == -1 || Vec_IntFind(p->pGia->vXors, iDriver) == 5 ) + { vConst = Hsh_VecReadEntry( p->pHashC, iConst ); Vec_IntAppendMinus2x( p->vTempC[0], vConst ); Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] ); // -C * x * y -- cgit v1.2.3