diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-27 17:21:08 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-27 17:21:08 -0700 |
| commit | 7a2132b237745d04a904350424c12c2afdfd0d42 (patch) | |
| tree | c7711e6a9a0b6d5d8e322338579ffcf1eeb6e9eb /src/sat/cnf | |
| parent | 272089221a530f61bceee07378cb747c88471b70 (diff) | |
| download | abc-7a2132b237745d04a904350424c12c2afdfd0d42.tar.gz abc-7a2132b237745d04a904350424c12c2afdfd0d42.tar.bz2 abc-7a2132b237745d04a904350424c12c2afdfd0d42.zip | |
Added dumping QDIMACS files in command 'qbf'.
Diffstat (limited to 'src/sat/cnf')
| -rw-r--r-- | src/sat/cnf/cnf.h | 2 | ||||
| -rw-r--r-- | src/sat/cnf/cnfMan.c | 38 |
2 files changed, 34 insertions, 6 deletions
diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h index f4c96709..61fa7f14 100644 --- a/src/sat/cnf/cnf.h +++ b/src/sat/cnf/cnf.h @@ -157,7 +157,7 @@ extern void Cnf_DataFree( Cnf_Dat_t * p ); extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ); extern void Cnf_DataFlipLastLiteral( Cnf_Dat_t * p ); extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ); -extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ); +extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vForAlls, Vec_Int_t * vExists ); extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); extern void * Cnf_DataWriteIntoSolverInt( void * pSat, Cnf_Dat_t * p, int nFrames, int fInit ); extern int Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf ); diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c index a8c63bf5..2aa5df6f 100644 --- a/src/sat/cnf/cnfMan.c +++ b/src/sat/cnf/cnfMan.c @@ -264,10 +264,10 @@ void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ) SeeAlso [] ***********************************************************************/ -void Cnf_DataWriteIntoFileGz( Cnf_Dat_t * p, char * pFileName, int fReadable ) +void Cnf_DataWriteIntoFileGz( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vForAlls, Vec_Int_t * vExists ) { gzFile pFile; - int * pLit, * pStop, i; + int * pLit, * pStop, i, VarId; pFile = gzopen( pFileName, "wb" ); if ( pFile == NULL ) { @@ -276,6 +276,20 @@ void Cnf_DataWriteIntoFileGz( Cnf_Dat_t * p, char * pFileName, int fReadable ) } gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" ); gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); + if ( vForAlls ) + { + gzprintf( pFile, "a " ); + Vec_IntForEachEntry( vForAlls, VarId, i ) + gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); + gzprintf( pFile, "0\n" ); + } + if ( vExists ) + { + gzprintf( pFile, "e " ); + Vec_IntForEachEntry( vExists, VarId, i ) + gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); + gzprintf( pFile, "0\n" ); + } for ( i = 0; i < p->nClauses; i++ ) { for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) @@ -297,13 +311,13 @@ void Cnf_DataWriteIntoFileGz( Cnf_Dat_t * p, char * pFileName, int fReadable ) SeeAlso [] ***********************************************************************/ -void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ) +void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vForAlls, Vec_Int_t * vExists ) { FILE * pFile; - int * pLit, * pStop, i; + int * pLit, * pStop, i, VarId; if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) ) { - Cnf_DataWriteIntoFileGz( p, pFileName, fReadable ); + Cnf_DataWriteIntoFileGz( p, pFileName, fReadable, vForAlls, vExists ); return; } pFile = fopen( pFileName, "w" ); @@ -314,6 +328,20 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ) } fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" ); fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); + if ( vForAlls ) + { + fprintf( pFile, "a " ); + Vec_IntForEachEntry( vForAlls, VarId, i ) + fprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); + fprintf( pFile, "0\n" ); + } + if ( vExists ) + { + fprintf( pFile, "e " ); + Vec_IntForEachEntry( vExists, VarId, i ) + fprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); + fprintf( pFile, "0\n" ); + } for ( i = 0; i < p->nClauses; i++ ) { for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) |