Skip to content
Projects
Groups
Snippets
Help
This project
Loading...
Sign in / Register
Toggle navigation
A
abc
Overview
Overview
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
lvzhengyang
abc
Commits
aa705a9a
Commit
aa705a9a
authored
Oct 02, 2012
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Renamed reference counting APIs in GIA package.
parent
49267fd3
Hide whitespace changes
Inline
Side-by-side
Showing
23 changed files
with
85 additions
and
93 deletions
+85
-93
src/aig/gia/gia.h
+10
-18
src/aig/gia/giaCSat.c
+3
-3
src/aig/gia/giaCSatOld.c
+3
-3
src/aig/gia/giaCTas.c
+3
-3
src/aig/gia/giaChoice.c
+1
-1
src/aig/gia/giaCof.c
+3
-3
src/aig/gia/giaDup.c
+4
-4
src/aig/gia/giaEmbed.c
+11
-11
src/aig/gia/giaEnable.c
+1
-1
src/aig/gia/giaForce.c
+11
-11
src/aig/gia/giaFront.c
+1
-1
src/aig/gia/giaIf.c
+2
-2
src/aig/gia/giaMan.c
+1
-1
src/aig/gia/giaSat.c
+1
-1
src/aig/gia/giaSwitch.c
+4
-4
src/aig/gia/giaUtil.c
+5
-5
src/base/cmd/cmdPlugin.c
+1
-1
src/opt/nwk/nwkAig.c
+4
-4
src/proof/abs/absRpm.c
+10
-10
src/proof/cec/cecClass.c
+2
-2
src/proof/cec/cecCorr.c
+2
-2
src/proof/cec/cecSeq.c
+1
-1
src/proof/cec/cecSweep.c
+1
-1
No files found.
src/aig/gia/gia.h
View file @
aa705a9a
...
...
@@ -109,7 +109,6 @@ struct Gia_Man_t_
int
nHTable
;
// hash table size
int
fAddStrash
;
// performs additional structural hashing
int
*
pRefs
;
// the reference count
int
*
pNodeRefs
;
// node references
Vec_Int_t
*
vLevels
;
// levels of the nodes
int
nLevels
;
// the mamixum level
int
nConstrs
;
// the number of constraints
...
...
@@ -368,21 +367,14 @@ static inline void Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj )
static
inline
int
Gia_ObjNum
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
)
{
return
(
int
)(
unsigned
char
)
Vec_StrGetEntry
(
p
->
vTtNums
,
Gia_ObjId
(
p
,
pObj
));
}
static
inline
void
Gia_ObjSetNum
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
,
int
n
)
{
assert
(
n
>=
0
&&
n
<
254
);
Vec_StrSetEntry
(
p
->
vTtNums
,
Gia_ObjId
(
p
,
pObj
),
(
char
)
n
);
}
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
int
Gia_ObjRefsId
(
Gia_Man_t
*
p
,
int
Id
)
{
assert
(
p
->
pRefs
);
return
p
->
pRefs
[
Id
];
}
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
));
}
static
inline
void
Gia_ObjRefFanin1Dec
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
){
assert
(
p
->
pRefs
);
Gia_ObjRefDec
(
p
,
Gia_ObjFanin1
(
pObj
));
}
static
inline
int
Gia_ObjNodeRefs
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
)
{
assert
(
p
->
pNodeRefs
);
return
p
->
pNodeRefs
[
Gia_ObjId
(
p
,
pObj
)];
}
static
inline
int
Gia_ObjNodeRefsId
(
Gia_Man_t
*
p
,
int
Id
)
{
assert
(
p
->
pNodeRefs
);
return
p
->
pNodeRefs
[
Id
];
}
static
inline
int
Gia_ObjNodeRefIncId
(
Gia_Man_t
*
p
,
int
Id
)
{
assert
(
p
->
pNodeRefs
);
return
p
->
pNodeRefs
[
Id
]
++
;
}
static
inline
int
Gia_ObjNodeRefDecId
(
Gia_Man_t
*
p
,
int
Id
)
{
assert
(
p
->
pNodeRefs
);
return
--
p
->
pNodeRefs
[
Id
];
}
static
inline
int
Gia_ObjNodeRefInc
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
)
{
assert
(
p
->
pNodeRefs
);
return
p
->
pNodeRefs
[
Gia_ObjId
(
p
,
pObj
)]
++
;
}
static
inline
int
Gia_ObjNodeRefDec
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
)
{
assert
(
p
->
pNodeRefs
);
return
--
p
->
pNodeRefs
[
Gia_ObjId
(
p
,
pObj
)];
}
static
inline
int
Gia_ObjRefNumId
(
Gia_Man_t
*
p
,
int
Id
)
{
assert
(
p
->
pRefs
);
return
p
->
pRefs
[
Id
];
}
static
inline
int
Gia_ObjRefNum
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
)
{
assert
(
p
->
pRefs
);
return
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
));
}
static
inline
void
Gia_ObjRefFanin1Dec
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
){
assert
(
p
->
pRefs
);
Gia_ObjRefDec
(
p
,
Gia_ObjFanin1
(
pObj
));
}
static
inline
void
Gia_ObjSetTravIdCurrent
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
)
{
assert
(
Gia_ObjId
(
p
,
pObj
)
<
p
->
nTravIdsAlloc
);
p
->
pTravIds
[
Gia_ObjId
(
p
,
pObj
)]
=
p
->
nTravIds
;
}
static
inline
void
Gia_ObjSetTravIdPrevious
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
)
{
assert
(
Gia_ObjId
(
p
,
pObj
)
<
p
->
nTravIdsAlloc
);
p
->
pTravIds
[
Gia_ObjId
(
p
,
pObj
)]
=
p
->
nTravIds
-
1
;
}
...
...
@@ -911,9 +903,9 @@ extern void Gia_ManSetPhase( Gia_Man_t * p );
extern
void
Gia_ManSetPhase1
(
Gia_Man_t
*
p
);
extern
void
Gia_ManCleanPhase
(
Gia_Man_t
*
p
);
extern
int
Gia_ManLevelNum
(
Gia_Man_t
*
p
);
extern
void
Gia_ManSetRefs
(
Gia_Man_t
*
p
);
extern
int
*
Gia_ManCreateMuxRefs
(
Gia_Man_t
*
p
);
extern
void
Gia_ManCreateValueRefs
(
Gia_Man_t
*
p
);
extern
void
Gia_ManCreateRefs
(
Gia_Man_t
*
p
);
extern
int
*
Gia_ManCreateMuxRefs
(
Gia_Man_t
*
p
);
extern
int
Gia_ManCrossCut
(
Gia_Man_t
*
p
);
extern
int
Gia_ManIsNormalized
(
Gia_Man_t
*
p
);
extern
Vec_Int_t
*
Gia_ManCollectPoIds
(
Gia_Man_t
*
p
);
...
...
src/aig/gia/giaCSat.c
View file @
aa705a9a
...
...
@@ -375,8 +375,8 @@ static inline int Cbs_VarFaninFanoutMax( Cbs_Man_t * p, Gia_Obj_t * pObj )
int
Count0
,
Count1
;
assert
(
!
Gia_IsComplement
(
pObj
)
);
assert
(
Gia_ObjIsAnd
(
pObj
)
);
Count0
=
Gia_ObjRef
s
(
p
->
pAig
,
Gia_ObjFanin0
(
pObj
)
);
Count1
=
Gia_ObjRef
s
(
p
->
pAig
,
Gia_ObjFanin1
(
pObj
)
);
Count0
=
Gia_ObjRef
Num
(
p
->
pAig
,
Gia_ObjFanin0
(
pObj
)
);
Count1
=
Gia_ObjRef
Num
(
p
->
pAig
,
Gia_ObjFanin1
(
pObj
)
);
return
Abc_MaxInt
(
Count0
,
Count1
);
}
...
...
@@ -888,7 +888,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
else
assert
(
0
);
assert
(
Cbs_VarIsJust
(
pVar
)
);
// chose decision variable using fanout count
if
(
Gia_ObjRef
s
(
p
->
pAig
,
Gia_ObjFanin0
(
pVar
))
>
Gia_ObjRefs
(
p
->
pAig
,
Gia_ObjFanin1
(
pVar
))
)
if
(
Gia_ObjRef
Num
(
p
->
pAig
,
Gia_ObjFanin0
(
pVar
))
>
Gia_ObjRefNum
(
p
->
pAig
,
Gia_ObjFanin1
(
pVar
))
)
pDecVar
=
Gia_Not
(
Gia_ObjChild0
(
pVar
));
else
pDecVar
=
Gia_Not
(
Gia_ObjChild1
(
pVar
));
...
...
src/aig/gia/giaCSatOld.c
View file @
aa705a9a
...
...
@@ -330,8 +330,8 @@ static inline int Cbs0_VarFaninFanoutMax( Cbs0_Man_t * p, Gia_Obj_t * pObj )
int
Count0
,
Count1
;
assert
(
!
Gia_IsComplement
(
pObj
)
);
assert
(
Gia_ObjIsAnd
(
pObj
)
);
Count0
=
Gia_ObjRef
s
(
p
->
pAig
,
Gia_ObjFanin0
(
pObj
)
);
Count1
=
Gia_ObjRef
s
(
p
->
pAig
,
Gia_ObjFanin1
(
pObj
)
);
Count0
=
Gia_ObjRef
Num
(
p
->
pAig
,
Gia_ObjFanin0
(
pObj
)
);
Count1
=
Gia_ObjRef
Num
(
p
->
pAig
,
Gia_ObjFanin1
(
pObj
)
);
return
Abc_MaxInt
(
Count0
,
Count1
);
}
...
...
@@ -612,7 +612,7 @@ int Cbs0_ManSolve_rec( Cbs0_Man_t * p )
else
assert
(
0
);
assert
(
Cbs0_VarIsJust
(
pVar
)
);
// chose decision variable using fanout count
if
(
Gia_ObjRef
s
(
p
->
pAig
,
Gia_ObjFanin0
(
pVar
))
>
Gia_ObjRefs
(
p
->
pAig
,
Gia_ObjFanin1
(
pVar
))
)
if
(
Gia_ObjRef
Num
(
p
->
pAig
,
Gia_ObjFanin0
(
pVar
))
>
Gia_ObjRefNum
(
p
->
pAig
,
Gia_ObjFanin1
(
pVar
))
)
pDecVar
=
Gia_Not
(
Gia_ObjChild0
(
pVar
));
else
pDecVar
=
Gia_Not
(
Gia_ObjChild1
(
pVar
));
...
...
src/aig/gia/giaCTas.c
View file @
aa705a9a
...
...
@@ -441,8 +441,8 @@ static inline int Tas_VarFaninFanoutMax( Tas_Man_t * p, Gia_Obj_t * pObj )
int
Count0
,
Count1
;
assert
(
!
Gia_IsComplement
(
pObj
)
);
assert
(
Gia_ObjIsAnd
(
pObj
)
);
Count0
=
Gia_ObjRef
s
(
p
->
pAig
,
Gia_ObjFanin0
(
pObj
)
);
Count1
=
Gia_ObjRef
s
(
p
->
pAig
,
Gia_ObjFanin1
(
pObj
)
);
Count0
=
Gia_ObjRef
Num
(
p
->
pAig
,
Gia_ObjFanin0
(
pObj
)
);
Count1
=
Gia_ObjRef
Num
(
p
->
pAig
,
Gia_ObjFanin1
(
pObj
)
);
return
Abc_MaxInt
(
Count0
,
Count1
);
}
...
...
@@ -1321,7 +1321,7 @@ int Tas_ManSolve_rec( Tas_Man_t * p, int Level )
if
(
pVar
!=
NULL
)
{
assert
(
Tas_VarIsJust
(
pVar
)
);
if
(
Gia_ObjRef
s
(
p
->
pAig
,
Gia_ObjFanin0
(
pVar
))
>
Gia_ObjRefs
(
p
->
pAig
,
Gia_ObjFanin1
(
pVar
))
)
if
(
Gia_ObjRef
Num
(
p
->
pAig
,
Gia_ObjFanin0
(
pVar
))
>
Gia_ObjRefNum
(
p
->
pAig
,
Gia_ObjFanin1
(
pVar
))
)
pDecVar
=
Gia_Not
(
Gia_ObjChild0
(
pVar
));
else
pDecVar
=
Gia_Not
(
Gia_ObjChild1
(
pVar
));
...
...
src/aig/gia/giaChoice.c
View file @
aa705a9a
...
...
@@ -228,7 +228,7 @@ int Gia_ManHasChoices( Gia_Man_t * p )
Gia_ManCreateRefs
(
p
);
Gia_ManForEachAnd
(
p
,
pObj
,
i
)
{
if
(
Gia_ObjRef
s
(
p
,
pObj
)
==
0
)
if
(
Gia_ObjRef
Num
(
p
,
pObj
)
==
0
)
{
if
(
Gia_ObjReprObj
(
p
,
Gia_ObjId
(
p
,
pObj
)
)
==
NULL
)
nFailNoRepr
++
;
...
...
src/aig/gia/giaCof.c
View file @
aa705a9a
...
...
@@ -143,7 +143,7 @@ Cof_Man_t * Cof_ManCreateLogicSimple( Gia_Man_t * pGia )
pObj
->
Value
=
iHandle
;
pObjLog
=
Cof_ManObj
(
p
,
iHandle
);
pObjLog
->
nFanins
=
0
;
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
pObj
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
pObj
);
pObjLog
->
Id
=
i
;
pObjLog
->
Value
=
0
;
if
(
Gia_ObjIsAnd
(
pObj
)
)
...
...
@@ -811,7 +811,7 @@ Vec_Int_t * Gia_ManCofVars( Gia_Man_t * p, int nFanLim )
Gia_ManCreateRefs
(
p
);
vVars
=
Vec_IntAlloc
(
100
);
Gia_ManForEachObj
(
p
,
pObj
,
i
)
if
(
Gia_ObjIsCand
(
pObj
)
&&
Gia_ObjRef
s
(
p
,
pObj
)
>=
nFanLim
)
if
(
Gia_ObjIsCand
(
pObj
)
&&
Gia_ObjRef
Num
(
p
,
pObj
)
>=
nFanLim
)
Vec_IntPush
(
vVars
,
i
);
ABC_FREE
(
p
->
pRefs
);
return
vVars
;
...
...
@@ -877,7 +877,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose
Vec_IntSort
(
vSigsNew
,
0
);
iVar
=
Vec_IntPop
(
vSigsNew
);
// Gia_ManCreateRefs( pAig );
// printf( "ref count = %d\n", Gia_ObjRef
s
( pAig, Gia_ManObj(pAig, iVar) ) );
// printf( "ref count = %d\n", Gia_ObjRef
Num
( pAig, Gia_ManObj(pAig, iVar) ) );
// ABC_FREE( pAig->pRefs );
pCof
=
Gia_ManDupCofInt
(
pAig
,
iVar
);
pNew
=
Gia_ManCleanup
(
pCof
);
...
...
src/aig/gia/giaDup.c
View file @
aa705a9a
...
...
@@ -1061,7 +1061,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fD
// check if there are PIs to be added
Gia_ManCreateRefs
(
p
);
Gia_ManForEachPi
(
p
,
pObj
,
i
)
if
(
!
fTrimCis
||
Gia_ObjRef
s
(
p
,
pObj
)
)
if
(
!
fTrimCis
||
Gia_ObjRef
Num
(
p
,
pObj
)
)
break
;
if
(
i
==
Gia_ManPiNum
(
p
)
)
// there is no PIs - add dummy PI
Gia_ManAppendCi
(
pNew
);
...
...
@@ -1069,7 +1069,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fD
Gia_ManFillValue
(
p
);
Gia_ManConst0
(
p
)
->
Value
=
0
;
Gia_ManForEachCi
(
p
,
pObj
,
i
)
if
(
!
fTrimCis
||
Gia_ObjRef
s
(
p
,
pObj
)
||
Gia_ObjIsRo
(
p
,
pObj
)
)
if
(
!
fTrimCis
||
Gia_ObjRef
Num
(
p
,
pObj
)
||
Gia_ObjIsRo
(
p
,
pObj
)
)
pObj
->
Value
=
Gia_ManAppendCi
(
pNew
);
Gia_ManForEachAnd
(
p
,
pObj
,
i
)
pObj
->
Value
=
Gia_ManAppendAnd
(
pNew
,
Gia_ObjFanin0Copy
(
pObj
),
Gia_ObjFanin1Copy
(
pObj
)
);
...
...
@@ -1142,7 +1142,7 @@ Gia_Man_t * Gia_ManDupTrimmed2( Gia_Man_t * p )
Gia_ObjRefFanin0Dec
(
p
,
pObj
);
// check if PIs are left
Gia_ManForEachPi
(
p
,
pObj
,
i
)
if
(
Gia_ObjRef
s
(
p
,
pObj
)
)
if
(
Gia_ObjRef
Num
(
p
,
pObj
)
)
break
;
if
(
i
==
Gia_ManPiNum
(
p
)
)
// there is no PIs - add dummy PI
Gia_ManAppendCi
(
pNew
);
...
...
@@ -1150,7 +1150,7 @@ Gia_Man_t * Gia_ManDupTrimmed2( Gia_Man_t * p )
Gia_ManFillValue
(
p
);
Gia_ManConst0
(
p
)
->
Value
=
0
;
Gia_ManForEachCi
(
p
,
pObj
,
i
)
if
(
Gia_ObjRef
s
(
p
,
pObj
)
||
Gia_ObjIsRo
(
p
,
pObj
)
)
if
(
Gia_ObjRef
Num
(
p
,
pObj
)
||
Gia_ObjIsRo
(
p
,
pObj
)
)
pObj
->
Value
=
Gia_ManAppendCi
(
pNew
);
Gia_ManForEachAnd
(
p
,
pObj
,
i
)
pObj
->
Value
=
Gia_ManAppendAnd
(
pNew
,
Gia_ObjFanin0Copy
(
pObj
),
Gia_ObjFanin1Copy
(
pObj
)
);
...
...
src/aig/gia/giaEmbed.c
View file @
aa705a9a
...
...
@@ -190,7 +190,7 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia )
pObjLog
=
Emb_ManObj
(
p
,
hHandle
);
pObjLog
->
hHandle
=
hHandle
;
pObjLog
->
nFanins
=
Gia_ManCoNum
(
pGia
);
//0;
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
Gia_ManConst0
(
pGia
)
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
Gia_ManConst0
(
pGia
)
);
// count objects
hHandle
+=
Emb_ObjSize
(
pObjLog
);
nNodes
=
1
;
...
...
@@ -204,7 +204,7 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia )
pObjLog
=
Emb_ManObj
(
p
,
hHandle
);
pObjLog
->
hHandle
=
hHandle
;
pObjLog
->
nFanins
=
Gia_ObjIsRo
(
pGia
,
pObj
);
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
pObj
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
pObj
);
pObjLog
->
fCi
=
1
;
// count objects
hHandle
+=
Emb_ObjSize
(
pObjLog
);
...
...
@@ -213,13 +213,13 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia )
// create internal nodes
Gia_ManForEachAnd
(
pGia
,
pObj
,
i
)
{
assert
(
Gia_ObjRef
s
(
pGia
,
pObj
)
>
0
);
assert
(
Gia_ObjRef
Num
(
pGia
,
pObj
)
>
0
);
// create node object
pObj
->
Value
=
hHandle
;
pObjLog
=
Emb_ManObj
(
p
,
hHandle
);
pObjLog
->
hHandle
=
hHandle
;
pObjLog
->
nFanins
=
2
;
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
pObj
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
pObj
);
// add fanins
pFanLog
=
Emb_ManObj
(
p
,
Gia_ObjValue
(
Gia_ObjFanin0
(
pObj
))
);
Emb_ObjAddFanin
(
pObjLog
,
pFanLog
);
...
...
@@ -364,7 +364,7 @@ void Emb_ManCreateRefsSpecial( Gia_Man_t * p )
Gia_ObjRefDec
(
p
,
Gia_Regular
(
pObjD0
)
);
}
Gia_ManForEachAnd
(
p
,
pObj
,
i
)
assert
(
Gia_ObjRef
s
(
p
,
pObj
)
>
0
);
assert
(
Gia_ObjRef
Num
(
p
,
pObj
)
>
0
);
Gia_ManCleanMark0
(
p
);
}
...
...
@@ -394,7 +394,7 @@ void Emb_ManTransformRefs( Gia_Man_t * p, int * pnObjs, int * pnFanios )
pObj
->
fMark0
=
1
;
// mark those nodes that have ref count more than 1
Gia_ManForEachAnd
(
p
,
pObj
,
i
)
pObj
->
fMark0
=
(
Gia_ObjRef
s
(
p
,
pObj
)
>
1
);
pObj
->
fMark0
=
(
Gia_ObjRef
Num
(
p
,
pObj
)
>
1
);
// mark the output drivers
Gia_ManForEachCoDriver
(
p
,
pObj
,
i
)
pObj
->
fMark0
=
1
;
...
...
@@ -516,7 +516,7 @@ Emb_Man_t * Emb_ManStart( Gia_Man_t * pGia )
pObjLog
=
Emb_ManObj
(
p
,
hHandle
);
pObjLog
->
hHandle
=
hHandle
;
pObjLog
->
nFanins
=
Gia_ManCoNum
(
pGia
);
//0;
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
Gia_ManConst0
(
pGia
)
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
Gia_ManConst0
(
pGia
)
);
// count objects
hHandle
+=
Emb_ObjSize
(
pObjLog
);
nNodes
++
;
...
...
@@ -530,7 +530,7 @@ Emb_Man_t * Emb_ManStart( Gia_Man_t * pGia )
pObjLog
=
Emb_ManObj
(
p
,
hHandle
);
pObjLog
->
hHandle
=
hHandle
;
pObjLog
->
nFanins
=
Gia_ObjIsRo
(
pGia
,
pObj
);
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
pObj
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
pObj
);
pObjLog
->
fCi
=
1
;
// count objects
hHandle
+=
Emb_ObjSize
(
pObjLog
);
...
...
@@ -543,17 +543,17 @@ Emb_Man_t * Emb_ManStart( Gia_Man_t * pGia )
{
if
(
pObj
->
fMark0
==
0
)
{
assert
(
Gia_ObjRef
s
(
pGia
,
pObj
)
==
0
);
assert
(
Gia_ObjRef
Num
(
pGia
,
pObj
)
==
0
);
continue
;
}
assert
(
Gia_ObjRef
s
(
pGia
,
pObj
)
>
0
);
assert
(
Gia_ObjRef
Num
(
pGia
,
pObj
)
>
0
);
Emb_ManCollectSuper
(
pGia
,
pObj
,
vSuper
,
vVisit
);
// create node object
pObj
->
Value
=
hHandle
;
pObjLog
=
Emb_ManObj
(
p
,
hHandle
);
pObjLog
->
hHandle
=
hHandle
;
pObjLog
->
nFanins
=
Vec_IntSize
(
vSuper
);
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
pObj
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
pObj
);
// add fanins
Gia_ManForEachObjVec
(
vSuper
,
pGia
,
pFanin
,
k
)
{
...
...
src/aig/gia/giaEnable.c
View file @
aa705a9a
...
...
@@ -110,7 +110,7 @@ void Gia_ManPrintSignals( Gia_Man_t * p, int * pFreq, char * pStr )
if
(
pFreq
[
i
]
>
10
)
{
printf
(
"%3d : Obj = %6d Refs = %6d Freq = %6d
\n
"
,
++
Counter
,
i
,
Gia_ObjRef
s
(
p
,
Gia_ManObj
(
p
,
i
)),
pFreq
[
i
]
);
++
Counter
,
i
,
Gia_ObjRef
Num
(
p
,
Gia_ManObj
(
p
,
i
)),
pFreq
[
i
]
);
Vec_IntPush
(
vObjs
,
i
);
}
Vec_IntFree
(
vObjs
);
...
...
src/aig/gia/giaForce.c
View file @
aa705a9a
...
...
@@ -168,7 +168,7 @@ Frc_Man_t * Frc_ManStartSimple( Gia_Man_t * pGia )
pObjLog
=
Frc_ManObj
(
p
,
hHandle
);
pObjLog
->
hHandle
=
hHandle
;
pObjLog
->
nFanins
=
0
;
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
Gia_ManConst0
(
pGia
)
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
Gia_ManConst0
(
pGia
)
);
// count objects
hHandle
+=
Frc_ObjSize
(
pObjLog
);
nNodes
=
1
;
...
...
@@ -182,7 +182,7 @@ Frc_Man_t * Frc_ManStartSimple( Gia_Man_t * pGia )
pObjLog
=
Frc_ManObj
(
p
,
hHandle
);
pObjLog
->
hHandle
=
hHandle
;
pObjLog
->
nFanins
=
0
;
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
pObj
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
pObj
);
pObjLog
->
fCi
=
0
;
// count objects
hHandle
+=
Frc_ObjSize
(
pObjLog
);
...
...
@@ -191,13 +191,13 @@ Frc_Man_t * Frc_ManStartSimple( Gia_Man_t * pGia )
// create internal nodes
Gia_ManForEachAnd
(
pGia
,
pObj
,
i
)
{
assert
(
Gia_ObjRef
s
(
pGia
,
pObj
)
>
0
);
assert
(
Gia_ObjRef
Num
(
pGia
,
pObj
)
>
0
);
// create node object
pObj
->
Value
=
hHandle
;
pObjLog
=
Frc_ManObj
(
p
,
hHandle
);
pObjLog
->
hHandle
=
hHandle
;
pObjLog
->
nFanins
=
2
;
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
pObj
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
pObj
);
// add fanins
pFanLog
=
Frc_ManObj
(
p
,
Gia_ObjValue
(
Gia_ObjFanin0
(
pObj
))
);
Frc_ObjAddFanin
(
pObjLog
,
pFanLog
);
...
...
@@ -341,7 +341,7 @@ void Frc_ManCreateRefsSpecial( Gia_Man_t * p )
Gia_ObjRefDec
(
p
,
Gia_Regular
(
pObjD0
)
);
}
Gia_ManForEachAnd
(
p
,
pObj
,
i
)
assert
(
Gia_ObjRef
s
(
p
,
pObj
)
>
0
);
assert
(
Gia_ObjRef
Num
(
p
,
pObj
)
>
0
);
Gia_ManCleanMark0
(
p
);
}
...
...
@@ -371,7 +371,7 @@ void Frc_ManTransformRefs( Gia_Man_t * p, int * pnObjs, int * pnFanios )
pObj
->
fMark0
=
1
;
// mark those nodes that have ref count more than 1
Gia_ManForEachAnd
(
p
,
pObj
,
i
)
pObj
->
fMark0
=
(
Gia_ObjRef
s
(
p
,
pObj
)
>
1
);
pObj
->
fMark0
=
(
Gia_ObjRef
Num
(
p
,
pObj
)
>
1
);
// mark the output drivers
Gia_ManForEachCoDriver
(
p
,
pObj
,
i
)
pObj
->
fMark0
=
1
;
...
...
@@ -451,7 +451,7 @@ Frc_Man_t * Frc_ManStart( Gia_Man_t * pGia )
pObjLog
=
Frc_ManObj
(
p
,
hHandle
);
pObjLog
->
hHandle
=
hHandle
;
pObjLog
->
nFanins
=
0
;
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
Gia_ManConst0
(
pGia
)
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
Gia_ManConst0
(
pGia
)
);
// count objects
hHandle
+=
Frc_ObjSize
(
pObjLog
);
nNodes
++
;
...
...
@@ -465,7 +465,7 @@ Frc_Man_t * Frc_ManStart( Gia_Man_t * pGia )
pObjLog
=
Frc_ManObj
(
p
,
hHandle
);
pObjLog
->
hHandle
=
hHandle
;
pObjLog
->
nFanins
=
0
;
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
pObj
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
pObj
);
pObjLog
->
fCi
=
1
;
// count objects
hHandle
+=
Frc_ObjSize
(
pObjLog
);
...
...
@@ -478,17 +478,17 @@ Frc_Man_t * Frc_ManStart( Gia_Man_t * pGia )
{
if
(
pObj
->
fMark0
==
0
)
{
assert
(
Gia_ObjRef
s
(
pGia
,
pObj
)
==
0
);
assert
(
Gia_ObjRef
Num
(
pGia
,
pObj
)
==
0
);
continue
;
}
assert
(
Gia_ObjRef
s
(
pGia
,
pObj
)
>
0
);
assert
(
Gia_ObjRef
Num
(
pGia
,
pObj
)
>
0
);
Frc_ManCollectSuper
(
pGia
,
pObj
,
vSuper
,
vVisit
);
// create node object
pObj
->
Value
=
hHandle
;
pObjLog
=
Frc_ManObj
(
p
,
hHandle
);
pObjLog
->
hHandle
=
hHandle
;
pObjLog
->
nFanins
=
Vec_IntSize
(
vSuper
);
pObjLog
->
nFanouts
=
Gia_ObjRef
s
(
pGia
,
pObj
);
pObjLog
->
nFanouts
=
Gia_ObjRef
Num
(
pGia
,
pObj
);
// add fanins
Gia_ManForEachObjVec
(
vSuper
,
pGia
,
pFanin
,
k
)
{
...
...
src/aig/gia/giaFront.c
View file @
aa705a9a
...
...
@@ -112,7 +112,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
int
nCrossCutMaxInit
=
Gia_ManCrossCut
(
p
);
int
iFront
=
0
;
//, clk = clock();
// set references for all objects
Gia_Man
Set
Refs
(
p
);
Gia_Man
CreateValue
Refs
(
p
);
// start the new manager
pNew
=
Gia_ManStart
(
Gia_ManObjNum
(
p
)
);
pNew
->
pName
=
Abc_UtilStrsav
(
p
->
pName
);
...
...
src/aig/gia/giaIf.c
View file @
aa705a9a
...
...
@@ -153,7 +153,7 @@ If_Man_t * Gia_ManToIf( Gia_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
// set up the choice node
/*
// if ( p->pReprs && p->pNexts && Gia_ObjIsHead( p, i ) )
if ( p->pNexts && Gia_ObjNext(p, i) && Gia_ObjRef
s
Id(p, i) )
if ( p->pNexts && Gia_ObjNext(p, i) && Gia_ObjRef
Num
Id(p, i) )
{
int iPrev, iFanin;
pIfMan->nChoices++;
...
...
@@ -509,7 +509,7 @@ void Gia_ManPrintNpnClasses( Gia_Man_t * p )
Gia_LutForEachFanin
(
p
,
i
,
iFan
,
k
)
{
Counter
+=
(
pLutClass
[
iFan
]
==
109
);
Counter2
+=
(
pLutClass
[
iFan
]
==
109
)
&&
(
Gia_ObjRef
s
Id
(
p
,
iFan
)
==
1
);
Counter2
+=
(
pLutClass
[
iFan
]
==
109
)
&&
(
Gia_ObjRef
Num
Id
(
p
,
iFan
)
==
1
);
}
OtherClasses
+=
(
Counter
>
1
);
OtherClasses2
+=
(
Counter2
>
1
);
...
...
src/aig/gia/giaMan.c
View file @
aa705a9a
...
...
@@ -108,7 +108,7 @@ void Gia_ManStop( Gia_Man_t * p )
ABC_FREE
(
p
->
pReprs
);
ABC_FREE
(
p
->
pNexts
);
ABC_FREE
(
p
->
pRefs
);
ABC_FREE
(
p
->
pNodeRefs
);
//
ABC_FREE( p->pNodeRefs );
ABC_FREE
(
p
->
pHTable
);
ABC_FREE
(
p
->
pObjs
);
ABC_FREE
(
p
->
pSpec
);
...
...
src/aig/gia/giaSat.c
View file @
aa705a9a
...
...
@@ -358,7 +358,7 @@ void Gia_ManSatExperiment( Gia_Man_t * p )
int
nWords
=
0
,
nWords2
=
0
;
pMan
=
Gia_ManSatStart
();
// mark the nodes to become roots of leaf-DAGs
Gia_Man
Set
Refs
(
p
);
Gia_Man
CreateValue
Refs
(
p
);
Gia_ManForEachObj
(
p
,
pObj
,
i
)
{
pObj
->
fMark0
=
0
;
...
...
src/aig/gia/giaSwitch.c
View file @
aa705a9a
...
...
@@ -720,7 +720,7 @@ float Gia_ManEvaluateSwitching( Gia_Man_t * p )
ABC_FREE
(
p
->
pRefs
);
Gia_ManCreateRefs
(
p
);
Gia_ManForEachObj
(
p
,
pObj
,
i
)
SwitchTotal
+=
(
float
)
Gia_ObjRef
s
(
p
,
pObj
)
*
p
->
pSwitching
[
i
]
/
255
;
SwitchTotal
+=
(
float
)
Gia_ObjRef
Num
(
p
,
pObj
)
*
p
->
pSwitching
[
i
]
/
255
;
return
SwitchTotal
;
}
...
...
@@ -777,9 +777,9 @@ float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbO
pObjDfs
=
Gia_ObjFromLit
(
pDfs
,
pObj
->
Value
);
Switch
=
pSwitching
[
Gia_ObjId
(
pDfs
,
pObjDfs
)
];
p
->
pSwitching
[
i
]
=
(
char
)((
Switch
>=
1
.
0
)
?
255
:
(
int
)((
0
.
002
+
Switch
)
*
255
));
// 0.00196 = (1/255)/2
SwitchTotal
+=
(
float
)
Gia_ObjRef
s
(
p
,
pObj
)
*
p
->
pSwitching
[
i
]
/
255
;
// SwitchTotal2 += Gia_ObjRef
s
(p, pObj) * Switch;
// printf( "%d = %.2f\n", i, Gia_ObjRef
s
(p, pObj) * Switch );
SwitchTotal
+=
(
float
)
Gia_ObjRef
Num
(
p
,
pObj
)
*
p
->
pSwitching
[
i
]
/
255
;
// SwitchTotal2 += Gia_ObjRef
Num
(p, pObj) * Switch;
// printf( "%d = %.2f\n", i, Gia_ObjRef
Num
(p, pObj) * Switch );
}
// printf( "\nSwitch float = %f. Switch char = %f.\n", SwitchTotal2, SwitchTotal );
Vec_IntFree
(
vSwitching
);
...
...
src/aig/gia/giaUtil.c
View file @
aa705a9a
...
...
@@ -465,7 +465,7 @@ int Gia_ManLevelNum( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
void
Gia_Man
Set
Refs
(
Gia_Man_t
*
p
)
void
Gia_Man
CreateValue
Refs
(
Gia_Man_t
*
p
)
{
Gia_Obj_t
*
pObj
;
int
i
;
...
...
@@ -554,7 +554,7 @@ int Gia_ManCrossCut( Gia_Man_t * p )
{
Gia_Obj_t
*
pObj
;
int
i
,
nCutCur
=
0
,
nCutMax
=
0
;
Gia_Man
Set
Refs
(
p
);
Gia_Man
CreateValue
Refs
(
p
);
Gia_ManForEachObj
(
p
,
pObj
,
i
)
{
if
(
pObj
->
Value
)
...
...
@@ -810,11 +810,11 @@ int Gia_NodeDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
return
0
;
assert
(
Gia_ObjIsAnd
(
pNode
)
);
pFanin
=
Gia_ObjFanin0
(
pNode
);
assert
(
Gia_ObjRef
s
(
p
,
pFanin
)
>
0
);
assert
(
Gia_ObjRef
Num
(
p
,
pFanin
)
>
0
);
if
(
Gia_ObjRefDec
(
p
,
pFanin
)
==
0
)
Counter
+=
Gia_NodeDeref_rec
(
p
,
pFanin
);
pFanin
=
Gia_ObjFanin1
(
pNode
);
assert
(
Gia_ObjRef
s
(
p
,
pFanin
)
>
0
);
assert
(
Gia_ObjRef
Num
(
p
,
pFanin
)
>
0
);
if
(
Gia_ObjRefDec
(
p
,
pFanin
)
==
0
)
Counter
+=
Gia_NodeDeref_rec
(
p
,
pFanin
);
return
Counter
+
1
;
...
...
@@ -1027,7 +1027,7 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
Gia_ObjFaninId0p
(
p
,
pObj
),
(
Gia_ObjFaninC0
(
pObj
)
?
"
\'
"
:
" "
),
Gia_ObjFaninId1p
(
p
,
pObj
),
(
Gia_ObjFaninC1
(
pObj
)
?
"
\'
"
:
" "
)
);
if
(
p
->
pRefs
)
printf
(
" (refs = %3d)"
,
Gia_ObjRef
s
(
p
,
pObj
)
);
printf
(
" (refs = %3d)"
,
Gia_ObjRef
Num
(
p
,
pObj
)
);
printf
(
"
\n
"
);
/*
if ( p->pRefs )
...
...
src/base/cmd/cmdPlugin.c
View file @
aa705a9a
...
...
@@ -301,7 +301,7 @@ Vec_Int_t * Abc_ManExpandCex( Gia_Man_t * pGia, Vec_Int_t * vCex )
{
Gia_ManForEachPi
(
pGia
,
pObj
,
i
)
{
if
(
Gia_ObjRef
s
(
pGia
,
pObj
)
==
0
)
if
(
Gia_ObjRef
Num
(
pGia
,
pObj
)
==
0
)
Vec_IntPush
(
vCexNew
,
0
);
else
{
...
...
src/opt/nwk/nwkAig.c
View file @
aa705a9a
...
...
@@ -165,12 +165,12 @@ Nwk_Man_t * Nwk_ManCreateFromGia( Gia_Man_t * p, Vec_Int_t * vPPis, Vec_Int_t *
ppCopies
=
ABC_ALLOC
(
Nwk_Obj_t
*
,
Gia_ManObjNum
(
p
)
);
// copy objects
pObj
=
Gia_ManConst0
(
p
);
// ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRef
s
(p,pObj) );
ppCopies
[
Gia_ObjId
(
p
,
pObj
)]
=
Nwk_ManCreateNode
(
pNtk
,
0
,
Gia_ObjRef
s
(
p
,
pObj
)
+
(
Vec_IntSize
(
vLeaves
)
>
Vec_IntSize
(
vPPis
)
?
Vec_IntSize
(
vLeaves
)
-
Vec_IntSize
(
vPPis
)
:
0
)
);
// ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRef
Num
(p,pObj) );
ppCopies
[
Gia_ObjId
(
p
,
pObj
)]
=
Nwk_ManCreateNode
(
pNtk
,
0
,
Gia_ObjRef
Num
(
p
,
pObj
)
+
(
Vec_IntSize
(
vLeaves
)
>
Vec_IntSize
(
vPPis
)
?
Vec_IntSize
(
vLeaves
)
-
Vec_IntSize
(
vPPis
)
:
0
)
);
Vec_IntPush
(
vMaps
,
Gia_ObjId
(
p
,
pObj
)
);
Gia_ManForEachObjVec
(
vLeaves
,
p
,
pObj
,
i
)
{
ppCopies
[
Gia_ObjId
(
p
,
pObj
)]
=
Nwk_ManCreateCi
(
pNtk
,
Gia_ObjRef
s
(
p
,
pObj
)
);
ppCopies
[
Gia_ObjId
(
p
,
pObj
)]
=
Nwk_ManCreateCi
(
pNtk
,
Gia_ObjRef
Num
(
p
,
pObj
)
);
assert
(
Vec_IntSize
(
vMaps
)
==
Nwk_ObjId
(
ppCopies
[
Gia_ObjId
(
p
,
pObj
)])
);
Vec_IntPush
(
vMaps
,
Gia_ObjId
(
p
,
pObj
)
);
}
...
...
@@ -181,7 +181,7 @@ Nwk_Man_t * Nwk_ManCreateFromGia( Gia_Man_t * p, Vec_Int_t * vPPis, Vec_Int_t *
}
Gia_ManForEachObjVec
(
vNodes
,
p
,
pObj
,
i
)
{
ppCopies
[
Gia_ObjId
(
p
,
pObj
)]
=
Nwk_ManCreateNode
(
pNtk
,
2
,
Gia_ObjRef
s
(
p
,
pObj
)
);
ppCopies
[
Gia_ObjId
(
p
,
pObj
)]
=
Nwk_ManCreateNode
(
pNtk
,
2
,
Gia_ObjRef
Num
(
p
,
pObj
)
);
Nwk_ObjAddFanin
(
ppCopies
[
Gia_ObjId
(
p
,
pObj
)],
ppCopies
[
Gia_ObjFaninId0p
(
p
,
pObj
)]
);
Nwk_ObjAddFanin
(
ppCopies
[
Gia_ObjId
(
p
,
pObj
)],
ppCopies
[
Gia_ObjFaninId1p
(
p
,
pObj
)]
);
assert
(
Vec_IntSize
(
vMaps
)
==
Nwk_ObjId
(
ppCopies
[
Gia_ObjId
(
p
,
pObj
)])
);
...
...
src/proof/abs/absRpm.c
View file @
aa705a9a
...
...
@@ -93,7 +93,7 @@ void Gia_ManComputeDoms( Gia_Man_t * p )
{
if
(
i
==
0
||
Gia_ObjIsCi
(
pObj
)
)
continue
;
if
(
pObj
->
fMark1
||
(
p
->
pRefs
&&
Gia_ObjIsAnd
(
pObj
)
&&
Gia_ObjRef
s
(
p
,
pObj
)
==
0
)
)
if
(
pObj
->
fMark1
||
(
p
->
pRefs
&&
Gia_ObjIsAnd
(
pObj
)
&&
Gia_ObjRef
Num
(
p
,
pObj
)
==
0
)
)
continue
;
if
(
Gia_ObjIsCo
(
pObj
)
)
{
...
...
@@ -173,7 +173,7 @@ Vec_Int_t * Gia_ManCollectDoms( Gia_Man_t * p )
{
if
(
!
pObj
->
fMark1
)
continue
;
if
(
p
->
pRefs
&&
Gia_ObjRef
s
(
p
,
pObj
)
==
0
)
if
(
p
->
pRefs
&&
Gia_ObjRef
Num
(
p
,
pObj
)
==
0
)
continue
;
iDom
=
Gia_ObjDom
(
p
,
pObj
);
if
(
iDom
==
-
1
)
...
...
@@ -238,7 +238,7 @@ void Gia_ManCountFanoutlessFlops( Gia_Man_t * p )
int
Counter
=
0
;
Gia_ManCreateRefs
(
p
);
Gia_ManForEachRo
(
p
,
pObj
,
i
)
if
(
Gia_ObjRef
s
(
p
,
pObj
)
==
0
)
if
(
Gia_ObjRef
Num
(
p
,
pObj
)
==
0
)
Counter
++
;
printf
(
"Fanoutless flops = %d.
\n
"
,
Counter
);
ABC_FREE
(
p
->
pRefs
);
...
...
@@ -305,11 +305,11 @@ int Abs_GiaObjDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
return
0
;
assert
(
Gia_ObjIsAnd
(
pNode
)
);
pFanin
=
Gia_ObjFanin0
(
pNode
);
assert
(
Gia_ObjRef
s
(
p
,
pFanin
)
>
0
);
assert
(
Gia_ObjRef
Num
(
p
,
pFanin
)
>
0
);
if
(
Gia_ObjRefDec
(
p
,
pFanin
)
==
0
)
Counter
+=
Abs_GiaObjDeref_rec
(
p
,
pFanin
);
pFanin
=
Gia_ObjFanin1
(
pNode
);
assert
(
Gia_ObjRef
s
(
p
,
pFanin
)
>
0
);
assert
(
Gia_ObjRef
Num
(
p
,
pFanin
)
>
0
);
if
(
Gia_ObjRefDec
(
p
,
pFanin
)
==
0
)
Counter
+=
Abs_GiaObjDeref_rec
(
p
,
pFanin
);
return
Counter
+
1
;
...
...
@@ -347,14 +347,14 @@ int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * vSupp )
int
nSize
=
Vec_IntSize
(
vSupp
);
int
i
,
RetValue
;
Gia_ManForEachObjVec
(
vSupp
,
p
,
pObj
,
i
)
if
(
i
<
nSize
&&
Gia_ObjRef
s
(
p
,
pObj
)
==
0
&&
!
Gia_ObjIsRo
(
p
,
pObj
)
)
// add removable leaves
if
(
i
<
nSize
&&
Gia_ObjRef
Num
(
p
,
pObj
)
==
0
&&
!
Gia_ObjIsRo
(
p
,
pObj
)
)
// add removable leaves
{
assert
(
pObj
->
fMark1
);
Vec_IntPush
(
vSupp
,
Gia_ObjId
(
p
,
pObj
)
);
}
RetValue
=
Vec_IntSize
(
vSupp
)
-
nSize
;
Gia_ManForEachObjVec
(
vSupp
,
p
,
pObj
,
i
)
if
(
i
<
nSize
&&
!
(
Gia_ObjRef
s
(
p
,
pObj
)
==
0
&&
!
Gia_ObjIsRo
(
p
,
pObj
))
)
// add non-removable leaves
if
(
i
<
nSize
&&
!
(
Gia_ObjRef
Num
(
p
,
pObj
)
==
0
&&
!
Gia_ObjIsRo
(
p
,
pObj
))
)
// add non-removable leaves
Vec_IntPush
(
vSupp
,
Gia_ObjId
(
p
,
pObj
)
);
assert
(
Vec_IntSize
(
vSupp
)
==
2
*
nSize
);
memmove
(
Vec_IntArray
(
vSupp
),
Vec_IntArray
(
vSupp
)
+
nSize
,
sizeof
(
int
)
*
nSize
);
...
...
@@ -413,7 +413,7 @@ void Abs_ManSupport2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
if
(
Gia_ObjIsTravIdCurrent
(
p
,
pObj
)
)
return
;
Gia_ObjSetTravIdCurrent
(
p
,
pObj
);
if
(
pObj
->
fMark1
||
Gia_ObjIsRo
(
p
,
pObj
)
||
Gia_ObjRef
s
(
p
,
pObj
)
>
0
)
if
(
pObj
->
fMark1
||
Gia_ObjIsRo
(
p
,
pObj
)
||
Gia_ObjRef
Num
(
p
,
pObj
)
>
0
)
{
Vec_IntPush
(
vSupp
,
Gia_ObjId
(
p
,
pObj
)
);
return
;
...
...
@@ -464,7 +464,7 @@ int Abs_ManSupport3( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
if
(
!
Gia_ObjIsAnd
(
pTemp
)
)
continue
;
assert
(
!
pTemp
->
fMark1
);
assert
(
Gia_ObjRef
s
(
p
,
pTemp
)
>
0
);
assert
(
Gia_ObjRef
Num
(
p
,
pTemp
)
>
0
);
pFan0
=
Gia_ObjFanin0
(
pTemp
);
pFan1
=
Gia_ObjFanin1
(
pTemp
);
if
(
Gia_ObjIsTravIdCurrent
(
p
,
pFan0
)
&&
Gia_ObjIsTravIdCurrent
(
p
,
pFan1
)
)
...
...
@@ -630,7 +630,7 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerb
Gia_ManForEachObjVec
(
vDoms
,
p
,
pObj
,
i
)
{
assert
(
!
pObj
->
fMark1
);
assert
(
Gia_ObjRef
s
(
p
,
pObj
)
>
0
);
assert
(
Gia_ObjRef
Num
(
p
,
pObj
)
>
0
);
// dereference root node
nNodes
=
Abs_GiaObjDeref_rec
(
p
,
pObj
);
/*
...
...
src/proof/cec/cecClass.c
View file @
aa705a9a
...
...
@@ -857,7 +857,7 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax )
p
->
pAig
->
pReprs
=
ABC_CALLOC
(
Gia_Rpr_t
,
Gia_ManObjNum
(
p
->
pAig
)
);
p
->
pAig
->
pNexts
=
ABC_CALLOC
(
int
,
Gia_ManObjNum
(
p
->
pAig
)
);
// create references
Gia_Man
Set
Refs
(
p
->
pAig
);
Gia_Man
CreateValue
Refs
(
p
->
pAig
);
// set starting representative of internal nodes to be constant 0
if
(
p
->
pPars
->
fLatchCorr
)
Gia_ManForEachObj
(
p
->
pAig
,
pObj
,
i
)
...
...
@@ -908,7 +908,7 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax )
int
Cec_ManSimClassesRefine
(
Cec_ManSim_t
*
p
)
{
int
i
;
Gia_Man
Set
Refs
(
p
->
pAig
);
Gia_Man
CreateValue
Refs
(
p
->
pAig
);
p
->
nWords
=
p
->
pPars
->
nWords
;
for
(
i
=
0
;
i
<
p
->
pPars
->
nRounds
;
i
++
)
{
...
...
src/proof/cec/cecCorr.c
View file @
aa705a9a
...
...
@@ -548,7 +548,7 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore
Vec_Ptr_t
*
vSimInfo
;
int
RetValue
=
0
,
iStart
=
0
;
vPairs
=
Gia_ManCorrCreateRemapping
(
pSim
->
pAig
);
Gia_Man
Set
Refs
(
pSim
->
pAig
);
Gia_Man
CreateValue
Refs
(
pSim
->
pAig
);
// pSim->pPars->nWords = 63;
pSim
->
pPars
->
nFrames
=
nFrames
;
vSimInfo
=
Vec_PtrAllocSimInfo
(
Gia_ManRegNum
(
pSim
->
pAig
)
+
Gia_ManPiNum
(
pSim
->
pAig
)
*
nFrames
,
pSim
->
pPars
->
nWords
);
...
...
@@ -584,7 +584,7 @@ int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexS
{
Vec_Ptr_t
*
vSimInfo
;
int
RetValue
=
0
,
iStart
=
0
;
Gia_Man
Set
Refs
(
pSim
->
pAig
);
Gia_Man
CreateValue
Refs
(
pSim
->
pAig
);
pSim
->
pPars
->
nFrames
=
1
;
vSimInfo
=
Vec_PtrAllocSimInfo
(
Gia_ManCiNum
(
pSim
->
pAig
),
pSim
->
pPars
->
nWords
);
while
(
iStart
<
Vec_IntSize
(
vCexStore
)
)
...
...
src/proof/cec/cecSeq.c
View file @
aa705a9a
...
...
@@ -191,7 +191,7 @@ int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t
pParsSim
->
nFrames
=
(
Vec_PtrSize
(
vSimInfo
)
-
Gia_ManRegNum
(
pAig
))
/
Gia_ManPiNum
(
pAig
);
pParsSim
->
nWords
=
Vec_PtrReadWordsSimInfo
(
vSimInfo
);
pParsSim
->
fCheckMiter
=
fCheckMiter
;
Gia_Man
Set
Refs
(
pAig
);
Gia_Man
CreateValue
Refs
(
pAig
);
pSim
=
Cec_ManSimStart
(
pAig
,
pParsSim
);
if
(
pBestState
)
pSim
->
pBestState
=
pBestState
;
...
...
src/proof/cec/cecSweep.c
View file @
aa705a9a
...
...
@@ -197,7 +197,7 @@ p->timePat += clock() - clk;
clk
=
clock
();
if
(
vInfo
!=
NULL
)
{
Gia_Man
Set
Refs
(
p
->
pAig
);
Gia_Man
CreateValue
Refs
(
p
->
pAig
);
for
(
i
=
0
;
i
<
pPat
->
nSeries
;
i
++
)
{
Cec_ManFraCreateInfo
(
pSim
,
pSim
->
vCiSimInfo
,
vInfo
,
i
);
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment