1 files changed, 51 insertions, 10 deletions

diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c
index ce2f34b8..f6d434f8 100644
--- a/src/opt/sfm/sfmCnf.c
+++ b/src/opt/sfm/sfmCnf.c
@@ -68,24 +68,63 @@ void Sfm_PrintCnf( Vec_Str_t * vCnf )
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
+int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
 {
+    int w, nWords = Abc_Truth6WordNum( nVars );
     Vec_StrClear( vCnf );
-    if ( Truth == 0 || ~Truth == 0 )
+    if ( nVars <= 6 )
     {
-//        assert( nVars == 0 );
-        Vec_StrPush( vCnf, (char)(Truth == 0) );
-        Vec_StrPush( vCnf, (char)-1 );
-        return 1;
+        if ( Truth == 0 || ~Truth == 0 )
+        {
+            //assert( nVars == 0 );
+            Vec_StrPush( vCnf, (char)(Truth == 0) );
+            Vec_StrPush( vCnf, (char)-1 );
+            return 1;
+        }
+    }
+    else
+    {
+        // const0
+        for ( w = 0; w < nWords; w++ )
+            if ( pTruth[w] )
+                break;
+        if ( w == nWords )
+        {
+            Vec_StrPush( vCnf, (char)1 );
+            Vec_StrPush( vCnf, (char)-1 );
+            return 1;
+        }
+        // const1
+        for ( w = 0; w < nWords; w++ )
+            if ( ~pTruth[w] )
+                break;
+        if ( w == nWords )
+        {
+            Vec_StrPush( vCnf, (char)0 );
+            Vec_StrPush( vCnf, (char)-1 );
+            return 1;
+        }
     }
-    else 
     {
         int i, k, c, RetValue, Literal, Cube, nCubes = 0;
         assert( nVars > 0 );
         for ( c = 0; c < 2; c ++ )
         {
-            Truth = c ? ~Truth : Truth;
-            RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
+            if ( nVars <= 6 )
+            {
+                Truth = c ? ~Truth : Truth;
+                RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
+            }
+            else
+            {
+                if ( c )
+                    for ( k = 0; k < nWords; k++ )
+                        pTruth[k] = ~pTruth[k];
+                RetValue = Kit_TruthIsop( (unsigned *)pTruth, nVars, vCover, 0 );
+                if ( c )
+                    for ( k = 0; k < nWords; k++ )
+                        pTruth[k] = ~pTruth[k];
+            }
             assert( RetValue == 0 );
             nCubes += Vec_IntSize( vCover );
             Vec_IntForEachEntry( vCover, Cube, i )
@@ -129,7 +168,9 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
     vCnfs = Vec_WecStart( p->nObjs );
     Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
     {
-        nCubes = Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
+        int Offset  = Vec_IntEntry( p->vStarts, i );
+        word * pRes = Vec_WrdSize(p->vTruths2) ? Vec_WrdEntryP( p->vTruths2, Offset ) : NULL;
+        nCubes = Sfm_TruthToCnf( uTruth, pRes, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
         vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
         Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
         memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), (size_t)Vec_StrSize(vCnf) );