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
820a147e
Commit
820a147e
authored
Aug 01, 2011
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Removed useless typecasts related to changes in Vec_VecEntry().
parent
957b9f01
Hide whitespace changes
Inline
Side-by-side
Showing
30 changed files
with
77 additions
and
77 deletions
+77
-77
src/aig/aig/aigPart.c
+1
-1
src/aig/aig/aigPartSat.c
+2
-2
src/aig/aig/aigUtil.c
+3
-3
src/aig/cgt/cgtAig.c
+2
-2
src/aig/cgt/cgtDecide.c
+2
-2
src/aig/dar/darBalance.c
+1
-1
src/aig/dar/darRefact.c
+2
-2
src/aig/fra/fraPart.c
+9
-9
src/aig/gia/giaEra2.c
+2
-2
src/aig/hop/hopBalance.c
+1
-1
src/aig/hop/hopUtil.c
+3
-3
src/aig/ivy/ivyBalance.c
+1
-1
src/aig/ivy/ivyCutTrav.c
+4
-4
src/aig/ivy/ivyRwr.c
+1
-1
src/aig/ivy/ivySeq.c
+1
-1
src/aig/saig/saigAbsCba.c
+5
-5
src/aig/saig/saigAbsPba.c
+4
-4
src/aig/saig/saigCexMin.c
+2
-2
src/aig/saig/saigConstr2.c
+2
-2
src/aig/saig/saigRefSat.c
+11
-11
src/base/abc/abcAig.c
+2
-2
src/base/abci/abcBalance.c
+1
-1
src/opt/lpk/lpkCore.c
+1
-1
src/opt/lpk/lpkCut.c
+1
-1
src/opt/res/resCore.c
+2
-2
src/opt/rwr/rwrEva.c
+4
-4
src/opt/sim/simSymSat.c
+1
-1
src/opt/sim/simSymSim.c
+1
-1
src/opt/sim/simUtils.c
+3
-3
src/sat/pdr/pdrCore.c
+2
-2
No files found.
src/aig/aig/aigPart.c
View file @
820a147e
...
...
@@ -343,7 +343,7 @@ Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * pMan )
pObj
->
pNext
=
NULL
;
/*
Aig_ManForEachPo( pMan, pObj, i )
printf( "%d ", Vec_IntSize(
(Vec_Int_t *)Vec_VecEntry
(vSupports, i) ) );
printf( "%d ", Vec_IntSize(
Vec_VecEntryInt
(vSupports, i) ) );
printf( "\n" );
*/
return
vSupports
;
...
...
src/aig/aig/aigPartSat.c
View file @
820a147e
...
...
@@ -559,12 +559,12 @@ int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize,
clk
=
clock
();
// transform polarity of the AIG
if
(
fAlignPol
)
Aig_ManPartSetNodePolarity
(
p
,
pAig
,
(
Vec_Int_t
*
)
Vec_VecEntry
(
vPio2Id
,
i
)
);
Aig_ManPartSetNodePolarity
(
p
,
pAig
,
Vec_VecEntryInt
(
vPio2Id
,
i
)
);
else
Aig_ManPartResetNodePolarity
(
pAig
);
// add CNF of this partition to the SAT solver
if
(
Aig_ManAddNewCnfToSolver
(
pSat
,
pAig
,
vNode2Var
,
(
Vec_Int_t
*
)
Vec_VecEntry
(
vPio2Id
,
i
),
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vPart2Pos
,
i
),
fAlignPol
)
)
Vec_VecEntryInt
(
vPio2Id
,
i
),
Vec_VecEntry
(
vPart2Pos
,
i
),
fAlignPol
)
)
{
RetValue
=
1
;
break
;
...
...
src/aig/aig/aigUtil.c
View file @
820a147e
...
...
@@ -574,7 +574,7 @@ void Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int L
}
// AND case
Vec_VecExpand
(
vLevels
,
Level
);
vSuper
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vLevels
,
Level
);
vSuper
=
Vec_VecEntry
(
vLevels
,
Level
);
Aig_ObjCollectMulti
(
pObj
,
vSuper
);
fprintf
(
pFile
,
"%s"
,
(
Level
==
0
?
""
:
"("
)
);
Vec_PtrForEachEntry
(
Aig_Obj_t
*
,
vSuper
,
pFanin
,
i
)
...
...
@@ -623,7 +623,7 @@ void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, i
if
(
Aig_ObjIsExor
(
pObj
)
)
{
Vec_VecExpand
(
vLevels
,
Level
);
vSuper
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vLevels
,
Level
);
vSuper
=
Vec_VecEntry
(
vLevels
,
Level
);
Aig_ObjCollectMulti
(
pObj
,
vSuper
);
fprintf
(
pFile
,
"%s"
,
(
Level
==
0
?
""
:
"("
)
);
Vec_PtrForEachEntry
(
Aig_Obj_t
*
,
vSuper
,
pFanin
,
i
)
...
...
@@ -661,7 +661,7 @@ void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, i
}
// AND case
Vec_VecExpand
(
vLevels
,
Level
);
vSuper
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vLevels
,
Level
);
vSuper
=
Vec_VecEntry
(
vLevels
,
Level
);
Aig_ObjCollectMulti
(
pObj
,
vSuper
);
fprintf
(
pFile
,
"%s"
,
(
Level
==
0
?
""
:
"("
)
);
Vec_PtrForEachEntry
(
Aig_Obj_t
*
,
vSuper
,
pFanin
,
i
)
...
...
src/aig/cgt/cgtAig.c
View file @
820a147e
...
...
@@ -382,7 +382,7 @@ void Cgt_ManConstructCare( Aig_Man_t * pNew, Aig_Man_t * pCare, Vec_Vec_t * vSup
// construct the constraints
Vec_PtrForEachEntry
(
Aig_Obj_t
*
,
vLeaves
,
pLeaf
,
i
)
{
vOuts
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vSuppsInv
,
Aig_ObjPioNum
(
pLeaf
)
);
vOuts
=
Vec_VecEntryInt
(
vSuppsInv
,
Aig_ObjPioNum
(
pLeaf
)
);
Vec_IntForEachEntry
(
vOuts
,
iOut
,
k
)
{
pPo
=
Aig_ManPo
(
pCare
,
iOut
);
...
...
@@ -573,7 +573,7 @@ Aig_Man_t * Cgt_ManDeriveGatedAig( Aig_Man_t * pAig, Vec_Vec_t * vGates, int fRe
pObj
->
pData
=
Aig_ObjCreatePo
(
pNew
,
Aig_ObjChild0Copy
(
pObj
)
);
Saig_ManForEachLiLo
(
pAig
,
pObjLi
,
pObjLo
,
i
)
{
vOne
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vGates
,
i
);
vOne
=
Vec_VecEntry
(
vGates
,
i
);
if
(
Vec_PtrSize
(
vOne
)
==
0
)
pObjNew
=
Aig_ObjChild0Copy
(
pObjLi
);
else
...
...
src/aig/cgt/cgtDecide.c
View file @
820a147e
...
...
@@ -103,7 +103,7 @@ int Cgt_ManCheckGateComplete( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, Aig_Obj_t
{
if
(
Saig_ObjIsPo
(
pAig
,
pObj
)
)
return
0
;
vGates
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vGatesAll
,
Aig_ObjPioNum
(
pObj
)
-
Saig_ManPoNum
(
pAig
)
);
vGates
=
Vec_VecEntry
(
vGatesAll
,
Aig_ObjPioNum
(
pObj
)
-
Saig_ManPoNum
(
pAig
)
);
if
(
Vec_PtrFind
(
vGates
,
pGate
)
==
-
1
)
return
0
;
}
...
...
@@ -200,7 +200,7 @@ Vec_Vec_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nO
{
nHitsMax
=
0
;
pCandBest
=
NULL
;
vCands
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vGatesAll
,
i
);
vCands
=
Vec_VecEntry
(
vGatesAll
,
i
);
Vec_PtrForEachEntry
(
Aig_Obj_t
*
,
vCands
,
pCand
,
k
)
{
// check if this is indeed a clock-gate
...
...
src/aig/dar/darBalance.c
View file @
820a147e
...
...
@@ -112,7 +112,7 @@ Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
if
(
Vec_VecSize
(
vStore
)
<=
Level
)
Vec_VecPush
(
vStore
,
Level
,
0
);
// get the temporary array of nodes
vNodes
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vStore
,
Level
);
vNodes
=
Vec_VecEntry
(
vStore
,
Level
);
Vec_PtrClear
(
vNodes
);
// collect the nodes in the implication supergate
RetValue
=
Dar_BalanceCone_rec
(
pObj
,
pObj
,
vNodes
);
...
...
src/aig/dar/darRefact.c
View file @
820a147e
...
...
@@ -513,8 +513,8 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
// resynthesize each node once
clkStart
=
clock
();
vCut
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vCuts
,
0
);
vCut2
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vCuts
,
1
);
vCut
=
Vec_VecEntry
(
p
->
vCuts
,
0
);
vCut2
=
Vec_VecEntry
(
p
->
vCuts
,
1
);
p
->
nNodesInit
=
Aig_ManNodeNum
(
pAig
);
nNodesOld
=
Vec_PtrSize
(
pAig
->
vObjs
);
// pProgress = Bar_ProgressStart( stdout, nNodesOld );
...
...
src/aig/fra/fraPart.c
View file @
820a147e
...
...
@@ -66,7 +66,7 @@ ABC_PRT( "Supports", clock() - clk );
// remove last entry
Aig_ManForEachPo
(
p
,
pObj
,
i
)
{
vSup
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vSupps
,
i
);
vSup
=
Vec_VecEntryInt
(
vSupps
,
i
);
Vec_IntPop
(
vSup
);
// remember support
// pObj->pNext = (Aig_Obj_t *)vSup;
...
...
@@ -77,7 +77,7 @@ clk = clock();
vSuppsIn
=
Vec_VecStart
(
Aig_ManPiNum
(
p
)
);
Aig_ManForEachPo
(
p
,
pObj
,
i
)
{
vSup
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vSupps
,
i
);
vSup
=
Vec_VecEntryInt
(
vSupps
,
i
);
Vec_IntForEachEntry
(
vSup
,
Entry
,
k
)
Vec_VecPush
(
vSuppsIn
,
Entry
,
(
void
*
)(
ABC_PTRUINT_T
)
i
);
}
...
...
@@ -94,7 +94,7 @@ clk = clock();
{
// Bar_ProgressUpdate( pProgress, i, NULL );
// get old supports
vSup
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vSupps
,
i
);
vSup
=
Vec_VecEntryInt
(
vSupps
,
i
);
if
(
Vec_IntSize
(
vSup
)
<
2
)
continue
;
// compute new supports
...
...
@@ -109,7 +109,7 @@ clk = clock();
// pObj = Aig_ManObj( p, Entry );
// get support of this output
// vSup2 = (Vec_Int_t *)pObj->pNext;
vSup2
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vSupps
,
k
);
vSup2
=
Vec_VecEntryInt
(
vSupps
,
k
);
// count the number of common vars
nCommon
=
Vec_IntTwoCountCommon
(
vSup
,
vSup2
);
if
(
nCommon
<
2
)
...
...
@@ -200,7 +200,7 @@ ABC_PRT( "Supports", clock() - clk );
// remove last entry
Aig_ManForEachPo
(
p
,
pObj
,
i
)
{
vSup
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vSupps
,
i
);
vSup
=
Vec_VecEntryInt
(
vSupps
,
i
);
Vec_IntPop
(
vSup
);
// remember support
// pObj->pNext = (Aig_Obj_t *)vSup;
...
...
@@ -213,7 +213,7 @@ clk = clock();
{
if
(
i
==
p
->
nAsserts
)
break
;
vSup
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vSupps
,
i
);
vSup
=
Vec_VecEntryInt
(
vSupps
,
i
);
Vec_IntForEachEntry
(
vSup
,
Entry
,
k
)
Vec_VecPush
(
vSuppsIn
,
Entry
,
(
void
*
)(
ABC_PTRUINT_T
)
i
);
}
...
...
@@ -226,17 +226,17 @@ clk = clock();
{
if
(
i
%
50
!=
0
)
continue
;
vSup
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vSupps
,
i
);
vSup
=
Vec_VecEntryInt
(
vSupps
,
i
);
memset
(
pSupp
,
0
,
sizeof
(
char
)
*
Aig_ManPiNum
(
p
)
);
// go through each input of this output
Vec_IntForEachEntry
(
vSup
,
Entry
,
k
)
{
pSupp
[
Entry
]
=
1
;
vSup2
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vSuppsIn
,
Entry
);
vSup2
=
Vec_VecEntryInt
(
vSuppsIn
,
Entry
);
// go though each assert of this input
Vec_IntForEachEntry
(
vSup2
,
Entry2
,
m
)
{
vSup3
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vSupps
,
Entry2
);
vSup3
=
Vec_VecEntryInt
(
vSupps
,
Entry2
);
// go through each input of this assert
Vec_IntForEachEntry
(
vSup3
,
Entry3
,
n
)
{
...
...
src/aig/gia/giaEra2.c
View file @
820a147e
...
...
@@ -1557,8 +1557,8 @@ int Gia_ManAreDeriveNexts_rec( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
return
p
->
fStopped
;
}
// remember values in the cone and perform update
vTfos
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
p
->
vCiTfos
,
Gia_ObjCioId
(
pPivot
)
);
vLits
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
p
->
vCiLits
,
Gia_ObjCioId
(
pPivot
)
);
vTfos
=
Vec_VecEntryInt
(
p
->
vCiTfos
,
Gia_ObjCioId
(
pPivot
)
);
vLits
=
Vec_VecEntryInt
(
p
->
vCiLits
,
Gia_ObjCioId
(
pPivot
)
);
assert
(
Vec_IntSize
(
vTfos
)
==
Vec_IntSize
(
vLits
)
);
Gia_ManForEachObjVec
(
vTfos
,
p
->
pAig
,
pObj
,
i
)
{
...
...
src/aig/hop/hopBalance.c
View file @
820a147e
...
...
@@ -188,7 +188,7 @@ Vec_Ptr_t * Hop_NodeBalanceCone( Hop_Obj_t * pObj, Vec_Vec_t * vStore, int Level
if
(
Vec_VecSize
(
vStore
)
<=
Level
)
Vec_VecPush
(
vStore
,
Level
,
0
);
// get the temporary array of nodes
vNodes
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vStore
,
Level
);
vNodes
=
Vec_VecEntry
(
vStore
,
Level
);
Vec_PtrClear
(
vNodes
);
// collect the nodes in the implication supergate
RetValue
=
Hop_NodeBalanceCone_rec
(
pObj
,
pObj
,
vNodes
);
...
...
src/aig/hop/hopUtil.c
View file @
820a147e
...
...
@@ -341,7 +341,7 @@ void Hop_ObjPrintEqn( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int L
}
// AND case
Vec_VecExpand
(
vLevels
,
Level
);
vSuper
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vLevels
,
Level
);
vSuper
=
Vec_VecEntry
(
vLevels
,
Level
);
Hop_ObjCollectMulti
(
pObj
,
vSuper
);
fprintf
(
pFile
,
"%s"
,
(
Level
==
0
?
""
:
"("
)
);
Vec_PtrForEachEntry
(
Hop_Obj_t
*
,
vSuper
,
pFanin
,
i
)
...
...
@@ -390,7 +390,7 @@ void Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, i
if
(
Hop_ObjIsExor
(
pObj
)
)
{
Vec_VecExpand
(
vLevels
,
Level
);
vSuper
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vLevels
,
Level
);
vSuper
=
Vec_VecEntry
(
vLevels
,
Level
);
Hop_ObjCollectMulti
(
pObj
,
vSuper
);
fprintf
(
pFile
,
"%s"
,
(
Level
==
0
?
""
:
"("
)
);
Vec_PtrForEachEntry
(
Hop_Obj_t
*
,
vSuper
,
pFanin
,
i
)
...
...
@@ -428,7 +428,7 @@ void Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, i
}
// AND case
Vec_VecExpand
(
vLevels
,
Level
);
vSuper
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vLevels
,
Level
);
vSuper
=
Vec_VecEntry
(
vLevels
,
Level
);
Hop_ObjCollectMulti
(
pObj
,
vSuper
);
fprintf
(
pFile
,
"%s"
,
(
Level
==
0
?
""
:
"("
)
);
Vec_PtrForEachEntry
(
Hop_Obj_t
*
,
vSuper
,
pFanin
,
i
)
...
...
src/aig/ivy/ivyBalance.c
View file @
820a147e
...
...
@@ -255,7 +255,7 @@ Vec_Ptr_t * Ivy_NodeBalanceCone( Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level
if
(
Vec_VecSize
(
vStore
)
<=
Level
)
Vec_VecPush
(
vStore
,
Level
,
0
);
// get the temporary array of nodes
vNodes
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vStore
,
Level
);
vNodes
=
Vec_VecEntry
(
vStore
,
Level
);
Vec_PtrClear
(
vNodes
);
// collect the nodes in the implication supergate
RetValue
=
Ivy_NodeBalanceCone_rec
(
pObj
,
pObj
,
vNodes
);
...
...
src/aig/ivy/ivyCutTrav.c
View file @
820a147e
...
...
@@ -86,7 +86,7 @@ Ivy_Store_t * Ivy_NodeFindCutsTravAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLea
Vec_PtrForEachEntry
(
Ivy_Obj_t
*
,
vNodes
,
pLeaf
,
i
)
{
// skip the leaves
vCuts
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vBitCuts
,
Ivy_ObjTravId
(
pLeaf
)
);
vCuts
=
Vec_VecEntry
(
vBitCuts
,
Ivy_ObjTravId
(
pLeaf
)
);
if
(
Vec_PtrSize
(
vCuts
)
>
0
)
continue
;
// add elementary cut
...
...
@@ -94,8 +94,8 @@ Ivy_Store_t * Ivy_NodeFindCutsTravAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLea
// set it as the cut of this leaf
Vec_VecPush
(
vBitCuts
,
Ivy_ObjTravId
(
pLeaf
),
pBitCut
);
// get the fanin cuts
vCuts0
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vBitCuts
,
Ivy_ObjTravId
(
Ivy_ObjFanin0
(
pLeaf
)
)
);
vCuts1
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vBitCuts
,
Ivy_ObjTravId
(
Ivy_ObjFanin1
(
pLeaf
)
)
);
vCuts0
=
Vec_VecEntry
(
vBitCuts
,
Ivy_ObjTravId
(
Ivy_ObjFanin0
(
pLeaf
)
)
);
vCuts1
=
Vec_VecEntry
(
vBitCuts
,
Ivy_ObjTravId
(
Ivy_ObjFanin1
(
pLeaf
)
)
);
assert
(
Vec_PtrSize
(
vCuts0
)
>
0
);
assert
(
Vec_PtrSize
(
vCuts1
)
>
0
);
// merge the cuts
...
...
@@ -106,7 +106,7 @@ Ivy_Store_t * Ivy_NodeFindCutsTravAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLea
pCutStore
->
nCuts
=
0
;
pCutStore
->
nCutsMax
=
IVY_CUT_LIMIT
;
// collect the cuts of the root node
vCuts
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vBitCuts
,
Ivy_ObjTravId
(
pObj
)
);
vCuts
=
Vec_VecEntry
(
vBitCuts
,
Ivy_ObjTravId
(
pObj
)
);
Vec_PtrForEachEntry
(
unsigned
*
,
vCuts
,
pBitCut
,
i
)
{
pCut
=
pCutStore
->
pCuts
+
pCutStore
->
nCuts
++
;
...
...
src/aig/ivy/ivyRwr.c
View file @
820a147e
...
...
@@ -366,7 +366,7 @@ Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoo
Rwt_Node_t
*
pNode
,
*
pFanin
;
int
nNodesAdded
,
GainBest
,
i
,
k
;
// find the matching class of subgraphs
vSubgraphs
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vClasses
,
p
->
pMap
[
uTruth
]
);
vSubgraphs
=
Vec_VecEntry
(
p
->
vClasses
,
p
->
pMap
[
uTruth
]
);
p
->
nSubgraphs
+=
vSubgraphs
->
nSize
;
// determine the best subgraph
GainBest
=
-
1
;
...
...
src/aig/ivy/ivySeq.c
View file @
820a147e
...
...
@@ -316,7 +316,7 @@ Dec_Graph_t * Rwt_CutEvaluateSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * p
Rwt_Node_t
*
pNode
;
int
nNodesAdded
,
GainBest
,
i
;
// find the matching class of subgraphs
vSubgraphs
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vClasses
,
p
->
pMap
[
uTruth
]
);
vSubgraphs
=
Vec_VecEntry
(
p
->
vClasses
,
p
->
pMap
[
uTruth
]
);
p
->
nSubgraphs
+=
vSubgraphs
->
nSize
;
// determine the best subgraph
GainBest
=
-
1
;
...
...
src/aig/saig/saigAbsCba.c
View file @
820a147e
...
...
@@ -336,10 +336,10 @@ 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_Int_t
*
)
Vec_VecEntry
(
vFrameCos
,
f
);
vRoots
=
Vec_VecEntryInt
(
vFrameCos
,
f
);
Aig_ManForEachNodeVec
(
pAig
,
vRoots
,
pObj
,
i
)
Saig_ManCbaUnrollCollect_rec
(
pAig
,
pObj
,
(
Vec_Int_t
*
)
Vec_VecEntry
(
vFrameObjs
,
f
),
Vec_VecEntryInt
(
vFrameObjs
,
f
),
(
Vec_Int_t
*
)(
f
?
Vec_VecEntry
(
vFrameCos
,
f
-
1
)
:
NULL
)
);
}
...
...
@@ -354,7 +354,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
for
(
f
=
0
;
f
<=
pCex
->
iFrame
;
f
++
)
{
// construct
vObjs
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vFrameObjs
,
f
);
vObjs
=
Vec_VecEntryInt
(
vFrameObjs
,
f
);
Aig_ManForEachNodeVec
(
pAig
,
vObjs
,
pObj
,
i
)
{
if
(
Aig_ObjIsNode
(
pObj
)
)
...
...
@@ -381,7 +381,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
if
(
f
==
pCex
->
iFrame
)
break
;
// transfer
vRoots
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vFrameCos
,
f
);
vRoots
=
Vec_VecEntryInt
(
vFrameCos
,
f
);
Aig_ManForEachNodeVec
(
pAig
,
vRoots
,
pObj
,
i
)
{
Saig_ObjLiToLo
(
pAig
,
pObj
)
->
pData
=
pObj
->
pData
;
...
...
@@ -480,7 +480,7 @@ void Saig_ManCbaShrink( Saig_ManCba_t * p )
// print statistics
Vec_VecForEachLevelInt
(
p
->
vReg2Frame
,
vLevel
,
k
)
{
vLevel2
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
p
->
vReg2Value
,
k
);
vLevel2
=
Vec_VecEntryInt
(
p
->
vReg2Value
,
k
);
printf
(
"Level = %4d StateBits = %4d (%6.2f %%) CareBits = %4d (%6.2f %%)
\n
"
,
k
,
Vec_IntSize
(
vLevel
)
/
2
,
100
.
0
*
(
Vec_IntSize
(
vLevel
)
/
2
)
/
Aig_ManRegNum
(
p
->
pAig
),
Vec_IntSize
(
vLevel2
),
100
.
0
*
Vec_IntSize
(
vLevel2
)
/
Aig_ManRegNum
(
p
->
pAig
)
);
...
...
src/aig/saig/saigAbsPba.c
View file @
820a147e
...
...
@@ -86,14 +86,14 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
for
(
f
=
nFrames
-
1
;
f
>=
0
;
f
--
)
{
// add POs of this frame
vRoots
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vFrameCos
,
f
);
vRoots
=
Vec_VecEntryInt
(
vFrameCos
,
f
);
Saig_ManForEachPo
(
pAig
,
pObj
,
i
)
Vec_IntPush
(
vRoots
,
Aig_ObjId
(
pObj
)
);
// collect nodes starting from the roots
Aig_ManIncrementTravId
(
pAig
);
Aig_ManForEachNodeVec
(
pAig
,
vRoots
,
pObj
,
i
)
Saig_ManUnrollForPba_rec
(
pAig
,
pObj
,
(
Vec_Int_t
*
)
Vec_VecEntry
(
vFrameObjs
,
f
),
Vec_VecEntryInt
(
vFrameObjs
,
f
),
(
Vec_Int_t
*
)(
f
?
Vec_VecEntry
(
vFrameCos
,
f
-
1
)
:
NULL
)
);
}
// derive unrolled timeframes
...
...
@@ -111,7 +111,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
for
(
f
=
0
;
f
<
nFrames
;
f
++
)
{
// construct
vObjs
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vFrameObjs
,
f
);
vObjs
=
Vec_VecEntryInt
(
vFrameObjs
,
f
);
Aig_ManForEachNodeVec
(
pAig
,
vObjs
,
pObj
,
i
)
{
if
(
Aig_ObjIsNode
(
pObj
)
)
...
...
@@ -131,7 +131,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
// transfer
if
(
f
==
nFrames
-
1
)
break
;
vRoots
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vFrameCos
,
f
);
vRoots
=
Vec_VecEntryInt
(
vFrameCos
,
f
);
Aig_ManForEachNodeVec
(
pAig
,
vRoots
,
pObj
,
i
)
{
if
(
Saig_ObjIsLi
(
pAig
,
pObj
)
)
...
...
src/aig/saig/saigCexMin.c
View file @
820a147e
...
...
@@ -184,7 +184,7 @@ void Saig_ManCollectFrameTerms( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t *
Aig_ManIncrementTravId
(
pAig
);
Vec_VecForEachEntryIntLevel
(
vFrameLis
,
Entry
,
i
,
f
)
Saig_ManCollectFrameTerms_rec
(
pAig
,
Aig_ManObj
(
pAig
,
Entry
),
(
Vec_Int_t
*
)
Vec_VecEntry
(
vFramePis
,
f
),
Vec_VecEntryInt
(
vFramePis
,
f
),
(
Vec_Int_t
*
)(
f
?
Vec_VecEntry
(
vFrameLis
,
f
-
1
)
:
NULL
)
);
}
}
...
...
@@ -302,7 +302,7 @@ Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex )
Aig_ManIncrementTravId
(
pAig
);
Vec_VecForEachEntryIntLevel
(
vFrameLis
,
Entry
,
i
,
f
)
Saig_ManCexMinFindReason_rec
(
pAig
,
Aig_ManObj
(
pAig
,
Entry
),
vPrios
,
(
Vec_Int_t
*
)
Vec_VecEntry
(
vReasonPis
,
f
),
Vec_VecEntryInt
(
vReasonPis
,
f
),
(
Vec_Int_t
*
)(
f
?
Vec_VecEntry
(
vReasonLis
,
f
-
1
)
:
NULL
)
);
}
...
...
src/aig/saig/saigConstr2.c
View file @
820a147e
...
...
@@ -784,7 +784,7 @@ Vec_Vec_t * Saig_ManDetectConstrFunc( Aig_Man_t * p, int nFrames, int nConfs, in
pObjNew
=
Aig_NotCond
(
pObj
,
!
Aig_IsComplement
(
pRepr
));
for
(
j
=
0
;
j
<
k
;
j
++
)
if
(
Vec_PtrFind
(
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vCands
,
j
),
pObjNew
)
>=
0
)
if
(
Vec_PtrFind
(
Vec_VecEntry
(
vCands
,
j
),
pObjNew
)
>=
0
)
break
;
if
(
j
==
k
)
Vec_VecPush
(
vCands
,
k
,
pObjNew
);
...
...
@@ -795,7 +795,7 @@ Vec_Vec_t * Saig_ManDetectConstrFunc( Aig_Man_t * p, int nFrames, int nConfs, in
pObjNew
=
Aig_NotCond
(
pObj
,
Aig_IsComplement
(
pRepr
));
for
(
j
=
0
;
j
<
k
;
j
++
)
if
(
Vec_PtrFind
(
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vCands
,
j
),
pObjNew
)
>=
0
)
if
(
Vec_PtrFind
(
Vec_VecEntry
(
vCands
,
j
),
pObjNew
)
>=
0
)
break
;
if
(
j
==
k
)
Vec_VecPush
(
vCands
,
k
,
pObjNew
);
...
...
src/aig/saig/saigRefSat.c
View file @
820a147e
...
...
@@ -286,10 +286,10 @@ 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_Int_t
*
)
Vec_VecEntry
(
vFrameCos
,
f
);
vRoots
=
Vec_VecEntryInt
(
vFrameCos
,
f
);
Aig_ManForEachNodeVec
(
pAig
,
vRoots
,
pObj
,
i
)
Saig_ManUnrollCollect_rec
(
pAig
,
pObj
,
(
Vec_Int_t
*
)
Vec_VecEntry
(
vFrameObjs
,
f
),
Vec_VecEntryInt
(
vFrameObjs
,
f
),
(
Vec_Int_t
*
)(
f
?
Vec_VecEntry
(
vFrameCos
,
f
-
1
)
:
NULL
)
);
}
...
...
@@ -304,7 +304,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
for
(
f
=
0
;
f
<=
pCex
->
iFrame
;
f
++
)
{
// construct
vObjs
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vFrameObjs
,
f
);
vObjs
=
Vec_VecEntryInt
(
vFrameObjs
,
f
);
Aig_ManForEachNodeVec
(
pAig
,
vObjs
,
pObj
,
i
)
{
if
(
Aig_ObjIsNode
(
pObj
)
)
...
...
@@ -331,7 +331,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
if
(
f
==
pCex
->
iFrame
)
break
;
// transfer
vRoots
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
vFrameCos
,
f
);
vRoots
=
Vec_VecEntryInt
(
vFrameCos
,
f
);
Aig_ManForEachNodeVec
(
pAig
,
vRoots
,
pObj
,
i
)
Saig_ObjLiToLo
(
pAig
,
pObj
)
->
pData
=
pObj
->
pData
;
}
...
...
@@ -574,7 +574,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder )
Vec_IntPush
(
vAssumps
,
Entry
);
for
(
i
=
0
;
i
<
Vec_VecSize
(
vLits
);
i
++
)
printf
(
"%d "
,
Vec_IntSize
(
(
Vec_Int_t
*
)
Vec_VecEntry
(
vLits
,
i
)
)
);
printf
(
"%d "
,
Vec_IntSize
(
Vec_VecEntryInt
(
vLits
,
i
)
)
);
printf
(
"
\n
"
);
if
(
p
->
fVerbose
)
...
...
@@ -624,7 +624,7 @@ clk = clock();
Vec_IntPush
(
vAssumps
,
Entry
);
// for ( i = 0; i < Vec_VecSize(vLits); i++ )
// printf( "%d ", Vec_IntSize(
(Vec_Int_t *)Vec_VecEntry
(vLits, i) ) );
// printf( "%d ", Vec_IntSize(
Vec_VecEntryInt
(vLits, i) ) );
// printf( "\n" );
if
(
p
->
fVerbose
)
...
...
@@ -655,12 +655,12 @@ clk = clock();
continue;
// UNSAT - remove literals
Vec_IntClear(
(Vec_Int_t *)Vec_VecEntry
(vLits, f) );
Vec_IntClear(
Vec_VecEntryInt
(vLits, f) );
Counter--;
}
for ( i = 0; i < Vec_VecSize(vLits); i++ )
printf( "%d ", Vec_IntSize(
(Vec_Int_t *)Vec_VecEntry
(vLits, i) ) );
printf( "%d ", Vec_IntSize(
Vec_VecEntryInt
(vLits, i) ) );
printf( "\n" );
if ( p->fVerbose )
...
...
@@ -787,7 +787,7 @@ Vec_Int_t * Saig_RefManRefineWithSat( Saig_RefMan_t * p, Vec_Int_t * vAigPis )
// derive literals
vLits
=
Saig_RefManOrderLiterals
(
p
,
vVar2PiId
,
vAssumps
);
for
(
i
=
0
;
i
<
Vec_VecSize
(
vLits
);
i
++
)
printf
(
"%d "
,
Vec_IntSize
(
(
Vec_Int_t
*
)
Vec_VecEntry
(
vLits
,
i
)
)
);
printf
(
"%d "
,
Vec_IntSize
(
Vec_VecEntryInt
(
vLits
,
i
)
)
);
printf
(
"
\n
"
);
// create different sets of assumptions
...
...
@@ -808,12 +808,12 @@ Vec_Int_t * Saig_RefManRefineWithSat( Saig_RefMan_t * p, Vec_Int_t * vAigPis )
continue
;
// UNSAT - remove literals
Vec_IntClear
(
(
Vec_Int_t
*
)
Vec_VecEntry
(
vLits
,
f
)
);
Vec_IntClear
(
Vec_VecEntryInt
(
vLits
,
f
)
);
Counter
--
;
}
for
(
i
=
0
;
i
<
Vec_VecSize
(
vLits
);
i
++
)
printf
(
"%d "
,
Vec_IntSize
(
(
Vec_Int_t
*
)
Vec_VecEntry
(
vLits
,
i
)
)
);
printf
(
"%d "
,
Vec_IntSize
(
Vec_VecEntryInt
(
vLits
,
i
)
)
);
printf
(
"
\n
"
);
// create assumptions
...
...
src/base/abc/abcAig.c
View file @
820a147e
...
...
@@ -1172,7 +1172,7 @@ void Abc_AigRemoveFromLevelStructure( Vec_Vec_t * vStruct, Abc_Obj_t * pNode )
Abc_Obj_t
*
pTemp
;
int
m
;
assert
(
pNode
->
fMarkA
);
vVecTemp
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vStruct
,
pNode
->
Level
);
vVecTemp
=
Vec_VecEntry
(
vStruct
,
pNode
->
Level
);
Vec_PtrForEachEntry
(
Abc_Obj_t
*
,
vVecTemp
,
pTemp
,
m
)
{
if
(
pTemp
!=
pNode
)
...
...
@@ -1201,7 +1201,7 @@ void Abc_AigRemoveFromLevelStructureR( Vec_Vec_t * vStruct, Abc_Obj_t * pNode )
Abc_Obj_t
*
pTemp
;
int
m
;
assert
(
pNode
->
fMarkB
);
vVecTemp
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vStruct
,
Abc_ObjReverseLevel
(
pNode
)
);
vVecTemp
=
Vec_VecEntry
(
vStruct
,
Abc_ObjReverseLevel
(
pNode
)
);
Vec_PtrForEachEntry
(
Abc_Obj_t
*
,
vVecTemp
,
pTemp
,
m
)
{
if
(
pTemp
!=
pNode
)
...
...
src/base/abci/abcBalance.c
View file @
820a147e
...
...
@@ -303,7 +303,7 @@ Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Le
if
(
Vec_VecSize
(
vStorage
)
<=
Level
)
Vec_VecPush
(
vStorage
,
Level
,
0
);
// get the temporary array of nodes
vNodes
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
vStorage
,
Level
);
vNodes
=
Vec_VecEntry
(
vStorage
,
Level
);
Vec_PtrClear
(
vNodes
);
// collect the nodes in the implication supergate
RetValue
=
Abc_NodeBalanceCone_rec
(
pNode
,
vNodes
,
1
,
fDuplicate
,
fSelective
);
...
...
src/opt/lpk/lpkCore.c
View file @
820a147e
...
...
@@ -98,7 +98,7 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
Vec_Ptr_t
*
vNodes
;
Abc_Obj_t
*
pTemp
;
int
i
;
vNodes
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vVisited
,
iNode
);
vNodes
=
Vec_VecEntry
(
p
->
vVisited
,
iNode
);
if
(
Vec_PtrSize
(
vNodes
)
==
0
)
return
1
;
Vec_PtrForEachEntry
(
Abc_Obj_t
*
,
vNodes
,
pTemp
,
i
)
...
...
src/opt/lpk/lpkCut.c
View file @
820a147e
...
...
@@ -233,7 +233,7 @@ unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv )
void
Lpk_NodeRecordImpact
(
Lpk_Man_t
*
p
)
{
Lpk_Cut_t
*
pCut
;
Vec_Ptr_t
*
vNodes
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vVisited
,
p
->
pObj
->
Id
);
Vec_Ptr_t
*
vNodes
=
Vec_VecEntry
(
p
->
vVisited
,
p
->
pObj
->
Id
);
Abc_Obj_t
*
pNode
;
int
i
,
k
;
// collect the nodes that impact the given node
...
...
src/opt/res/resCore.c
View file @
820a147e
...
...
@@ -320,7 +320,7 @@ p->timeSim += clock() - clk;
p
->
nConstsUsed
++
;
pFunc
=
p
->
pSim
->
fConst1
?
Hop_ManConst1
((
Hop_Man_t
*
)
pNtk
->
pManFunc
)
:
Hop_ManConst0
((
Hop_Man_t
*
)
pNtk
->
pManFunc
);
vFanins
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vResubsW
,
0
);
vFanins
=
Vec_VecEntry
(
p
->
vResubsW
,
0
);
Vec_PtrClear
(
vFanins
);
Res_UpdateNetwork
(
pObj
,
vFanins
,
pFunc
,
p
->
vLevels
);
continue
;
...
...
@@ -389,7 +389,7 @@ p->timeInt += clock() - clk;
// update the network
clk
=
clock
();
Res_UpdateNetwork
(
pObj
,
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vResubsW
,
k
),
pFunc
,
p
->
vLevels
);
Res_UpdateNetwork
(
pObj
,
Vec_VecEntry
(
p
->
vResubsW
,
k
),
pFunc
,
p
->
vLevels
);
p
->
timeUpd
+=
clock
()
-
clk
;
break
;
}
...
...
src/opt/rwr/rwrEva.c
View file @
820a147e
...
...
@@ -263,7 +263,7 @@ Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCu
float
CostBest
;
//, CostCur;
// find the matching class of subgraphs
uTruth
=
0xFFFF
&
*
Cut_CutReadTruth
(
pCut
);
vSubgraphs
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vClasses
,
p
->
pMap
[
uTruth
]
);
vSubgraphs
=
Vec_VecEntry
(
p
->
vClasses
,
p
->
pMap
[
uTruth
]
);
p
->
nSubgraphs
+=
vSubgraphs
->
nSize
;
// determine the best subgraph
GainBest
=
-
1
;
...
...
@@ -509,7 +509,7 @@ void Rwr_ScoresClean( Rwr_Man_t * p )
int
i
,
k
;
for
(
i
=
0
;
i
<
p
->
vClasses
->
nSize
;
i
++
)
{
vSubgraphs
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vClasses
,
i
);
vSubgraphs
=
Vec_VecEntry
(
p
->
vClasses
,
i
);
Vec_PtrForEachEntry
(
Rwr_Node_t
*
,
vSubgraphs
,
pNode
,
k
)
pNode
->
nScore
=
pNode
->
nGain
=
pNode
->
nAdded
=
0
;
}
...
...
@@ -562,7 +562,7 @@ void Rwr_ScoresReport( Rwr_Man_t * p )
{
Perm
[
i
]
=
i
;
Gains
[
i
]
=
0
;
vSubgraphs
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vClasses
,
i
);
vSubgraphs
=
Vec_VecEntry
(
p
->
vClasses
,
i
);
Vec_PtrForEachEntry
(
Rwr_Node_t
*
,
vSubgraphs
,
pNode
,
k
)
Gains
[
i
]
+=
pNode
->
nGain
;
}
...
...
@@ -575,7 +575,7 @@ void Rwr_ScoresReport( Rwr_Man_t * p )
iNew
=
Perm
[
i
];
if
(
Gains
[
iNew
]
==
0
)
break
;
vSubgraphs
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vClasses
,
iNew
);
vSubgraphs
=
Vec_VecEntry
(
p
->
vClasses
,
iNew
);
printf
(
"CLASS %3d: Subgr = %3d. Total gain = %6d. "
,
iNew
,
Vec_PtrSize
(
vSubgraphs
),
Gains
[
iNew
]
);
uTruth
=
(
unsigned
)
p
->
pMapInv
[
iNew
];
Extra_PrintBinary
(
stdout
,
&
uTruth
,
16
);
...
...
src/opt/sim/simSymSat.c
View file @
820a147e
...
...
@@ -63,7 +63,7 @@ int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern )
pMatNonSym
=
(
Extra_BitMat_t
*
)
Vec_PtrEntry
(
p
->
vMatrNonSymms
,
out
);
// go through the remaining variable pairs
vSupport
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
p
->
vSupports
,
out
);
vSupport
=
Vec_VecEntryInt
(
p
->
vSupports
,
out
);
Vec_IntForEachEntry
(
vSupport
,
v
,
Index1
)
Vec_IntForEachEntryStart
(
vSupport
,
u
,
Index2
,
Index1
+
1
)
{
...
...
src/opt/sim/simSymSim.c
View file @
820a147e
...
...
@@ -137,7 +137,7 @@ void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec
int
i
,
w
,
Index
;
// get the matrix, the support, and the simulation info
pMat
=
(
Extra_BitMat_t
*
)
Vec_PtrEntry
(
vMatrsNonSym
,
Output
);
vSupport
=
(
Vec_Int_t
*
)
Vec_VecEntry
(
p
->
vSupports
,
Output
);
vSupport
=
Vec_VecEntryInt
(
p
->
vSupports
,
Output
);
pSupport
=
(
unsigned
*
)
Vec_PtrEntry
(
p
->
vSuppFun
,
Output
);
pSimInfo
=
(
unsigned
*
)
Vec_PtrEntry
(
p
->
vSim
,
pNode
->
Id
);
// generate vectors A1 and A2
...
...
src/opt/sim/simUtils.c
View file @
820a147e
...
...
@@ -639,7 +639,7 @@ clk = clock();
for
(
i
=
0
;
i
<
p
->
nOutputs
;
i
++
)
{
printf
(
"Output %2d :"
,
i
);
Sim_UtilCountPairsOnePrint
(
(
Extra_BitMat_t
*
)
Vec_PtrEntry
(
p
->
vMatrSymms
,
i
),
(
Vec_Int_t
*
)
Vec_VecEntry
(
p
->
vSupports
,
i
)
);
Sim_UtilCountPairsOnePrint
(
(
Extra_BitMat_t
*
)
Vec_PtrEntry
(
p
->
vMatrSymms
,
i
),
Vec_VecEntryInt
(
p
->
vSupports
,
i
)
);
printf
(
"
\n
"
);
}
p
->
timeCount
+=
clock
()
-
clk
;
...
...
@@ -674,8 +674,8 @@ clk = clock();
p
->
nPairsNonSymm
+=
nPairsNonSym
;
continue
;
}
nPairsSym
=
Sim_UtilCountPairsOne
(
(
Extra_BitMat_t
*
)
Vec_PtrEntry
(
p
->
vMatrSymms
,
i
),
(
Vec_Int_t
*
)
Vec_VecEntry
(
p
->
vSupports
,
i
)
);
nPairsNonSym
=
Sim_UtilCountPairsOne
(
(
Extra_BitMat_t
*
)
Vec_PtrEntry
(
p
->
vMatrNonSymms
,
i
),
(
Vec_Int_t
*
)
Vec_VecEntry
(
p
->
vSupports
,
i
)
);
nPairsSym
=
Sim_UtilCountPairsOne
(
(
Extra_BitMat_t
*
)
Vec_PtrEntry
(
p
->
vMatrSymms
,
i
),
Vec_VecEntryInt
(
p
->
vSupports
,
i
)
);
nPairsNonSym
=
Sim_UtilCountPairsOne
(
(
Extra_BitMat_t
*
)
Vec_PtrEntry
(
p
->
vMatrNonSymms
,
i
),
Vec_VecEntryInt
(
p
->
vSupports
,
i
)
);
assert
(
nPairsTotal
>=
nPairsSym
+
nPairsNonSym
);
Vec_IntWriteEntry
(
p
->
vPairsSym
,
i
,
nPairsSym
);
Vec_IntWriteEntry
(
p
->
vPairsNonSym
,
i
,
nPairsNonSym
);
...
...
src/sat/pdr/pdrCore.c
View file @
820a147e
...
...
@@ -133,7 +133,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
Vec_VecForEachLevelStartStop
(
p
->
vClauses
,
vArrayK
,
k
,
1
,
kMax
)
{
Vec_PtrSort
(
vArrayK
,
(
int
(
*
)(
void
))
Pdr_SetCompare
);
vArrayK1
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vClauses
,
k
+
1
);
vArrayK1
=
Vec_VecEntry
(
p
->
vClauses
,
k
+
1
);
Vec_PtrForEachEntry
(
Pdr_Set_t
*
,
vArrayK
,
pCubeK
,
j
)
{
Counter
++
;
...
...
@@ -187,7 +187,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
}
// clean up the last one
vArrayK
=
(
Vec_Ptr_t
*
)
Vec_VecEntry
(
p
->
vClauses
,
kMax
);
vArrayK
=
Vec_VecEntry
(
p
->
vClauses
,
kMax
);
Vec_PtrSort
(
vArrayK
,
(
int
(
*
)(
void
))
Pdr_SetCompare
);
Vec_PtrForEachEntry
(
Pdr_Set_t
*
,
vArrayK
,
pCubeK
,
j
)
{
...
...
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