summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/aig/aig.h8
-rw-r--r--src/aig/aig/aigDfs.c2
-rw-r--r--src/aig/aig/aigDup.c48
-rw-r--r--src/aig/aig/aigFanout.c2
-rw-r--r--src/aig/aig/aigMffc.c4
-rw-r--r--src/aig/aig/aigObj.c2
-rw-r--r--src/aig/aig/aigPartReg.c4
-rw-r--r--src/aig/aig/aigRet.c14
-rw-r--r--src/aig/aig/aigTiming.c2
-rw-r--r--src/aig/aig/aigUtil.c4
-rw-r--r--src/aig/bbr/bbrReach.c98
-rw-r--r--src/aig/cec/cecCec.c3
-rw-r--r--src/aig/cec/cecClass.c26
-rw-r--r--src/aig/cec/cecCore.c12
-rw-r--r--src/aig/cec/cecCorr.c148
-rw-r--r--src/aig/cec/cecIso.c4
-rw-r--r--src/aig/cec/cecPat.c22
-rw-r--r--src/aig/cec/cecSeq.c16
-rw-r--r--src/aig/cec/cecSolve.c6
-rw-r--r--src/aig/cec/cecSweep.c6
-rw-r--r--src/aig/cnf/cnfMap.c2
-rw-r--r--src/aig/dar/darCore.c4
-rw-r--r--src/aig/dar/darLib.c6
-rw-r--r--src/aig/dar/darRefact.c6
-rw-r--r--src/aig/dch/dchClass.c2
-rw-r--r--src/aig/dch/dchSimSat.c4
-rw-r--r--src/aig/fra/fraBmc.c2
-rw-r--r--src/aig/fra/fraCec.c4
-rw-r--r--src/aig/fra/fraClass.c4
-rw-r--r--src/aig/fra/fraImp.c12
-rw-r--r--src/aig/fra/fraInd.c2
-rw-r--r--src/aig/fra/fraSat.c2
-rw-r--r--src/aig/fra/fraSec.c8
-rw-r--r--src/aig/fra/fraSim.c4
-rw-r--r--src/aig/gia/gia.h59
-rw-r--r--src/aig/gia/giaAig.c2
-rw-r--r--src/aig/gia/giaAig.h62
-rw-r--r--src/aig/gia/giaAiger.c6
-rw-r--r--src/aig/gia/giaCSat.c3
-rw-r--r--src/aig/gia/giaCof.c4
-rw-r--r--src/aig/gia/giaDup.c38
-rw-r--r--src/aig/gia/giaEmbed.c20
-rw-r--r--src/aig/gia/giaEnable.c6
-rw-r--r--src/aig/gia/giaEquiv.c68
-rw-r--r--src/aig/gia/giaFanout.c2
-rw-r--r--src/aig/gia/giaForce.c6
-rw-r--r--src/aig/gia/giaFrames.c4
-rw-r--r--src/aig/gia/giaFront.c2
-rw-r--r--src/aig/gia/giaGlitch.c18
-rw-r--r--src/aig/gia/giaHash.c33
-rw-r--r--src/aig/gia/giaMan.c1
-rw-r--r--src/aig/gia/giaRetime.c2
-rw-r--r--src/aig/gia/giaSat.c2
-rw-r--r--src/aig/gia/giaSim.c112
-rw-r--r--src/aig/gia/giaSwitch.c29
-rw-r--r--src/aig/gia/giaTsim.c22
-rw-r--r--src/aig/gia/giaUtil.c199
-rw-r--r--src/aig/hop/hop.h5
-rw-r--r--src/aig/hop/hopDfs.c4
-rw-r--r--src/aig/hop/hopObj.c2
-rw-r--r--src/aig/int/intCtrex.c2
-rw-r--r--src/aig/ivy/ivyFraig.c2
-rw-r--r--src/aig/ivy/ivyHaig.c2
-rw-r--r--src/aig/ivy/ivyMan.c4
-rw-r--r--src/aig/ivy/ivyObj.c2
-rw-r--r--src/aig/kit/kitDsd.c4
-rw-r--r--src/aig/mfx/mfxCore.c4
-rw-r--r--src/aig/ntl/ntlExtract.c2
-rw-r--r--src/aig/nwk/nwkFanio.c2
-rw-r--r--src/aig/nwk/nwkMan.c2
-rw-r--r--src/aig/nwk/nwkTiming.c4
-rw-r--r--src/aig/nwk/nwkUtil.c6
-rw-r--r--src/aig/nwk2/nwkFanio.c2
-rw-r--r--src/aig/nwk2/nwkUtil.c6
-rw-r--r--src/aig/saig/saig.h2
-rw-r--r--src/aig/saig/saigAbs.c13
-rw-r--r--src/aig/saig/saigMiter.c2
-rw-r--r--src/aig/saig/saigSimMv.c2
-rw-r--r--src/aig/saig/saigSynch.c2
-rw-r--r--src/aig/saig/saigTrans.c2
-rw-r--r--src/aig/ssw/sswClass.c2
-rw-r--r--src/aig/ssw/sswCore.c4
-rw-r--r--src/aig/ssw/sswDyn.c4
-rw-r--r--src/aig/ssw/sswLcorr.c4
-rw-r--r--src/aig/ssw/sswSemi.c2
-rw-r--r--src/aig/ssw/sswSim.c6
-rw-r--r--src/aig/tim/tim.c8
-rw-r--r--src/base/abc/abcAig.c2
-rw-r--r--src/base/abc/abcLatch.c110
-rw-r--r--src/base/abc/abcNtk.c18
-rw-r--r--src/base/abc/abcObj.c4
-rw-r--r--src/base/abc/abcUtil.c2
-rw-r--r--src/base/abci/abc.c152
-rw-r--r--src/base/abci/abcBmc.c2
-rw-r--r--src/base/abci/abcDar.c17
-rw-r--r--src/base/abci/abcFxu.c4
-rw-r--r--src/base/abci/abcHaig.c2
-rw-r--r--src/base/abci/abcMv.c2
-rw-r--r--src/base/abci/abcPrint.c2
-rw-r--r--src/base/abci/abcReach.c2
-rw-r--r--src/base/abci/abcSat.c2
-rw-r--r--src/base/abci/abcSweep.c2
-rw-r--r--src/base/abci/abcUnreach.c2
-rw-r--r--src/base/abci/abcVerify.c2
-rw-r--r--src/base/io/io.c2
-rw-r--r--src/base/io/ioReadAiger.c2
-rw-r--r--src/base/io/ioReadBlifMv.c2
-rw-r--r--src/base/io/ioWriteCnf.c2
-rw-r--r--src/base/ver/verCore.c8
-rw-r--r--src/map/amap/amapGraph.c10
-rw-r--r--src/map/amap/amapMatch.c6
-rw-r--r--src/map/fpga/fpgaCut.c2
-rw-r--r--src/map/if/ifMan.c2
-rw-r--r--src/map/mapper/mapperCut.c2
-rw-r--r--src/map/mio/mioFunc.c2
-rw-r--r--src/map/mio/mioUtils.c4
-rw-r--r--src/misc/hash/hashFlt.h4
-rw-r--r--src/misc/hash/hashInt.h4
-rw-r--r--src/misc/hash/hashPtr.h4
-rw-r--r--src/misc/vec/vecAtt.h6
-rw-r--r--src/misc/vec/vecPtr.h4
-rw-r--r--src/opt/lpk/lpkAbcDsd.c4
-rw-r--r--src/opt/lpk/lpkMulti.c2
-rw-r--r--src/opt/lpk/lpkSets.c2
-rw-r--r--src/opt/mfs/mfsCore.c2
-rw-r--r--src/opt/ret/retIncrem.c2
-rw-r--r--src/sat/csat/csat_apis.c2
-rw-r--r--src/sat/fraig/fraigFeed.c2
-rw-r--r--src/sat/fraig/fraigInt.h4
-rw-r--r--src/sat/fraig/fraigNode.c2
-rw-r--r--src/sat/fraig/fraigSat.c2
-rw-r--r--src/sat/fraig/fraigUtil.c2
-rw-r--r--src/sat/msat/msatSolverApi.c4
133 files changed, 1311 insertions, 413 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 1f51f300..1750a7b7 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -215,11 +215,6 @@ static inline Aig_Cut_t * Aig_CutNext( Aig_Cut_t * pCut ) { return
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-#define AIG_MIN(a,b) (((a) < (b))? (a) : (b))
-#define AIG_MAX(a,b) (((a) > (b))? (a) : (b))
-#define AIG_ABS(a) (((a) >= 0)? (a) :-(a))
-#define AIG_INFINITY (100000000)
-
static inline int Aig_IntAbs( int n ) { return (n < 0)? -n : n; }
static inline int Aig_Float2Int( float Val ) { return *((int *)&Val); }
static inline float Aig_Int2Float( int Num ) { return *((float *)&Num); }
@@ -320,7 +315,7 @@ static inline Aig_Obj_t * Aig_ObjChild1Next( Aig_Obj_t * pObj ) { assert( !Aig
static inline void Aig_ObjChild0Flip( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); pObj->pFanin0 = Aig_Not(pObj->pFanin0); }
static inline void Aig_ObjChild1Flip( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); pObj->pFanin1 = Aig_Not(pObj->pFanin1); }
static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level; }
-static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
+static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + ABC_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
static inline int Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level = i; }
static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); }
static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); }
@@ -483,6 +478,7 @@ extern Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vPos );
extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p );
+extern Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index db80a7f9..dfc35c83 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -407,7 +407,7 @@ int Aig_ManLevelNum( Aig_Man_t * p )
int i, LevelsMax;
LevelsMax = 0;
Aig_ManForEachPo( p, pObj, i )
- LevelsMax = AIG_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
+ LevelsMax = ABC_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
return LevelsMax;
}
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 6c9cb499..febe8a0c 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "aig.h"
+#include "saig.h"
#include "tim.h"
////////////////////////////////////////////////////////////////////////
@@ -301,6 +301,52 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
printf( "Aig_ManDupOrdered(): The check has failed.\n" );
return pNew;
}
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager.]
+
+ Description [Assumes topological ordering of the nodes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjNew;
+ int i, nNodes;
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+ // create the PIs
+ Aig_ManCleanData( p );
+ // duplicate internal nodes
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( Aig_ObjIsNode(pObj) )
+ pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+ else if ( Aig_ObjIsPi(pObj) )
+ pObjNew = (Aig_ObjRefs(pObj) > 0 || Saig_ObjIsLo(p, pObj)) ? Aig_ObjCreatePi(pNew) : NULL;
+ else if ( Aig_ObjIsPo(pObj) )
+ pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ else if ( Aig_ObjIsConst1(pObj) )
+ pObjNew = Aig_ManConst1(pNew);
+ else
+ assert( 0 );
+ pObj->pData = pObjNew;
+ }
+ assert( Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+ if ( (nNodes = Aig_ManCleanup( pNew )) )
+ printf( "Aig_ManDupTrim(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+ // check the resulting network
+ if ( !Aig_ManCheck(pNew) )
+ printf( "Aig_ManDupTrim(): The check has failed.\n" );
+ return pNew;
+}
/**Function*************************************************************
diff --git a/src/aig/aig/aigFanout.c b/src/aig/aig/aigFanout.c
index 89702087..a3b1e684 100644
--- a/src/aig/aig/aigFanout.c
+++ b/src/aig/aig/aigFanout.c
@@ -109,7 +109,7 @@ void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout )
assert( pFanout->Id > 0 );
if ( pObj->Id >= p->nFansAlloc || pFanout->Id >= p->nFansAlloc )
{
- int nFansAlloc = 2 * AIG_MAX( pObj->Id, pFanout->Id );
+ int nFansAlloc = 2 * ABC_MAX( pObj->Id, pFanout->Id );
p->pFanData = ABC_REALLOC( int, p->pFanData, 5 * nFansAlloc );
memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) );
p->nFansAlloc = nFansAlloc;
diff --git a/src/aig/aig/aigMffc.c b/src/aig/aig/aigMffc.c
index f681c76a..2c648382 100644
--- a/src/aig/aig/aigMffc.c
+++ b/src/aig/aig/aigMffc.c
@@ -266,13 +266,13 @@ int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves
// dereference the current cut
LevelMax = 0;
Vec_PtrForEachEntry( vLeaves, pObj, i )
- LevelMax = AIG_MAX( LevelMax, (int)pObj->Level );
+ LevelMax = ABC_MAX( LevelMax, (int)pObj->Level );
if ( LevelMax == 0 )
return 0;
// dereference the cut
ConeSize1 = Aig_NodeDeref_rec( pNode, 0, NULL, NULL );
// try expanding each node in the boundary
- ConeBest = AIG_INFINITY;
+ ConeBest = ABC_INFINITY;
pLeafBest = NULL;
Vec_PtrForEachEntry( vLeaves, pObj, i )
{
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 2c373ee1..8d243419 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -529,7 +529,7 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
if ( p->pFanData && Aig_ObjIsBuf(pObjOld) )
{
Vec_PtrPush( p->vBufs, pObjOld );
- p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
+ p->nBufMax = ABC_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
Aig_ManPropagateBuffers( p, fUpdateLevel );
}
}
diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c
index 1e77c224..dd10e91e 100644
--- a/src/aig/aig/aigPartReg.c
+++ b/src/aig/aig/aigPartReg.c
@@ -39,7 +39,7 @@ struct Aig_ManPre_t_
// info about the current partition
Vec_Int_t * vRegs; // registers of this partition
Vec_Int_t * vUniques; // unique registers of this partition
- Vec_Int_t * vFreeVars; // ABC_FREE variables of this partition
+ Vec_Int_t * vFreeVars; // free variables of this partition
Vec_Flt_t * vPartCost; // costs of adding each variable
char * pfPartVars; // input/output registers of the partition
};
@@ -153,7 +153,7 @@ int Aig_ManRegFindSeed( Aig_ManPre_t * p )
int Aig_ManRegFindBestVar( Aig_ManPre_t * p )
{
Vec_Int_t * vSupp;
- int nNewVars, nNewVarsBest = AIG_INFINITY;
+ int nNewVars, nNewVarsBest = ABC_INFINITY;
int iVarFree, iVarSupp, iVarBest = -1, i, k;
// go through the ABC_FREE variables
Vec_IntForEachEntry( p->vFreeVars, iVarFree, i )
diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c
index c5cc6392..6dea6503 100644
--- a/src/aig/aig/aigRet.c
+++ b/src/aig/aig/aigRet.c
@@ -173,7 +173,7 @@ void Rtm_ObjTransferToBig( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
assert( pEdge->nLats == 10 );
if ( p->nExtraCur + 1 > p->nExtraAlloc )
{
- int nExtraAllocNew = AIG_MAX( 2 * p->nExtraAlloc, 1024 );
+ int nExtraAllocNew = ABC_MAX( 2 * p->nExtraAlloc, 1024 );
p->pExtra = ABC_REALLOC( unsigned, p->pExtra, nExtraAllocNew );
p->nExtraAlloc = nExtraAllocNew;
}
@@ -199,7 +199,7 @@ void Rtm_ObjTransferToBigger( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
nWords = (pEdge->nLats + 1) >> 4;
if ( p->nExtraCur + nWords + 1 > p->nExtraAlloc )
{
- int nExtraAllocNew = AIG_MAX( 2 * p->nExtraAlloc, 1024 );
+ int nExtraAllocNew = ABC_MAX( 2 * p->nExtraAlloc, 1024 );
p->pExtra = ABC_REALLOC( unsigned, p->pExtra, nExtraAllocNew );
p->nExtraAlloc = nExtraAllocNew;
}
@@ -357,7 +357,7 @@ int Rtm_ManLatchMax( Rtm_Man_t * p )
assert( Val == 1 || Val == 2 );
}
*/
- nLatchMax = AIG_MAX( nLatchMax, (int)pEdge->nLats );
+ nLatchMax = ABC_MAX( nLatchMax, (int)pEdge->nLats );
}
return nLatchMax;
}
@@ -474,7 +474,7 @@ int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj )
Rtm_Obj_t * pFanin;
int i, Degree = 0;
Rtm_ObjForEachFanin( pObj, pFanin, i )
- Degree = AIG_MAX( Degree, (int)pFanin->Num );
+ Degree = ABC_MAX( Degree, (int)pFanin->Num );
return Degree + 1;
}
@@ -494,7 +494,7 @@ int Rtm_ObjGetDegreeBwd( Rtm_Obj_t * pObj )
Rtm_Obj_t * pFanout;
int i, Degree = 0;
Rtm_ObjForEachFanout( pObj, pFanout, i )
- Degree = AIG_MAX( Degree, (int)pFanout->Num );
+ Degree = ABC_MAX( Degree, (int)pFanout->Num );
return Degree + 1;
}
@@ -907,7 +907,7 @@ clk = clock();
if ( !Rtm_ObjCheckRetimeFwd( pNext ) ) // skip non-retimable
continue;
Degree = Rtm_ObjGetDegreeFwd( pNext );
- DegreeMax = AIG_MAX( DegreeMax, Degree );
+ DegreeMax = ABC_MAX( DegreeMax, Degree );
if ( Degree > nStepsMax ) // skip nodes with high degree
continue;
pNext->fMark = 1;
@@ -928,7 +928,7 @@ clk = clock();
if ( !Rtm_ObjCheckRetimeBwd( pNext ) ) // skip non-retimable
continue;
Degree = Rtm_ObjGetDegreeBwd( pNext );
- DegreeMax = AIG_MAX( DegreeMax, Degree );
+ DegreeMax = ABC_MAX( DegreeMax, Degree );
if ( Degree > nStepsMax ) // skip nodes with high degree
continue;
pNext->fMark = 1;
diff --git a/src/aig/aig/aigTiming.c b/src/aig/aig/aigTiming.c
index de8fdc7c..d0cc99e3 100644
--- a/src/aig/aig/aigTiming.c
+++ b/src/aig/aig/aigTiming.c
@@ -118,7 +118,7 @@ int Aig_ObjReverseLevelNew( Aig_Man_t * p, Aig_Obj_t * pObj )
Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
{
LevelCur = Aig_ObjReverseLevel( p, pFanout );
- Level = AIG_MAX( Level, LevelCur );
+ Level = ABC_MAX( Level, LevelCur );
}
return Level + 1;
}
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 80d1f527..d49fffd3 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -114,7 +114,7 @@ int Aig_ManLevels( Aig_Man_t * p )
Aig_Obj_t * pObj;
int i, LevelMax = 0;
Aig_ManForEachPo( p, pObj, i )
- LevelMax = AIG_MAX( LevelMax, (int)Aig_ObjFanin0(pObj)->Level );
+ LevelMax = ABC_MAX( LevelMax, (int)Aig_ObjFanin0(pObj)->Level );
return LevelMax;
}
@@ -1255,7 +1255,7 @@ void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * v
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) ) );
+ Vec_PtrGrow( vArr, ABC_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
pBeg = (Aig_Obj_t **)vArr->pArray;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c
index c2982856..1d43f6fb 100644
--- a/src/aig/bbr/bbrReach.c
+++ b/src/aig/bbr/bbrReach.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "bbr.h"
+#include "ssw.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -180,7 +181,7 @@ DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder,
bVar = Cudd_bddIthVar( dd, Saig_ManCiNum(p) + i );
pbParts[i] = Cudd_bddXnor( dd, bVar, Aig_ObjGlobalBdd(pNode) ); Cudd_Ref( pbParts[i] );
}
- // ABC_FREE global BDDs
+ // free global BDDs
Aig_ManFreeGlobalBdds( p, dd );
// reorder and disable reordering
@@ -220,9 +221,6 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
int nThreshold = 10000;
Vec_Ptr_t * vOnionRings;
- // start the onion rings
- vOnionRings = Vec_PtrAlloc( 1000 );
-
// start the image computation
bCubeCs = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs );
if ( fPartition )
@@ -237,6 +235,9 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
return -1;
}
+ // start the onion rings
+ vOnionRings = Vec_PtrAlloc( 1000 );
+
// perform reachability analisys
bCurrent = bInitial; Cudd_Ref( bCurrent );
bReached = bInitial; Cudd_Ref( bReached );
@@ -256,6 +257,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
Bbr_bddImageTreeDelete( pTree );
else
Bbr_bddImageTreeDelete2( pTree2 );
+ Vec_PtrFree( vOnionRings );
return -1;
}
Cudd_Ref( bNext );
@@ -316,7 +318,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
fprintf( stdout, "\r" );
}
Cudd_RecursiveDeref( dd, bNext );
- // ABC_FREE the onion rings
+ // free the onion rings
Vec_PtrForEachEntry( vOnionRings, bTemp, i )
Cudd_RecursiveDeref( dd, bTemp );
Vec_PtrFree( vOnionRings );
@@ -353,7 +355,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
/**Function*************************************************************
- Synopsis [Performs reachability to see if any .]
+ Synopsis [Performs reachability to see if any PO can be asserted.]
Description []
@@ -362,7 +364,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
SeeAlso []
***********************************************************************/
-int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
+int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
{
DdManager * dd;
DdNode ** pbParts, ** pbOutputs;
@@ -372,9 +374,6 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
assert( Saig_ManRegNum(p) > 0 );
- // start the onion rings
- vOnionRings = Vec_PtrAlloc( 1000 );
-
// compute the global BDDs of the latches
dd = Aig_ManComputeGlobalBdds( p, nBddMax, 1, fReorder, fVerbose );
if ( dd == NULL )
@@ -386,6 +385,9 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
if ( fVerbose )
printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+ // start the onion rings
+ vOnionRings = Vec_PtrAlloc( 1000 );
+
// save outputs
pbOutputs = Aig_ManCreateOutputs( dd, p );
@@ -413,7 +415,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
break;
}
}
- // ABC_FREE the onion rings
+ // free the onion rings
Vec_PtrForEachEntry( vOnionRings, bTemp, i )
Cudd_RecursiveDeref( dd, bTemp );
Vec_PtrFree( vOnionRings );
@@ -443,6 +445,80 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
return RetValue;
}
+/**Function*************************************************************
+
+ Synopsis [Performs reachability to see if any PO can be asserted.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
+{
+ Ssw_Cex_t * pCexOld, * pCexNew;
+ Aig_Man_t * p;
+ Aig_Obj_t * pObj;
+ Vec_Int_t * vInputMap;
+ int i, k, Entry, iBitOld, iBitNew, RetValue;
+ // check if there are PIs without fanout
+ Saig_ManForEachPi( pInit, pObj, i )
+ if ( Aig_ObjRefs(pObj) == 0 )
+ break;
+ if ( i == Saig_ManPiNum(pInit) )
+ return Aig_ManVerifyUsingBdds_int( pInit, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent );
+ // create new AIG
+ p = Aig_ManDupTrim( pInit );
+ assert( Aig_ManPiNum(p) < Aig_ManPiNum(pInit) );
+ assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) );
+ RetValue = Aig_ManVerifyUsingBdds_int( p, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent );
+ if ( RetValue != 0 )
+ {
+ Aig_ManStop( p );
+ return RetValue;
+ }
+ // the problem is satisfiable - remap the pattern
+ pCexOld = p->pSeqModel;
+ assert( pCexOld != NULL );
+ // create input map
+ vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) );
+ Saig_ManForEachPi( pInit, pObj, i )
+ if ( pObj->pData != NULL )
+ Vec_IntPush( vInputMap, Aig_ObjPioNum(pObj->pData) );
+ else
+ Vec_IntPush( vInputMap, -1 );
+ // create new pattern
+ pCexNew = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 );
+ pCexNew->iFrame = pCexOld->iFrame;
+ pCexNew->iPo = pCexOld->iPo;
+ // copy the bit-data
+ for ( iBitOld = 0; iBitOld < pCexOld->nRegs; iBitOld++ )
+ if ( Aig_InfoHasBit( pCexOld->pData, iBitOld ) )
+ Aig_InfoSetBit( pCexNew->pData, iBitOld );
+ // copy the primary input data
+ iBitNew = iBitOld;
+ for ( i = 0; i <= pCexNew->iFrame; i++ )
+ {
+ Vec_IntForEachEntry( vInputMap, Entry, k )
+ {
+ if ( Entry == -1 )
+ continue;
+ if ( Aig_InfoHasBit( pCexOld->pData, iBitOld + Entry ) )
+ Aig_InfoSetBit( pCexNew->pData, iBitNew + k );
+ }
+ iBitOld += Saig_ManPiNum(p);
+ iBitNew += Saig_ManPiNum(pInit);
+ }
+ assert( iBitOld < iBitNew );
+ assert( iBitOld == pCexOld->nBits );
+ assert( iBitNew == pCexNew->nBits );
+ Vec_IntFree( vInputMap );
+ pInit->pSeqModel = pCexNew;
+ Aig_ManStop( p );
+ return 0;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index 82df6008..ee9f6d3c 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "cecInt.h"
+#include "giaAig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -44,7 +45,7 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues )
int i;
assert( p->pCexComb == NULL );
p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char,
- sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p)) );
+ sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p)) );
p->pCexComb->iPo = iOut;
p->pCexComb->nPis = Gia_ManCiNum(p);
p->pCexComb->nBits = Gia_ManCiNum(p);
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index 49930836..5a52e913 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -111,14 +111,14 @@ int Cec_ManSimCompareConstFirstBit( unsigned * p, int nWords )
{
for ( w = 0; w < nWords; w++ )
if ( p[w] != ~0 )
- return 32*w + Aig_WordFindFirstBit( ~p[w] );
+ return 32*w + Gia_WordFindFirstBit( ~p[w] );
return -1;
}
else
{
for ( w = 0; w < nWords; w++ )
if ( p[w] != 0 )
- return 32*w + Aig_WordFindFirstBit( p[w] );
+ return 32*w + Gia_WordFindFirstBit( p[w] );
return -1;
}
}
@@ -141,14 +141,14 @@ int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords )
{
for ( w = 0; w < nWords; w++ )
if ( p0[w] != p1[w] )
- return 32*w + Aig_WordFindFirstBit( p0[w] ^ p1[w] );
+ return 32*w + Gia_WordFindFirstBit( p0[w] ^ p1[w] );
return -1;
}
else
{
for ( w = 0; w < nWords; w++ )
if ( p0[w] != ~p1[w] )
- return 32*w + Aig_WordFindFirstBit( p0[w] ^ ~p1[w] );
+ return 32*w + Gia_WordFindFirstBit( p0[w] ^ ~p1[w] );
return -1;
}
}
@@ -467,7 +467,7 @@ void Cec_ManSimProcessRefined( Cec_ManSim_t * p, Vec_Int_t * vRefined )
int * pTable, nTableSize, i, k, Key;
if ( Vec_IntSize(vRefined) == 0 )
return;
- nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
+ nTableSize = Gia_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
pTable = ABC_CALLOC( int, nTableSize );
Vec_IntForEachEntry( vRefined, i, k )
{
@@ -519,15 +519,15 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
assert( p->pCexComb == NULL );
assert( iPat >= 0 && iPat < 32 * p->nWords );
p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char,
- sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p->pAig)) );
+ sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p->pAig)) );
p->pCexComb->iPo = p->iOut;
p->pCexComb->nPis = Gia_ManCiNum(p->pAig);
p->pCexComb->nBits = Gia_ManCiNum(p->pAig);
for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
{
pInfo = Vec_PtrEntry( p->vCiSimInfo, i );
- if ( Aig_InfoHasBit( pInfo, iPat ) )
- Aig_InfoSetBit( p->pCexComb->pData, i );
+ if ( Gia_InfoHasBit( pInfo, iPat ) )
+ Gia_InfoSetBit( p->pCexComb->pData, i );
}
}
@@ -560,8 +560,8 @@ void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
pInfo = Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
- if ( Aig_InfoHasBit(p->pBestState->pData, i) != Aig_InfoHasBit(pInfo, iPatBest) )
- Aig_InfoXorBit( p->pBestState->pData, i );
+ if ( Gia_InfoHasBit(p->pBestState->pData, i) != Gia_InfoHasBit(pInfo, iPatBest) )
+ Gia_InfoXorBit( p->pBestState->pData, i );
}
p->pBestState->iPo = ScoreBest;
}
@@ -686,7 +686,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
else
{
for ( w = 1; w <= p->nWords; w++ )
- pRes[w] = Aig_ManRandom( 0 );
+ pRes[w] = Gia_ManRandom( 0 );
}
// make sure the first pattern is always zero
pRes[1] ^= (pRes[1] & 1);
@@ -798,7 +798,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v
{
pRes0 = Vec_PtrEntry( vInfoCis, i );
for ( w = 0; w < p->nWords; w++ )
- pRes0[w] = Aig_ManRandom( 0 );
+ pRes0[w] = Gia_ManRandom( 0 );
}
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
@@ -814,7 +814,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v
{
pRes0 = Vec_PtrEntry( vInfoCis, i );
for ( w = 0; w < p->nWords; w++ )
- pRes0[w] = Aig_ManRandom( 0 );
+ pRes0[w] = Gia_ManRandom( 0 );
}
}
}
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index 7759428e..ca0a3665 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -246,7 +246,7 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
if ( pPars->fSeqSimulate )
printf( "Performing sequential simulation of %d frames with %d words.\n",
pPars->nRounds, pPars->nWords );
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
pSim = Cec_ManSimStart( pAig, pPars );
if ( pAig->pReprs == NULL )
RetValue = Cec_ManSimClassesPrepare( pSim );
@@ -283,7 +283,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
double clkTotal = clock();
// duplicate AIG and transfer equivalence classes
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
pIni = Gia_ManDup(pAig);
pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL;
pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL;
@@ -420,7 +420,8 @@ p->timeSat += clock() - clk;
printf( "Switching into reduced mode.\n" );
pPars->fColorDiff = 0;
}
- if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 )
+// if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 )
+ else if ( pPars->fDualOut && (Gia_ManAndNum(p->pAig) < 20000 || p->nAllProved + p->nAllDisproved < 10) )
{
if ( p->pPars->fVerbose )
printf( "Switching into normal mode.\n" );
@@ -431,6 +432,11 @@ p->timeSat += clock() - clk;
finalize:
if ( p->pPars->fVerbose )
{
+ printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
+ Gia_ManAndNum(pAig), Gia_ManAndNum(p->pAig),
+ 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(p->pAig))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
+ Gia_ManRegNum(pAig), Gia_ManRegNum(p->pAig),
+ 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(p->pAig))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
ABC_PRTP( "Sim ", p->timeSim, clock() - (int)clkTotal );
ABC_PRTP( "Sat ", p->timeSat-pPat->timeTotalSave, clock() - (int)clkTotal );
ABC_PRTP( "Pat ", p->timePat+pPat->timeTotalSave, clock() - (int)clkTotal );
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index 05259bc7..dccd90b0 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -49,6 +49,11 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f );
return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) );
}
+ if ( f == 0 )
+ {
+ assert( Gia_ObjIsRo(p, pObj) );
+ return Gia_ObjCopyF(p, f, pObj);
+ }
assert( f && Gia_ObjIsRo(p, pObj) );
pObj = Gia_ObjRoToRi( p, pObj );
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1 );
@@ -107,7 +112,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 );
Gia_ManForEachRo( p, pObj, i )
@@ -202,6 +207,74 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
/**Function*************************************************************
+ Synopsis [Derives SRM for signal correspondence.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj, * pRepr;
+ Vec_Int_t * vXorLits;
+ int f, i, iPrevNew, iObjNew;
+ assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) );
+ assert( Gia_ManRegNum(p) > 0 );
+ assert( p->pReprs != NULL );
+ p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
+ Gia_ManSetPhase( p );
+ pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
+ pNew->pName = Gia_UtilStrsav( p->pName );
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachRo( p, pObj, i )
+ {
+ Gia_ManAppendCi(pNew);
+ Gia_ObjSetCopyF( p, 0, pObj, 0 );
+ }
+ for ( f = 0; f < nFrames+fScorr; f++ )
+ {
+ Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
+ Gia_ManForEachPi( p, pObj, i )
+ Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
+ }
+ *pvOutputs = Vec_IntAlloc( 1000 );
+ vXorLits = Vec_IntAlloc( 1000 );
+ for ( f = 0; f < nFrames; f++ )
+ {
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+ if ( pRepr == NULL )
+ continue;
+ iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f );
+ iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f );
+ iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+ if ( iPrevNew != iObjNew )
+ {
+ Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
+ Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
+ Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
+ }
+ }
+ }
+ Vec_IntForEachEntry( vXorLits, iObjNew, i )
+ Gia_ManAppendCo( pNew, iObjNew );
+ Vec_IntFree( vXorLits );
+ Gia_ManHashStop( pNew );
+ ABC_FREE( p->pCopies );
+//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Initializes simulation info for lcorr/scorr counter-examples.]
Description []
@@ -227,7 +300,7 @@ void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
- pInfo[w] = Aig_ManRandom( 0 );
+ pInfo[w] = Gia_ManRandom( 0 );
}
}
@@ -351,17 +424,17 @@ int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBi
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
- if ( Aig_InfoHasBit( pPres, iBit ) &&
- Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+ if ( Gia_InfoHasBit( pPres, iBit ) &&
+ Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
- Aig_InfoSetBit( pPres, iBit );
- if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
- Aig_InfoXorBit( pInfo, iBit );
+ Gia_InfoSetBit( pPres, iBit );
+ if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+ Gia_InfoXorBit( pInfo, iBit );
}
return 1;
}
@@ -403,7 +476,7 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS
for ( k = 1; k < nBits; k++ )
if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
break;
- kMax = AIG_MAX( kMax, k );
+ kMax = ABC_MAX( kMax, k );
if ( k == nBits-1 )
break;
}
@@ -443,8 +516,8 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
{
iLit = Vec_IntEntry( vCexStore, iStart++ );
pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) );
- if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) )
- Aig_InfoXorBit( pInfo, iBit );
+ if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) )
+ Gia_InfoXorBit( pInfo, iBit );
}
if ( ++iBit == nBits )
break;
@@ -591,7 +664,11 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int
}
CounterX -= Gia_ManCoNum(p);
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
- printf( "%3d : c =%8d cl =%7d lit =%8d ", iIter, Counter0, Counter, nLits );
+ if ( iIter == -1 )
+ printf( "BMC : " );
+ else
+ printf( "%3d : ", iIter );
+ printf( "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits );
if ( vStatus )
Vec_StrForEachEntry( vStatus, Entry, i )
{
@@ -638,7 +715,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
return NULL;
}
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
@@ -704,14 +781,57 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
}
+ // check the base case
+ if ( !pPars->fLatchCorr || pPars->nFrames > 1 )
+ {
+ int fChanges = 1;
+ while ( fChanges )
+ {
+ int clkBmc = clock();
+ fChanges = 0;
+ pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
+ if ( Gia_ManPoNum(pSrm) == 0 )
+ {
+ Gia_ManStop( pSrm );
+ Vec_IntFree( vOutputs );
+ break;
+ }
+ pParsSat->nBTLimit *= 10;
+ if ( pPars->fUseCSat )
+ vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+ else
+ vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
+ // refine classes with these counter-examples
+ if ( Vec_IntSize(vCexStore) )
+ {
+ clk2 = clock();
+ RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames );
+ clkSim += clock() - clk2;
+ Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
+ fChanges = 1;
+ }
+ if ( pPars->fVerbose )
+ Cec_ManLCorrPrintStats( pAig, vStatus, -1, clock() - clkBmc );
+ // recycle
+ Vec_IntFree( vCexStore );
+ Vec_StrFree( vStatus );
+ Gia_ManStop( pSrm );
+ Vec_IntFree( vOutputs );
+ }
+ }
+ else
+ {
+ if ( pPars->fVerbose )
+ Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk );
+ }
+ // check the overflow
if ( r == 100000 )
printf( "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
clkTotal = clock() - clkTotal;
- if ( pPars->fVerbose )
- Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk );
// derive reduced AIG
Gia_ManSetProvedNodes( pAig );
+ Gia_ManEquivImprove( pAig );
pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 );
//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
pNew = Gia_ManSeqCleanup( pTemp = pNew );
diff --git a/src/aig/cec/cecIso.c b/src/aig/cec/cecIso.c
index ddb539c2..d9aa5240 100644
--- a/src/aig/cec/cecIso.c
+++ b/src/aig/cec/cecIso.c
@@ -125,7 +125,7 @@ static inline void Gia_ManIsoRandom( int Id, unsigned * pStore, int nWords )
unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id );
int w;
for ( w = 0; w < nWords; w++ )
- pInfo0[w] = Aig_ManRandom( 0 );
+ pInfo0[w] = Gia_ManRandom( 0 );
}
/**Function*************************************************************
@@ -314,7 +314,7 @@ int * Cec_ManDetectIsomorphism( Gia_Man_t * p )
// start simulation info
pStore = ABC_ALLOC( unsigned, Gia_ManObjNum(p) * nWords );
// simulate and create table
- nTableSize = Aig_PrimeCudd( 100 + Gia_ManObjNum(p)/2 );
+ nTableSize = Gia_PrimeCudd( 100 + Gia_ManObjNum(p)/2 );
pTable = ABC_CALLOC( int, nTableSize );
Gia_ManCleanValue( p );
Gia_ManForEachObj1( p, pObj, i )
diff --git a/src/aig/cec/cecPat.c b/src/aig/cec/cecPat.c
index a5be4c1c..8537fe4a 100644
--- a/src/aig/cec/cecPat.c
+++ b/src/aig/cec/cecPat.c
@@ -414,17 +414,17 @@ int Cec_ManPatCollectTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int *
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
- if ( Aig_InfoHasBit( pPres, iBit ) &&
- Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+ if ( Gia_InfoHasBit( pPres, iBit ) &&
+ Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
- Aig_InfoSetBit( pPres, iBit );
- if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
- Aig_InfoXorBit( pInfo, iBit );
+ Gia_InfoSetBit( pPres, iBit );
+ if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+ Gia_InfoXorBit( pInfo, iBit );
}
return 1;
}
@@ -450,7 +450,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW
int nBits = 32 * nWords;
int clk = clock();
vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
- Aig_ManRandomInfo( vInfo, 0, 0, nWords );
+ Gia_ManRandomInfo( vInfo, 0, 0, nWords );
vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
Vec_PtrCleanSimInfo( vPres, 0, nWords );
while ( pMan->iStart < Vec_StrSize(pMan->vStorage) )
@@ -460,11 +460,11 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW
for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) )
if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
break;
- kMax = AIG_MAX( kMax, k );
+ kMax = ABC_MAX( kMax, k );
if ( k == nBits-1 )
{
Vec_PtrReallocSimInfo( vInfo );
- Aig_ManRandomInfo( vInfo, 0, nWords, 2*nWords );
+ Gia_ManRandomInfo( vInfo, 0, nWords, 2*nWords );
Vec_PtrReallocSimInfo( vPres );
Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
nWords *= 2;
@@ -511,7 +511,7 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg
vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
Vec_PtrCleanSimInfo( vInfo, 0, nWords );
- Aig_ManRandomInfo( vInfo, nRegs, 0, nWords );
+ Gia_ManRandomInfo( vInfo, nRegs, 0, nWords );
vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
Vec_PtrCleanSimInfo( vPres, 0, nWords );
@@ -538,12 +538,12 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg
// RetValue = Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) );
// assert( RetValue == 1 );
- kMax = AIG_MAX( kMax, k );
+ kMax = ABC_MAX( kMax, k );
if ( k == nBits-1 )
{
Vec_PtrReallocSimInfo( vInfo );
Vec_PtrCleanSimInfo( vInfo, nWords, 2*nWords );
- Aig_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords );
+ Gia_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords );
Vec_PtrReallocSimInfo( vPres );
Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index 3d05172f..28f3a637 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -51,7 +51,7 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
- pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0;
+ pInfo[w] = Gia_InfoHasBit( pCex->pData, k )? ~0 : 0;
}
*/
for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
@@ -65,16 +65,16 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t
{
pInfo = Vec_PtrEntry( vInfo, k++ );
for ( w = 0; w < nWords; w++ )
- pInfo[w] = Aig_ManRandom(0);
+ pInfo[w] = Gia_ManRandom(0);
// set simulation pattern and make sure it is second (first will be erased during simulation)
- pInfo[0] = (pInfo[0] << 1) | Aig_InfoHasBit( pCex->pData, i );
+ pInfo[0] = (pInfo[0] << 1) | Gia_InfoHasBit( pCex->pData, i );
pInfo[0] <<= 1;
}
for ( ; k < Vec_PtrSize(vInfo); k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
- pInfo[w] = Aig_ManRandom(0);
+ pInfo[w] = Gia_ManRandom(0);
}
}
@@ -100,14 +100,14 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
- pInfo[w] = (pCex && Aig_InfoHasBit(pCex->pData, k))? ~0 : 0;
+ pInfo[w] = (pCex && Gia_InfoHasBit(pCex->pData, k))? ~0 : 0;
}
for ( ; k < Vec_PtrSize(vInfo); k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
- pInfo[w] = Aig_ManRandom( 0 );
+ pInfo[w] = Gia_ManRandom( 0 );
}
}
@@ -229,7 +229,7 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex
}
if ( pPars->fVerbose )
printf( "Resimulating %d timeframes.\n", pPars->nRounds + pCex->iFrame + 1 );
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) +
Gia_ManPiNum(pAig) * (pPars->nRounds + pCex->iFrame + 1), 1 );
Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex );
@@ -275,7 +275,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
printf( "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" );
return -1;
}
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
// prepare starting pattern
pState = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), 0, 0 );
pState->iFrame = -1;
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index fc2d5d7f..5f032b59 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -369,7 +369,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
Cec_ObjSetSatNum( p, pObj, 0 );
Vec_PtrClear( p->vUsedNodes );
-// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
+// memset( p->pSatVars, 0, sizeof(int) * Gia_ManObjNumMax(p->pAigTotal) );
sat_solver_delete( p->pSat );
}
p->pSat = sat_solver_new();
@@ -636,8 +636,8 @@ void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pOb
if ( Gia_ObjIsCi(pObj) )
{
unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
- if ( Cec_ObjSatVarValue( pSat, pObj ) != Aig_InfoHasBit( pInfo, iPat ) )
- Aig_InfoXorBit( pInfo, iPat );
+ if ( Cec_ObjSatVarValue( pSat, pObj ) != Gia_InfoHasBit( pInfo, iPat ) )
+ Gia_InfoXorBit( pInfo, iPat );
pSat->nCexLits++;
// Vec_IntPush( pSat->vCex, Gia_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) );
return;
diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c
index f5e5bd06..1b68efe0 100644
--- a/src/aig/cec/cecSweep.c
+++ b/src/aig/cec/cecSweep.c
@@ -50,7 +50,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
if ( p->pPars->nLevelMax )
Gia_ManLevelNum( p->pAig );
pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
- pNew->pName = Aig_UtilStrsav( p->pAig->pName );
+ pNew->pName = Gia_UtilStrsav( p->pAig->pName );
Gia_ManHashAlloc( pNew );
piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
pDepths = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
@@ -70,7 +70,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
- pDepths[i] = AIG_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] );
+ pDepths[i] = ABC_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] );
if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID || Gia_ObjFailed(p->pAig, i) )
continue;
assert( Gia_ObjRepr(p->pAig, i) < i );
@@ -109,7 +109,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
Vec_IntPush( p->vXorNodes, Gia_ObjRepr(p->pAig, i) );
Vec_IntPush( p->vXorNodes, i );
// add to the depth of this node
- pDepths[i] = 1 + AIG_MAX( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] );
+ pDepths[i] = 1 + ABC_MAX( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] );
if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax )
piCopies[i] = -1;
}
diff --git a/src/aig/cnf/cnfMap.c b/src/aig/cnf/cnfMap.c
index 63625e6f..58c9b803 100644
--- a/src/aig/cnf/cnfMap.c
+++ b/src/aig/cnf/cnfMap.c
@@ -123,7 +123,7 @@ void Cnf_DeriveMapping( Cnf_Man_t * p )
// Aig_ObjCollectSuper( pObj, vSuper );
// get the area flow of this cut
// AreaFlow = Cnf_CutSuperAreaFlow( vSuper, pAreaFlows );
- AreaFlow = AIG_INFINITY;
+ AreaFlow = ABC_INFINITY;
if ( AreaFlow >= (int)pCutBest->uSign )
{
pAreaFlows[pObj->Id] = pCutBest->uSign;
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index 3c8423cf..83b6e08e 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -151,7 +151,7 @@ p->timeCuts += clock() - clk;
// evaluate the cuts
p->GainBest = -1;
- Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY;
+ Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY;
Dar_ObjForEachCut( pObj, pCut, k )
Dar_LibEval( p, pObj, pCut, Required );
// check the best gain
@@ -292,7 +292,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose
Dar_ObjCutPrint( pAig, pObj );
*/
}
- // ABC_FREE the cuts
+ // free the cuts
pMemCuts = p->pMemCuts;
p->pMemCuts = NULL;
// Dar_ManCutsFree( p );
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index c5fd4696..cfa4594d 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -472,7 +472,7 @@ void Dar_LibPrepare( int nSubgraphs )
if ( i == 1 ) // special classes
p->nSubgr0[i] = p->nSubgr[i];
else
- p->nSubgr0[i] = AIG_MIN( p->nSubgr[i], nSubgraphs );
+ p->nSubgr0[i] = ABC_MIN( p->nSubgr[i], nSubgraphs );
p->nSubgr0Total += p->nSubgr0[i];
for ( k = 0; k < p->nSubgr0[i]; k++ )
p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ];
@@ -494,7 +494,7 @@ void Dar_LibPrepare( int nSubgraphs )
for ( k = 0; k < p->nSubgr0[i]; k++ )
Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 );
p->nNodes0Total += p->nNodes0[i];
- p->nNodes0Max = AIG_MAX( p->nNodes0Max, p->nNodes0[i] );
+ p->nNodes0Max = ABC_MAX( p->nNodes0Max, p->nNodes0[i] );
}
// clean node counters
@@ -799,7 +799,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot )
assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 );
pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num;
pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num;
- pData->Level = 1 + AIG_MAX(pData0->Level, pData1->Level);
+ pData->Level = 1 + ABC_MAX(pData0->Level, pData1->Level);
if ( pData0->pFunc == NULL || pData1->pFunc == NULL )
continue;
pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 );
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index f64564fa..6118dd71 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -267,7 +267,7 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, K
return -1;
}
// count the number of new levels
- LevelNew = 1 + AIG_MAX( pNode0->Level, pNode1->Level );
+ LevelNew = 1 + ABC_MAX( pNode0->Level, pNode1->Level );
if ( pAnd )
{
if ( Aig_Regular(pAnd) == Aig_ManConst1(pAig) )
@@ -527,7 +527,7 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
//printf( "\nConsidering node %d.\n", pObj->Id );
// get the bounded MFFC size
clk = clock();
- nLevelMin = AIG_MAX( 0, Aig_ObjLevel(pObj) - 10 );
+ nLevelMin = ABC_MAX( 0, Aig_ObjLevel(pObj) - 10 );
nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut );
if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider
{
@@ -564,7 +564,7 @@ p->timeCuts += clock() - clk;
// try the cuts
clk = clock();
- Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY;
+ Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY;
Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required );
p->timeEval += clock() - clk;
diff --git a/src/aig/dch/dchClass.c b/src/aig/dch/dchClass.c
index d8fbe8ed..9f4bd68c 100644
--- a/src/aig/dch/dchClass.c
+++ b/src/aig/dch/dchClass.c
@@ -544,7 +544,7 @@ void Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes,
{
int i, Limit;
Vec_PtrClear( vRoots );
- Limit = AIG_MIN( pObj->Id + nNodes, Aig_ManObjNumMax(p->pAig) );
+ Limit = ABC_MIN( pObj->Id + nNodes, Aig_ManObjNumMax(p->pAig) );
for ( i = pObj->Id; i < Limit; i++ )
{
pObj = Aig_ManObj( p->pAig, i );
diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c
index 61d2ab93..4f31b928 100644
--- a/src/aig/dch/dchSimSat.c
+++ b/src/aig/dch/dchSimSat.c
@@ -183,7 +183,7 @@ void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
Dch_ManResimulateSolved_rec( p, pObj );
Dch_ManResimulateSolved_rec( p, pRepr );
- p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis );
+ p->nConeMax = ABC_MAX( p->nConeMax, p->nConeThis );
// resimulate the cone of influence of the other nodes
Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
Dch_ManResimulateOther_rec( p, pRoot );
@@ -233,7 +233,7 @@ void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
Dch_ManResimulateSolved_rec( p, pObj );
Dch_ManResimulateSolved_rec( p, pRepr );
- p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis );
+ p->nConeMax = ABC_MAX( p->nConeMax, p->nConeThis );
// resimulate the cone of influence of the other nodes
Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
Dch_ManResimulateOther_rec( p, pRoot );
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index 689d7d67..7b08d74d 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -360,7 +360,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
printf( "\n" );
}
- // ABC_FREE the BMC manager
+ // free the BMC manager
Fra_BmcStop( p->pBmc );
p->pBmc = NULL;
}
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 0cc6748c..b7a78050 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -136,7 +136,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
{
pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
}
- // ABC_FREE the sat_solver
+ // free the sat_solver
if ( fVerbose )
Sat_SolverPrintStats( stdout, pSat );
//sat_solver_store_write( pSat, "trace.cnf" );
@@ -318,7 +318,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimi
printf( "Timed out after verifying %d partitions (out of %d).\n", nOutputs, Vec_PtrSize(vParts) );
fflush( stdout );
}
- // ABC_FREE intermediate results
+ // free intermediate results
Vec_PtrForEachEntry( vParts, pAig, i )
Aig_ManStop( pAig );
Vec_PtrFree( vParts );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 8554b312..94cac80a 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -652,7 +652,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
if ( pRepr == NULL )
continue;
pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id );
- WeightMax = AIG_MAX( WeightMax, pWeights[i] );
+ WeightMax = ABC_MAX( WeightMax, pWeights[i] );
}
Fra_SmlStop( pComb );
printf( "Before: Const = %6d. Class = %6d. ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
@@ -710,7 +710,7 @@ void Fra_ClassesSelectRepr( Fra_Cla_t * p )
// collect support sizes and find the min-support node
cMinSupp = -1;
pNodeMin = NULL;
- nSuppSizeMin = AIG_INFINITY;
+ nSuppSizeMin = ABC_INFINITY;
for ( c = 0; pClass[c]; c++ )
{
nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index d579146e..716e83d5 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -290,8 +290,8 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax,
***********************************************************************/
int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
{
- int Max1 = AIG_MAX( pImp1[0], pImp1[1] );
- int Max2 = AIG_MAX( pImp2[0], pImp2[1] );
+ int Max1 = ABC_MAX( pImp1[0], pImp1[1] );
+ int Max2 = ABC_MAX( pImp2[0], pImp2[1] );
if ( Max1 < Max2 )
return -1;
if ( Max1 > Max2 )
@@ -323,7 +323,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
Vec_Ptr_t * vNodes;
int * pImpCosts, * pNodesI, * pNodesK;
int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
- int CostMin = AIG_INFINITY, CostMax = 0;
+ int CostMin = ABC_INFINITY, CostMax = 0;
int i, k, Imp, CostRange, clk = clock();
assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
@@ -364,8 +364,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
nImpsCollected++;
Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
- CostMin = AIG_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
- CostMax = AIG_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
+ CostMin = ABC_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
+ CostMax = ABC_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
Vec_IntPush( vImps, Imp );
if ( Vec_IntSize(vImps) == nImpMaxLimit )
goto finish;
@@ -508,7 +508,7 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
continue;
Left = Fra_ImpLeft(Imp);
Right = Fra_ImpRight(Imp);
- Max = AIG_MAX( Left, Right );
+ Max = ABC_MAX( Left, Right );
assert( Max >= pNode->Id );
if ( Max > pNode->Id )
return i;
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 4f3812c6..84b739a4 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -629,7 +629,7 @@ p->timeTotal = clock() - clk;
p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
p->nRegsEnd = Aig_ManRegNum(pManAigNew);
- // ABC_FREE the manager
+ // free the manager
finish:
Fra_ManStop( p );
// check the output
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index c2eaf453..039a660f 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -539,7 +539,7 @@ clk = clock();
Aig_ManIncrementTravId( p->pManFraig );
// determine the min and max level to visit
assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 );
- LevelMax = AIG_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
+ LevelMax = ABC_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio));
// traverse
if ( pOld && !Aig_ObjIsConst1(pOld) )
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index a97af278..8064d2ee 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -170,7 +170,7 @@ clk = clock();
if ( RetValue == -1 && pParSec->TimeLimit )
{
TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
- TimeLeft = AIG_MAX( TimeLeft, 0.0 );
+ TimeLeft = ABC_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
@@ -240,7 +240,7 @@ ABC_PRT( "Time", clock() - clk );
if ( RetValue == -1 && pParSec->TimeLimit )
{
TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
- TimeLeft = AIG_MAX( TimeLeft, 0.0 );
+ TimeLeft = ABC_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
@@ -275,7 +275,7 @@ ABC_PRT( "Time", clock() - clk );
if ( RetValue == -1 && pParSec->TimeLimit )
{
TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
- TimeLeft = AIG_MAX( TimeLeft, 0.0 );
+ TimeLeft = ABC_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
@@ -315,7 +315,7 @@ ABC_PRT( "Time", clock() - clk );
if ( RetValue == -1 && pParSec->TimeLimit )
{
TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
- TimeLeft = AIG_MAX( TimeLeft, 0.0 );
+ TimeLeft = ABC_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index aff21219..4f164e5c 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -436,7 +436,7 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
Aig_ManForEachPi( p->pAig, pObj, i )
Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
// flip one bit
- Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
+ Limit = ABC_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
}
@@ -458,7 +458,7 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
// flip one bit of the last frame
if ( fUseDist1 ) //&& p->nFrames == 2 )
{
- Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
+ Limit = ABC_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
}
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 5395f361..feee5472 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -24,8 +24,14 @@
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
-
-#include "aig.h"
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
+#include "vec.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@@ -124,6 +130,7 @@ struct Gia_Man_t_
int nFansAlloc; // the size of fanout representation
int * pMapping; // mapping for each node
Gia_Cex_t * pCexComb; // combinational counter-example
+ Gia_Cex_t * pCexSeq; // sequential counter-example
int * pCopies; // intermediate copies
Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc
unsigned char* pSwitching; // switching activity for each object
@@ -174,6 +181,36 @@ extern void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p );
extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
+static inline int Gia_IntAbs( int n ) { return (n < 0)? -n : n; }
+static inline int Gia_Float2Int( float Val ) { return *((int *)&Val); }
+static inline float Gia_Int2Float( int Num ) { return *((float *)&Num); }
+static inline int Gia_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
+static inline int Gia_Base10Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
+static inline char * Gia_UtilStrsav( char * s ) { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL; }
+static inline int Gia_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
+static inline int Gia_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
+static inline int Gia_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
+static inline void Gia_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
+static inline void Gia_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
+static inline unsigned Gia_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); }
+static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
+static inline int Gia_WordCountOnes( unsigned uWord )
+{
+ uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
+ uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
+ uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
+ uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
+ return (uWord & 0x0000FFFF) + (uWord>>16);
+}
+static inline int Gia_WordFindFirstBit( unsigned uWord )
+{
+ int i;
+ for ( i = 0; i < 32; i++ )
+ if ( uWord & (1 << i) )
+ return i;
+ return -1;
+}
+
static inline int Gia_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
static inline int Gia_Lit2Var( int Lit ) { return Lit >> 1; }
@@ -265,8 +302,8 @@ static inline int Gia_ObjValue( Gia_Obj_t * pObj ) {
static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(p->pLevels);return p->pLevels[Gia_ObjId(p, pObj)]; }
static inline int Gia_ObjRefs( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]; }
-static inline void Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); p->pRefs[Gia_ObjId(p, pObj)]++; }
-static inline void Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); p->pRefs[Gia_ObjId(p, pObj)]--; }
+static inline int Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]++; }
+static inline int Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return --p->pRefs[Gia_ObjId(p, pObj)]; }
static inline void Gia_ObjRefFanin0Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin0(pObj)); }
static inline void Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin1(pObj)); }
static inline void Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj)); }
@@ -368,6 +405,7 @@ static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { p
static inline int Gia_ObjProved( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fProved; }
static inline void Gia_ObjSetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 1; }
+static inline void Gia_ObjUnsetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 0; }
static inline int Gia_ObjFailed( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fFailed; }
static inline void Gia_ObjSetFailed( Gia_Man_t * p, int Id ) { p->pReprs[Id].fFailed = 1; }
@@ -451,10 +489,6 @@ static inline int * Gia_ObjGateFanins( Gia_Man_t * p, int Id ) { re
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-/*=== giaAig.c =============================================================*/
-extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p );
-extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
-extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p );
/*=== giaAiger.c ===========================================================*/
extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck );
extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
@@ -509,6 +543,7 @@ extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut );
extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
+extern void Gia_ManEquivImprove( Gia_Man_t * p );
/*=== giaFanout.c =========================================================*/
extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
extern void Gia_ObjRemoveFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
@@ -530,7 +565,7 @@ extern int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
extern int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 );
extern int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 );
extern int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 );
-extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p );
+extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash );
extern void Gia_ManHashProfile( Gia_Man_t * p );
/*=== giaLogic.c ===========================================================*/
extern void Gia_ManTestDistance( Gia_Man_t * p );
@@ -567,6 +602,10 @@ extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames,
/*=== giaTsim.c ============================================================*/
extern Gia_Man_t * Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose );
/*=== giaUtil.c ===========================================================*/
+extern unsigned Gia_ManRandom( int fReset );
+extern void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop );
+extern unsigned int Gia_PrimeCudd( unsigned int p );
+extern char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix );
extern void Gia_ManSetMark0( Gia_Man_t * p );
extern void Gia_ManCleanMark0( Gia_Man_t * p );
extern void Gia_ManCheckMark0( Gia_Man_t * p );
@@ -589,7 +628,7 @@ extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t **
extern Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames );
extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut );
extern void Gia_ManPrintCounterExample( Gia_Cex_t * p );
-
+extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
#ifdef __cplusplus
}
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 1c341d6f..601b85af 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "gia.h"
+#include "giaAig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
new file mode 100644
index 00000000..07cf7bae
--- /dev/null
+++ b/src/aig/gia/giaAig.h
@@ -0,0 +1,62 @@
+/**CFile****************************************************************
+
+ FileName [giaAig.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaAig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __GIA_AIG_H__
+#define __GIA_AIG_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig.h"
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== giaAig.c =============================================================*/
+extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p );
+extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
+extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index adc58e6c..8dbc0cab 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -143,7 +143,7 @@ int Gia_FileSize( char * pFileName )
char * Gia_FileNameGeneric( char * FileName )
{
char * pDot, * pRes;
- pRes = Aig_UtilStrsav( FileName );
+ pRes = Gia_UtilStrsav( FileName );
if ( (pDot = strrchr( pRes, '.' )) )
*pDot = 0;
return pRes;
@@ -412,7 +412,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
// allocate the empty AIG
pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
pName = Gia_FileNameGeneric( pFileName );
- pNew->pName = Aig_UtilStrsav( pName );
+ pNew->pName = Gia_UtilStrsav( pName );
// pNew->pSpec = Aig_UtilStrsav( pFileName );
ABC_FREE( pName );
@@ -549,7 +549,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
pCur++;
// read model name
ABC_FREE( pNew->pName );
- pNew->pName = Aig_UtilStrsav( pCur );
+ pNew->pName = Gia_UtilStrsav( pCur );
}
}
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 15faea72..832eff26 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -20,6 +20,9 @@
#include "gia.h"
+//#define gia_assert(exp) ((void)0)
+//#define gia_assert(exp) (assert(exp))
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c
index b256100c..da48c1b0 100644
--- a/src/aig/gia/giaCof.c
+++ b/src/aig/gia/giaCof.c
@@ -580,7 +580,7 @@ void Cof_ManPrintFanio( Cof_Man_t * p )
}
// allocate storage for fanin/fanout numbers
- nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
+ nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );
@@ -714,7 +714,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
return NULL;
}
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 2510f572..bd5297e4 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -168,7 +168,7 @@ Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCo( p, pObj, i )
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
@@ -200,7 +200,7 @@ Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCoReverse( p, pObj, i )
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
@@ -232,7 +232,7 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@@ -265,7 +265,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
@@ -297,7 +297,7 @@ Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i, iCtrl;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
@@ -337,7 +337,7 @@ Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass )
int i, Counter1 = 0, Counter2 = 0;
assert( p->vFlopClasses != NULL );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
@@ -381,7 +381,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
int i, nRos = 0, nRis = 0;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
@@ -426,7 +426,7 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
int i, t, Entry;
assert( nTimes > 0 );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
vPis = Vec_IntAlloc( Gia_ManPiNum(p) * nTimes );
vPos = Vec_IntAlloc( Gia_ManPoNum(p) * nTimes );
@@ -536,7 +536,7 @@ Gia_Man_t * Gia_ManDupDfs2( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCo( p, pObj, i )
Gia_ManDupDfs2_rec( pNew, p, pObj );
@@ -594,7 +594,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@@ -625,7 +625,7 @@ Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@@ -655,7 +655,7 @@ Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pRoot )
assert( Gia_ObjIsCo(pRoot) );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@@ -682,7 +682,7 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits )
int i, iLit, iLitRes;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@@ -712,7 +712,7 @@ Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@@ -743,7 +743,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManSetRefs( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@@ -797,7 +797,7 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
{
@@ -847,7 +847,7 @@ Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p )
assert( p->pReprsOld != NULL );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@@ -1064,7 +1064,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq
}
// start the manager
pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) );
- pNew->pName = Aig_UtilStrsav( "miter" );
+ pNew->pName = Gia_UtilStrsav( "miter" );
// map combinational inputs
Gia_ManFillValue( p0 );
Gia_ManFillValue( p1 );
@@ -1161,7 +1161,7 @@ Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p )
int i, iLit;
assert( (Gia_ManPoNum(p) & 1) == 0 );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManHashAlloc( pNew );
Gia_ManForEachCi( p, pObj, i )
diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c
index fa172f70..bd14eea9 100644
--- a/src/aig/gia/giaEmbed.c
+++ b/src/aig/gia/giaEmbed.c
@@ -691,7 +691,7 @@ void Emb_ManPrintFanio( Emb_Man_t * p )
}
// allocate storage for fanin/fanout numbers
- nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
+ nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );
@@ -836,14 +836,14 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
int nAttempts = 20;
int i, iNode, Dist, clk;
Emb_Obj_t * pPivot, * pNext;
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
Emb_ManResetTravId( p );
// compute distances from several randomly selected PIs
clk = clock();
printf( "From inputs: " );
for ( i = 0; i < nAttempts; i++ )
{
- iNode = Aig_ManRandom( 0 ) % Emb_ManCiNum(p);
+ iNode = Gia_ManRandom( 0 ) % Emb_ManCiNum(p);
pPivot = Emb_ManCi( p, iNode );
if ( Emb_ObjFanoutNum(pPivot) == 0 )
{ i--; continue; }
@@ -859,7 +859,7 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
printf( "From outputs: " );
for ( i = 0; i < nAttempts; i++ )
{
- iNode = Aig_ManRandom( 0 ) % Emb_ManCoNum(p);
+ iNode = Gia_ManRandom( 0 ) % Emb_ManCoNum(p);
pPivot = Emb_ManCo( p, iNode );
pNext = Emb_ObjFanin( pPivot, 0 );
if ( !Emb_ObjIsNode(pNext) )
@@ -873,7 +873,7 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
printf( "From nodes: " );
for ( i = 0; i < nAttempts; i++ )
{
- iNode = Aig_ManRandom( 0 ) % Gia_ManObjNum(p->pGia);
+ iNode = Gia_ManRandom( 0 ) % Gia_ManObjNum(p->pGia);
if ( !~Gia_ManObj(p->pGia, iNode)->Value )
{ i--; continue; }
pPivot = Emb_ManObj( p, Gia_ManObj(p->pGia, iNode)->Value );
@@ -1043,7 +1043,7 @@ Emb_Obj_t * Emb_ManRandomVertex( Emb_Man_t * p )
{
Emb_Obj_t * pPivot;
do {
- int iNode = (911 * Aig_ManRandom(0)) % Gia_ManObjNum(p->pGia);
+ int iNode = (911 * Gia_ManRandom(0)) % Gia_ManObjNum(p->pGia);
if ( ~Gia_ManObj(p->pGia, iNode)->Value )
pPivot = Emb_ManObj( p, Gia_ManObj(p->pGia, iNode)->Value );
else
@@ -1240,7 +1240,7 @@ void Emb_ManVecRandom( float * pVec, int nDims )
{
int i;
for ( i = 0; i < nDims; i++ )
- pVec[i] = Aig_ManRandom( 0 );
+ pVec[i] = Gia_ManRandom( 0 );
}
/**Function*************************************************************
@@ -1702,7 +1702,7 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI
printf( "Emb_ManDumpGnuplot(): Placement is not available.\n" );
return;
}
- sprintf( Buffer, "%s%s", pDirectory, Aig_FileNameGenericAppend(pName, ".plt") );
+ sprintf( Buffer, "%s%s", pDirectory, Gia_FileNameGenericAppend(pName, ".plt") );
pFile = fopen( Buffer, "w" );
fprintf( pFile, "# This Gnuplot file was produced by ABC on %s\n", Ioa_TimeStamp() );
fprintf( pFile, "\n" );
@@ -1712,7 +1712,7 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI
{
// fprintf( pFile, "set terminal postscript\n" );
fprintf( pFile, "set terminal gif font \'arial\' 10 size 800,600 xffffff x000000 x000000 x000000\n" );
- fprintf( pFile, "set output \'%s\'\n", Aig_FileNameGenericAppend(pName, ".gif") );
+ fprintf( pFile, "set output \'%s\'\n", Gia_FileNameGenericAppend(pName, ".gif") );
fprintf( pFile, "\n" );
}
fprintf( pFile, "set title \"%s : PI = %d PO = %d FF = %d Node = %d Obj = %d HPWL = %.2e\\n",
@@ -1806,7 +1806,7 @@ clk = clock();
// Emb_ManPrintFanio( p );
// prepare data-structure
- Aig_ManRandom( 1 ); // reset random numbers for deterministic behavior
+ Gia_ManRandom( 1 ); // reset random numbers for deterministic behavior
Emb_ManResetTravId( p );
Emb_ManSetValue( p );
clkSetup = clock() - clk;
diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c
index 13d6145c..c768bb43 100644
--- a/src/aig/gia/giaEnable.c
+++ b/src/aig/gia/giaEnable.c
@@ -362,7 +362,7 @@ Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames )
ABC_FREE( p->pCopies );
p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i )
Gia_ObjSetCopyF( p, 0, pObj, 0 );
@@ -437,7 +437,7 @@ Gia_Man_t * Gia_ManRemoveEnables2( Gia_Man_t * p )
Gia_Obj_t * pThis, * pNode;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
@@ -607,7 +607,7 @@ Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p )
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 79345fd0..f802e15d 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -330,7 +330,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
if ( fDualOut )
Gia_ManEquivSetColors( p, fVerbose );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@@ -682,7 +682,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
if ( fDualOut )
Gia_ManEquivSetColors( p, fVerbose );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@@ -809,10 +809,10 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
if ( fDualOut )
Gia_ManEquivSetColors( p, 0 );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i )
- Gia_ObjSetCopyF( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) );
+ Gia_ObjSetCopyF( p, 0, pObj, Gia_InfoHasBit(pInit->pData, i) );
for ( f = 0; f < nFrames; f++ )
{
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
@@ -906,6 +906,66 @@ void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose )
nRemovedClas, nTotalClas, nRemovedLits, nTotalLits );
}
+/**Function*************************************************************
+
+ Synopsis [Transforms equiv classes by setting a good representative.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManEquivImprove( Gia_Man_t * p )
+{
+ Vec_Int_t * vClass;
+ int i, k, iNode, iRepr;
+ int iReprBest, iLevelBest, iLevelCur, iMffcBest, iMffcCur;
+ assert( p->pReprs != NULL && p->pNexts != NULL );
+ Gia_ManLevelNum( p );
+ Gia_ManCreateRefs( p );
+ // iterate over class candidates
+ vClass = Vec_IntAlloc( 100 );
+ Gia_ManForEachClass( p, i )
+ {
+ Vec_IntClear( vClass );
+ iReprBest = -1;
+ iLevelBest = iMffcBest = ABC_INFINITY;
+ Gia_ClassForEachObj( p, i, k )
+ {
+ iLevelCur = Gia_ObjLevel( p,Gia_ManObj(p, k) );
+ iMffcCur = Gia_NodeMffcSize( p, Gia_ManObj(p, k) );
+ if ( iLevelBest > iLevelCur || (iLevelBest == iLevelCur && iMffcBest > iMffcCur) )
+ {
+ iReprBest = k;
+ iLevelBest = iLevelCur;
+ iMffcBest = iMffcCur;
+ }
+ Vec_IntPush( vClass, k );
+ }
+ assert( Vec_IntSize( vClass ) > 1 );
+ assert( iReprBest > 0 );
+ if ( i == iReprBest )
+ continue;
+/*
+ printf( "Repr/Best = %6d/%6d. Lev = %3d/%3d. Mffc = %3d/%3d.\n",
+ i, iReprBest, Gia_ObjLevel( p,Gia_ManObj(p, i) ), Gia_ObjLevel( p,Gia_ManObj(p, iReprBest) ),
+ Gia_NodeMffcSize( p, Gia_ManObj(p, i) ), Gia_NodeMffcSize( p, Gia_ManObj(p, iReprBest) ) );
+*/
+ iRepr = iReprBest;
+ Gia_ObjSetRepr( p, iRepr, GIA_VOID );
+ Gia_ObjSetProved( p, i );
+ Gia_ObjUnsetProved( p, iRepr );
+ Vec_IntForEachEntry( vClass, iNode, k )
+ if ( iNode != iRepr )
+ Gia_ObjSetRepr( p, iNode, iRepr );
+ }
+ Vec_IntFree( vClass );
+ ABC_FREE( p->pNexts );
+// p->pNexts = Gia_ManDeriveNexts( p );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaFanout.c b/src/aig/gia/giaFanout.c
index 42ccd7e7..b32484af 100644
--- a/src/aig/gia/giaFanout.c
+++ b/src/aig/gia/giaFanout.c
@@ -117,7 +117,7 @@ void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout )
assert( Gia_ObjId(p, pFanout) > 0 );
if ( Gia_ObjId(p, pObj) >= p->nFansAlloc || Gia_ObjId(p, pFanout) >= p->nFansAlloc )
{
- int nFansAlloc = 2 * AIG_MAX( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) );
+ int nFansAlloc = 2 * ABC_MAX( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) );
p->pFanData = ABC_REALLOC( int, p->pFanData, 5 * nFansAlloc );
memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) );
p->nFansAlloc = nFansAlloc;
diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c
index cf4c4aa5..04c8f2e7 100644
--- a/src/aig/gia/giaForce.c
+++ b/src/aig/gia/giaForce.c
@@ -747,7 +747,7 @@ void Frc_ManPlaceRandom( Frc_Man_t * p )
pPlacement[i] = i;
for ( i = 0; i < p->nObjs; i++ )
{
- iNext = Aig_ManRandom( 0 ) % p->nObjs;
+ iNext = Gia_ManRandom( 0 ) % p->nObjs;
Temp = pPlacement[i];
pPlacement[i] = pPlacement[iNext];
pPlacement[iNext] = Temp;
@@ -774,7 +774,7 @@ void Frc_ManArrayShuffle( Vec_Int_t * vArray )
int i, iNext, Temp;
for ( i = 0; i < vArray->nSize; i++ )
{
- iNext = Aig_ManRandom( 0 ) % vArray->nSize;
+ iNext = Gia_ManRandom( 0 ) % vArray->nSize;
Temp = vArray->pArray[i];
vArray->pArray[i] = vArray->pArray[iNext];
vArray->pArray[iNext] = Temp;
@@ -1036,7 +1036,7 @@ void Frc_DumpGraphIntoFile( Frc_Man_t * p )
void For_ManExperiment( Gia_Man_t * pGia, int nIters, int fClustered, int fVerbose )
{
Frc_Man_t * p;
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
if ( fClustered )
p = Frc_ManStart( pGia );
else
diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c
index e99ef514..c0ea6680 100644
--- a/src/aig/gia/giaFrames.c
+++ b/src/aig/gia/giaFrames.c
@@ -180,7 +180,7 @@ Gia_Man_t * Gia_ManFramesInit( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
Gia_ManFraSupports( p );
pFrames = Gia_ManStart( Vec_VecSizeSize((Vec_Vec_t*)p->vIns)+
Vec_VecSizeSize((Vec_Vec_t*)p->vAnds)+Vec_VecSizeSize((Vec_Vec_t*)p->vOuts) );
- pFrames->pName = Aig_UtilStrsav( pAig->pName );
+ pFrames->pName = Gia_UtilStrsav( pAig->pName );
Gia_ManHashAlloc( pFrames );
Gia_ManConst0(pAig)->Value = 0;
for ( f = 0; f < pPars->nFrames; f++ )
@@ -290,7 +290,7 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
if ( pPars->fInit )
return Gia_ManFramesInit( pAig, pPars );
pFrames = Gia_ManStart( pPars->nFrames * Gia_ManObjNum(pAig) );
- pFrames->pName = Aig_UtilStrsav( pAig->pName );
+ pFrames->pName = Gia_UtilStrsav( pAig->pName );
Gia_ManHashAlloc( pFrames );
Gia_ManConst0(pAig)->Value = 0;
for ( f = 0; f < pPars->nFrames; f++ )
diff --git a/src/aig/gia/giaFront.c b/src/aig/gia/giaFront.c
index ee9e5b5f..b3a3c2d0 100644
--- a/src/aig/gia/giaFront.c
+++ b/src/aig/gia/giaFront.c
@@ -112,7 +112,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
Gia_ManSetRefs( p );
// start the new manager
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
pNew->nFront = 1 + (int)((float)1.1 * nCrossCutMaxInit);
// start the frontier
pFront = ABC_CALLOC( char, pNew->nFront );
diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c
index 443a1ae8..ed636540 100644
--- a/src/aig/gia/giaGlitch.c
+++ b/src/aig/gia/giaGlitch.c
@@ -330,7 +330,7 @@ static inline int Gli_NodeComputeValue( Gli_Obj_t * pNode )
int i, Phase = 0;
for ( i = 0; i < (int)pNode->nFanins; i++ )
Phase |= (Gli_ObjFanin(pNode, i)->fPhase << i);
- return Aig_InfoHasBit( pNode->uTruth, Phase );
+ return Gia_InfoHasBit( pNode->uTruth, Phase );
}
/**Function*************************************************************
@@ -349,7 +349,7 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode )
int i, Phase = 0;
for ( i = 0; i < (int)pNode->nFanins; i++ )
Phase |= (Gli_ObjFanin(pNode, i)->fPhase2 << i);
- return Aig_InfoHasBit( pNode->uTruth, Phase );
+ return Gia_InfoHasBit( pNode->uTruth, Phase );
}
/**Function*************************************************************
@@ -429,7 +429,7 @@ void Gli_ManSetPiRandom( Gli_Man_t * p, float PiTransProb )
assert( 0.0 < PiTransProb && PiTransProb < 1.0 );
Vec_IntClear( p->vCisChanged );
Gli_ManForEachCi( p, pObj, i )
- if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb )
+ if ( Multi * (Gia_ManRandom(0) & 0xffff) < PiTransProb )
{
Vec_IntPush( p->vCisChanged, pObj->Handle );
pObj->fPhase ^= 1;
@@ -590,7 +590,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode )
for ( k = 0; k < nFanins; k++ )
if ( (pSimInfos[k] >> i) & 1 )
Phase |= (1 << k);
- if ( Aig_InfoHasBit( pNode->uTruth, Phase ) )
+ if ( Gia_InfoHasBit( pNode->uTruth, Phase ) )
Result |= (1 << i);
}
return Result;
@@ -612,9 +612,9 @@ static inline unsigned Gli_ManUpdateRandomInput( unsigned uInfo, float PiTransPr
float Multi = 1.0 / (1 << 16);
int i;
if ( PiTransProb == 0.5 )
- return Aig_ManRandom(0);
+ return Gia_ManRandom(0);
for ( i = 0; i < 32; i++ )
- if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb )
+ if ( Multi * (Gia_ManRandom(0) & 0xffff) < PiTransProb )
uInfo ^= (1 << i);
return uInfo;
}
@@ -703,7 +703,7 @@ void Gli_ManSetPiRandomSeq( Gli_Man_t * p, float PiTransProb )
// set changed PIs
Vec_IntClear( p->vCisChanged );
Gli_ManForEachPi( p, pObj, i )
- if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb )
+ if ( Multi * (Gia_ManRandom(0) & 0xffff) < PiTransProb )
{
Vec_IntPush( p->vCisChanged, pObj->Handle );
pObj->fPhase ^= 1;
@@ -738,7 +738,7 @@ void Gli_ManSetPiRandomSeq( Gli_Man_t * p, float PiTransProb )
void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb, int fVerbose )
{
int i, k, clk = clock();
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
Gli_ManFinalize( p );
if ( p->nRegs == 0 )
{
@@ -752,7 +752,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb
}
else
{
- int nIters = Aig_BitWordNum(nPatterns);
+ int nIters = Gia_BitWordNum(nPatterns);
Gli_ManSimulateSeqPref( p, 16 );
for ( i = 0; i < 32; i++ )
{
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index a7cae8fe..97326c92 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -86,7 +86,7 @@ static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1 )
void Gia_ManHashAlloc( Gia_Man_t * p )
{
assert( p->pHTable == NULL );
- p->nHTable = Aig_PrimeCudd( p->nObjsAlloc );
+ p->nHTable = Gia_PrimeCudd( p->nObjsAlloc );
p->pHTable = ABC_CALLOC( int, p->nHTable );
}
@@ -152,7 +152,7 @@ void Gia_ManHashResize( Gia_Man_t * p )
// replace the table
pHTableOld = p->pHTable;
nHTableOld = p->nHTable;
- p->nHTable = Aig_PrimeCudd( 2 * Gia_ManAndNum(p) );
+ p->nHTable = Gia_PrimeCudd( 2 * Gia_ManAndNum(p) );
p->pHTable = ABC_CALLOC( int, p->nHTable );
// rehash the entries from the old table
Counter = 0;
@@ -322,14 +322,14 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O
{
Gia_Obj_t * pNode0, * pNode1, * pFanA, * pFanB, * pFanC, * pFanD;
assert( p->fAddStrash );
- if ( !Gia_ObjIsAnd(Gia_Regular(p0)) && !Gia_ObjIsAnd(Gia_Regular(p1)) )
- return NULL;
pNode0 = Gia_Regular(p0);
pNode1 = Gia_Regular(p1);
- pFanA = Gia_ObjChild0(pNode0);
- pFanB = Gia_ObjChild1(pNode0);
- pFanC = Gia_ObjChild0(pNode1);
- pFanD = Gia_ObjChild1(pNode1);
+ if ( !Gia_ObjIsAnd(pNode0) && !Gia_ObjIsAnd(pNode1) )
+ return NULL;
+ pFanA = Gia_ObjIsAnd(pNode0) ? Gia_ObjChild0(pNode0) : NULL;
+ pFanB = Gia_ObjIsAnd(pNode0) ? Gia_ObjChild1(pNode0) : NULL;
+ pFanC = Gia_ObjIsAnd(pNode1) ? Gia_ObjChild0(pNode1) : NULL;
+ pFanD = Gia_ObjIsAnd(pNode1) ? Gia_ObjChild1(pNode1) : NULL;
if ( Gia_IsComplement(p0) )
{
if ( pFanA == Gia_Not(p1) || pFanB == Gia_Not(p1) )
@@ -404,6 +404,7 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O
if ( pFanB == pFanD && pFanA == Gia_Not(pFanC) )
return Gia_Not(pFanB);
}
+/*
if ( !Gia_IsComplement(p0) || !Gia_IsComplement(p1) )
return NULL;
if ( !Gia_ObjIsAnd(pNode0) || !Gia_ObjIsAnd(pNode1) )
@@ -424,8 +425,12 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O
}
pNode0 = Gia_ManHashAndP( p, Gia_Not(pNodeC), pNodeE );
pNode1 = Gia_ManHashAndP( p, pNodeC, pNodeT );
- return Gia_NotCond( Gia_ManHashAndP( p, pNode0, pNode1 ), !fCompl );
+ p->fAddStrash = 0;
+ pNodeC = Gia_NotCond( Gia_ManHashAndP( p, Gia_Not(pNode0), Gia_Not(pNode1) ), !fCompl );
+ p->fAddStrash = 1;
+ return pNodeC;
}
+*/
return NULL;
}
@@ -555,13 +560,14 @@ int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManRehash( Gia_Man_t * p )
+Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash )
{
- Gia_Man_t * pNew;
+ Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
+ pNew->fAddStrash = fAddStrash;
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj( p, pObj, i )
@@ -574,8 +580,11 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
Gia_ManHashStop( pNew );
+ pNew->fAddStrash = 0;
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
// printf( "Top gate is %s\n", Gia_ObjFaninC0(Gia_ManCo(pNew, 0))? "OR" : "AND" );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
return pNew;
}
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index dba90507..f69ac266 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -72,6 +72,7 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_IntFree( p->vCos );
ABC_FREE( p->pPlacement );
ABC_FREE( p->pSwitching );
+ ABC_FREE( p->pCexSeq );
ABC_FREE( p->pCexComb );
ABC_FREE( p->pIso );
ABC_FREE( p->pMapping );
diff --git a/src/aig/gia/giaRetime.c b/src/aig/gia/giaRetime.c
index 965b5981..69dea59d 100644
--- a/src/aig/gia/giaRetime.c
+++ b/src/aig/gia/giaRetime.c
@@ -122,7 +122,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut )
int i;
// create the new manager
pNew = Gia_ManStart( Gia_ManObjNum(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
// create the true PIs
Gia_ManFillValue( p );
diff --git a/src/aig/gia/giaSat.c b/src/aig/gia/giaSat.c
index 6d127223..29ade5c6 100644
--- a/src/aig/gia/giaSat.c
+++ b/src/aig/gia/giaSat.c
@@ -262,7 +262,7 @@ int Gia_ManSatPartCount( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnLeaves, int *
(*pnLeaves)++;
else
Level1 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC1(pObj);
- return AIG_MAX( Level0, Level1 );
+ return ABC_MAX( Level0, Level1 );
}
/**Function*************************************************************
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 020683ad..ae9e304c 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -64,7 +64,7 @@ void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p )
p->nIters = 32; // the number of timeframes
p->TimeLimit = 60; // time limit in seconds
p->fCheckMiter = 0; // check if miter outputs are non-zero
- p->fVerbose = 1; // enables verbose output
+ p->fVerbose = 0; // enables verbose output
}
/**Function*************************************************************
@@ -92,7 +92,7 @@ Gia_ManSim_t * Gia_ManSimCreate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
p->pDataSimCos = ABC_ALLOC( unsigned, p->nWords * Gia_ManCoNum(p->pAig) );
p->vCis2Ids = Vec_IntAlloc( Gia_ManCiNum(p->pAig) );
Vec_IntForEachEntry( pAig->vCis, Entry, i )
- Vec_IntPush( p->vCis2Ids, Entry );
+ Vec_IntPush( p->vCis2Ids, i ); // do we need p->vCis2Ids?
printf( "AIG = %7.2f Mb. Front mem = %7.2f Mb. Other mem = %7.2f Mb.\n",
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
4.0*p->nWords*p->pAig->nFront/(1<<20),
@@ -136,7 +136,7 @@ static inline void Gia_ManSimInfoRandom( Gia_ManSim_t * p, unsigned * pInfo )
{
int w;
for ( w = p->nWords-1; w >= 0; w-- )
- pInfo[w] = Aig_ManRandom( 0 );
+ pInfo[w] = Gia_ManRandom( 0 );
}
/**Function*************************************************************
@@ -173,7 +173,7 @@ static inline int Gia_ManSimInfoIsZero( Gia_ManSim_t * p, unsigned * pInfo )
int w;
for ( w = p->nWords-1; w >= 0; w-- )
if ( pInfo[w] )
- return 32*(w-1) + Aig_WordFindFirstBit( pInfo[w] );
+ return 32*(w-1) + Gia_WordFindFirstBit( pInfo[w] );
return -1;
}
@@ -382,6 +382,71 @@ static inline void Gia_ManSimulateRound( Gia_ManSim_t * p )
/**Function*************************************************************
+ Synopsis [Returns index of the PO and pattern that failed it.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Gia_ManCheckPos( Gia_ManSim_t * p, int * piPo, int * piPat )
+{
+ int i, iPat;
+ for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
+ {
+ iPat = Gia_ManSimInfoIsZero( p, Gia_SimDataCo(p, i) );
+ if ( iPat >= 0 )
+ {
+ *piPo = i;
+ *piPat = iPat;
+ return 1;
+ }
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids )
+{
+ Gia_Cex_t * p;
+ unsigned * pData;
+ int f, i, w, iPioId, Counter;
+ p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
+ p->iFrame = iFrame;
+ p->iPo = iOut;
+ // fill in the binary data
+ Gia_ManRandom( 1 );
+ Counter = p->nRegs;
+ pData = ABC_ALLOC( unsigned, nWords );
+ for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
+ for ( i = 0; i < Gia_ManPiNum(pAig); i++ )
+ {
+ iPioId = Vec_IntEntry( vCis2Ids, i );
+ if ( iPioId >= p->nPis )
+ continue;
+ for ( w = nWords-1; w >= 0; w-- )
+ pData[w] = Gia_ManRandom( 0 );
+ if ( Gia_InfoHasBit( pData, iPat ) )
+ Gia_InfoSetBit( p->pData, Counter + iPioId );
+ }
+ ABC_FREE( pData );
+ return p;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -394,40 +459,53 @@ static inline void Gia_ManSimulateRound( Gia_ManSim_t * p )
int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
{
Gia_ManSim_t * p;
- int i, clk = clock();
+ int i, clkTotal = clock();
+ int iOut, iPat, RetValue = 0;
+ ABC_FREE( pAig->pCexSeq );
p = Gia_ManSimCreate( pAig, pPars );
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
Gia_ManSimInfoInit( p );
for ( i = 0; i < pPars->nIters; i++ )
{
Gia_ManSimulateRound( p );
-/*
+
if ( pPars->fVerbose )
{
printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
- printf( "Time = %7.2f sec\r", (1.0*clock()-clk)/CLOCKS_PER_SEC );
+ printf( "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
}
if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
{
- assert( pAig->pSeqModel == NULL );
- pAig->pSeqModel = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
- if ( pPars->fVerbose )
- printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
+ pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", iOut, i );
+ if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
+ {
+ printf( "\n" );
+ printf( "Generated counter-example is INVALID \n" );
+ printf( "\n" );
+ }
+ else
+ {
+ printf( "\n" );
+ printf( "Generated counter-example is fine \n" );
+ printf( "\n" );
+ }
+ RetValue = 1;
break;
}
if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
{
- printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, pPars->TimeLimit );
+ printf( "No bug detected after %d frames with time limit %d seconds. \n", i+1, pPars->TimeLimit );
break;
}
-*/
+
if ( i < pPars->nIters - 1 )
Gia_ManSimInfoTransfer( p );
}
Gia_ManSimDelete( p );
- printf( "Simulated %d frames with %d words. ", pPars->nIters, pPars->nWords );
- ABC_PRT( "Time", clock() - clk );
- return 0;
+ printf( "Simulated %d frames with %d words. ", i, pPars->nWords );
+ ABC_PRT( "Time", clock() - clkTotal );
+ return RetValue;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c
index 713f224b..5dac1fbc 100644
--- a/src/aig/gia/giaSwitch.c
+++ b/src/aig/gia/giaSwitch.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "gia.h"
+#include "giaAig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -146,23 +146,23 @@ static inline void Gia_ManSwiSimInfoRandom( Gia_ManSwi_t * p, unsigned * pInfo,
int w, i;
if ( nProbNum == -1 )
{ // 3/8 = 1/4 + 1/8
- Mask = (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 )) |
- (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ));
+ Mask = (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 )) |
+ (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ));
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] ^= Mask;
}
else if ( nProbNum > 0 )
{
- Mask = Aig_ManRandom( 0 );
+ Mask = Gia_ManRandom( 0 );
for ( i = 0; i < nProbNum; i++ )
- Mask &= Aig_ManRandom( 0 );
+ Mask &= Gia_ManRandom( 0 );
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] ^= Mask;
}
else if ( nProbNum == 0 )
{
for ( w = p->nWords-1; w >= 0; w-- )
- pInfo[w] = Aig_ManRandom( 0 );
+ pInfo[w] = Gia_ManRandom( 0 );
}
else
assert( 0 );
@@ -185,14 +185,14 @@ static inline void Gia_ManSwiSimInfoRandomShift( Gia_ManSwi_t * p, unsigned * pI
int w, i;
if ( nProbNum == -1 )
{ // 3/8 = 1/4 + 1/8
- Mask = (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 )) |
- (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ));
+ Mask = (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 )) |
+ (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ));
}
else if ( nProbNum >= 0 )
{
- Mask = Aig_ManRandom( 0 );
+ Mask = Gia_ManRandom( 0 );
for ( i = 0; i < nProbNum; i++ )
- Mask &= Aig_ManRandom( 0 );
+ Mask &= Gia_ManRandom( 0 );
}
else
assert( 0 );
@@ -430,7 +430,7 @@ static inline int Gia_ManSwiSimInfoCountOnes( Gia_ManSwi_t * p, int iPlace )
int w, Counter = 0;
pInfo = Gia_SwiData( p, iPlace );
for ( w = p->nWords-1; w >= 0; w-- )
- Counter += Aig_WordCountOnes( pInfo[w] );
+ Counter += Gia_WordCountOnes( pInfo[w] );
return Counter;
}
@@ -451,7 +451,7 @@ static inline int Gia_ManSwiSimInfoCountTrans( Gia_ManSwi_t * p, int iPlace )
int w, Counter = 0;
pInfo = Gia_SwiData( p, iPlace );
for ( w = p->nWords-1; w >= 0; w-- )
- Counter += 2*Aig_WordCountOnes( (pInfo[w] ^ (pInfo[w] >> 16)) & 0xffff );
+ Counter += 2*Gia_WordCountOnes( (pInfo[w] ^ (pInfo[w] >> 16)) & 0xffff );
return Counter;
}
@@ -565,7 +565,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
{
printf( "Obj = %8d (%8d). F = %6d. ",
pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront,
- 4.0*Aig_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
+ 4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb. ",
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
4.0*p->nWords*p->pAig->nFront/(1<<20),
@@ -573,7 +573,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
ABC_PRT( "Time", clock() - clk );
}
// perform simulation
- Aig_ManRandom( 1 );
+ Gia_ManRandom( 1 );
Gia_ManSwiSimInfoInit( p );
for ( i = 0; i < pPars->nIters; i++ )
{
@@ -612,7 +612,6 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
return vSwitching;
}
-
/**Function*************************************************************
Synopsis [Computes probability of switching (or of being 1).]
diff --git a/src/aig/gia/giaTsim.c b/src/aig/gia/giaTsim.c
index 8cfe5959..a4cdf88a 100644
--- a/src/aig/gia/giaTsim.c
+++ b/src/aig/gia/giaTsim.c
@@ -81,15 +81,15 @@ Gia_ManTer_t * Gia_ManTerCreate( Gia_Man_t * pAig )
p = ABC_CALLOC( Gia_ManTer_t, 1 );
p->pAig = Gia_ManFront( pAig );
p->nIters = 300;
- p->pDataSim = ABC_ALLOC( unsigned, Aig_BitWordNum(2*p->pAig->nFront) );
- p->pDataSimCis = ABC_ALLOC( unsigned, Aig_BitWordNum(2*Gia_ManCiNum(p->pAig)) );
- p->pDataSimCos = ABC_ALLOC( unsigned, Aig_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
+ p->pDataSim = ABC_ALLOC( unsigned, Gia_BitWordNum(2*p->pAig->nFront) );
+ p->pDataSimCis = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCiNum(p->pAig)) );
+ p->pDataSimCos = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
// allocate storage for terminary states
- p->nStateWords = Aig_BitWordNum( 2*Gia_ManRegNum(pAig) );
+ p->nStateWords = Gia_BitWordNum( 2*Gia_ManRegNum(pAig) );
p->vStates = Vec_PtrAlloc( 1000 );
p->pCount0 = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
p->pCountX = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
- p->nBins = Aig_PrimeCudd( 500 );
+ p->nBins = Gia_PrimeCudd( 500 );
p->pBins = ABC_CALLOC( unsigned *, p->nBins );
p->vRetired = Vec_IntAlloc( 100 );
p->pRetired = ABC_CALLOC( char, Gia_ManRegNum(pAig) );
@@ -508,7 +508,7 @@ void Gia_ManTerAnalyze2( Vec_Ptr_t * vStates, int nRegs )
unsigned * pTemp, * pStates = Vec_PtrPop( vStates );
int i, w, nZeros, nConsts, nStateWords;
// detect constant zero registers
- nStateWords = Aig_BitWordNum( 2*nRegs );
+ nStateWords = Gia_BitWordNum( 2*nRegs );
memset( pStates, 0, sizeof(int) * nStateWords );
Vec_PtrForEachEntry( vStates, pTemp, i )
for ( w = 0; w < nStateWords; w++ )
@@ -576,7 +576,7 @@ Vec_Ptr_t * Gia_ManTerTranspose( Gia_ManTer_t * p )
unsigned * pState, * pFlop;
int i, k, nFlopWords;
vFlops = Vec_PtrAlloc( 100 );
- nFlopWords = Aig_BitWordNum( 2*Vec_PtrSize(p->vStates) );
+ nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) );
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
if ( p->pCount0[i] == Vec_PtrSize(p->vStates) )
@@ -631,7 +631,7 @@ int * Gia_ManTerCreateMap( Gia_ManTer_t * p, int fVerbose )
Gia_Obj_t * pObj;
Vec_Int_t * vMapKtoI;
int i, iRepr, nFlopWords, Counter0 = 0, CounterE = 0;
- nFlopWords = Aig_BitWordNum( 2*Vec_PtrSize(p->vStates) );
+ nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) );
p->vFlops = Gia_ManTerTranspose( p );
pCi2Lit = ABC_FALLOC( unsigned, Gia_ManCiNum(p->pAig) );
vMapKtoI = Vec_IntAlloc( 100 );
@@ -679,11 +679,11 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose )
{
printf( "Obj = %8d (%8d). F = %6d. ",
pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront,
- 4.0*Aig_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
+ 4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb. ",
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
- 4.0*Aig_BitWordNum(2 * p->pAig->nFront)/(1<<20),
- 4.0*Aig_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) );
+ 4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20),
+ 4.0*Gia_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) );
ABC_PRT( "Time", clock() - clk );
}
// perform simulation
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 822f1e64..5716c1a0 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -23,6 +23,9 @@
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+
+#define NUMBER1 3716960521u
+#define NUMBER2 2174103536u
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -30,6 +33,113 @@
/**Function*************************************************************
+ Synopsis [Creates a sequence or random numbers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]
+
+***********************************************************************/
+unsigned Gia_ManRandom( int fReset )
+{
+ static unsigned int m_z = NUMBER1;
+ static unsigned int m_w = NUMBER2;
+ if ( fReset )
+ {
+ m_z = NUMBER1;
+ m_w = NUMBER2;
+ }
+ m_z = 36969 * (m_z & 65535) + (m_z >> 16);
+ m_w = 18000 * (m_w & 65535) + (m_w >> 16);
+ return (m_z << 16) + m_w;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Creates random info for the primary inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop )
+{
+ unsigned * pInfo;
+ int i, w;
+ Vec_PtrForEachEntryStart( vInfo, pInfo, i, iInputStart )
+ for ( w = iWordStart; w < iWordStop; w++ )
+ pInfo[w] = Gia_ManRandom(0);
+}
+
+/**Function********************************************************************
+
+ Synopsis [Returns the next prime >= p.]
+
+ Description [Copied from CUDD, for stand-aloneness.]
+
+ SideEffects [None]
+
+ SeeAlso []
+
+******************************************************************************/
+unsigned int Gia_PrimeCudd( unsigned int p )
+{
+ int i,pn;
+
+ p--;
+ do {
+ p++;
+ if (p&1) {
+ pn = 1;
+ i = 3;
+ while ((unsigned) (i * i) <= p) {
+ if (p % i == 0) {
+ pn = 0;
+ break;
+ }
+ i += 2;
+ }
+ } else {
+ pn = 0;
+ }
+ } while (!pn);
+ return(p);
+
+} /* end of Cudd_Prime */
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns the composite name of the file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix )
+{
+ static char Buffer[1000];
+ char * pDot;
+ strcpy( Buffer, pBase );
+ if ( (pDot = strrchr( Buffer, '.' )) )
+ *pDot = 0;
+ strcat( Buffer, pSuffix );
+ if ( (pDot = strrchr( Buffer, '\\' )) || (pDot = strrchr( Buffer, '/' )) )
+ return pDot+1;
+ return Buffer;
+}
+
+/**Function*************************************************************
+
Synopsis [Sets phases of the internal nodes.]
Description []
@@ -592,7 +702,7 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob
Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames )
{
Gia_Cex_t * pCex;
- int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
+ int nWords = Gia_BitWordNum( nRegs + nRealPis * nFrames );
pCex = (Gia_Cex_t *)ABC_ALLOC( char, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords );
memset( pCex, 0, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords );
pCex->nRegs = nRegs;
@@ -617,11 +727,11 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut )
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
Gia_ManForEachRo( pAig, pObj, i )
- pObj->fMark0 = Aig_InfoHasBit(p->pData, iBit++);
+ pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
for ( i = 0; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
- pObj->fMark0 = Aig_InfoHasBit(p->pData, iBit++);
+ pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
Gia_ManForEachAnd( pAig, pObj, k )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
@@ -657,18 +767,97 @@ void Gia_ManPrintCounterExample( Gia_Cex_t * p )
p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits );
printf( "State : " );
for ( k = 0; k < p->nRegs; k++ )
- printf( "%d", Aig_InfoHasBit(p->pData, k) );
+ printf( "%d", Gia_InfoHasBit(p->pData, k) );
printf( "\n" );
for ( f = 0; f <= p->iFrame; f++ )
{
printf( "Frame %2d : ", f );
for ( i = 0; i < p->nPis; i++ )
- printf( "%d", Aig_InfoHasBit(p->pData, k++) );
+ printf( "%d", Gia_InfoHasBit(p->pData, k++) );
printf( "\n" );
}
assert( k == p->nBits );
}
+/**Function*************************************************************
+
+ Synopsis [Dereferences the node's MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_NodeDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
+{
+ Gia_Obj_t * pFanin;
+ int Counter = 0;
+ if ( Gia_ObjIsCi(pNode) )
+ return 0;
+ assert( Gia_ObjIsAnd(pNode) );
+ pFanin = Gia_ObjFanin0(pNode);
+ assert( Gia_ObjRefs(p, pFanin) > 0 );
+ if ( Gia_ObjRefDec(p, pFanin) == 0 )
+ Counter += Gia_NodeDeref_rec( p, pFanin );
+ pFanin = Gia_ObjFanin1(pNode);
+ assert( Gia_ObjRefs(p, pFanin) > 0 );
+ if ( Gia_ObjRefDec(p, pFanin) == 0 )
+ Counter += Gia_NodeDeref_rec( p, pFanin );
+ return Counter + 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [References the node's MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_NodeRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
+{
+ Gia_Obj_t * pFanin;
+ int Counter = 0;
+ if ( Gia_ObjIsCi(pNode) )
+ return 0;
+ assert( Gia_ObjIsAnd(pNode) );
+ pFanin = Gia_ObjFanin0(pNode);
+ if ( Gia_ObjRefInc(p, pFanin) == 0 )
+ Counter += Gia_NodeRef_rec( p, pFanin );
+ pFanin = Gia_ObjFanin1(pNode);
+ if ( Gia_ObjRefInc(p, pFanin) == 0 )
+ Counter += Gia_NodeRef_rec( p, pFanin );
+ return Counter + 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of internal nodes in the MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode )
+{
+ int ConeSize1, ConeSize2;
+ assert( !Gia_IsComplement(pNode) );
+ assert( Gia_ObjIsCand(pNode) );
+ ConeSize1 = Gia_NodeDeref_rec( p, pNode );
+ ConeSize2 = Gia_NodeRef_rec( p, pNode );
+ assert( ConeSize1 == ConeSize2 );
+ assert( ConeSize1 >= 0 );
+ return ConeSize1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index 1e58e825..15641250 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -112,9 +112,6 @@ struct Hop_Man_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-#define AIG_MIN(a,b) (((a) < (b))? (a) : (b))
-#define AIG_MAX(a,b) (((a) > (b))? (a) : (b))
-
static inline int Hop_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
static inline int Hop_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline int Hop_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
@@ -186,7 +183,7 @@ static inline Hop_Obj_t * Hop_ObjChild1( Hop_Obj_t * pObj ) { return pObj-
static inline Hop_Obj_t * Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin0(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin0(pObj)->pData, Hop_ObjFaninC0(pObj)) : NULL; }
static inline Hop_Obj_t * Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL; }
static inline int Hop_ObjLevel( Hop_Obj_t * pObj ) { return pObj->nRefs; }
-static inline int Hop_ObjLevelNew( Hop_Obj_t * pObj ) { return 1 + Hop_ObjIsExor(pObj) + AIG_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs); }
+static inline int Hop_ObjLevelNew( Hop_Obj_t * pObj ) { return 1 + Hop_ObjIsExor(pObj) + ABC_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs); }
static inline int Hop_ObjPhaseCompl( Hop_Obj_t * pObj ) { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; }
static inline void Hop_ObjClean( Hop_Obj_t * pObj ) { memset( pObj, 0, sizeof(Hop_Obj_t) ); }
static inline int Hop_ObjWhatFanin( Hop_Obj_t * pObj, Hop_Obj_t * pFanin )
diff --git a/src/aig/hop/hopDfs.c b/src/aig/hop/hopDfs.c
index 3dd8793c..27fb1aa6 100644
--- a/src/aig/hop/hopDfs.c
+++ b/src/aig/hop/hopDfs.c
@@ -125,13 +125,13 @@ int Hop_ManCountLevels( Hop_Man_t * p )
{
Level0 = (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData;
Level1 = (int)(ABC_PTRUINT_T)Hop_ObjFanin1(pObj)->pData;
- pObj->pData = (void *)(ABC_PTRUINT_T)(1 + Hop_ObjIsExor(pObj) + AIG_MAX(Level0, Level1));
+ pObj->pData = (void *)(ABC_PTRUINT_T)(1 + Hop_ObjIsExor(pObj) + ABC_MAX(Level0, Level1));
}
Vec_PtrFree( vNodes );
// get levels of the POs
LevelsMax = 0;
Hop_ManForEachPo( p, pObj, i )
- LevelsMax = AIG_MAX( LevelsMax, (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData );
+ LevelsMax = ABC_MAX( LevelsMax, (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData );
return LevelsMax;
}
diff --git a/src/aig/hop/hopObj.c b/src/aig/hop/hopObj.c
index eccf58b8..f173248f 100644
--- a/src/aig/hop/hopObj.c
+++ b/src/aig/hop/hopObj.c
@@ -193,7 +193,7 @@ void Hop_ObjDelete( Hop_Man_t * p, Hop_Obj_t * pObj )
// remove PIs/POs from the arrays
if ( Hop_ObjIsPi(pObj) )
Vec_PtrRemove( p->vPis, pObj );
- // ABC_FREE the node
+ // free the node
Hop_ManRecycleMemory( p, pObj );
}
diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c
index c0bbec1c..ddb0bce6 100644
--- a/src/aig/int/intCtrex.c
+++ b/src/aig/int/intCtrex.c
@@ -138,7 +138,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
Aig_InfoSetBit( pCtrex->pData, Saig_ManRegNum(pAig) + i );
ABC_FREE( pModel );
}
- // ABC_FREE the sat_solver
+ // free the sat_solver
sat_solver_delete( pSat );
Vec_IntFree( vCiIds );
// verify counter-example
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index c0ec3021..68726501 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -1218,7 +1218,7 @@ void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p )
Ivy_ObjSetClassNodeRepr( pObj, NULL );
Ivy_FraigAddClass( &p->lClasses, pObj );
}
- // ABC_FREE the table
+ // free the table
ABC_FREE( pTable );
}
diff --git a/src/aig/ivy/ivyHaig.c b/src/aig/ivy/ivyHaig.c
index 62624642..87021600 100644
--- a/src/aig/ivy/ivyHaig.c
+++ b/src/aig/ivy/ivyHaig.c
@@ -518,7 +518,7 @@ printf( "Using latch %d with fanin %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id );
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
pObj->Init = pObj->Level, pObj->Level = 0;
}
- // ABC_FREE arrays
+ // free arrays
Vec_IntFree( vNodes );
Vec_IntFree( vLatches );
}
diff --git a/src/aig/ivy/ivyMan.c b/src/aig/ivy/ivyMan.c
index d09f6ffd..909548d1 100644
--- a/src/aig/ivy/ivyMan.c
+++ b/src/aig/ivy/ivyMan.c
@@ -143,7 +143,7 @@ Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
// update the counters of different objects
pNew->nObjs[IVY_PI] -= Ivy_ManLatchNum(p);
pNew->nObjs[IVY_LATCH] += Ivy_ManLatchNum(p);
- // ABC_FREE arrays
+ // free arrays
Vec_IntFree( vNodes );
Vec_IntFree( vLatches );
// make sure structural hashing did not change anything
@@ -346,7 +346,7 @@ int Ivy_ManCleanupSeq( Ivy_Man_t * p )
// delete buffer from the array of buffers
if ( p->fFanout && Ivy_ObjIsBuf(pObj) )
Vec_PtrRemove( p->vBufs, pObj );
- // ABC_FREE the node
+ // free the node
Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
Ivy_ManRecycleMemory( p, pObj );
}
diff --git a/src/aig/ivy/ivyObj.c b/src/aig/ivy/ivyObj.c
index d7925fab..59dda19c 100644
--- a/src/aig/ivy/ivyObj.c
+++ b/src/aig/ivy/ivyObj.c
@@ -268,7 +268,7 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
// clean and recycle the entry
if ( fFreeTop )
{
- // ABC_FREE the node
+ // free the node
Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
Ivy_ManRecycleMemory( p, pObj );
}
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index c4ed70e4..a85262a9 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -2422,7 +2422,7 @@ int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit
// compute the sum total of supports
nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+0], nVars );
nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+1], nVars );
- // ABC_FREE the networks
+ // free the networks
Kit_DsdNtkFree( ppNtks[nStep+1][2*i+0] );
Kit_DsdNtkFree( ppNtks[nStep+1][2*i+1] );
}
@@ -2460,7 +2460,7 @@ int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit
}
}
- // ABC_FREE the networks
+ // free the networks
for ( i = 0; i < 5; i++ )
for ( k = 0; k < 16; k++ )
if ( ppNtks[i][k] )
diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c
index c0d3b650..e0f6dd82 100644
--- a/src/aig/mfx/mfxCore.c
+++ b/src/aig/mfx/mfxCore.c
@@ -86,7 +86,7 @@ p->timeWin += clock() - clk;
// compute the divisors of the window
clk = clock();
p->vDivs = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) );
-// p->vDivs = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY );
+// p->vDivs = Mfx_ComputeDivisors( p, pNode, ABC_INFINITY );
p->nTotalDivs += Vec_PtrSize(p->vDivs);
p->timeDiv += clock() - clk;
// construct AIG for the window
@@ -371,7 +371,7 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
if ( pPars->fPower )
printf( "Total switching after = %7.2f.\n", Nwl_ManComputeTotalSwitching(pNtk) );
- // ABC_FREE the manager
+ // free the manager
p->timeTotal = clock() - clk;
Mfx_ManStop( p );
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 6923ac7a..b4abe3bf 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -185,7 +185,7 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
Ntl_ObjForEachFanin( pObj, pNetFanin, i )
{
LevelCur = Aig_ObjLevel( Aig_Regular(pNetFanin->pCopy) );
- LevelMax = AIG_MAX( LevelMax, LevelCur );
+ LevelMax = ABC_MAX( LevelMax, LevelCur );
Vec_PtrPush( p->vCos, pNetFanin );
Aig_ObjCreatePo( p->pAig, pNetFanin->pCopy );
}
diff --git a/src/aig/nwk/nwkFanio.c b/src/aig/nwk/nwkFanio.c
index 56a13741..daea19d5 100644
--- a/src/aig/nwk/nwkFanio.c
+++ b/src/aig/nwk/nwkFanio.c
@@ -172,7 +172,7 @@ void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
pObj->pFanio[i] = pObj->pFanio[i-1];
pObj->pFanio[pObj->nFanins++] = pFanin;
pFanin->pFanio[pFanin->nFanins + pFanin->nFanouts++] = pObj;
- pObj->Level = AIG_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) );
+ pObj->Level = ABC_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) );
}
/**Function*************************************************************
diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c
index d6e20672..8f971871 100644
--- a/src/aig/nwk/nwkMan.c
+++ b/src/aig/nwk/nwkMan.c
@@ -127,7 +127,7 @@ int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl )
int nPis; // the number of primary inputs
int nPos; // the number of primary outputs
} ParsNew, ParsBest = { 0 };
- // ABC_FREE storage for the name
+ // free storage for the name
if ( pNtk == NULL )
{
ABC_FREE( ParsBest.pName );
diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c
index 80391c66..5c53038c 100644
--- a/src/aig/nwk/nwkTiming.c
+++ b/src/aig/nwk/nwkTiming.c
@@ -736,7 +736,7 @@ int Nwk_ObjLevelNew( Nwk_Obj_t * pObj )
for ( i = 0; i < nTerms; i++ )
{
pFanin = Nwk_ManCo(pObj->pMan, iTerm1 + i);
- Level = AIG_MAX( Level, Nwk_ObjLevel(pFanin) );
+ Level = ABC_MAX( Level, Nwk_ObjLevel(pFanin) );
}
Level++;
}
@@ -745,7 +745,7 @@ int Nwk_ObjLevelNew( Nwk_Obj_t * pObj )
}
assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) );
Nwk_ObjForEachFanin( pObj, pFanin, i )
- Level = AIG_MAX( Level, Nwk_ObjLevel(pFanin) );
+ Level = ABC_MAX( Level, Nwk_ObjLevel(pFanin) );
return Level + (Nwk_ObjIsNode(pObj) && Nwk_ObjFaninNum(pObj) > 0);
}
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index fccac175..10b7b462 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -368,12 +368,12 @@ void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk )
nFanouts = Nwk_ObjFanoutNum(pNode);
nFaninsAll += nFanins;
nFanoutsAll += nFanouts;
- nFaninsMax = AIG_MAX( nFaninsMax, nFanins );
- nFanoutsMax = AIG_MAX( nFanoutsMax, nFanouts );
+ nFaninsMax = ABC_MAX( nFaninsMax, nFanins );
+ nFanoutsMax = ABC_MAX( nFanoutsMax, nFanouts );
}
// allocate storage for fanin/fanout numbers
- nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
+ nSizeMax = ABC_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );
diff --git a/src/aig/nwk2/nwkFanio.c b/src/aig/nwk2/nwkFanio.c
index 4068a1a5..30037a83 100644
--- a/src/aig/nwk2/nwkFanio.c
+++ b/src/aig/nwk2/nwkFanio.c
@@ -172,7 +172,7 @@ void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
pObj->pFanio[i] = pObj->pFanio[i-1];
pObj->pFanio[pObj->nFanins++] = pFanin;
pFanin->pFanio[pFanin->nFanins + pFanin->nFanouts++] = pObj;
- pObj->Level = AIG_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) );
+ pObj->Level = ABC_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) );
}
/**Function*************************************************************
diff --git a/src/aig/nwk2/nwkUtil.c b/src/aig/nwk2/nwkUtil.c
index d6daca4e..5473e628 100644
--- a/src/aig/nwk2/nwkUtil.c
+++ b/src/aig/nwk2/nwkUtil.c
@@ -368,12 +368,12 @@ void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk )
nFanouts = Nwk_ObjFanoutNum(pNode);
nFaninsAll += nFanins;
nFanoutsAll += nFanouts;
- nFaninsMax = AIG_MAX( nFaninsMax, nFanins );
- nFanoutsMax = AIG_MAX( nFanoutsMax, nFanouts );
+ nFaninsMax = ABC_MAX( nFaninsMax, nFanins );
+ nFanoutsMax = ABC_MAX( nFanoutsMax, nFanouts );
}
// allocate storage for fanin/fanout numbers
- nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
+ nSizeMax = ABC_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index f11345eb..5ddef829 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -90,7 +90,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) {
////////////////////////////////////////////////////////////////////////
/*=== sswAbs.c ==========================================================*/
-extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose );
+extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose );
/*=== saigBmc.c ==========================================================*/
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index c9e76626..a2a915f7 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -693,15 +693,15 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex
SeeAlso []
***********************************************************************/
-Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int fVerbose )
-{
+Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fVerbose )
+{
extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose );
Vec_Int_t * vFlopsNew, * vPiToReg;
Aig_Obj_t * pObj;
int i, Entry, iFlop;
- Saig_BmcPerform( pAbs, 2000, 2000, 5000, 1000000, fVerbose );
+ Saig_BmcPerform( pAbs, nFrames, 2000, nConfMaxOne, 1000000, fVerbose );
if ( pAbs->pSeqModel == NULL )
return NULL;
// Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
@@ -765,7 +765,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
SeeAlso []
***********************************************************************/
-Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose )
+Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose )
{
Aig_Man_t * pResult, * pTemp;
Cnf_Dat_t * pCnf;
@@ -779,11 +779,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
if ( fSkipProof )
{
- assert( 0 );
+// assert( 0 );
if ( fVerbose )
printf( "Performing counter-example-based refinement.\n" );
// vFlops = Vec_IntStartNatural( 100 );
// Vec_IntPush( vFlops, 0 );
+ vFlops = Vec_IntStartNatural( 1 );
}
else
{
@@ -858,7 +859,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
printf( "Refining abstraction...\n" );
for ( Iter = 0; ; Iter++ )
{
- pTemp = Saig_ManProofRefine( p, pResult, vFlops, fVerbose );
+ pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose );
if ( pTemp == NULL )
break;
Aig_ManStop( pResult );
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
index 71bdadf6..0a9f230b 100644
--- a/src/aig/saig/saigMiter.c
+++ b/src/aig/saig/saigMiter.c
@@ -327,7 +327,7 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames )
assert( Saig_ManRegNum(pBot) == Saig_ManRegNum(pTop) );
assert( Saig_ManRegNum(pBot) > 0 || Saig_ManRegNum(pTop) > 0 );
// start timeframes
- p = Aig_ManStart( nFrames * AIG_MAX(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) );
+ p = Aig_ManStart( nFrames * ABC_MAX(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) );
p->pName = Aig_UtilStrsav( "frames" );
// create variables for register outputs
pAig = pBot;
diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c
index 9bc6416b..a3fdaf93 100644
--- a/src/aig/saig/saigSimMv.c
+++ b/src/aig/saig/saigSimMv.c
@@ -180,7 +180,7 @@ static inline int Saig_MvCreateObj( Saig_MvMan_t * p, int iFan0, int iFan1 )
pNode->iFan1 = iFan1;
pNode->iNext = 0;
if ( iFan0 || iFan1 )
- p->pLevels[p->nObjs] = 1 + AIG_MAX( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) );
+ p->pLevels[p->nObjs] = 1 + ABC_MAX( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) );
else
p->pLevels[p->nObjs] = 0, p->nPis++;
return p->nObjs++;
diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c
index ff46634e..b29fcb9b 100644
--- a/src/aig/saig/saigSynch.c
+++ b/src/aig/saig/saigSynch.c
@@ -616,7 +616,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
return NULL;
}
clk = clock();
- vSimInfo = Vec_PtrAllocSimInfo( AIG_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 );
+ vSimInfo = Vec_PtrAllocSimInfo( ABC_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 );
// process Design 1
RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq1, 1 );
diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c
index f50af285..a92d9369 100644
--- a/src/aig/saig/saigTrans.c
+++ b/src/aig/saig/saigTrans.c
@@ -398,7 +398,7 @@ ABC_PRT( "Fraiging", clock() - clk );
clk = clock();
pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
ABC_PRT( "Mapped", clock() - clk );
- // ABC_FREE mapping
+ // free mapping
Saig_ManStopMap2( pAig );
clk = clock();
pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 967d29e9..8fce7904 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -597,7 +597,7 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr,
// int nWords = 4;
// int nIters = 0;
- int nFrames = AIG_MAX( nFramesK, 4 );
+ int nFrames = ABC_MAX( nFramesK, 4 );
int nWords = 2;
int nIters = 16;
Ssw_Cla_t * p;
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 9a31a056..56b37fbe 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -204,8 +204,8 @@ clk = clock();
nSatFailsReal = p->nSatFailsReal;
nUniques = p->nUniques;
- p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars );
- p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
+ p->nVarsMax = ABC_MAX( p->nVarsMax, p->pMSat->nSatVars );
+ p->nCallsMax = ABC_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
Ssw_SatStop( p->pMSat );
p->pMSat = NULL;
Ssw_ManCleanup( p );
diff --git a/src/aig/ssw/sswDyn.c b/src/aig/ssw/sswDyn.c
index d9ac07a9..04e66f09 100644
--- a/src/aig/ssw/sswDyn.c
+++ b/src/aig/ssw/sswDyn.c
@@ -438,8 +438,8 @@ p->timeReduce += clock() - clk;
// replace the solver
if ( p->pMSat )
{
- p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars );
- p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
+ p->nVarsMax = ABC_MAX( p->nVarsMax, p->pMSat->nSatVars );
+ p->nCallsMax = ABC_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
Ssw_SatStop( p->pMSat );
p->nRecycles++;
p->nRecyclesTotal++;
diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c
index 80bc5853..fb36c31d 100644
--- a/src/aig/ssw/sswLcorr.c
+++ b/src/aig/ssw/sswLcorr.c
@@ -300,8 +300,8 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
p->pMSat->nSatVars > p->pPars->nSatVarMax &&
p->nRecycleCalls > p->pPars->nRecycleCalls )
{
- p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars );
- p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
+ p->nVarsMax = ABC_MAX( p->nVarsMax, p->pMSat->nSatVars );
+ p->nCallsMax = ABC_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
Ssw_SatStop( p->pMSat );
p->pMSat = Ssw_SatStart( 0 );
p->nRecycles++;
diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c
index 5f426093..1d578291 100644
--- a/src/aig/ssw/sswSemi.c
+++ b/src/aig/ssw/sswSemi.c
@@ -68,7 +68,7 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
memset( p, 0, sizeof(Ssw_Sem_t) );
p->nConfMaxStart = nConfMax;
p->nConfMax = nConfMax;
- p->nFramesSweep = AIG_MAX( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
+ p->nFramesSweep = ABC_MAX( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
p->fVerbose = fVerbose;
// equivalences considered
p->pMan = pMan;
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index 7a2f4664..deb8d5d4 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -590,7 +590,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
Aig_ManForEachPi( p->pAig, pObj, i )
Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
// flip one bit
- Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
+ Limit = ABC_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
}
@@ -612,7 +612,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
// flip one bit of the last frame
if ( fUseDist1 ) //&& p->nFrames == 2 )
{
- Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
+ Limit = ABC_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
}
@@ -641,7 +641,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
// set distance one PIs for the first frame
- Limit = AIG_MIN( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 );
+ Limit = ABC_MIN( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 );
diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c
index 7327606e..e565b01f 100644
--- a/src/aig/tim/tim.c
+++ b/src/aig/tim/tim.c
@@ -28,10 +28,6 @@
#include "mem.h"
#include "tim.h"
-#define AIG_MIN(a,b) (((a) < (b))? (a) : (b))
-#define AIG_MAX(a,b) (((a) > (b))? (a) : (b))
-#define AIG_ABS(a) (((a) >= 0)? (a) :-(a))
-
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -773,7 +769,7 @@ float Tim_ManGetCiArrival( Tim_Man_t * p, int iCi )
pDelays = pBox->pDelayTable + i * pBox->nInputs;
DelayBest = -TIM_ETERNITY;
Tim_ManBoxForEachInput( p, pBox, pObj, k )
- DelayBest = AIG_MAX( DelayBest, pObj->timeArr + pDelays[k] );
+ DelayBest = ABC_MAX( DelayBest, pObj->timeArr + pDelays[k] );
pObjRes->timeArr = DelayBest;
pObjRes->TravId = p->nTravIds;
}
@@ -820,7 +816,7 @@ float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo )
Tim_ManBoxForEachOutput( p, pBox, pObj, k )
{
pDelays = pBox->pDelayTable + k * pBox->nInputs;
- DelayBest = AIG_MIN( DelayBest, pObj->timeReq - pDelays[i] );
+ DelayBest = ABC_MIN( DelayBest, pObj->timeReq - pDelays[i] );
}
pObjRes->timeReq = DelayBest;
pObjRes->TravId = p->nTravIds;
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 289c422d..a3188901 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -163,7 +163,7 @@ void Abc_AigFree( Abc_Aig_t * pMan )
{
assert( Vec_PtrSize( pMan->vStackReplaceOld ) == 0 );
assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 );
- // ABC_FREE the table
+ // free the table
if ( pMan->vAddedCells )
Vec_PtrFree( pMan->vAddedCells );
if ( pMan->vUpdatedNets )
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index aef44b11..d870a610 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -371,6 +371,116 @@ printf( "Converted %d one-hot registers.\n", Vec_IntSize(vNumbers) );
}
+/**Function*************************************************************
+
+ Synopsis [Converts registers with DC values into additional PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Ntk_t * pNtkNew;
+ Abc_Obj_t * pObj, * pFanin, * pObjNew, * pObjLiNew, * pObjLoNew;
+ int i, k, nFlops, nStates, iState, pfCompl[32];
+ assert( Abc_NtkIsLogic(pNtk) );
+ nFlops = Abc_NtkLatchNum(pNtk);
+ if ( nFlops == 0 )
+ return Abc_NtkDup( pNtk );
+ if ( nFlops > 16 )
+ {
+ printf( "Cannot reencode %d flops because it will lead to 2^%d states.\n", nFlops, nFlops );
+ return NULL;
+ }
+ // check if there are latches with DC values
+ iState = 0;
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ {
+ if ( Abc_LatchIsInitDc(pObj) )
+ {
+ printf( "Cannot process logic network with don't-care init values. Run \"zero\".\n" );
+ return NULL;
+ }
+ if ( Abc_LatchIsInit1(pObj) )
+ iState |= (1 << i);
+ }
+ // transfer logic to SOPs
+ Abc_NtkToSop( pNtk, 0 );
+ // create new network
+ pNtkNew = Abc_NtkStartFromNoLatches( pNtk, pNtk->ntkType, pNtk->ntkFunc );
+ nStates = (1 << nFlops);
+ for ( i = 0; i < nStates; i++ )
+ {
+ pObjNew = Abc_NtkCreateLatch( pNtkNew );
+ pObjLiNew = Abc_NtkCreateBi( pNtkNew );
+ pObjLoNew = Abc_NtkCreateBo( pNtkNew );
+ Abc_ObjAddFanin( pObjNew, pObjLiNew );
+ Abc_ObjAddFanin( pObjLoNew, pObjNew );
+ if ( i == iState )
+ Abc_LatchSetInit1( pObjNew );
+ else
+ Abc_LatchSetInit0( pObjNew );
+ }
+ Abc_NtkAddDummyBoxNames( pNtkNew );
+ assert( Abc_NtkLatchNum(pNtkNew) == nStates );
+ assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) );
+ assert( Abc_NtkPoNum(pNtkNew) == Abc_NtkPoNum(pNtk) );
+ assert( Abc_NtkCiNum(pNtkNew) == Abc_NtkPiNum(pNtkNew) + nStates );
+ assert( Abc_NtkCoNum(pNtkNew) == Abc_NtkPoNum(pNtkNew) + nStates );
+ assert( Abc_NtkCiNum(pNtk) == Abc_NtkPiNum(pNtk) + nFlops );
+ assert( Abc_NtkCoNum(pNtk) == Abc_NtkPoNum(pNtk) + nFlops );
+ // create hot-to-log transformers
+ for ( i = 0; i < nFlops; i++ )
+ {
+ pObjNew = Abc_NtkCreateNode( pNtkNew );
+ for ( k = 0; k < nStates; k++ )
+ if ( (k >> i) & 1 )
+ Abc_ObjAddFanin( pObjNew, Abc_NtkCi(pNtkNew, Abc_NtkPiNum(pNtkNew)+k) );
+ assert( Abc_ObjFaninNum(pObjNew) == nStates/2 );
+ pObjNew->pData = Abc_SopCreateOr( pNtkNew->pManFunc, nStates/2, NULL );
+ // save the new flop
+ pObj = Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i );
+ pObj->pCopy = pObjNew;
+ }
+ // duplicate the nodes
+ vNodes = Abc_NtkDfs( pNtk, 0 );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ pObj->pCopy = Abc_NtkDupObj( pNtkNew, pObj, 1 );
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+ }
+ Vec_PtrFree( vNodes );
+ // connect the POs
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ Abc_ObjAddFanin( pObj->pCopy, Abc_ObjNotCond(Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj)) );
+ // write entries into the nodes
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ pObj->pCopy = Abc_ObjNotCond(Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj));
+ // create log-to-hot transformers
+ for ( k = 0; k < nStates; k++ )
+ {
+ pObjNew = Abc_NtkCreateNode( pNtkNew );
+ for ( i = 0; i < nFlops; i++ )
+ {
+ pObj = Abc_NtkCo( pNtk, Abc_NtkPoNum(pNtk) + i );
+ Abc_ObjAddFanin( pObjNew, Abc_ObjRegular(pObj->pCopy) );
+ pfCompl[i] = Abc_ObjIsComplement(pObj->pCopy) ^ !((k >> i) & 1);
+ }
+ pObjNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, nFlops, pfCompl );
+ // connect it to the flop input
+ Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, Abc_NtkPoNum(pNtkNew)+k), pObjNew );
+ }
+ if ( !Abc_NtkCheck( pNtkNew ) )
+ fprintf( stdout, "Abc_NtkConvertOnehot(): Network check has failed.\n" );
+ return pNtkNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 639319d1..d6ab7ea1 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -935,10 +935,10 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
// int LargePiece = (4 << ABC_NUM_STEPS);
if ( pNtk == NULL )
return;
- // ABC_FREE the HAIG
+ // free the HAIG
// if ( pNtk->pHaig )
// Abc_NtkHaigStop( pNtk );
- // ABC_FREE EXDC Ntk
+ // free EXDC Ntk
if ( pNtk->pExdc )
Abc_NtkDelete( pNtk->pExdc );
if ( pNtk->pExcare )
@@ -952,7 +952,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
// make sure all the marks are clean
Abc_NtkForEachObj( pNtk, pObj, i )
{
- // ABC_FREE large fanout arrays
+ // free large fanout arrays
// if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece )
// ABC_FREE( pObj->vFanouts.pArray );
// these flags should be always zero
@@ -961,7 +961,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
assert( pObj->fMarkB == 0 );
assert( pObj->fMarkC == 0 );
}
- // ABC_FREE the nodes
+ // free the nodes
if ( pNtk->pMmStep == NULL )
{
Abc_NtkForEachObj( pNtk, pObj, i )
@@ -976,7 +976,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
ABC_FREE( pObj );
}
- // ABC_FREE the arrays
+ // free the arrays
Vec_PtrFree( pNtk->vPios );
Vec_PtrFree( pNtk->vPis );
Vec_PtrFree( pNtk->vPos );
@@ -992,14 +992,14 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
TotalMemory += pNtk->pMmObj? Extra_MmFixedReadMemUsage(pNtk->pMmObj) : 0;
TotalMemory += pNtk->pMmStep? Extra_MmStepReadMemUsage(pNtk->pMmStep) : 0;
// fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) );
- // ABC_FREE the storage
+ // free the storage
if ( pNtk->pMmObj )
Extra_MmFixedStop( pNtk->pMmObj );
if ( pNtk->pMmStep )
Extra_MmStepStop ( pNtk->pMmStep );
// name manager
Nm_ManFree( pNtk->pManName );
- // ABC_FREE the timing manager
+ // free the timing manager
if ( pNtk->pManTime )
Abc_ManTimeStop( pNtk->pManTime );
// start the functionality manager
@@ -1015,7 +1015,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
pNtk->pManFunc = NULL;
else if ( !Abc_NtkHasBlackbox(pNtk) )
assert( 0 );
- // ABC_FREE the hierarchy
+ // free the hierarchy
if ( pNtk->pDesign )
{
Abc_LibFree( pNtk->pDesign, pNtk );
@@ -1023,7 +1023,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
}
// if ( pNtk->pBlackBoxes )
// Vec_IntFree( pNtk->pBlackBoxes );
- // ABC_FREE node attributes
+ // free node attributes
Vec_PtrForEachEntry( pNtk->vAttrs, pAttrMan, i )
if ( pAttrMan )
{
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 4b18aa36..e4484ec5 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -71,9 +71,9 @@ void Abc_ObjRecycle( Abc_Obj_t * pObj )
{
Abc_Ntk_t * pNtk = pObj->pNtk;
// int LargePiece = (4 << ABC_NUM_STEPS);
- // ABC_FREE large fanout arrays
+ // free large fanout arrays
// if ( pNtk->pMmStep && pObj->vFanouts.nCap * 4 > LargePiece )
-// ABC_FREE( pObj->vFanouts.pArray );
+// free( pObj->vFanouts.pArray );
if ( pNtk->pMmStep == NULL )
{
ABC_FREE( pObj->vFanouts.pArray );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index cdb9b465..8ebb00a3 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1770,7 +1770,7 @@ void Abc_NtkCompareCones( Abc_Ntk_t * pNtk )
printf( "%4d CO %5d : Supp = %5d. Lev = %3d. Cone = %5d. Rev = %5d. COs = %3d (%3d).\n",
Iter, pPerms[i], Vec_PtrSize(vSupp), Abc_ObjLevel(Abc_ObjFanin0(pObj)), Vec_PtrSize(vNodes), Counter, CounterCos, CounterCosNew );
- // ABC_FREE arrays
+ // free arrays
Vec_PtrFree( vSupp );
Vec_PtrFree( vNodes );
Vec_PtrFree( vReverse );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ef7969be..c48b7e95 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27,7 +27,7 @@
#include "if.h"
#include "res.h"
#include "lpk.h"
-#include "aig.h"
+#include "giaAig.h"
#include "dar.h"
#include "mfs.h"
#include "mfx.h"
@@ -39,7 +39,6 @@
#include "ssw.h"
#include "cgt.h"
#include "amap.h"
-#include "gia.h"
#include "cec.h"
////////////////////////////////////////////////////////////////////////
@@ -194,6 +193,7 @@ static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandZero ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUndc ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOneHot ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -513,6 +513,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "zero", Abc_CommandZero, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "undc", Abc_CommandUndc, 1 );
+ Cmd_CommandAdd( pAbc, "Sequential", "onehot", Abc_CommandOneHot, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "dretime", Abc_CommandDRetime, 1 );
@@ -598,7 +599,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "AIG", "&psig", Abc_CommandAbc9PSig, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&status", Abc_CommandAbc9Status, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&show", Abc_CommandAbc9Show, 0 );
- Cmd_CommandAdd( pAbc, "AIG", "&hash", Abc_CommandAbc9Hash, 0 );
+ Cmd_CommandAdd( pAbc, "AIG", "&st", Abc_CommandAbc9Hash, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&topand", Abc_CommandAbc9Topand, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&cof", Abc_CommandAbc9Cof, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&trim", Abc_CommandAbc9Trim, 0 );
@@ -11945,7 +11946,7 @@ usage:
fprintf( pErr, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->fEpsilon );
fprintf( pErr, "\t-m : toggles using MUX matching [default = %s]\n", pPars->fUseMuxes? "yes": "no" );
fprintf( pErr, "\t-x : toggles using XOR matching [default = %s]\n", pPars->fUseXors? "yes": "no" );
- fprintf( pErr, "\t-i : toggles assuming inverters are ABC_FREE [default = %s]\n", pPars->fFreeInvs? "yes": "no" );
+ fprintf( pErr, "\t-i : toggles assuming inverters are free [default = %s]\n", pPars->fFreeInvs? "yes": "no" );
fprintf( pErr, "\t-s : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
@@ -13094,7 +13095,74 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: undc [-h]\n" );
- fprintf( pErr, "\t converts latches with DC init values into ABC_FREE PIs\n" );
+ fprintf( pErr, "\t converts latches with DC init values into free PIs\n" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandOneHot( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c;
+ extern Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkIsComb(pNtk) )
+ {
+ fprintf( pErr, "The current network is combinational.\n" );
+ return 0;
+ }
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ fprintf( pErr, "This command works only for logic networks.\n" );
+ return 0;
+ }
+ // get the new network
+ pNtkRes = Abc_NtkConvertOnehot( pNtk );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Converting to one-hot encoding has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: onehot [-h]\n" );
+ fprintf( pErr, "\t converts natural encoding into one-hot encoding\n" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@@ -15030,7 +15098,7 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- fNew = 1;
+ fNew = 0;
fComb = 0;
nFrames = 32;
nWords = 8;
@@ -18381,22 +18449,28 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
int nConfMax;
int fDynamic;
int fExtend;
+ int fSkipProof;
+ int nFramesBmc;
+ int nConfMaxBmc;
int fVerbose;
int c;
- extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nFramesMax = 10;
- nConfMax = 10000;
- fDynamic = 1;
- fExtend = 0;
- fVerbose = 0;
+ nFramesMax = 10;
+ nConfMax = 10000;
+ fDynamic = 1;
+ fExtend = 0;
+ fSkipProof = 0;
+ nFramesBmc = 2000;
+ nConfMaxBmc = 5000;
+ fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FCdevh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDdesvh" ) ) != EOF )
{
switch ( c )
{
@@ -18422,12 +18496,37 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConfMax < 0 )
goto usage;
break;
+ case 'G':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFramesBmc = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFramesBmc < 0 )
+ goto usage;
+ break;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfMaxBmc = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfMaxBmc < 0 )
+ goto usage;
+ break;
case 'd':
fDynamic ^= 1;
break;
case 'e':
fExtend ^= 1;
break;
+ case 's':
+ fSkipProof ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -18454,7 +18553,7 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
- pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose );
+ pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose );
if ( pNtkRes == NULL )
{
if ( pNtk->pSeqModel == NULL )
@@ -18465,12 +18564,16 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
- fprintf( pErr, "usage: abs [-FC num] [-devh]\n" );
- fprintf( pErr, "\t proof-based abstraction from UNSAT core of the BMC instance\n" );
- fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
- fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
+ fprintf( pErr, "usage: abs [-FCGD num] [-desvh]\n" );
+ fprintf( pErr, "\t proof-based abstraction (PBA) using UNSAT core of BMC\n" );
+ fprintf( pErr, "\t followed by counter-example-based abstraction\n" );
+ fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax );
+ fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", nConfMax );
+ fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", nFramesBmc );
+ fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", nConfMaxBmc );
fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" );
fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" );
+ fprintf( pErr, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -22128,11 +22231,15 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
int c;
+ int fAddStrash = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
{
switch ( c )
{
+ case 'a':
+ fAddStrash ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -22144,13 +22251,14 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" );
return 1;
}
- pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig );
+ pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig, fAddStrash );
Gia_ManStop( pTemp );
return 0;
usage:
- fprintf( stdout, "usage: &hash [-h]\n" );
+ fprintf( stdout, "usage: &st [-ah]\n" );
fprintf( stdout, "\t performs structural hashing\n" );
+ fprintf( stdout, "\t-a : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
@@ -22186,7 +22294,7 @@ int Abc_CommandAbc9Topand( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pAig == NULL )
{
- printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" );
+ printf( "Abc_CommandAbc9Topand(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pAig) > 0 )
diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c
index d2c5a12c..1512c76f 100644
--- a/src/base/abci/abcBmc.c
+++ b/src/base/abci/abcBmc.c
@@ -64,7 +64,7 @@ printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) );
// report the classes
// if ( fVerbose )
// Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames );
- // ABC_FREE stuff
+ // free stuff
Vec_PtrFree( vMapping );
Ivy_ManStop( pFraig );
Ivy_ManStop( pFrames );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 91046340..840068d6 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -19,7 +19,7 @@
***********************************************************************/
#include "abc.h"
-#include "aig.h"
+#include "giaAig.h"
#include "saig.h"
#include "dar.h"
#include "cnf.h"
@@ -2299,7 +2299,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pCex;
RetValue = 1;
- }
+ }
else
{
RetValue = 0;
@@ -2375,7 +2375,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
pGia = Gia_ManFromAig( pMan );
if ( Gia_ManSimSimulate( pGia, pPars ) )
{
- if ( (pCex = pMan->pSeqModel) )
+ if ( (pCex = (Fra_Cex_t *)pGia->pCexSeq) )
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
@@ -2404,8 +2404,13 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
pCex = Fra_SmlGetCounterExample( pSml );
if ( pCex )
+ {
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
+ status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ if ( status == 0 )
+ printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+ }
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pCex;
@@ -2557,7 +2562,7 @@ ABC_PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
@@ -2567,7 +2572,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
return NULL;
Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, 0, fVerbose );
+ pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose );
if ( pTemp->pSeqModel )
{
ABC_FREE( pNtk->pModel );
@@ -3380,7 +3385,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
return NULL;
/*
Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, 1 );
+ pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 1 );
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index 1596e774..6109870e 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -177,12 +177,12 @@ void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
void Abc_NtkFxuFreeInfo( Fxu_Data_t * p )
{
int i;
- // ABC_FREE the arrays of new fanins
+ // free the arrays of new fanins
if ( p->vFaninsNew )
for ( i = 0; i < p->vFaninsNew->nSize; i++ )
if ( p->vFaninsNew->pArray[i] )
Vec_IntFree( p->vFaninsNew->pArray[i] );
- // ABC_FREE the arrays
+ // free the arrays
if ( p->vSops ) Vec_PtrFree( p->vSops );
if ( p->vSopsNew ) Vec_PtrFree( p->vSopsNew );
if ( p->vFanins ) Vec_PtrFree( p->vFanins );
diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c
index 569275f2..3f3fefcd 100644
--- a/src/base/abci/abcHaig.c
+++ b/src/base/abci/abcHaig.c
@@ -691,7 +691,7 @@ Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan );
Hop_ManStop( pMan );
- // ABC_FREE HAIG
+ // free HAIG
return pNtkAig;
}
diff --git a/src/base/abci/abcMv.c b/src/base/abci/abcMv.c
index dacd16b2..8ea3697f 100644
--- a/src/base/abci/abcMv.c
+++ b/src/base/abci/abcMv.c
@@ -349,7 +349,7 @@ void Abc_MvDecompose( Mv_Man_t * p )
printf( "%d ", Vec_PtrSize(vCofs) );
Vec_PtrFree( vCofs );
- // ABC_FREE the cofactors
+ // free the cofactors
for ( v1 = 0; v1 < 4; v1++ )
for ( v2 = 0; v2 < 4; v2++ )
Cudd_RecursiveDeref( p->dd, bCofs[v1 * 4 + v2] );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index e65ce11a..d47dfe1f 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -64,7 +64,7 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
int nPis; // the number of primary inputs
int nPos; // the number of primary outputs
} ParsNew, ParsBest = { 0 };
- // ABC_FREE storage for the name
+ // free storage for the name
if ( pNtk == NULL )
{
ABC_FREE( ParsBest.pName );
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
index 3834c00d..e25be81a 100644
--- a/src/base/abci/abcReach.c
+++ b/src/base/abci/abcReach.c
@@ -102,7 +102,7 @@ DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorde
bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
pbParts[i] = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) ); Cudd_Ref( pbParts[i] );
}
- // ABC_FREE the global BDDs
+ // free the global BDDs
Abc_NtkFreeGlobalBdds( pNtk, 0 );
// reorder and disable reordering
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 3cee19ca..5e14116c 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -117,7 +117,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsL
pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
Vec_IntFree( vCiIds );
}
- // ABC_FREE the sat_solver
+ // free the sat_solver
if ( fVerbose )
Sat_SolverPrintStats( stdout, pSat );
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index d1f4d4f7..dfb8137c 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -111,7 +111,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose,
Abc_NtkFraigTransform( pNtk, tEquiv, fUseInv, fVerbose );
stmm_free_table( tEquiv );
- // ABC_FREE the manager
+ // free the manager
Fraig_ManFree( pMan );
Abc_NtkDelete( pNtkAig );
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index 196ff643..251d3953 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -143,7 +143,7 @@ DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bProd );
}
- // ABC_FREE the global BDDs
+ // free the global BDDs
// Abc_NtkFreeGlobalBdds( pNtk );
Abc_NtkFreeGlobalBdds( pNtk, 0 );
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 60197d29..424c26ec 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -799,7 +799,7 @@ void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo )
for ( k = 0; k <= iFrame; k++ )
if ( Abc_NtkPi(pFrames, k*Abc_NtkPiNum(pNtk) + i)->pCopy )
pObj->pCopy = (void *)1;
- // ABC_FREE stuff
+ // free stuff
Vec_PtrFree( vSupp );
Abc_NtkDelete( pFrames );
}
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 20f412e0..46d61583 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1140,7 +1140,7 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
printf( "The library contains %d gates.\n", st_count(pLibrary->tModules) );
- // ABC_FREE old library
+ // free old library
if ( Abc_FrameReadLibVer() )
Abc_LibFree( Abc_FrameReadLibVer(), NULL );
// read new library
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index c26e4cd5..85475204 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -327,7 +327,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
i++;
}
else // modified AIGER
- {
+ {
vLits = Io_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
}
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 34ea4294..eea601a8 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -160,7 +160,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
pDesignName = Extra_FileNameGeneric( pFileName );
p->pDesign = Abc_LibCreate( pDesignName );
ABC_FREE( pDesignName );
- // ABC_FREE the HOP manager
+ // free the HOP manager
Hop_ManStop( p->pDesign->pManFunc );
p->pDesign->pManFunc = NULL;
// prepare the file for parsing
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 7d03e545..3df189d1 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -78,7 +78,7 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes )
s_pNtk = pNtk;
Sat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 );
s_pNtk = NULL;
- // ABC_FREE the solver
+ // free the solver
sat_solver_delete( pSat );
return 1;
}
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index c318545b..42d6349a 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -274,7 +274,7 @@ void Ver_ParsePrintErrorMessage( Ver_Man_t * p )
else // print the error message with the line number
fprintf( p->Output, "%s (line %d): %s\n",
p->pFileName, Ver_StreamGetLineNumber(p->pReader), p->sError );
- // ABC_FREE the data
+ // free the data
Ver_ParseFreeData( p );
}
@@ -2104,7 +2104,7 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
i--;
}
- // ABC_FREE the bundling
+ // free the bundling
Vec_PtrForEachEntry( vBundles, pBundle, k )
Ver_ParseFreeBundle( pBundle );
Vec_PtrFree( vBundles );
@@ -2227,7 +2227,7 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
i--;
}
- // ABC_FREE the bundling
+ // free the bundling
Vec_PtrForEachEntry( vBundles, pBundle, k )
Ver_ParseFreeBundle( pBundle );
Vec_PtrFree( vBundles );
@@ -2626,7 +2626,7 @@ int Ver_ParseDriveInputs( Ver_Man_t * pMan, Vec_Ptr_t * vUndefs )
Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
}
- // ABC_FREE the bundles
+ // free the bundles
Vec_PtrFree( (Vec_Ptr_t *)pBox->pCopy );
pBox->pCopy = NULL;
}
diff --git a/src/map/amap/amapGraph.c b/src/map/amap/amapGraph.c
index 83cadc2c..0e9fd85c 100644
--- a/src/map/amap/amapGraph.c
+++ b/src/map/amap/amapGraph.c
@@ -139,7 +139,7 @@ Amap_Obj_t * Amap_ManCreateAnd( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t *
pObj->Fan[1] = Amap_ObjToLit(pFan1); Amap_Regular(pFan1)->nRefs++;
assert( Amap_Lit2Var(pObj->Fan[0]) != Amap_Lit2Var(pObj->Fan[1]) );
pObj->fPhase = Amap_ObjPhaseReal(pFan0) & Amap_ObjPhaseReal(pFan1);
- pObj->Level = 1 + AIG_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
+ pObj->Level = 1 + ABC_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
if ( p->nLevelMax < (int)pObj->Level )
p->nLevelMax = (int)pObj->Level;
p->nObjs[AMAP_OBJ_AND]++;
@@ -165,7 +165,7 @@ Amap_Obj_t * Amap_ManCreateXor( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t *
pObj->Fan[0] = Amap_ObjToLit(pFan0); Amap_Regular(pFan0)->nRefs++;
pObj->Fan[1] = Amap_ObjToLit(pFan1); Amap_Regular(pFan1)->nRefs++;
pObj->fPhase = Amap_ObjPhaseReal(pFan0) ^ Amap_ObjPhaseReal(pFan1);
- pObj->Level = 2 + AIG_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
+ pObj->Level = 2 + ABC_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
if ( p->nLevelMax < (int)pObj->Level )
p->nLevelMax = (int)pObj->Level;
p->nObjs[AMAP_OBJ_XOR]++;
@@ -193,8 +193,8 @@ Amap_Obj_t * Amap_ManCreateMux( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t *
pObj->Fan[2] = Amap_ObjToLit(pFanC); Amap_Regular(pFanC)->nRefs++;
pObj->fPhase = (Amap_ObjPhaseReal(pFan1) & Amap_ObjPhaseReal(pFanC)) |
(Amap_ObjPhaseReal(pFan0) & ~Amap_ObjPhaseReal(pFanC));
- pObj->Level = AIG_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
- pObj->Level = 2 + AIG_MAX( pObj->Level, Amap_Regular(pFanC)->Level );
+ pObj->Level = ABC_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
+ pObj->Level = 2 + ABC_MAX( pObj->Level, Amap_Regular(pFanC)->Level );
if ( p->nLevelMax < (int)pObj->Level )
p->nLevelMax = (int)pObj->Level;
p->nObjs[AMAP_OBJ_MUX]++;
@@ -221,7 +221,7 @@ void Amap_ManCreateChoice( Amap_Man_t * p, Amap_Obj_t * pObj )
// update the level of this node (needed for correct required time computation)
for ( pTemp = pObj; pTemp; pTemp = Amap_ObjChoice(p, pTemp) )
{
- pObj->Level = AIG_MAX( pObj->Level, pTemp->Level );
+ pObj->Level = ABC_MAX( pObj->Level, pTemp->Level );
// pTemp->nVisits++; pTemp->nVisitsCopy++;
}
// mark the largest level
diff --git a/src/map/amap/amapMatch.c b/src/map/amap/amapMatch.c
index 0ea65219..a997ad48 100644
--- a/src/map/amap/amapMatch.c
+++ b/src/map/amap/amapMatch.c
@@ -102,7 +102,7 @@ float Amap_ManMaxDelay( Amap_Man_t * p )
float Delay = 0.0;
int i;
Amap_ManForEachPo( p, pObj, i )
- Delay = AIG_MAX( Delay, Amap_ObjFanin0(p,pObj)->Best.Delay );
+ Delay = ABC_MAX( Delay, Amap_ObjFanin0(p,pObj)->Best.Delay );
return Delay;
}
@@ -373,7 +373,7 @@ static inline void Amap_ManMatchGetFlows( Amap_Man_t * p, Amap_Mat_t * pM )
Amap_MatchForEachFanin( p, pM, pFanin, i )
{
pMFanin = &pFanin->Best;
- pM->Delay = AIG_MAX( pM->Delay, pMFanin->Delay );
+ pM->Delay = ABC_MAX( pM->Delay, pMFanin->Delay );
pM->AveFan += Amap_ObjRefsTotal(pFanin);
if ( Amap_ObjRefsTotal(pFanin) == 0 )
pM->Area += pMFanin->Area;
@@ -409,7 +409,7 @@ static inline void Amap_ManMatchGetExacts( Amap_Man_t * p, Amap_Obj_t * pNode, A
Amap_MatchForEachFanin( p, pM, pFanin, i )
{
pMFanin = &pFanin->Best;
- pM->Delay = AIG_MAX( pM->Delay, pMFanin->Delay );
+ pM->Delay = ABC_MAX( pM->Delay, pMFanin->Delay );
pM->AveFan += Amap_ObjRefsTotal(pFanin);
}
pM->AveFan /= pGate->nPins;
diff --git a/src/map/fpga/fpgaCut.c b/src/map/fpga/fpgaCut.c
index a9108871..aca4a8ef 100644
--- a/src/map/fpga/fpgaCut.c
+++ b/src/map/fpga/fpgaCut.c
@@ -1115,7 +1115,7 @@ Fpga_Cut_t * Fpga_CutSortCuts( Fpga_Man_t * pMan, Fpga_CutTable_t * p, Fpga_Cut_
if ( nCuts > FPGA_CUTS_MAX_USE - 1 )
{
// printf( "*" );
- // ABC_FREE the remaining cuts
+ // free the remaining cuts
for ( i = FPGA_CUTS_MAX_USE - 1; i < nCuts; i++ )
Extra_MmFixedEntryRecycle( pMan->mmCuts, (char *)p->pCuts1[i] );
// update the number of cuts
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 97f2a06a..6294e3d2 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -138,7 +138,7 @@ void If_ManStop( If_Man_t * p )
ABC_FREE( p->pMemCi );
ABC_FREE( p->pMemAnd );
ABC_FREE( p->puTemp[0] );
- // ABC_FREE pars memory
+ // free pars memory
if ( p->pPars->pTimesArr )
ABC_FREE( p->pPars->pTimesArr );
if ( p->pPars->pTimesReq )
diff --git a/src/map/mapper/mapperCut.c b/src/map/mapper/mapperCut.c
index 00ec9fe5..19878d5b 100644
--- a/src/map/mapper/mapperCut.c
+++ b/src/map/mapper/mapperCut.c
@@ -1005,7 +1005,7 @@ Map_Cut_t * Map_CutSortCuts( Map_Man_t * pMan, Map_CutTable_t * p, Map_Cut_t * p
// move them back into the list
if ( nCuts > MAP_CUTS_MAX_USE - 1 )
{
- // ABC_FREE the remaining cuts
+ // free the remaining cuts
for ( i = MAP_CUTS_MAX_USE - 1; i < nCuts; i++ )
Extra_MmFixedEntryRecycle( pMan->mmCuts, (char *)p->pCuts1[i] );
// update the number of cuts
diff --git a/src/map/mio/mioFunc.c b/src/map/mio/mioFunc.c
index a06151f0..05fe245d 100644
--- a/src/map/mio/mioFunc.c
+++ b/src/map/mio/mioFunc.c
@@ -173,7 +173,7 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
{
if ( pPinNames[i] && strcmp( pPinNames[i], pPin->pName ) == 0 )
{
- // ABC_FREE pPinNames[i] because it is already available as pPin->pName
+ // free pPinNames[i] because it is already available as pPin->pName
// setting pPinNames[i] to NULL is useful to make sure that
// this name is not assigned to two pins in the list
ABC_FREE( pPinNames[i] );
diff --git a/src/map/mio/mioUtils.c b/src/map/mio/mioUtils.c
index 3f42d2bb..376a0bed 100644
--- a/src/map/mio/mioUtils.c
+++ b/src/map/mio/mioUtils.c
@@ -47,9 +47,9 @@ void Mio_LibraryDelete( Mio_Library_t * pLib )
Mio_Gate_t * pGate, * pGate2;
if ( pLib == NULL )
return;
- // ABC_FREE the bindings of nodes to gates from this library for all networks
+ // free the bindings of nodes to gates from this library for all networks
Abc_FrameUnmapAllNetworks( Abc_FrameGetGlobalFrame() );
- // ABC_FREE the library
+ // free the library
ABC_FREE( pLib->pName );
Mio_LibraryForEachGateSafe( pLib, pGate, pGate2 )
Mio_GateDelete( pGate );
diff --git a/src/misc/hash/hashFlt.h b/src/misc/hash/hashFlt.h
index 43b9dd7f..4b9951cb 100644
--- a/src/misc/hash/hashFlt.h
+++ b/src/misc/hash/hashFlt.h
@@ -309,7 +309,7 @@ static inline void Hash_FltFree( Hash_Flt_t *p ) {
int bin;
Hash_Flt_Entry_t *pEntry;
- // ABC_FREE bins
+ // free bins
for(bin = 0; bin < p->nBins; bin++) {
pEntry = p->pArray[bin];
while(pEntry) {
@@ -318,7 +318,7 @@ static inline void Hash_FltFree( Hash_Flt_t *p ) {
}
}
- // ABC_FREE hash
+ // free hash
ABC_FREE( p->pArray );
ABC_FREE( p );
}
diff --git a/src/misc/hash/hashInt.h b/src/misc/hash/hashInt.h
index 7993e562..f58a9fac 100644
--- a/src/misc/hash/hashInt.h
+++ b/src/misc/hash/hashInt.h
@@ -272,7 +272,7 @@ static inline void Hash_IntFree( Hash_Int_t *p ) {
int bin;
Hash_Int_Entry_t *pEntry, *pTemp;
- // ABC_FREE bins
+ // free bins
for(bin = 0; bin < p->nBins; bin++) {
pEntry = p->pArray[bin];
while(pEntry) {
@@ -282,7 +282,7 @@ static inline void Hash_IntFree( Hash_Int_t *p ) {
}
}
- // ABC_FREE hash
+ // free hash
ABC_FREE( p->pArray );
ABC_FREE( p );
}
diff --git a/src/misc/hash/hashPtr.h b/src/misc/hash/hashPtr.h
index 224e5c84..136250ee 100644
--- a/src/misc/hash/hashPtr.h
+++ b/src/misc/hash/hashPtr.h
@@ -310,7 +310,7 @@ static inline void Hash_PtrFree( Hash_Ptr_t *p ) {
int bin;
Hash_Ptr_Entry_t *pEntry;
- // ABC_FREE bins
+ // free bins
for(bin = 0; bin < p->nBins; bin++) {
pEntry = p->pArray[bin];
while(pEntry) {
@@ -319,7 +319,7 @@ static inline void Hash_PtrFree( Hash_Ptr_t *p ) {
}
}
- // ABC_FREE hash
+ // free hash
ABC_FREE( p->pArray );
ABC_FREE( p );
}
diff --git a/src/misc/vec/vecAtt.h b/src/misc/vec/vecAtt.h
index 9129321c..983b7c1c 100644
--- a/src/misc/vec/vecAtt.h
+++ b/src/misc/vec/vecAtt.h
@@ -124,7 +124,7 @@ static inline void * Vec_AttFree( Vec_Att_t * p, int fFreeMan )
void * pMan;
if ( p == NULL )
return NULL;
- // ABC_FREE the attributes of objects
+ // free the attributes of objects
if ( p->pFuncFreeObj )
{
int i;
@@ -132,7 +132,7 @@ static inline void * Vec_AttFree( Vec_Att_t * p, int fFreeMan )
if ( p->pArrayPtr[i] )
p->pFuncFreeObj( p->pMan, p->pArrayPtr[i] );
}
- // ABC_FREE the memory manager
+ // free the memory manager
pMan = fFreeMan? NULL : p->pMan;
if ( p->pMan && fFreeMan )
p->pFuncFreeMan( p->pMan );
@@ -154,7 +154,7 @@ static inline void * Vec_AttFree( Vec_Att_t * p, int fFreeMan )
***********************************************************************/
static inline void Vec_AttClear( Vec_Att_t * p )
{
- // ABC_FREE the attributes of objects
+ // free the attributes of objects
if ( p->pFuncFreeObj )
{
int i;
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 6fc5109b..3f958b6f 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -785,7 +785,7 @@ static inline void Vec_PtrDoubleSimInfo( Vec_Ptr_t * vInfo )
vInfo->pArray = vInfoNew->pArray;
vInfo->nSize *= 2;
vInfo->nCap *= 2;
- // ABC_FREE the old array
+ // free the old array
vInfoNew->pArray = NULL;
ABC_FREE( vInfoNew );
}
@@ -815,7 +815,7 @@ static inline void Vec_PtrReallocSimInfo( Vec_Ptr_t * vInfo )
// replace the array
ABC_FREE( vInfo->pArray );
vInfo->pArray = vInfoNew->pArray;
- // ABC_FREE the old array
+ // free the old array
vInfoNew->pArray = NULL;
ABC_FREE( vInfoNew );
}
diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c
index c2a46d3e..a1cd9def 100644
--- a/src/opt/lpk/lpkAbcDsd.c
+++ b/src/opt/lpk/lpkAbcDsd.c
@@ -420,7 +420,7 @@ Kit_DsdPrint( stdout, pNtks[i] );
pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1], p->nLutK - nCofDepth );
// compare bound-sets
Lpk_FunCompareBoundSets( p, pvBSets[0][0], nCofDepth, uNonDecSupp, uLateArrSupp, pRes );
- // ABC_FREE the bound sets
+ // free the bound sets
for ( i = nCofDepth; i >= 0; i-- )
for ( k = 0; k < (1<<i); k++ )
Vec_IntFree( pvBSets[i][k] );
@@ -539,7 +539,7 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p, int nShared )
}
finish:
- // ABC_FREE the networks
+ // free the networks
for ( i = 0; i < (1<<nShared); i++ )
if ( pNtks[i] )
Kit_DsdNtkFree( pNtks[i] );
diff --git a/src/opt/lpk/lpkMulti.c b/src/opt/lpk/lpkMulti.c
index b013570e..d5f1fd11 100644
--- a/src/opt/lpk/lpkMulti.c
+++ b/src/opt/lpk/lpkMulti.c
@@ -492,7 +492,7 @@ If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj
printf( "Verification failed.\n" );
- // ABC_FREE the networks
+ // free the networks
for ( i = 0; i < 8; i++ )
if ( ppNtks[i] )
Kit_DsdNtkFree( ppNtks[i] );
diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c
index 6cb3f12d..90e46863 100644
--- a/src/opt/lpk/lpkSets.c
+++ b/src/opt/lpk/lpkSets.c
@@ -362,7 +362,7 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
Lpk_PrintSets( vSets0 );
if ( fVerbose )
Lpk_PrintSets( vSets1 );
- // ABC_FREE the networks
+ // free the networks
Kit_DsdNtkFree( ppNtks[0] );
Kit_DsdNtkFree( ppNtks[1] );
// evaluate the pair
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 456b5d71..20d3799c 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -567,7 +567,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
#endif
}
- // ABC_FREE the manager
+ // free the manager
p->timeTotal = clock() - clk;
Mfs_ManStop( p );
return 1;
diff --git a/src/opt/ret/retIncrem.c b/src/opt/ret/retIncrem.c
index 233fb436..1866e4c9 100644
--- a/src/opt/ret/retIncrem.c
+++ b/src/opt/ret/retIncrem.c
@@ -194,7 +194,7 @@ int Abc_NtkRetimeFinalizeLatches( Abc_Ntk_t * pNtk, st_table * tLatches, int nId
Vec_PtrPush( vCosNew, pLatchIn );
Vec_PtrPush( vBoxesNew, pLatch );
}
- // ABC_FREE useless Cis/Cos
+ // free useless Cis/Cos
Vec_PtrForEachEntry( vCisOld, pObj, i )
if ( !Abc_ObjIsPi(pObj) && Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
Abc_NtkDeleteObj(pObj);
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 79c0655b..ecad9d37 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -569,7 +569,7 @@ void ABC_SolveInit( ABC_Manager mng )
if ( mng->nog == 0 )
{ printf( "ABC_SolveInit: Target is not specified by ABC_AddTarget().\n" ); return; }
- // ABC_FREE the previous target network if present
+ // free the previous target network if present
if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
// set the new target network
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index 7d99d146..7977824d 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -412,7 +412,7 @@ void Fraig_FeedBackCovering( Fraig_Man_t * p, Msat_IntVec_t * vPats )
Msat_IntVecPush( vPats, iPat );
}
- // ABC_FREE the set of columns
+ // free the set of columns
for ( i = 0; i < vColumns->nSize; i++ )
Fraig_MemFixedEntryRecycle( p->mmSims, (char *)vColumns->pArray[i] );
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 3bea5e42..ac6ea873 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -68,10 +68,6 @@
#define FRAIG_FULL (~((unsigned)0))
#define FRAIG_NUM_WORDS(n) (((n)>>5) + (((n)&31) > 0))
-// maximum/minimum operators
-#define FRAIG_MIN(a,b) (((a) < (b))? (a) : (b))
-#define FRAIG_MAX(a,b) (((a) > (b))? (a) : (b))
-
// generating random unsigned (#define RAND_MAX 0x7fff)
#define FRAIG_RANDOM_UNSIGNED ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
diff --git a/src/sat/fraig/fraigNode.c b/src/sat/fraig/fraigNode.c
index 6e3d3c7d..4cfe035d 100644
--- a/src/sat/fraig/fraigNode.c
+++ b/src/sat/fraig/fraigNode.c
@@ -174,7 +174,7 @@ Fraig_Node_t * Fraig_NodeCreate( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_
pNode->NumPi = -1;
// compute the level of this node
- pNode->Level = 1 + FRAIG_MAX(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level);
+ pNode->Level = 1 + ABC_MAX(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level);
pNode->fInv = Fraig_NodeIsSimComplement(p1) & Fraig_NodeIsSimComplement(p2);
pNode->fFailTfo = Fraig_Regular(p1)->fFailTfo | Fraig_Regular(p2)->fFailTfo;
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index 66698600..084d1538 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -1434,7 +1434,7 @@ void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t *
float * pFactors = Msat_SolverReadFactors(pMan->pSat);
if ( pFactors == NULL )
return;
- MaxLevel = FRAIG_MAX( pOld->Level, pNew->Level );
+ MaxLevel = ABC_MAX( pOld->Level, pNew->Level );
// create the variable order
for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ )
{
diff --git a/src/sat/fraig/fraigUtil.c b/src/sat/fraig/fraigUtil.c
index ea52d363..0930edbd 100644
--- a/src/sat/fraig/fraigUtil.c
+++ b/src/sat/fraig/fraigUtil.c
@@ -457,7 +457,7 @@ int Fraig_MappingUpdateLevel_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int
// compute levels of the children nodes
Level1 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p1), fMaximum );
Level2 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p2), fMaximum );
- pNode->Level = 1 + FRAIG_MAX( Level1, Level2 );
+ pNode->Level = 1 + ABC_MAX( Level1, Level2 );
if ( pNode->pNextE )
{
LevelE = Fraig_MappingUpdateLevel_rec( pMan, pNode->pNextE, fMaximum );
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index dece390c..6a518212 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -304,7 +304,7 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
void Msat_SolverClean( Msat_Solver_t * p, int nVars )
{
int i;
- // ABC_FREE the clauses
+ // free the clauses
int nClauses;
Msat_Clause_t ** pClauses;
@@ -384,7 +384,7 @@ void Msat_SolverFree( Msat_Solver_t * p )
{
int i;
- // ABC_FREE the clauses
+ // free the clauses
int nClauses;
Msat_Clause_t ** pClauses;
//printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ),