diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index dfddc6931..69a6e7235 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -3161,6 +3161,119 @@ void Gia_ManPrintArray( Gia_Man_t * p ) printf( "};\n" ); } + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_GetMValue( int i, int nIns, int Mint, unsigned Truth ) +{ + assert( i >= 0 && i < 16 ); + if ( i < nIns ) + return (Mint >> i) & 1; + if ( i == nIns ) + { + if ( Mint < (1 << nIns) ) + return (Truth >> Mint) & 1; + else + return ((Truth >> (Mint-(1 << nIns))) & 1) == 0; + } + else + return 1; +} +void Gia_ManTestProblem() +{ + unsigned Truth = 0xFE; + int i, j, k, c, nIns = 3, nAux = 3; + int nTotal = nIns + 1 + nAux; + int nPairs = nTotal * (nTotal - 1) / 2; + int nMints = (1 << (nIns+1)); + int M[64][100] = {{0}}; + float Value[64] = {0}; + float Solution[100] = {0}; + assert( nMints <= 64 ); + assert( nPairs <= 100 ); + // 7 nodes: 3 inputs + 1 output + 3 aux + // 7*6/2 = 21 pairs + // 16 minterms + for ( k = 0; k < nMints; k++ ) + { + for ( i = c = 0; i < nTotal; i++ ) + for ( j = i+1; j < nTotal; j++ ) + { + int iVal = Gia_GetMValue( i, nIns, k, Truth ); + int jVal = Gia_GetMValue( j, nIns, k, Truth ); + M[k][c++] = iVal == jVal ? 1 : -1; + } + Value[k] = k < (1 << nIns) ? -1 : 1; + assert( c == nPairs ); + } + + for ( k = 0; k < nMints; k++ ) + { + for ( c = 0; c < nPairs; c++ ) + printf( "%2d ", M[k][c] ); + printf( "%3f\n", Value[k] ); + } + + // solve + float Delta = 0.02; + for ( i = 0; i < 100; i++ ) + { + float Error = 0; + for ( k = 0; k < nMints; k++ ) + Error += Value[k] > 0 ? Value[k] : -Value[k]; + printf( "Round %3d : Error = %5f ", i, Error ); + for ( c = 0; c < nPairs; c++ ) + printf( "%2f ", Solution[c] ); + printf( "\n" ); + + //if ( Error < 1 ) + // Delta /= 10; + + for ( c = 0; c < nPairs; c++ ) + { + int Count = 0; + for ( k = 0; k < nMints; k++ ) + if ( (M[k][c] > 0 && Value[k] > 0) || (M[k][c] < 0 && Value[k] < 0) ) + Count++; + else + Count--; + if ( Count == 0 ) + continue; + printf( "Count = %3d ", Count ); + if ( Count > 0 ) + { + printf( "Increasing %d by %f\n", c, Delta ); + Solution[c] += Delta; + for ( k = 0; k < nMints; k++ ) + if ( M[k][c] > 0 ) + Value[k] -= Delta; + else + Value[k] -= Delta; + } + else + { + printf( "Reducing %d by %f\n", c, Delta ); + Solution[c] -= Delta; + for ( k = 0; k < nMints; k++ ) + if ( M[k][c] > 0 ) + Value[k] += Delta; + else + Value[k] += Delta; + } + } + } +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 586ac2c57..43207c887 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -139,6 +139,7 @@ static int Abc_CommandTestDec ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandTestNpn ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestRPO ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestTruth ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRunSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunEco ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -914,6 +915,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "testnpn", Abc_CommandTestNpn, 0 ); Cmd_CommandAdd( pAbc, "LogiCS", "testrpo", Abc_CommandTestRPO, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "testtruth", Abc_CommandTestTruth, 0 ); + Cmd_CommandAdd( pAbc, "Synthesis", "runsat", Abc_CommandRunSat, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "runeco", Abc_CommandRunEco, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "rungen", Abc_CommandRunGen, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "xec", Abc_CommandRunTest, 0 ); @@ -7168,6 +7170,93 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandRunSat( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pFile = NULL; + char * pFileCnf = NULL; + int c, i, fWalk = 0, fKissat = 0, nIters = 10, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Ikwvh" ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nIters < 0 ) + goto usage; + break; + case 'k': + fKissat ^= 1; + break; + case 'w': + fWalk ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( fKissat + fWalk != 1 ) { + printf( "Exactly one SAT solver should be selected.\n" ); + return 1; + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + pFileCnf = argv[globalUtilOptind]; + pFile = fopen( pFileCnf, "rb" ); + if ( pFile == NULL ) { + printf( "The file \"%s\" cannot be found.\n", pFileCnf ); + return 1; + } + fclose( pFile ); + abctime clk = Abc_Clock(); + for ( i = 0; i < nIters; i++ ) { + char pCommand[1000]; + if ( fKissat ) + sprintf( pCommand, "kissat -q --seed=%d %s", i, pFileCnf ); + else if ( fWalk ) + sprintf( pCommand, "walk -s%d %s", i, pFileCnf ); + if (system(pCommand) == -1) { + fprintf(stdout, "Command \"%s\" did not succeed.\n", pCommand); + return 0; + } + } + printf( "Performed %d iterations of SAT solving. ", nIters ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return 0; + +usage: + Abc_Print( -2, "usage: runsat [-I num] [-kwvh] \n" ); + Abc_Print( -2, "\t performs randomized iterations of SAT solving\n" ); + Abc_Print( -2, "\t-I num : the number of iterations [default = %d]\n", nIters ); + Abc_Print( -2, "\t-k : toggle using Kissat (binary name \"kissat\") [default = %s]\n", fKissat? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle using WalkSat (binary name \"walk\") [default = %s]\n", fWalk? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -14622,7 +14711,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); } */ - + //Gia_ManTestProblem(); return 0; usage: Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] \n" ); diff --git a/src/base/io/io.c b/src/base/io/io.c index e808d1d0b..f988a0078 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -52,6 +52,7 @@ static int IoCommandReadInit ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadPlaMo ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadTruth ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandReadCnf ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadStatus ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadGig ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -124,6 +125,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_plamo", IoCommandReadPlaMo, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_truth", IoCommandReadTruth, 1 ); + Cmd_CommandAdd( pAbc, "I/O", "read_cnf", IoCommandReadCnf, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_status", IoCommandReadStatus, 0 ); Cmd_CommandAdd( pAbc, "I/O", "&read_gig", IoCommandReadGig, 0 ); @@ -1209,6 +1211,75 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandReadCnf( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Vec_Ptr_t * Io_FileReadCnf( char * pFileName ); + FILE * pFile; + Abc_Ntk_t * pNtk; + Vec_Ptr_t * vSops; + int c; + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( argc != globalUtilOptind + 1 ) + goto usage; + + pFile = fopen( argv[globalUtilOptind], "rb" ); + if ( pFile == NULL ) + { + printf( "The file \"%s\" cannot be found.\n", argv[globalUtilOptind] ); + return 1; + } + else + fclose( pFile ); + vSops = Io_FileReadCnf( argv[globalUtilOptind] ); + if ( Vec_PtrSize(vSops) == 0 ) + { + Vec_PtrFreeFree( vSops ); + fprintf( pAbc->Err, "Reading CNF file has failed.\n" ); + return 1; + } + pNtk = Abc_NtkCreateWithNodes( vSops ); + Vec_PtrFreeFree( vSops ); + if ( pNtk == NULL ) + { + fprintf( pAbc->Err, "Deriving the network has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); + Abc_FrameClearVerifStatus( pAbc ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: read_cnf [-h] \n" ); + fprintf( pAbc->Err, "\t creates network with one node\n" ); + fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); + fprintf( pAbc->Err, "\tfile : file name with the truth table\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index eef80efa3..e57fa9574 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -920,6 +920,93 @@ void Io_TransformSF2PLA( char * pNameIn, char * pNameOut ) ABC_FREE( pBuffer ); } +/**Function************************************************************* + + Synopsis [Reads CNF from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Io_ConvertNumsToSop( Vec_Wec_t * vNums, int nVars ) +{ + Vec_Int_t * vLevel; int i, k, Num; + int nSize = (nVars + 3)*Vec_WecSize(vNums); + char * pStr = ABC_ALLOC( char, nSize+1 ); + memset( pStr, '-', nSize ); + pStr[nSize] = 0; + Vec_WecForEachLevel( vNums, vLevel, i ) + { + char * pCube = pStr + (nVars + 3)*i; + Vec_IntForEachEntry( vLevel, Num, k ) + pCube[Abc_Lit2Var(Num)] = '0' + Abc_LitIsCompl(Num); + pCube[nVars+0] = ' '; + pCube[nVars+1] = '1'; + pCube[nVars+2] = '\n'; + } + return pStr; +} +Vec_Ptr_t * Io_FileReadCnf( char * pFileName ) +{ + Vec_Ptr_t * vSops = Vec_PtrAlloc( 1 ); + Vec_Wec_t * vNums = Vec_WecAlloc( 100 ); + Vec_Int_t * vLevel; + char * pThis, pLine[10000]; + int nVars = -1, nClas = -1; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) { + printf( "Cannot open file \"%s\" for reading.\n", pFileName ); + return NULL; + } + while ( fgets( pLine, 10000, pFile ) ) + { + if ( pLine[0] == 'c' ) + continue; + if ( pLine[0] == 'p' ) + { + pThis = strtok(pLine+1, " \t\n\r"); + if ( strcmp(pThis, "cnf") ) + { + Vec_PtrFree( vSops ); + Vec_WecFree( vNums ); + fclose( pFile ); + printf( "Wrong file format.\n" ); + return NULL; + } + pThis = strtok(NULL, " \t\n\r"); + nVars = atoi(pThis); + pThis = strtok(NULL, " \t\n\r"); + nClas = atoi(pThis); + continue; + } + pThis = strtok(pLine, " \t\n\r"); + if ( pThis == NULL ) + continue; + vLevel = Vec_WecPushLevel( vNums ); + while ( pThis ) { + int fComp, Temp = atoi(pThis); + if ( Temp == 0 ) + break; + fComp = Temp < 0; + Temp = Temp < 0 ? -Temp : Temp; + Temp -= 1; + assert( Temp < nVars ); + Vec_IntPush( vLevel, Abc_Var2Lit(Temp, fComp) ); + pThis = strtok(NULL, " \t\n\r"); + } + } + fclose( pFile ); + if ( nClas != Vec_WecSize(vNums) ) + printf( "Warning: The number of clauses (%d) listed is different from the actual number (%d).\n", nClas, Vec_WecSize(vNums) ); + //Vec_WecPrint( vNums, 0 ); + Vec_PtrPush( vSops, Io_ConvertNumsToSop(vNums, nVars) ); + Vec_WecFree( vNums ); + return vSops; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////