From 6e6c728b65f470c1c3d9d1715c86948f0e1569d0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 3 Dec 2022 20:29:06 -0800 Subject: [PATCH] Another way of dumping QBF problem into a file. --- src/aig/gia/giaQbf.c | 39 +++++++++++++++++++ src/base/abci/abc.c | 14 +++++-- src/sat/cnf/cnf.h | 1 + src/sat/cnf/cnfMan.c | 89 ++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 140 insertions(+), 3 deletions(-) diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index ac6fb22ce..ef97f4350 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -482,6 +482,45 @@ void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ) Vec_IntFree( vVarMap ); printf( "The 2QBF formula was written into file \"%s\".\n", pFileName ); } +void Gia_QbfDumpFileInv( Gia_Man_t * pGia, int nPars ) +{ + // original problem: \exists p \forall x \exists y. M(p,x,y) + // negated problem: \forall p \exists x \exists y. !M(p,x,y) + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 ); + Vec_Int_t * vVarMap, * vForAlls, * vExists1, * vExists2; + Gia_Obj_t * pObj; + char * pFileName; + int i, Entry; + // complement the last clause + //int * pLit = pCnf->pClauses[pCnf->nClauses] - 1; *pLit ^= 1; + // create var map + vVarMap = Vec_IntStart( pCnf->nVars ); + Gia_ManForEachCi( pGia, pObj, i ) + Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Gia_ManCiIdToId(pGia, i)], i < nPars ? 1 : 2 ); + // create various maps + vExists1 = Vec_IntAlloc( nPars ); + vForAlls = Vec_IntAlloc( nPars ); + vExists2 = Vec_IntAlloc( Gia_ManCiNum(pGia) - 2*nPars ); + Vec_IntForEachEntry( vVarMap, Entry, i ) + if ( Entry == 1 ) + Vec_IntPush( vExists1, i ); + else if ( Entry == 2 ) + Vec_IntPush( vForAlls, i ); + else + Vec_IntPush( vExists2, i ); + // generate CNF + pFileName = Extra_FileNameGenericAppend( pGia->pSpec, ".qdimacs" ); + Cnf_DataWriteIntoFileInv( pCnf, pFileName, 0, vExists1, vForAlls, vExists2 ); + Cnf_DataFree( pCnf ); + Vec_IntFree( vExists1 ); + Vec_IntFree( vForAlls ); + Vec_IntFree( vExists2 ); + Vec_IntFree( vVarMap ); + printf( "The 2QBF formula was written into file \"%s\".\n", pFileName ); +} + + + /**Function************************************************************* diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a65b37e27..36367a204 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -46191,6 +46191,7 @@ usage: int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ); + extern void Gia_QbfDumpFileInv( Gia_Man_t * pGia, int nPars ); 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; @@ -46198,10 +46199,11 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) int nTimeOut = 0; int nEncVars = 0; int fDumpCnf = 0; + int fDumpCnf2 = 0; int fGlucose = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PICTKdgvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PICTKdegvh" ) ) != EOF ) { switch ( c ) { @@ -46263,6 +46265,9 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': fDumpCnf ^= 1; break; + case 'e': + fDumpCnf2 ^= 1; + break; case 'g': fGlucose ^= 1; break; @@ -46297,19 +46302,22 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( fDumpCnf ) Gia_QbfDumpFile( pAbc->pGia, nPars ); + else if ( fDumpCnf2 ) + Gia_QbfDumpFileInv( pAbc->pGia, nPars ); else Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, nEncVars, fGlucose, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &qbf [-PICTK num] [-dgvh]\n" ); + Abc_Print( -2, "usage: &qbf [-PICTK num] [-degvh]\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-d : toggle dumping QDIMACS file instead of solving (complemented QBF) [default = %s]\n", fDumpCnf? "yes": "no" ); + Abc_Print( -2, "\t-e : toggle dumping QDIMACS file instead of solving (original QBF) [default = %s]\n", fDumpCnf2? "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" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h index 01728c81e..35c0fa2f7 100644 --- a/src/sat/cnf/cnf.h +++ b/src/sat/cnf/cnf.h @@ -160,6 +160,7 @@ extern void Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec extern void Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits ); extern void Cnf_DataPrint( Cnf_Dat_t * p, 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_DataWriteIntoFileInv( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vExists1, Vec_Int_t * vForAlls, Vec_Int_t * vExists2 ); 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 5a125ec3c..f63cc6335 100644 --- a/src/sat/cnf/cnfMan.c +++ b/src/sat/cnf/cnfMan.c @@ -303,6 +303,48 @@ void Cnf_DataWriteIntoFileGz( Cnf_Dat_t * p, char * pFileName, int fReadable, Ve gzprintf( pFile, "\n" ); gzclose( pFile ); } +void Cnf_DataWriteIntoFileInvGz( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vExists1, Vec_Int_t * vForAlls, Vec_Int_t * vExists2 ) +{ + gzFile pFile; + int * pLit, * pStop, i, VarId; + pFile = gzopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" ); + return; + } + 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 ( vExists1 ) + { + gzprintf( pFile, "e " ); + Vec_IntForEachEntry( vExists1, VarId, i ) + gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); + gzprintf( pFile, "0\n" ); + } + if ( vForAlls ) + { + gzprintf( pFile, "a " ); + Vec_IntForEachEntry( vForAlls, VarId, i ) + gzprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); + gzprintf( pFile, "0\n" ); + } + if ( vExists2 ) + { + gzprintf( pFile, "e " ); + Vec_IntForEachEntry( vExists2, 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++ ) + gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); + gzprintf( pFile, "0\n" ); + } + gzprintf( pFile, "\n" ); + gzclose( pFile ); +} /**Function************************************************************* @@ -355,6 +397,53 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_ fprintf( pFile, "\n" ); fclose( pFile ); } +void Cnf_DataWriteIntoFileInv( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vExists1, Vec_Int_t * vForAlls, Vec_Int_t * vExists2 ) +{ + FILE * pFile; + int * pLit, * pStop, i, VarId; + if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) ) + { + Cnf_DataWriteIntoFileInvGz( p, pFileName, fReadable, vExists1, vForAlls, vExists2 ); + return; + } + pFile = fopen( pFileName, "w" ); + if ( pFile == NULL ) + { + printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" ); + return; + } + 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 ( vExists1 ) + { + fprintf( pFile, "e " ); + Vec_IntForEachEntry( vExists1, VarId, i ) + fprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); + fprintf( pFile, "0\n" ); + } + if ( vForAlls ) + { + fprintf( pFile, "a " ); + Vec_IntForEachEntry( vForAlls, VarId, i ) + fprintf( pFile, "%d ", fReadable? VarId : VarId+1 ); + fprintf( pFile, "0\n" ); + } + if ( vExists2 ) + { + fprintf( pFile, "e " ); + Vec_IntForEachEntry( vExists2, 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++ ) + fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); + fprintf( pFile, "0\n" ); + } + fprintf( pFile, "\n" ); + fclose( pFile ); +} /**Function*************************************************************