summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw/sswUnique.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw/sswUnique.c')
-rw-r--r--src/aig/ssw/sswUnique.c155
1 files changed, 41 insertions, 114 deletions
diff --git a/src/aig/ssw/sswUnique.c b/src/aig/ssw/sswUnique.c
index 888ed3da..0d9b016f 100644
--- a/src/aig/ssw/sswUnique.c
+++ b/src/aig/ssw/sswUnique.c
@@ -30,83 +30,39 @@
/**Function*************************************************************
- Synopsis [Returns the result of merging the two vectors.]
+ Synopsis [Performs computation of signal correspondence with constraints.]
- Description [Assumes that the vectors are sorted in the increasing order.]
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-static inline void Vec_PtrTwoMerge( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
+void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
{
- Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
- Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
- Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
- Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
- Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
- Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) );
- pBeg = (Aig_Obj_t **)vArr->pArray;
- while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ Aig_Obj_t * pObjLo, * pObj0, * pObj1;
+ int i;
+ if ( p->vDiffPairs == NULL )
+ p->vDiffPairs = Vec_IntAlloc( Saig_ManRegNum(p->pAig) );
+ Vec_IntClear( p->vDiffPairs );
+ Saig_ManForEachLo( p->pAig, pObjLo, i )
{
- if ( (*pBeg1)->Id == (*pBeg2)->Id )
- *pBeg++ = *pBeg1++, pBeg2++;
- else if ( (*pBeg1)->Id < (*pBeg2)->Id )
- *pBeg++ = *pBeg1++;
+ pObj0 = Ssw_ObjFrame( p, pObjLo, 0 );
+ pObj1 = Ssw_ObjFrame( p, pObjLo, 1 );
+ if ( pObj0 == pObj1 )
+ Vec_IntPush( p->vDiffPairs, 0 );
+ else if ( pObj0 == Aig_Not(pObj1) )
+ Vec_IntPush( p->vDiffPairs, 1 );
else
- *pBeg++ = *pBeg2++;
+ {
+ // assume that if the nodes are structurally different
+ // they can also be functionally different
+ Vec_IntPush( p->vDiffPairs, 1 );
+ }
}
- while ( pBeg1 < pEnd1 )
- *pBeg++ = *pBeg1++;
- while ( pBeg2 < pEnd2 )
- *pBeg++ = *pBeg2++;
- vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
- assert( vArr->nSize <= vArr->nCap );
- assert( vArr->nSize >= vArr1->nSize );
- assert( vArr->nSize >= vArr2->nSize );
}
-/**Function*************************************************************
-
- Synopsis [Returns the result of merging the two vectors.]
-
- Description [Assumes that the vectors are sorted in the increasing order.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Vec_PtrTwoCommon( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
-{
- Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
- Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
- Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
- Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
- Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
- Vec_PtrGrow( vArr, AIG_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
- pBeg = (Aig_Obj_t **)vArr->pArray;
- while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
- {
- if ( (*pBeg1)->Id == (*pBeg2)->Id )
- *pBeg++ = *pBeg1++, pBeg2++;
- else if ( (*pBeg1)->Id < (*pBeg2)->Id )
-// *pBeg++ = *pBeg1++;
- pBeg1++;
- else
-// *pBeg++ = *pBeg2++;
- pBeg2++;
- }
-// while ( pBeg1 < pEnd1 )
-// *pBeg++ = *pBeg1++;
-// while ( pBeg2 < pEnd2 )
-// *pBeg++ = *pBeg2++;
- vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
- assert( vArr->nSize <= vArr->nCap );
- assert( vArr->nSize <= vArr1->nSize );
- assert( vArr->nSize <= vArr2->nSize );
-}
/**Function*************************************************************
@@ -123,56 +79,32 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
{
int fVerbose = 0;
Aig_Obj_t * ppObjs[2], * pTemp;
- Vec_Ptr_t * vSupp, * vSupp2;
- int i, k, Value0, Value1, RetValue;
- assert( p->pPars->nFramesK > 1 );
+ int i, k, Value0, Value1, RetValue, fFeasible;
- vSupp = Vec_PtrAlloc( 100 );
- vSupp2 = Vec_PtrAlloc( 100 );
- Vec_PtrClear( p->vCommon );
+ assert( p->pPars->nFramesK > 1 );
+ assert( p->vDiffPairs && Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) );
// compute the first support in terms of LOs
ppObjs[0] = pRepr;
ppObjs[1] = pObj;
- Aig_SupportNodes( p->pAig, ppObjs, 2, vSupp );
- // modify support to be in terms of LIs
+ Aig_SupportNodes( p->pAig, ppObjs, 2, p->vCommon );
+ // keep only LOs
+ RetValue = Vec_PtrSize( p->vCommon );
+ fFeasible = 0;
k = 0;
- Vec_PtrForEachEntry( vSupp, pTemp, i )
+ Vec_PtrForEachEntry( p->vCommon, pTemp, i )
if ( Saig_ObjIsLo(p->pAig, pTemp) )
- Vec_PtrWriteEntry( vSupp, k++, Saig_ObjLoToLi(p->pAig, pTemp) );
- Vec_PtrShrink( vSupp, k );
- // compute the support of support
- Aig_SupportNodes( p->pAig, (Aig_Obj_t **)Vec_PtrArray(vSupp), Vec_PtrSize(vSupp), vSupp2 );
- // return support to LO
- Vec_PtrForEachEntry( vSupp, pTemp, i )
- Vec_PtrWriteEntry( vSupp, i, Saig_ObjLiToLo(p->pAig, pTemp) );
- // find the number of common vars
- Vec_PtrSort( vSupp, Aig_ObjCompareIdIncrease );
- Vec_PtrSort( vSupp2, Aig_ObjCompareIdIncrease );
- Vec_PtrTwoCommon( vSupp, vSupp2, p->vCommon );
-/*
- {
- Vec_Ptr_t * vNew = Vec_PtrDup(vSupp);
- Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
- if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp) )
- printf( "Not unique!\n" );
- }
- {
- Vec_Ptr_t * vNew = Vec_PtrDup(vSupp2);
- Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
- if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp2) )
- printf( "Not unique!\n" );
- }
- {
- Vec_Ptr_t * vNew = Vec_PtrDup(p->vCommon);
- Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
- if ( Vec_PtrSize(vNew) != Vec_PtrSize(p->vCommon) )
- printf( "Not unique!\n" );
- }
-*/
+ {
+ Vec_PtrWriteEntry( p->vCommon, k++, pTemp );
+ if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjPioNum(pTemp) - Saig_ManPiNum(p->pAig)) )
+ fFeasible = 1;
+ }
+ Vec_PtrShrink( p->vCommon, k );
+
if ( fVerbose )
- printf( "Node = %5d : One = %3d. Two = %3d. Common = %3d. ",
- Aig_ObjId(pObj), Vec_PtrSize(vSupp), Vec_PtrSize(vSupp2), Vec_PtrSize(p->vCommon) );
+ printf( "Node = %5d : Supp = %3d. Regs = %3d. Feasible = %s. ",
+ Aig_ObjId(pObj), RetValue, Vec_PtrSize(p->vCommon),
+ fFeasible? "yes": "no " );
// check the current values
RetValue = 1;
@@ -185,14 +117,10 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
if ( fVerbose )
printf( "%d", Value0 ^ Value1 );
}
- if ( Vec_PtrSize(p->vCommon) == 0 )
- RetValue = 0;
if ( fVerbose )
printf( "\n" );
- Vec_PtrFree( vSupp );
- Vec_PtrFree( vSupp2 );
- return RetValue;
+ return RetValue && fFeasible;
}
/**Function*************************************************************
@@ -227,11 +155,10 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int
// printf( "Skipped\n" );
return 0;
}
- p->nUniques++;
// create CNF
- Ssw_CnfNodeAddToSolver( p, Aig_Regular(pTotal) );
+ Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pTotal) );
// add output constraint
- pLits[0] = toLitCond( Ssw_ObjSatNum(p,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) );
+ pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) );
/*
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
assert( RetValue );
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-18 19:20:57 +0000