From 652b2792345978c34ea614800b76996930a21a49 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 8 May 2016 19:01:46 -0700 Subject: Experiments with CEC for arithmetic circuits. --- src/aig/gia/gia.h | 2 +- src/aig/gia/giaShow.c | 235 ++++++++++++++++++++++++++++++++++++++++++--- src/base/abci/abc.c | 34 +++++-- src/proof/acec/acec.h | 13 ++- src/proof/acec/acecCore.c | 10 +- src/proof/acec/acecFadds.c | 66 +++++++++---- src/proof/acec/acecInt.h | 7 -- src/proof/acec/acecOrder.c | 172 ++++++++++++++++++++------------- src/proof/acec/acecPolyn.c | 44 ++++++--- 9 files changed, 447 insertions(+), 136 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 390dbafb..ab6870d8 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1389,7 +1389,7 @@ extern Gia_Man_t * Gia_ManCleanupOutputs( Gia_Man_t * p, int nOutputs ); extern Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose ); /*=== giaShow.c ===========================================================*/ -extern void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold ); +extern void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders ); /*=== giaShrink.c ===========================================================*/ extern Gia_Man_t * Gia_ManMapShrink4( Gia_Man_t * p, int fKeepLevel, int fVerbose ); extern Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int nFanoutMax, int fKeepLevel, int fVerbose ); diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c index 6224d37f..91edbaa5 100644 --- a/src/aig/gia/giaShow.c +++ b/src/aig/gia/giaShow.c @@ -19,6 +19,8 @@ ***********************************************************************/ #include "gia.h" +#include "proof/cec/cec.h" +#include "proof/acec/acec.h" ABC_NAMESPACE_IMPL_START @@ -31,6 +33,147 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +/* +Vec_Int_t * Gia_WriteDotAigMarks( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds ) +{ + int i; + Vec_Int_t * vMarks = Vec_IntStart( Gia_ManObjNum(p) ); + for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ ) + { + Vec_IntWriteEntry( vMarks, Vec_IntEntry(vHadds, 2*i+0), Abc_Var2Lit(i+1, 0) ); + Vec_IntWriteEntry( vMarks, Vec_IntEntry(vHadds, 2*i+1), Abc_Var2Lit(i+1, 0) ); + } + for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ ) + { + Vec_IntWriteEntry( vMarks, Vec_IntEntry(vFadds, 5*i+3), Abc_Var2Lit(i+1, 1) ); + Vec_IntWriteEntry( vMarks, Vec_IntEntry(vFadds, 5*i+4), Abc_Var2Lit(i+1, 1) ); + } + return vMarks; +} +int Gia_WriteDotAigLevel_rec( Gia_Man_t * p, Vec_Int_t * vMarks, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int Id, Vec_Int_t * vLevel ) +{ + int Level = Vec_IntEntry(vLevel, Id), Mark = Vec_IntEntry(vMarks, Id); + if ( Level || Mark == -1 ) + return Level; + if ( Mark == 0 ) + { + Gia_Obj_t * pObj = Gia_ManObj( p, Id ); + int Level0 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId0(pObj, Id), vLevel ); + int Level1 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId1(pObj, Id), vLevel ); + Level = Abc_MaxInt(Level0, Level1) + 1; + Vec_IntWriteEntry( vLevel, Id, Level ); + Vec_IntWriteEntry( vMarks, Id, -1 ); + } + else if ( Abc_LitIsCompl(Mark) ) // FA + { + int i, * pFanins = Vec_IntEntryP( vFadds, 5*(Abc_Lit2Var(Mark)-1) ); + assert( pFanins[3] == Id || pFanins[4] == Id ); + for ( i = 0; i < 3; i++ ) + Level = Abc_MaxInt( Level, Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, pFanins[i], vLevel ) ); + Vec_IntWriteEntry( vLevel, pFanins[3], Level+1 ); + Vec_IntWriteEntry( vLevel, pFanins[4], Level+1 ); + } + else // HA + { + int * pFanins = Vec_IntEntryP( vHadds, 2*(Abc_Lit2Var(Mark)-1) ); + Gia_Obj_t * pObj = Gia_ManObj( p, pFanins[1] ); + int Level0 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId0(pObj, Id), vLevel ); + int Level1 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId1(pObj, Id), vLevel ); + assert( pFanins[0] == Id || pFanins[1] == Id ); + Level = Abc_MaxInt(Level0, Level1) + 1; + Vec_IntWriteEntry( vLevel, pFanins[0], Level ); + Vec_IntWriteEntry( vLevel, pFanins[1], Level ); + } + return Level; +} +int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds, Vec_Int_t ** pvMarks, Vec_Int_t ** pvLevel ) +{ + Vec_Int_t * vMarks = Gia_WriteDotAigMarks( p, vFadds, vHadds ); + Vec_Int_t * vLevel = Vec_IntStart( Gia_ManObjNum(p) ); + int i, Id, Level = 0; + Vec_IntWriteEntry( vMarks, 0, -1 ); + Gia_ManForEachCiId( p, Id, i ) + Vec_IntWriteEntry( vMarks, Id, -1 ); + Gia_ManForEachCoDriverId( p, Id, i ) + Level = Abc_MaxInt( Level, Gia_WriteDotAigLevel_rec(p, vMarks, vFadds, vHadds, Id, vLevel) ); + Gia_ManForEachCoId( p, Id, i ) + Vec_IntWriteEntry( vMarks, Id, -1 ); + *pvMarks = vMarks; + *pvLevel = vLevel; + return Level; +} +*/ +int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds, Vec_Int_t * vRecord, Vec_Int_t ** pvLevel, Vec_Int_t ** pvMarks, Vec_Int_t ** pvRemap ) +{ + Vec_Int_t * vLevel = Vec_IntStart( Gia_ManObjNum(p) ); + Vec_Int_t * vMarks = Vec_IntStart( Gia_ManObjNum(p) ); + Vec_Int_t * vRemap = Vec_IntStartNatural( Gia_ManObjNum(p) ); + int i, k, Id, Entry, LevelMax = 0; + + Vec_IntWriteEntry( vMarks, 0, -1 ); + Gia_ManForEachCiId( p, Id, i ) + Vec_IntWriteEntry( vMarks, Id, -1 ); + Gia_ManForEachCoId( p, Id, i ) + Vec_IntWriteEntry( vMarks, Id, -1 ); + + Vec_IntForEachEntry( vRecord, Entry, i ) + { + int Level = 0; + int Node = Abc_Lit2Var2(Entry); + int Attr = Abc_Lit2Att2(Entry); + if ( Attr == 2 ) + { + int * pFanins = Vec_IntEntryP( vFadds, 5*Node ); + for ( k = 0; k < 3; k++ ) + Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, pFanins[k]) ); + Vec_IntWriteEntry( vLevel, pFanins[3], Level+1 ); + Vec_IntWriteEntry( vLevel, pFanins[4], Level+1 ); + Vec_IntWriteEntry( vMarks, pFanins[4], Entry ); + Vec_IntWriteEntry( vRemap, pFanins[3], pFanins[4] ); + //printf( "Making FA output %d.\n", pFanins[4] ); + } + else if ( Attr == 1 ) + { + int * pFanins = Vec_IntEntryP( vHadds, 2*Node ); + Gia_Obj_t * pObj = Gia_ManObj( p, pFanins[1] ); + int pFaninsIn[2] = { Gia_ObjFaninId0(pObj, pFanins[1]), Gia_ObjFaninId1(pObj, pFanins[1]) }; + for ( k = 0; k < 2; k++ ) + Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, pFaninsIn[k]) ); + Vec_IntWriteEntry( vLevel, pFanins[0], Level+1 ); + Vec_IntWriteEntry( vLevel, pFanins[1], Level+1 ); + Vec_IntWriteEntry( vMarks, pFanins[1], Entry ); + Vec_IntWriteEntry( vRemap, pFanins[0], pFanins[1] ); + //printf( "Making HA output %d.\n", pFanins[1] ); + } + else + { + Gia_Obj_t * pObj = Gia_ManObj( p, Node ); + int pFaninsIn[2] = { Gia_ObjFaninId0(pObj, Node), Gia_ObjFaninId1(pObj, Node) }; + for ( k = 0; k < 2; k++ ) + Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, pFaninsIn[k]) ); + Vec_IntWriteEntry( vLevel, Node, Level+1 ); + Vec_IntWriteEntry( vMarks, Node, -1 ); + //printf( "Making node %d.\n", Node ); + } + LevelMax = Abc_MaxInt( LevelMax, Level+1 ); + } + *pvLevel = vLevel; + *pvMarks = vMarks; + *pvRemap = vRemap; + return LevelMax; +} + /**Function************************************************************* Synopsis [Writes the graph structure of AIG for DOT.] @@ -43,16 +186,17 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) +void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int fAdders ) { + Vec_Int_t * vFadds = NULL, * vHadds = NULL, * vRecord = NULL, * vMarks = NULL, * vRemap = NULL; FILE * pFile; Gia_Obj_t * pNode;//, * pTemp, * pPrev; int LevelMax, Prev, Level, i; int fConstIsUsed = 0; - if ( Gia_ManAndNum(pMan) > 300 ) + if ( Gia_ManAndNum(pMan) > 1000 ) { - fprintf( stdout, "Cannot visualize AIG with more than 300 nodes.\n" ); + fprintf( stdout, "Cannot visualize AIG with more than 1000 nodes.\n" ); return; } if ( (pFile = fopen( pFileName, "w" )) == NULL ) @@ -71,7 +215,18 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) pNode->fMark0 = 1; // compute levels - LevelMax = 1 + Gia_ManLevelNum( pMan ); + if ( fAdders ) + { + Vec_IntFreeP( &pMan->vLevels ); + vFadds = Gia_ManDetectFullAdders( pMan, 0 ); + vHadds = Gia_ManDetectHalfAdders( pMan, 0 ); + vRecord = Gia_PolynFindOrder( pMan, vFadds, vHadds, 0, 0 ); + LevelMax = 1 + Gia_WriteDotAigLevel( pMan, vFadds, vHadds, vRecord, &pMan->vLevels, &vMarks, &vRemap ); + } + else + LevelMax = 1 + Gia_ManLevelNum( pMan ); + + // set output levels Gia_ManForEachCo( pMan, pNode, i ) Vec_IntWriteEntry( pMan->vLevels, Gia_ObjId(pMan, pNode), LevelMax ); @@ -196,6 +351,8 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) fprintf( pFile, " Level%d;\n", Level ); Gia_ManForEachObj( pMan, pNode, i ) { + if ( vMarks && Vec_IntEntry(vMarks, i) == 0 ) + continue; if ( (int)Gia_ObjLevel(pMan, pNode) != Level ) continue; /* @@ -206,8 +363,14 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) Gia_Regular(pNode->pEquiv)->Id, Gia_IsComplement(pNode->pEquiv)? "\'":"" ); */ fprintf( pFile, " Node%d [label = \"%d\"", i, i ); - - if ( Gia_ObjIsXor(pNode) ) + if ( vMarks && Vec_IntEntry(vMarks, i) > 0 ) + { + if ( Abc_Lit2Att2(Vec_IntEntry(vMarks, i)) == 2 ) + fprintf( pFile, ", shape = doubleoctagon" ); + else + fprintf( pFile, ", shape = octagon" ); + } + else if ( Gia_ObjIsXor(pNode) ) fprintf( pFile, ", shape = doublecircle" ); else if ( Gia_ObjIsMux(pMan, pNode) ) fprintf( pFile, ", shape = trapezium" ); @@ -277,10 +440,54 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) { if ( !Gia_ObjIsAnd(pNode) && !Gia_ObjIsCo(pNode) && !Gia_ObjIsBuf(pNode) ) continue; + if ( vMarks && Vec_IntEntry(vMarks, i) == 0 ) + continue; + // consider half/full-adder + if ( vMarks && Vec_IntEntry(vMarks, i) > 0 ) + { + int k, Mark = Vec_IntEntry(vMarks, i); + if ( Abc_Lit2Att2(Mark) == 2 ) // FA + { + int * pFanins = Vec_IntEntryP( vFadds, 5*Abc_Lit2Var2(Mark) ); + if ( pFanins[3] == i ) + continue; + assert( pFanins[4] == i ); + // generate the edge from this node to the next + for ( k = 0; k < 3; k++ ) + { + fprintf( pFile, "Node%d", i ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Vec_IntEntry(vRemap, pFanins[k]) ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", "bold" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + } + } + else // HA + { + int * pFanins = Vec_IntEntryP( vHadds, 2*Abc_Lit2Var2(Mark) ); + int pFaninsIn[2] = { Vec_IntEntry(vRemap, Gia_ObjFaninId0(pNode, i)), Vec_IntEntry(vRemap, Gia_ObjFaninId1(pNode, i)) }; + if ( pFanins[0] == i ) + continue; + assert( pFanins[1] == i ); + for ( k = 0; k < 2; k++ ) + { + fprintf( pFile, "Node%d", i ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Vec_IntEntry(vRemap, pFaninsIn[k]) ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", "bold" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + } + } + continue; + } // generate the edge from this node to the next fprintf( pFile, "Node%d", i ); fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", Gia_ObjFaninId0(pNode, i) ); + fprintf( pFile, "Node%d", vRemap ? Vec_IntEntry(vRemap, Gia_ObjFaninId0(pNode, i)) : Gia_ObjFaninId0(pNode, i) ); fprintf( pFile, " [" ); fprintf( pFile, "style = %s", Gia_ObjFaninC0(pNode)? "dotted" : "bold" ); // if ( Gia_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 ) @@ -292,7 +499,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) // generate the edge from this node to the next fprintf( pFile, "Node%d", i ); fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", Gia_ObjFaninId1(pNode, i) ); + fprintf( pFile, "Node%d", vRemap ? Vec_IntEntry(vRemap, Gia_ObjFaninId1(pNode, i)) : Gia_ObjFaninId1(pNode, i) ); fprintf( pFile, " [" ); fprintf( pFile, "style = %s", Gia_ObjFaninC1(pNode)? "dotted" : "bold" ); // if ( Gia_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 ) @@ -305,7 +512,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) // generate the edge from this node to the next fprintf( pFile, "Node%d", i ); fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", Gia_ObjFaninId2(pMan, i) ); + fprintf( pFile, "Node%d", vRemap ? Vec_IntEntry(vRemap, Gia_ObjFaninId2(pMan, i)) : Gia_ObjFaninId2(pMan, i) ); fprintf( pFile, " [" ); fprintf( pFile, "style = %s", Gia_ObjFaninC2(pMan, pNode)? "dotted" : "bold" ); // if ( Gia_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 ) @@ -349,7 +556,13 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) else if ( pMan->nXors || pMan->nMuxes ) Gia_ManCleanMark0( pMan ); + Vec_IntFreeP( &vFadds ); + Vec_IntFreeP( &vHadds ); + Vec_IntFreeP( &vRecord ); + Vec_IntFreeP( &pMan->vLevels ); + Vec_IntFreeP( &vMarks ); + Vec_IntFreeP( &vRemap ); } /**Function************************************************************* @@ -363,7 +576,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) SeeAlso [] ***********************************************************************/ -void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold ) +void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders ) { extern void Abc_ShowFile( char * FileNameDot ); static int Counter = 0; @@ -380,7 +593,7 @@ void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold ) } fclose( pFile ); // generate the file - Gia_WriteDotAig( pMan, FileNameDot, vBold ); + Gia_WriteDotAig( pMan, FileNameDot, vBold, fAdders ); // visualize the file Abc_ShowFile( FileNameDot ); } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6d6e16f5..11d61c14 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27541,12 +27541,15 @@ usage: int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv ) { Vec_Int_t * vBold = NULL; - int c; + int c, fAdders = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF ) { switch ( c ) { + case 'a': + fAdders ^= 1; + break; case 'h': goto usage; default: @@ -27563,19 +27566,20 @@ int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Show(): Cannot show GIA with barrier buffers.\n" ); return 1; } - if ( Gia_ManHasMapping(pAbc->pGia) ) + if ( !fAdders && Gia_ManHasMapping(pAbc->pGia) ) { vBold = Vec_IntAlloc( 100 ); Gia_ManForEachLut( pAbc->pGia, c ) Vec_IntPush( vBold, c ); } - Gia_ManShow( pAbc->pGia, vBold ); + Gia_ManShow( pAbc->pGia, vBold, fAdders ); Vec_IntFreeP( &vBold ); return 0; usage: - Abc_Print( -2, "usage: &show [-h]\n" ); + Abc_Print( -2, "usage: &show [-ah]\n" ); Abc_Print( -2, "\t shows the current GIA using GSView\n" ); + Abc_Print( -2, "\t-a : toggle visualazing adders [default = %s]\n", fAdders? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -39301,16 +39305,22 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose ); - int c, fVerbose = 0; + Vec_Int_t * vOrder = NULL; + int c, fSimple = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "svwh" ) ) != EOF ) { switch ( c ) { + case 's': + fSimple ^= 1; + break; case 'v': fVerbose ^= 1; break; + case 'w': + fVeryVerbose ^= 1; + break; case 'h': goto usage; default: @@ -39322,13 +39332,17 @@ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" ); return 0; } - Gia_PolynBuild( pAbc->pGia, NULL, fVerbose ); + vOrder = fSimple ? NULL : Gia_PolynReorder( pAbc->pGia, fVerbose, fVeryVerbose ); + Gia_PolynBuild( pAbc->pGia, vOrder, fVerbose, fVeryVerbose ); + Vec_IntFreeP( &vOrder ); return 0; usage: - Abc_Print( -2, "usage: &polyn [-vh]\n" ); + Abc_Print( -2, "usage: &polyn [-svwh]\n" ); Abc_Print( -2, "\t derives algebraic polynomial from AIG\n" ); + Abc_Print( -2, "\t-s : toggles simple computation [default = %s]\n", fSimple? "yes": "no" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggles printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/proof/acec/acec.h b/src/proof/acec/acec.h index 3f05e5e6..fd7814d8 100644 --- a/src/proof/acec/acec.h +++ b/src/proof/acec/acec.h @@ -51,10 +51,15 @@ ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// /*=== acecCore.c ========================================================*/ -extern int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars ); -/*=== acecMiter.c ========================================================*/ -extern int Gia_ManDemiterDual( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 ); -extern int Gia_ManDemiterXor( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 ); +extern int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars ); +/*=== acecFadds.c ========================================================*/ +extern Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose ); +extern Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose ); +/*=== acecOrder.c ========================================================*/ +extern Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose ); +extern Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose ); +/*=== acecPolyn.c ========================================================*/ +extern void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVeryVerbose ); ABC_NAMESPACE_HEADER_END diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c index bfece8dc..991067d8 100644 --- a/src/proof/acec/acecCore.c +++ b/src/proof/acec/acecCore.c @@ -44,10 +44,12 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars ) { - Vec_Int_t * vOrder0 = Gia_PolynReorder( pGia0, pPars->fVerbose ); - Vec_Int_t * vOrder1 = Gia_PolynReorder( pGia1, pPars->fVerbose ); - Gia_PolynBuild( pGia0, vOrder0, pPars->fVerbose ); - Gia_PolynBuild( pGia1, vOrder1, pPars->fVerbose ); + Vec_Int_t * vOrder0 = Gia_PolynReorder( pGia0, pPars->fVerbose, pPars->fVeryVerbose ); + Vec_Int_t * vOrder1 = Gia_PolynReorder( pGia1, pPars->fVerbose, pPars->fVeryVerbose ); + Gia_PolynBuild( pGia0, vOrder0, pPars->fVerbose, pPars->fVeryVerbose ); + Gia_PolynBuild( pGia1, vOrder1, pPars->fVerbose, pPars->fVeryVerbose ); + Vec_IntFree( vOrder0 ); + Vec_IntFree( vOrder1 ); return 1; } diff --git a/src/proof/acec/acecFadds.c b/src/proof/acec/acecFadds.c index 3d526dbf..6b954398 100644 --- a/src/proof/acec/acecFadds.c +++ b/src/proof/acec/acecFadds.c @@ -52,40 +52,61 @@ Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose ) Vec_Int_t * vHadds = Vec_IntAlloc( 1000 ); Gia_Obj_t * pObj, * pFan0, * pFan1; int i, iLit, iFan0, iFan1, fComplDiff, Count, Counts[5] = {0}; - ABC_FREE( p->pRefs ); - Gia_ManCreateRefs( p ); Gia_ManHashStart( p ); - Gia_ManForEachAnd( p, pObj, i ) + if ( p->nXors ) { - if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) - continue; - Count = 0; - if ( Gia_ObjRefNumId(p, Gia_ObjFaninId0(pObj, i)) > 1 ) - Vec_IntPushTwo( vHadds, i, Gia_ObjFaninId0(pObj, i) ), Count++; - if ( Gia_ObjRefNumId(p, Gia_ObjFaninId1(pObj, i)) > 1 ) - Vec_IntPushTwo( vHadds, i, Gia_ObjFaninId1(pObj, i) ), Count++; - iFan0 = Gia_ObjId( p, pFan0 ); - iFan1 = Gia_ObjId( p, pFan1 ); - fComplDiff = (Gia_ObjFaninC0(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC1(Gia_ObjFanin0(pObj))); - assert( fComplDiff == (Gia_ObjFaninC0(Gia_ObjFanin1(pObj)) ^ Gia_ObjFaninC1(Gia_ObjFanin1(pObj))) ); - if ( fComplDiff ) + Gia_ManForEachAnd( p, pObj, i ) { + if ( !Gia_ObjIsXor(pObj) ) + continue; + iFan0 = Gia_ObjFaninId0(pObj, i); + iFan1 = Gia_ObjFaninId1(pObj, i); if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 0))) ) Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++; if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 1), Abc_Var2Lit(iFan1, 1))) ) Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++; - } - else - { if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 1))) ) Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++; if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 1), Abc_Var2Lit(iFan1, 0))) ) Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++; } - Counts[Count]++; + } + else + { + ABC_FREE( p->pRefs ); + Gia_ManCreateRefs( p ); + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) + continue; + Count = 0; + if ( Gia_ObjRefNumId(p, Gia_ObjFaninId0(pObj, i)) > 1 ) + Vec_IntPushTwo( vHadds, i, Gia_ObjFaninId0(pObj, i) ), Count++; + if ( Gia_ObjRefNumId(p, Gia_ObjFaninId1(pObj, i)) > 1 ) + Vec_IntPushTwo( vHadds, i, Gia_ObjFaninId1(pObj, i) ), Count++; + iFan0 = Gia_ObjId( p, pFan0 ); + iFan1 = Gia_ObjId( p, pFan1 ); + fComplDiff = (Gia_ObjFaninC0(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC1(Gia_ObjFanin0(pObj))); + assert( fComplDiff == (Gia_ObjFaninC0(Gia_ObjFanin1(pObj)) ^ Gia_ObjFaninC1(Gia_ObjFanin1(pObj))) ); + if ( fComplDiff ) + { + if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 0))) ) + Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++; + if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 1), Abc_Var2Lit(iFan1, 1))) ) + Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++; + } + else + { + if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 1))) ) + Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++; + if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 1), Abc_Var2Lit(iFan1, 0))) ) + Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++; + } + Counts[Count]++; + } + ABC_FREE( p->pRefs ); } Gia_ManHashStop( p ); - ABC_FREE( p->pRefs ); if ( fVerbose ) { int iXor, iAnd; @@ -210,7 +231,10 @@ int Dtc_ObjComputeTruth_rec( Gia_Obj_t * pObj ) assert( Gia_ObjIsAnd(pObj) ); Truth0 = Dtc_ObjComputeTruth_rec( Gia_ObjFanin0(pObj) ); Truth1 = Dtc_ObjComputeTruth_rec( Gia_ObjFanin1(pObj) ); - return (pObj->Value = (Gia_ObjFaninC0(pObj) ? ~Truth0 : Truth0) & (Gia_ObjFaninC1(pObj) ? ~Truth1 : Truth1)); + if ( Gia_ObjIsXor(pObj) ) + return (pObj->Value = (Gia_ObjFaninC0(pObj) ? ~Truth0 : Truth0) ^ (Gia_ObjFaninC1(pObj) ? ~Truth1 : Truth1)); + else + return (pObj->Value = (Gia_ObjFaninC0(pObj) ? ~Truth0 : Truth0) & (Gia_ObjFaninC1(pObj) ? ~Truth1 : Truth1)); } void Dtc_ObjCleanTruth_rec( Gia_Obj_t * pObj ) { diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h index 28e8740b..7f70658e 100644 --- a/src/proof/acec/acecInt.h +++ b/src/proof/acec/acecInt.h @@ -54,13 +54,6 @@ ABC_NAMESPACE_HEADER_START /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== acecFadds.c ========================================================*/ -extern Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose ); -extern Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose ); -/*=== acecOrder.c ========================================================*/ -extern Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose ); -/*=== acecPolyn.c ========================================================*/ -extern void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose ); /*=== acecUtil.c ========================================================*/ extern void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose ); diff --git a/src/proof/acec/acecOrder.c b/src/proof/acec/acecOrder.c index 0cf686c8..fbce0835 100644 --- a/src/proof/acec/acecOrder.c +++ b/src/proof/acec/acecOrder.c @@ -42,44 +42,19 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose ) +Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose ) { - int fDumpLeftOver = 0; - Vec_Int_t * vOrder, * vOrder2; - Gia_Obj_t * pFan0, * pFan1; - int i, k, iDriver, Iter, iXor, iMaj, Entry, fFound; - Vec_Int_t * vFadds = Gia_ManDetectFullAdders( pGia, fVerbose ); - Vec_Int_t * vHadds = Gia_ManDetectHalfAdders( pGia, fVerbose ); + int i, iXor, iMaj, iAnd, Entry, Iter, fFound, fFoundAll = 1; Vec_Int_t * vRecord = Vec_IntAlloc( 100 ); - Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(pGia) ); - Gia_ManForEachCoDriverId( pGia, iDriver, i ) - Vec_IntWriteEntry( vMap, iDriver, 1 ); - - for ( Iter = 0; ; Iter++ ) + Gia_ManForEachCoDriverId( pGia, iAnd, i ) + Vec_IntWriteEntry( vMap, iAnd, 1 ); + for ( Iter = 0; fFoundAll; Iter++ ) { - int fFoundAll = 0; - printf( "Iteration %d\n", Iter ); - - // find the last one - iDriver = -1; - Vec_IntForEachEntryReverse( vMap, Entry, i ) - if ( Entry ) - { - iDriver = i; - break; - } - - if ( iDriver > 0 && Gia_ObjRecognizeExor(Gia_ManObj(pGia, iDriver), &pFan0, &pFan1) && Vec_IntFind(vFadds, iDriver) == -1 && Vec_IntFind(vHadds, iDriver) == -1 ) - { - Vec_IntWriteEntry( vMap, iDriver, 0 ); - Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan0), 1 ); - Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan1), 1 ); - Vec_IntPush( vRecord, iDriver ); - printf( "Recognizing %d => XOR(%d %d)\n", iDriver, Gia_ObjId(pGia, pFan0), Gia_ObjId(pGia, pFan1) ); - } - + if ( fVeryVerbose ) + printf( "Iteration %d\n", Iter ); // check if we can extract FADDs + fFoundAll = 0; do { fFound = 0; for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ ) @@ -93,19 +68,23 @@ Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose ) Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+0), 1 ); Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+1), 1 ); Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+2), 1 ); - Vec_IntPush( vRecord, iXor ); - Vec_IntPush( vRecord, iMaj ); + //Vec_IntPush( vRecord, iXor ); + //Vec_IntPush( vRecord, iMaj ); + Vec_IntPush( vRecord, Abc_Var2Lit2(i, 2) ); fFound = 1; fFoundAll = 1; - printf( "Recognizing (%d %d) => FA(%d %d %d)\n", iXor, iMaj, Vec_IntEntry(vFadds, 5*i+0), Vec_IntEntry(vFadds, 5*i+1), Vec_IntEntry(vFadds, 5*i+2) ); + if ( fVeryVerbose ) + printf( "Recognizing (%d %d) => FA(%d %d %d)\n", iXor, iMaj, Vec_IntEntry(vFadds, 5*i+0), Vec_IntEntry(vFadds, 5*i+1), Vec_IntEntry(vFadds, 5*i+2) ); } } } while ( fFound ); // check if we can extract HADDs do { - fFound = 0; - Vec_IntForEachEntryDouble( vHadds, iXor, iMaj, i ) + fFound = 0; + for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ ) { + iXor = Vec_IntEntry(vHadds, 2*i+0); + iMaj = Vec_IntEntry(vHadds, 2*i+1); if ( Vec_IntEntry(vMap, iXor) && Vec_IntEntry(vMap, iMaj) ) { Gia_Obj_t * pAnd = Gia_ManObj( pGia, iMaj ); @@ -113,32 +92,52 @@ Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose ) Vec_IntWriteEntry( vMap, iMaj, 0 ); Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iMaj), 1 ); Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iMaj), 1 ); - Vec_IntPush( vRecord, iXor ); - Vec_IntPush( vRecord, iMaj ); + //Vec_IntPush( vRecord, iXor ); + //Vec_IntPush( vRecord, iMaj ); + Vec_IntPush( vRecord, Abc_Var2Lit2(i, 1) ); fFound = 1; fFoundAll = 1; - printf( "Recognizing (%d %d) => HA(%d %d)\n", iXor, iMaj, Gia_ObjFaninId0(pAnd, iMaj), Gia_ObjFaninId1(pAnd, iMaj) ); + if ( fVeryVerbose ) + printf( "Recognizing (%d %d) => HA(%d %d)\n", iXor, iMaj, Gia_ObjFaninId0(pAnd, iMaj), Gia_ObjFaninId1(pAnd, iMaj) ); } } + break; // only one iter! } while ( fFound ); - if ( fFoundAll == 0 ) - break; + if ( fFoundAll ) + continue; + // find the last one + Vec_IntForEachEntryReverse( vMap, Entry, iAnd ) + if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, iAnd)) )//&& Vec_IntFind(vFadds, iAnd) == -1 )//&& Vec_IntFind(vHadds, iAnd) == -1 ) + { + Gia_Obj_t * pFan0, * pFan1, * pAnd = Gia_ManObj( pGia, iAnd ); + if ( !Gia_ObjRecognizeExor(pAnd, &pFan0, &pFan1) ) + { + Vec_IntWriteEntry( vMap, iAnd, 0 ); + Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iAnd), 1 ); + Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iAnd), 1 ); + //Vec_IntPush( vRecord, iAnd ); + Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 0) ); + } + else + { + Vec_IntWriteEntry( vMap, iAnd, 0 ); + Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan0), 1 ); + Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan1), 1 ); + //Vec_IntPush( vRecord, iAnd ); + Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 0) ); + Vec_IntPush( vRecord, Abc_Var2Lit2(Gia_ObjFaninId0(pAnd, iAnd), 0) ); + Vec_IntPush( vRecord, Abc_Var2Lit2(Gia_ObjFaninId1(pAnd, iAnd), 0) ); + printf( "Recognizing %d => XOR(%d %d)\n", iAnd, Gia_ObjId(pGia, pFan0), Gia_ObjId(pGia, pFan1) ); + } + fFoundAll = 1; + if ( fVeryVerbose ) + printf( "Recognizing %d => AND(%d %d)\n", iAnd, Gia_ObjFaninId0(pAnd, iAnd), Gia_ObjFaninId1(pAnd, iAnd) ); + break; + } } + //Vec_IntPrint( vMap ); - //Vec_IntPrint( vRecord ); - printf( "Remaining: " ); - Vec_IntForEachEntry( vMap, Entry, i ) - if ( Entry ) - printf( "%d ", i ); - printf( "\n" ); - - // collect remaining nodes - k = 0; - Vec_IntForEachEntry( vMap, Entry, i ) - if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, i)) ) - Vec_IntWriteEntry( vMap, k++, i ); - Vec_IntShrink( vMap, k ); - +/* // dump remaining nodes as an AIG if ( fDumpLeftOver ) { @@ -146,25 +145,66 @@ Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose ) Gia_AigerWrite( pNew, "leftover.aig", 0, 0 ); Gia_ManStop( pNew ); } +*/ + Vec_IntFree( vMap ); + Vec_IntReverseOrder( vRecord ); + return vRecord; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose ) +{ + Vec_Int_t * vFadds = Gia_ManDetectFullAdders( pGia, fVeryVerbose ); + Vec_Int_t * vHadds = Gia_ManDetectHalfAdders( pGia, fVeryVerbose ); + Vec_Int_t * vRecord = Gia_PolynFindOrder( pGia, vFadds, vHadds, fVerbose, fVeryVerbose ); + Vec_Int_t * vOrder = Vec_IntAlloc( Gia_ManAndNum(pGia) ); + Vec_Int_t * vOrder2 = Vec_IntStart( Gia_ManObjNum(pGia) ); + int i, k, Entry; // collect nodes - vOrder = Vec_IntAlloc( Gia_ManAndNum(pGia) ); Gia_ManIncrementTravId( pGia ); - Gia_ManCollectAnds( pGia, Vec_IntArray(vMap), Vec_IntSize(vMap), vOrder, NULL ); - Vec_IntForEachEntryReverse( vRecord, Entry, i ) - Gia_ManCollectAnds_rec( pGia, Entry, vOrder ); - assert( Vec_IntSize(vOrder) == Gia_ManAndNum(pGia) ); + Vec_IntForEachEntry( vRecord, Entry, i ) + { + int Node = Abc_Lit2Var2(Entry); + int Attr = Abc_Lit2Att2(Entry); + if ( Attr == 2 ) + { + int * pFanins = Vec_IntEntryP( vFadds, 5*Node ); + for ( k = 3; k < 5; k++ ) + Gia_ManCollectAnds_rec( pGia, pFanins[k], vOrder ); + } + else if ( Attr == 1 ) + { + int * pFanins = Vec_IntEntryP( vHadds, 2*Node ); + for ( k = 0; k < 2; k++ ) + Gia_ManCollectAnds_rec( pGia, pFanins[k], vOrder ); + } + else + Gia_ManCollectAnds_rec( pGia, Node, vOrder ); + } + //assert( Vec_IntSize(vOrder) == Gia_ManAndNum(pGia) ); // remap order - vOrder2 = Vec_IntStart( Gia_ManObjNum(pGia) ); + Gia_ManForEachCiId( pGia, Entry, i ) + Vec_IntWriteEntry( vOrder2, Entry, 1+i ); Vec_IntForEachEntry( vOrder, Entry, i ) - Vec_IntWriteEntry( vOrder2, Entry, i+1 ); - Vec_IntFree( vOrder ); + Vec_IntWriteEntry( vOrder2, Entry, 1+Gia_ManCiNum(pGia)+i ); + //Vec_IntPrint( vOrder ); - Vec_IntFree( vMap ); Vec_IntFree( vRecord ); Vec_IntFree( vFadds ); Vec_IntFree( vHadds ); + Vec_IntFree( vOrder ); return vOrder2; } diff --git a/src/proof/acec/acecPolyn.c b/src/proof/acec/acecPolyn.c index df6ef2a2..5e20ef30 100644 --- a/src/proof/acec/acecPolyn.c +++ b/src/proof/acec/acecPolyn.c @@ -61,7 +61,25 @@ struct Pln_Man_t_ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Pln_ManSimpleOrder( Gia_Man_t * p ) +{ + Vec_Int_t * vOrder; int Id; + vOrder = Vec_IntStart( Gia_ManObjNum(p) ); + Gia_ManForEachAndId( p, Id ) + Vec_IntWriteEntry( vOrder, Id, Id ); + return vOrder; +} /**Function************************************************************* @@ -112,10 +130,10 @@ void Pln_ManStop( Pln_Man_t * p ) Vec_IntFree( p->vTempM[1] ); Vec_IntFree( p->vTempM[2] ); Vec_IntFree( p->vTempM[3] ); - Vec_IntFree( p->vOrder ); + //Vec_IntFree( p->vOrder ); ABC_FREE( p ); } -void Pln_ManPrintFinal( Pln_Man_t * p ) +void Pln_ManPrintFinal( Pln_Man_t * p, int fVerbose, int fVeryVerbose ) { Vec_Int_t * vArray; int k, Entry, iMono, iConst, Count = 0; @@ -126,7 +144,7 @@ void Pln_ManPrintFinal( Pln_Man_t * p ) Count++; - if ( Count > 40 ) + if ( !fVeryVerbose ) continue; vArray = Hsh_VecReadEntry( p->pHashC, iConst ); @@ -301,7 +319,7 @@ int Gia_PolyFindNext( Pln_Man_t * p ) //Vec_IntPrint( Hsh_VecReadEntry(p->pHashM, iBest) ); return iBest; } -void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose ) +void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVeryVerbose ) { abctime clk = Abc_Clock();//, clk2 = 0; Gia_Obj_t * pObj; @@ -336,18 +354,20 @@ void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose ) // report vTempM = Hsh_VecReadEntry( p->pHashM, iMono ); //printf( "Removing var %d\n", Vec_IntEntryLast(vTempM) ); + LevCur = Vec_IntEntryLast(vTempM); + if ( !Gia_ObjIsAnd(Gia_ManObj(pGia, LevCur)) ) + continue; -// LevCur = Vec_IntEntryLast(vTempM); - LevCur = Vec_IntEntry(p->vOrder, Vec_IntEntryLast(vTempM)); if ( LevPrev != LevCur ) { - if ( Vec_BitEntry( vPres, LevCur & 0xFF ) ) - printf( "Repeating entry %d\n", LevCur & 0xFF ); + if ( Vec_BitEntry( vPres, LevCur ) && fVerbose ) + printf( "Repeating entry %d\n", LevCur ); else - Vec_BitSetEntry( vPres, LevCur & 0xFF, 1 ); + Vec_BitSetEntry( vPres, LevCur, 1 ); - printf( "Line %5d Iter %6d : Cur = %8x. Obj = %5d. HashC =%8d. HashM =%8d. Total =%8d. Used =%8d.\n", - Line++, Iter, LevCur, LevCur & 0xFF, Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, -1 ); + if ( fVerbose ) + printf( "Line%5d Iter%10d : Obj =%6d. Order =%6d. HashC =%6d. HashM =%10d. Total =%10d. Used =%6d.\n", + Line++, Iter, LevCur, Vec_IntEntry(p->vOrder, LevCur), Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, -1 ); } LevPrev = LevCur; @@ -356,7 +376,7 @@ void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose ) } Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); //Abc_PrintTime( 1, "Time2", clk2 ); - Pln_ManPrintFinal( p ); + Pln_ManPrintFinal( p, fVerbose, fVeryVerbose ); Pln_ManStop( p ); Vec_BitFree( vPres ); } -- cgit v1.2.3