Added dumping QDIMACS files in command 'qbf'.

5 files changed, 82 insertions, 13 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index cd77c98d..fa160963 100644
--- a/src/base/abci/abc.c
+++ b/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;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 933bab87..28b95b95 100644
--- a/src/base/abci/abcDar.c
+++ b/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 );
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c
index abbcc172..0731d23f 100644
--- a/src/base/abci/abcQbf.c
+++ b/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) );
 
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++ )