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

4 files changed, 57 insertions, 19 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++ )