From 7a2132b237745d04a904350424c12c2afdfd0d42 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 27 Mar 2013 17:21:08 -0700
Subject: Added dumping QDIMACS files in command 'qbf'.

---
 src/base/abci/abcQbf.c | 37 ++++++++++++++++++++++++++++++++++++-
 1 file changed, 36 insertions(+), 1 deletion(-)

(limited to 'src/base/abci/abcQbf.c')

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) );
 
-- 
cgit v1.2.3