Added dumping QDIMACS files in command 'qbf'.

3 files changed, 48 insertions, 7 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) );