luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Improvements to CNF generation.

This commit is contained in:
Alan Mishchenko 2014-06-23 13:11:59 -07:00
parent f93e524421
commit 44d9c7e543
11 changed files with 2066 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/aig/gia/giaJf.c
View File

@ -1750,23 +1750,30 @@ Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p, int fCnfObjIds )
pPars->fCnfObjIds = fCnfObjIds;
return Jf_ManPerformMapping( p, pPars );
}
Gia_Man_t * Jf_ManDeriveCnfMiter( Gia_Man_t * p )
Gia_Man_t * Jf_ManDeriveCnfMiter( Gia_Man_t * p, int fVerbose )
{
Jf_Par_t Pars, * pPars = &Pars;
Jf_ManSetDefaultPars( pPars );
pPars->fGenCnf = 1;
pPars->fCnfObjIds = 0;
pPars->fAddOrCla = 1;
pPars->fVerbose = fVerbose;
return Jf_ManPerformMapping( p, pPars );
}
void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName )
void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int fVerbose )
{
abctime clk = Abc_Clock();
Gia_Man_t * pNew;
Cnf_Dat_t * pCnf;
pNew = Jf_ManDeriveCnfMiter( p );
pNew = Jf_ManDeriveCnfMiter( p, fVerbose );
pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL );
Gia_ManStop( pNew );
// if ( fVerbose )
{
printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
Cnf_DataFree(pCnf);
}

1582
src/aig/gia/giaMf.c
View File

File diff suppressed because it is too large Load Diff

19
src/base/abci/abc.c
View File

@ -20965,6 +20965,22 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
if ( argc == globalUtilOptind + 1 )
{
extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int fVerbose );
// get the input file name
char * pFileName = argv[globalUtilOptind];
FILE * pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\" for writing.\n", pFileName );
return 0;
}
fclose( pFile );
Cnf_DataSolveFromFile( pFileName, nConfLimit, fVerbose );
return 0;
}
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
@ -20987,7 +21003,6 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
clk = Abc_Clock();
RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fAlignPol, fAndOuts, fNewSolver, fVerbose );
// verify that the pattern is correct
@ -31406,6 +31421,8 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Lf(): Mapping into LUTs has failed.\n" );
return 1;
}
if ( pPars->fGenCnf )
Cnf_DataFree( pAbc->pGia->pData ), pAbc->pGia->pData = NULL;
Abc_FrameUpdateGia( pAbc, pNew );
return 0;

4
src/base/abci/abcDar.c
View File

@ -1561,9 +1561,9 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
Cnf_DataTranformPolarity( pCnf, 0 );
// print stats
if ( fVerbose )
// if ( fVerbose )
{
Abc_Print( 1, "Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
Abc_Print( 1, "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}

44
src/base/io/io.c
View File

@ -1938,15 +1938,30 @@ usage:
***********************************************************************/
int IoCommandWriteCnf2( Abc_Frame_t * pAbc, int argc, char **argv )
{
extern void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName );
extern void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int fVerbose );
extern void Mf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int nLutSize, int fVerbose );
FILE * pFile;
char * pFileName;
int nLutSize = 6;
int fNewAlgo = 1;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Kavh" ) ) != 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++;
break;
case 'a':
fNewAlgo ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -1966,7 +1981,12 @@ int IoCommandWriteCnf2( Abc_Frame_t * pAbc, int argc, char **argv )
Abc_Print( -1, "IoCommandWriteCnf2(): Works only for combinational miters.\n" );
return 0;
}
if ( !Sdm_ManCanRead() )
if ( nLutSize < 3 || nLutSize > 8 )
{
Abc_Print( -1, "IoCommandWriteCnf2(): Invalid LUT size (%d).\n", nLutSize );
return 0;
}
if ( !fNewAlgo && !Sdm_ManCanRead() )
{
Abc_Print( -1, "IoCommandWriteCnf2(): Cannot input precomputed DSD information.\n" );
return 0;
@ -1981,15 +2001,21 @@ int IoCommandWriteCnf2( Abc_Frame_t * pAbc, int argc, char **argv )
printf( "Cannot open file \"%s\" for writing.\n", pFileName );
return 0;
}
Jf_ManDumpCnf( pAbc->pGia, pFileName );
fclose( pFile );
if ( fNewAlgo )
Mf_ManDumpCnf( pAbc->pGia, pFileName, nLutSize, fVerbose );
else
Jf_ManDumpCnf( pAbc->pGia, pFileName, fVerbose );
return 0;
usage:
fprintf( pAbc->Err, "usage: &write_cnf [-vh] <file>\n" );
fprintf( pAbc->Err, "\t writes CNF produced by new DSD-based generator\n" );
fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
fprintf( pAbc->Err, "usage: &write_cnf [-Kavh] <file>\n" );
fprintf( pAbc->Err, "\t writes CNF produced by a new generator\n" );
fprintf( pAbc->Err, "\t-K <num> : the LUT size (3 <= num <= 8) [default = %d]\n", nLutSize );
fprintf( pAbc->Err, "\t-a : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" );
fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
return 1;
}

250
src/misc/util/utilTruth.h
View File

@ -1450,6 +1450,256 @@ static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars, int * pnCubes )
assert( (uRes2 & ~uOnDc) == 0 );
return uRes2;
}
static inline int Abc_Tt7Isop( word uOn[2], word uOnDc[2], int nVars, word uRes[2] )
{
int nCubes = 0;
if ( nVars <= 6 || (uOn[0] == uOn[1] && uOnDc[0] == uOnDc[1]) )
uRes[0] = uRes[1] = Abc_Tt6Isop( uOn[0], uOnDc[0], Abc_MinInt(nVars, 6), &nCubes );
else
{
word uRes0, uRes1, uRes2;
assert( nVars == 7 );
// solve for cofactors
uRes0 = Abc_Tt6Isop( uOn[0] & ~uOnDc[1], uOnDc[0], 6, &nCubes );
uRes1 = Abc_Tt6Isop( uOn[1] & ~uOnDc[0], uOnDc[1], 6, &nCubes );
uRes2 = Abc_Tt6Isop( (uOn[0] & ~uRes0) | (uOn[1] & ~uRes1), uOnDc[0] & uOnDc[1], 6, &nCubes );
// derive the final truth table
uRes[0] = uRes2 | uRes0;
uRes[1] = uRes2 | uRes1;
assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 );
assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 );
}
return nCubes;
}
static inline int Abc_Tt8Isop( word uOn[4], word uOnDc[4], int nVars, word uRes[4] )
{
int nCubes = 0;
if ( nVars <= 6 )
uRes[0] = uRes[1] = uRes[2] = uRes[3] = Abc_Tt6Isop( uOn[0], uOnDc[0], nVars, &nCubes );
else if ( nVars == 7 || (uOn[0] == uOn[2] && uOn[1] == uOn[3] && uOnDc[0] == uOnDc[2] && uOnDc[1] == uOnDc[3]) )
{
nCubes = Abc_Tt7Isop( uOn, uOnDc, 7, uRes );
uRes[2] = uRes[0];
uRes[3] = uRes[1];
}
else
{
word uOn0[2], uOn1[2], uOn2[2], uOnDc2[2], uRes0[2], uRes1[2], uRes2[2];
assert( nVars == 8 );
// cofactor
uOn0[0] = uOn[0] & ~uOnDc[2];
uOn0[1] = uOn[1] & ~uOnDc[3];
uOn1[0] = uOn[2] & ~uOnDc[0];
uOn1[1] = uOn[3] & ~uOnDc[1];
uOnDc2[0] = uOnDc[0] & uOnDc[2];
uOnDc2[1] = uOnDc[1] & uOnDc[3];
// solve for cofactors
nCubes += Abc_Tt7Isop( uOn0, uOnDc+0, 7, uRes0 );
nCubes += Abc_Tt7Isop( uOn1, uOnDc+2, 7, uRes1 );
uOn2[0] = (uOn[0] & ~uRes0[0]) | (uOn[2] & ~uRes1[0]);
uOn2[1] = (uOn[1] & ~uRes0[1]) | (uOn[3] & ~uRes1[1]);
nCubes += Abc_Tt7Isop( uOn2, uOnDc2, 7, uRes2 );
// derive the final truth table
uRes[0] = uRes2[0] | uRes0[0];
uRes[1] = uRes2[1] | uRes0[1];
uRes[2] = uRes2[0] | uRes1[0];
uRes[3] = uRes2[1] | uRes1[1];
assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 && (uOn[2] & ~uRes[2]) == 0 && (uOn[3] & ~uRes[3]) == 0 );
assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 && (uRes[2] & ~uOnDc[2])==0 && (uRes[3] & ~uOnDc[3])==0 );
}
return nCubes;
}
/**Function*************************************************************
Synopsis [Computes CNF size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_Tt6CnfSize( word t, int nVars )
{
int nCubes = 0;
Abc_Tt6Isop( t, t, nVars, &nCubes );
Abc_Tt6Isop( ~t, ~t, nVars, &nCubes );
assert( nCubes <= 64 );
return nCubes;
}
static inline int Abc_Tt8CnfSize( word t[4], int nVars )
{
word uRes[4], tc[4] = {~t[0], ~t[1], ~t[2], ~t[3]};
int nCubes = 0;
nCubes += Abc_Tt8Isop( t, t, nVars, uRes );
nCubes += Abc_Tt8Isop( tc, tc, nVars, uRes );
assert( nCubes <= 256 );
return nCubes;
}
/**Function*************************************************************
Synopsis [Derives ISOP cover for the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline word Abc_Tt6IsopCover( word uOn, word uOnDc, int nVars, int * pCover, int * pnCubes )
{
word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
int c, Var, nBeg0, nEnd0, nEnd1;
assert( nVars <= 6 );
assert( (uOn & ~uOnDc) == 0 );
if ( uOn == 0 )
return 0;
if ( uOnDc == ~(word)0 )
{
pCover[(*pnCubes)++] = 0;
return ~(word)0;
}
assert( nVars > 0 );
// find the topmost var
for ( Var = nVars-1; Var >= 0; Var-- )
if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
break;
assert( Var >= 0 );
// cofactor
uOn0 = Abc_Tt6Cofactor0( uOn, Var );
uOn1 = Abc_Tt6Cofactor1( uOn , Var );
uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
// solve for cofactors
nBeg0 = *pnCubes;
uRes0 = Abc_Tt6IsopCover( uOn0 & ~uOnDc1, uOnDc0, Var, pCover, pnCubes );
nEnd0 = *pnCubes;
uRes1 = Abc_Tt6IsopCover( uOn1 & ~uOnDc0, uOnDc1, Var, pCover, pnCubes );
nEnd1 = *pnCubes;
uRes2 = Abc_Tt6IsopCover( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pCover, pnCubes );
// derive the final truth table
uRes2 |= (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
for ( c = nBeg0; c < nEnd0; c++ )
pCover[c] |= (1 << (2*Var+0));
for ( c = nEnd0; c < nEnd1; c++ )
pCover[c] |= (1 << (2*Var+1));
assert( (uOn & ~uRes2) == 0 );
assert( (uRes2 & ~uOnDc) == 0 );
return uRes2;
}
static inline void Abc_Tt7IsopCover( word uOn[2], word uOnDc[2], int nVars, word uRes[2], int * pCover, int * pnCubes )
{
if ( nVars <= 6 || (uOn[0] == uOn[1] && uOnDc[0] == uOnDc[1]) )
uRes[0] = uRes[1] = Abc_Tt6IsopCover( uOn[0], uOnDc[0], Abc_MinInt(nVars, 6), pCover, pnCubes );
else
{
word uRes0, uRes1, uRes2;
int c, nBeg0, nEnd0, nEnd1;
assert( nVars == 7 );
// solve for cofactors
nBeg0 = *pnCubes;
uRes0 = Abc_Tt6IsopCover( uOn[0] & ~uOnDc[1], uOnDc[0], 6, pCover, pnCubes );
nEnd0 = *pnCubes;
uRes1 = Abc_Tt6IsopCover( uOn[1] & ~uOnDc[0], uOnDc[1], 6, pCover, pnCubes );
nEnd1 = *pnCubes;
uRes2 = Abc_Tt6IsopCover( (uOn[0] & ~uRes0) | (uOn[1] & ~uRes1), uOnDc[0] & uOnDc[1], 6, pCover, pnCubes );
// derive the final truth table
uRes[0] = uRes2 | uRes0;
uRes[1] = uRes2 | uRes1;
for ( c = nBeg0; c < nEnd0; c++ )
pCover[c] |= (1 << (2*6+0));
for ( c = nEnd0; c < nEnd1; c++ )
pCover[c] |= (1 << (2*6+1));
assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 );
assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 );
}
}
static inline void Abc_Tt8IsopCover( word uOn[4], word uOnDc[4], int nVars, word uRes[4], int * pCover, int * pnCubes )
{
int nCubes = 0;
if ( nVars <= 6 )
uRes[0] = uRes[1] = uRes[2] = uRes[3] = Abc_Tt6IsopCover( uOn[0], uOnDc[0], nVars, pCover, pnCubes );
else if ( nVars == 7 || (uOn[0] == uOn[2] && uOn[1] == uOn[3] && uOnDc[0] == uOnDc[2] && uOnDc[1] == uOnDc[3]) )
{
Abc_Tt7IsopCover( uOn, uOnDc, 7, uRes, pCover, pnCubes );
uRes[2] = uRes[0];
uRes[3] = uRes[1];
}
else
{
word uOn0[2], uOn1[2], uOn2[2], uOnDc2[2], uRes0[2], uRes1[2], uRes2[2];
int c, nBeg0, nEnd0, nEnd1;
assert( nVars == 8 );
// cofactor
uOn0[0] = uOn[0] & ~uOnDc[2];
uOn0[1] = uOn[1] & ~uOnDc[3];
uOn1[0] = uOn[2] & ~uOnDc[0];
uOn1[1] = uOn[3] & ~uOnDc[1];
uOnDc2[0] = uOnDc[0] & uOnDc[2];
uOnDc2[1] = uOnDc[1] & uOnDc[3];
// solve for cofactors
nBeg0 = *pnCubes;
Abc_Tt7IsopCover( uOn0, uOnDc+0, 7, uRes0, pCover, pnCubes );
nEnd0 = *pnCubes;
Abc_Tt7IsopCover( uOn1, uOnDc+2, 7, uRes1, pCover, pnCubes );
nEnd1 = *pnCubes;
uOn2[0] = (uOn[0] & ~uRes0[0]) | (uOn[2] & ~uRes1[0]);
uOn2[1] = (uOn[1] & ~uRes0[1]) | (uOn[3] & ~uRes1[1]);
Abc_Tt7IsopCover( uOn2, uOnDc2, 7, uRes2, pCover, pnCubes );
// derive the final truth table
uRes[0] = uRes2[0] | uRes0[0];
uRes[1] = uRes2[1] | uRes0[1];
uRes[2] = uRes2[0] | uRes1[0];
uRes[3] = uRes2[1] | uRes1[1];
for ( c = nBeg0; c < nEnd0; c++ )
pCover[c] |= (1 << (2*7+0));
for ( c = nEnd0; c < nEnd1; c++ )
pCover[c] |= (1 << (2*7+1));
assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 && (uOn[2] & ~uRes[2]) == 0 && (uOn[3] & ~uRes[3]) == 0 );
assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 && (uRes[2] & ~uOnDc[2])==0 && (uRes[3] & ~uOnDc[3])==0 );
}
}
/**Function*************************************************************
Synopsis [Computes CNF for the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_Tt6Cnf( word t, int nVars, int * pCover )
{
int c, nCubes = 0;
Abc_Tt6IsopCover( t, t, nVars, pCover, &nCubes );
for ( c = 0; c < nCubes; c++ )
pCover[c] |= (1 << (2*nVars+0));
Abc_Tt6IsopCover( ~t, ~t, nVars, pCover, &nCubes );
for ( ; c < nCubes; c++ )
pCover[c] |= (1 << (2*nVars+1));
assert( nCubes <= 64 );
return nCubes;
}
static inline int Abc_Tt8Cnf( word t[4], int nVars, int * pCover )
{
word uRes[4], tc[4] = {~t[0], ~t[1], ~t[2], ~t[3]};
int c, nCubes = 0;
Abc_Tt8IsopCover( t, t, nVars, uRes, pCover, &nCubes );
for ( c = 0; c < nCubes; c++ )
pCover[c] |= (1 << (2*nVars+0));
Abc_Tt8IsopCover( tc, tc, nVars, uRes, pCover, &nCubes );
for ( ; c < nCubes; c++ )
pCover[c] |= (1 << (2*nVars+1));
assert( nCubes <= 256 );
return nCubes;
}
/**Function*************************************************************

12
src/proof/fra/fraCec.c
View File

@ -67,6 +67,12 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
if ( fFlipBits )
Cnf_DataTranformPolarity( pCnf, 0 );
if ( fVerbose )
{
printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// convert into SAT solver
pSat = (sat_solver2 *)Cnf_DataWriteIntoSolver2( pCnf, 1, 0 );
if ( pSat == NULL )
@ -173,6 +179,12 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
if ( fFlipBits )
Cnf_DataTranformPolarity( pCnf, 0 );
if ( fVerbose )
{
printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// convert into SAT solver
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )

1
src/sat/bmc/bmcFault.c
View File

@ -141,6 +141,7 @@ static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
Aig_ManStop( pAig );
return pCnf;
// return Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
}
/**Function*************************************************************

1
src/sat/cnf/cnf.h
View File

@ -178,6 +178,7 @@ extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPre
extern Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p );
extern Cnf_Dat_t * Cnf_DataReadFromFile( char * pFileName );
/*=== cnfWrite.c ========================================================*/
extern Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped );
extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );

2
src/sat/cnf/cnfFast.c
View File

@ -681,7 +681,7 @@ Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs )
Aig_ManCleanMarkA( p );
// Abc_PrintTime( 1, "TOTAL ", Abc_Clock() - clkTotal );
// printf( "Vars = %6d. Clauses = %7d. Literals = %8d. \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
// printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
// Cnf_DataFree( pCnf );
// pCnf = NULL;

158
src/sat/cnf/cnfUtil.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "cnf.h"
#include "sat/bsat/satSolver.h"
ABC_NAMESPACE_IMPL_START
@ -289,6 +290,163 @@ unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p )
return pPres;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_DataReadFromFile( char * pFileName )
{
int MaxLine = 1000000;
int Var, Lit, nVars = -1, nClas = -1, i, Entry, iLine = 0;
Cnf_Dat_t * pCnf = NULL;
Vec_Int_t * vClas = NULL;
Vec_Int_t * vLits = NULL;
char * pBuffer, * pToken;
FILE * pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\" for writing.\n", pFileName );
return NULL;
}
pBuffer = ABC_ALLOC( char, MaxLine );
while ( fgets(pBuffer, MaxLine, pFile) != NULL )
{
iLine++;
if ( pBuffer[0] == 'c' )
continue;
if ( pBuffer[0] == 'p' )
{
pToken = strtok( pBuffer+1, " \t" );
if ( strcmp(pToken, "cnf") )
{
printf( "Incorrect input file.\n" );
goto finish;
}
pToken = strtok( NULL, " \t" );
nVars = atoi( pToken );
pToken = strtok( NULL, " \t" );
nClas = atoi( pToken );
if ( nVars <= 0 || nClas <= 0 )
{
printf( "Incorrect parameters.\n" );
goto finish;
}
// temp storage
vClas = Vec_IntAlloc( nClas+1 );
vLits = Vec_IntAlloc( nClas*8 );
continue;
}
pToken = strtok( pBuffer, " \t\r\n" );
if ( pToken == NULL )
continue;
Vec_IntPush( vClas, Vec_IntSize(vLits) );
while ( pToken )
{
Var = atoi( pToken );
if ( Var == 0 )
break;
Lit = (Var > 0) ? Abc_Var2Lit(Var-1, 0) : Abc_Var2Lit(-Var-1, 1);
if ( Lit >= 2*nVars )
{
printf( "Literal %d is out-of-bound for %d variables.\n", Lit, nVars );
goto finish;
}
Vec_IntPush( vLits, Lit );
pToken = strtok( NULL, " \t\r\n" );
}
if ( Var != 0 )
{
printf( "There is no zero-terminator in line %d.\n", iLine );
goto finish;
}
}
// finalize
if ( Vec_IntSize(vClas) != nClas )
printf( "Warning! The number of clauses (%d) is different from declaration (%d).\n", Vec_IntSize(vClas), nClas );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
// create
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->nVars = nVars;
pCnf->nClauses = nClas;
pCnf->nLiterals = Vec_IntSize(vLits);
pCnf->pClauses = ABC_ALLOC( int *, Vec_IntSize(vClas) );
pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
Vec_IntForEachEntry( vClas, Entry, i )
pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
finish:
fclose( pFile );
Vec_IntFreeP( &vClas );
Vec_IntFreeP( &vLits );
ABC_FREE( pBuffer );
return pCnf;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int fVerbose )
{
abctime clk = Abc_Clock();
Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName );
sat_solver * pSat;
int status, RetValue = -1;
if ( pCnf == NULL )
return -1;
if ( fVerbose )
{
printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// convert into SAT solver
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
Cnf_DataFree( pCnf );
if ( pSat == NULL )
{
printf( "The problem is trivially UNSAT.\n" );
return 1;
}
// solve the miter
// if ( fVerbose )
// pSat->verbosity = 1;
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_Undef )
RetValue = -1;
else if ( status == l_True )
RetValue = 0;
else if ( status == l_False )
RetValue = 1;
else
assert( 0 );
if ( fVerbose )
Sat_SolverPrintStats( stdout, pSat );
sat_solver_delete( pSat );
if ( RetValue == -1 )
Abc_Print( 1, "UNDECIDED " );
else if ( RetValue == 0 )
Abc_Print( 1, "SATISFIABLE " );
else
Abc_Print( 1, "UNSATISFIABLE " );
//Abc_Print( -1, "\n" );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////