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

Another way of dumping QBF problem into a file.

This commit is contained in:
Alan Mishchenko 2022-12-03 20:29:06 -08:00
parent 2c7a456c37
commit 6e6c728b65
4 changed files with 140 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
src/aig/gia/giaQbf.c
View File

@ -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*************************************************************

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

@ -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");

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

@ -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 );

89
src/sat/cnf/cnfMan.c
View File

@ -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*************************************************************