summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaShow.c14
-rw-r--r--src/base/abci/abc.c2
-rw-r--r--src/misc/vec/vecInt.h18
-rw-r--r--src/misc/vec/vecWec.h17
-rw-r--r--src/proof/acec/acecCore.c108
-rw-r--r--src/proof/acec/acecMult.c20
-rw-r--r--src/proof/acec/acecNorm.c2
-rw-r--r--src/proof/acec/acecRe.c27
-rw-r--r--src/proof/acec/acecTree.c28
9 files changed, 201 insertions, 35 deletions
diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c
index cf89d942..4dd85aab 100644
--- a/src/aig/gia/giaShow.c
+++ b/src/aig/gia/giaShow.c
@@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+#define NODE_MAX 2000
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -79,11 +81,11 @@ void Gia_ShowPath( Gia_Man_t * p, char * pFileName )
}
}
- if ( nNodes > 500 )
+ if ( nNodes > NODE_MAX )
{
ABC_FREE( pLevels );
Vec_BitFree( vPath );
- fprintf( stdout, "Cannot visualize AIG with more than 500 critical nodes.\n" );
+ fprintf( stdout, "Cannot visualize AIG with more than %d critical nodes.\n", NODE_MAX );
return;
}
if ( (pFile = fopen( pFileName, "w" )) == NULL )
@@ -341,9 +343,9 @@ void Gia_WriteDotAigSimple( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold )
int LevelMax, Prev, Level, i;
int fConstIsUsed = 0;
- if ( Gia_ManAndNum(p) > 500 )
+ if ( Gia_ManAndNum(p) > NODE_MAX )
{
- fprintf( stdout, "Cannot visualize AIG with more than 500 nodes.\n" );
+ fprintf( stdout, "Cannot visualize AIG with more than %d nodes.\n", NODE_MAX );
return;
}
if ( (pFile = fopen( pFileName, "w" )) == NULL )
@@ -678,9 +680,9 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_In
int fConstIsUsed = 0;
int nFadds = Ree_ManCountFadds( vAdds );
- if ( Gia_ManAndNum(p) > 1000 )
+ if ( Gia_ManAndNum(p) > NODE_MAX )
{
- fprintf( stdout, "Cannot visualize AIG with more than 1000 nodes.\n" );
+ fprintf( stdout, "Cannot visualize AIG with more than %d nodes.\n", NODE_MAX );
return;
}
if ( (pFile = fopen( pFileName, "w" )) == NULL )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1e94f28f..9db3d7d6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -42690,7 +42690,7 @@ 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 );
-// Gia_PolynExplore( pAbc->pGia );
+ Acec_MultFindPPsTest( pAbc->pGia );
// printf( "\nThis command is currently disabled.\n\n" );
return 0;
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index f09b8783..d952518f 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1692,6 +1692,24 @@ static inline int Vec_IntTwoFindCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Ve
}
return Vec_IntSize(vArr);
}
+static inline int Vec_IntTwoFindCommonReverse( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr )
+{
+ int * pBeg1 = vArr1->pArray;
+ int * pBeg2 = vArr2->pArray;
+ int * pEnd1 = vArr1->pArray + vArr1->nSize;
+ int * pEnd2 = vArr2->pArray + vArr2->nSize;
+ Vec_IntClear( vArr );
+ while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ {
+ if ( *pBeg1 == *pBeg2 )
+ Vec_IntPush( vArr, *pBeg1 ), pBeg1++, pBeg2++;
+ else if ( *pBeg1 > *pBeg2 )
+ pBeg1++;
+ else
+ pBeg2++;
+ }
+ return Vec_IntSize(vArr);
+}
/**Function*************************************************************
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index e4e92503..8180e984 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -303,6 +303,23 @@ static inline Vec_Int_t * Vec_WecPushLevel( Vec_Wec_t * p )
++p->nSize;
return Vec_WecEntryLast( p );
}
+static inline Vec_Int_t * Vec_WecInsertLevel( Vec_Wec_t * p, int i )
+{
+ Vec_Int_t * pTemp;
+ if ( p->nSize == p->nCap )
+ {
+ if ( p->nCap < 16 )
+ Vec_WecGrow( p, 16 );
+ else
+ Vec_WecGrow( p, 2 * p->nCap );
+ }
+ ++p->nSize;
+ assert( i >= 0 && i < p->nSize );
+ for ( pTemp = p->pArray + p->nSize - 2; pTemp >= p->pArray + i; pTemp-- )
+ pTemp[1] = pTemp[0];
+ Vec_IntZero( p->pArray + i );
+ return p->pArray + i;
+}
/**Function*************************************************************
diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index 4a91663f..6b631a1b 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -20,6 +20,8 @@
#include "acecInt.h"
#include "proof/cec/cec.h"
+#include "misc/util/utilTruth.h"
+#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
@@ -118,18 +120,19 @@ Vec_Int_t * Acec_CountRemap( Gia_Man_t * pAdd, Gia_Man_t * pBase )
}
void Acec_ComputeEquivClasses( Gia_Man_t * pOne, Gia_Man_t * pTwo, Vec_Int_t ** pvMap1, Vec_Int_t ** pvMap2 )
{
+ abctime clk = Abc_Clock();
Gia_Man_t * pBase, * pRepr;
pBase = Acec_CommonStart( NULL, pOne );
pBase = Acec_CommonStart( pBase, pTwo );
Acec_CommonFinish( pBase );
-
//Gia_ManShow( pBase, NULL, 0, 0, 0 );
-
pRepr = Gia_ManComputeGiaEquivs( pBase, 100, 0 );
*pvMap1 = Acec_CountRemap( pOne, pBase );
*pvMap2 = Acec_CountRemap( pTwo, pBase );
Gia_ManStop( pBase );
Gia_ManStop( pRepr );
+ printf( "Finished computing equivalent nodes. " );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCostLits )
{
@@ -143,8 +146,10 @@ void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCostLits )
ABC_SWAP( int, pArray[i], pArray[best_i] );
}
}
-void Acec_MatchPrintEquivLits( Vec_Wec_t * vLits, 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 * vLevel;
int i, k, Entry;
printf( "Leaf literals and their classes:\n" );
@@ -155,6 +160,85 @@ void Acec_MatchPrintEquivLits( Vec_Wec_t * vLits, int * pCostLits )
printf( "%s%d(%d) ", Abc_LitIsCompl(Entry) ? "-":"+", Abc_Lit2Var(Entry), Abc_Lit2LitL(pCostLits, Entry) );
printf( "\n" );
}
+ if ( !fVerbose )
+ return;
+ Vec_WecForEachLevel( vLits, vLevel, i )
+ {
+ if ( i != 20 )
+ continue;
+ Vec_IntForEachEntry( vLevel, Entry, k )
+ {
+ word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
+ printf( "Rank = %4d : ", i );
+ printf( "Obj = %4d ", Abc_Lit2Var(Entry) );
+ if ( Vec_IntSize(vSupp) > 6 )
+ {
+ printf( "Supp = %d.\n", Vec_IntSize(vSupp) );
+ continue;
+ }
+ vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
+ if ( Vec_IntSize(vSupp) > 5 )
+ {
+ printf( "Supp = %d.\n", Vec_IntSize(vSupp) );
+ continue;
+ }
+ Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) );
+ if ( Vec_IntSize(vSupp) == 4 ) printf( " " );
+ if ( Vec_IntSize(vSupp) == 3 ) printf( " " );
+ if ( Vec_IntSize(vSupp) <= 2 ) printf( " " );
+ printf( " " );
+ Vec_IntPrint( vSupp );
+ }
+ printf( "\n" );
+ }
+ Vec_IntFree( vSupp );
+ Vec_WrdFree( vTemp );
+}
+Vec_Wec_t * Acec_MatchCopy( Vec_Wec_t * vLits, Vec_Int_t * vMap )
+{
+ Vec_Wec_t * vRes = Vec_WecStart( Vec_WecSize(vLits) );
+ Vec_Int_t * vLevel; int i, k, iLit;
+ Vec_WecForEachLevel( vLits, vLevel, i )
+ Vec_IntForEachEntry( vLevel, iLit, k )
+ Vec_WecPush( vRes, i, Abc_Lit2LitL(Vec_IntArray(vMap), iLit) );
+ return vRes;
+}
+int Acec_MatchCountCommon( Vec_Wec_t * vLits1, Vec_Wec_t * vLits2, int Shift )
+{
+ Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+ Vec_Int_t * vLevel1, * vLevel2;
+ int i, nCommon = 0;
+ Vec_WecForEachLevel( vLits1, vLevel1, i )
+ {
+ if ( i+Shift < 0 || i+Shift >= Vec_WecSize(vLits2) )
+ continue;
+ vLevel2 = Vec_WecEntry( vLits2, i+Shift );
+ nCommon += Vec_IntTwoFindCommonReverse( vLevel1, vLevel2, vRes );
+ }
+ 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 )
+{
+ Vec_Wec_t * vRes0 = Acec_MatchCopy( vLits0, vMap0 );
+ Vec_Wec_t * vRes1 = Acec_MatchCopy( vLits1, vMap1 );
+ int nCommon = Acec_MatchCountCommon( vRes0, vRes1, 0 );
+ int nCommonPlus = Acec_MatchCountCommon( vRes0, vRes1, 1 );
+ int nCommonMinus = Acec_MatchCountCommon( vRes0, vRes1, -1 );
+ if ( nCommonPlus >= nCommonMinus && nCommonPlus > nCommon )
+ {
+ Vec_WecInsertLevel( vLits0, 0 );
+ Vec_WecInsertLevel( vRoots0, 0 );
+ }
+ else if ( nCommonMinus > nCommonPlus && nCommonMinus > nCommon )
+ {
+ Vec_WecInsertLevel( vLits1, 0 );
+ Vec_WecInsertLevel( vRoots1, 0 );
+ }
+ Vec_WecPrint( vRes0, 0 );
+ Vec_WecPrint( vRes1, 0 );
+ Vec_WecFree( vRes0 );
+ Vec_WecFree( vRes1 );
}
int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
{
@@ -166,8 +250,11 @@ 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_MatchPrintEquivLits( pBox0->vLeafLits, Vec_IntArray(vMap0) );
- //Acec_MatchPrintEquivLits( pBox1->vLeafLits, Vec_IntArray(vMap1) );
+ Acec_MatchCheckShift( 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 );
+
// reorder nodes to have the same order
assert( pBox0->vShared == NULL );
assert( pBox1->vShared == NULL );
@@ -216,11 +303,15 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
assert( Vec_IntSize(vShared0) + Vec_IntSize(vUnique0) == Vec_IntSize(vLevel0) );
assert( Vec_IntSize(vShared1) + Vec_IntSize(vUnique1) == Vec_IntSize(vLevel1) );
}
- Vec_IntFree( vMap0 );
- Vec_IntFree( vMap1 );
nTotal = Vec_WecSizeSize(pBox0->vShared);
printf( "Box0: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox0->vLeafLits) );
printf( "Box1: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox1->vLeafLits) );
+
+ //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vUnique, Vec_IntArray(vMap0), 0 );
+ //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vUnique, Vec_IntArray(vMap1), 0 );
+
+ Vec_IntFree( vMap0 );
+ Vec_IntFree( vMap1 );
return nTotal;
}
@@ -258,6 +349,9 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
pGia1n = Acec_InsertBox( pBox1, 1 );
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 );
}
// solve regular CEC problem
Cec_ManCecSetDefaultParams( pCecPars );
diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c
index 0733c00b..d868c399 100644
--- a/src/proof/acec/acecMult.c
+++ b/src/proof/acec/acecMult.c
@@ -504,14 +504,18 @@ Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p )
break;
}
}
-/*
- Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) );
- if ( Vec_IntSize(vSupp) == 4 ) printf( " " );
- if ( Vec_IntSize(vSupp) == 3 ) printf( " " );
- if ( Vec_IntSize(vSupp) <= 2 ) printf( " " );
- printf( " " );
- Vec_IntPrint( vSupp );
-*/
+ /*
+ if ( Saved[i] )
+ {
+ printf( "Obj = %4d ", iObj );
+ Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) );
+ if ( Vec_IntSize(vSupp) == 4 ) printf( " " );
+ if ( Vec_IntSize(vSupp) == 3 ) printf( " " );
+ if ( Vec_IntSize(vSupp) <= 2 ) printf( " " );
+ printf( " " );
+ Vec_IntPrint( vSupp );
+ }
+ */
}
Gia_ManCleanMark0(p);
printf( "Collected %d pps and %d nodes.\n", nProds, Vec_IntSize(vBold) );
diff --git a/src/proof/acec/acecNorm.c b/src/proof/acec/acecNorm.c
index 4ed32e7b..0d209524 100644
--- a/src/proof/acec/acecNorm.c
+++ b/src/proof/acec/acecNorm.c
@@ -112,7 +112,7 @@ int Acec_InsertBox_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
assert( Gia_ObjIsAnd(pObj) );
Acec_InsertBox_rec( pNew, p, Gia_ObjFanin0(pObj) );
Acec_InsertBox_rec( pNew, p, Gia_ObjFanin1(pObj) );
- return (pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ));
+ return (pObj->Value = Gia_ManAppendAnd2( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ));
}
Vec_Int_t * Acec_BuildTree( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Wec_t * vLeafLits )
{
diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c
index 161b6fbb..7f87df85 100644
--- a/src/proof/acec/acecRe.c
+++ b/src/proof/acec/acecRe.c
@@ -147,6 +147,7 @@ static inline int Ree_ManCutFind( int iObj, int * pCut )
}
static inline int Ree_ManCutNotFind( int iObj1, int iObj2, int * pCut )
{
+ assert( pCut[0] == 3 );
if ( pCut[3] != iObj1 && pCut[3] != iObj2 ) return 0;
if ( pCut[2] != iObj1 && pCut[2] != iObj2 ) return 1;
if ( pCut[1] != iObj1 && pCut[1] != iObj2 ) return 2;
@@ -162,13 +163,19 @@ static inline int Ree_ManCutTruthOne( int * pCut0, int * pCut )
Truth0 = fComp0 ? ~Truth0 : Truth0;
if ( pCut0[0] == 2 )
{
- int Truths[3][8] = {
- { 0x00, 0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77 }, // {0,1,-}
- { 0x00, 0x05, 0x0A, 0x0F, 0x50, 0x55, 0x5A, 0x5F }, // {0,-,1}
- { 0x00, 0x03, 0x0C, 0x0F, 0x30, 0x33, 0x3C, 0x3F } // {-,0,1}
- };
- int Truth = Truths[Ree_ManCutNotFind(pCut0[1], pCut0[2], pCut)][Truth0 & 0x7];
- return 0xFF & (fComp0 ? ~Truth : Truth);
+ if ( pCut[0] == 3 )
+ {
+ int Truths[3][8] = {
+ { 0x00, 0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77 }, // {0,1,-}
+ { 0x00, 0x05, 0x0A, 0x0F, 0x50, 0x55, 0x5A, 0x5F }, // {0,-,1}
+ { 0x00, 0x03, 0x0C, 0x0F, 0x30, 0x33, 0x3C, 0x3F } // {-,0,1}
+ };
+ int Truth = Truths[Ree_ManCutNotFind(pCut0[1], pCut0[2], pCut)][Truth0 & 0x7];
+ return 0xFF & (fComp0 ? ~Truth : Truth);
+ }
+ assert( pCut[0] == 2 );
+ assert( pCut[1] == pCut0[1] && pCut[2] == pCut0[2] );
+ return pCut0[pCut0[0]+1];
}
if ( pCut0[0] == 1 )
{
@@ -236,10 +243,10 @@ int Ree_ObjComputeTruth( Gia_Man_t * p, int iObj, int * pCut )
SeeAlso []
***********************************************************************/
-void Ree_ManCutPrint( int * pCut, int Count, word Truth )
+void Ree_ManCutPrint( int * pCut, int Count, word Truth, int iObj )
{
int c;
- printf( "%d : ", Count );
+ printf( "%d : %d : ", Count, iObj );
for ( c = 1; c <= pCut[0]; c++ )
printf( "%3d ", pCut[c] );
for ( ; c <= 4; c++ )
@@ -290,7 +297,7 @@ void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
Vec_IntPushThree( vData, iObj, Value, TruthC );
}
if ( fVerbose )
- Ree_ManCutPrint( pCut, ++Count, TruthC );
+ Ree_ManCutPrint( pCut, ++Count, TruthC, iObj );
}
if ( !vXors )
return;
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
index fef36923..295fd738 100644
--- a/src/proof/acec/acecTree.c
+++ b/src/proof/acec/acecTree.c
@@ -392,7 +392,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;
@@ -478,7 +478,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;
+ int i, j, k, Box, Rank, Count = 0;
Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
pBox->pGia = p;
@@ -532,6 +532,30 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
Vec_IntSort( vLevel, 0 );
Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
Vec_IntSort( vLevel, 0 );
+ //return pBox;
+ // push literals forward
+ //Vec_WecPrint( pBox->vLeafLits, 0 );
+ Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
+ {
+ int This, Prev = Vec_IntEntry(vLevel, 0);
+ Vec_IntForEachEntryStart( vLevel, This, j, 1 )
+ {
+ if ( Prev != This )
+ {
+ Prev = This;
+ continue;
+ }
+ if ( i+1 >= Vec_WecSize(pBox->vLeafLits) )
+ continue;
+ Vec_IntPushOrder( Vec_WecEntry(pBox->vLeafLits, i+1), This );
+ Vec_IntDrop( vLevel, j-- );
+ Vec_IntDrop( vLevel, j-- );
+ Prev = -1;
+ Count++;
+ }
+ }
+ printf( "Pushed forward %d input literals.\n", Count );
+ //Vec_WecPrint( pBox->vLeafLits, 0 );
return pBox;
}
void Acec_CreateBoxTest( Gia_Man_t * p )
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 18:29:03 +0000