Cumulative changes in the last few weeks.

8 files changed, 55 insertions, 49 deletions

diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index bda95d55..72774730 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -268,10 +268,10 @@ clk = clock();
         p->nNodesBad++;
         return 1;
     }
-clk = clock();
-    if ( p->pPars->fGiaSat )
-        Abc_NtkMfsConstructGia( p );
-p->timeGia += clock() - clk;
+//clk = clock();
+//    if ( p->pPars->fGiaSat )
+//        Abc_NtkMfsConstructGia( p );
+//p->timeGia += clock() - clk;
     // solve the SAT problem
     if ( p->pPars->fPower )
         Abc_NtkMfsEdgePower( p, pNode );
@@ -284,8 +284,8 @@ p->timeGia += clock() - clk;
             Abc_NtkMfsResubNode2( p, pNode );
     }
 p->timeSat += clock() - clk;
-    if ( p->pPars->fGiaSat )
-        Abc_NtkMfsDeconstructGia( p );
+//    if ( p->pPars->fGiaSat )
+//        Abc_NtkMfsDeconstructGia( p );
     return 1;
 }
 
diff --git a/src/opt/mfs/mfsGia.c b/src/opt/mfs/mfsGia.c
index 016b4ae2..af6cc159 100644
--- a/src/opt/mfs/mfsGia.c
+++ b/src/opt/mfs/mfsGia.c
@@ -271,7 +271,7 @@ int Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands )
             assert( Val3 == 1 );
 */
             // store the counter-example
-            Vec_IntForEachEntry( p->vProjVars, iVar, i )
+            Vec_IntForEachEntry( p->vProjVarsSat, iVar, i )
             {
                 pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
                 iOut = iVar - 2 * p->pCnf->nVars;
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 5611afa0..28a68bd8 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -61,19 +61,22 @@ struct Mfs_Man_t_
     Vec_Ptr_t *         vNodes;    // the internal nodes of the window
     Vec_Ptr_t *         vDivs;     // the divisors of the node
     Vec_Int_t *         vDivLits;  // the SAT literals of divisor nodes
-    Vec_Int_t *         vProjVars; // the projection variables
+    Vec_Int_t *         vProjVarsCnf; // the projection variables
+    Vec_Int_t *         vProjVarsSat; // the projection variables
     // intermediate simulation data
     Vec_Ptr_t *         vDivCexes; // the counter-example for dividors
     int                 nDivWords; // the number of words
     int                 nCexes;    // the numbe rof current counter-examples
     int                 nSatCalls; 
     int                 nSatCexes;
+/*
     // intermediate AIG data
     Gia_Man_t *         pGia;      // replica of the AIG in the new package
 //    Gia_Obj_t **        pSat2Gia;  // mapping of PO SAT var into internal GIA nodes
     Tas_Man_t *         pTas;      // the SAT solver
     Vec_Int_t *         vCex;      // the counter-example
     Vec_Ptr_t *         vGiaLits;  // literals given as assumptions
+*/
     // used for bidecomposition
     Vec_Int_t *         vTruth;
     Bdc_Man_t *         pManDec;
@@ -87,7 +90,7 @@ struct Mfs_Man_t_
     Int_Man_t *         pMan;      // interpolation manager;
     Vec_Int_t *         vMem;      // memory for intermediate SOPs
     Vec_Vec_t *         vLevels;   // levelized structure for updating
-    Vec_Ptr_t *         vFanins;   // the new set of fanins
+    Vec_Ptr_t *         vMfsFanins;   // the new set of fanins
     int                 nTotConfLim; // total conflict limit
     int                 nTotConfLevel; // total conflicts on this level
     // switching activity
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 1b3f2415..0934513b 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -96,13 +96,13 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
     Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert );
 
     // collect the outputs of the divisors
-    Vec_IntClear( p->vProjVars );
+    Vec_IntClear( p->vProjVarsCnf );
     Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
     {
         assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
-        Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
+        Vec_IntPush( p->vProjVarsCnf, p->pCnf->pVarNums[pObjPo->Id] );
     }
-    assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) );
+    assert( Vec_IntSize(p->vProjVarsCnf) == Vec_PtrSize(p->vDivs) );
 
     // start the solver
     pSat = sat_solver_new();
@@ -178,7 +178,7 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
             // get the variable number of this divisor
             i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
             // get the corresponding SAT variable
-            iVar = Vec_IntEntry( p->vProjVars, i );
+            iVar = Vec_IntEntry( p->vProjVarsCnf, i );
             // add the corresponding EXOR gate
             if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
             {
@@ -198,15 +198,17 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
     else
     {
         // add the clauses for the EXOR gates - and remember their outputs
-        Vec_IntForEachEntry( p->vProjVars, iVar, i )
+        Vec_IntClear( p->vProjVarsSat );
+        Vec_IntForEachEntry( p->vProjVarsCnf, iVar, i )
         {
             if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
             {
                 sat_solver_delete( pSat );
                 return NULL;
             }
-            Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i );
+            Vec_IntPush( p->vProjVarsSat, 2 * p->pCnf->nVars + i );
         }
+        assert( Vec_IntSize(p->vProjVarsCnf) == Vec_IntSize(p->vProjVarsSat) );
         // simplify the solver
         status = sat_solver_simplify(pSat);
         if ( status == 0 )
@@ -259,7 +261,7 @@ unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, i
         // get the variable number of this divisor
         i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
         // get the corresponding SAT variable
-        pGloVars[c] = Vec_IntEntry( p->vProjVars, i );
+        pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i );
     }
 
     // derive the interpolant
@@ -362,7 +364,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
         // get the variable number of this divisor
         i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
         // get the corresponding SAT variable
-        pGloVars[c] = Vec_IntEntry( p->vProjVars, i );
+        pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i );
     }
 
     // derive the interpolant
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 74889c45..df331b43 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -49,14 +49,15 @@ Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars )
     p = ABC_ALLOC( Mfs_Man_t, 1 );
     memset( p, 0, sizeof(Mfs_Man_t) );
     p->pPars     = pPars;
-    p->vProjVars = Vec_IntAlloc( 100 );
+    p->vProjVarsCnf = Vec_IntAlloc( 100 );
+    p->vProjVarsSat = Vec_IntAlloc( 100 );
     p->vDivLits  = Vec_IntAlloc( 100 );
     p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX);
     p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords );
     p->pMan      = Int_ManAlloc();
     p->vMem      = Vec_IntAlloc( 0 );
     p->vLevels   = Vec_VecStart( 32 );
-    p->vFanins   = Vec_PtrAlloc( 32 );
+    p->vMfsFanins= Vec_PtrAlloc( 32 );
     return p;
 }
 
@@ -201,8 +202,9 @@ void Mfs_ManStop( Mfs_Man_t * p )
     Int_ManFree( p->pMan );
     Vec_IntFree( p->vMem );
     Vec_VecFree( p->vLevels );
-    Vec_PtrFree( p->vFanins );
-    Vec_IntFree( p->vProjVars );
+    Vec_PtrFree( p->vMfsFanins );
+    Vec_IntFree( p->vProjVarsCnf );
+    Vec_IntFree( p->vProjVarsSat );
     Vec_IntFree( p->vDivLits );
     Vec_PtrFree( p->vDivCexes );
     ABC_FREE( p );
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 38004089..40cb6198 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -42,14 +42,14 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc )
+void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vMfsFanins, Hop_Obj_t * pFunc )
 {
     Abc_Obj_t * pObjNew, * pFanin;
     int k;
     // create the new node
     pObjNew = Abc_NtkCreateNode( pObj->pNtk );
     pObjNew->pData = pFunc;
-    Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pFanin, k )
+    Vec_PtrForEachEntry( Abc_Obj_t *, vMfsFanins, pFanin, k )
         Abc_ObjAddFanin( pObjNew, pFanin );
     // replace the old node by the new node
 //printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
@@ -103,14 +103,14 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
     int fVeryVerbose = 0;
     unsigned * pData;
     int RetValue, RetValue2 = -1, iVar, i, clk = clock();
-
+/*
     if ( p->pPars->fGiaSat )
     {
         RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
 p->timeGia += clock() - clk;
         return RetValue2;
     }
- 
+*/ 
     p->nSatCalls++;
     RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 //    assert( RetValue == l_False || RetValue == l_True );
@@ -137,7 +137,7 @@ p->timeGia += clock() - clk;
     printf( "S " );
     p->nSatCexes++;
     // store the counter-example
-    Vec_IntForEachEntry( p->vProjVars, iVar, i )
+    Vec_IntForEachEntry( p->vProjVarsSat, iVar, i )
     {
         pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
         if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
@@ -186,14 +186,14 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
 
     // try fanins without the critical fanin
     nCands = 0;
-    Vec_PtrClear( p->vFanins );
+    Vec_PtrClear( p->vMfsFanins );
     Abc_ObjForEachFanin( pNode, pFanin, i )
     {
         if ( i == iFanin )
             continue;
-        Vec_PtrPush( p->vFanins, pFanin );
+        Vec_PtrPush( p->vMfsFanins, pFanin );
         iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
-        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
     }
     RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
     if ( RetValue == -1 )
@@ -212,7 +212,7 @@ clk = clock();
         if ( pFunc == NULL )
             return 0;
         // update the network
-        Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+        Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
 p->timeInt += clock() - clk;
         return 1;
     }
@@ -269,7 +269,7 @@ p->timeInt += clock() - clk;
         if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
             return 0;
 
-        pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
+        pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
         RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 );
         if ( RetValue == -1 )
             return 0;
@@ -287,8 +287,8 @@ clk = clock();
             if ( pFunc == NULL )
                 return 0;
             // update the network
-            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
-            Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+            Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
+            Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
 p->timeInt += clock() - clk;
             return 1;
         }
@@ -334,14 +334,14 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
 
     // try fanins without the critical fanin
     nCands = 0;
-    Vec_PtrClear( p->vFanins );
+    Vec_PtrClear( p->vMfsFanins );
     Abc_ObjForEachFanin( pNode, pFanin, i )
     {
         if ( i == iFanin || i == iFanin2 )
             continue;
-        Vec_PtrPush( p->vFanins, pFanin );
+        Vec_PtrPush( p->vMfsFanins, pFanin );
         iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
-        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
     }
     RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
     if ( RetValue == -1 )
@@ -358,7 +358,7 @@ clk = clock();
         if ( pFunc == NULL )
             return 0;
         // update the network
-        Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+        Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
 p->timeInt += clock() - clk;
         return 1;
     }
@@ -435,8 +435,8 @@ p->timeInt += clock() - clk;
         if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
             return 0;
 
-        pCands[nCands]   = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 );
-        pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
+        pCands[nCands]   = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar2), 1 );
+        pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
         RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 );
         if ( RetValue == -1 )
             return 0;
@@ -452,10 +452,10 @@ clk = clock();
             if ( pFunc == NULL )
                 return 0;
             // update the network
-            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar2) );
-            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
-            assert( Vec_PtrSize(p->vFanins) == nCands + 2 );
-            Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+            Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar2) );
+            Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
+            assert( Vec_PtrSize(p->vMfsFanins) == nCands + 2 );
+            Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
 p->timeInt += clock() - clk;
             return 1;
         }
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index c5806f2a..37ee2b39 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -63,7 +63,7 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
     p->nCares++;
     // add SAT assignment to the solver
     Mint = 0;
-    Vec_IntForEachEntry( p->vProjVars, iVar, b )
+    Vec_IntForEachEntry( p->vProjVarsSat, iVar, b )
     {
         Lits[b] = toLit( iVar );
         if ( sat_solver_var_value( p->pSat, iVar ) )
@@ -75,7 +75,7 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
     assert( !Aig_InfoHasBit(p->uCare, Mint) );
     Aig_InfoSetBit( p->uCare, Mint );
     // add the blocking clause
-    RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) );
+    RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVarsSat) );
     if ( RetValue == 0 )
         return 0;
     return 1;
@@ -97,15 +97,15 @@ int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
     Aig_Obj_t * pObjPo;
     int RetValue, i;
     // collect projection variables
-    Vec_IntClear( p->vProjVars );
+    Vec_IntClear( p->vProjVarsSat );
     Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) )
     {
         assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
-        Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
+        Vec_IntPush( p->vProjVarsSat, p->pCnf->pVarNums[pObjPo->Id] );
     }
 
     // prepare the truth table of care set
-    p->nFanins = Vec_IntSize( p->vProjVars );
+    p->nFanins = Vec_IntSize( p->vProjVarsSat );
     p->nWords = Aig_TruthWordNum( p->nFanins );
     memset( p->uCare, 0, sizeof(unsigned) * p->nWords );
 
diff --git a/src/opt/mfs/module.make b/src/opt/mfs/module.make
index bafc1ce5..544accec 100644
--- a/src/opt/mfs/module.make
+++ b/src/opt/mfs/module.make
@@ -1,6 +1,5 @@
 SRC +=  src/opt/mfs/mfsCore.c \
     src/opt/mfs/mfsDiv.c \
-    src/opt/mfs/mfsGia.c \
     src/opt/mfs/mfsInter.c \
     src/opt/mfs/mfsMan.c \
     src/opt/mfs/mfsResub.c \