summaryrefslogtreecommitdiffstats
path: root/src/sat/aig/fraigClass.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/aig/fraigClass.c')
-rw-r--r--src/sat/aig/fraigClass.c182
1 files changed, 178 insertions, 4 deletions
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++;
+ }
+ }
}
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 15:44:37 +0000