5 files changed, 55 insertions, 0 deletions

diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index 989cd718..9550a31b 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -52,6 +52,7 @@ struct Mfs_Par_t_
     int           fArea;         // performs optimization for area
     int           fMoreEffort;   // performs high-affort minimization
     int           fSwapEdge;     // performs edge swapping
+    int           fOneHotness;   // adds one-hotness conditions
     int           fDelay;        // performs optimization for delay
     int           fVerbose;      // enable basic stats
     int           fVeryVerbose;  // enable detailed stats
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 0b2ba47d..3444bab1 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -41,6 +41,7 @@
 ***********************************************************************/
 void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
 {
+    memset( pPars, 0, sizeof(Mfs_Par_t) );
     pPars->nWinTfoLevs  =    2;
     pPars->nFanoutsMax  =   10;
     pPars->nDepthMax    =   20;
@@ -52,6 +53,7 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
     pPars->fArea        =    0;
     pPars->fMoreEffort  =    0;
     pPars->fSwapEdge    =    0;
+    pPars->fOneHotness  =    0;
     pPars->fVerbose     =    0;
     pPars->fVeryVerbose =    0;
 }
@@ -155,6 +157,8 @@ p->timeCnf += clock() - clk;
     // create the SAT problem
 clk = clock();
     p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
+    if ( p->pSat && p->pPars->fOneHotness )
+        Abc_NtkAddOneHotness( p );
     if ( p->pSat == NULL )
         return 0;
     // solve the SAT problem
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 37521189..df8a4848 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -141,6 +141,7 @@ extern int              Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode );
 extern int              Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsSat.c ==========================================================*/
 extern int              Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern int              Abc_NtkAddOneHotness( Mfs_Man_t * p );
 /*=== mfsStrash.c ==========================================================*/
 extern Aig_Man_t *      Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode );
 extern double           Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode );
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 5944fd5b..6e50d444 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -123,6 +123,15 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
         return NULL;
     }
 
+    // add one-hotness constraints
+    if ( p->pPars->fOneHotness )
+    {
+        p->pSat = pSat;
+        if ( !Abc_NtkAddOneHotness( p ) )
+            return NULL;
+        p->pSat = NULL;
+    }
+
     // bookmark the clauses of A
     if ( pCands )
         sat_solver_store_mark_clauses_a( pSat );
@@ -139,6 +148,14 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
             return NULL;
         }
     }
+    // add one-hotness constraints
+    if ( p->pPars->fOneHotness )
+    {
+        p->pSat = pSat;
+        if ( !Abc_NtkAddOneHotness( p ) )
+            return NULL;
+        p->pSat = NULL;
+    }
     // transform the literals
     for ( i = 0; i < p->pCnf->nLiterals; i++ )
         p->pCnf->pClauses[0][i] -= 2 * p->pCnf->nVars;
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index 5023bf62..6cc0f0fd 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -133,6 +133,38 @@ int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Adds one-hotness constraints for the window inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+int Abc_NtkAddOneHotness( Mfs_Man_t * p )
+{
+    Aig_Obj_t * pObj1, * pObj2;
+    int i, k, Lits[2];
+    for ( i = 0; i < Vec_PtrSize(p->pAigWin->vPis); i++ )
+    for ( k = i+1; k < Vec_PtrSize(p->pAigWin->vPis); k++ )
+    {
+        pObj1 = Aig_ManPi( p->pAigWin, i );
+        pObj2 = Aig_ManPi( p->pAigWin, k );
+        Lits[0] = toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 );
+        Lits[1] = toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 );
+        if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
+        {
+            sat_solver_delete( p->pSat );
+            p->pSat = NULL;
+            return 0;
+        }
+    }
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////