Cumulative changes in the last few weeks.

5 files changed, 27 insertions, 22 deletions

diff --git a/src/aig/mfx/mfxInt.h b/src/aig/mfx/mfxInt.h
index 1fcf4e91..320e7a8e 100644
--- a/src/aig/mfx/mfxInt.h
+++ b/src/aig/mfx/mfxInt.h
@@ -60,7 +60,8 @@ struct Mfx_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
diff --git a/src/aig/mfx/mfxInter.c b/src/aig/mfx/mfxInter.c
index 2263398d..db2e5e7e 100644
--- a/src/aig/mfx/mfxInter.c
+++ b/src/aig/mfx/mfxInter.c
@@ -96,13 +96,13 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int
     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();
@@ -161,7 +161,7 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int
             // 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 ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
             {
@@ -181,15 +181,17 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int
     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 ( !Mfx_SatAddXor( 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 )
@@ -242,7 +244,7 @@ unsigned * Mfx_InterplateTruth( Mfx_Man_t * p, int * pCands, int nCands, int fIn
         // 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
@@ -342,7 +344,7 @@ Hop_Obj_t * Mfx_Interplate( Mfx_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/aig/mfx/mfxMan.c b/src/aig/mfx/mfxMan.c
index 9d9994bf..ff8b02fd 100644
--- a/src/aig/mfx/mfxMan.c
+++ b/src/aig/mfx/mfxMan.c
@@ -49,7 +49,8 @@ Mfx_Man_t * Mfx_ManAlloc( Mfx_Par_t * pPars )
     p = ABC_ALLOC( Mfx_Man_t, 1 );
     memset( p, 0, sizeof(Mfx_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 + MFX_FANIN_MAX);
     p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFX_FANIN_MAX+1, p->nDivWords );
@@ -178,7 +179,8 @@ void Mfx_ManStop( Mfx_Man_t * p )
     Vec_IntFree( p->vMem );
     Vec_VecFree( p->vLevels );
     Vec_PtrFree( p->vFanins );
-    Vec_IntFree( p->vProjVars );
+    Vec_IntFree( p->vProjVarsCnf );
+    Vec_IntFree( p->vProjVarsSat );
     Vec_IntFree( p->vDivLits );
     Vec_PtrFree( p->vDivCexes );
     ABC_FREE( p );
diff --git a/src/aig/mfx/mfxResub.c b/src/aig/mfx/mfxResub.c
index 83673661..5a4786d6 100644
--- a/src/aig/mfx/mfxResub.c
+++ b/src/aig/mfx/mfxResub.c
@@ -111,7 +111,7 @@ int Mfx_TryResubOnce( Mfx_Man_t * p, int * pCands, int nCands )
     }
     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!!!
@@ -166,7 +166,7 @@ int Mfx_SolveSatResub( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int fOnlyRe
             continue;
         Vec_PtrPush( p->vFanins, pFanin );
         iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i;
-        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
     }
     RetValue = Mfx_TryResubOnce( p, pCands, nCands );
     if ( RetValue == -1 )
@@ -244,7 +244,7 @@ p->timeInt += clock() - clk;
         if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) )
             return 0;
 
-        pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
+        pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
         RetValue = Mfx_TryResubOnce( p, pCands, nCands+1 );
         if ( RetValue == -1 )
             return 0;
@@ -316,7 +316,7 @@ int Mfx_SolveSatResub2( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int iFanin
             continue;
         Vec_PtrPush( p->vFanins, pFanin );
         iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i;
-        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
     }
     RetValue = Mfx_TryResubOnce( p, pCands, nCands );
     if ( RetValue == -1 )
@@ -390,8 +390,8 @@ p->timeInt += clock() - clk;
         if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_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 = Mfx_TryResubOnce( p, pCands, nCands+2 );
         if ( RetValue == -1 )
             return 0;
diff --git a/src/aig/mfx/mfxSat.c b/src/aig/mfx/mfxSat.c
index dc4cd862..974563ab 100644
--- a/src/aig/mfx/mfxSat.c
+++ b/src/aig/mfx/mfxSat.c
@@ -58,7 +58,7 @@ int Mfx_SolveSat_iter( Mfx_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 ) )
@@ -70,7 +70,7 @@ int Mfx_SolveSat_iter( Mfx_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;
@@ -92,15 +92,15 @@ int Mfx_SolveSat( Mfx_Man_t * p, Nwk_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) - Nwk_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 );