summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaAiger.c2
-rw-r--r--src/aig/gia/giaDup.c5
-rw-r--r--src/aig/gia/giaHash.c34
-rw-r--r--src/aig/gia/giaRex.c2
-rw-r--r--src/aig/gia/giaTim.c2
-rw-r--r--src/base/abci/abc.c4
-rw-r--r--src/base/cba/cbaBlast.c2
-rw-r--r--src/base/wlc/wlcBlast.c15
9 files changed, 41 insertions, 27 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 81a6d11a..58b00db2 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1204,7 +1204,7 @@ extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
extern Gia_Man_t * Gia_ManDupAndOr( Gia_Man_t * p, int nOuts, int fUseOr, int fCompl );
-extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose );
+extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int fVerbose );
extern Gia_Man_t * Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManTransformMiter2( Gia_Man_t * p );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 2aadf07f..8e7423aa 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -848,7 +848,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
}
}
pInit[i] = 0;
- pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 1 );
+ pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, fGiaSimple, 1 );
pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
Gia_ManStop( pTemp );
ABC_FREE( pInit );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 66b80ace..3ffb948e 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -2618,7 +2618,7 @@ Gia_Man_t * Gia_ManTransformTwoWord2DualOutput( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose )
+Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int fVerbose )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
@@ -2635,6 +2635,7 @@ Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose )
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ pNew->fGiaSimple = fGiaSimple;
Gia_ManConst0(p)->Value = 0;
// create primary inputs
Gia_ManForEachPi( p, pObj, i )
@@ -2707,7 +2708,7 @@ Gia_Man_t * Gia_ManMiter2( Gia_Man_t * pStart, char * pInit, int fVerbose )
for ( i = 0; i < Gia_ManPiNum(pStart); i++ )
assert( pInit[i] == 'x' || pInit[i] == 'X' );
// normalize the manager
- pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), fVerbose );
+ pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), 0, fVerbose );
// create new init string
pInitNew = ABC_ALLOC( char, Gia_ManPiNum(pUndc)+1 );
for ( i = 0; i < Gia_ManPiNum(pStart); i++ )
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index 5bfdbae2..d4a47ac5 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -666,10 +666,15 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 )
***********************************************************************/
int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
{
- int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1);
- int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) );
- int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) );
- return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
+ if ( p->fGiaSimple )
+ return Gia_ManHashOr(p, Gia_ManHashAnd(p, iLit0, Abc_LitNot(iLit1)), Gia_ManHashAnd(p, Abc_LitNot(iLit0), iLit1) );
+ else
+ {
+ int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1);
+ int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) );
+ int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) );
+ return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
+ }
}
/**Function*************************************************************
@@ -685,14 +690,19 @@ int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
***********************************************************************/
int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
{
- int iTemp0, iTemp1, fCompl = 0;
- if ( iData0 > iData1 )
- iData0 ^= iData1, iData1 ^= iData0, iData0 ^= iData1, iCtrl = Abc_LitNot(iCtrl);
- if ( Abc_LitIsCompl(iData1) )
- iData0 = Abc_LitNot(iData0), iData1 = Abc_LitNot(iData1), fCompl = 1;
- iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 );
- iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 );
- return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
+ if ( p->fGiaSimple )
+ return Gia_ManHashOr(p, Gia_ManHashAnd(p, iCtrl, iData1), Gia_ManHashAnd(p, Abc_LitNot(iCtrl), iData0) );
+ else
+ {
+ int iTemp0, iTemp1, fCompl = 0;
+ if ( iData0 > iData1 )
+ iData0 ^= iData1, iData1 ^= iData0, iData0 ^= iData1, iCtrl = Abc_LitNot(iCtrl);
+ if ( Abc_LitIsCompl(iData1) )
+ iData0 = Abc_LitNot(iData0), iData1 = Abc_LitNot(iData1), fCompl = 1;
+ iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 );
+ iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 );
+ return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
+ }
}
/**Function*************************************************************
diff --git a/src/aig/gia/giaRex.c b/src/aig/gia/giaRex.c
index 2eacc8d7..ebfc9401 100644
--- a/src/aig/gia/giaRex.c
+++ b/src/aig/gia/giaRex.c
@@ -309,7 +309,7 @@ Gia_Man_t * Gia_ManRex2Gia( char * pStrInit, int fOrder, int fVerbose )
Gia_ManStop( pTemp );
// add initial state
- pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0 );
+ pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 0 );
Gia_ManStop( pTemp );
Vec_StrFree( vInit );
/*
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 40573025..71b9a475 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -871,7 +871,7 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
pInit[i] = 'X';
}
pInit[i] = 0;
- pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 1 );
+ pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, 1 );
pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
Gia_ManStop( pTemp );
ABC_FREE( pInit );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 551961c9..e1d69bf1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26761,7 +26761,7 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
Aig_ManStop( pAig );
// perform undc/zero
pInits = Abc_NtkCollectLatchValuesStr( pAbc->pNtkCur );
- pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, fVerbose );
+ pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, 0, fVerbose );
Gia_ManStop( pTemp );
ABC_FREE( pInits );
}
@@ -32141,7 +32141,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pTemp;
if ( !pPars->fSilent )
Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
- pTemp = Gia_ManTransformToDual( pAbc->pGia );
+ pTemp = Gia_ManDemiterToDual( pAbc->pGia );
pAbc->Status = Cec_ManVerify( pTemp, pPars );
ABC_SWAP( Abc_Cex_t *, pAbc->pGia->pCexComb, pTemp->pCexComb );
Gia_ManStop( pTemp );
diff --git a/src/base/cba/cbaBlast.c b/src/base/cba/cbaBlast.c
index 322d4372..490a36eb 100644
--- a/src/base/cba/cbaBlast.c
+++ b/src/base/cba/cbaBlast.c
@@ -1013,7 +1013,7 @@ Gia_Man_t * Cba_NtkBlast( Cba_Ntk_t * p, int fSeq )
{
Gia_ManSetRegNum( pNew, Vec_StrSize(vInit) );
Vec_StrPush( vInit, '\0' );
- pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 1 );
+ pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 1 );
Gia_ManDupRemapLiterals( vBits, pTemp );
Gia_ManStop( pTemp );
Vec_StrFreeP( &vInit );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index adce0d57..65940176 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -274,10 +274,10 @@ void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int *
{
int And1 = Gia_ManHashAnd(pNew, a, b);
int And1_= Gia_ManHashAnd(pNew, Abc_LitNot(a), Abc_LitNot(b));
- int Xor = Abc_LitNot(Gia_ManHashOr(pNew, And1, And1_));
+ int Xor = Gia_ManHashAnd(pNew, Abc_LitNot(And1), Abc_LitNot(And1_));
int And2 = Gia_ManHashAnd(pNew, c, Xor);
int And2_= Gia_ManHashAnd(pNew, Abc_LitNot(c), Abc_LitNot(Xor));
- *ps = Abc_LitNot(Gia_ManHashOr(pNew, And2, And2_));
+ *ps = Gia_ManHashAnd(pNew, Abc_LitNot(And2), Abc_LitNot(And2_));
*pc = Gia_ManHashOr (pNew, And1, And2);
}
}
@@ -1209,9 +1209,12 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
assert( nFFins == nFFouts );
Gia_ManSetRegNum( pNew, nFFins );
// finalize AIG
- pNew = Gia_ManCleanup( pTemp = pNew );
- Gia_ManDupRemapLiterals( vBits, pTemp );
- Gia_ManStop( pTemp );
+ if ( !fGiaSimple )
+ {
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManDupRemapLiterals( vBits, pTemp );
+ Gia_ManStop( pTemp );
+ }
// transform AIG with init state
if ( p->pInits )
{
@@ -1222,7 +1225,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
}
else
{
- pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, 1 );
+ pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 1 );
Gia_ManDupRemapLiterals( vBits, pTemp );
Gia_ManStop( pTemp );
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 10:16:39 +0000