Standardizing the use of new CNF generator. Adding CNF variable connectivity information.

17 files changed, 76 insertions, 57 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 3bc97e6b..6677e0ad 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -311,6 +311,7 @@ struct Jf_Par_t_
     int            fGenCnf;
     int            fCnfObjIds;
     int            fAddOrCla;
+    int            fCnfMapping;
     int            fPureAig;
     int            fDoAverage;
     int            fCutHashing;
@@ -1405,6 +1406,7 @@ extern int                 Gia_MmStepReadMemUsage( Gia_MmStep_t * p );
 /*=== giaMf.c ===========================================================*/
 extern void                Mf_ManSetDefaultPars( Jf_Par_t * pPars );
 extern Gia_Man_t *         Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );
+extern void *              Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose );
 /*=== giaMini.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManReadMiniAig( char * pFileName );
 extern void                Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName );
diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c
index a500a839..24c1e6a0 100644
--- a/src/aig/gia/giaMf.c
+++ b/src/aig/gia/giaMf.c
@@ -388,6 +388,8 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla )
         Gia_ManForEachCoId( p->pGia, Id, i )
             pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], 0);
     }
+    if ( p->pPars->fCnfMapping )
+        pCnf->vMapping = Vec_IntStart( nVars );
     // add clauses for the COs
     Gia_ManForEachCo( p->pGia, pObj, i )
     {
@@ -401,6 +403,14 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla )
         pCnf->pClauses[iCla++] = pCnf->pClauses[0] + iLit;
         pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], 1);
         pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[DriId], Gia_ObjFaninC0(pObj));
+        // generate mapping
+        if ( pCnf->vMapping )
+        {
+            Vec_IntWriteEntry( pCnf->vMapping, pCnfIds[Id], Vec_IntSize(pCnf->vMapping) );
+            Vec_IntPush( pCnf->vMapping, 1 );
+            Vec_IntPush( pCnf->vMapping, pCnfIds[DriId] );
+            Vec_IntPush( pCnf->vMapping, Gia_ObjFaninC0(pObj) ? 0x55555555 : 0xAAAAAAAA );
+        }
     }
     // add clauses for the mapping
     Gia_ManForEachAndReverseId( p->pGia, Id )
@@ -427,6 +437,35 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla )
                 if ( Mf_CubeLit(pCubes[c], k) )
                     pCnf->pClauses[0][iLit++] = Abc_Var2Lit( pFanins[k], Mf_CubeLit(pCubes[c], k) == 2 );
         }
+        // generate mapping
+        if ( pCnf->vMapping )
+        {
+            word pTruth[4], * pTruthP = Vec_MemReadEntry(p->vTtMem, iFunc);
+            assert( p->pPars->nLutSize <= 8 );
+            Abc_TtCopy( pTruth, pTruthP, Abc_Truth6WordNum(p->pPars->nLutSize), Abc_LitIsCompl(iFunc) );
+            assert( pCnfIds[Id] >= 0 && pCnfIds[Id] < nVars );
+            Vec_IntWriteEntry( pCnf->vMapping, pCnfIds[Id], Vec_IntSize(pCnf->vMapping) );
+            Vec_IntPush( pCnf->vMapping, Mf_CutSize(pCut) );
+            for ( k = 0; k < Mf_CutSize(pCut); k++ )
+                Vec_IntPush( pCnf->vMapping, pCnfIds[pCut[k+1]] );
+            Vec_IntPush( pCnf->vMapping, (unsigned)pTruth[0] );
+            if ( Mf_CutSize(pCut) >= 6 )
+            {
+                Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[0] >> 32) );
+                if ( Mf_CutSize(pCut) >= 7 )
+                {
+                    Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[1]) );
+                    Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[1] >> 32) );
+                }
+                if ( Mf_CutSize(pCut) >= 8 )
+                {
+                    Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[2]) );
+                    Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[2] >> 32) );
+                    Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[3]) );
+                    Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[3] >> 32) );
+                }
+            }
+        }
     }
     // constant clause
     pCnf->pClauses[iCla++] = pCnf->pClauses[0] + iLit;
@@ -1636,28 +1675,29 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose )
+void * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose )
 {
     Gia_Man_t * pNew;
     Jf_Par_t Pars, * pPars = &Pars;
     assert( nLutSize >= 3 && nLutSize <= 8 );
     Mf_ManSetDefaultPars( pPars );
-    pPars->fGenCnf    = 1;
-    pPars->fCoarsen   = !fCnfObjIds;
-    pPars->nLutSize   = nLutSize;
-    pPars->fCnfObjIds = fCnfObjIds;
-    pPars->fAddOrCla  = fAddOrCla;
-    pPars->fVerbose   = fVerbose;
+    pPars->fGenCnf     = 1;
+    pPars->fCoarsen    = !fCnfObjIds;
+    pPars->nLutSize    = nLutSize;
+    pPars->fCnfObjIds  = fCnfObjIds;
+    pPars->fAddOrCla   = fAddOrCla;
+    pPars->fCnfMapping = fMapping;
+    pPars->fVerbose    = fVerbose;
     pNew = Mf_ManPerformMapping( pGia, pPars );
     Gia_ManStopP( &pNew );
 //    Cnf_DataPrint( (Cnf_Dat_t *)pGia->pData, 1 );
-    return (Cnf_Dat_t*)pGia->pData;
+    return pGia->pData;
 }
 void Mf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose )
 {
     abctime clk = Abc_Clock();
     Cnf_Dat_t * pCnf;
-    pCnf = Mf_ManGenerateCnf( p, nLutSize, fCnfObjIds, fAddOrCla, fVerbose );
+    pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, nLutSize, fCnfObjIds, fAddOrCla, 0, fVerbose );
     Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL );
 //    if ( fVerbose )
     {
diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c
index 4ca0bac3..2dfd83fc 100644
--- a/src/aig/gia/giaQbf.c
+++ b/src/aig/gia/giaQbf.c
@@ -48,8 +48,6 @@ struct Qbf_Man_t_
     abctime         clkSat;         // SAT solver time
 };
 
-extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -192,7 +190,7 @@ int Gia_ManSatEnum( Gia_Man_t * pGia, int nConfLimit, int nTimeOut, int fVerbose
     int i, iLit, iParVarBeg, Iter;
     int nSolutions = 0, RetValue = 0;
     abctime clkStart = Abc_Clock();
-    pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
+    pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 );
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1;
     Cnf_DataFree( pCnf );
@@ -247,7 +245,7 @@ void Gia_QbfDumpFile( 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 = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 );
     Vec_Int_t * vVarMap, * vForAlls, * vExists;
     Gia_Obj_t * pObj;
     char * pFileName;
@@ -291,7 +289,7 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose )
     Qbf_Man_t * p;
     Cnf_Dat_t * pCnf;
     Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) );
-    pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
+    pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 );
     Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) );
     p = ABC_CALLOC( Qbf_Man_t, 1 );
     p->clkStart   = Abc_Clock();
@@ -426,7 +424,7 @@ Gia_Man_t * Gia_QbfCofactor( Gia_Man_t * p, int nPars, Vec_Int_t * vValues, Vec_
 /*
 int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof )
 {
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 1, 0, 0 );
     int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof);// - 1;
     pCnf->pMan = NULL;
     Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) );
@@ -459,7 +457,7 @@ void Cnf_SpecialDataLift( Cnf_Dat_t * p, int nVarsPlus, int firstPiVar, int last
 
 int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof )
 {
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 1, 0, 0 );
     int i, useold = 0;
     int iFirstVar = useold ? sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) : pCnf->nVars - Gia_ManPiNum(pCof); //-1   
     pCnf->pMan = NULL;
diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c
index fc8e5c28..db81bd85 100644
--- a/src/aig/gia/giaSatoko.c
+++ b/src/aig/gia/giaSatoko.c
@@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -50,7 +48,7 @@ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfOb
 satoko_t * Gia_ManCreateSatoko( Gia_Man_t * p )
 {
     satoko_t * pSat = satoko_create();
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 1, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 );
     int i, status;
     //sat_solver_setnvars( pSat, p->nVars );
     for ( i = 0; i < pCnf->nClauses; i++ )
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index 8c2b3b39..1542c25a 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -537,8 +537,6 @@ extern Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose );
 extern int         Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps );
 extern Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose );
 
-extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-
 /**Function*************************************************************
 
   Synopsis    [Derives GIA for the network.]
@@ -802,7 +800,7 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
     if ( fCnfShared )
     {
         vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
-        pCnf = Mf_ManGenerateCnf( p, 8, 1, 0, 0 );
+        pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 1, 0, 0, 0 );
     }
     vSopsRepr = Vec_PtrStart( Vec_IntSize(vReprs) );
     pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) );
diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c
index 8b8bba64..7adbed5d 100644
--- a/src/base/abci/abcDetect.c
+++ b/src/base/abci/abcDetect.c
@@ -901,8 +901,7 @@ Vec_Int_t * Abc_NtkFinCheckPair( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t
     }
     else
     {
-        extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-        Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
+        Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 );
         sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
         if ( pSat == NULL )
         {
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index f7e45c57..be6df65f 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -225,8 +225,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
 ***********************************************************************/
 int Cec_ManVerifyNaive( Gia_Man_t * p, Cec_ParCec_t * pPars )
 {
-    extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     Gia_Obj_t * pObj0, * pObj1;
     abctime clkStart = Abc_Clock();
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 95adb10c..fe759fff 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -626,8 +626,6 @@ Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
 ***********************************************************************/
 #define Pdr_ForEachCube( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 1 )
 
-extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-
 Vec_Int_t * Pdr_InvMap( Vec_Int_t * vCounts )
 {
     int i, k = 0, Count;
@@ -779,7 +777,7 @@ int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver
 int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
 {
     int RetValue;
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     assert( sat_solver_nvars(pSat) == pCnf->nVars );
     Cnf_DataFree( pCnf );
@@ -796,7 +794,7 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
     int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0; 
     Vec_Int_t * vRes = NULL;
     // create SAT solver
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0];
     // create variables
@@ -914,7 +912,7 @@ Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
     Vec_Int_t * vRes = NULL;
     abctime clk = Abc_Clock();
     int i, k, nLits = 0, * pCube, * pList = Vec_IntArray(vInv), nRemoved = 0;
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     sat_solver * pSat;
 //    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     Pdr_ForEachCube( pList, pCube, i )
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index 8087046a..3490d34f 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -986,8 +986,7 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
     {
 //        p->pFrames = Jf_ManDeriveCnf( pTemp = p->pFrames, 1 );  Gia_ManStop( pTemp );
 //        p->pCnf = (Cnf_Dat_t *)p->pFrames->pData; p->pFrames->pData = NULL;
-        extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-        p->pCnf = Mf_ManGenerateCnf( p->pFrames, pPars->nLutSize, 1, 0, pPars->fVerbose );
+        p->pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p->pFrames, pPars->nLutSize, 1, 0, 0, pPars->fVerbose );
     }
     Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
     // create clauses for constant node
diff --git a/src/sat/bmc/bmcChain.c b/src/sat/bmc/bmcChain.c
index 324c7f6d..5af54306 100644
--- a/src/sat/bmc/bmcChain.c
+++ b/src/sat/bmc/bmcChain.c
@@ -185,10 +185,9 @@ Gia_Man_t * Gia_ManDupPosAndPropagateInit( Gia_Man_t * p )
 }
 sat_solver * Gia_ManDeriveSatSolver( Gia_Man_t * p, Vec_Int_t * vSatIds )
 {
-//    extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
     sat_solver * pSat;
     Aig_Man_t * pAig = Gia_ManToAigSimple( p );
-//    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+//    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     Cnf_Dat_t * pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
     // save SAT vars for the primary inputs
     if ( vSatIds )
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c
index 8a69fe56..cfc608b1 100644
--- a/src/sat/bmc/bmcClp.c
+++ b/src/sat/bmc/bmcClp.c
@@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -651,7 +649,7 @@ Vec_Str_t * Bmc_CollapseOneInt2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int
     int iOut = 0, iLit, iVar, status, n, Count, Start;
 
     // create SAT solver
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     sat_solver * pSat[3] = { 
         (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), 
         (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0),
@@ -841,7 +839,7 @@ Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
 {
     int fVeryVerbose = fVerbose;
     int nVars = Gia_ManCiNum(p);
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     sat_solver * pSat[2]      = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) };
     sat_solver * pSatClean[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) };
     Vec_Str_t * vSop[2]   = { Vec_StrAlloc(1000),  Vec_StrAlloc(1000)  }, * vRes = NULL;
@@ -1173,7 +1171,7 @@ cleanup:
 }
 Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
 {
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     sat_solver * pSat0 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
     sat_solver * pSat1 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
     sat_solver * pSat2 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
@@ -1507,7 +1505,7 @@ cleanup:
 }
 Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
 {
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
     Vec_Str_t * vSop = Bmc_CollapseOne_int( pSat, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
     sat_solver_delete( pSat );
diff --git a/src/sat/bmc/bmcEnum.c b/src/sat/bmc/bmcEnum.c
index 5fe2c1ed..45aeb2b3 100644
--- a/src/sat/bmc/bmcEnum.c
+++ b/src/sat/bmc/bmcEnum.c
@@ -29,8 +29,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -169,7 +167,7 @@ void Gia_ManDeriveOneTest( Gia_Man_t * p )
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj, * pRoot;
     Vec_Int_t * vValues = Vec_IntStart( Gia_ManCiNum(p) );
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     int i, iVar, nIter, iPoVarBeg = pCnf->nVars - Gia_ManCiNum(p);
     sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     Vec_Int_t * vLits = Vec_IntAlloc( 100 );
diff --git a/src/sat/bmc/bmcExpand.c b/src/sat/bmc/bmcExpand.c
index f3ec999e..6c7a5988 100644
--- a/src/sat/bmc/bmcExpand.c
+++ b/src/sat/bmc/bmcExpand.c
@@ -33,8 +33,6 @@ ABC_NAMESPACE_IMPL_START
 // iterator thought the cubes
 #define Bmc_SopForEachCube( pSop, nVars, pCube )  for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )
 
-extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -93,7 +91,7 @@ int Abc_ObjExpandCubes( Vec_Str_t * vSop, Gia_Man_t * p, int nVars )
 
     int fReverse = 0;
     Vec_Int_t * vVars = Vec_IntAlloc( nVars );
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
     int v, n, iLit, status, nCubesNew, iCiVarBeg = sat_solver_nvars(pSat) - nVars;
 
diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index 8dc2a57f..71eef2c4 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -280,7 +280,7 @@ static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
     pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
     Aig_ManStop( pAig );
     return pCnf;
-//    return Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+//    return (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
 }
 
 /**Function*************************************************************
diff --git a/src/sat/bmc/bmcFx.c b/src/sat/bmc/bmcFx.c
index 9cd37c88..15ea4f05 100644
--- a/src/sat/bmc/bmcFx.c
+++ b/src/sat/bmc/bmcFx.c
@@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -598,7 +596,7 @@ int Bmc_FxCompute( Gia_Man_t * p )
     extern Gia_Man_t * Gia_ManDupOnsetOffset( Gia_Man_t * p );
     Gia_Man_t * p2 = Gia_ManDupOnsetOffset( p );
     // create SAT solver
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p2, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p2, 8, 0, 0, 0, 0 );
     sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     // compute parameters
     int nOuts = Gia_ManCoNum(p);
@@ -674,7 +672,7 @@ int Bmc_FxComputeOne( Gia_Man_t * p, int nIterMax, int nDiv2Add )
 {
     int Extra    = 1000;
     // create SAT solver
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     // compute parameters
     int nCiVars   = Gia_ManCiNum(p);             // PI count
diff --git a/src/sat/bmc/bmcGen.c b/src/sat/bmc/bmcGen.c
index 74af1b78..5d84ce87 100644
--- a/src/sat/bmc/bmcGen.c
+++ b/src/sat/bmc/bmcGen.c
@@ -29,8 +29,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -131,7 +129,7 @@ void Gia_ManMoFindSimulate( Gia_Man_t * p, int nWords )
 int Gia_ManTestSatEnum( Gia_Man_t * p )
 {
     abctime clk = Abc_Clock(), clk2, clkTotal = 0;
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
     sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
     int i, v, status, iLit, nWords = 1, iOutVar = 1, Count = 0;
     Vec_Int_t * vVars = Vec_IntAlloc( 1000 );
diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c
index a779b1ed..8d8c7c6b 100644
--- a/src/sat/bmc/bmcICheck.c
+++ b/src/sat/bmc/bmcICheck.c
@@ -392,11 +392,10 @@ int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRev
         pCnf = Cnf_DeriveGiaRemapped( pMiter );
     else
     {
-        extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
         //pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
         //Gia_ManStop( pTemp );
         //pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
-        pCnf = Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0 );
+        pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0, 0 );
     }
 /*
     // collect positive literals