diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
| -rw-r--r-- | src/aig/gia/giaDup.c | 65 | ||||
| -rw-r--r-- | src/aig/gia/giaShow.c | 13 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 54 | ||||
| -rw-r--r-- | src/misc/vec/vecWec.h | 12 | ||||
| -rw-r--r-- | src/proof/acec/acec.h | 2 | ||||
| -rw-r--r-- | src/proof/acec/acecCl.c | 88 | ||||
| -rw-r--r-- | src/proof/acec/acecCore.c | 124 | ||||
| -rw-r--r-- | src/proof/acec/acecInt.h | 2 | ||||
| -rw-r--r-- | src/proof/acec/acecRe.c | 5 | ||||
| -rw-r--r-- | src/proof/acec/acecTree.c | 138 | ||||
| -rw-r--r-- | src/proof/acec/acecUtil.c | 23 |
12 files changed, 501 insertions, 27 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index dc6c679a..3bc97e6b 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1242,6 +1242,8 @@ extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ); extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ); extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ); extern Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrimPis ); +extern Gia_Man_t * Gia_ManDupAndConesLimit( Gia_Man_t * p, int * pAnds, int nAnds, int Level ); +extern Gia_Man_t * Gia_ManDupAndConesLimit2( Gia_Man_t * p, int * pAnds, int nAnds, int Level ); extern Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupLevelized( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index cdb6a208..b0ba3472 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -3046,6 +3046,71 @@ Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrim return pNew; } +void Gia_ManDupAndConesLimit_rec( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, int Level ) +{ + Gia_Obj_t * pObj = Gia_ManObj(p, iObj); + if ( ~pObj->Value ) + return; + if ( !Gia_ObjIsAnd(pObj) || Gia_ObjLevel(p, pObj) < Level ) + { + pObj->Value = Gia_ManAppendCi( pNew ); + //printf( "PI %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj ); + return; + } + Gia_ManDupAndConesLimit_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj), Level ); + Gia_ManDupAndConesLimit_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj), Level ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + //printf( "Obj %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj ); +} +Gia_Man_t * Gia_ManDupAndConesLimit( Gia_Man_t * p, int * pAnds, int nAnds, int Level ) +{ + Gia_Man_t * pNew; + int i; + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManLevelNum( p ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + for ( i = 0; i < nAnds; i++ ) + Gia_ManDupAndConesLimit_rec( pNew, p, pAnds[i], Level ); + for ( i = 0; i < nAnds; i++ ) + Gia_ManAppendCo( pNew, Gia_ManObj(p, pAnds[i])->Value ); + return pNew; +} + +void Gia_ManDupAndConesLimit2_rec( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, int Level ) +{ + Gia_Obj_t * pObj = Gia_ManObj(p, iObj); + if ( ~pObj->Value ) + return; + if ( !Gia_ObjIsAnd(pObj) || Level <= 0 ) + { + pObj->Value = Gia_ManAppendCi( pNew ); + //printf( "PI %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj ); + return; + } + Gia_ManDupAndConesLimit2_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj), Level-1 ); + Gia_ManDupAndConesLimit2_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj), Level-1 ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + //printf( "Obj %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj ); +} +Gia_Man_t * Gia_ManDupAndConesLimit2( Gia_Man_t * p, int * pAnds, int nAnds, int Level ) +{ + Gia_Man_t * pNew; + int i; + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + for ( i = 0; i < nAnds; i++ ) + Gia_ManDupAndConesLimit2_rec( pNew, p, pAnds[i], Level ); + for ( i = 0; i < nAnds; i++ ) + Gia_ManAppendCo( pNew, Gia_ManObj(p, pAnds[i])->Value ); + return pNew; + +} /**Function************************************************************* diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c index 4dd85aab..4deebd7a 100644 --- a/src/aig/gia/giaShow.c +++ b/src/aig/gia/giaShow.c @@ -1014,16 +1014,23 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_In SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds, int fFadds ) +Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds, int fFadds, Vec_Int_t * vBold ) { - Vec_Int_t * vMapAdds = Vec_IntStartFull( Gia_ManObjNum(p) ); int i; + Vec_Bit_t * vIsBold = Vec_BitStart( Gia_ManObjNum(p) ); + Vec_Int_t * vMapAdds = Vec_IntStartFull( Gia_ManObjNum(p) ); int i, Entry; + if ( vBold ) + Vec_IntForEachEntry( vBold, Entry, i ) + Vec_BitWriteEntry( vIsBold, Entry, 1 ); for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) { if ( fFadds && Vec_IntEntry(vAdds, 6*i+2) == 0 ) continue; + if ( Vec_BitEntry(vIsBold, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIsBold, Vec_IntEntry(vAdds, 6*i+4)) ) + continue; Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+3), i ); Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+4), i ); } + Vec_BitFree( vIsBold ); return vMapAdds; } Vec_Int_t * Gia_ShowMapXors( Gia_Man_t * p, Vec_Int_t * vXors ) @@ -1105,7 +1112,7 @@ Vec_Int_t * Gia_ShowCollectObjs( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * v ***********************************************************************/ void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_Int_t * vAdds, Vec_Int_t * vXors, int fFadds ) { - Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds ); + Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds, vBold ); Vec_Int_t * vMapXors = Gia_ShowMapXors( p, vXors ); Vec_Int_t * vOrder = Gia_ShowCollectObjs( p, vAdds, vXors, vMapAdds, vMapXors ); Gia_WriteDotAig( p, pFileName, vBold, vAdds, vXors, vMapAdds, vMapXors, vOrder ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9db3d7d6..58a14e81 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -482,6 +482,7 @@ static int Abc_CommandAbc9ATree ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Polyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Acec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Anorm ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Decla ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Esop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1126,6 +1127,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&polyn", Abc_CommandAbc9Polyn, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&acec", Abc_CommandAbc9Acec, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&anorm", Abc_CommandAbc9Anorm, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&decla", Abc_CommandAbc9Decla, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&esop", Abc_CommandAbc9Esop, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&exorcism", Abc_CommandAbc9Exorcism, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 ); @@ -40799,6 +40801,57 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9Decla( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Gia_Man_t * pTemp; + int c, fBooth = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF ) + { + switch ( c ) + { + case 'b': + fBooth ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Decla(): There is no AIG.\n" ); + return 0; + } + pTemp = Acec_ManDecla( pAbc->pGia, fBooth, fVerbose ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &decla [-bvh]\n" ); + Abc_Print( -2, "\t removes carry look ahead adders\n" ); + Abc_Print( -2, "\t-b : toggles working with Booth multipliers [default = %s]\n", fBooth? "yes": "no" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9Esop( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes ); @@ -42690,7 +42743,6 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Jf_ManTestCnf( pAbc->pGia ); // Gia_ManCheckFalseTest( pAbc->pGia, nFrames ); // Gia_ParTest( pAbc->pGia, nWords, nProcs ); - Acec_MultFindPPsTest( pAbc->pGia ); // printf( "\nThis command is currently disabled.\n\n" ); return 0; diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h index 8180e984..c8c89701 100644 --- a/src/misc/vec/vecWec.h +++ b/src/misc/vec/vecWec.h @@ -561,6 +561,18 @@ static inline void Vec_WecPrint( Vec_Wec_t * p, int fSkipSingles ) printf( " }\n" ); } } +static inline void Vec_WecPrintLits( Vec_Wec_t * p ) +{ + Vec_Int_t * vVec; + int i, k, iLit; + Vec_WecForEachLevel( p, vVec, i ) + { + printf( " %4d : %2d {", i, Vec_IntSize(vVec) ); + Vec_IntForEachEntry( vVec, iLit, k ) + printf( " %c%d", Abc_LitIsCompl(iLit) ? '-' : '+', Abc_Lit2Var(iLit) ); + printf( " }\n" ); + } +} /**Function************************************************************* diff --git a/src/proof/acec/acec.h b/src/proof/acec/acec.h index 5a24bec7..fcbd32df 100644 --- a/src/proof/acec/acec.h +++ b/src/proof/acec/acec.h @@ -66,6 +66,8 @@ struct Acec_ParCec_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== acecCl.c ========================================================*/ +extern Gia_Man_t * Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose ); /*=== acecCore.c ========================================================*/ extern void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p ); extern int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars ); diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c index 145f2e0b..6a5f4040 100644 --- a/src/proof/acec/acecCl.c +++ b/src/proof/acec/acecCl.c @@ -335,6 +335,94 @@ Gia_Man_t * Acec_DetectAdditional( Gia_Man_t * p, int fVerbose ) return pNew; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Acec_RewriteTop( Gia_Man_t * p, Acec_Box_t * pBox ) +{ + Vec_Int_t * vRes = Vec_IntAlloc( Gia_ManCoNum(p) + 1 ); + Vec_Int_t * vLevel; + int i, k, iLit; + Vec_WecPrintLits( pBox->vRootLits ); + Vec_WecForEachLevel( pBox->vRootLits, vLevel, i ) + { + int In[3] = {0}, Out[2]; + assert( Vec_IntSize(vLevel) > 0 ); + assert( Vec_IntSize(vLevel) <= 3 ); + if ( Vec_IntSize(vLevel) == 1 ) + { + Vec_IntPush( vRes, Vec_IntEntry(vLevel, 0) ); + continue; + } + Vec_IntForEachEntry( vLevel, iLit, k ) + In[k] = iLit; + Acec_InsertFadd( p, In, Out ); + Vec_IntPush( vRes, Out[0] ); + if ( i+1 < Vec_WecSize(pBox->vRootLits) ) + Vec_IntPush( Vec_WecEntry(pBox->vRootLits, i+1), Out[1] ); + else + Vec_IntPush( Vec_WecPushLevel(pBox->vRootLits), Out[1] ); + } + assert( Vec_IntSize(vRes) >= Gia_ManCoNum(p) ); + Vec_IntShrink( vRes, Gia_ManCoNum(p) ); + return vRes; +} +Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; int i; + assert( Gia_ManCoNum(p) == Vec_IntSize(vRes) ); + // create new manager + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManSetPhase( p ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + { + int iLit = Vec_IntEntry( vRes, i ); + int Phase1 = Gia_ObjPhase(pObj); + int Phase2 = Abc_LitIsCompl(iLit) ^ Gia_ObjPhase(Gia_ManObj(p, Abc_Lit2Var(iLit))); + int iLitNew = Abc_Var2Lit( Abc_Lit2Var(iLit), Phase1 ^ Phase2 ); + pObj->Value = Gia_ManAppendCo( pNew, iLitNew ); + } + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} +Gia_Man_t * Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose ) +{ + int status = -1; + abctime clk = Abc_Clock(); + Gia_Man_t * pNew = NULL; + Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG(pGia) : NULL; + Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, fVerbose ); + Vec_Int_t * vResult; + Vec_BitFreeP( &vIgnore ); + if ( pBox == NULL ) // cannot match + { + printf( "Cannot find arithmetic boxes.\n" ); + return Gia_ManDup( pGia ); + } + vResult = Acec_RewriteTop( pGia, pBox ); + pNew = Acec_RewriteReplace( pGia, vResult ); + Vec_IntFree( vResult ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c index 6b631a1b..4fddcfab 100644 --- a/src/proof/acec/acecCore.c +++ b/src/proof/acec/acecCore.c @@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define TRUTH_UNUSED 0x1234567812345678 + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -70,6 +72,79 @@ void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p ) SeeAlso [] ***********************************************************************/ +void Acec_VerifyClasses( Gia_Man_t * p, Vec_Wec_t * vLits, Vec_Wec_t * vReprs ) +{ + Vec_Ptr_t * vFunc = Vec_PtrAlloc( Vec_WecSize(vLits) ); + Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); + Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) ); + Vec_Int_t * vLevel; + int i, j, k, Entry, Entry2, nOvers = 0, nErrors = 0; + Vec_WecForEachLevel( vLits, vLevel, i ) + { + Vec_Wrd_t * vTruths = Vec_WrdAlloc( Vec_IntSize(vLevel) ); + Vec_IntForEachEntry( vLevel, Entry, k ) + { + word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp ); + if ( Vec_IntSize(vSupp) > 6 ) + { + nOvers++; + Vec_WrdPush( vTruths, TRUTH_UNUSED ); + continue; + } + vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize ); + if ( Vec_IntSize(vSupp) > 5 ) + { + nOvers++; + Vec_WrdPush( vTruths, TRUTH_UNUSED ); + continue; + } + Vec_WrdPush( vTruths, Truth ); + } + Vec_PtrPush( vFunc, vTruths ); + } + if ( nOvers ) + printf( "Detected %d oversize support nodes.\n", nOvers ); + Vec_IntFree( vSupp ); + Vec_WrdFree( vTemp ); + // verify the classes + Vec_WecForEachLevel( vReprs, vLevel, i ) + { + Vec_Wrd_t * vTruths = (Vec_Wrd_t *)Vec_PtrEntry( vFunc, i ); + Vec_IntForEachEntry( vLevel, Entry, k ) + Vec_IntForEachEntryStart( vLevel, Entry2, j, k+1 ) + { + word Truth = Vec_WrdEntry( vTruths, k ); + word Truth2 = Vec_WrdEntry( vTruths, j ); + if ( Entry == Entry2 ) + { + nErrors++; + if ( Truth != Truth2 && Truth != TRUTH_UNUSED && Truth2 != TRUTH_UNUSED ) + printf( "Rank %d: Lit %d and %d do not pass verification.\n", i, k, j ); + } + if ( Entry == Abc_LitNot(Entry2) ) + { + nErrors++; + if ( Truth != ~Truth2 && Truth != TRUTH_UNUSED && Truth2 != TRUTH_UNUSED ) + printf( "Rank %d: Lit %d and %d do not pass verification.\n", i, k, j ); + } + } + } + if ( nErrors ) + printf( "Total errors in equivalence classes = %d.\n", nErrors ); + Vec_VecFree( (Vec_Vec_t *)vFunc ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Gia_Man_t * Acec_CommonStart( Gia_Man_t * pBase, Gia_Man_t * pAdd ) { Gia_Obj_t * pObj; @@ -148,13 +223,15 @@ void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCostLits ) } void Acec_MatchPrintEquivLits( Gia_Man_t * p, Vec_Wec_t * vLits, int * pCostLits, int fVerbose ) { - Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); - Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) ); + Vec_Int_t * vSupp; + Vec_Wrd_t * vTemp; Vec_Int_t * vLevel; int i, k, Entry; printf( "Leaf literals and their classes:\n" ); Vec_WecForEachLevel( vLits, vLevel, i ) { + if ( Vec_IntSize(vLevel) == 0 ) + continue; printf( "Rank %2d : %2d ", i, Vec_IntSize(vLevel) ); Vec_IntForEachEntry( vLevel, Entry, k ) printf( "%s%d(%d) ", Abc_LitIsCompl(Entry) ? "-":"+", Abc_Lit2Var(Entry), Abc_Lit2LitL(pCostLits, Entry) ); @@ -162,13 +239,25 @@ void Acec_MatchPrintEquivLits( Gia_Man_t * p, Vec_Wec_t * vLits, int * pCostLits } if ( !fVerbose ) return; + vSupp = Vec_IntAlloc( 100 ); + vTemp = Vec_WrdStart( Gia_ManObjNum(p) ); Vec_WecForEachLevel( vLits, vLevel, i ) { - if ( i != 20 ) + //if ( i != 20 ) + // continue; + if ( Vec_IntSize(vLevel) == 0 ) continue; Vec_IntForEachEntry( vLevel, Entry, k ) { word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp ); +/* + { + int iObj = Abc_Lit2Var(Entry); + Gia_Man_t * pGia0 = Gia_ManDupAndCones( p, &iObj, 1, 1 ); + Gia_ManShow( pGia0, NULL, 0, 0, 0 ); + Gia_ManStop( pGia0 ); + } +*/ printf( "Rank = %4d : ", i ); printf( "Obj = %4d ", Abc_Lit2Var(Entry) ); if ( Vec_IntSize(vSupp) > 6 ) @@ -218,7 +307,7 @@ int Acec_MatchCountCommon( Vec_Wec_t * vLits1, Vec_Wec_t * vLits2, int Shift ) Vec_IntFree( vRes ); return nCommon; } -void Acec_MatchCheckShift( Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Wec_t * vRoots0, Vec_Wec_t * vRoots1 ) +void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Wec_t * vRoots0, Vec_Wec_t * vRoots1 ) { Vec_Wec_t * vRes0 = Acec_MatchCopy( vLits0, vMap0 ); Vec_Wec_t * vRes1 = Acec_MatchCopy( vLits1, vMap1 ); @@ -229,14 +318,24 @@ void Acec_MatchCheckShift( Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * v { Vec_WecInsertLevel( vLits0, 0 ); Vec_WecInsertLevel( vRoots0, 0 ); + printf( "Shifted one level up.\n" ); } else if ( nCommonMinus > nCommonPlus && nCommonMinus > nCommon ) { Vec_WecInsertLevel( vLits1, 0 ); Vec_WecInsertLevel( vRoots1, 0 ); + printf( "Shifted one level down.\n" ); } - Vec_WecPrint( vRes0, 0 ); - Vec_WecPrint( vRes1, 0 ); + //printf( "Input literals:\n" ); + //Vec_WecPrintLits( vLits0 ); + printf( "Equiv classes:\n" ); + Vec_WecPrintLits( vRes0 ); + //printf( "Input literals:\n" ); + //Vec_WecPrintLits( vLits1 ); + printf( "Equiv classes:\n" ); + Vec_WecPrintLits( vRes1 ); + //Acec_VerifyClasses( pGia0, vLits0, vRes0 ); + //Acec_VerifyClasses( pGia1, vLits1, vRes1 ); Vec_WecFree( vRes0 ); Vec_WecFree( vRes1 ); } @@ -250,10 +349,14 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 ) Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap0) ); Vec_WecForEachLevel( pBox1->vLeafLits, vLevel, i ) Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap1) ); - Acec_MatchCheckShift( pBox0->vLeafLits, pBox1->vLeafLits, vMap0, vMap1, pBox0->vRootLits, pBox1->vRootLits ); + Acec_MatchCheckShift( pBox0->pGia, pBox1->pGia, pBox0->vLeafLits, pBox1->vLeafLits, vMap0, vMap1, pBox0->vRootLits, pBox1->vRootLits ); //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vLeafLits, Vec_IntArray(vMap0), 0 ); //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vLeafLits, Vec_IntArray(vMap1), 0 ); + printf( "Outputs:\n" ); + Vec_WecPrintLits( pBox0->vRootLits ); + printf( "Outputs:\n" ); + Vec_WecPrintLits( pBox1->vRootLits ); // reorder nodes to have the same order assert( pBox0->vShared == NULL ); @@ -350,8 +453,11 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars ) printf( "Matching of adder trees in LHS and RHS succeeded. " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); // remove the last output - //Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-1, 0 ); - //Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-1, 0 ); + Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-1, 0 ); + Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-1, 0 ); + + Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-2, 0 ); + Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-2, 0 ); } // solve regular CEC problem Cec_ManCecSetDefaultParams( pCecPars ); diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h index cc5786bb..c49945db 100644 --- a/src/proof/acec/acecInt.h +++ b/src/proof/acec/acecInt.h @@ -71,8 +71,10 @@ extern Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdd extern Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits ); extern Vec_Bit_t * Acec_BoothFindPPG( Gia_Man_t * p ); /*=== acecNorm.c ========================================================*/ +extern void Acec_InsertFadd( Gia_Man_t * pNew, int In[3], int Out[2] ); extern Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll ); /*=== acecTree.c ========================================================*/ +extern void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds ); extern Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose ); extern void Acec_BoxFreeP( Acec_Box_t ** ppBox ); /*=== acecUtil.c ========================================================*/ diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c index 7f87df85..5e5ca688 100644 --- a/src/proof/acec/acecRe.c +++ b/src/proof/acec/acecRe.c @@ -450,6 +450,7 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose Hash_IntManStop( pHash ); Ree_ManRemoveTrivial( p, vAdds ); Ree_ManRemoveContained( p, vAdds ); + //Ree_ManPrintAdders( vAdds, 1 ); return vAdds; } @@ -523,6 +524,10 @@ void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds ) { pObjX = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+3) ); pObjM = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+4) ); + // rule out if MAJ is a fanout of XOR + //if ( pObjX == Gia_ObjFanin0(pObjM) || pObjX == Gia_ObjFanin1(pObjM) ) + // continue; + // rule out if MAJ is a fanin of XOR and has no other fanouts if ( (pObjM == Gia_ObjFanin0(pObjX) || pObjM == Gia_ObjFanin1(pObjX)) && Gia_ObjRefNum(p, pObjM) == 1 ) continue; } diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c index 295fd738..2b356574 100644 --- a/src/proof/acec/acecTree.c +++ b/src/proof/acec/acecTree.c @@ -66,6 +66,30 @@ void Acec_BoxFreeP( Acec_Box_t ** ppBox ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acec_VerifyBoxLeaves( Acec_Box_t * pBox, Vec_Bit_t * vIgnore ) +{ + Vec_Int_t * vLevel; + int i, k, iLit, Count = 0; + if ( vIgnore == NULL ) + return; + Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i ) + Vec_IntForEachEntry( vLevel, iLit, k ) + if ( Gia_ObjIsAnd(Gia_ManObj(pBox->pGia, Abc_Lit2Var(iLit))) && !Vec_BitEntry(vIgnore, Abc_Lit2Var(iLit)) ) + printf( "Internal node %d of rank %d is not part of PPG.\n", Abc_Lit2Var(iLit), i ), Count++; + printf( "Detected %d suspicious leaves.\n", Count ); +} + +/**Function************************************************************* + Synopsis [Filters trees by removing TFO of roots.] Description [] @@ -103,6 +127,18 @@ void Acec_TreeFilterOne( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree ) // remove those that overlap with roots Vec_IntForEachEntryDouble( vTree, Box, Rank, i ) { +/* + if ( Vec_IntEntry(vAdds, 6*Box+3) == 24 && Vec_IntEntry(vAdds, 6*Box+4) == 22 ) + { + printf( "**** removing special one \n" ); + continue; + } + if ( Vec_IntEntry(vAdds, 6*Box+3) == 48 && Vec_IntEntry(vAdds, 6*Box+4) == 49 ) + { + printf( "**** removing special one \n" ); + continue; + } +*/ if ( Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+3)) || Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+4)) ) { printf( "Removing box %d=(%d,%d) of rank %d.\n", Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4), Rank ); @@ -125,6 +161,73 @@ void Acec_TreeFilterTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees /**Function************************************************************* + Synopsis [Filters trees by removing TFO of roots.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acec_TreeMarkTFI_rec( Gia_Man_t * p, int Id, Vec_Bit_t * vMarked ) +{ + Gia_Obj_t * pObj = Gia_ManObj(p, Id); + if ( Vec_BitEntry(vMarked, Id) ) + return; + Vec_BitWriteEntry( vMarked, Id, 1 ); + if ( !Gia_ObjIsAnd(pObj) ) + return; + Acec_TreeMarkTFI_rec( p, Gia_ObjFaninId0(pObj, Id), vMarked ); + Acec_TreeMarkTFI_rec( p, Gia_ObjFaninId1(pObj, Id), vMarked ); +} +void Acec_TreeFilterOne2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree ) +{ + Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) ); + Vec_Bit_t * vMarked = Vec_BitStart( Gia_ManObjNum(p) ) ; + Gia_Obj_t * pObj; + int i, k = 0, Box, Rank; + // mark leaves + Vec_IntForEachEntryDouble( vTree, Box, Rank, i ) + { + Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+0), 1 ); + Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+1), 1 ); + Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+2), 1 ); + } + Vec_IntForEachEntryDouble( vTree, Box, Rank, i ) + { + Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+3), 0 ); + Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4), 0 ); + } + // mark TFI of leaves + Gia_ManForEachAnd( p, pObj, i ) + if ( Vec_BitEntry(vIsLeaf, i) ) + Acec_TreeMarkTFI_rec( p, i, vMarked ); + // remove those that overlap with the marked TFI + Vec_IntForEachEntryDouble( vTree, Box, Rank, i ) + { + if ( Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+3)) || Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+4)) ) + { + printf( "Removing box %d=(%d,%d) of rank %d.\n", Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4), Rank ); + continue; + } + Vec_IntWriteEntry( vTree, k++, Box ); + Vec_IntWriteEntry( vTree, k++, Rank ); + } + Vec_IntShrink( vTree, k ); + Vec_BitFree( vIsLeaf ); + Vec_BitFree( vMarked ); +} +void Acec_TreeFilterTrees2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees ) +{ + Vec_Int_t * vLevel; + int i; + Vec_WecForEachLevel( vTrees, vLevel, i ) + Acec_TreeFilterOne2( p, vAdds, vLevel ); +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -392,7 +495,7 @@ Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vI Vec_BitFree( vFound ); Vec_IntFree( vMap ); // filter trees - //Acec_TreeFilterTrees( p, vAdds, vTrees ); + Acec_TreeFilterTrees( p, vAdds, vTrees ); // sort by size Vec_WecSort( vTrees, 1 ); return vTrees; @@ -437,20 +540,11 @@ void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds ) { printf( " %4d : %2d {", i, Vec_IntSize(vLevel) ); Vec_IntForEachEntry( vLevel, iBox, k ) + { printf( " %s%d=(%d,%d)", Vec_IntEntry(vAdds, 6*iBox+2) == 0 ? "*":"", iBox, Vec_IntEntry(vAdds, 6*iBox+3), Vec_IntEntry(vAdds, 6*iBox+4) ); - printf( " }\n" ); - } -} -void Vec_WecPrintLits( Vec_Wec_t * p ) -{ - Vec_Int_t * vVec; - int i, k, Entry; - Vec_WecForEachLevel( p, vVec, i ) - { - printf( " %4d : %2d {", i, Vec_IntSize(vVec) ); - Vec_IntForEachEntry( vVec, Entry, k ) - printf( " %c%d", Abc_LitIsCompl(Entry) ? '-' : '+', Abc_Lit2Var(Entry) ); + //printf( "(%d,%d,%d)", Vec_IntEntry(vAdds, 6*iBox+0), Vec_IntEntry(vAdds, 6*iBox+1), Vec_IntEntry(vAdds, 6*iBox+2) ); + } printf( " }\n" ); } } @@ -505,7 +599,10 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree Vec_WecForEachLevelReverse( pBox->vAdds, vLevel, i ) Vec_IntForEachEntry( vLevel, Box, k ) if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4) ) ) + { + //printf( "Pushing phase of output %d of box %d\n", Vec_IntEntry(vAdds, 6*Box+4), Box ); Acec_TreePhases_rec( p, vAdds, vMap, Vec_IntEntry(vAdds, 6*Box+4), Vec_IntEntry(vAdds, 6*Box+2) != 0, vVisit ); + } Acec_TreeVerifyPhases( p, vAdds, pBox->vAdds ); Acec_TreeVerifyPhases2( p, vAdds, pBox->vAdds ); Vec_BitFree( vVisit ); @@ -521,7 +618,14 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree Vec_WecPush( pBox->vLeafLits, i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_SignBit2(vAdds, Box, k)) ); for ( k = 3; k < 5; k++ ) if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k) ) ) + { + //if ( Vec_IntEntry(vAdds, 6*Box+k) == 10942 ) + //{ + // printf( "++++++++++++ Skipping special\n" ); + // continue; + //} Vec_WecPush( pBox->vRootLits, k == 4 ? i + 1 : i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_SignBit2(vAdds, Box, k)) ); + } if ( Vec_IntEntry(vAdds, 6*Box+2) == 0 && Acec_SignBit2(vAdds, Box, 2) ) Vec_WecPush( pBox->vLeafLits, i, 1 ); } @@ -531,8 +635,9 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i ) Vec_IntSort( vLevel, 0 ); Vec_WecForEachLevel( pBox->vRootLits, vLevel, i ) - Vec_IntSort( vLevel, 0 ); + Vec_IntSort( vLevel, 1 ); //return pBox; +/* // push literals forward //Vec_WecPrint( pBox->vLeafLits, 0 ); Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i ) @@ -555,6 +660,7 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree } } printf( "Pushed forward %d input literals.\n", Count ); +*/ //Vec_WecPrint( pBox->vLeafLits, 0 ); return pBox; } @@ -607,13 +713,17 @@ Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose ) Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, fVerbose ); Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore ); if ( vTrees && Vec_WecSize(vTrees) > 0 ) + { pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, 0) ); + Acec_VerifyBoxLeaves( pBox, vIgnore ); + } if ( pBox )//&& fVerbose ) printf( "Processing tree %d: Ranks = %d. Adders = %d. Leaves = %d. Roots = %d.\n", 0, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds), Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits) ); if ( pBox && fVerbose ) Acec_PrintBox( pBox, vAdds ); + //Acec_PrintAdders( pBox0->vAdds, vAdds ); //Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits ); Vec_WecFreeP( &vTrees ); Vec_IntFree( vAdds ); diff --git a/src/proof/acec/acecUtil.c b/src/proof/acec/acecUtil.c index 191856cf..be12afef 100644 --- a/src/proof/acec/acecUtil.c +++ b/src/proof/acec/acecUtil.c @@ -90,6 +90,29 @@ void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose ) Vec_IntFree( vXors ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupTopMostRange( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Vec_Int_t * vTops = Vec_IntAlloc( 10 ); + int i; + for ( i = 45; i < 52; i++ ) + Vec_IntPush( vTops, Gia_ObjId( p, Gia_ObjFanin0(Gia_ManCo(p, i)) ) ); + pNew = Gia_ManDupAndConesLimit( p, Vec_IntArray(vTops), Vec_IntSize(vTops), 100 ); + Vec_IntFree( vTops ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |