summaryrefslogtreecommitdiffstats
path: root/src/temp/ivy/ivyMulti.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/temp/ivy/ivyMulti.c')
-rw-r--r--src/temp/ivy/ivyMulti.c504
1 files changed, 189 insertions, 315 deletions
diff --git a/src/temp/ivy/ivyMulti.c b/src/temp/ivy/ivyMulti.c
index 059d1500..e2a44e2d 100644
--- a/src/temp/ivy/ivyMulti.c
+++ b/src/temp/ivy/ivyMulti.c
@@ -24,22 +24,18 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-typedef struct Ivy_Eval_t_ Ivy_Eval_t;
-struct Ivy_Eval_t_
+#define IVY_EVAL_LIMIT 128
+
+typedef struct Ivy_Eva_t_ Ivy_Eva_t;
+struct Ivy_Eva_t_
{
- unsigned Mask : 5; // the mask of covered nodes
- unsigned Weight : 3; // the number of covered nodes
- unsigned Cost : 4; // the number of overlapping nodes
- unsigned Level : 12; // the level of this node
- unsigned Fan0 : 4; // the first fanin
- unsigned Fan1 : 4; // the second fanin
+ Ivy_Obj_t * pArg; // the argument node
+ unsigned Mask; // the mask of covered nodes
+ int Weight; // the number of covered nodes
};
-static Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
-static void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs );
-static int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode );
-static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
-
+static void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals );
+static int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -47,212 +43,121 @@ static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type
/**Function*************************************************************
- Synopsis [Constructs the well-balanced tree of gates.]
-
- Description [Disregards levels and possible logic sharing.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type )
-{
- Ivy_Obj_t * pObj1, * pObj2;
- if ( nObjs == 1 )
- return ppObjs[0];
- pObj1 = Ivy_Multi_rec( ppObjs, nObjs/2, Type );
- pObj2 = Ivy_Multi_rec( ppObjs + nObjs/2, nObjs - nObjs/2, Type );
- return Ivy_Oper( pObj1, pObj2, Type );
-}
-
-/**Function*************************************************************
-
Synopsis [Constructs a balanced tree while taking sharing into account.]
- Description []
+ Description [Returns 1 if the implementation exists.]
SideEffects []
SeeAlso []
***********************************************************************/
-Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgsInit, int nArgs, Ivy_Type_t Type )
+int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSols )
{
- static char NumBits[32] = {0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5};
- static Ivy_Eval_t pEvals[15+15*14/2];
- static Ivy_Obj_t * pArgs[16];
- Ivy_Eval_t * pEva, * pEvaBest;
- int nArgsNew, nEvals, i, k;
- Ivy_Obj_t * pTemp;
-
- // consider the case of one argument
- assert( nArgs > 0 );
- if ( nArgs == 1 )
- return pArgsInit[0];
- // consider the case of two arguments
- if ( nArgs == 2 )
- return Ivy_Oper( pArgsInit[0], pArgsInit[1], Type );
-
-//Ivy_MultiEval( pArgsInit, nArgs, Type ); printf( "\n" );
-
- // set the initial ones
- for ( i = 0; i < nArgs; i++ )
+ static Ivy_Eva_t pEvals[IVY_EVAL_LIMIT];
+ Ivy_Eva_t * pEval, * pFan0, * pFan1;
+ Ivy_Obj_t * pObj, * pTemp;
+ int nEvals, nEvalsOld, i, k, x, nLeaves;
+ unsigned uMaskAll;
+
+ // consider special cases
+ nLeaves = Vec_PtrSize(vLeaves);
+ assert( nLeaves > 2 );
+ if ( nLeaves > 32 || nLeaves + Vec_PtrSize(vCone) > IVY_EVAL_LIMIT )
+ return 0;
+// if ( nLeaves == 1 )
+// return Vec_PtrEntry( vLeaves, 0 );
+// if ( nLeaves == 2 )
+// return Ivy_Oper( Vec_PtrEntry(vLeaves, 0), Vec_PtrEntry(vLeaves, 1), Type );
+
+ // set the leaf entries
+ uMaskAll = ((1 << nLeaves) - 1);
+ nEvals = 0;
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
{
- pArgs[i] = pArgsInit[i];
- pEva = pEvals + i;
- pEva->Mask = (1 << i);
- pEva->Weight = 1;
- pEva->Cost = 0;
- pEva->Level = Ivy_Regular(pArgs[i])->Level;
- pEva->Fan0 = 0;
- pEva->Fan1 = 0;
+ pEval = pEvals + nEvals;
+ pEval->pArg = pObj;
+ pEval->Mask = (1 << nEvals);
+ pEval->Weight = 1;
+ // mark the leaf
+ Ivy_Regular(pObj)->TravId = nEvals;
+ nEvals++;
}
- // find the available nodes
- pEvaBest = pEvals;
- nArgsNew = nArgs;
- for ( i = 1; i < nArgsNew; i++ )
- for ( k = 0; k < i; k++ )
- if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)) )
- {
- pEva = pEvals + nArgsNew;
- pEva->Mask = pEvals[k].Mask | pEvals[i].Mask;
- pEva->Weight = NumBits[pEva->Mask];
- pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask];
- pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level);
- pEva->Fan0 = k;
- pEva->Fan1 = i;
-// assert( pEva->Level == (unsigned)Ivy_ObjLevel(pTemp) );
- // compare
- if ( pEvaBest->Weight < pEva->Weight ||
- pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost ||
- pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level )
- pEvaBest = pEva;
- // save the argument
- pArgs[nArgsNew++] = pTemp;
- if ( nArgsNew == 15 )
- goto Outside;
- }
-Outside:
-
-// printf( "Best = %d.\n", pEvaBest - pEvals );
-
- // the case of no common nodes
- if ( nArgsNew == nArgs )
+ // propagate masks through the cone
+ Vec_PtrForEachEntry( vCone, pObj, i )
{
- Ivy_MultiSort( pArgs, nArgs );
- return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+ pObj->TravId = nEvals + i;
+ if ( Ivy_ObjIsBuf(pObj) )
+ pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask;
+ else
+ pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask | pEvals[Ivy_ObjFanin1(pObj)->TravId].Mask;
}
- // the case of one common node
- if ( nArgsNew == nArgs + 1 )
+
+ // set the internal entries
+ Vec_PtrForEachEntry( vCone, pObj, i )
{
- assert( pEvaBest - pEvals == nArgs );
- k = 0;
- for ( i = 0; i < nArgs; i++ )
- if ( i != (int)pEvaBest->Fan0 && i != (int)pEvaBest->Fan1 )
- pArgs[k++] = pArgs[i];
- pArgs[k++] = pArgs[nArgs];
- assert( k == nArgs - 1 );
- nArgs = k;
- Ivy_MultiSort( pArgs, nArgs );
- return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+ if ( i == Vec_PtrSize(vCone) - 1 )
+ break;
+ // skip buffers
+ if ( Ivy_ObjIsBuf(pObj) )
+ continue;
+ // skip nodes without external fanout
+ if ( Ivy_ObjRefs(pObj) == 0 )
+ continue;
+ assert( !Ivy_IsComplement(pObj) );
+ pEval = pEvals + nEvals;
+ pEval->pArg = pObj;
+ pEval->Mask = pEvals[pObj->TravId].Mask;
+ pEval->Weight = Extra_WordCountOnes(pEval->Mask);
+ // mark the node
+ pObj->TravId = nEvals;
+ nEvals++;
}
- // the case when there is a node that covers everything
- if ( (int)pEvaBest->Mask == ((1 << nArgs) - 1) )
- return Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type );
- // evaluate node pairs
- nEvals = nArgsNew;
- for ( i = 1; i < nArgsNew; i++ )
+ // find the available nodes
+ nEvalsOld = nEvals;
+ for ( i = 1; i < nEvals; i++ )
for ( k = 0; k < i; k++ )
{
- pEva = pEvals + nEvals;
- pEva->Mask = pEvals[k].Mask | pEvals[i].Mask;
- pEva->Weight = NumBits[pEva->Mask];
- pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask];
- pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level);
- pEva->Fan0 = k;
- pEva->Fan1 = i;
- // compare
- if ( pEvaBest->Weight < pEva->Weight ||
- pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost ||
- pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level )
- pEvaBest = pEva;
+ pFan0 = pEvals + i;
+ pFan1 = pEvals + k;
+ pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE));
+ // skip nodes in the cone
+ if ( pTemp == NULL || pTemp->fMarkB )
+ continue;
+ // skip the leaves
+ for ( x = 0; x < nLeaves; x++ )
+ if ( pTemp == Ivy_Regular(vLeaves->pArray[x]) )
+ break;
+ if ( x < nLeaves )
+ continue;
+ pEval = pEvals + nEvals;
+ pEval->pArg = pTemp;
+ pEval->Mask = pFan0->Mask | pFan1->Mask;
+ pEval->Weight = (pFan0->Mask & pFan1->Mask) ? Extra_WordCountOnes(pEval->Mask) : pFan0->Weight + pFan1->Weight;
// save the argument
+ pObj->TravId = nEvals;
nEvals++;
+ // quit if the number of entries exceeded the limit
+ if ( nEvals == IVY_EVAL_LIMIT )
+ goto Outside;
+ // quit if we found an acceptable implementation
+ if ( pEval->Mask == uMaskAll )
+ goto Outside;
}
- assert( pEvaBest - pEvals >= nArgsNew );
-
-// printf( "Used (%d, %d).\n", pEvaBest->Fan0, pEvaBest->Fan1 );
-
- // get the best implementation
- pTemp = Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type );
-
- // collect those not covered by EvaBest
- k = 0;
- for ( i = 0; i < nArgs; i++ )
- if ( (pEvaBest->Mask & (1 << i)) == 0 )
- pArgs[k++] = pArgs[i];
- pArgs[k++] = pTemp;
- assert( k == nArgs - (int)pEvaBest->Weight + 1 );
- nArgs = k;
- Ivy_MultiSort( pArgs, nArgs );
- return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
-}
-
-/**Function*************************************************************
-
- Synopsis [Implements multi-input AND/EXOR operation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
-{
- Ivy_Obj_t * pNode0, * pNode1;
- if ( iNum < nArgs )
- return pArgs[iNum];
- pNode0 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan0, pArgs, nArgs, Type );
- pNode1 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan1, pArgs, nArgs, Type );
- return Ivy_Oper( pNode0, pNode1, Type );
-}
-
-/**Function*************************************************************
-
- Synopsis [Selection-sorts the nodes in the decreasing over of level.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs )
-{
- Ivy_Obj_t * pTemp;
- int i, j, iBest;
+Outside:
- for ( i = 0; i < nArgs-1; i++ )
- {
- iBest = i;
- for ( j = i+1; j < nArgs; j++ )
- if ( Ivy_Regular(pArgs[j])->Level > Ivy_Regular(pArgs[iBest])->Level )
- iBest = j;
- pTemp = pArgs[i];
- pArgs[i] = pArgs[iBest];
- pArgs[iBest] = pTemp;
- }
+// Ivy_MultiPrint( pEvals, nLeaves, nEvals );
+ if ( !Ivy_MultiCover( pEvals, nLeaves, nEvals, nLimit, vSols ) )
+ return 0;
+ assert( Vec_PtrSize( vSols ) > 0 );
+ return 1;
}
/**Function*************************************************************
- Synopsis [Inserts a new node in the order by levels.]
+ Synopsis [Computes how many uncovered ones this one covers.]
Description []
@@ -261,32 +166,28 @@ void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs )
SeeAlso []
***********************************************************************/
-int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode )
+void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals )
{
- Ivy_Obj_t * pNode1, * pNode2;
- int i;
- // try to find the node in the array
- for ( i = 0; i < nArgs; i++ )
- if ( pArray[i] == pNode )
- return nArgs;
- // put the node last
- pArray[nArgs++] = pNode;
- // find the place to put the new node
- for ( i = nArgs-1; i > 0; i-- )
+ Ivy_Eva_t * pEval;
+ int i, k;
+ for ( i = nLeaves; i < nEvals; i++ )
{
- pNode1 = pArray[i ];
- pNode2 = pArray[i-1];
- if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level )
- break;
- pArray[i ] = pNode2;
- pArray[i-1] = pNode1;
+ pEval = pEvals + i;
+ printf( "%2d (id = %5d) : |", i-nLeaves, Ivy_ObjId(pEval->pArg) );
+ for ( k = 0; k < nLeaves; k++ )
+ {
+ if ( pEval->Mask & (1 << k) )
+ printf( "+" );
+ else
+ printf( " " );
+ }
+ printf( "| Lev = %d.\n", Ivy_ObjLevel(pEval->pArg) );
}
- return nArgs;
}
/**Function*************************************************************
- Synopsis [Balances the array recursively.]
+ Synopsis [Computes how many uncovered ones this one covers.]
Description []
@@ -295,129 +196,102 @@ int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t *
SeeAlso []
***********************************************************************/
-Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+static inline int Ivy_MultiWeight( unsigned uMask, int nMaskOnes, unsigned uFound )
{
- Ivy_Obj_t * pNodeNew;
- // consider the case of one argument
- assert( nArgs > 0 );
- if ( nArgs == 1 )
- return pArgs[0];
- // consider the case of two arguments
- if ( nArgs == 2 )
- return Ivy_Oper( pArgs[0], pArgs[1], Type );
- // get the last two nodes
- pNodeNew = Ivy_Oper( pArgs[nArgs-1], pArgs[nArgs-2], Type );
- // add the new node
- nArgs = Ivy_MultiPushUniqueOrderByLevel( pArgs, nArgs - 2, pNodeNew );
- return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+ assert( uMask & ~uFound );
+ if ( (uMask & uFound) == 0 )
+ return nMaskOnes;
+ return Extra_WordCountOnes( uMask & ~uFound );
}
/**Function*************************************************************
- Synopsis [Implements multi-input AND/EXOR operation.]
+ Synopsis [Finds the cover.]
- Description []
+ Description [Returns 1 if the cover is found.]
SideEffects []
SeeAlso []
***********************************************************************/
-Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols )
{
- Ivy_Obj_t * pTemp;
- int i, k;
- int nArgsOld = nArgs;
- for ( i = 0; i < nArgs; i++ )
- printf( "%d[%d] ", i, Ivy_Regular(pArgs[i])->Level );
- for ( i = 1; i < nArgs; i++ )
- for ( k = 0; k < i; k++ )
+ int fVerbose = 0;
+ Ivy_Eva_t * pEval, * pEvalBest;
+ unsigned uMaskAll, uFound, uTemp;
+ int i, k, BestK, WeightBest, WeightCur, LevelBest, LevelCur;
+ uMaskAll = (nLeaves == 32)? (~(unsigned)0) : ((1 << nLeaves) - 1);
+ uFound = 0;
+ // solve the covering problem
+ if ( fVerbose )
+ printf( "Solution: " );
+ Vec_PtrClear( vSols );
+ for ( i = 0; i < nLimit; i++ )
+ {
+ BestK = -1;
+ for ( k = nEvals - 1; k >= 0; k-- )
{
- pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE));
- if ( pTemp != NULL )
+ pEval = pEvals + k;
+ if ( (pEval->Mask & ~uFound) == 0 )
+ continue;
+ if ( BestK == -1 )
{
- printf( "%d[%d]=(%d,%d) ", nArgs, Ivy_Regular(pTemp)->Level, k, i );
- pArgs[nArgs++] = pTemp;
+ BestK = k;
+ pEvalBest = pEval;
+ WeightBest = Ivy_MultiWeight( pEvalBest->Mask, pEvalBest->Weight, uFound );
+ LevelBest = Ivy_ObjLevel( Ivy_Regular(pEvalBest->pArg) );
+ continue;
+ }
+ // compare BestK and the new one (k)
+ WeightCur = Ivy_MultiWeight( pEval->Mask, pEval->Weight, uFound );
+ LevelCur = Ivy_ObjLevel( Ivy_Regular(pEval->pArg) );
+ if ( WeightBest < WeightCur ||
+ (WeightBest == WeightCur && LevelBest > LevelCur) )
+ {
+ BestK = k;
+ pEvalBest = pEval;
+ WeightBest = WeightCur;
+ LevelBest = LevelCur;
}
}
- printf( " ((%d/%d)) ", nArgsOld, nArgs-nArgsOld );
- return NULL;
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis [Old code.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
-{
- Ivy_Obj_t * pArgsRef[5], * pTemp;
- int i, k, m, nArgsNew, Counter = 0;
-
-
-//Ivy_MultiEval( pArgs, nArgs, Type ); printf( "\n" );
-
-
- assert( Type == IVY_AND || Type == IVY_EXOR );
- assert( nArgs > 0 );
- if ( nArgs == 1 )
- return pArgs[0];
-
- // find the nodes with more than one fanout
- nArgsNew = 0;
- for ( i = 0; i < nArgs; i++ )
- if ( Ivy_ObjRefs( Ivy_Regular(pArgs[i]) ) > 0 )
- pArgsRef[nArgsNew++] = pArgs[i];
-
- // go through pairs
- if ( nArgsNew >= 2 )
- for ( i = 0; i < nArgsNew; i++ )
- for ( k = i + 1; k < nArgsNew; k++ )
- if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) )
- Counter++;
-// printf( "%d", Counter );
-
- // go through pairs
- if ( nArgsNew >= 2 )
- for ( i = 0; i < nArgsNew; i++ )
- for ( k = i + 1; k < nArgsNew; k++ )
- if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) )
+ assert( BestK != -1 );
+ // if the cost is only 1, take the leaf
+ if ( WeightBest == 1 && BestK >= nLeaves )
{
- nArgsNew = 0;
- for ( m = 0; m < nArgs; m++ )
- if ( pArgs[m] != pArgsRef[i] && pArgs[m] != pArgsRef[k] )
- pArgs[nArgsNew++] = pArgs[m];
- pArgs[nArgsNew++] = pTemp;
- assert( nArgsNew == nArgs - 1 );
- return Ivy_Multi1( pArgs, nArgsNew, Type );
+ uTemp = (pEvalBest->Mask & ~uFound);
+ for ( k = 0; k < nLeaves; k++ )
+ if ( uTemp & (1 << k) )
+ break;
+ assert( k < nLeaves );
+ BestK = k;
+ pEvalBest = pEvals + BestK;
}
- return Ivy_Multi_rec( pArgs, nArgs, Type );
-}
-
-/**Function*************************************************************
-
- Synopsis [Old code.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Multi2( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
-{
- assert( Type == IVY_AND || Type == IVY_EXOR );
- assert( nArgs > 0 );
- return Ivy_Multi_rec( pArgs, nArgs, Type );
+ if ( fVerbose )
+ {
+ if ( BestK < nLeaves )
+ printf( "L(%d) ", BestK );
+ else
+ printf( "%d ", BestK - nLeaves );
+ }
+ // update the found set
+ Vec_PtrPush( vSols, pEvalBest->pArg );
+ uFound |= pEvalBest->Mask;
+ if ( uFound == uMaskAll )
+ break;
+ }
+ if ( uFound == uMaskAll )
+ {
+ if ( fVerbose )
+ printf( " Found \n\n" );
+ return 1;
+ }
+ else
+ {
+ if ( fVerbose )
+ printf( " Not found \n\n" );
+ return 0;
+ }
}
////////////////////////////////////////////////////////////////////////