summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/acec/acec.h13
-rw-r--r--src/proof/acec/acecCore.c10
-rw-r--r--src/proof/acec/acecFadds.c66
-rw-r--r--src/proof/acec/acecInt.h7
-rw-r--r--src/proof/acec/acecOrder.c172
-rw-r--r--src/proof/acec/acecPolyn.c44
6 files changed, 198 insertions, 114 deletions
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 );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-14 06:02:23 +0000