5 files changed, 28 insertions, 2 deletions
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 20d3799c..78d45b14 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -265,6 +265,9 @@ clk = clock();
         p->nNodesBad++;
         return 1;
     }
+clk = clock();
+    Abc_NtkMfsConstructGia( p );
+p->timeGia += clock() - clk;
     // solve the SAT problem
     if ( p->pPars->fPower )
         Abc_NtkMfsEdgePower( p, pNode );
@@ -277,6 +280,7 @@ clk = clock();
             Abc_NtkMfsResubNode2( p, pNode );
     }
 p->timeSat += clock() - clk;
+    Abc_NtkMfsDeconstructGia( p );
     return 1;
 }
 
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 13f0bce2..6a1d9688 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -32,6 +32,7 @@
 #include "satSolver.h"
 #include "satStore.h"
 #include "bdc.h"
+#include "gia.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -65,6 +66,12 @@ struct Mfs_Man_t_
     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;
@@ -110,6 +117,7 @@ struct Mfs_Man_t_
     int                 timeWin;
     int                 timeDiv;
     int                 timeAig;
+    int                 timeGia;
     int                 timeCnf;
     int                 timeSat;
     int                 timeInt;
@@ -155,6 +163,10 @@ extern double           Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode
 /*=== mfsWin.c ==========================================================*/
 extern Vec_Ptr_t *      Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit );
 
+/*=== mfsGia.c ==========================================================*/
+extern void             Abc_NtkMfsConstructGia( Mfs_Man_t * p );
+extern void             Abc_NtkMfsDeconstructGia( Mfs_Man_t * p );
+extern int              Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands );
 
 #ifdef __cplusplus
 }
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index e947bd52..71595f6c 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -157,15 +157,16 @@ void Mfs_ManPrint( Mfs_Man_t * p )
         printf( "Nodes resyn = %d. Ratio = %5.2f.  Total AIG node gain = %d. Timeouts = %d.\n", 
             p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts );
     }
-/*
+
     ABC_PRTP( "Win", p->timeWin            ,  p->timeTotal );
     ABC_PRTP( "Div", p->timeDiv            ,  p->timeTotal );
     ABC_PRTP( "Aig", p->timeAig            ,  p->timeTotal );
+    ABC_PRTP( "Gia", p->timeGia            ,  p->timeTotal );
     ABC_PRTP( "Cnf", p->timeCnf            ,  p->timeTotal );
     ABC_PRTP( "Sat", p->timeSat-p->timeInt ,  p->timeTotal );
     ABC_PRTP( "Int", p->timeInt            ,  p->timeTotal );
     ABC_PRTP( "ALL", p->timeTotal          ,  p->timeTotal );
-*/
+
 }
 
 /**Function*************************************************************
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 008b6863..8cd70dbf 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -99,9 +99,17 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
 {
     unsigned * pData;
     int RetValue, iVar, i;
+    int clk = clock(), RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
+p->timeGia += clock() - clk;
+
     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 );
+    if ( RetValue != l_Undef && RetValue2 != -1 )
+    {
+        assert( (RetValue == l_False) == (RetValue2 == 1) );
+    }
+
     if ( RetValue == l_False )
         return 1;
     if ( RetValue != l_True )
diff --git a/src/opt/mfs/module.make b/src/opt/mfs/module.make
index 544accec..bafc1ce5 100644
--- a/src/opt/mfs/module.make
+++ b/src/opt/mfs/module.make
@@ -1,5 +1,6 @@
 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 \