From ea0f22de4dad98bec0fef7e0ee4332bab8d26bc1 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 8 Feb 2023 00:25:17 -0800
Subject: [PATCH] Bug fix in &mfs.

---
 src/opt/sfm/sfmCnf.c  | 5 ++++-
 src/opt/sfm/sfmCore.c | 8 +++++---
 src/opt/sfm/sfmNtk.c  | 2 +-
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c
index f6d434f85..e3af7e011 100644
--- a/src/opt/sfm/sfmCnf.c
+++ b/src/opt/sfm/sfmCnf.c
@@ -76,7 +76,7 @@ int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Ve
     {
         if ( Truth == 0 || ~Truth == 0 )
         {
-            //assert( nVars == 0 );
+            assert( nVars == 0 );
             Vec_StrPush( vCnf, (char)(Truth == 0) );
             Vec_StrPush( vCnf, (char)-1 );
             return 1;
@@ -92,6 +92,7 @@ int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Ve
         {
             Vec_StrPush( vCnf, (char)1 );
             Vec_StrPush( vCnf, (char)-1 );
+            assert( 0 );
             return 1;
         }
         // const1
@@ -102,6 +103,7 @@ int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Ve
         {
             Vec_StrPush( vCnf, (char)0 );
             Vec_StrPush( vCnf, (char)-1 );
+            assert( 0 );
             return 1;
         }
     }
@@ -196,6 +198,7 @@ void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap
     Vec_Int_t * vClause;
     signed char Entry;
     int i, Lit;
+    assert( Vec_StrEntry(vCnf, 1) != -1 || Vec_IntSize(vFaninMap) == 1 );
     Vec_WecClear( vRes );
     vClause = Vec_WecPushLevel( vRes );
     Vec_StrForEachEntry( vCnf, Entry, i )
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 571a35ec8..f363e1cb0 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -218,7 +218,9 @@ finish:
     Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth, p->pTruth );
     // the number of fanins cannot increase
     assert( nFanins >= Sfm_ObjFaninNum(p, iNode) );
-    //printf( "Modifying node %d with %d fanins (resulting in %d fanins).\n", iNode, nFanins, Sfm_ObjFaninNum(p, iNode) );
+    //printf( "Modifying node %d with %d fanins (resulting in %d fanins).  ", iNode, nFanins, Sfm_ObjFaninNum(p, iNode) );
+    //Abc_TtPrintHexRev( stdout, p->pTruth, Sfm_ObjFaninNum(p, iNode) );
+    //printf( "\n" );
     return 1;
 }
 
@@ -386,8 +388,8 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
             continue;
         if ( p->pPars->nDepthMax && Sfm_ObjLevel(p, i) > p->pPars->nDepthMax )
             continue;
-        if ( Sfm_ObjFaninNum(p, i) < 2 )
-            continue;
+        //if ( Sfm_ObjFaninNum(p, i) < 2 )
+        //    continue;
         if ( Sfm_ObjFaninNum(p, i) > SFM_SUPP_MAX )
         {
             CounterLarge++;
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 2d6b928b9..70afd91aa 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -322,7 +322,7 @@ void Sfm_NtkUpdateLevelR_rec( Sfm_Ntk_t * p, int iNode )
 void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth, word * pTruth )
 {
     int iFanin = Sfm_ObjFanin( p, iNode, f );
-    int nWords = Abc_Truth6WordNum( Sfm_ObjFaninNum(p, iNode) );
+    int nWords = Abc_Truth6WordNum( Sfm_ObjFaninNum(p, iNode) - (int)(iFaninNew == -1) );
     assert( Sfm_ObjIsNode(p, iNode) );
     assert( iFanin != iFaninNew );
     assert( Sfm_ObjFaninNum(p, iNode) <= SFM_FANIN_MAX );