diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/acec/acec.h | 2 | ||||
| -rw-r--r-- | src/proof/acec/acecCover.c | 263 | ||||
| -rw-r--r-- | src/proof/acec/acecFadds.c | 54 | ||||
| -rw-r--r-- | src/proof/acec/acecOrder.c | 2 | ||||
| -rw-r--r-- | src/proof/acec/acecPolyn.c | 89 | ||||
| -rw-r--r-- | src/proof/acec/module.make | 1 | ||||
| -rw-r--r-- | src/proof/cec/cec.h | 1 | ||||
| -rw-r--r-- | src/proof/cec/cecCore.c | 10 | ||||
| -rw-r--r-- | src/proof/cec/cecInt.h | 2 | ||||
| -rw-r--r-- | src/proof/cec/cecSolve.c | 12 | ||||
| -rw-r--r-- | src/proof/ssw/sswConstr.c | 6 | ||||
| -rw-r--r-- | src/proof/ssw/sswSweep.c | 3 |
12 files changed, 395 insertions, 50 deletions
diff --git a/src/proof/acec/acec.h b/src/proof/acec/acec.h index f39041c8..c61b4485 100644 --- a/src/proof/acec/acec.h +++ b/src/proof/acec/acec.h @@ -53,7 +53,7 @@ ABC_NAMESPACE_HEADER_START /*=== acecCore.c ========================================================*/ 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_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** vCutsXor2 ); 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 ); diff --git a/src/proof/acec/acecCover.c b/src/proof/acec/acecCover.c new file mode 100644 index 00000000..e0d16419 --- /dev/null +++ b/src/proof/acec/acecCover.c @@ -0,0 +1,263 @@ +/**CFile**************************************************************** + + FileName [acecCover.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecCover.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "acecInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_AcecMark_rec( Gia_Man_t * p, int iObj, int fFirst ) +{ + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + if ( pObj->fMark0 && !fFirst ) + return; + assert( Gia_ObjIsAnd(pObj) ); + pObj->fMark1 = 1; + Gia_AcecMark_rec( p, Gia_ObjFaninId0(pObj, iObj), 0 ); + Gia_AcecMark_rec( p, Gia_ObjFaninId1(pObj, iObj), 0 ); +} +void Gia_AcecMarkFadd( Gia_Man_t * p, int * pSigs ) +{ +// if ( Gia_ManObj(p, pSigs[3])->fMark1 || Gia_ManObj(p, pSigs[4])->fMark1 ) +// return; + Gia_ManObj( p, pSigs[0] )->fMark0 = 1; + Gia_ManObj( p, pSigs[1] )->fMark0 = 1; + Gia_ManObj( p, pSigs[2] )->fMark0 = 1; +// assert( !Gia_ManObj(p, pSigs[3])->fMark1 ); +// assert( !Gia_ManObj(p, pSigs[4])->fMark1 ); + Gia_AcecMark_rec( p, pSigs[3], 1 ); + Gia_AcecMark_rec( p, pSigs[4], 1 ); +} +void Gia_AcecMarkHadd( Gia_Man_t * p, int * pSigs ) +{ + Gia_Obj_t * pObj = Gia_ManObj( p, pSigs[0] ); + int iFan0 = Gia_ObjFaninId0( pObj, pSigs[0] ); + int iFan1 = Gia_ObjFaninId1( pObj, pSigs[0] ); + Gia_ManObj( p, iFan0 )->fMark0 = 1; + Gia_ManObj( p, iFan1 )->fMark0 = 1; + Gia_AcecMark_rec( p, pSigs[0], 1 ); + Gia_AcecMark_rec( p, pSigs[1], 1 ); +} + +/**Function************************************************************* + + Synopsis [Collect XORs reachable from the last output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_AcecCollectXors_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Bit_t * vMap, Vec_Int_t * vXors ) +{ + if ( !Gia_ObjIsXor(pObj) )//|| Vec_BitEntry(vMap, Gia_ObjId(p, pObj)) ) + return; + Vec_IntPush( vXors, Gia_ObjId(p, pObj) ); + Gia_AcecCollectXors_rec( p, Gia_ObjFanin0(pObj), vMap, vXors ); + Gia_AcecCollectXors_rec( p, Gia_ObjFanin1(pObj), vMap, vXors ); +} +Vec_Int_t * Gia_AcecCollectXors( Gia_Man_t * p, Vec_Bit_t * vMap ) +{ + Vec_Int_t * vXors = Vec_IntAlloc( 100 ); + Gia_Obj_t * pObj = Gia_ObjFanin0( Gia_ManCo(p, Gia_ManCoNum(p)-1) ); + Gia_AcecCollectXors_rec( p, pObj, vMap, vXors ); + return vXors; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_AcecExplore( Gia_Man_t * p, int fVerbose ) +{ + Vec_Int_t * vNodes = Vec_IntAlloc( 100 ); + Vec_Int_t * vFadds, * vHadds, * vXors; + Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(p) ); + Gia_Obj_t * pObj; + int i, nSupp, nCone, nHadds = 0; + assert( p->pMuxes != NULL ); + vFadds = Gia_ManDetectFullAdders( p, fVerbose, NULL ); + vHadds = Gia_ManDetectHalfAdders( p, fVerbose ); + + pObj = Gia_ManObj( p, 352 ); + printf( "Xor = %d.\n", Gia_ObjIsXor(pObj) ); + printf( "Fanin0 = %d. Fanin1 = %d.\n", Gia_ObjFaninId0(pObj, 352), Gia_ObjFaninId1(pObj, 352) ); + printf( "Fan00 = %d. Fan01 = %d. Fan10 = %d. Fan11 = %d.\n", + Gia_ObjFaninId0(Gia_ObjFanin0(pObj), Gia_ObjFaninId0(pObj, 352)), + Gia_ObjFaninId1(Gia_ObjFanin0(pObj), Gia_ObjFaninId0(pObj, 352)), + Gia_ObjFaninId0(Gia_ObjFanin1(pObj), Gia_ObjFaninId1(pObj, 352)), + Gia_ObjFaninId1(Gia_ObjFanin1(pObj), Gia_ObjFaninId1(pObj, 352)) ); + + // create a map of all HADD/FADD outputs + for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ ) + { + int * pSigs = Vec_IntEntryP(vHadds, 2*i); + Vec_BitWriteEntry( vMap, pSigs[0], 1 ); + Vec_BitWriteEntry( vMap, pSigs[1], 1 ); + } + for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ ) + { + int * pSigs = Vec_IntEntryP(vFadds, 5*i); + Vec_BitWriteEntry( vMap, pSigs[3], 1 ); + Vec_BitWriteEntry( vMap, pSigs[4], 1 ); + } + + Gia_ManCleanMark01( p ); + + // mark outputs + Gia_ManForEachCo( p, pObj, i ) + Gia_ObjFanin0(pObj)->fMark0 = 1; + + // collect XORs + vXors = Gia_AcecCollectXors( p, vMap ); + Vec_BitFree( vMap ); + + printf( "Collected XORs: " ); + Vec_IntPrint( vXors ); + + // mark their fanins + Gia_ManForEachObjVec( vXors, p, pObj, i ) + { + pObj->fMark1 = 1; + Gia_ObjFanin0(pObj)->fMark0 = 1; + Gia_ObjFanin1(pObj)->fMark0 = 1; + } + + // mark FADDs + for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ ) + Gia_AcecMarkFadd( p, Vec_IntEntryP(vFadds, 5*i) ); + + // iterate through HADDs and find those that fit in + while ( 1 ) + { + int fChange = 0; + for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ ) + { + int * pSigs = Vec_IntEntryP(vHadds, 2*i); + if ( !Gia_ManObj(p, pSigs[0])->fMark0 || !Gia_ManObj(p, pSigs[1])->fMark0 ) + continue; + if ( Gia_ManObj(p, pSigs[0])->fMark1 || Gia_ManObj(p, pSigs[1])->fMark1 ) + continue; + Gia_AcecMarkHadd( p, pSigs ); + fChange = 1; + nHadds++; + } + if ( !fChange ) + break; + } + // print inputs to the adder network + Gia_ManForEachAnd( p, pObj, i ) + if ( pObj->fMark0 && !pObj->fMark1 ) + { + nSupp = Gia_ManSuppSize( p, &i, 1 ); + nCone = Gia_ManConeSize( p, &i, 1 ); + printf( "Node %5d : Supp = %5d. Cone = %5d.\n", i, nSupp, nCone ); + Vec_IntPush( vNodes, i ); + } + printf( "Fadds = %d. Hadds = %d. Root nodes found = %d.\n", Vec_IntSize(vFadds)/5, nHadds, Vec_IntSize(vNodes) ); + + Gia_ManCleanMark01( p ); + + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + pObj->fMark0 = 1; + + Vec_IntFree( vFadds ); + Vec_IntFree( vHadds ); + Vec_IntFree( vNodes ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_AcecCover( Gia_Man_t * p ) +{ + int fVerbose = 1; + int i, k, Entry; + Gia_Obj_t * pObj; + Vec_Int_t * vCutsXor2 = NULL; + Vec_Int_t * vFadds = Gia_ManDetectFullAdders( p, fVerbose, &vCutsXor2 ); + + // mark FADDs + Gia_ManCleanMark01( p ); + for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ ) + Gia_AcecMarkFadd( p, Vec_IntEntryP(vFadds, 5*i) ); + + k = 0; + Vec_IntForEachEntry( vCutsXor2, Entry, i ) + { + if ( i % 3 != 2 ) + continue; + pObj = Gia_ManObj( p, Entry ); + if ( pObj->fMark1 ) + continue; + printf( "%d ", Entry ); + } + printf( "\n" ); + + Gia_ManCleanMark01( p ); + + Vec_IntFree( vFadds ); + Vec_IntFree( vCutsXor2 ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/acecFadds.c b/src/proof/acec/acecFadds.c index 6b954398..7f6dcd53 100644 --- a/src/proof/acec/acecFadds.c +++ b/src/proof/acec/acecFadds.c @@ -59,6 +59,7 @@ Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose ) { if ( !Gia_ObjIsXor(pObj) ) continue; + Count = 0; iFan0 = Gia_ObjFaninId0(pObj, i); iFan1 = Gia_ObjFaninId1(pObj, i); if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 0))) ) @@ -69,6 +70,7 @@ Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose ) 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 @@ -116,7 +118,10 @@ Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose ) printf( "\n" ); Vec_IntForEachEntryDouble( vHadds, iXor, iAnd, i ) - printf( "%3d : %5d %5d\n", i, iXor, iAnd ); + { + pObj = Gia_ManObj( p, iXor ); + printf( "%3d : %5d %5d -> %5d %5d\n", i, Gia_ObjFaninId0(pObj, iXor), Gia_ObjFaninId1(pObj, iXor), iXor, iAnd ); + } } return vHadds; } @@ -255,6 +260,8 @@ int Dtc_ObjComputeTruth( Gia_Man_t * p, int iObj, int * pCut, int * pTruth ) Dtc_ObjCleanTruth_rec( Gia_ManObj(p, iObj) ); if ( pTruth ) *pTruth = Truth; + if ( Truth == 0x66 || Truth == 0x99 ) + return 3; if ( Truth == 0x96 || Truth == 0x69 ) return 1; if ( Truth == 0xE8 || Truth == 0xD4 || Truth == 0xB2 || Truth == 0x71 || @@ -262,11 +269,13 @@ int Dtc_ObjComputeTruth( Gia_Man_t * p, int iObj, int * pCut, int * pTruth ) return 2; return 0; } -void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Vec_Int_t * vCutsXor, Vec_Int_t * vCutsMaj ) +void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Vec_Int_t * vCutsXor2, Vec_Int_t * vCutsXor, Vec_Int_t * vCutsMaj ) { int fVerbose = 0; Vec_Int_t * vTemp; int i, k, c, Type, * pCut0, * pCut1, pCut[4]; + if ( fVerbose ) + printf( "Object %d = :\n", iObj ); Vec_IntFill( vCuts, 2, 1 ); Vec_IntPush( vCuts, iObj ); Dtc_ForEachCut( pList0, pCut0, i ) @@ -277,8 +286,28 @@ void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I if ( Dtc_ManCutCheckEqual(vCuts, pCut) ) continue; Vec_IntAddToEntry( vCuts, 0, 1 ); + if ( fVerbose ) + printf( "%d : ", pCut[0] ); for ( c = 0; c <= pCut[0]; c++ ) + { Vec_IntPush( vCuts, pCut[c] ); + if ( fVerbose && c ) + printf( "%d ", pCut[c] ); + } + if ( fVerbose ) + printf( "\n" ); + if ( pCut[0] == 2 ) + { + int Value = Dtc_ObjComputeTruth( p, iObj, pCut, NULL ); + assert( Value == 3 || Value == 0 ); + if ( Value == 3 ) + { + Vec_IntPush( vCutsXor2, pCut[1] ); + Vec_IntPush( vCutsXor2, pCut[2] ); + Vec_IntPush( vCutsXor2, iObj ); + } + continue; + } if ( pCut[0] != 3 ) continue; Type = Dtc_ObjComputeTruth( p, iObj, pCut, NULL ); @@ -298,11 +327,12 @@ void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I Vec_IntPush( vTemp, iObj ); } } -void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvCutsMaj, int fVerbose ) +void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor2, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvCutsMaj, int fVerbose ) { Gia_Obj_t * pObj; int * pList0, * pList1, i, nCuts = 0; Vec_Int_t * vTemp = Vec_IntAlloc( 1000 ); + Vec_Int_t * vCutsXor2 = Vec_IntAlloc( Gia_ManAndNum(p) ); Vec_Int_t * vCutsXor = Vec_IntAlloc( Gia_ManAndNum(p) ); Vec_Int_t * vCutsMaj = Vec_IntAlloc( Gia_ManAndNum(p) ); Vec_Int_t * vCuts = Vec_IntAlloc( 30 * Gia_ManAndNum(p) ); @@ -319,7 +349,7 @@ void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvC { pList0 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId0(pObj, i)) ); pList1 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId1(pObj, i)) ); - Dtc_ManCutMerge( p, i, pList0, pList1, vTemp, vCutsXor, vCutsMaj ); + Dtc_ManCutMerge( p, i, pList0, pList1, vTemp, vCutsXor2, vCutsXor, vCutsMaj ); Vec_IntWriteEntry( vCuts, i, Vec_IntSize(vCuts) ); Vec_IntAppend( vCuts, vTemp ); nCuts += Vec_IntEntry( vTemp, 0 ); @@ -329,6 +359,10 @@ void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvC Gia_ManAndNum(p), nCuts, 1.0*nCuts/Gia_ManAndNum(p), 1.0*Vec_IntSize(vCuts)/Gia_ManAndNum(p) ); Vec_IntFree( vTemp ); Vec_IntFree( vCuts ); + if ( pvCutsXor2 ) + *pvCutsXor2 = vCutsXor2; + else + Vec_IntFree( vCutsXor2 ); *pvCutsXor = vCutsXor; *pvCutsMaj = vCutsMaj; } @@ -375,6 +409,12 @@ void Dtc_ManPrintFadds( Vec_Int_t * vFadds ) printf( "%6d ", Vec_IntEntry(vFadds, 5*i+3) ); printf( "%6d ", Vec_IntEntry(vFadds, 5*i+4) ); printf( "\n" ); + + if ( i == 100 ) + { + printf( "Skipping other FADDs.\n" ); + break; + } } } int Dtc_ManCompare( int * pCut0, int * pCut1 ) @@ -394,10 +434,10 @@ int Dtc_ManCompare2( int * pCut0, int * pCut1 ) return 0; } // returns array of 5-tuples containing inputs/sum/cout of each full adder -Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose ) +Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** pvCutsXor2 ) { Vec_Int_t * vCutsXor, * vCutsMaj, * vFadds; - Dtc_ManComputeCuts( p, &vCutsXor, &vCutsMaj, fVerbose ); + Dtc_ManComputeCuts( p, pvCutsXor2, &vCutsXor, &vCutsMaj, fVerbose ); qsort( Vec_IntArray(vCutsXor), Vec_IntSize(vCutsXor)/4, 16, (int (*)(const void *, const void *))Dtc_ManCompare ); qsort( Vec_IntArray(vCutsMaj), Vec_IntSize(vCutsMaj)/4, 16, (int (*)(const void *, const void *))Dtc_ManCompare ); vFadds = Dtc_ManFindCommonCuts( p, vCutsXor, vCutsMaj ); @@ -762,7 +802,7 @@ Gia_Man_t * Gia_ManDupWithNaturalBoxes( Gia_Man_t * p, int nFaddMin, int fVerbos assert( Gia_ManBoxNum(p) == 0 ); // detect FADDs - vFadds = Gia_ManDetectFullAdders( p, fVerbose ); + vFadds = Gia_ManDetectFullAdders( p, fVerbose, NULL ); assert( Vec_IntSize(vFadds) % 5 == 0 ); // map MAJ into its FADD vMap = Gia_ManCreateMap( p, vFadds ); diff --git a/src/proof/acec/acecOrder.c b/src/proof/acec/acecOrder.c index 9b2242d0..93ef7f10 100644 --- a/src/proof/acec/acecOrder.c +++ b/src/proof/acec/acecOrder.c @@ -198,7 +198,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t ***********************************************************************/ Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose ) { - Vec_Int_t * vFadds = Gia_ManDetectFullAdders( pGia, fVeryVerbose ); + Vec_Int_t * vFadds = Gia_ManDetectFullAdders( pGia, fVeryVerbose, NULL ); 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) ); diff --git a/src/proof/acec/acecPolyn.c b/src/proof/acec/acecPolyn.c index be601405..042e0c59 100644 --- a/src/proof/acec/acecPolyn.c +++ b/src/proof/acec/acecPolyn.c @@ -64,26 +64,6 @@ struct Pln_Man_t_ /**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************************************************************* - Synopsis [Computation manager.] Description [] @@ -108,7 +88,7 @@ Pln_Man_t * Pln_ManAlloc( Gia_Man_t * pGia, Vec_Int_t * vOrder ) p->vTempM[1] = Vec_IntAlloc( 100 ); p->vTempM[2] = Vec_IntAlloc( 100 ); p->vTempM[3] = Vec_IntAlloc( 100 ); - p->vOrder = vOrder ? vOrder : Vec_IntStartNatural( Gia_ManObjNum(pGia) ); + p->vOrder = vOrder ? Vec_IntDup(vOrder) : Vec_IntStartNatural( Gia_ManObjNum(pGia) ); assert( Vec_IntSize(p->vOrder) == Gia_ManObjNum(pGia) ); Vec_QueSetPriority( p->vQue, Vec_FltArrayP(p->vCounts) ); // add 0-constant and 1-monomial @@ -131,36 +111,52 @@ 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 ); } +int Pln_ManCompare3( int * pData0, int * pData1 ) +{ + if ( pData0[0] < pData1[0] ) return -1; + if ( pData0[0] > pData1[0] ) return 1; + if ( pData0[1] < pData1[1] ) return -1; + if ( pData0[1] > pData1[1] ) return 1; + return 0; +} void Pln_ManPrintFinal( Pln_Man_t * p, int fVerbose, int fVeryVerbose ) { Vec_Int_t * vArray; - int k, Entry, iMono, iConst, Count = 0; + int i, k, Entry, iMono, iConst; + // collect triples + Vec_Int_t * vPairs = Vec_IntAlloc( 100 ); Vec_IntForEachEntry( p->vCoefs, iConst, iMono ) { if ( iConst == 0 ) continue; - - Count++; - - if ( !fVerbose ) - continue; - - if ( Count > 25 ) + vArray = Hsh_VecReadEntry( p->pHashC, iConst ); + Vec_IntPush( vPairs, Vec_IntEntry(vArray, 0) ); + vArray = Hsh_VecReadEntry( p->pHashM, iMono ); + Vec_IntPush( vPairs, Vec_IntSize(vArray) ? Vec_IntEntry(vArray, 0) : 0 ); + Vec_IntPushTwo( vPairs, iConst, iMono ); + } + // sort triples + qsort( Vec_IntArray(vPairs), Vec_IntSize(vPairs)/4, 16, (int (*)(const void *, const void *))Pln_ManCompare3 ); + // print + if ( fVerbose ) + Vec_IntForEachEntryDouble( vPairs, iConst, iMono, i ) + { + if ( i % 4 == 0 ) continue; - + printf( "%-6d : ", i/4 ); vArray = Hsh_VecReadEntry( p->pHashC, iConst ); Vec_IntForEachEntry( vArray, Entry, k ) printf( "%s%d", Entry < 0 ? "-" : "+", (1 << (Abc_AbsInt(Entry)-1)) ); - vArray = Hsh_VecReadEntry( p->pHashM, iMono ); Vec_IntForEachEntry( vArray, Entry, k ) printf( " * %d", Entry ); printf( "\n" ); } - printf( "HashC = %d. HashM = %d. Total = %d. Used = %d.\n", Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, Count ); + printf( "HashC = %d. HashM = %d. Total = %d. Used = %d. ", Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, Vec_IntSize(vPairs)/4 ); + Vec_IntFree( vPairs ); } /**Function************************************************************* @@ -400,7 +396,7 @@ void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fSigned, int fVer else Vec_BitSetEntry( vPres, LevCur, 1 ); - if ( fVerbose ) + if ( fVeryVerbose ) printf( "Line%5d Iter%10d : Obj =%6d. Order =%6d. HashC =%6d. HashM =%10d. Total =%10d. Used =%10d.\n", Line++, Iter, LevCur, Vec_IntEntry(p->vOrder, LevCur), Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, p->nUsed ); } @@ -409,14 +405,37 @@ void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fSigned, int fVer Gia_PolynBuildOne( p, iMono ); //clk2 += Abc_Clock() - temp; } - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); //Abc_PrintTime( 1, "Time2", clk2 ); Pln_ManPrintFinal( p, fVerbose, fVeryVerbose ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Pln_ManStop( p ); Vec_BitFree( vPres ); } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_PolynBuild2( Gia_Man_t * pGia, int fSigned, int fVerbose, int fVeryVerbose ) +{ + Hsh_VecMan_t * pHashC = Hsh_VecManStart( 1000 ); // hash table for constants + Hsh_VecMan_t * pHashM = Hsh_VecManStart( 1000 ); // hash table for monomials + Vec_Wec_t * vLit2Mono = Vec_WecStart( Gia_ManObjNum(pGia) * 2 ); + + Hsh_VecManStop( pHashC ); + Hsh_VecManStop( pHashM ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make index c70b0a7d..900d3f5f 100644 --- a/src/proof/acec/module.make +++ b/src/proof/acec/module.make @@ -1,4 +1,5 @@ SRC += src/proof/acec/acecCore.c \ + src/proof/acec/acecCover.c \ src/proof/acec/acecFadds.c \ src/proof/acec/acecOrder.c \ src/proof/acec/acecPolyn.c \ diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index a0b92b52..e8b243d3 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -108,6 +108,7 @@ struct Cec_ParFra_t_ int fColorDiff; // miter with separate outputs int fSatSweeping; // enable SAT sweeping int fRunCSat; // enable another solver + int fUseOrigIds; // enable recording of original IDs int fVeryVerbose; // verbose stats int fVerbose; // verbose stats int iOutFail; // the failed output diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index c9e9f67a..ed5c4ab7 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -236,7 +236,7 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) Gia_Man_t * pNew; Cec_ManPat_t * pPat; pPat = Cec_ManPatStart(); - Cec_ManSatSolve( pPat, pAig, pPars ); + Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL ); // pNew = Gia_ManDupDfsSkip( pAig ); pNew = Gia_ManDup( pAig ); Cec_ManPatStop( pPat ); @@ -351,6 +351,12 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil pIni = Gia_ManDup(pAig); pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL; pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL; + if ( pPars->fUseOrigIds ) + { + Gia_ManOrigIdsInit( pIni ); + Vec_IntFreeP( &pAig->vIdsEquiv ); + pAig->vIdsEquiv = Vec_IntAlloc( 1000 ); + } // prepare the managers // SAT sweeping @@ -429,7 +435,7 @@ clk = Abc_Clock(); if ( pPars->fRunCSat ) Cec_ManSatSolveCSat( pPat, pSrm, pParsSat ); else - Cec_ManSatSolve( pPat, pSrm, pParsSat ); + Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv ); p->timeSat += Abc_Clock() - clk; if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) ) { diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h index ef1dd983..d93e5e86 100644 --- a/src/proof/cec/cecInt.h +++ b/src/proof/cec/cecInt.h @@ -201,7 +201,7 @@ extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig ); extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig ); /*=== cecSolve.c ============================================================*/ extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj ); -extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ); +extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs ); extern void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ); extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats ); extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus ); diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c index e3db0b93..f75914e4 100644 --- a/src/proof/cec/cecSolve.c +++ b/src/proof/cec/cecSolve.c @@ -673,7 +673,7 @@ p->timeSatUndec += Abc_Clock() - clk; SeeAlso [] ***********************************************************************/ -void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ) +void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs ) { Bar_Progress_t * pProgress = NULL; Cec_ManSat_t * p; @@ -706,6 +706,16 @@ clk2 = Abc_Clock(); status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) ); pObj->fMark0 = (status == 0); pObj->fMark1 = (status == 1); + if ( status == 1 && vIdsOrig ) + { + int iObj1 = Vec_IntEntry(vMiterPairs, 2*i); + int iObj2 = Vec_IntEntry(vMiterPairs, 2*i+1); + int OrigId1 = Vec_IntEntry(vIdsOrig, iObj1); + int OrigId2 = Vec_IntEntry(vIdsOrig, iObj2); + assert( OrigId1 >= 0 && OrigId2 >= 0 ); + Vec_IntPushTwo( vEquivPairs, OrigId1, OrigId2 ); + } + /* if ( status == -1 ) { diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c index a9ed17fc..a3a7e66f 100644 --- a/src/proof/ssw/sswConstr.c +++ b/src/proof/ssw/sswConstr.c @@ -533,8 +533,10 @@ clk = Abc_Clock(); continue; } Ssw_NodesAreConstrained( p, pObjNew, Aig_ManConst0(p->pFrames) ); - } - + } + // sweep flops + Saig_ManForEachLo( p->pAig, pObj, i ) + p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 1 ); // sweep internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) { diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c index 6db673cc..77cb24de 100644 --- a/src/proof/ssw/sswSweep.c +++ b/src/proof/ssw/sswSweep.c @@ -287,6 +287,9 @@ clk = Abc_Clock(); Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) ); + // sweep flops + Saig_ManForEachLo( p->pAig, pObj, i ) + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL ); // sweep internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) { |