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
961f7532
Commit
961f7532
authored
Aug 01, 2011
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Changing the ordering of arguments in two iterators.
parent
820a147e
Hide whitespace changes
Inline
Side-by-side
Showing
16 changed files
with
82 additions
and
51 deletions
+82
-51
src/aig/aig/aig.h
+3
-8
src/aig/aig/aigJust.c
+1
-1
src/aig/dar/darCore.c
+6
-0
src/aig/llb/llb1Group.c
+4
-4
src/aig/llb/llb2Driver.c
+1
-1
src/aig/llb/llb2Image.c
+1
-1
src/aig/llb/llb4Nonlin.c
+1
-1
src/aig/saig/saigAbsCba.c
+3
-3
src/aig/saig/saigAbsPba.c
+3
-3
src/aig/saig/saigCexMin.c
+30
-0
src/aig/saig/saigDup.c
+1
-1
src/aig/saig/saigRefSat.c
+3
-3
src/base/abc/abc.h
+1
-1
src/base/abci/abcMffc.c
+9
-9
src/sat/pdr/pdrSat.c
+1
-1
src/sat/pdr/pdrTsim.c
+14
-14
No files found.
src/aig/aig/aig.h
View file @
961f7532
...
...
@@ -419,20 +419,15 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
// iterator over all objects, including those currently not used
#define Aig_ManForEachObj( p, pObj, i ) \
Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
// iterator over the objects whose IDs are stored in an array
#define Aig_ManForEachObjVec( vIds, p, pObj, i ) \
for ( i = 0; i < Vec_IntSize(vIds) && (((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))), 1); i++ )
// iterator over all nodes
#define Aig_ManForEachNode( p, pObj, i ) \
Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
// iterator over all nodes
#define Aig_ManForEachExor( p, pObj, i ) \
Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
// iterator over the nodes whose IDs are stored in the array
#define Aig_ManForEachNodeVec( p, vIds, pObj, i ) \
for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
// iterator over the nodes in the topological order
#define Aig_ManForEachNodeInOrder( p, pObj ) \
for ( assert(p->pOrderData), p->iPrev = 0, p->iNext = p->pOrderData[1]; \
p->iNext && (((pObj) = Aig_ManObj(p, p->iNext)), 1); \
p->iNext = p->pOrderData[2*p->iPrev+1] )
// these two procedures are only here for the use inside the iterator
static
inline
int
Aig_ObjFanout0Int
(
Aig_Man_t
*
p
,
int
ObjId
)
{
assert
(
ObjId
<
p
->
nFansAlloc
);
return
p
->
pFanData
[
5
*
ObjId
];
}
...
...
src/aig/aig/aigJust.c
View file @
961f7532
...
...
@@ -259,7 +259,7 @@ void Aig_ManJustExperiment( Aig_Man_t * pAig )
pPack
=
Aig_ManPackStart
(
pAig
);
vNodes
=
Aig_ManPackConstNodes
(
pPack
);
// Aig_ManForEachPo( pAig, pObj, i )
Aig_ManForEach
NodeVec
(
pAig
,
vNodes
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vNodes
,
pAig
,
pObj
,
i
)
{
if
(
pObj
->
fPhase
)
// const 1
{
...
...
src/aig/dar/darCore.c
View file @
961f7532
...
...
@@ -27,6 +27,12 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// iterator over the nodes in the topological order
#define Aig_ManForEachNodeInOrder( p, pObj ) \
for ( assert(p->pOrderData), p->iPrev = 0, p->iNext = p->pOrderData[1]; \
p->iNext && (((pObj) = Aig_ManObj(p, p->iNext)), 1); \
p->iNext = p->pOrderData[2*p->iPrev+1] )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
...
...
src/aig/llb/llb1Group.c
View file @
961f7532
...
...
@@ -318,19 +318,19 @@ Llb_Grp_t * Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec
// mark Cut1
Aig_ManIncrementTravId
(
pMan
->
pAig
);
Aig_ManForEach
NodeVec
(
pMan
->
pAig
,
vCut1
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCut1
,
pMan
->
pAig
,
pObj
,
i
)
Aig_ObjSetTravIdCurrent
(
pMan
->
pAig
,
pObj
);
// collect unmarked Cut2
Aig_ManForEach
NodeVec
(
pMan
->
pAig
,
vCut2
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCut2
,
pMan
->
pAig
,
pObj
,
i
)
if
(
!
Aig_ObjIsTravIdCurrent
(
pMan
->
pAig
,
pObj
)
)
Vec_PtrPush
(
p
->
vOuts
,
pObj
);
// mark nodes reachable from Cut2
Aig_ManIncrementTravId
(
pMan
->
pAig
);
Aig_ManForEach
NodeVec
(
pMan
->
pAig
,
vCut2
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCut2
,
pMan
->
pAig
,
pObj
,
i
)
Llb_ManGroupMarkNodes_rec
(
pMan
->
pAig
,
pObj
);
// collect marked Cut1
Aig_ManForEach
NodeVec
(
pMan
->
pAig
,
vCut1
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCut1
,
pMan
->
pAig
,
pObj
,
i
)
if
(
Aig_ObjIsTravIdCurrent
(
pMan
->
pAig
,
pObj
)
)
Vec_PtrPush
(
p
->
vIns
,
pObj
);
...
...
src/aig/llb/llb2Driver.c
View file @
961f7532
...
...
@@ -172,7 +172,7 @@ DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int Tim
bRes
=
Cudd_ReadOne
(
dd
);
Cudd_Ref
(
bRes
);
// mark the duplicated flop inputs
Aig_ManForEach
NodeVec
(
p
,
vVarsNs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vVarsNs
,
p
,
pObj
,
i
)
{
if
(
!
Saig_ObjIsLi
(
p
,
pObj
)
)
continue
;
...
...
src/aig/llb/llb2Image.c
View file @
961f7532
...
...
@@ -262,7 +262,7 @@ DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager *
int
i
,
TimeStop
;
TimeStop
=
dd
->
TimeStop
;
dd
->
TimeStop
=
0
;
bProd
=
Cudd_ReadOne
(
dd
);
Cudd_Ref
(
bProd
);
Aig_ManForEach
NodeVec
(
pAig
,
vNodeIds
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vNodeIds
,
pAig
,
pObj
,
i
)
{
bProd
=
Cudd_bddAnd
(
dd
,
bTemp
=
bProd
,
Cudd_bddIthVar
(
dd
,
Aig_ObjId
(
pObj
))
);
Cudd_Ref
(
bProd
);
Cudd_RecursiveDeref
(
dd
,
bTemp
);
...
...
src/aig/llb/llb4Nonlin.c
View file @
961f7532
...
...
@@ -340,7 +340,7 @@ Vec_Int_t * Llb_Nonlin4CreateOrder( Aig_Man_t * pAig )
// mark internal nodes to be used
Aig_ManCleanMarkA( pAig );
vNodes = Llb_Nonlin4CollectHighRefNodes( pAig, 4 );
Aig_ManForEach
NodeVec( pAig, vNodes
, pObj, i )
Aig_ManForEach
ObjVec( vNodes, pAig
, pObj, i )
pObj->fMarkA = 1;
printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
*/
...
...
src/aig/saig/saigAbsCba.c
View file @
961f7532
...
...
@@ -337,7 +337,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
// collect nodes starting from the roots
Aig_ManIncrementTravId
(
pAig
);
vRoots
=
Vec_VecEntryInt
(
vFrameCos
,
f
);
Aig_ManForEach
NodeVec
(
pAig
,
vRoots
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vRoots
,
pAig
,
pObj
,
i
)
Saig_ManCbaUnrollCollect_rec
(
pAig
,
pObj
,
Vec_VecEntryInt
(
vFrameObjs
,
f
),
(
Vec_Int_t
*
)(
f
?
Vec_VecEntry
(
vFrameCos
,
f
-
1
)
:
NULL
)
);
...
...
@@ -355,7 +355,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
{
// construct
vObjs
=
Vec_VecEntryInt
(
vFrameObjs
,
f
);
Aig_ManForEach
NodeVec
(
pAig
,
vObjs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vObjs
,
pAig
,
pObj
,
i
)
{
if
(
Aig_ObjIsNode
(
pObj
)
)
pObj
->
pData
=
Aig_And
(
pFrames
,
Aig_ObjChild0Copy
(
pObj
),
Aig_ObjChild1Copy
(
pObj
)
);
...
...
@@ -382,7 +382,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
break
;
// transfer
vRoots
=
Vec_VecEntryInt
(
vFrameCos
,
f
);
Aig_ManForEach
NodeVec
(
pAig
,
vRoots
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vRoots
,
pAig
,
pObj
,
i
)
{
Saig_ObjLiToLo
(
pAig
,
pObj
)
->
pData
=
pObj
->
pData
;
if
(
*
pvReg2Frame
)
...
...
src/aig/saig/saigAbsPba.c
View file @
961f7532
...
...
@@ -91,7 +91,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
Vec_IntPush
(
vRoots
,
Aig_ObjId
(
pObj
)
);
// collect nodes starting from the roots
Aig_ManIncrementTravId
(
pAig
);
Aig_ManForEach
NodeVec
(
pAig
,
vRoots
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vRoots
,
pAig
,
pObj
,
i
)
Saig_ManUnrollForPba_rec
(
pAig
,
pObj
,
Vec_VecEntryInt
(
vFrameObjs
,
f
),
(
Vec_Int_t
*
)(
f
?
Vec_VecEntry
(
vFrameCos
,
f
-
1
)
:
NULL
)
);
...
...
@@ -112,7 +112,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
{
// construct
vObjs
=
Vec_VecEntryInt
(
vFrameObjs
,
f
);
Aig_ManForEach
NodeVec
(
pAig
,
vObjs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vObjs
,
pAig
,
pObj
,
i
)
{
if
(
Aig_ObjIsNode
(
pObj
)
)
pObj
->
pData
=
Aig_And
(
pFrames
,
Aig_ObjChild0Copy
(
pObj
),
Aig_ObjChild1Copy
(
pObj
)
);
...
...
@@ -132,7 +132,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
if
(
f
==
nFrames
-
1
)
break
;
vRoots
=
Vec_VecEntryInt
(
vFrameCos
,
f
);
Aig_ManForEach
NodeVec
(
pAig
,
vRoots
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vRoots
,
pAig
,
pObj
,
i
)
{
if
(
Saig_ObjIsLi
(
pAig
,
pObj
)
)
{
...
...
src/aig/saig/saigCexMin.c
View file @
961f7532
...
...
@@ -321,6 +321,36 @@ Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex )
return
pCexMin
;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Saig_ManCexMinGetCos
(
Aig_Man_t
*
pAig
,
Abc_Cex_t
*
pCex
,
Vec_Vec_t
*
vFrameCis
,
int
f
,
Vec_Int_t
*
vTemp
)
{
Vec_Int_t
*
vFrameCisOne
;
Aig_Obj_t
*
pObj
;
int
i
;
Vec_IntClear
(
vTemp
);
if
(
f
==
Vec_VecSize
(
vFrameCis
)
-
1
)
{
pObj
=
Aig_ManPo
(
pAig
,
pCex
->
iPo
);
Vec_IntPush
(
vTemp
,
Aig_ObjId
(
pObj
)
);
return
;
}
vFrameCisOne
=
Vec_VecEntryInt
(
vFrameCis
,
f
+
1
);
Aig_ManForEachObjVec
(
vFrameCisOne
,
pAig
,
pObj
,
i
)
if
(
Saig_ObjIsLo
(
pAig
,
pObj
)
)
Vec_IntPush
(
vTemp
,
Aig_ObjId
(
Saig_ObjLoToLi
(
pAig
,
pObj
)
)
);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
...
...
src/aig/saig/saigDup.c
View file @
961f7532
...
...
@@ -112,7 +112,7 @@ Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs )
pObj
->
pData
=
Aig_And
(
pAigNew
,
Aig_ObjChild0Copy
(
pObj
),
Aig_ObjChild1Copy
(
pObj
)
);
// create POs
assert
(
Vec_IntSize
(
vPairs
)
%
2
==
0
);
Aig_ManForEach
NodeVec
(
pAig
,
vPairs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vPairs
,
pAig
,
pObj
,
i
)
{
pObj2
=
Aig_ManObj
(
pAig
,
Vec_IntEntry
(
vPairs
,
++
i
)
);
pMiter
=
Aig_Exor
(
pAigNew
,
(
Aig_Obj_t
*
)
pObj
->
pData
,
(
Aig_Obj_t
*
)
pObj2
->
pData
);
...
...
src/aig/saig/saigRefSat.c
View file @
961f7532
...
...
@@ -287,7 +287,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
// collect nodes starting from the roots
Aig_ManIncrementTravId
(
pAig
);
vRoots
=
Vec_VecEntryInt
(
vFrameCos
,
f
);
Aig_ManForEach
NodeVec
(
pAig
,
vRoots
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vRoots
,
pAig
,
pObj
,
i
)
Saig_ManUnrollCollect_rec
(
pAig
,
pObj
,
Vec_VecEntryInt
(
vFrameObjs
,
f
),
(
Vec_Int_t
*
)(
f
?
Vec_VecEntry
(
vFrameCos
,
f
-
1
)
:
NULL
)
);
...
...
@@ -305,7 +305,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
{
// construct
vObjs
=
Vec_VecEntryInt
(
vFrameObjs
,
f
);
Aig_ManForEach
NodeVec
(
pAig
,
vObjs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vObjs
,
pAig
,
pObj
,
i
)
{
if
(
Aig_ObjIsNode
(
pObj
)
)
pObj
->
pData
=
Aig_And
(
pFrames
,
Aig_ObjChild0Copy
(
pObj
),
Aig_ObjChild1Copy
(
pObj
)
);
...
...
@@ -332,7 +332,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
break
;
// transfer
vRoots
=
Vec_VecEntryInt
(
vFrameCos
,
f
);
Aig_ManForEach
NodeVec
(
pAig
,
vRoots
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vRoots
,
pAig
,
pObj
,
i
)
Saig_ObjLiToLo
(
pAig
,
pObj
)
->
pData
=
pObj
->
pData
;
}
// create output
...
...
src/base/abc/abc.h
View file @
961f7532
...
...
@@ -451,7 +451,7 @@ static inline void Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_At
#define Abc_NtkForEachObj( pNtk, pObj, i ) \
for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pObj) = Abc_NtkObj(pNtk, i)), 1); i++ ) \
if ( (pObj) == NULL ) {} else
#define Abc_NtkForEachObjVec(
pNtk, vIds
, pObj, i ) \
#define Abc_NtkForEachObjVec(
vIds, pNtk
, pObj, i ) \
for ( i = 0; i < Vec_IntSize(vIds) && (((pObj) = Abc_NtkObj(pNtk, Vec_IntEntry(vIds,i))), 1); i++ ) \
if ( (pObj) == NULL ) {} else
#define Abc_NtkForEachNet( pNtk, pNet, i ) \
...
...
src/base/abci/abcMffc.c
View file @
961f7532
...
...
@@ -455,14 +455,14 @@ void Abc_NktMffcPrintInt( char * pFileName, Abc_Ntk_t * pNtk, Vec_Int_t * vRoots
pFile
=
fopen
(
pFileName
,
"wb"
);
fprintf
(
pFile
,
".model %s_part
\n
"
,
pNtk
->
pName
);
fprintf
(
pFile
,
".inputs"
);
Abc_NtkForEachObjVec
(
pNtk
,
vLeaves
,
pObj
,
i
)
Abc_NtkForEachObjVec
(
vLeaves
,
pNtk
,
pObj
,
i
)
fprintf
(
pFile
,
" %s"
,
Abc_ObjName
(
pObj
)
);
fprintf
(
pFile
,
"
\n
"
);
fprintf
(
pFile
,
".outputs"
);
Abc_NtkForEachObjVec
(
pNtk
,
vRoots
,
pObj
,
i
)
Abc_NtkForEachObjVec
(
vRoots
,
pNtk
,
pObj
,
i
)
fprintf
(
pFile
,
" %s"
,
Abc_ObjName
(
pObj
)
);
fprintf
(
pFile
,
"
\n
"
);
Abc_NtkForEachObjVec
(
pNtk
,
vNodes
,
pObj
,
i
)
Abc_NtkForEachObjVec
(
vNodes
,
pNtk
,
pObj
,
i
)
{
fprintf
(
pFile
,
".names"
);
Abc_ObjForEachFanin
(
pObj
,
pFanin
,
k
)
...
...
@@ -757,12 +757,12 @@ void Abc_NktMffCollectLeafRootInt( Abc_Ntk_t * pNtk, Vec_Int_t * vNodes, Vec_Int
Abc_Obj_t
*
pObj
,
*
pNext
;
int
i
,
k
;
// mark
Abc_NtkForEachObjVec
(
pNtk
,
vNodes
,
pObj
,
i
)
Abc_NtkForEachObjVec
(
vNodes
,
pNtk
,
pObj
,
i
)
pObj
->
fMarkA
=
1
;
// collect leaves
Vec_IntClear
(
vLeaves
);
Abc_NtkIncrementTravId
(
pNtk
);
Abc_NtkForEachObjVec
(
pNtk
,
vNodes
,
pObj
,
i
)
Abc_NtkForEachObjVec
(
vNodes
,
pNtk
,
pObj
,
i
)
Abc_ObjForEachFanin
(
pObj
,
pNext
,
k
)
{
if
(
pNext
->
fMarkA
||
Abc_NodeIsTravIdCurrent
(
pNext
)
)
...
...
@@ -774,7 +774,7 @@ void Abc_NktMffCollectLeafRootInt( Abc_Ntk_t * pNtk, Vec_Int_t * vNodes, Vec_Int
if
(
vRoots
)
{
Vec_IntClear
(
vRoots
);
Abc_NtkForEachObjVec
(
pNtk
,
vNodes
,
pObj
,
i
)
Abc_NtkForEachObjVec
(
vNodes
,
pNtk
,
pObj
,
i
)
{
Abc_ObjForEachFanout
(
pObj
,
pNext
,
k
)
if
(
!
pNext
->
fMarkA
)
...
...
@@ -785,7 +785,7 @@ void Abc_NktMffCollectLeafRootInt( Abc_Ntk_t * pNtk, Vec_Int_t * vNodes, Vec_Int
}
}
// unmark
Abc_NtkForEachObjVec
(
pNtk
,
vNodes
,
pObj
,
i
)
Abc_NtkForEachObjVec
(
vNodes
,
pNtk
,
pObj
,
i
)
pObj
->
fMarkA
=
0
;
}
...
...
@@ -1051,7 +1051,7 @@ Abc_Obj_t * Abc_NktMffcFindBest( Abc_Ntk_t * pNtk, Vec_Int_t * vMarks, Vec_Int_t
int
i
,
Volume
;
// collect the fanouts of the fanins
vOuts
=
Vec_IntAlloc
(
100
);
Abc_NtkForEachObjVec
(
pNtk
,
vIns
,
pObj
,
i
)
Abc_NtkForEachObjVec
(
vIns
,
pNtk
,
pObj
,
i
)
{
vOuts2
=
(
Vec_Int_t
*
)
Vec_PtrEntry
(
vFanouts
,
Abc_ObjId
(
pObj
)
);
if
(
Vec_IntSize
(
vOuts2
)
>
16
)
...
...
@@ -1060,7 +1060,7 @@ Abc_Obj_t * Abc_NktMffcFindBest( Abc_Ntk_t * pNtk, Vec_Int_t * vMarks, Vec_Int_t
Vec_IntFree
(
vTemp
);
}
// check the pairs
Abc_NtkForEachObjVec
(
pNtk
,
vOuts
,
pPivot2
,
i
)
Abc_NtkForEachObjVec
(
vOuts
,
pNtk
,
pPivot2
,
i
)
{
if
(
Vec_IntEntry
(
vMarks
,
Abc_ObjId
(
pPivot2
))
==
0
)
continue
;
...
...
src/sat/pdr/pdrSat.c
View file @
961f7532
...
...
@@ -219,7 +219,7 @@ void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t
int
iVar
,
i
;
Vec_IntClear
(
vValues
);
pSat
=
Pdr_ManSolver
(
p
,
k
);
Aig_ManForEach
NodeVec
(
p
->
pAig
,
vObjIds
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vObjIds
,
p
->
pAig
,
pObj
,
i
)
{
iVar
=
Pdr_ObjSatVar
(
p
,
k
,
pObj
);
assert
(
iVar
>=
0
);
Vec_IntPush
(
vValues
,
sat_solver_var_value
(
pSat
,
iVar
)
);
...
...
src/sat/pdr/pdrTsim.c
View file @
961f7532
...
...
@@ -112,7 +112,7 @@ void Pdr_ManCollectCone( Aig_Man_t * pAig, Vec_Int_t * vCoObjs, Vec_Int_t * vCiO
Vec_IntClear
(
vNodes
);
Aig_ManIncrementTravId
(
pAig
);
Aig_ObjSetTravIdCurrent
(
pAig
,
Aig_ManConst1
(
pAig
)
);
Aig_ManForEach
NodeVec
(
pAig
,
vCoObjs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCoObjs
,
pAig
,
pObj
,
i
)
Pdr_ManCollectCone_rec
(
pAig
,
pObj
,
vCiObjs
,
vNodes
);
}
...
...
@@ -166,20 +166,20 @@ int Pdr_ManSimDataInit( Aig_Man_t * pAig,
int
i
;
// set the CI values
Pdr_ManSimInfoSet
(
pAig
,
Aig_ManConst1
(
pAig
),
PDR_ONE
);
Aig_ManForEach
NodeVec
(
pAig
,
vCiObjs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCiObjs
,
pAig
,
pObj
,
i
)
Pdr_ManSimInfoSet
(
pAig
,
pObj
,
(
Vec_IntEntry
(
vCiVals
,
i
)
?
PDR_ONE
:
PDR_ZER
)
);
// set the FOs to remove
if
(
vCi2Rem
!=
NULL
)
Aig_ManForEach
NodeVec
(
pAig
,
vCi2Rem
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCi2Rem
,
pAig
,
pObj
,
i
)
Pdr_ManSimInfoSet
(
pAig
,
pObj
,
PDR_UND
);
// perform ternary simulation
Aig_ManForEach
NodeVec
(
pAig
,
vNodes
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vNodes
,
pAig
,
pObj
,
i
)
Pdr_ManExtendOneEval
(
pAig
,
pObj
);
// transfer results to the output
Aig_ManForEach
NodeVec
(
pAig
,
vCoObjs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCoObjs
,
pAig
,
pObj
,
i
)
Pdr_ManExtendOneEval
(
pAig
,
pObj
);
// check the results
Aig_ManForEach
NodeVec
(
pAig
,
vCoObjs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCoObjs
,
pAig
,
pObj
,
i
)
if
(
Pdr_ManSimInfoGet
(
pAig
,
pObj
)
!=
(
Vec_IntEntry
(
vCoVals
,
i
)
?
PDR_ONE
:
PDR_ZER
)
)
return
0
;
return
1
;
...
...
@@ -212,7 +212,7 @@ int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec
// traverse
Vec_IntClear
(
vVis
);
Vec_IntPush
(
vVis
,
Aig_ObjId
(
pObj
)
);
Aig_ManForEach
NodeVec
(
pAig
,
vVis
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vVis
,
pAig
,
pObj
,
i
)
{
Aig_ObjForEachFanout
(
pAig
,
pObj
,
pFanout
,
iFanout
,
k
)
{
...
...
@@ -252,7 +252,7 @@ void Pdr_ManExtendUndo( Aig_Man_t * pAig, Vec_Int_t * vUndo )
{
Aig_Obj_t
*
pObj
;
int
i
,
Value
;
Aig_ManForEach
NodeVec
(
pAig
,
vUndo
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vUndo
,
pAig
,
pObj
,
i
)
{
Value
=
Vec_IntEntry
(
vUndo
,
++
i
);
assert
(
Pdr_ManSimInfoGet
(
pAig
,
pObj
)
==
PDR_UND
);
...
...
@@ -277,7 +277,7 @@ void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCi
int
i
,
Lit
;
// mark removed flop outputs
Aig_ManIncrementTravId
(
pAig
);
Aig_ManForEach
NodeVec
(
pAig
,
vCi2Rem
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCi2Rem
,
pAig
,
pObj
,
i
)
{
assert
(
Saig_ObjIsLo
(
pAig
,
pObj
)
);
Aig_ObjSetTravIdCurrent
(
pAig
,
pObj
);
...
...
@@ -285,7 +285,7 @@ void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCi
// collect flop outputs that are not marked
Vec_IntClear
(
vRes
);
Vec_IntClear
(
vPiLits
);
Aig_ManForEach
NodeVec
(
pAig
,
vCiObjs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCiObjs
,
pAig
,
pObj
,
i
)
{
if
(
Saig_ObjIsPi
(
pAig
,
pObj
)
)
{
...
...
@@ -322,10 +322,10 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals
for
(
i
=
0
;
i
<
Aig_ManPiNum
(
pAig
);
i
++
)
pBuff
[
i
]
=
'-'
;
pBuff
[
i
]
=
0
;
Aig_ManForEach
NodeVec
(
pAig
,
vCiObjs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCiObjs
,
pAig
,
pObj
,
i
)
pBuff
[
Aig_ObjPioNum
(
pObj
)]
=
(
Vec_IntEntry
(
vCiVals
,
i
)
?
'1'
:
'0'
);
if
(
vCi2Rem
)
Aig_ManForEach
NodeVec
(
pAig
,
vCi2Rem
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCi2Rem
,
pAig
,
pObj
,
i
)
pBuff
[
Aig_ObjPioNum
(
pObj
)]
=
'x'
;
printf
(
"%s
\n
"
,
pBuff
);
ABC_FREE
(
pBuff
);
...
...
@@ -402,7 +402,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
// try removing high-priority flops
Vec_IntClear
(
vCi2Rem
);
Aig_ManForEach
NodeVec
(
p
->
pAig
,
vCiObjs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCiObjs
,
p
->
pAig
,
pObj
,
i
)
{
if
(
!
Saig_ObjIsLo
(
p
->
pAig
,
pObj
)
)
continue
;
...
...
@@ -416,7 +416,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
Pdr_ManExtendUndo
(
p
->
pAig
,
vUndo
);
}
// try removing low-priority flops
Aig_ManForEach
NodeVec
(
p
->
pAig
,
vCiObjs
,
pObj
,
i
)
Aig_ManForEach
ObjVec
(
vCiObjs
,
p
->
pAig
,
pObj
,
i
)
{
if
(
!
Saig_ObjIsLo
(
p
->
pAig
,
pObj
)
)
continue
;
...
...
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