summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/proof/acec/acecCl.c33
-rw-r--r--src/proof/acec/acecCore.c20
-rw-r--r--src/proof/acec/acecInt.h2
-rw-r--r--src/proof/acec/acecNorm.c2
-rw-r--r--src/proof/acec/acecTree.c28
5 files changed, 55 insertions, 30 deletions
diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c
index 6a5f4040..6185677b 100644
--- a/src/proof/acec/acecCl.c
+++ b/src/proof/acec/acecCl.c
@@ -350,9 +350,15 @@ 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 i, k, iStart, iLit, Driver, Count = 0;
+ // determine how much to shift
+ Driver = Gia_ObjFaninId0p( p, Gia_ManCo(p, 0) );
+ Vec_WecForEachLevel( pBox->vRootLits, vLevel, iStart )
+ if ( Abc_Lit2Var(Vec_IntEntry(vLevel,0)) == Driver )
+ break;
+ assert( iStart < Gia_ManCoNum(p) );
+ //Vec_WecPrintLits( pBox->vRootLits );
+ Vec_WecForEachLevelStart( pBox->vRootLits, vLevel, i, iStart )
{
int In[3] = {0}, Out[2];
assert( Vec_IntSize(vLevel) > 0 );
@@ -370,9 +376,11 @@ Vec_Int_t * Acec_RewriteTop( Gia_Man_t * p, Acec_Box_t * pBox )
Vec_IntPush( Vec_WecEntry(pBox->vRootLits, i+1), Out[1] );
else
Vec_IntPush( Vec_WecPushLevel(pBox->vRootLits), Out[1] );
+ Count++;
}
assert( Vec_IntSize(vRes) >= Gia_ManCoNum(p) );
Vec_IntShrink( vRes, Gia_ManCoNum(p) );
+ printf( "Added %d adders for replace CLAs. ", Count );
return vRes;
}
Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
@@ -384,7 +392,6 @@ Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
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 )
@@ -394,22 +401,26 @@ Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
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 );
+ Gia_Obj_t * pRepr = Gia_ManObj( p, Abc_Lit2Var(iLit) );
+ pObj->Value = Gia_ManAppendCo( pNew, pRepr->Value );
}
+ // set correct phase
+ Gia_ManSetPhase( p );
+ Gia_ManSetPhase( pNew );
+ Gia_ManForEachCo( pNew, pObj, i )
+ if ( Gia_ObjPhase(pObj) != Gia_ObjPhase(Gia_ManCo(p, i)) )
+ Gia_ObjFlipFaninC0( pObj );
+ // remove dangling nodes
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 );
+ Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, 0, 0, fVerbose );
Vec_Int_t * vResult;
Vec_BitFreeP( &vIgnore );
if ( pBox == NULL ) // cannot match
@@ -418,8 +429,10 @@ Gia_Man_t * Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose )
return Gia_ManDup( pGia );
}
vResult = Acec_RewriteTop( pGia, pBox );
+ Acec_BoxFreeP( &pBox );
pNew = Acec_RewriteReplace( pGia, vResult );
Vec_IntFree( vResult );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return pNew;
}
diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index 4fddcfab..06385f3c 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -328,12 +328,12 @@ void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLi
}
//printf( "Input literals:\n" );
//Vec_WecPrintLits( vLits0 );
- printf( "Equiv classes:\n" );
- Vec_WecPrintLits( vRes0 );
+ //printf( "Equiv classes:\n" );
+ //Vec_WecPrintLits( vRes0 );
//printf( "Input literals:\n" );
//Vec_WecPrintLits( vLits1 );
- printf( "Equiv classes:\n" );
- Vec_WecPrintLits( vRes1 );
+ //printf( "Equiv classes:\n" );
+ //Vec_WecPrintLits( vRes1 );
//Acec_VerifyClasses( pGia0, vLits0, vRes0 );
//Acec_VerifyClasses( pGia1, vLits1, vRes1 );
Vec_WecFree( vRes0 );
@@ -353,10 +353,10 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
//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 );
+ //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 );
@@ -438,8 +438,8 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
Cec_ParCec_t ParsCec, * pCecPars = &ParsCec;
Vec_Bit_t * vIgnore0 = pPars->fBooth ? Acec_BoothFindPPG(pGia0) : NULL;
Vec_Bit_t * vIgnore1 = pPars->fBooth ? Acec_BoothFindPPG(pGia1) : NULL;
- Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, vIgnore0, pPars->fVerbose );
- Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, pPars->fVerbose );
+ Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, vIgnore0, 0, 0, pPars->fVerbose );
+ Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, 0, 0, pPars->fVerbose );
Vec_BitFreeP( &vIgnore0 );
Vec_BitFreeP( &vIgnore1 );
if ( pBox0 == NULL || pBox1 == NULL ) // cannot match
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h
index c49945db..b8ec2455 100644
--- a/src/proof/acec/acecInt.h
+++ b/src/proof/acec/acecInt.h
@@ -75,7 +75,7 @@ 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 Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut, int fVerbose );
extern void Acec_BoxFreeP( Acec_Box_t ** ppBox );
/*=== acecUtil.c ========================================================*/
extern void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose );
diff --git a/src/proof/acec/acecNorm.c b/src/proof/acec/acecNorm.c
index 0d209524..6b36589c 100644
--- a/src/proof/acec/acecNorm.c
+++ b/src/proof/acec/acecNorm.c
@@ -201,7 +201,7 @@ Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll )
Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fBooth, int fVerbose )
{
Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG( pGia ) : NULL;
- Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, fVerbose );
+ Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, 0, 0, fVerbose );
Gia_Man_t * pNew = Acec_InsertBox( pBox, 1 );
Acec_BoxFreeP( &pBox );
Vec_BitFreeP( &vIgnore );
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
index 2b356574..fe5ca01b 100644
--- a/src/proof/acec/acecTree.c
+++ b/src/proof/acec/acecTree.c
@@ -127,6 +127,10 @@ 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 )
{
+ // special case of the first bit
+// if ( i == 0 )
+// continue;
+
/*
if ( Vec_IntEntry(vAdds, 6*Box+3) == 24 && Vec_IntEntry(vAdds, 6*Box+4) == 22 )
{
@@ -415,7 +419,7 @@ Vec_Int_t * Acec_TreeFindPoints( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * v
int i;
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
- if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) )
+ if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) && Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) )
continue;
Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+0), i, 0 );
Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+1), i, 0 );
@@ -468,7 +472,7 @@ void Acec_TreeFindTrees_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iObj, int
Acec_TreeFindTrees2_rec( vAdds, vMap, In, Acec_TreeWhichPoint(vAdds, In, iObj) == 4 ? Rank-1 : Rank, vTree, vFound );
Acec_TreeFindTrees2_rec( vAdds, vMap, Out, Rank, vTree, vFound );
}
-Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vIgnore )
+Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut )
{
Vec_Wec_t * vTrees = Vec_WecAlloc( 10 );
Vec_Int_t * vMap = Acec_TreeFindPoints( p, vAdds, vIgnore );
@@ -495,7 +499,10 @@ 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 );
+ if ( fFilterIn )
+ Acec_TreeFilterTrees2( p, vAdds, vTrees );
+ else if ( fFilterOut )
+ Acec_TreeFilterTrees( p, vAdds, vTrees );
// sort by size
Vec_WecSort( vTrees, 1 );
return vTrees;
@@ -511,7 +518,7 @@ void Acec_TreeFindTreesTest( Gia_Man_t * p )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
clk = Abc_Clock();
- vTrees = Acec_TreeFindTrees( p, vAdds, NULL );
+ vTrees = Acec_TreeFindTrees( p, vAdds, NULL, 0, 0 );
printf( "Collected %d trees with %d adders in them. ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Vec_WecPrint( vTrees, 0 );
@@ -572,7 +579,7 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Int_t * vLevel, * vMap;
- int i, j, k, Box, Rank, Count = 0;
+ int i, j, k, Box, Rank;//, Count = 0;
Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
pBox->pGia = p;
@@ -583,6 +590,11 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
// collect boxes; mark inputs/outputs
Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
{
+// if ( 37 == Box && 6 == Rank )
+// {
+// printf( "Skipping one adder...\n" );
+// continue;
+// }
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 );
@@ -677,7 +689,7 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
clk = Abc_Clock();
- vTrees = Acec_TreeFindTrees( p, vAdds, NULL );
+ vTrees = Acec_TreeFindTrees( p, vAdds, NULL, 0, 0 );
printf( "Collected %d trees with %d adders in them. ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
//Vec_WecPrint( vTrees, 0 );
@@ -707,11 +719,11 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose )
+Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut, int fVerbose )
{
Acec_Box_t * pBox = NULL;
Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, fVerbose );
- Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore );
+ Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore, fFilterIn, fFilterOut );
if ( vTrees && Vec_WecSize(vTrees) > 0 )
{
pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, 0) );
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-03 18:14:24 +0000