summaryrefslogtreecommitdiffstats
path: root/src/sat/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/aig')
-rw-r--r--src/sat/aig/aig.h12
-rw-r--r--src/sat/aig/aigMan.c12
-rw-r--r--src/sat/aig/fraigClass.c182
-rw-r--r--src/sat/aig/fraigCore.c2
-rw-r--r--src/sat/aig/fraigEngine.c125
-rw-r--r--src/sat/aig/fraigSim.c55
-rw-r--r--src/sat/aig/rwrTruth.c454
7 files changed, 781 insertions, 61 deletions
diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
index 55a75cf5..ee029789 100644
--- a/src/sat/aig/aig.h
+++ b/src/sat/aig/aig.h
@@ -160,6 +160,7 @@ struct Aig_Man_t_
Aig_SimInfo_t * pInfo; // random and systematic sim info for PIs
Aig_SimInfo_t * pInfoPi; // temporary sim info for the PI nodes
Aig_SimInfo_t * pInfoTemp; // temporary sim info for all nodes
+ Aig_Pattern_t * pPatMask; // the mask which shows what patterns are used
// simulation patterns
int nPiWords; // the number of words in the PI info
int nPatsMax; // the max number of patterns
@@ -169,6 +170,7 @@ struct Aig_Man_t_
// temporary data
Vec_Ptr_t * vFanouts; // temporary storage for fanouts of a node
Vec_Ptr_t * vToReplace; // the nodes to replace
+ Vec_Int_t * vClassTemp; // temporary class representatives
};
// the simulation patter
@@ -254,6 +256,7 @@ static inline int Aig_NodeWhatFanin( Aig_Node_t * pNode, Aig_Node_t * p
static inline int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); }
static inline int Aig_NodeRequiredLevel( Aig_Node_t * pNode ) { return pNode->pMan->nLevelMax + 1 - pNode->LevelR; }
+static inline unsigned * Aig_SimInfoForNodeId( Aig_SimInfo_t * p, int NodeId ) { assert( p->Type ); return p->pData + p->nWords * NodeId; }
static inline unsigned * Aig_SimInfoForNode( Aig_SimInfo_t * p, Aig_Node_t * pNode ) { assert( p->Type ); return p->pData + p->nWords * pNode->Id; }
static inline unsigned * Aig_SimInfoForPi( Aig_SimInfo_t * p, int Num ) { assert( !p->Type ); return p->pData + p->nWords * Num; }
@@ -332,15 +335,16 @@ extern Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t
extern Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan );
/*=== fraigClasses.c ==========================================================*/
extern Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfoAll );
-extern void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses );
+extern int Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses, Aig_Pattern_t * pPatMask );
+extern void Aig_ManCollectPatterns( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Aig_Pattern_t * pMask, Vec_Ptr_t * vPats );
/*=== fraigCnf.c ==========================================================*/
extern Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan );
/*=== fraigEngine.c ==========================================================*/
+extern void Aig_EngineSimulateRandomFirst( Aig_Man_t * p );
extern void Aig_EngineSimulateFirst( Aig_Man_t * p );
extern int Aig_EngineSimulate( Aig_Man_t * p );
-extern void Aig_EngineSimulateRandomFirst( Aig_Man_t * p );
/*=== fraigSim.c ==========================================================*/
-extern Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type );
+extern Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nBits, int Type );
extern void Aig_SimInfoClean( Aig_SimInfo_t * p );
extern void Aig_SimInfoRandom( Aig_SimInfo_t * p );
extern void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat );
@@ -349,6 +353,8 @@ extern void Aig_SimInfoFree( Aig_SimInfo_t * p );
extern void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll );
extern Aig_Pattern_t * Aig_PatternAlloc( int nBits );
extern void Aig_PatternClean( Aig_Pattern_t * pPat );
+extern void Aig_PatternFill( Aig_Pattern_t * pPat );
+extern int Aig_PatternCount( Aig_Pattern_t * pPat );
extern void Aig_PatternRandom( Aig_Pattern_t * pPat );
extern void Aig_PatternFree( Aig_Pattern_t * pPat );
diff --git a/src/sat/aig/aigMan.c b/src/sat/aig/aigMan.c
index 3807d28a..4c64c897 100644
--- a/src/sat/aig/aigMan.c
+++ b/src/sat/aig/aigMan.c
@@ -42,7 +42,7 @@
void Aig_ManSetDefaultParams( Aig_Param_t * pParam )
{
memset( pParam, 0, sizeof(Aig_Param_t) );
- pParam->nPatsRand = 1024; // the number of random patterns
+ pParam->nPatsRand = 4096; // the number of random patterns
pParam->nBTLimit = 99; // backtrack limit at the intermediate nodes
pParam->nSeconds = 1; // the timeout for the final miter in seconds
}
@@ -67,8 +67,8 @@ Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam )
p = ALLOC( Aig_Man_t, 1 );
memset( p, 0, sizeof(Aig_Man_t) );
p->pParam = &p->Param;
- p->nTravIds = 1;
- p->nPatsMax = 20;
+ p->nTravIds = 1;
+ p->nPatsMax = 25;
// set the defaults
*p->pParam = *pParam;
// start memory managers
@@ -84,6 +84,8 @@ Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam )
// initialize other variables
p->vFanouts = Vec_PtrAlloc( 10 );
p->vToReplace = Vec_PtrAlloc( 10 );
+ p->vClassTemp = Vec_IntAlloc( 10 );
+ p->vPats = Vec_PtrAlloc( p->nPatsMax );
return p;
}
@@ -132,6 +134,9 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vFanFans0 ) Vec_PtrFree( p->vFanFans0 );
if ( p->vFanFans1 ) Vec_PtrFree( p->vFanFans1 );
if ( p->vClasses ) Vec_VecFree( p->vClasses );
+ // patterns
+ if ( p->vPats ) Vec_PtrFree( p->vPats );
+ if ( p->pPatMask ) Aig_PatternFree( p->pPatMask );
// nodes
Aig_MemFixedStop( p->mmNodes, 0 );
Vec_PtrFree( p->vNodes );
@@ -140,6 +145,7 @@ void Aig_ManStop( Aig_Man_t * p )
// temporary
Vec_PtrFree( p->vFanouts );
Vec_PtrFree( p->vToReplace );
+ Vec_IntFree( p->vClassTemp );
Aig_TableFree( p->pTable );
free( p );
}
diff --git a/src/sat/aig/fraigClass.c b/src/sat/aig/fraigClass.c
index 2f2d3e0c..a8df9a72 100644
--- a/src/sat/aig/fraigClass.c
+++ b/src/sat/aig/fraigClass.c
@@ -80,7 +80,7 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
}
}
stmm_free_table( tSim2Node );
-
+/*
// print the classes
{
Vec_Ptr_t * vVec;
@@ -93,6 +93,8 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
printf( "%d ", Vec_PtrSize(vVec) );
printf( "\n" );
}
+*/
+ printf( "Classes = %6d. Pairs = %6d.\n", Vec_VecSize(vClasses), Vec_VecSizeSize(vClasses) - Vec_VecSize(vClasses) );
return vClasses;
}
@@ -115,14 +117,86 @@ unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase )
uKey = 0;
if ( fPhase )
for ( i = 0; i < nWords; i++ )
- uKey ^= Primes[i%10] * pData[i];
+ uKey ^= i * Primes[i%10] * pData[i];
else
for ( i = 0; i < nWords; i++ )
- uKey ^= Primes[i%10] * ~pData[i];
+ uKey ^= i * Primes[i%10] * ~pData[i];
return uKey;
}
+
+/**Function*************************************************************
+
+ Synopsis [Splits the equivalence class.]
+
+ Description [Given an equivalence class (vClass) and the simulation info,
+ split the class into two based on the info.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManSplitClass( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Int_t * vClass, Vec_Int_t * vClass2, Aig_Pattern_t * pPat )
+{
+ int NodeId, i, k, w;
+ Aig_Node_t * pRoot, * pTemp;
+ unsigned * pRootData, * pTempData;
+ assert( Vec_IntSize(vClass) > 1 );
+ assert( pInfo->nPatsCur == pPat->nBits );
+// printf( "Class = %5d. --> ", Vec_IntSize(vClass) );
+ // clear storage for the new classes
+ Vec_IntClear( vClass2 );
+ // get the root member of the class
+ pRoot = Aig_ManNode( p, Vec_IntEntry(vClass, 0) );
+ pRootData = Aig_SimInfoForNode( pInfo, pRoot );
+ // sort the class members:
+ // (1) with the same siminfo as pRoot remain in vClass
+ // (2) nodes with other siminfo go to vClass2
+ k = 1;
+ Vec_IntForEachEntryStart( vClass, NodeId, i, 1 )
+ {
+ NodeId = Vec_IntEntry(vClass, i);
+ pTemp = Aig_ManNode( p, NodeId );
+ pTempData = Aig_SimInfoForNode( pInfo, pTemp );
+ if ( pRoot->fPhase == pTemp->fPhase )
+ {
+ for ( w = 0; w < pInfo->nWords; w++ )
+ if ( pRootData[w] != pTempData[w] )
+ break;
+ if ( w == pInfo->nWords ) // the same info
+ Vec_IntWriteEntry( vClass, k++, NodeId );
+ else
+ {
+ Vec_IntPush( vClass2, NodeId );
+ // record the diffs if they are not distinguished by the first pattern
+ if ( ((pRootData[0] ^ pTempData[0]) & 1) == 0 )
+ for ( w = 0; w < pInfo->nWords; w++ )
+ pPat->pData[w] |= (pRootData[w] ^ pTempData[w]);
+ }
+ }
+ else
+ {
+ for ( w = 0; w < pInfo->nWords; w++ )
+ if ( pRootData[w] != ~pTempData[w] )
+ break;
+ if ( w == pInfo->nWords ) // the same info
+ Vec_IntWriteEntry( vClass, k++, NodeId );
+ else
+ {
+ Vec_IntPush( vClass2, NodeId );
+ // record the diffs if they are not distinguished by the first pattern
+ if ( ((pRootData[0] ^ ~pTempData[0]) & 1) == 0 )
+ for ( w = 0; w < pInfo->nWords; w++ )
+ pPat->pData[w] |= (pRootData[w] ^ ~pTempData[w]);
+ }
+ }
+ }
+ Vec_IntShrink( vClass, k );
+// printf( "Class1 = %5d. Class2 = %5d.\n", Vec_IntSize(vClass), Vec_IntSize(vClass2) );
+}
+
/**Function*************************************************************
Synopsis [Updates the equivalence classes using the simulation info.]
@@ -135,8 +209,108 @@ unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase )
SeeAlso []
***********************************************************************/
-void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses )
+int Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses, Aig_Pattern_t * pPatMask )
+{
+ Vec_Ptr_t * vClass;
+ int i, k, fSplit = 0;
+ assert( Vec_VecSize(vClasses) > 0 );
+ // collect patterns that lead to changes
+ Aig_PatternClean( pPatMask );
+ // split the classes using the new symmetry info
+ Vec_VecForEachLevel( vClasses, vClass, i )
+ {
+ if ( i == 0 )
+ continue;
+ // split vClass into two parts (vClass and vClassTemp)
+ Aig_ManSplitClass( p, pInfo, (Vec_Int_t *)vClass, p->vClassTemp, pPatMask );
+ // check if there is any splitting
+ if ( Vec_IntSize(p->vClassTemp) > 0 )
+ fSplit = 1;
+ // skip the new class if it is empty or trivial
+ if ( Vec_IntSize(p->vClassTemp) < 2 )
+ continue;
+ // consider replacing the current class with the new one
+ if ( Vec_PtrSize(vClass) == 1 )
+ {
+ assert( vClasses->pArray[i] == vClass );
+ vClasses->pArray[i] = p->vClassTemp;
+ p->vClassTemp = (Vec_Int_t *)vClass;
+ i--;
+ continue;
+ }
+ // add the new non-trival class in the end
+ Vec_PtrPush( (Vec_Ptr_t *)vClasses, p->vClassTemp );
+ p->vClassTemp = Vec_IntAlloc( 10 );
+ }
+ // free trivial classes
+ k = 0;
+ Vec_VecForEachLevel( vClasses, vClass, i )
+ {
+ assert( Vec_PtrSize(vClass) > 0 );
+ if ( Vec_PtrSize(vClass) == 1 )
+ Vec_PtrFree(vClass);
+ else
+ vClasses->pArray[k++] = vClass;
+ }
+ Vec_PtrShrink( (Vec_Ptr_t *)vClasses, k );
+ // catch the patterns which led to splitting
+ printf( "Classes = %6d. Pairs = %6d. Patterns = %3d.\n",
+ Vec_VecSize(vClasses),
+ Vec_VecSizeSize(vClasses) - Vec_VecSize(vClasses),
+ Vec_PtrSize(p->vPats) );
+ return fSplit;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects useful patterns.]
+
+ Description [If the flag fAddToVector is 1, creates and adds new patterns
+ to the internal storage of patterns.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManCollectPatterns( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Aig_Pattern_t * pMask, Vec_Ptr_t * vPats )
{
+ Aig_SimInfo_t * pInfoRes = p->pInfo;
+ Aig_Pattern_t * pPatNew;
+ Aig_Node_t * pNode;
+ int i, k;
+
+ assert( Aig_InfoHasBit(pMask->pData, 0) == 0 );
+ for ( i = 0; i < pMask->nBits; i++ )
+ {
+ if ( vPats && Vec_PtrSize(vPats) >= p->nPatsMax )
+ break;
+ if ( i == 0 || Aig_InfoHasBit(pMask->pData, i) )
+ {
+ // expand storage if needed
+ if ( pInfoRes->nPatsCur == pInfoRes->nPatsMax )
+ Aig_SimInfoResize( pInfoRes );
+ // create a new pattern
+ if ( vPats )
+ {
+ pPatNew = Aig_PatternAlloc( Aig_ManPiNum(p) );
+ Aig_PatternClean( pPatNew );
+ }
+ // go through the PIs
+ Aig_ManForEachPi( p, pNode, k )
+ {
+ if ( Aig_InfoHasBit( Aig_SimInfoForNode(pInfo, pNode), i ) )
+ {
+ Aig_InfoSetBit( Aig_SimInfoForPi(pInfoRes, k), pInfoRes->nPatsCur );
+ if ( vPats ) Aig_InfoSetBit( pPatNew->pData, k );
+ }
+ }
+ // store the new pattern
+ if ( vPats ) Vec_PtrPush( vPats, pPatNew );
+ // increment the number of patterns stored
+ pInfoRes->nPatsCur++;
+ }
+ }
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c
index e7df1335..decf05ee 100644
--- a/src/sat/aig/fraigCore.c
+++ b/src/sat/aig/fraigCore.c
@@ -68,6 +68,8 @@ Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan )
// create equivalence classes
Aig_EngineSimulateRandomFirst( pMan );
+ // reduce equivalence classes using simulation
+ Aig_EngineSimulateFirst( pMan );
return RetValue;
}
diff --git a/src/sat/aig/fraigEngine.c b/src/sat/aig/fraigEngine.c
index 6214bf3b..17468e8f 100644
--- a/src/sat/aig/fraigEngine.c
+++ b/src/sat/aig/fraigEngine.c
@@ -30,6 +30,39 @@
/**Function*************************************************************
+ Synopsis [Simulates all nodes using random simulation for the first time.]
+
+ Description [Assigns the original simulation info and the storage for the
+ future simulation info.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_EngineSimulateRandomFirst( Aig_Man_t * p )
+{
+ Aig_SimInfo_t * pInfoPi, * pInfoAll;
+ assert( !p->pInfo && !p->pInfoTemp );
+ // create random PI info
+ pInfoPi = Aig_SimInfoAlloc( Aig_ManPiNum(p), p->pParam->nPatsRand, 0 );
+ Aig_SimInfoRandom( pInfoPi );
+ // allocate sim info for all nodes
+ pInfoAll = Aig_SimInfoAlloc( Aig_ManNodeNum(p), p->pParam->nPatsRand, 1 );
+ // simulate though the circuit
+ Aig_ManSimulateInfo( p, pInfoPi, pInfoAll );
+ // detect classes
+ p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
+ Aig_SimInfoFree( pInfoAll );
+ // save simulation info
+ p->pInfo = pInfoPi;
+ p->pInfoPi = Aig_SimInfoAlloc( Aig_ManPiNum(p), Aig_ManPiNum(p)+1, 0 );
+ p->pInfoTemp = Aig_SimInfoAlloc( Aig_ManNodeNum(p), Aig_ManPiNum(p)+1, 1 );
+ p->pPatMask = Aig_PatternAlloc( Aig_ManPiNum(p)+1 );
+}
+
+/**Function*************************************************************
+
Synopsis [Starts the simulation engine for the first time.]
Description [Tries several random patterns and their distance-1
@@ -43,15 +76,55 @@
void Aig_EngineSimulateFirst( Aig_Man_t * p )
{
Aig_Pattern_t * pPat;
- int i;
- assert( Vec_PtrSize(p->vPats) == 0 );
- for ( i = 0; i < p->nPatsMax; i++ )
+ int i, Counter;
+
+ // simulate the pattern of all zeros
+ pPat = Aig_PatternAlloc( Aig_ManPiNum(p) );
+ Aig_PatternClean( pPat );
+ Vec_PtrPush( p->vPats, pPat );
+ if ( !Aig_EngineSimulate( p ) )
+ return;
+
+ // simulate the pattern of all ones
+ pPat = Aig_PatternAlloc( Aig_ManPiNum(p) );
+ Aig_PatternFill( pPat );
+ Vec_PtrPush( p->vPats, pPat );
+ if ( !Aig_EngineSimulate( p ) )
+ return;
+
+ // simulate random until the number of new patterns is reasonable
+ do {
+ // generate random PI siminfo
+ Aig_SimInfoRandom( p->pInfoPi );
+ // simulate this info
+ Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
+ // split the classes and collect the new patterns
+ if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) )
+ Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, NULL );
+ if ( Vec_VecSize(p->vClasses) == 0 )
+ return;
+ // count the number of useful patterns
+ Counter = Aig_PatternCount(p->pPatMask);
+ }
+ while ( Counter > p->nPatsMax/2 );
+
+ // perform targetted simulation
+ for ( i = 0; i < 3; i++ )
{
- pPat = Aig_PatternAlloc( Aig_ManPiNum(p) );
- Aig_PatternRandom( pPat );
- Vec_PtrPush( p->vPats, pPat );
- if ( !Aig_EngineSimulate( p ) )
+ assert( Vec_PtrSize(p->vPats) == 0 );
+ // generate random PI siminfo
+ Aig_SimInfoRandom( p->pInfoPi );
+ // simulate this info
+ Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
+ // split the classes and collect the new patterns
+ if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) )
+ Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, p->vPats );
+ if ( Vec_VecSize(p->vClasses) == 0 )
return;
+ // simulate the remaining patters
+ if ( Vec_PtrSize(p->vPats) > 0 )
+ if ( !Aig_EngineSimulate( p ) )
+ return;
}
}
@@ -79,51 +152,21 @@ int Aig_EngineSimulate( Aig_Man_t * p )
{
// get the pattern and create new siminfo
pPat = Vec_PtrPop(p->vPats);
+ assert( pPat->nBits == Aig_ManPiNum(p) );
// create the new siminfo
Aig_SimInfoFromPattern( p->pInfoPi, pPat );
- // free the patter
+ // free the pattern
Aig_PatternFree( pPat );
// simulate this info
Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
// split the classes and collect the new patterns
- Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses );
+ if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) )
+ Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, p->vPats );
}
return Vec_VecSize(p->vClasses) > 0;
}
-/**Function*************************************************************
-
- Synopsis [Simulates all nodes using random simulation for the first time.]
-
- Description [Assigns the original simulation info and the storage for the
- future simulation info.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_EngineSimulateRandomFirst( Aig_Man_t * p )
-{
- Aig_SimInfo_t * pInfoPi, * pInfoAll;
- assert( !p->pInfo && !p->pInfoTemp );
- // create random PI info
- pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 );
- Aig_SimInfoRandom( pInfoPi );
- // allocate sim info for all nodes
- pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 );
- // simulate though the circuit
- Aig_ManSimulateInfo( p, pInfoPi, pInfoAll );
- // detect classes
- p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
- Aig_SimInfoFree( pInfoAll );
- // save simulation info
- p->pInfo = pInfoPi;
- p->pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->vPis->nSize), 0 );
- p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 );
-}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/aig/fraigSim.c b/src/sat/aig/fraigSim.c
index 415b6918..6d4f214c 100644
--- a/src/sat/aig/fraigSim.c
+++ b/src/sat/aig/fraigSim.c
@@ -80,7 +80,7 @@ void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t
pDataAnd[k] = pData0[k] & pData1[k];
}
// derive the PO siminfo
- Aig_ManForEachPi( p, pNode, i )
+ Aig_ManForEachPo( p, pNode, i )
{
pDataPo = Aig_SimInfoForNode( pInfoAll, pNode );
pDataAnd = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) );
@@ -106,16 +106,17 @@ void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t
SeeAlso []
***********************************************************************/
-Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type )
+Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nBits, int Type )
{
Aig_SimInfo_t * p;
p = ALLOC( Aig_SimInfo_t, 1 );
memset( p, 0, sizeof(Aig_SimInfo_t) );
p->Type = Type;
p->nNodes = nNodes;
- p->nWords = nWords;
- p->nPatsMax = nWords * sizeof(unsigned) * 8;
- p->pData = ALLOC( unsigned, nNodes * nWords );
+ p->nWords = Aig_BitWordNum(nBits);
+ p->nPatsCur = nBits;
+ p->nPatsMax = p->nWords * sizeof(unsigned) * 8;
+ p->pData = ALLOC( unsigned, nNodes * p->nWords );
return p;
}
@@ -161,7 +162,6 @@ void Aig_SimInfoRandom( Aig_SimInfo_t * p )
pData = p->pData + p->nWords * i;
*pData <<= 1;
}
- p->nPatsCur = p->nPatsMax;
}
/**Function*************************************************************
@@ -180,8 +180,8 @@ void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat )
unsigned * pData;
int i, k;
assert( p->Type == 0 );
- assert( p->nNodes == pPat->nBits );
- for ( i = 0; i < p->nNodes; i++ )
+ assert( p->nPatsCur == pPat->nBits+1 );
+ for ( i = 0; i < p->nPatsCur; i++ )
{
// get the pointer to the bitdata for node i
pData = p->pData + p->nWords * i;
@@ -192,8 +192,8 @@ void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat )
else
for ( k = 0; k < p->nWords; k++ )
pData[k] = 0;
- // flip one bit
- Aig_InfoXorBit( pData, i );
+ // flip one bit, starting from the first pattern
+ if ( i ) Aig_InfoXorBit( pData, i-1 );
}
}
@@ -285,6 +285,22 @@ void Aig_PatternClean( Aig_Pattern_t * pPat )
/**Function*************************************************************
+ Synopsis [Cleans the pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_PatternFill( Aig_Pattern_t * pPat )
+{
+ memset( pPat->pData, 0xff, sizeof(unsigned) * pPat->nWords );
+}
+
+/**Function*************************************************************
+
Synopsis [Sets the random pattern.]
Description []
@@ -303,6 +319,25 @@ void Aig_PatternRandom( Aig_Pattern_t * pPat )
/**Function*************************************************************
+ Synopsis [Counts the number of 1s in the pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_PatternCount( Aig_Pattern_t * pPat )
+{
+ int i, Counter = 0;
+ for ( i = 0; i < pPat->nBits; i++ )
+ Counter += Aig_InfoHasBit( pPat->pData, i );
+ return Counter;
+}
+
+/**Function*************************************************************
+
Synopsis [Deallocates the pattern.]
Description []
diff --git a/src/sat/aig/rwrTruth.c b/src/sat/aig/rwrTruth.c
new file mode 100644
index 00000000..2c402184
--- /dev/null
+++ b/src/sat/aig/rwrTruth.c
@@ -0,0 +1,454 @@
+/**CFile****************************************************************
+
+ FileName [rwrTruth.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rwrTruth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+/* The code in this file was written with portability to 64-bits in mind.
+ The type "unsigned" is assumed to be 32-bit on any platform.
+*/
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define ABCTMAX 8 // the max number of vars
+
+typedef struct Aig_Truth_t_ Aig_Truth_t;
+struct Aig_Truth_t_
+{
+ short nVars; // the number of variables
+ short nWords; // the number of 32-bit words
+ unsigned Truth[1<<(ABCTMAX-5)]; // the truth table
+ unsigned Cofs[2][1<<(ABCTMAX-6)]; // the truth table of cofactors
+ unsigned Data[4][1<<(ABCTMAX-7)]; // the truth table of cofactors
+ short Counts[ABCTMAX][2]; // the minterm counters
+ Aig_Node_t * pLeaves[ABCTMAX]; // the pointers to leaves
+ Aig_Man_t * pMan; // the AIG manager
+};
+
+static void Aig_TruthCount( Aig_Truth_t * p );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Creates the function given the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Truth_t * Aig_TruthCreate( int nVars, unsigned * pTruth, Aig_Node_t ** pLeaves )
+{
+ Aig_Truth_t * p;
+ int i;
+ p = ALLOC( Aig_Truth_t, 1 );
+ memset( p, 0, sizeof(Aig_Truth_t) );
+ p->nVars = nVars;
+ p->nWords = (nVars < 5)? 1 : (1 << (nVars-5));
+ for ( i = 0; i < p->nWords; i++ )
+ p->Truth[i] = pTruth[i];
+ if ( nVars < 5 )
+ p->Truth[0] &= (~0u >> (32-(1<<nVars)));
+ for ( i = 0; i < p->nVars; i++ )
+ p->pLeaves[i] = pLeaves[i];
+ Aig_TruthCount( p );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of miterms in the cofactors.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Aig_WordCountOnes( unsigned val )
+{
+ val = (val & 0x55555555) + ((val>>1) & 0x55555555);
+ val = (val & 0x33333333) + ((val>>2) & 0x33333333);
+ val = (val & 0x0F0F0F0F) + ((val>>4) & 0x0F0F0F0F);
+ val = (val & 0x00FF00FF) + ((val>>8) & 0x00FF00FF);
+ return (val & 0x0000FFFF) + (val>>8);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of miterms in the cofactors.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TruthCount( Aig_Truth_t * p )
+{
+ static unsigned Masks[5][2] = {
+ { 0x33333333, 0xAAAAAAAA },
+ { 0x55555555, 0xCCCCCCCC },
+ { 0x0F0F0F0F, 0xF0F0F0F0 },
+ { 0x00FF00FF, 0xFF00FF00 },
+ { 0x0000FFFF, 0xFFFF0000 }
+ };
+
+ int i, k;
+ assert( p->Counts[0][0] == 0 && p->Counts[0][1] == 0 );
+ for ( i = 0; i < p->nVars; i++ )
+ {
+ p->Counts[i][0] = p->Counts[i][1] = 0;
+ if ( i < 5 )
+ {
+ for ( k = 0; k < p->nWords; k++ )
+ {
+ p->Counts[i][0] += Aig_WordCountOnes( p->Truth[k] & Masks[i][0] );
+ p->Counts[i][1] += Aig_WordCountOnes( p->Truth[k] & Masks[i][1] );
+ }
+ }
+ else
+ {
+ for ( k = 0; k < p->nWords; k++ )
+ if ( i & (1 << (k-5)) )
+ p->Counts[i][1] += Aig_WordCountOnes( p->Truth[k] );
+ else
+ p->Counts[i][0] += Aig_WordCountOnes( p->Truth[k] );
+ }
+ }
+/*
+ // normalize the variables
+ for ( i = 0; i < p->nVars; i++ )
+ if ( p->Counts[i][0] > p->Counts[i][1] )
+ {
+ k = p->Counts[i][0];
+ p->Counts[i][0] = p->Counts[i][1];
+ p->Counts[i][1] = k;
+ p->pLeaves[i] = Aig_Not( p->pLeaves[i] );
+ }
+*/
+}
+
+/**Function*************************************************************
+
+ Synopsis [Extracts one part of the bitstring.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Aig_WordGetPart( unsigned * p, int Start, int Size )
+{
+ return (p[Start/5] >> (Start%32)) & (~0u >> (32-Size));
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts one part of the bitstring.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Aig_WordSetPart( unsigned * p, int Start, unsigned Part )
+{
+ p[Start/5] |= (Part << (Start%32));
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cofactor with respect to one variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TruthCofactor( int Var, int Pol, int nVars, unsigned * pTruth, unsigned * pResult )
+{
+ if ( Var < 5 )
+ {
+ int nPartSize = ( 1 << Var );
+ int nParts = ( 1 << (nVars-Var-1) );
+ unsigned uPart;
+ int i;
+ for ( i = 0; i < nParts; i++ )
+ {
+ uPart = Aig_WordGetPart( pTruth, (2*i+Pol)*nPartSize, nPartSize );
+ Aig_WordSetPart( pResult, i*nPartSize, uPart );
+ }
+ if ( nVars <= 5 )
+ pResult[0] &= (~0u >> (32-(1<<(nVars-1))));
+ }
+ else
+ {
+ int nWords = (1 << (nVars-5));
+ int i, k = 0;
+ for ( i = 0; i < nWords; i++ )
+ if ( (i & (1 << (Var-5))) == Pol )
+ pResult[k++] = pTruth[i];
+ assert( k == nWords/2 );
+ }
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes the BDD of the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Aig_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int Shift, int nVars, int iVar )
+{
+ DdNode * bCof0, * bCof1, * bRes;
+ if ( nVars == 1 )
+ return Cudd_NotCond( Cudd_ReadOne(dd), !Aig_WordGetPart(pTruth, Shift, 1) );
+ if ( nVars == 3 )
+ {
+ unsigned char * pChar = ((char *)pTruth) + Shift/8;
+ assert( Shift % 8 == 0 );
+ if ( *pChar == 0 )
+ return Cudd_ReadLogicZero(dd);
+ if ( *pChar == 0xFF )
+ return Cudd_ReadOne(dd);
+ }
+ if ( nVars == 5 )
+ {
+ unsigned * pWord = pTruth + Shift/32;
+ assert( Shift % 32 == 0 );
+ if ( *pWord == 0 )
+ return Cudd_ReadLogicZero(dd);
+ if ( *pWord == 0xFFFFFFFF )
+ return Cudd_ReadOne(dd);
+ }
+ bCof0 = Aig_TruthToBdd_rec( dd, pTruth, Shift, nVars-1, iVar+1 ); Cudd_Ref( bCof0 );
+ bCof1 = Aig_TruthToBdd_rec( dd, pTruth, Shift + (1 << (nVars-1)), nVars-1, iVar+1 ); Cudd_Ref( bCof1 );
+ bRes = Cudd_bddIte( dd, Cudd_bddIthVar(dd, iVar), bCof1, bCof0 ); Cudd_Ref( bRes );
+ Cudd_RecursiveDeref( dd, bCof0 );
+ Cudd_RecursiveDeref( dd, bCof1 );
+ Cudd_Deref( bRes );
+ return bRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the BDD of the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Aig_TruthToBdd( DdManager * dd, Aig_Truth_t * p )
+{
+ return Aig_TruthToBdd_rec( dd, p->Truth, 0, p->nVars, 0 );
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Compare bistrings.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Aig_WordCompare( unsigned * p0, unsigned * p1, int nWords )
+{
+ int i;
+ for ( i = 0; i < nWords; i++ )
+ if ( p0[i] != p1[i] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compare bistrings.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Aig_WordCompareCompl( unsigned * p0, unsigned * p1, int nWords )
+{
+ int i;
+ for ( i = 0; i < nWords; i++ )
+ if ( p0[i] != ~p1[i] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cofactor with respect to one variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TruthReplaceByCofactor( Aig_Truth_t * p, int iVar, unsigned * pTruth )
+{
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cofactor with respect to one variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Node_t * Aig_TruthDecompose( Aig_Truth_t * p )
+{
+ Aig_Node_t * pVar;
+ int nOnesCof = ( 1 << (p->nVars-1) );
+ int nWordsCof = (p->nWords == 1 ? 1 : p->nWords/2);
+ int i;
+
+ // check for constant function
+ if ( p->nVars == 0 )
+ return Aig_NotCond( Aig_ManConst1(p->pMan), (p->Truth[0]&1)==0 );
+
+ // count the number of minterms in the cofactors
+ Aig_TruthCount( p );
+
+ // remove redundant variables and EXORs
+ for ( i = p->nVars - 1; i >= 0; i-- )
+ {
+ if ( p->Counts[i][0] == p->Counts[i][1] )
+ {
+ // compute cofactors
+ Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] );
+ Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] );
+ if ( Aig_WordCompare( p->Cofs[0], p->Cofs[1], nWordsCof ) )
+ { // equal
+ // remove redundant variable
+ Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] );
+ return Aig_TruthDecompose( p );
+ }
+ }
+ // check the case of EXOR
+ if ( p->Counts[i][0] == nOnesCof - p->Counts[i][1] )
+ {
+ // compute cofactors
+ Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] );
+ Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] );
+ if ( Aig_WordCompareCompl( p->Cofs[0], p->Cofs[1], nWordsCof ) )
+ { // equal
+ pVar = p->pLeaves[i];
+ // remove redundant variable
+ Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] );
+ // F = x' * F0 + x * F1 = x <+> F0 assuming that F0 == ~F1
+ return Aig_Xor( p->pMan, pVar, Aig_TruthDecompose( p ) );
+ }
+ }
+ }
+
+ // process variables with constant cofactors
+ for ( i = p->nVars - 1; i >= 0; i-- )
+ {
+ if ( p->Counts[i][0] != 0 && p->Counts[i][1] != 0 &&
+ p->Counts[i][0] != nOnesCof && p->Counts[i][1] != nOnesCof )
+ continue;
+ pVar = p->pLeaves[i];
+ if ( p->Counts[i][0] == 0 )
+ {
+ Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] );
+ // remove redundant variable
+ Aig_TruthReplaceByCofactor( p, i, p->Cofs[1] );
+ // F = x' * 0 + x * F1 = x * F1
+ return Aig_And( p->pMan, pVar, Aig_TruthDecompose( p ) );
+ }
+ if ( p->Counts[i][1] == 0 )
+ {
+ Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] );
+ // remove redundant variable
+ Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] );
+ // F = x' * F0 + x * 0 = x' * F0
+ return Aig_And( p->pMan, Aig_Not(pVar), Aig_TruthDecompose( p ) );
+ }
+ if ( p->Counts[i][0] == nOnesCof )
+ {
+ Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] );
+ // remove redundant variable
+ Aig_TruthReplaceByCofactor( p, i, p->Cofs[1] );
+ // F = x' * 1 + x * F1 = x' + F1
+ return Aig_Or( p->pMan, Aig_Not(pVar), Aig_TruthDecompose( p ) );
+ }
+ if ( p->Counts[i][1] == nOnesCof )
+ {
+ Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] );
+ // remove redundant variable
+ Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] );
+ // F = x' * F0 + x * 1 = x + F0
+ return Aig_Or( p->pMan, pVar, Aig_TruthDecompose( p ) );
+ }
+ assert( 0 );
+ }
+
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 17:45:51 +0000