summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--abclib.dsp24
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaShrink.c3
-rw-r--r--src/aig/gia/giaShrink6.c481
-rw-r--r--src/aig/gia/module.make1
-rw-r--r--src/base/abci/abc.c14
-rw-r--r--src/bool/rsb/module.make2
-rw-r--r--src/bool/rsb/rsb.h65
-rw-r--r--src/bool/rsb/rsbDec6.c733
-rw-r--r--src/bool/rsb/rsbInt.h84
-rw-r--r--src/bool/rsb/rsbMan.c99
-rw-r--r--src/misc/util/utilTruth.h140
13 files changed, 1642 insertions, 7 deletions
diff --git a/Makefile b/Makefile
index c533aeeb..7ea37b2c 100644
--- a/Makefile
+++ b/Makefile
@@ -20,7 +20,7 @@ MODULES := \
src/opt/ret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau \
src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \
- src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
+ src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky src/bool/rsb \
src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \
src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \
src/proof/abs \
diff --git a/abclib.dsp b/abclib.dsp
index 979f6bcf..6c2d3ee6 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3543,6 +3543,10 @@ SOURCE=.\src\aig\gia\giaShrink.c
# End Source File
# Begin Source File
+SOURCE=.\src\aig\gia\giaShrink6.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\aig\gia\giaSim.c
# End Source File
# Begin Source File
@@ -3786,6 +3790,26 @@ SOURCE=.\src\bool\lucky\luckySwap.c
SOURCE=.\src\bool\lucky\luckySwapIJ.c
# End Source File
# End Group
+# Begin Group "rsb"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\bool\rsb\rsb.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bool\rsb\rsbDec6.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bool\rsb\rsbInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bool\rsb\rsbMan.c
+# End Source File
+# End Group
# End Group
# Begin Group "prove"
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 23afc45e..eb3bedab 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -980,6 +980,7 @@ extern Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose );
/*=== giaShrink.c ===========================================================*/
extern Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose );
+extern Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int fKeepLevel, int fVerbose );
/*=== giaSort.c ============================================================*/
extern int * Gia_SortFloats( float * pArray, int * pPerm, int nSize );
/*=== giaSim.c ============================================================*/
diff --git a/src/aig/gia/giaShrink.c b/src/aig/gia/giaShrink.c
index 487f9aa6..69dec67c 100644
--- a/src/aig/gia/giaShrink.c
+++ b/src/aig/gia/giaShrink.c
@@ -85,7 +85,8 @@ Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose
if ( Gia_ObjIsCi(pObj) )
{
pObj->Value = Gia_ManAppendCi( pNew );
- Gia_ObjSetLevel( pNew, Gia_ObjFromLit(pNew, Gia_ObjValue(pObj)), Gia_ObjLevel(p, pObj) );
+ if ( p->vLevels )
+ Gia_ObjSetLevel( pNew, Gia_ObjFromLit(pNew, Gia_ObjValue(pObj)), Gia_ObjLevel(p, pObj) );
}
else if ( Gia_ObjIsCo(pObj) )
{
diff --git a/src/aig/gia/giaShrink6.c b/src/aig/gia/giaShrink6.c
new file mode 100644
index 00000000..0d7f7541
--- /dev/null
+++ b/src/aig/gia/giaShrink6.c
@@ -0,0 +1,481 @@
+/**CFile****************************************************************
+
+ FileName [giaShrink6.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [Implementation of DAG-aware unmapping for 6-input cuts.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaShrink6.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "bool/bdc/bdc.h"
+#include "bool/rsb/rsb.h"
+//#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static word Truth[8] = {
+ ABC_CONST(0xAAAAAAAAAAAAAAAA),
+ ABC_CONST(0xCCCCCCCCCCCCCCCC),
+ ABC_CONST(0xF0F0F0F0F0F0F0F0),
+ ABC_CONST(0xFF00FF00FF00FF00),
+ ABC_CONST(0xFFFF0000FFFF0000),
+ ABC_CONST(0xFFFFFFFF00000000),
+ ABC_CONST(0x0000000000000000),
+ ABC_CONST(0xFFFFFFFFFFFFFFFF)
+};
+
+// fanout structure
+typedef struct Shr_Fan_t_ Shr_Fan_t;
+struct Shr_Fan_t_
+{
+ int iFan; // fanout ID
+ int Next; // next structure
+};
+
+// operation manager
+typedef struct Shr_Man_t_ Shr_Man_t;
+struct Shr_Man_t_
+{
+ Gia_Man_t * pGia; // user's AIG
+ Gia_Man_t * pNew; // constructed AIG
+ int nDivMax; // max number of divisors
+ int nNewSize; // max growth size
+ // dynamic fanout (can only grow)
+ Vec_Wrd_t * vFanMem; // fanout memory
+ Vec_Int_t * vObj2Fan; // fanout
+ Shr_Fan_t * pFanTemp; // temporary fanout
+ // divisors
+ Vec_Int_t * vDivs; // divisors
+ Vec_Int_t * vPrio; // priority queue
+ Vec_Int_t * vDivResub; // resubstitution
+ Vec_Int_t * vLeaves; // cut leaves
+ // truth tables
+ Vec_Wrd_t * vTruths; // truth tables
+ Vec_Wrd_t * vDivTruths; // truth tables
+ // bidecomposition
+ Rsb_Man_t * pManRsb;
+ Bdc_Man_t * pManDec;
+ Bdc_Par_t Pars;
+};
+
+#define Shr_ObjForEachFanout( p, iNode, iFan ) \
+ for ( iFan = Shr_ManFanIterStart(p, iNode); iFan; iFan = Shr_ManFanIterNext(p) )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Shr_Man_t * Shr_ManAlloc( Gia_Man_t * pGia )
+{
+ Shr_Man_t * p;
+ p = ABC_CALLOC( Shr_Man_t, 1 );
+ p->nDivMax = 64;
+ p->nNewSize = 3 * Gia_ManObjNum(pGia) / 2;
+ p->pGia = pGia;
+ p->vFanMem = Vec_WrdAlloc( 1000 ); Vec_WrdPush(p->vFanMem, -1);
+ p->vObj2Fan = Vec_IntStart( p->nNewSize );
+ p->vDivs = Vec_IntAlloc( 1000 );
+ p->vPrio = Vec_IntAlloc( 1000 );
+ p->vTruths = Vec_WrdStart( p->nNewSize );
+ p->vDivTruths = Vec_WrdAlloc( 100 );
+ p->vDivResub = Vec_IntAlloc( 6 );
+ p->vLeaves = Vec_IntAlloc( 6 );
+ // start new manager
+ p->pNew = Gia_ManStart( p->nNewSize );
+ p->pNew->pName = Abc_UtilStrsav( pGia->pName );
+ p->pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
+ Gia_ManHashAlloc( p->pNew );
+ Gia_ManCleanLevels( p->pNew, p->nNewSize );
+ // allocate traversal IDs
+ p->pNew->nObjs = p->nNewSize;
+ Gia_ManIncrementTravId( p->pNew );
+ p->pNew->nObjs = 1;
+ // start decompostion
+ p->Pars.nVarsMax = 6;
+ p->Pars.fVerbose = 0;
+ p->pManDec = Bdc_ManAlloc( &p->Pars );
+ p->pManRsb = Rsb_ManAlloc( 6, p->nDivMax, 4, 1 );
+ return p;
+}
+Gia_Man_t * Shr_ManFree( Shr_Man_t * p )
+{
+ // prepare the manager
+ Gia_Man_t * pTemp;
+ Gia_ManHashStop( p->pNew );
+ Vec_IntFreeP( &p->pNew->vLevels );
+ if ( Gia_ManHasDangling(p->pNew) )
+ {
+ p->pNew = Gia_ManCleanup( pTemp = p->pNew );
+ if ( Gia_ManAndNum(p->pNew) != Gia_ManAndNum(pTemp) )
+ printf( "Gia_ManShrink6() node reduction after sweep %6d -> %6d.\n", Gia_ManAndNum(pTemp), Gia_ManAndNum(p->pNew) );
+ Gia_ManStop( pTemp );
+ }
+ Gia_ManSetRegNum( p->pNew, Gia_ManRegNum(p->pGia) );
+ pTemp = p->pNew; p->pNew = NULL;
+ // free data structures
+ Rsb_ManFree( p->pManRsb );
+ Bdc_ManFree( p->pManDec );
+ Gia_ManStopP( &p->pNew );
+ Vec_WrdFree( p->vFanMem );
+ Vec_IntFree( p->vObj2Fan );
+ Vec_IntFree( p->vDivs );
+ Vec_IntFree( p->vPrio );
+ Vec_WrdFree( p->vTruths );
+ Vec_WrdFree( p->vDivTruths );
+ Vec_IntFree( p->vDivResub );
+ Vec_IntFree( p->vLeaves );
+ ABC_FREE( p );
+ return pTemp;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Fanout manipulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Shr_ManAddFanout( Shr_Man_t * p, int iFanin, int iFanout )
+{
+ Shr_Fan_t FanStr;
+ FanStr.iFan = iFanout;
+ FanStr.Next = Vec_IntEntry(p->vObj2Fan, iFanin);
+ Vec_IntWriteEntry( p->vObj2Fan, iFanin, Vec_WrdSize(p->vFanMem) );
+ Vec_WrdPush(p->vFanMem, *((word *)&FanStr) );
+}
+static inline int Shr_ManFanIterStart( Shr_Man_t * p, int iNode )
+{
+ if ( Vec_IntEntry(p->vObj2Fan, iNode) == 0 )
+ return 0;
+ p->pFanTemp = (Shr_Fan_t *)Vec_WrdEntryP( p->vFanMem, Vec_IntEntry(p->vObj2Fan, iNode) );
+ return p->pFanTemp->iFan;
+}
+static inline int Shr_ManFanIterNext( Shr_Man_t * p )
+{
+ if ( p->pFanTemp->Next == 0 )
+ return 0;
+ p->pFanTemp = (Shr_Fan_t *)Vec_WrdEntryP( p->vFanMem, p->pFanTemp->Next );
+ return p->pFanTemp->iFan;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collect divisors.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Shr_ManDivPushOrderByLevel( Shr_Man_t * p, int iDiv )
+{
+ int iPlace, * pArray;
+ Vec_IntPush( p->vPrio, iDiv );
+ if ( Vec_IntSize(p->vPrio) == 1 )
+ return 0;
+ pArray = Vec_IntArray(p->vPrio);
+ for ( iPlace = Vec_IntSize(p->vPrio) - 1; iPlace > 0; iPlace-- )
+ if ( Gia_ObjLevel(p->pNew, Gia_ManObj(p->pNew, pArray[iPlace-1])) >
+ Gia_ObjLevel(p->pNew, Gia_ManObj(p->pNew, pArray[iPlace])) )
+ ABC_SWAP( int, pArray[iPlace-1], pArray[iPlace] )
+ else
+ break;
+ return iPlace; // the place of the new divisor
+}
+static inline int Shr_ManCollectDivisors( Shr_Man_t * p, Vec_Int_t * vLeaves, int Limit )
+{
+ Gia_Obj_t * pFan;
+ int i, iDiv, iFan, iPlace;
+ assert( Limit > 6 );
+ Vec_IntClear( p->vDivs );
+ Vec_IntClear( p->vPrio );
+ Gia_ManIncrementTravId( p->pNew );
+ Vec_IntForEachEntry( vLeaves, iDiv, i )
+ {
+ Vec_IntPush( p->vDivs, iDiv );
+ Shr_ManDivPushOrderByLevel( p, iDiv );
+ Gia_ObjSetTravIdCurrentId( p->pNew, iDiv );
+ }
+ Vec_IntForEachEntry( p->vPrio, iDiv, i )
+ {
+ assert( Gia_ObjIsTravIdCurrentId(p->pNew, iDiv) );
+ Shr_ObjForEachFanout( p, iDiv, iFan )
+ {
+ if ( Gia_ObjIsTravIdCurrentId(p->pNew, iFan) )
+ continue;
+ pFan = Gia_ManObj( p->pNew, iFan );
+ assert( Gia_ObjIsAnd(pFan) );
+ assert( Gia_ObjLevel(p->pNew, Gia_ManObj(p->pNew, iDiv)) < Gia_ObjLevel(p->pNew, pFan) );
+ if ( !Gia_ObjIsTravIdCurrentId(p->pNew, Gia_ObjFaninId0(pFan, iFan)) ||
+ !Gia_ObjIsTravIdCurrentId(p->pNew, Gia_ObjFaninId1(pFan, iFan)) )
+ continue;
+ Vec_IntPush( p->vDivs, iFan );
+ Gia_ObjSetTravIdCurrentId( p->pNew, iFan );
+ iPlace = Shr_ManDivPushOrderByLevel( p, iFan );
+ assert( i < iPlace );
+ if ( Vec_IntSize(p->vDivs) == Limit )
+ return Vec_IntSize(p->vDivs);
+ }
+ }
+ return Vec_IntSize(p->vDivs);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resynthesizes nodes using bi-decomposition.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Shr_ObjPerformBidec( Shr_Man_t * p, Bdc_Man_t * pManDec, Gia_Man_t * pNew, Vec_Int_t * vLeafLits, word uTruth1, word uTruthC )
+{
+ Bdc_Fun_t * pFunc;
+ Gia_Obj_t * pObj;
+ int i, iVar, iLit, nNodes, iLast;
+ int nVars = Vec_IntSize(vLeafLits);
+ assert( uTruth1 != 0 && uTruthC != 0 );
+ Bdc_ManDecompose( pManDec, (unsigned *)&uTruth1, (unsigned *)&uTruthC, nVars, NULL, 1000 );
+ Bdc_FuncSetCopyInt( Bdc_ManFunc(pManDec, 0), 1 );
+ Vec_IntForEachEntry( vLeafLits, iVar, i )
+ Bdc_FuncSetCopyInt( Bdc_ManFunc(pManDec, i+1), Abc_Var2Lit(iVar, 0) );
+ nNodes = Bdc_ManNodeNum( pManDec );
+ for ( i = nVars + 1; i < nNodes; i++ )
+ {
+ pFunc = Bdc_ManFunc( pManDec, i );
+ iLast = Gia_ManObjNum(pNew);
+ iLit = Gia_ManHashAnd( pNew, Bdc_FunFanin0Copy(pFunc), Bdc_FunFanin1Copy(pFunc) );
+ Bdc_FuncSetCopyInt( pFunc, iLit );
+ if ( iLast == Gia_ManObjNum(pNew) )
+ continue;
+ assert( iLast + 1 == Gia_ManObjNum(pNew) );
+ pObj = Gia_ManObj(pNew, Abc_Lit2Var(iLit));
+ Gia_ObjSetAndLevel( pNew, pObj );
+ Shr_ManAddFanout( p, Gia_ObjFaninId0p(pNew, pObj), Gia_ObjId(pNew, pObj) );
+ Shr_ManAddFanout( p, Gia_ObjFaninId1p(pNew, pObj), Gia_ObjId(pNew, pObj) );
+ assert( Gia_ManObjNum(pNew) < p->nNewSize );
+ }
+ return Bdc_FunObjCopy( Bdc_ManRoot(pManDec) );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Compute truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+word Shr_ManComputeTruth6_rec( Gia_Man_t * p, int iNode, Vec_Wrd_t * vTruths )
+{
+ Gia_Obj_t * pObj;
+ word Truth0, Truth1;
+ if ( Gia_ObjIsTravIdCurrentId(p, iNode) )
+ return Vec_WrdEntry(vTruths, iNode);
+ Gia_ObjSetTravIdCurrentId(p, iNode);
+ pObj = Gia_ManObj( p, iNode );
+ assert( Gia_ObjIsAnd(pObj) );
+ Truth0 = Shr_ManComputeTruth6_rec( p, Gia_ObjFaninId0p(p, pObj), vTruths );
+ Truth1 = Shr_ManComputeTruth6_rec( p, Gia_ObjFaninId1p(p, pObj), vTruths );
+ if ( Gia_ObjFaninC0(pObj) )
+ Truth0 = ~Truth0;
+ if ( Gia_ObjFaninC1(pObj) )
+ Truth1 = ~Truth1;
+ Vec_WrdWriteEntry( vTruths, iNode, Truth0 & Truth1 );
+ return Truth0 & Truth1;
+}
+word Shr_ManComputeTruth6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves, Vec_Wrd_t * vTruths )
+{
+ int i, iLeaf;
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_ManIncrementTravId( p );
+ Vec_IntForEachEntry( vLeaves, iLeaf, i )
+ {
+ Gia_ObjSetTravIdCurrentId( p, iLeaf );
+ Vec_WrdWriteEntry( vTruths, iLeaf, Truth[i] );
+ }
+ return Shr_ManComputeTruth6_rec( p, Gia_ObjId(p, pObj), vTruths );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compute truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Shr_ManComputeTruths( Gia_Man_t * p, int nVars, Vec_Int_t * vDivs, Vec_Wrd_t * vDivTruths, Vec_Wrd_t * vTruths )
+{
+ Gia_Obj_t * pObj;
+ word Truth0, Truth1;//, Truthh;
+ int i, iDiv;
+ Vec_WrdClear( vDivTruths );
+ Vec_IntForEachEntryStop( vDivs, iDiv, i, nVars )
+ {
+ Vec_WrdWriteEntry( vTruths, iDiv, Truth[i] );
+ Vec_WrdPush( vDivTruths, Truth[i] );
+ }
+ Vec_IntForEachEntryStart( vDivs, iDiv, i, nVars )
+ {
+ pObj = Gia_ManObj( p, iDiv );
+ Truth0 = Vec_WrdEntry( vTruths, Gia_ObjFaninId0(pObj, iDiv) );
+ Truth1 = Vec_WrdEntry( vTruths, Gia_ObjFaninId1(pObj, iDiv) );
+ if ( Gia_ObjFaninC0(pObj) )
+ Truth0 = ~Truth0;
+ if ( Gia_ObjFaninC1(pObj) )
+ Truth1 = ~Truth1;
+ Vec_WrdWriteEntry( vTruths, iDiv, Truth0 & Truth1 );
+ Vec_WrdPush( vDivTruths, Truth0 & Truth1 );
+
+// Truthh = Truth0 & Truth1;
+// Abc_TtPrintBinary( &Truthh, nVars ); //printf( "\n" );
+// Kit_DsdPrintFromTruth( &Truthh, nVars ); printf( "\n" );
+ }
+// printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int fKeepLevel, int fVerbose )
+{
+ Shr_Man_t * pMan;
+ Gia_Obj_t * pObj, * pFanin;
+ word uTruth, uTruth0, uTruth1;
+ int i, k, nDivs, iNode;
+ int RetValue, Counter1 = 0, Counter2 = 0;
+ clock_t clk = clock();
+ assert( p->pMapping != NULL );
+ pMan = Shr_ManAlloc( p );
+ Gia_ManFillValue( p );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( Gia_ObjIsCi(pObj) )
+ {
+ pObj->Value = Gia_ManAppendCi( pMan->pNew );
+ if ( p->vLevels )
+ Gia_ObjSetLevel( pMan->pNew, Gia_ObjFromLit(pMan->pNew, Gia_ObjValue(pObj)), Gia_ObjLevel(p, pObj) );
+ }
+ else if ( Gia_ObjIsCo(pObj) )
+ {
+ pObj->Value = Gia_ManAppendCo( pMan->pNew, Gia_ObjFanin0Copy(pObj) );
+ }
+ else if ( Gia_ObjIsLut(p, i) )
+ {
+ // collect leaves of this gate
+ Vec_IntClear( pMan->vLeaves );
+ Gia_LutForEachFanin( p, i, iNode, k )
+ Vec_IntPush( pMan->vLeaves, iNode );
+ assert( Vec_IntSize(pMan->vLeaves) <= 6 );
+ // compute truth table
+ uTruth = Shr_ManComputeTruth6( pMan->pGia, pObj, pMan->vLeaves, pMan->vTruths );
+ assert( pObj->Value == ~0 );
+ if ( uTruth == 0 || ~uTruth == 0 )
+ pObj->Value = Abc_LitNotCond( 0, ~uTruth == 0 );
+ else
+ Gia_ManForEachObjVec( pMan->vLeaves, p, pFanin, k )
+ if ( uTruth == Truth[k] || ~uTruth == Truth[k] )
+ pObj->Value = Abc_LitNotCond( pFanin->Value, ~uTruth == Truth[k] );
+ if ( pObj->Value != ~0 )
+ continue;
+ // translate into new nodes
+ Gia_ManForEachObjVec( pMan->vLeaves, p, pFanin, k )
+ {
+ if ( Abc_LitIsCompl(pFanin->Value) )
+ uTruth = ((uTruth & Truth[k]) >> (1 << k)) | ((uTruth & ~Truth[k]) << (1 << k));
+ Vec_IntWriteEntry( pMan->vLeaves, k, Abc_Lit2Var(pFanin->Value) );
+ }
+ // compute divisors
+ nDivs = Shr_ManCollectDivisors( pMan, pMan->vLeaves, pMan->nDivMax );
+ assert( nDivs <= pMan->nDivMax );
+ // compute truth tables
+ Shr_ManComputeTruths( pMan->pNew, Vec_IntSize(pMan->vLeaves), pMan->vDivs, pMan->vDivTruths, pMan->vTruths );
+ // perform resubstitution
+ RetValue = Rsb_ManPerformResub6( pMan->pManRsb, Vec_IntSize(pMan->vLeaves), uTruth, pMan->vDivTruths, &uTruth0, &uTruth1, 0 );
+ if ( RetValue ) // resub exists
+ {
+ Vec_Int_t * vResult = Rsb_ManGetFanins(pMan->pManRsb);
+ Vec_IntClear( pMan->vDivResub );
+ Vec_IntForEachEntry( vResult, iNode, k )
+ Vec_IntPush( pMan->vDivResub, Vec_IntEntry(pMan->vDivs, iNode) );
+ pObj->Value = Shr_ObjPerformBidec( pMan, pMan->pManDec, pMan->pNew, pMan->vDivResub, uTruth1, uTruth0 | uTruth1 );
+ Counter1++;
+ }
+ else
+ {
+ pObj->Value = Shr_ObjPerformBidec( pMan, pMan->pManDec, pMan->pNew, pMan->vLeaves, uTruth, ~(word)0 );
+ Counter2++;
+ }
+ }
+ }
+ if ( fVerbose )
+ {
+ printf( "Performed %d resubs and %d decomps. ", Counter1, Counter2 );
+ printf( "Gain in AIG nodes = %d. ", Gia_ManObjNum(p)-Gia_ManObjNum(pMan->pNew) );
+ ABC_PRT( "Runtime", clock() - clk );
+ }
+ return Shr_ManFree( pMan );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 17147f49..5cb60633 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -31,6 +31,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaRetime.c \
src/aig/gia/giaScl.c \
src/aig/gia/giaShrink.c \
+ src/aig/gia/giaShrink6.c \
src/aig/gia/giaSim.c \
src/aig/gia/giaSim2.c \
src/aig/gia/giaSort.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d972b506..b913e04e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26155,7 +26155,8 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Shrink( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- Gia_Man_t * pTemp;
+ Gia_Man_t * pTemp = NULL;
+ int nLutSize;
int c,fVerbose = 0;
int fKeepLevel = 0;
Extra_UtilGetoptReset();
@@ -26185,8 +26186,15 @@ int Abc_CommandAbc9Shrink( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Shrink(): Mapping of the AIG is not defined.\n" );
return 1;
}
- pTemp = Gia_ManPerformMapShrink( pAbc->pGia, fKeepLevel, fVerbose );
- Abc_FrameUpdateGia( pAbc, pTemp );
+ nLutSize = Gia_ManLutSizeMax( pAbc->pGia );
+ if ( nLutSize <= 4 )
+ pTemp = Gia_ManPerformMapShrink( pAbc->pGia, fKeepLevel, fVerbose );
+ else if ( nLutSize <= 6 )
+ pTemp = Gia_ManMapShrink6( pAbc->pGia, fKeepLevel, fVerbose );
+ else
+ Abc_Print( -1, "Abc_CommandAbc9Shrink(): Works only for 4-LUTs and 6-LUTs.\n" );
+ if ( pTemp )
+ Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
diff --git a/src/bool/rsb/module.make b/src/bool/rsb/module.make
new file mode 100644
index 00000000..0011e6a5
--- /dev/null
+++ b/src/bool/rsb/module.make
@@ -0,0 +1,2 @@
+SRC += src/bool/rsb/rsbDec6.c \
+ src/bool/rsb/rsbMan.c
diff --git a/src/bool/rsb/rsb.h b/src/bool/rsb/rsb.h
new file mode 100644
index 00000000..e0b92d30
--- /dev/null
+++ b/src/bool/rsb/rsb.h
@@ -0,0 +1,65 @@
+/**CFile****************************************************************
+
+ FileName [rsb.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Truth-table based resubstitution.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rsb.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__bool_Rsb_h
+#define ABC__bool_Rsb_h
+
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Rsb_Man_t_ Rsb_Man_t;
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== rsbMan.c ==========================================================*/
+extern Rsb_Man_t * Rsb_ManAlloc( int nLeafMax, int nDivMax, int nDecMax, int fVerbose );
+extern void Rsb_ManFree( Rsb_Man_t * p );
+extern Vec_Int_t * Rsb_ManGetFanins( Rsb_Man_t * p );
+extern Vec_Int_t * Rsb_ManGetFaninsOld( Rsb_Man_t * p );
+/*=== rsbDec6.c ==========================================================*/
+extern int Rsb_ManPerformResub6( Rsb_Man_t * p, int nVars, word uTruth, Vec_Wrd_t * vDivTruths, word * puTruth0, word * puTruth1, int fVerbose );
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/bool/rsb/rsbDec6.c b/src/bool/rsb/rsbDec6.c
new file mode 100644
index 00000000..90f88938
--- /dev/null
+++ b/src/bool/rsb/rsbDec6.c
@@ -0,0 +1,733 @@
+/**CFile****************************************************************
+
+ FileName [rsbDec6.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Truth-table-based resubstitution.]
+
+ Synopsis [Implementation of the algorithm.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rsbDec6.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rsbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Rsb_DecTry0( word c )
+{
+ return (unsigned)(c != 0);
+}
+static inline unsigned Rsb_DecTry1( word c, word f1 )
+{
+ return (Rsb_DecTry0(c&f1) << 1) | Rsb_DecTry0(c&~f1);
+}
+static inline unsigned Rsb_DecTry2( word c, word f1, word f2 )
+{
+ return (Rsb_DecTry1(c&f2, f1) << 2) | Rsb_DecTry1(c&~f2, f1);
+}
+static inline unsigned Rsb_DecTry3( word c, word f1, word f2, word f3 )
+{
+ return (Rsb_DecTry2(c&f3, f1, f2) << 4) | Rsb_DecTry2(c&~f3, f1, f2);
+}
+static inline unsigned Rsb_DecTry4( word c, word f1, word f2, word f3, word f4 )
+{
+ return (Rsb_DecTry3(c&f4, f1, f2, f3) << 8) | Rsb_DecTry3(c&~f4, f1, f2, f3);
+}
+static inline unsigned Rsb_DecTry5( word c, word f1, word f2, word f3, word f4, word f5 )
+{
+ return (Rsb_DecTry4(c&f5, f1, f2, f3, f4) << 16) | Rsb_DecTry4(c&~f5, f1, f2, f3, f4);
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Rsb_DecTryCex( word * g, int iCexA, int iCexB )
+{
+ return Abc_TtGetBit(g, iCexA) == Abc_TtGetBit(g, iCexB);
+}
+static inline void Rsb_DecVerifyCex( word * f, word ** g, int nGs, int iCexA, int iCexB )
+{
+ int i;
+ // f distinquished it
+ if ( Rsb_DecTryCex( f, iCexA, iCexB ) )
+ printf( "Verification of CEX has failed: f(A) == f(B)!!!\n" );
+ // g do not distinguish it
+ for ( i = 0; i < nGs; i++ )
+ if ( !Rsb_DecTryCex( g[i], iCexA, iCexB ) )
+ printf( "Verification of CEX has failed: g[%d](A) != g[%d](B)!!!\n", i, i );
+}
+static inline void Rsb_DecRecordCex( word ** g, int nGs, int iCexA, int iCexB, word * pCexes, int nCexes )
+{
+ int i;
+ assert( nCexes < 64 );
+ for ( i = 0; i < nGs; i++ )
+ if ( Rsb_DecTryCex(g[i], iCexA, iCexB) )
+ Abc_TtSetBit( pCexes + i, nCexes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks decomposability of f with divisors g.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline word Rsb_DecCofactor( word ** g, int nGs, int w, int iMint )
+{
+ int i;
+ word Cof = ~(word)0;
+ for ( i = 0; i < nGs; i++ )
+ Cof &= ((iMint >> i) & 1) ? g[i][w] : ~g[i][w];
+ return Cof;
+}
+unsigned Rsb_DecCheck( int nVars, word * f, word ** g, int nGs, unsigned * pPat, int * pCexA, int * pCexB )
+{
+ word CofA, CofB;
+ int nWords = Abc_TtWordNum( nVars );
+ int w, k, iMint, iShift = ( 1 << nGs );
+ unsigned uMask = (~(unsigned)0) >> (32-iShift);
+ unsigned uTotal = 0;
+ assert( nGs > 0 && nGs < 5 );
+ for ( w = 0; w < nWords; w++ )
+ {
+ // generate decomposition pattern
+ if ( nGs == 1 )
+ pPat[w] = Rsb_DecTry2( ~(word)0, g[0][w], f[w] );
+ else if ( nGs == 2 )
+ pPat[w] = Rsb_DecTry3( ~(word)0, g[0][w], g[1][w], f[w] );
+ else if ( nGs == 3 )
+ pPat[w] = Rsb_DecTry4( ~(word)0, g[0][w], g[1][w], g[2][w], f[w] );
+ else if ( nGs == 4 )
+ pPat[w] = Rsb_DecTry5( ~(word)0, g[0][w], g[1][w], g[2][w], g[3][w], f[w] );
+ // check if it is consistent
+ iMint = Abc_Tt6FirstBit( (pPat[w] >> iShift) & pPat[w] & uMask );
+ if ( iMint >= 0 )
+ { // generate a cex
+ CofA = Rsb_DecCofactor( g, nGs, w, iMint );
+ assert( (~f[w] & CofA) && (f[w] & CofA) );
+ *pCexA = w * 64 + Abc_Tt6FirstBit( ~f[w] & CofA );
+ *pCexB = w * 64 + Abc_Tt6FirstBit( f[w] & CofA );
+ return 0;
+ }
+ uTotal |= pPat[w];
+ if ( w == 0 )
+ continue;
+ // check if it is consistent with other patterns seen so far
+ iMint = Abc_Tt6FirstBit( (uTotal >> iShift) & uTotal & uMask );
+ if ( iMint == -1 )
+ continue;
+ // find an overlap and generate a cex
+ for ( k = 0; k < w; k++ )
+ {
+ iMint = Abc_Tt6FirstBit( ((pPat[k] | pPat[w]) >> iShift) & (pPat[k] | pPat[w]) & uMask );
+ if ( iMint == -1 )
+ continue;
+ CofA = Rsb_DecCofactor( g, nGs, k, iMint );
+ CofB = Rsb_DecCofactor( g, nGs, w, iMint );
+ if ( (~f[k] & CofA) && (f[w] & CofB) )
+ {
+ *pCexA = k * 64 + Abc_Tt6FirstBit( ~f[k] & CofA );
+ *pCexB = w * 64 + Abc_Tt6FirstBit( f[w] & CofB );
+ }
+ else
+ {
+ assert( (f[k] & CofA) && (~f[w] & CofB) );
+ *pCexA = k * 64 + Abc_Tt6FirstBit( f[k] & CofA );
+ *pCexB = w * 64 + Abc_Tt6FirstBit( ~f[w] & CofB );
+ }
+ return 0;
+ }
+ }
+ return uTotal;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rsb_DecPrintTable( word * pCexes, int nGs, int nGsAll, Vec_Int_t * vTries )
+{
+ int pCands[16], nCands;
+ int i, c, Cand, iStart = 0;
+ if ( Vec_IntSize(vTries) == 0 )
+ return;
+
+// printf( "\n" );
+ for ( i = 0; i < 4; i++ )
+ printf( " " );
+ printf( " " );
+ for ( i = 0; i < nGs; i++ )
+ printf( "%d", (i % 100) / 10 );
+ printf( "|" );
+ for ( ; i < nGsAll; i++ )
+ printf( "%d", (i % 100) / 10 );
+ printf( "\n" );
+
+ for ( i = 0; i < 4; i++ )
+ printf( " " );
+ printf( " " );
+ for ( i = 0; i < nGs; i++ )
+ printf( "%d", i % 10 );
+ printf( "|" );
+ for ( ; i < nGsAll; i++ )
+ printf( "%d", i % 10 );
+ printf( "\n" );
+ printf( "\n" );
+
+ for ( c = 0; iStart < Vec_IntSize(vTries); c++ )
+ {
+ // collect candidates
+ for ( i = 0; i < 4; i++ )
+ pCands[i] = -1;
+ nCands = 0;
+ Vec_IntForEachEntryStart( vTries, Cand, i, iStart )
+ if ( Cand == -1 )
+ {
+ iStart = i + 1;
+ break;
+ }
+ else
+ pCands[nCands++] = Cand;
+ assert( nCands <= 4 );
+ // print them
+ for ( i = 0; i < 4; i++ )
+ if ( pCands[i] >= 0 )
+ printf( "%4d", pCands[i] );
+ else
+ printf( " " );
+ // print the bit-string
+ printf( " " );
+ for ( i = 0; i < nGs; i++ )
+ printf( "%c", Abc_TtGetBit( pCexes + i, c ) ? '.' : '+' );
+ printf( "|" );
+ for ( ; i < nGsAll; i++ )
+ printf( "%c", Abc_TtGetBit( pCexes + i, c ) ? '.' : '+' );
+ printf( " %3d\n", c );
+ }
+ printf( "\n" );
+
+ // write the number of ones
+ for ( i = 0; i < 4; i++ )
+ printf( " " );
+ printf( " " );
+ for ( i = 0; i < nGs; i++ )
+ printf( "%d", Abc_TtCountOnes(pCexes[i]) / 10 );
+ printf( "|" );
+ for ( ; i < nGsAll; i++ )
+ printf( "%d", Abc_TtCountOnes(pCexes[i]) / 10 );
+ printf( "\n" );
+
+ for ( i = 0; i < 4; i++ )
+ printf( " " );
+ printf( " " );
+ for ( i = 0; i < nGs; i++ )
+ printf( "%d", Abc_TtCountOnes(pCexes[i]) % 10 );
+ printf( "|" );
+ for ( ; i < nGsAll; i++ )
+ printf( "%d", Abc_TtCountOnes(pCexes[i]) % 10 );
+ printf( "\n" );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Init ]
+
+ Description [Returns the numbers of the decomposition functions and
+ the truth table of a function up to 4 variables.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rsb_DecInitCexes( int nVars, word * f, word ** g, int nGs, int nGsAll, word * pCexes, Vec_Int_t * vTries )
+{
+ int nWords = Abc_TtWordNum( nVars );
+ int ValueB = Abc_TtGetBit( f, 0 );
+ int ValueE = Abc_TtGetBit( f, 64*nWords-1 );
+ int iCexT0, iCexT1, iCexF0, iCexF1;
+
+ iCexT0 = ValueB ? 0 : Abc_TtFindFirstBit( f, nVars );
+ iCexT1 = ValueE ? 64*nWords-1 : Abc_TtFindLastBit( f, nVars );
+
+ iCexF0 = !ValueB ? 0 : Abc_TtFindFirstZero( f, nVars );
+ iCexF1 = !ValueE ? 64*nWords-1 : Abc_TtFindLastZero( f, nVars );
+
+ assert( !Rsb_DecTryCex( f, iCexT0, iCexF0 ) );
+ assert( !Rsb_DecTryCex( f, iCexT0, iCexF1 ) );
+ assert( !Rsb_DecTryCex( f, iCexT1, iCexF0 ) );
+ assert( !Rsb_DecTryCex( f, iCexT1, iCexF1 ) );
+
+ Rsb_DecRecordCex( g, nGsAll, iCexT0, iCexF0, pCexes, 0 );
+ Rsb_DecRecordCex( g, nGsAll, iCexT0, iCexF1, pCexes, 1 );
+ Rsb_DecRecordCex( g, nGsAll, iCexT1, iCexF0, pCexes, 2 );
+ Rsb_DecRecordCex( g, nGsAll, iCexT1, iCexF1, pCexes, 3 );
+
+ if ( vTries )
+ {
+ Vec_IntPush( vTries, -1 );
+ Vec_IntPush( vTries, -1 );
+ Vec_IntPush( vTries, -1 );
+ Vec_IntPush( vTries, -1 );
+ }
+ return 4;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Finds a setset of gs to decompose f.]
+
+ Description [Returns the numbers of the decomposition functions and
+ the truth table of a function up to 4 variables.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll )
+{
+ word * pCexes = Vec_WrdArray(p->vCexes);
+ unsigned * pPat = (unsigned *)Vec_IntArray(p->vDecPats);
+ /*
+ The following filtering hueristic can be used:
+ after the first round (if there is more than 5 cexes,
+ remove all the divisors, except fanins of the node
+ This should lead to a speadup without sacrifying quality.
+
+ Another idea is to precompute several counter-examples
+ like the first and last 0 and 1 mints of the function
+ which yields 4 cexes.
+ */
+
+ word * pDivs[16];
+ unsigned uTruth = 0;
+ int i, k, j, n, iCexA, iCexB, nCexes = 0;
+ memset( pCexes, 0, sizeof(word) * nGsAll );
+ Vec_IntClear( p->vTries );
+ // populate the counter-examples with the three most obvious
+// nCexes = Rsb_DecInitCexes( nVars, f, g, nGs, nGsAll, pCexes, vTries );
+ // start by checking each function
+ p->vFanins->nSize = 1;
+ for ( i = 0; i < nGs; i++ )
+ {
+ if ( pCexes[i] )
+ continue;
+ pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
+ uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
+ if ( uTruth )
+ return uTruth;
+ if ( nCexes == 64 )
+ return 0;
+ Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
+ Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ );
+ if ( !p->fVerbose )
+ continue;
+ Vec_IntPush( p->vTries, i );
+ Vec_IntPush( p->vTries, -1 );
+ }
+ if ( p->nDecMax == 1 )
+ return 0;
+ // continue by checking pairs
+ p->vFanins->nSize = 2;
+ for ( i = 1; i < nGs; i++ )
+ for ( k = 0; k < i; k++ )
+ {
+ if ( pCexes[i] & pCexes[k] )
+ continue;
+ pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
+ pDivs[1] = g[k]; p->vFanins->pArray[1] = k;
+ uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
+ if ( uTruth )
+ return uTruth;
+ if ( nCexes == 64 )
+ return 0;
+ Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
+ Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ );
+ if ( !p->fVerbose )
+ continue;
+ Vec_IntPush( p->vTries, i );
+ Vec_IntPush( p->vTries, k );
+ Vec_IntPush( p->vTries, -1 );
+ }
+ if ( p->nDecMax == 2 )
+ return 0;
+ // continue by checking triples
+ p->vFanins->nSize = 3;
+ for ( i = 2; i < nGs; i++ )
+ for ( k = 1; k < i; k++ )
+ for ( j = 0; j < k; j++ )
+ {
+ if ( pCexes[i] & pCexes[k] & pCexes[j] )
+ continue;
+ pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
+ pDivs[1] = g[k]; p->vFanins->pArray[1] = k;
+ pDivs[2] = g[j]; p->vFanins->pArray[2] = j;
+ uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
+ if ( uTruth )
+ return uTruth;
+ if ( nCexes == 64 )
+ return 0;
+ Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
+ Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ );
+ if ( !p->fVerbose )
+ continue;
+ Vec_IntPush( p->vTries, i );
+ Vec_IntPush( p->vTries, k );
+ Vec_IntPush( p->vTries, j );
+ Vec_IntPush( p->vTries, -1 );
+ }
+ if ( p->nDecMax == 3 )
+ return 0;
+ // continue by checking quadras
+ p->vFanins->nSize = 4;
+ for ( i = 3; i < nGs; i++ )
+ for ( k = 2; k < i; k++ )
+ for ( j = 1; j < k; j++ )
+ for ( n = 0; n < j; n++ )
+ {
+ if ( pCexes[i] & pCexes[k] & pCexes[j] & pCexes[n] )
+ continue;
+ pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
+ pDivs[1] = g[k]; p->vFanins->pArray[1] = k;
+ pDivs[2] = g[j]; p->vFanins->pArray[2] = j;
+ pDivs[3] = g[n]; p->vFanins->pArray[3] = n;
+ uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
+ if ( uTruth )
+ return uTruth;
+ if ( nCexes == 64 )
+ return 0;
+ Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
+ Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ );
+ if ( !p->fVerbose )
+ continue;
+ Vec_IntPush( p->vTries, i );
+ Vec_IntPush( p->vTries, k );
+ Vec_IntPush( p->vTries, j );
+ Vec_IntPush( p->vTries, n );
+ Vec_IntPush( p->vTries, -1 );
+ }
+// printf( "%d ", nCexes );
+ if ( p->nDecMax == 4 )
+ return 0;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Verifies 4-input decomposition.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rsb_DecPrintFunc( Rsb_Man_t * p, unsigned Truth4, word * f, word ** ppGs, int nGs, int nVarsAll )
+{
+ int nVars = Vec_IntSize(p->vFanins);
+ word Copy = Truth4;
+ word wOn = Abc_Tt6Stretch( Copy >> (1 << nVars), nVars );
+ word wOnDc = ~Abc_Tt6Stretch( Copy, nVars );
+ word wIsop = Abc_Tt6Isop( wOn, wOnDc, nVars );
+ int i;
+
+ printf( "Offset : " );
+ Abc_TtPrintBinary( &Copy, nVars ); //printf( "\n" );
+ Copy >>= (1 << nVars);
+ printf( "Onset : " );
+ Abc_TtPrintBinary( &Copy, nVars ); //printf( "\n" );
+ printf( "Result : " );
+ Abc_TtPrintBinary( &wIsop, nVars ); //printf( "\n" );
+ Kit_DsdPrintFromTruth( (unsigned *)&wIsop, nVars ); printf( "\n" );
+
+ // print functions
+ printf( "Func : " );
+ Abc_TtPrintBinary( f, nVarsAll ); //printf( "\n" );
+ Kit_DsdPrintFromTruth( (unsigned *)f, nVarsAll ); printf( "\n" );
+ for ( i = 0; i < nGs; i++ )
+ {
+ printf( "Div%3d : ", i );
+ Kit_DsdPrintFromTruth( (unsigned *)ppGs[i], nVarsAll ); printf( "\n" );
+ }
+ printf( "Solution : " );
+ for ( i = 0; i < Vec_IntSize(p->vFanins); i++ )
+ printf( "%d ", Vec_IntEntry(p->vFanins, i) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Verifies 4-input decomposition.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rsb_DecVerify( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, unsigned Truth4, word * pTemp1, word * pTemp2 )
+{
+ word * pFanins[16];
+ int b, m, Num, nSuppSize;
+ int nWords = Abc_TtWordNum(nVars);
+ Truth4 >>= (1 << Vec_IntSize(p->vFanins));
+ Truth4 = (unsigned)Abc_Tt6Stretch( (word)Truth4, Vec_IntSize(p->vFanins) );
+//Kit_DsdPrintFromTruth( (unsigned *)&Truth4, Vec_IntSize(p->vFanins) );
+//printf( "\n" );
+// nSuppSize = Rsb_Word6SupportSize( Truth4 );
+// assert( nSuppSize == Vec_IntSize(p->vFanins) );
+ nSuppSize = Vec_IntSize(p->vFanins);
+ // collect the fanins
+ Vec_IntForEachEntry( p->vFanins, Num, b )
+ {
+ assert( Num < nGs );
+ pFanins[b] = g[Num];
+ }
+ // create the or of ands
+ Abc_TtClear( pTemp1, nWords );
+ for ( m = 0; m < (1<<nSuppSize); m++ )
+ {
+ if ( ((Truth4 >> m) & 1) == 0 )
+ continue;
+ Abc_TtFill( pTemp2, nWords );
+ for ( b = 0; b < nSuppSize; b++ )
+ if ( (m >> b) & 1 )
+ Abc_TtAnd( pTemp2, pTemp2, pFanins[b], nWords, 0 );
+ else
+ Abc_TtSharp( pTemp2, pTemp2, pFanins[b], nWords );
+ Abc_TtOr( pTemp1, pTemp1, pTemp2, nWords );
+ }
+ // check the function
+ if ( !Abc_TtEqual( pTemp1, f, nWords ) )
+ printf( "Verification failed.\n" );
+// else
+// printf( "Verification passed.\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Finds a setset of gs to decompose f.]
+
+ Description [Returns the numbers of the decomposition functions and
+ the truth table of a function up to 4 variables.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Rsb_ManPerform( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll, int fVerbose0 )
+{
+ word * pCexes = Vec_WrdArray(p->vCexes);
+ unsigned * pPat = (unsigned *)Vec_IntArray(p->vDecPats);
+ int fVerbose = 0;//(nGs > 40);
+ Vec_Int_t * vTries = NULL;
+ unsigned uTruth;
+
+ // verify original decomposition
+ if ( Vec_IntSize(p->vFaninsOld) && Vec_IntSize(p->vFaninsOld) <= 4 )
+ {
+ word * pDivs[8];
+ int i, Entry, iCexA, iCexB;
+ Vec_IntForEachEntry( p->vFaninsOld, Entry, i )
+ pDivs[i] = g[Entry];
+ uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFaninsOld), pPat, &iCexA, &iCexB );
+// assert( uTruth != 0 );
+ if ( fVerbose )
+ {
+ printf( "Verified orig decomp with %d vars {", Vec_IntSize(p->vFaninsOld) );
+ Vec_IntForEachEntry( p->vFaninsOld, Entry, i )
+ printf( " %d", Entry );
+ printf( " }\n" );
+ }
+ if ( uTruth )
+ {
+// if ( fVerbose )
+// Rsb_DecPrintFunc( p, uTruth );
+ }
+ else
+ {
+ printf( "Verified orig decomp with %d vars {", Vec_IntSize(p->vFaninsOld) );
+ Vec_IntForEachEntry( p->vFaninsOld, Entry, i )
+ printf( " %d", Entry );
+ printf( " }\n" );
+ printf( "Verification FAILED.\n" );
+ }
+ }
+ // start tries
+if ( fVerbose )
+vTries = Vec_IntAlloc( 100 );
+ assert( nGs < nGsAll );
+ uTruth = Rsb_DecPerformInt( p, nVars, f, g, nGs, nGsAll );
+
+ if ( uTruth )
+ {
+ if ( fVerbose )
+ {
+ int i, Entry;
+ printf( "Found decomp with %d vars {", Vec_IntSize(p->vFanins) );
+ Vec_IntForEachEntry( p->vFanins, Entry, i )
+ printf( " %d", Entry );
+ printf( " }\n" );
+// Rsb_DecPrintFunc( p, uTruth );
+// Rsb_DecVerify( nVars, f, g, nGs, p->vFanins, uTruth, g[nGsAll], g[nGsAll+1] );
+ }
+ }
+ else
+ {
+ Vec_IntShrink( p->vFanins, 0 );
+ if ( fVerbose )
+ printf( "Did not find decomposition with 4 variables.\n" );
+ }
+
+if ( fVerbose )
+Rsb_DecPrintTable( pCexes, nGs, nGsAll, vTries );
+if ( fVerbose )
+Vec_IntFree( vTries );
+ if ( fVerbose && Vec_IntSize(p->vFaninsOld) && Vec_IntSize(p->vFaninsOld) <= 4 && Vec_IntSize(p->vFaninsOld) > Vec_IntSize(p->vFanins) )
+ {
+ int s = 0;
+ }
+ return uTruth;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rsb_ManPerformResub6( Rsb_Man_t * p, int nVarsAll, word uTruth, Vec_Wrd_t * vDivTruths, word * puTruth0, word * puTruth1, int fVerbose )
+{
+ word * pGs[64];
+ unsigned uTruthRes;
+ int i, nVars, nGs = Vec_WrdSize(vDivTruths);
+ for ( i = 0; i < nGs; i++ )
+ pGs[i] = Vec_WrdEntryP(vDivTruths,i);
+ uTruthRes = Rsb_DecPerformInt( p, nVarsAll, &uTruth, pGs, nGs, nGs );
+ if ( uTruthRes == 0 )
+ return 0;
+
+ if ( fVerbose )
+ Rsb_DecPrintFunc( p, uTruthRes, &uTruth, pGs, nGs, nVarsAll );
+ if ( fVerbose )
+ Rsb_DecPrintTable( Vec_WrdArray(p->vCexes), nGs, nGs, p->vTries );
+
+ nVars = Vec_IntSize(p->vFanins);
+ *puTruth0 = Abc_Tt6Stretch( uTruthRes, nVars );
+ *puTruth1 = Abc_Tt6Stretch( uTruthRes >> (1 << nVars), nVars );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rsb_ManPerformResub6Test()
+{
+ Rsb_Man_t * p;
+ Vec_Wrd_t * vDivTruths;
+ int RetValue;
+ word a = s_Truths6[0];
+ word b = s_Truths6[1];
+ word c = s_Truths6[2];
+ word d = s_Truths6[3];
+ word e = s_Truths6[4];
+ word f = s_Truths6[5];
+ word ab = a & b;
+ word cd = c & d;
+ word ef = e & f;
+ word F = ab | cd | ef;
+ word uTruth0, uTruth1;
+
+ vDivTruths = Vec_WrdAlloc( 100 );
+ Vec_WrdPush( vDivTruths, a );
+ Vec_WrdPush( vDivTruths, b );
+ Vec_WrdPush( vDivTruths, c );
+ Vec_WrdPush( vDivTruths, d );
+ Vec_WrdPush( vDivTruths, e );
+ Vec_WrdPush( vDivTruths, f );
+ Vec_WrdPush( vDivTruths, ab );
+ Vec_WrdPush( vDivTruths, cd );
+ Vec_WrdPush( vDivTruths, ef );
+
+ p = Rsb_ManAlloc( 6, 64, 4, 1 );
+
+ RetValue = Rsb_ManPerformResub6( p, 6, F, vDivTruths, &uTruth0, &uTruth1, 1 );
+
+ Rsb_ManFree( p );
+ Vec_WrdFree( vDivTruths );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bool/rsb/rsbInt.h b/src/bool/rsb/rsbInt.h
new file mode 100644
index 00000000..862ce8c7
--- /dev/null
+++ b/src/bool/rsb/rsbInt.h
@@ -0,0 +1,84 @@
+/**CFile****************************************************************
+
+ FileName [rsbInt.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Truth-table based resubstitution.]
+
+ Synopsis [Internal declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rsbInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__bool_RsbInt_h
+#define ABC__bool_RsbInt_h
+
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "misc/vec/vec.h"
+#include "misc/util/utilTruth.h"
+#include "bool/kit/kit.h"
+#include "rsb.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+// truth table computation manager
+struct Rsb_Man_t_
+{
+ // parameters
+ int nLeafMax; // the max number of leaves of a cut
+ int nDivMax; // the max number of divisors to collect
+ int nDecMax; // the max number of decompositions
+ int fVerbose; // verbosity level
+ // decomposition
+ Vec_Wrd_t * vCexes; // counter-examples
+ Vec_Int_t * vDecPats; // decomposition patterns
+ Vec_Int_t * vFanins; // the result of decomposition
+ Vec_Int_t * vFaninsOld; // original fanins
+ Vec_Int_t * vTries; // intermediate
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== rsbMan.c ==========================================================*/
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/bool/rsb/rsbMan.c b/src/bool/rsb/rsbMan.c
new file mode 100644
index 00000000..0d91cca4
--- /dev/null
+++ b/src/bool/rsb/rsbMan.c
@@ -0,0 +1,99 @@
+/**CFile****************************************************************
+
+ FileName [rsbMan.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Truth-table based resubstitution.]
+
+ Synopsis [Manager maintenance.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rsbMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rsbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Rsb_Man_t * Rsb_ManAlloc( int nLeafMax, int nDivMax, int nDecMax, int fVerbose )
+{
+ Rsb_Man_t * p;
+ assert( nLeafMax <= 20 );
+ assert( nDivMax <= 200 );
+ p = ABC_CALLOC( Rsb_Man_t, 1 );
+ p->nLeafMax = nLeafMax;
+ p->nDivMax = nDivMax;
+ p->nDecMax = nDecMax;
+ p->fVerbose = fVerbose;
+ // decomposition
+ p->vCexes = Vec_WrdAlloc( nDivMax + 150 );
+ p->vDecPats = Vec_IntAlloc( Abc_TtWordNum(nLeafMax) );
+ p->vFanins = Vec_IntAlloc( 10 );
+ p->vFaninsOld = Vec_IntAlloc( 10 );
+ p->vTries = Vec_IntAlloc( 10 );
+ return p;
+}
+void Rsb_ManFree( Rsb_Man_t * p )
+{
+ Vec_WrdFree( p->vCexes );
+ Vec_IntFree( p->vDecPats );
+ Vec_IntFree( p->vFanins );
+ Vec_IntFree( p->vFaninsOld );
+ Vec_IntFree( p->vTries );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Rsb_ManGetFanins( Rsb_Man_t * p )
+{
+ return p->vFanins;
+}
+Vec_Int_t * Rsb_ManGetFaninsOld( Rsb_Man_t * p )
+{
+ return p->vFaninsOld;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 4275912f..0072a808 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -116,6 +116,18 @@ static inline int Abc_TtHexDigitNum( int nVars ) { return nVars <= 2 ? 1 : 1 <<
SeeAlso []
***********************************************************************/
+static inline void Abc_TtClear( word * pOut, int nWords )
+{
+ int w;
+ for ( w = 0; w < nWords; w++ )
+ pOut[w] = 0;
+}
+static inline void Abc_TtFill( word * pOut, int nWords )
+{
+ int w;
+ for ( w = 0; w < nWords; w++ )
+ pOut[w] = ~(word)0;
+}
static inline void Abc_TtNot( word * pOut, int nWords )
{
int w;
@@ -142,6 +154,18 @@ static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords,
for ( w = 0; w < nWords; w++ )
pOut[w] = pIn1[w] & pIn2[w];
}
+static inline void Abc_TtSharp( word * pOut, word * pIn1, word * pIn2, int nWords )
+{
+ int w;
+ for ( w = 0; w < nWords; w++ )
+ pOut[w] = pIn1[w] & ~pIn2[w];
+}
+static inline void Abc_TtOr( word * pOut, word * pIn1, word * pIn2, int nWords )
+{
+ int w;
+ for ( w = 0; w < nWords; w++ )
+ pOut[w] = pIn1[w] | pIn2[w];
+}
static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
{
int w;
@@ -756,10 +780,10 @@ static inline int Abc_TtReadHex( word * pTruth, char * pString )
static inline void Abc_TtPrintBinary( word * pTruth, int nVars )
{
word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
- int k;
+ int k, Limit = Abc_MinInt( 64, (1 << nVars) );
assert( nVars >= 2 );
for ( pThis = pTruth; pThis < pLimit; pThis++ )
- for ( k = 0; k < 64; k++ )
+ for ( k = 0; k < Limit; k++ )
printf( "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
printf( "\n" );
}
@@ -1109,6 +1133,75 @@ static inline int Abc_TtCountOnes( word x )
SeeAlso []
***********************************************************************/
+static inline int Abc_Tt6FirstBit( word t )
+{
+ int n = 0;
+ if ( t == 0 ) return -1;
+ if ( (t & 0x00000000FFFFFFFF) == 0 ) { n += 32; t >>= 32; }
+ if ( (t & 0x000000000000FFFF) == 0 ) { n += 16; t >>= 16; }
+ if ( (t & 0x00000000000000FF) == 0 ) { n += 8; t >>= 8; }
+ if ( (t & 0x000000000000000F) == 0 ) { n += 4; t >>= 4; }
+ if ( (t & 0x0000000000000003) == 0 ) { n += 2; t >>= 2; }
+ if ( (t & 0x0000000000000001) == 0 ) { n++; }
+ return n;
+}
+static inline int Abc_Tt6LastBit( word t )
+{
+ int n = 0;
+ if ( t == 0 ) return -1;
+ if ( (t & 0xFFFFFFFF00000000) == 0 ) { n += 32; t <<= 32; }
+ if ( (t & 0xFFFF000000000000) == 0 ) { n += 16; t <<= 16; }
+ if ( (t & 0xFF00000000000000) == 0 ) { n += 8; t <<= 8; }
+ if ( (t & 0xF000000000000000) == 0 ) { n += 4; t <<= 4; }
+ if ( (t & 0xC000000000000000) == 0 ) { n += 2; t <<= 2; }
+ if ( (t & 0x8000000000000000) == 0 ) { n++; }
+ return 63-n;
+}
+static inline int Abc_TtFindFirstBit( word * pIn, int nVars )
+{
+ int w, nWords = Abc_TtWordNum(nVars);
+ for ( w = 0; w < nWords; w++ )
+ if ( pIn[w] )
+ return 64*w + Abc_Tt6FirstBit(pIn[w]);
+ return -1;
+}
+static inline int Abc_TtFindFirstZero( word * pIn, int nVars )
+{
+ int w, nWords = Abc_TtWordNum(nVars);
+ for ( w = 0; w < nWords; w++ )
+ if ( ~pIn[w] )
+ return 64*w + Abc_Tt6FirstBit(~pIn[w]);
+ return -1;
+}
+static inline int Abc_TtFindLastBit( word * pIn, int nVars )
+{
+ int w, nWords = Abc_TtWordNum(nVars);
+ for ( w = nWords - 1; w >= 0; w-- )
+ if ( pIn[w] )
+ return 64*w + Abc_Tt6LastBit(pIn[w]);
+ return -1;
+}
+static inline int Abc_TtFindLastZero( word * pIn, int nVars )
+{
+ int w, nWords = Abc_TtWordNum(nVars);
+ for ( w = nWords - 1; w >= 0; w-- )
+ if ( ~pIn[w] )
+ return 64*w + Abc_Tt6LastBit(~pIn[w]);
+ return -1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
static inline void Abc_TtReverseVars( word * pTruth, int nVars )
{
int k;
@@ -1146,6 +1239,49 @@ static inline void Abc_TtReverseBits( word * pTruth, int nVars )
}
+/**Function*************************************************************
+
+ Synopsis [Computes ISOP for 6 variables or less.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars )
+{
+ word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
+ int Var;
+ assert( nVars <= 5 );
+ assert( (uOn & ~uOnDc) == 0 );
+ if ( uOn == 0 )
+ return 0;
+ if ( uOnDc == ~(word)0 )
+ return ~(word)0;
+ assert( nVars > 0 );
+ // find the topmost var
+ for ( Var = nVars-1; Var >= 0; Var-- )
+ if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
+ break;
+ assert( Var >= 0 );
+ // cofactor
+ uOn0 = Abc_Tt6Cofactor0( uOn, Var );
+ uOn1 = Abc_Tt6Cofactor1( uOn , Var );
+ uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
+ uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
+ // solve for cofactors
+ uRes0 = Abc_Tt6Isop( uOn0 & ~uOnDc1, uOnDc0, Var );
+ uRes1 = Abc_Tt6Isop( uOn1 & ~uOnDc0, uOnDc1, Var );
+ uRes2 = Abc_Tt6Isop( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var );
+ // derive the final truth table
+ uRes2 |= (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
+ assert( (uOn & ~uRes2) == 0 );
+ assert( (uRes2 & ~uOnDc) == 0 );
+ return uRes2;
+}
+
/*=== utilTruth.c ===========================================================*/
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-10 07:11:15 +0000