Skip to content

A
abc
Commit 7a2132b2 by Alan Mishchenko
Options

Added dumping QDIMACS files in command 'qbf'.

parent 27208922
Showing with 82 additions and 13 deletions
src/base/abci/abc.c
......@@ -11560,15 +11560,17 @@ int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int nPars;
int nIters;
int fDumpCnf;
int fVerbose;
extern void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nIters, int fVerbose );
extern void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nIters, int fDumpCnf, int fVerbose );
// set defaults
nPars = -1;
nIters = 500;
fDumpCnf = 0;
fVerbose = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PIvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PIdvh" ) ) != EOF )
{
switch ( c )
{
......@@ -11594,6 +11596,9 @@ int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nIters < 0 )
goto usage;
break;
case 'd':
fDumpCnf ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -11624,20 +11629,21 @@ int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( Abc_NtkIsStrash(pNtk) )
Abc_NtkQbf( pNtk, nPars, nIters, fVerbose );
Abc_NtkQbf( pNtk, nPars, nIters, fDumpCnf, fVerbose );
else
{
pNtk = Abc_NtkStrash( pNtk, 0, 1, 0 );
Abc_NtkQbf( pNtk, nPars, nIters, fVerbose );
Abc_NtkQbf( pNtk, nPars, nIters, fDumpCnf, fVerbose );
Abc_NtkDelete( pNtk );
}
return 0;
usage:
Abc_Print( -2, "usage: qbf [-PI num] [-vh]\n" );
Abc_Print( -2, "usage: qbf [-PI num] [-dvh]\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", nIters );
Abc_Print( -2, "\t-d : toggle dumping QDIMACS file instead of solving [default = %s]\n", fDumpCnf? "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");
return 1;
......
src/base/abci/abcDar.c
......@@ -1562,7 +1562,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
Vec_PtrFree( vMapped );
*/
// write CNF into a file
Cnf_DataWriteIntoFile( pCnf, pFileName, 0 );
Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL );
Cnf_DataFree( pCnf );
Cnf_ManFree();
Aig_ManStop( pMan );
......
src/base/abci/abcQbf.c
......@@ -19,6 +19,7 @@
***********************************************************************/
#include "base/abc/abc.h"
#include "sat/cnf/cnf.h"
ABC_NAMESPACE_IMPL_START
......@@ -60,7 +61,7 @@ extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nI
SeeAlso []
***********************************************************************/
void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose )
void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fDumpCnf, int fVerbose )
{
Abc_Ntk_t * pNtkVer, * pNtkSyn, * pNtkSyn2, * pNtkTemp;
Vec_Int_t * vPiValues;
......@@ -74,6 +75,40 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose )
// assert( Abc_NtkPiNum(pNtk)-nPars < 32 );
nInputs = Abc_NtkPiNum(pNtk) - nPars;
Abc_ObjXorFaninC( Abc_NtkPo(pNtk,0), 0 );
if ( fDumpCnf )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pMan = Abc_NtkToDar( pNtk, 0, 0 );
Cnf_Dat_t * pCnf = Cnf_DeriveSimple( pMan, 0 );
Vec_Int_t * vVarMap, * vForAlls, * vExists;
Aig_Obj_t * pObj;
int i, Entry;
// create var map
vVarMap = Vec_IntStart( pCnf->nVars );
Aig_ManForEachCi( pMan, pObj, i )
if ( i >= nPars )
Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Aig_ObjId(pObj)], 1 );
// create various maps
vExists = Vec_IntAlloc( Abc_NtkPiNum(pNtk) - nPars );
vForAlls = Vec_IntAlloc( pCnf->nVars );
Vec_IntForEachEntry( vVarMap, Entry, i )
if ( Entry )
Vec_IntPush( vExists, i );
else
Vec_IntPush( vForAlls, i );
// generate CNF
Cnf_DataWriteIntoFile( pCnf, "test.qdimacs", 0, vForAlls, vExists );
Aig_ManStop( pMan );
Cnf_DataFree( pCnf );
Vec_IntFree( vForAlls );
Vec_IntFree( vExists );
Vec_IntFree( vVarMap );
Abc_ObjXorFaninC( Abc_NtkPo(pNtk,0), 0 );
return;
}
Abc_ObjXorFaninC( Abc_NtkPo(pNtk,0), 0 );
// initialize the synthesized network with 0000-combination
vPiValues = Vec_IntStart( Abc_NtkPiNum(pNtk) );
......
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 );
......
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++ )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment