diff --git a/src/aig/gia/giaLutCas.c b/src/aig/gia/giaLutCas.c new file mode 100644 index 000000000..1d1721ab0 --- /dev/null +++ b/src/aig/gia/giaLutCas.c @@ -0,0 +1,149 @@ +/**CFile**************************************************************** + + FileName [giaLutCas.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [LUT cascade generator.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaLutCas.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "sat/cnf/cnf.h" +#include "misc/util/utilTruth.h" +#include "sat/cadical/cadicalSolver.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_LutCasSort( char * pStr, int iStart, int nChars ) +{ + int i, j; + for ( i = iStart; i < iStart + nChars - 1; i++ ) + for ( j = i + 1; j < iStart + nChars; j++ ) + if ( pStr[i] > pStr[j] ) + ABC_SWAP( char, pStr[i], pStr[j] ); +} +char * Gia_LutCasPerm( int nVars, int nLuts, int LutSize ) +{ + assert( nVars <= 26 && nLuts <= 100 ); + int nStrLen = nLuts * LutSize; + char * pRes = ABC_CALLOC( char, nStrLen+1 ); + int i, j, iVar, pPerm[26], nVarCount[100] = {0}; + // create a random permutation + for ( i = 0; i < nVars; i++ ) + pPerm[i] = i; + for ( i = nVars - 1; i > 0; i-- ) { + j = rand() % (i + 1); + ABC_SWAP( int, pPerm[i], pPerm[j] ); + } + // assign the first variable + for ( i = 0; i < nLuts; i++ ) { + pRes[i * LutSize] = i ? '_' : 'a' + pPerm[0]; + nVarCount[i] = 1; + } + // First pass: distribute each variable (starting from the second in permutation) to at least one LUT + for ( i = 1; i < nVars; i++ ) { + // Find a LUT with space that doesn't have this variable + int Tries = 0, iLut = rand() % nLuts; + while ( nVarCount[iLut] >= LutSize && Tries++ < nLuts ) + iLut = (iLut + 1) % nLuts; + // the variables are unique - no need to check this + pRes[iLut * LutSize + nVarCount[iLut]] = 'a' + pPerm[i]; + nVarCount[iLut]++; + } + // Second pass: fill remaining slots with random variables (cycling through permutation) + for ( i = 0; i < nLuts; i++ ) { + while ( nVarCount[i] < LutSize ) { + iVar = pPerm[rand() % nVars]; + // Check this LUT already has this variable + for ( j = 0; j < nVarCount[i]; j++ ) + if ( pRes[i * LutSize + j] == 'a' + iVar ) + break; + if ( j == nVarCount[i] ) { // does not have + pRes[i * LutSize + nVarCount[i]] = 'a' + iVar; + nVarCount[i]++; + } + } + } + // Sort inputs within each LUT (skip '_' for non-first LUTs) + Gia_LutCasSort( pRes, 0, LutSize ); + for ( i = 1; i < nLuts; i++ ) + Gia_LutCasSort( pRes + i * LutSize, 1, LutSize-1 ); + return pRes; +} +int Gia_ManLutCasGen_rec( Gia_Man_t * pNew, Vec_Int_t * vCtrls, int iCtrl, Vec_Int_t * vDatas, int Shift ) +{ + if ( iCtrl-- == 0 ) + return Vec_IntEntry( vDatas, Shift ); + int iLit0 = Gia_ManLutCasGen_rec( pNew, vCtrls, iCtrl, vDatas, Shift ); + int iLit1 = Gia_ManLutCasGen_rec( pNew, vCtrls, iCtrl, vDatas, Shift + (1<pName = Abc_UtilStrsav( pPerm ); + Vec_Int_t * vDatas = Vec_IntAlloc( nParams ); + Vec_Int_t * vCtrls = Vec_IntAlloc( nVars ); + for ( int i = 0; i < nParams; i++ ) + Vec_IntPush( vDatas, Gia_ManAppendCi(pNew) ); + for ( int i = 0; i < nVars; i++ ) + Vec_IntPush( vCtrls, Gia_ManAppendCi(pNew) ); + Vec_Int_t * vLits = Vec_IntStart( LutSize ); + Vec_IntWriteEntry( vLits, 0, Vec_IntEntry(vCtrls, (int)(pPerm[0]-'a')) ); + char * pCur = pPerm; + for ( int i = 0; i < nLuts; i++ ) { + pCur++; + for ( int k = 1; k < LutSize; k++ ) + Vec_IntWriteEntry( vLits, k, Vec_IntEntry(vCtrls, (int)(*pCur++ - 'a')) ); + Vec_IntWriteEntry( vLits, 0, Gia_ManLutCasGen_rec(pNew, vLits, LutSize, vDatas, i * (1 << LutSize)) ); + } + Gia_ManAppendCo( pNew, Vec_IntEntry(vLits, 0) ); + Vec_IntFree( vDatas ); + Vec_IntFree( vCtrls ); + Vec_IntFree( vLits ); + ABC_FREE( pPerm ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index dcb30e90a..4aad1385b 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -50,6 +50,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaJf.c \ src/aig/gia/giaKf.c \ src/aig/gia/giaLf.c \ + src/aig/gia/giaLutCas.c \ src/aig/gia/giaMf.c \ src/aig/gia/giaMan.c \ src/aig/gia/giaMem.c \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 55e2c2c7e..e75ceadc2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -580,6 +580,7 @@ static int Abc_CommandAbc9FFTest ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Qbf ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9QVar ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenQbf ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GenLutCas ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9HomoQbf ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatFx ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatClp ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1402,6 +1403,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&qbf", Abc_CommandAbc9Qbf, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&qvar", Abc_CommandAbc9QVar, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&genqbf", Abc_CommandAbc9GenQbf, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&genlutcas", Abc_CommandAbc9GenLutCas, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&homoqbf", Abc_CommandAbc9HomoQbf, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&satfx", Abc_CommandAbc9SatFx, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&satclp", Abc_CommandAbc9SatClp, 0 ); @@ -51659,6 +51661,126 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9GenLutCas( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManLutCasGen( int nVars, int nLuts, int LutSize, int Seed, int fVerbose ); + int nVars = 8; + int nLuts = 2; + int LutSize = 6; + int Seed = 0; + int fVerbose = 0; + int c; + Gia_Man_t * pTemp; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NMKSvh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nVars < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + nLuts = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLuts < 0 ) + goto usage; + break; + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + LutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( LutSize < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + Seed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Seed < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( nVars <= LutSize ) + { + Abc_Print( -1, "The number of inputs (%d) should be more than LUT size (%d).\n", nVars, LutSize ); + return 1; + } + if ( nVars > 100 ) + { + Abc_Print( -1, "The number of inputs (%d) should be less than 100.\n", nVars ); + return 1; + } + if ( nLuts < 2 || nLuts > 100 ) + { + Abc_Print( -1, "The LUT count (%d) should be morein the range [2;100].\n", nLuts ); + return 1; + } + if ( LutSize < 2 || LutSize > 12 ) + { + Abc_Print( -1, "The LUT size (%d) should be in the range [2;12].\n", LutSize ); + return 1; + } + if ( nVars > (nLuts-1)*(LutSize-1) + LutSize ) + { + Abc_Print( -1, "Function with %d variables is too large for a cascade composed of %d connected %d-LUTs.\n", nVars, nLuts, LutSize ); + return 1; + } + pTemp = Gia_ManLutCasGen( nVars, nLuts, LutSize, Seed, fVerbose ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &genlutcas[-NMKS num] [-vh]\n" ); + Abc_Print( -2, "\t generates single-rail LUT cascade\n" ); + Abc_Print( -2, "\t-N num : the number of primary inputs [default = %d]\n", nVars ); + Abc_Print( -2, "\t-M num : the number of LUTs [default = %d]\n", nLuts ); + Abc_Print( -2, "\t-K num : the LUT size [default = %d]\n", LutSize ); + Abc_Print( -2, "\t-S num : the random seed [default = %d]\n", Seed ); + Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/sat/cadical/cadical_restart.cpp b/src/sat/cadical/cadical_restart.cpp index 1c6dc44c8..d309d5f10 100644 --- a/src/sat/cadical/cadical_restart.cpp +++ b/src/sat/cadical/cadical_restart.cpp @@ -35,12 +35,12 @@ bool Internal::stabilizing () { STOP (stable); else STOP (unstable); - const int64_t delta_conflicts = - stats.conflicts - last.stabilize.conflicts; + //const int64_t delta_conflicts = + // stats.conflicts - last.stabilize.conflicts; const int64_t delta_ticks = stats.ticks.search[stable] - last.stabilize.ticks; - const char *current_mode = stable ? "stable" : "unstable"; - const char *next_mode = stable ? "unstable" : "stable"; + //const char *current_mode = stable ? "stable" : "unstable"; + //const char *next_mode = stable ? "unstable" : "stable"; PHASE ("stabilizing", stats.stabphases, "reached %s stabilization limit %" PRId64 " after %" PRId64 " conflicts and %" PRId64 " ticks at %" PRId64