320 unsigned pVars[100] = {0};
321 unsigned pMints[100] = {0};
322 unsigned pFuncs[100] = {0};
324 int FuncDone[100] = {0}, nFuncDone = 0;
325 int GateCount[100] = {0};
326 int i, k, n, a, b, v;
328 Vec_Int_t * vGates = Vec_IntAlloc( 100000 );
329 Vec_Int_t * vTruths = Vec_IntAlloc( 100000 );
335 Abc_GetSecond( &nVars, &nMints, &nFuncs, pVars, pMints, pFuncs );
339 assert( nMints == 16 || nMints == 32 );
343 for ( k = 0; k < nVars; k++ )
346 Abc_DataXorBit( pHash, pVars[k] );
347 Vec_IntPush( vTruths, pVars[k] );
348 Vec_IntPush( vGates, -1 );
349 Vec_IntPush( vGates, -1 );
354 GateCount[1] = nVars;
355 assert( Vec_IntSize(vTruths) == nVars );
356 for ( n = 0; n < nDecMax && nFuncDone < nFuncs; n++ )
358 for ( a = 0; a <= n; a++ )
359 for ( b = a; b <= n; b++ )
362 printf(
"Trying %d + %d + 1 = %d\n", a, b, n+1 );
363 for ( i = GateCount[a]; i < GateCount[a+1]; i++ )
364 for ( k = GateCount[b]; k < GateCount[b+1]; k++ )
367 Truth = Vec_IntEntry(vTruths, i) & Vec_IntEntry(vTruths, k);
369 if ( !Abc_DataHasBit(pHash, Truth) )
372 Abc_DataXorBit( pHash, Truth );
373 Vec_IntPush( vTruths, Truth );
374 Vec_IntPush( vGates, i );
375 Vec_IntPush( vGates, k );
377 for ( v = 0; v < nFuncs; v++ )
378 if ( !FuncDone[v] && Truth == pFuncs[v] )
380 printf(
"Found function %d with %d gates: ", v, n+1 );
386 Truth = Vec_IntEntry(vTruths, i) | Vec_IntEntry(vTruths, k);
388 if ( !Abc_DataHasBit(pHash, Truth) )
391 Abc_DataXorBit( pHash, Truth );
392 Vec_IntPush( vTruths, Truth );
393 Vec_IntPush( vGates, k );
394 Vec_IntPush( vGates, i );
396 for ( v = 0; v < nFuncs; v++ )
397 if ( !FuncDone[v] && Truth == pFuncs[v] )
399 printf(
"Found function %d with %d gates: ", v, n+1 );
407 GateCount[n+2] = Vec_IntSize(vTruths);
408 printf(
"Finished %d gates. Truths = %10d. ", n+1, Vec_IntSize(vTruths) );
409 Abc_PrintTime( 1,
"Time", Abc_Clock() - clk );
413 Vec_IntFree( vGates );
414 Vec_IntFree( vTruths );
569 if (
p->nNodes ==
p->nNodeMax )
573 Abc_EnumPrintOne(
p );
578 int i, k, c, cLim = 4 +
p->fUseXor, n =
p->nNodes;
579 int nRefedFans =
p->nNodeMax - n + 1 -
p->nTops;
580 int high0 = fNew ? iNode1st :
p->pFans1[n-1];
581 int high1 = fNew ? n : iNode1st;
582 int low0 = fNew ? 0 :
p->pFans0[n-1];
583 int c0 = fNew ? 0 :
p->Polar[n-1];
584 int Level =
p->pLevel[high0];
585 assert(
p->nTops > 0 &&
p->nTops <=
p->nNodeMax - n + 1 );
587 for ( k = high0; k < high1; k++ )
589 if ( nRefedFans == 0 &&
p->pRefs[k] > 0 )
591 if (
p->pRefs[k] > 0 )
593 assert( nRefedFans >= 0 );
595 for ( i = (k == high0) ? low0 : 0; i < k; i++ )
597 if ( nRefedFans == 0 &&
p->pRefs[i] > 0 )
599 if ( Level == 0 &&
p->pRefs[i] == 0 &&
p->pRefs[k] == 0 && (i+1 != k || (i > 0 &&
p->pRefs[i-1] == 0)) )
601 if (
p->pLevel[k] == 0 &&
p->pRefs[k] == 0 &&
p->pRefs[i] != 0 && k > 0 &&
p->pRefs[k-1] == 0 )
606 for ( c = (k == high0 && i == low0 && !fNew) ? c0 + 1 : 0; c < cLim; c++ )
608 if (
p->pLevel[i] == 0 &&
p->pRefs[i] == 0 && (c & 1) == 1 )
610 if (
p->pLevel[k] == 0 &&
p->pRefs[k] == 0 && (c & 2) == 2 )
617 p->fCompl0[n] = c & 1;
618 p->fCompl1[n] = (c >> 1) & 1;
621 p->pTruths[n] =
p->pTruths[i] ^
p->pTruths[k];
623 p->pTruths[n] = ((c & 1) ?
~p->pTruths[i] :
p->pTruths[i]) & ((c & 2) ? ~
p->pTruths[k] :
p->pTruths[k]);
624 if ( Abc_EnumerateFilter(
p) )
627 assert( Level == Abc_MaxInt(
p->pLevel[i],
p->pLevel[k]) );
628 p->pLevel[n] = Level + 1;
629 Abc_EnumRefNode(
p, n );
631 Abc_EnumDerefNode(
p, n );
635 if (
p->pRefs[k] > 0 )