diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaQbf.c | 186 | ||||
-rw-r--r-- | src/base/abci/abc.c | 95 |
2 files changed, 275 insertions, 6 deletions
diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index f32db0a4..1539fa29 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -184,6 +184,184 @@ Gia_Man_t * Gia_GenQbfMiter( Gia_Man_t * p, int nFrames, int nLutNum, int nLutSi return pNew; } + +/**Function************************************************************* + + Synopsis [Generate miter for the encoding problem.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_Gen2CreateMux_rec( Gia_Man_t * pNew, int * pCtrl, int nCtrl, Vec_Int_t * vData, int Shift ) +{ + int iLit0, iLit1; + if ( nCtrl == 0 ) + return Vec_IntEntry( vData, Shift ); + iLit0 = Gia_Gen2CreateMux_rec( pNew, pCtrl, nCtrl-1, vData, Shift ); + iLit1 = Gia_Gen2CreateMux_rec( pNew, pCtrl, nCtrl-1, vData, Shift + (1<<(nCtrl-1)) ); + return Gia_ManHashMux( pNew, pCtrl[nCtrl-1], iLit1, iLit0 ); +} +Vec_Int_t * Gia_Gen2CreateMuxes( Gia_Man_t * pNew, int nLutSize, int nLutNum, Vec_Int_t * vPLits, Vec_Int_t * vXLits ) +{ + Vec_Int_t * vLits = Vec_IntAlloc( nLutNum ); + int i, iMux; + // add MUXes for each group of flops + assert( Vec_IntSize(vPLits) == nLutNum * (1 << nLutSize) ); + assert( Vec_IntSize(vXLits) == nLutSize ); + for ( i = 0; i < nLutNum; i++ ) + { + iMux = Gia_Gen2CreateMux_rec( pNew, Vec_IntArray(vXLits), nLutSize, vPLits, i * (1 << nLutSize) ); + Vec_IntPush( vLits, iMux ); + } + return vLits; +} +Gia_Man_t * Gia_Gen2CreateMiter( int nLutSize, int nLutNum ) +{ + // |<-- PVars(0)-->|...|<-- PVars(nLutNum-1)-->|<-- XVars-->|<-- YVars-->| + Vec_Int_t * vPLits = Vec_IntAlloc( nLutNum * (1 << nLutSize) ); + Vec_Int_t * vXLits = Vec_IntAlloc( nLutSize ); + Vec_Int_t * vYLits = Vec_IntAlloc( nLutSize ); + Vec_Int_t * vXYLits = Vec_IntAlloc( nLutSize ); + Vec_Int_t * vXRes, * vYRes, * vXYRes; + Vec_Int_t * vXYRes2 = Vec_IntAlloc( 2 * nLutNum ); + Gia_Man_t * pTemp, * pNew = Gia_ManStart( 1000 ); int i, k, v, Cond, Res; + pNew->pName = Abc_UtilStrsav( "homoqbf" ); + Gia_ManHashAlloc( pNew ); + for ( i = 0; i < nLutNum * (1 << nLutSize); i++ ) + Vec_IntPush( vPLits, Gia_ManAppendCi(pNew) ); + for ( i = 0; i < nLutSize; i++ ) + Vec_IntPush( vXLits, Gia_ManAppendCi(pNew) ); + for ( i = 0; i < nLutSize; i++ ) + Vec_IntPush( vYLits, Gia_ManAppendCi(pNew) ); + for ( i = 0; i < nLutSize; i++ ) + Vec_IntPush( vXYLits, Abc_LitNot(Gia_ManHashAnd(pNew, Vec_IntEntry(vXLits, i), Vec_IntEntry(vYLits, i))) ); + vXRes = Gia_Gen2CreateMuxes( pNew, nLutSize, nLutNum, vPLits, vXLits ); + vYRes = Gia_Gen2CreateMuxes( pNew, nLutSize, nLutNum, vPLits, vYLits ); + vXYRes = Gia_Gen2CreateMuxes( pNew, nLutSize, nLutNum, vPLits, vXYLits ); + for ( i = 0; i < nLutNum; i++ ) + { + Vec_IntPush( vXYRes2, Vec_IntEntry(vXYRes, i) ); + Vec_IntPush( vXYRes2, Abc_LitNot(Gia_ManHashAnd(pNew, Vec_IntEntry(vXRes, i), Vec_IntEntry(vYRes, i))) ); + } + Res = Gia_ManHashDualMiter( pNew, vXYRes2 ); + // uniqueness of codes + for ( i = 0; i < (1 << nLutSize); i++ ) + { + Vec_Int_t * vCondA = Vec_IntAlloc( nLutNum ); + Vec_Int_t * vCondB = Vec_IntAlloc( nLutNum ); + for ( v = 0; v < nLutNum; v++ ) + Vec_IntPush( vCondA, Vec_IntEntry(vPLits, v*(1 << nLutSize)+i) ); + for ( k = i+1; k < (1 << nLutSize); k++ ) + { + Vec_IntClear( vCondB ); + for ( v = 0; v < nLutNum; v++ ) + { + Vec_IntPush( vCondB, Vec_IntEntry(vCondA, v) ); + Vec_IntPush( vCondB, Vec_IntEntry(vPLits, v*(1 << nLutSize)+k) ); + } + Cond = Gia_ManHashDualMiter( pNew, vCondB ); + Res = Gia_ManHashOr( pNew, Res, Abc_LitNot(Cond) ); + } + Vec_IntFree( vCondA ); + Vec_IntFree( vCondB ); + } + Gia_ManAppendCo( pNew, Abc_LitNot(Res) ); + Gia_ManHashStop( pNew ); + Vec_IntFree( vPLits ); + Vec_IntFree( vXLits ); + Vec_IntFree( vYLits ); + Vec_IntFree( vXYLits ); + Vec_IntFree( vXRes ); + Vec_IntFree( vYRes ); + Vec_IntFree( vXYRes ); + Vec_IntFree( vXYRes2 ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + printf( "Generated QBF miter with %d parameters, %d functional variables, and %d AIG nodes.\n", + nLutNum * (1 << nLutSize), 2*nLutNum, Gia_ManAndNum(pNew) ); + return pNew; +} +int Gia_Gen2CodeOne( int nLutSize, int nLutNum, Vec_Int_t * vCode, int x ) +{ + int k, Code = 0; + for ( k = 0; k < nLutNum; k++ ) + if ( Vec_IntEntry(vCode, k*(1 << nLutSize)+x) ) + Code |= (1 << k); + return Code; +} +void Gia_Gen2CodePrint( int nLutSize, int nLutNum, Vec_Int_t * vCode ) +{ + // |<-- PVars(0)-->|...|<-- PVars(nLutNum-1)-->| + int i, n, nPairs = 16; + printf( "%d-input %d-output code table:\n", nLutSize, nLutNum ); + for ( i = 0; i < (1 << nLutSize); i++ ) + { + int Code = Gia_Gen2CodeOne( nLutSize, nLutNum, vCode, i ); + printf( "%3d ", i ); + Extra_PrintBinary( stdout, &i, nLutSize ); + printf( " --> " ); + printf( "%3d ", Code ); + Extra_PrintBinary( stdout, &Code, nLutNum ); + printf( "\n" ); + } + // create several different pairs + srand( time(NULL) ); + printf( "Simulation of the encoding with %d random pairs:\n", nPairs ); + for ( n = 0; n < nPairs; n++ ) + { + unsigned MaskIn = Abc_InfoMask( nLutSize ); + unsigned MaskOut = Abc_InfoMask( nLutNum ); + int CodeX, CodeY, CodeXY, CodeXCodeY; + int NumX = 0, NumY = 0, NumXY; + while ( NumX == NumY ) + { + NumX = rand() % (1 << nLutSize); + NumY = rand() % (1 << nLutSize); + NumXY = MaskIn & ~(NumX & NumY); + } + CodeX = Gia_Gen2CodeOne( nLutSize, nLutNum, vCode, NumX ); + CodeY = Gia_Gen2CodeOne( nLutSize, nLutNum, vCode, NumY ); + CodeXY = Gia_Gen2CodeOne( nLutSize, nLutNum, vCode, NumXY ); + CodeXCodeY = MaskOut & ~(CodeX & CodeY); + + printf( "%2d :", n ); + printf( " x =%3d ", NumX ); + Extra_PrintBinary( stdout, &NumX, nLutSize ); + printf( " y =%3d ", NumY ); + Extra_PrintBinary( stdout, &NumY, nLutSize ); + printf( " nand =%3d ", NumXY ); + Extra_PrintBinary( stdout, &NumXY, nLutSize ); + printf( " " ); + + printf( " c(x) =%3d ", CodeX ); + Extra_PrintBinary( stdout, &CodeX, nLutNum ); + printf( " c(y) =%3d ", CodeY ); + Extra_PrintBinary( stdout, &CodeY, nLutNum ); + printf( " c(nand) =%3d ", CodeXY ); + Extra_PrintBinary( stdout, &CodeXY, nLutNum ); + printf( " nand(c(x), c(y)) =%3d ", CodeXCodeY ); + Extra_PrintBinary( stdout, &CodeXCodeY, nLutNum ); + printf( " " ); + + printf( "%s", CodeXCodeY == CodeXY ? "yes" : "no" ); + printf( "\n" ); + } +} +void Gia_Gen2CodeTest() +{ + int i, nLutSize = 1, nLutNum = 2; + Vec_Int_t * vCode = Vec_IntAlloc( (1 << nLutSize) * nLutNum ); + srand( time(NULL) ); + for ( i = 0; i < (1 << nLutSize) * nLutNum; i++ ) + Vec_IntPush( vCode, rand() & 1 ); + Gia_Gen2CodePrint( nLutSize, nLutNum, vCode ); + Vec_IntFree( vCode ); +} + /**Function************************************************************* Synopsis [Naive way to enumerate SAT assignments.] @@ -632,7 +810,7 @@ void Gia_QbfLearnConstraint( Qbf_Man_t * p, Vec_Int_t * vValues ) SeeAlso [] ***********************************************************************/ -int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fGlucose, int fVerbose ) +int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fVerbose ) { Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fGlucose, fVerbose ); Gia_Man_t * pCof; @@ -679,6 +857,12 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i assert( Vec_IntSize(p->vValues) == nPars ); Vec_IntPrintBinary( p->vValues ); printf( " Statistics: 0=%d 1=%d\n", nZeros, Vec_IntSize(p->vValues) - nZeros ); + if ( nEncVars ) + { + int nBits = Vec_IntSize(p->vValues)/(1 << nEncVars); + assert( Vec_IntSize(p->vValues) == (1 << nEncVars) * nBits ); + Gia_Gen2CodePrint( nEncVars, nBits, p->vValues ); + } } if ( RetValue == -1 && nTimeOut && (Abc_Clock() - p->clkStart)/CLOCKS_PER_SEC >= nTimeOut ) printf( "The problem timed out after %d sec. ", nTimeOut ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2a664cd0..4498f390 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -519,6 +519,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_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 ); static int Abc_CommandAbc9Inse ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1235,6 +1236,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", "&homoqbf", Abc_CommandAbc9HomoQbf, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&satfx", Abc_CommandAbc9SatFx, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&satclp", Abc_CommandAbc9SatClp, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&inse", Abc_CommandAbc9Inse, 0 ); @@ -13673,6 +13675,7 @@ int Abc_CommandTestColor( Abc_Frame_t * pAbc, int argc, char ** argv ) ***********************************************************************/ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern void Gia_Gen2CodeTest(); extern void Dau_NetworkEnumTest(); //Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int nCutMax = 1; @@ -13886,7 +13889,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) //Dau_NetworkEnumTest(); //Extra_SimulationTest( nDivMax, nNumOnes, fNewOrder ); //Mnist_ExperimentWithScaling( nDecMax ); - //Extra_ReadForestTest(); + Gia_Gen2CodeTest(); return 0; usage: Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" ); @@ -43715,16 +43718,17 @@ usage: int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ); - extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fGlucose, int fVerbose ); + extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fVerbose ); int c, nPars = -1; int nIterLimit = 0; int nConfLimit = 0; int nTimeOut = 0; + int nEncVars = 0; int fDumpCnf = 0; int fGlucose = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PICTdgvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PICTKdgvh" ) ) != EOF ) { switch ( c ) { @@ -43772,6 +43776,17 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nTimeOut < 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; + } + nEncVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nEncVars < 0 ) + goto usage; + break; case 'd': fDumpCnf ^= 1; break; @@ -43810,16 +43825,17 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fDumpCnf ) Gia_QbfDumpFile( pAbc->pGia, nPars ); else - Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, fGlucose, fVerbose ); + Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, nEncVars, fGlucose, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &qbf [-PICT num] [-dgvh]\n" ); + Abc_Print( -2, "usage: &qbf [-PICTK num] [-dgvh]\n" ); Abc_Print( -2, "\t solves QBF problem EpVxM(p,x)\n" ); Abc_Print( -2, "\t-P num : number of parameters p (should be the first PIs) [default = %d]\n", nPars ); Abc_Print( -2, "\t-I num : quit after the given iteration even if unsolved [default = %d]\n", nIterLimit ); Abc_Print( -2, "\t-C num : conflict limit per problem [default = %d]\n", nConfLimit ); Abc_Print( -2, "\t-T num : global timeout [default = %d]\n", nTimeOut ); + Abc_Print( -2, "\t-K num : the number of input bits (for encoding miters only) [default = %d]\n", nEncVars ); Abc_Print( -2, "\t-d : toggle dumping QDIMACS file instead of solving [default = %s]\n", fDumpCnf? "yes": "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", fGlucose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); @@ -44038,6 +44054,75 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9HomoQbf( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_Gen2CreateMiter( int nLutSize, int nLutNum ); + int nLutSize = 2; + int nLutNum = 3; + int fVerbose = 0; + int c; + Gia_Man_t * pTemp; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "KNvh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLutSize < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nLutNum = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLutNum < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + pTemp = Gia_Gen2CreateMiter( nLutSize, nLutNum ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &homoqbf [-KN num] [-vh]\n" ); + Abc_Print( -2, "\t generates QBF miter for the encoding problem\n" ); + Abc_Print( -2, "\t-K num : the LUT size [default = %d]\n", nLutSize ); + Abc_Print( -2, "\t-N num : the number of LUTs [default = %d]\n", nLutNum ); + 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 [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9SatFx( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern int Bmc_FxCompute( Gia_Man_t * p ); |