Fixing big-endian problems in mfs2 and &mfs.

berkeley-abc · Dec 24, 2024 · 733fec3 · 733fec3
1 parent cc894c5
commit 733fec3
Show file tree

Hide file tree

Showing 7 changed files with 41 additions and 6 deletions.
diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c
@@ -395,15 +395,21 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
                 int nVarsNew;
                 Abc_TtSimplify( pTruth, Vec_IntArray(vLeaves), Vec_IntSize(vLeaves), &nVarsNew );
                 Vec_IntShrink( vLeaves, nVarsNew );
+                Abc_TtFlipVar5( pTruth, Vec_IntSize(vLeaves) );
                 iLitNew = Gia_ManFromIfLogicCreateLut( pNew, pTruth, vLeaves, vCover, vMapping, vMapping2 );
+                Abc_TtFlipVar5( pTruth, Vec_IntSize(vLeaves) );
                 if ( MapSize < Vec_IntSize(vMapping2) )
                 {
                     assert( Vec_IntEntryLast(vMapping2) == Abc_Lit2Var(iLitNew) );
                     Vec_IntWriteEntry(vMapping2, Vec_IntSize(vMapping2)-1, -Abc_Lit2Var(iLitNew) );
                 }
             }
             else
+            {
+                Abc_TtFlipVar5( pTruth, Vec_IntSize(vLeaves) );
                 iLitNew = Gia_ManFromIfLogicCreateLut( pNew, pTruth, vLeaves, vCover, vMapping, vMapping2 );
+                Abc_TtFlipVar5( pTruth, Vec_IntSize(vLeaves) );
+            }
         }
         else if ( Abc_LitIsCompl(iGroup) ) // internal CI
         {

diff --git a/src/aig/gia/giaTruth.c b/src/aig/gia/giaTruth.c
@@ -559,6 +559,11 @@ void Gia_ObjComputeTruthTableStart( Gia_Man_t * p, int nVarsMax )
     p->vTtMemory = Vec_WrdStart( p->nTtWords * 64 );
     p->vTtNums   = Vec_IntAlloc( Gia_ManObjNum(p) + 1000 );
     Vec_IntFill( p->vTtNums, Vec_IntCap(p->vTtNums), -ABC_INFINITY );
+    if ( nVarsMax >= 6 ) {
+        word * pTruth; int i;
+        Vec_PtrForEachEntry( word *, p->vTtInputs, pTruth, i )
+            Abc_TtFlipVar5( pTruth, nVarsMax );
+    }
 }
 void Gia_ObjComputeTruthTableStop( Gia_Man_t * p )
 {

diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c
@@ -22,6 +22,7 @@
 #include "bool/kit/kit.h"
 #include "opt/sfm/sfm.h"
 #include "base/io/ioAbc.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -330,6 +331,7 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
         // update fanins
         vArray = Sfm_NodeReadFanins( p, pNode->iTemp );
         pTruth = Sfm_NodeReadTruth( p, pNode->iTemp );
+        Abc_TtFlipVar5( pTruth, Vec_IntSize(vArray) );
         pNode->pData = Abc_SopCreateFromTruthIsop( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), pTruth, vCover );
         if ( Abc_SopGetVarNum((char *)pNode->pData) == 0 )
             continue;

diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
@@ -3854,6 +3854,23 @@ static inline word * Abc_TtSymFunGenerate( char * pOnes, int nVars )
     return pTruth;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Fix big-endian when dealilng with 5-var truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Abc_TtFlipVar5( word * p, int nVars )
+{
+    int Test = 1;
+    if ( *((char *)&Test) == 0 && nVars > 5 )
+        Abc_TtFlip( p, Abc_TtWordNum(nVars), 5 );
+}
 
 ABC_NAMESPACE_HEADER_END
 

diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c
@@ -110,6 +110,9 @@ int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Ve
     {
         int i, k, c, RetValue, Literal, Cube, nCubes = 0;
         assert( nVars > 0 );
+
+        Abc_TtFlipVar5( &Truth, nVars );
+        Abc_TtFlipVar5( pTruth, nVars );
         for ( c = 0; c < 2; c ++ )
         {
             if ( nVars <= 6 )
@@ -145,6 +148,8 @@ int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Ve
                 Vec_StrPush( vCnf, (char)-1 );
             }
         }
+        Abc_TtFlipVar5( pTruth, nVars );
+
         return nCubes;
     }
 }

diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
@@ -169,7 +169,7 @@ p->timeSat += Abc_Clock() - clk;
         {
             printf( "%3d: %3d ", p->nCexes, iVar );
             Vec_WrdForEachEntry( p->vDivCexes, uSign, i )
-                printf( "%d", Abc_InfoHasBit((unsigned *)&uSign, p->nCexes-1) );
+                printf( "%d", Abc_TtGetBit(&uSign, p->nCexes-1) );
             printf( "\n" );
         }
         // find the next divisor to try

diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
@@ -213,8 +213,8 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
         if ( Vec_IntEntry(p->vValues, i) ^ sat_solver_var_value(p->pSat, iVar) ) // insert 1
         {
             pSign = Vec_WrdEntryP( p->vDivCexes, i );
-            assert( !Abc_InfoHasBit( (unsigned *)pSign, p->nCexes) );
-            Abc_InfoXorBit( (unsigned *)pSign, p->nCexes );
+            assert( !Abc_TtGetBit( pSign, p->nCexes) );
+            Abc_TtXorBit( pSign, p->nCexes );
         }
     p->nCexes++;
     return SFM_SAT_SAT;
@@ -284,8 +284,8 @@ int Sfm_ComputeInterpolantInt( Sfm_Ntk_t * p, word Truth[2] )
         if ( Value ^ sat_solver_var_value(p->pSat, iVar) ) // insert 1
         {
             word * pSign = Vec_WrdEntryP( p->vDivCexes, i );
-            assert( !Abc_InfoHasBit( (unsigned *)pSign, p->nCexes) );
-            Abc_InfoXorBit( (unsigned *)pSign, p->nCexes );
+            assert( !Abc_TtGetBit( pSign, p->nCexes) );
+            Abc_TtXorBit( pSign, p->nCexes );
         }
     }
     p->nCexes++;
@@ -310,7 +310,7 @@ word Sfm_ComputeInterpolant2( Sfm_Ntk_t * p )
     ResP = Abc_Tt6Isop( Truth[1], ~Truth[0], Vec_IntSize(p->vDivIds), &nCubesP );
     ResN = Abc_Tt6Isop( Truth[0], ~Truth[1], Vec_IntSize(p->vDivIds), &nCubesN );
     Res  = nCubesP <= nCubesN ? ResP : ~ResN;
-    //Dau_DsdPrintFromTruth( &Res, Vec_IntSize(p->vDivIds) );            
+    //Dau_DsdPrintFromTruth( &Res, Vec_IntSize(p->vDivIds) );
     return Res;
 }