From 733fec328ce1dc60378b95390a7338e99552e3b7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 23 Dec 2024 20:04:21 -0800 Subject: [PATCH] Fixing big-endian problems in mfs2 and &mfs. --- src/aig/gia/giaMfs.c | 6 ++++++ src/aig/gia/giaTruth.c | 5 +++++ src/base/abci/abcMfs.c | 2 ++ src/misc/util/utilTruth.h | 17 +++++++++++++++++ src/opt/sfm/sfmCnf.c | 5 +++++ src/opt/sfm/sfmCore.c | 2 +- src/opt/sfm/sfmSat.c | 10 +++++----- 7 files changed, 41 insertions(+), 6 deletions(-) diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index a0e6caed4f..7ddef2b893 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -395,7 +395,9 @@ 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) ); @@ -403,7 +405,11 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) } } 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 index c24748ede0..0845eae96c 100644 --- 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 index 0533d189f9..90fa268ed4 100644 --- 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 index 323c96467a..6cfab71094 100644 --- 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 index e3af7e0116..7c917fa7e8 100644 --- 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 index f363e1cb0e..a988297592 100644 --- 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 index c83f868835..5d670f81de 100644 --- 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; }