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
596bbbe6
Commit
596bbbe6
authored
Feb 19, 2012
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Added QuickSort based on 3-way partitioning.
parent
9aab58f6
Hide whitespace changes
Inline
Side-by-side
Showing
8 changed files
with
368 additions
and
241 deletions
+368
-241
src/aig/gia/giaIso.c
+1
-217
src/aig/saig/saigAbsCba.c
+1
-1
src/aig/saig/saigIsoFast.c
+1
-1
src/bool/bdc/bdcSpfd.c
+1
-1
src/misc/util/abc_global.h
+10
-2
src/misc/util/utilSort.c
+352
-17
src/sat/bsat/satProof.c
+1
-1
src/sat/bsat/satSolver2.c
+1
-1
No files found.
src/aig/gia/giaIso.c
View file @
596bbbe6
...
...
@@ -137,222 +137,6 @@ static inline void Gia_IsoSetItem( Gia_IsoMan_t * p, int i, unsigned v ) {
/**Function*************************************************************
Synopsis [QuickSort algorithm as implemented by qsort().]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Abc_QuickSortCompare
(
word
*
p1
,
word
*
p2
)
{
if
(
(
unsigned
)(
*
p1
)
<
(
unsigned
)(
*
p2
)
)
return
-
1
;
if
(
(
unsigned
)(
*
p1
)
>
(
unsigned
)(
*
p2
)
)
return
1
;
return
0
;
}
void
Abc_QuickSort1
(
word
*
pData
,
int
nSize
)
{
int
i
,
fVerify
=
0
;
qsort
(
(
void
*
)
pData
,
nSize
,
sizeof
(
word
),
(
int
(
*
)(
const
void
*
,
const
void
*
))
Abc_QuickSortCompare
);
if
(
fVerify
)
for
(
i
=
1
;
i
<
nSize
;
i
++
)
assert
(
(
unsigned
)
pData
[
i
-
1
]
<=
(
unsigned
)
pData
[
i
]
);
}
/**Function*************************************************************
Synopsis [QuickSort algorithm based on 2/3-way partitioning.]
Description [This code is based on the online presentation
"QuickSort is Optimal" by Robert Sedgewick and Jon Bentley.
http://www.sorting-algorithms.com/static/QuicksortIsOptimal.pdf
The first 32-bits of the input data contain values to be compared.
The last 32-bits contain the user's data. When sorting is finished,
the 64-bit words are ordered in the increasing order of their value ]
SideEffects []
SeeAlso []
***********************************************************************/
#define ABC_SWAP(Type, a, b) { Type t = a; a = b; b = t; }
static
inline
void
Iso_SelectSort
(
word
*
pData
,
int
nSize
)
{
int
i
,
j
,
best_i
;
for
(
i
=
0
;
i
<
nSize
-
1
;
i
++
)
{
best_i
=
i
;
for
(
j
=
i
+
1
;
j
<
nSize
;
j
++
)
if
(
(
unsigned
)
pData
[
j
]
<
(
unsigned
)
pData
[
best_i
]
)
best_i
=
j
;
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
best_i
]
);
}
}
void
Abc_QuickSort2_rec
(
word
*
pData
,
int
l
,
int
r
)
{
word
v
=
pData
[
r
];
int
i
=
l
-
1
,
j
=
r
;
if
(
l
>=
r
)
return
;
assert
(
l
<
r
);
if
(
r
-
l
<
10
)
{
Iso_SelectSort
(
pData
+
l
,
r
-
l
+
1
);
return
;
}
while
(
1
)
{
while
(
(
unsigned
)
pData
[
++
i
]
<
(
unsigned
)
v
);
while
(
(
unsigned
)
v
<
(
unsigned
)
pData
[
--
j
]
)
if
(
j
==
l
)
break
;
if
(
i
>=
j
)
break
;
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
j
]
);
}
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
r
]
);
Abc_QuickSort2_rec
(
pData
,
l
,
i
-
1
);
Abc_QuickSort2_rec
(
pData
,
i
+
1
,
r
);
}
void
Abc_QuickSort3_rec
(
word
*
pData
,
int
l
,
int
r
)
{
word
v
=
pData
[
r
];
int
k
,
i
=
l
-
1
,
j
=
r
,
p
=
l
-
1
,
q
=
r
;
if
(
l
>=
r
)
return
;
assert
(
l
<
r
);
if
(
r
-
l
<
10
)
{
Iso_SelectSort
(
pData
+
l
,
r
-
l
+
1
);
return
;
}
while
(
1
)
{
while
(
(
unsigned
)
pData
[
++
i
]
<
(
unsigned
)
v
);
while
(
(
unsigned
)
v
<
(
unsigned
)
pData
[
--
j
]
)
if
(
j
==
l
)
break
;
if
(
i
>=
j
)
break
;
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
j
]
);
if
(
(
unsigned
)
pData
[
i
]
==
(
unsigned
)
v
)
{
p
++
;
ABC_SWAP
(
word
,
pData
[
p
],
pData
[
i
]
);
}
if
(
(
unsigned
)
v
==
(
unsigned
)
pData
[
j
]
)
{
q
--
;
ABC_SWAP
(
word
,
pData
[
j
],
pData
[
q
]
);
}
}
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
r
]
);
j
=
i
-
1
;
i
=
i
+
1
;
for
(
k
=
l
;
k
<
p
;
k
++
,
j
--
)
ABC_SWAP
(
word
,
pData
[
k
],
pData
[
j
]
);
for
(
k
=
r
-
1
;
k
>
q
;
k
--
,
i
++
)
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
k
]
);
Abc_QuickSort3_rec
(
pData
,
l
,
j
);
Abc_QuickSort3_rec
(
pData
,
i
,
r
);
}
void
Abc_QuickSort2
(
word
*
pData
,
int
nSize
)
{
int
i
,
fVerify
=
0
;
Abc_QuickSort2_rec
(
pData
,
0
,
nSize
-
1
);
if
(
fVerify
)
for
(
i
=
1
;
i
<
nSize
;
i
++
)
assert
(
(
unsigned
)
pData
[
i
-
1
]
<=
(
unsigned
)
pData
[
i
]
);
}
void
Abc_QuickSort3
(
word
*
pData
,
int
nSize
)
{
int
i
,
fVerify
=
0
;
Abc_QuickSort3_rec
(
pData
,
0
,
nSize
-
1
);
if
(
fVerify
)
for
(
i
=
1
;
i
<
nSize
;
i
++
)
assert
(
(
unsigned
)
pData
[
i
-
1
]
<=
(
unsigned
)
pData
[
i
]
);
}
/**Function*************************************************************
Synopsis [Wrapper around QuickSort to sort entries based on cost.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Abc_QuickSortCostData
(
int
*
pCosts
,
int
nSize
,
word
*
pData
,
int
*
pResult
)
{
int
i
;
for
(
i
=
0
;
i
<
nSize
;
i
++
)
pData
[
i
]
=
((
word
)
i
<<
32
)
|
pCosts
[
i
];
Abc_QuickSort3
(
pData
,
nSize
);
for
(
i
=
0
;
i
<
nSize
;
i
++
)
pResult
[
i
]
=
(
int
)(
pData
[
i
]
>>
32
);
}
int
*
Abc_QuickSortCost
(
int
*
pCosts
,
int
nSize
)
{
word
*
pData
=
ABC_ALLOC
(
word
,
nSize
);
int
*
pResult
=
ABC_ALLOC
(
int
,
nSize
);
Abc_QuickSortCostData
(
pCosts
,
nSize
,
pData
,
pResult
);
ABC_FREE
(
pData
);
return
pResult
;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Abc_QuickSortTest
()
{
int
nSize
=
10000000
;
int
fVerbose
=
0
;
word
*
pData1
,
*
pData2
;
int
i
,
clk
=
clock
();
// generate numbers
pData1
=
ABC_ALLOC
(
word
,
nSize
);
pData2
=
ABC_ALLOC
(
word
,
nSize
);
srand
(
1111
);
for
(
i
=
0
;
i
<
nSize
;
i
++
)
pData2
[
i
]
=
pData1
[
i
]
=
((
word
)
i
<<
32
)
|
rand
();
Abc_PrintTime
(
1
,
"Prepare "
,
clock
()
-
clk
);
// perform sorting
clk
=
clock
();
Abc_QuickSort3
(
pData1
,
nSize
);
Abc_PrintTime
(
1
,
"Sort new"
,
clock
()
-
clk
);
// print the result
if
(
fVerbose
)
{
for
(
i
=
0
;
i
<
nSize
;
i
++
)
printf
(
"(%d,%d) "
,
(
int
)(
pData1
[
i
]
>>
32
),
(
int
)
pData1
[
i
]
);
printf
(
"
\n
"
);
}
// create new numbers
clk
=
clock
();
Abc_QuickSort1
(
pData2
,
nSize
);
Abc_PrintTime
(
1
,
"Sort old"
,
clock
()
-
clk
);
// print the result
if
(
fVerbose
)
{
for
(
i
=
0
;
i
<
nSize
;
i
++
)
printf
(
"(%d,%d) "
,
(
int
)(
pData2
[
i
]
>>
32
),
(
int
)
pData2
[
i
]
);
printf
(
"
\n
"
);
}
ABC_FREE
(
pData1
);
ABC_FREE
(
pData2
);
}
/**Function*************************************************************
Synopsis []
Description []
...
...
@@ -619,7 +403,7 @@ void Gia_IsoSort( Gia_IsoMan_t * p )
}
// sort objects
clk
=
clock
();
Abc_QuickSort3
(
p
->
pStoreW
+
iBegin
,
nSize
);
Abc_QuickSort3
(
p
->
pStoreW
+
iBegin
,
nSize
,
0
);
p
->
timeSort
+=
clock
()
-
clk
;
// divide into new classes
iBeginOld
=
iBegin
;
...
...
src/aig/saig/saigAbsCba.c
View file @
596bbbe6
...
...
@@ -113,7 +113,7 @@ Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_I
Vec_IntForEachEntry
(
vAbsFfsToAdd
,
Entry
,
i
)
Vec_IntPush
(
vFlopAddCosts
,
-
Vec_IntEntry
(
vFlopCosts
,
Entry
)
);
// sort the flops
pPerm
=
Abc_SortCost
(
Vec_IntArray
(
vFlopAddCosts
),
Vec_IntSize
(
vFlopAddCosts
)
);
pPerm
=
Abc_
Merge
SortCost
(
Vec_IntArray
(
vFlopAddCosts
),
Vec_IntSize
(
vFlopAddCosts
)
);
// shrink the array
vFfsToAddBest
=
Vec_IntAlloc
(
nFfsToSelect
);
for
(
i
=
0
;
i
<
nFfsToSelect
;
i
++
)
...
...
src/aig/saig/saigIsoFast.c
View file @
596bbbe6
...
...
@@ -219,7 +219,7 @@ Vec_Int_t * Iso_StoCollectInfo( Iso_Sto_t * p, Aig_Obj_t * pPo )
// printf( "%d ", Vec_IntSize(p->vVisited) );
// sort the costs in the increasing order
pPerm
=
Abc_SortCost
(
Vec_IntArray
(
p
->
vVisited
),
Vec_IntSize
(
p
->
vVisited
)
);
pPerm
=
Abc_
Merge
SortCost
(
Vec_IntArray
(
p
->
vVisited
),
Vec_IntSize
(
p
->
vVisited
)
);
assert
(
Vec_IntEntry
(
p
->
vVisited
,
pPerm
[
0
])
<=
Vec_IntEntry
(
p
->
vVisited
,
pPerm
[
Vec_IntSize
(
p
->
vVisited
)
-
1
])
);
// create information
...
...
src/bool/bdc/bdcSpfd.c
View file @
596bbbe6
...
...
@@ -299,7 +299,7 @@ Bdc_SpfdPrint( pNode + i, 1, vLevels, Truth );
goto
cleanup
;
}
}
pPerm
=
Abc_SortCost
(
Vec_IntArray
(
vWeight
),
c
);
pPerm
=
Abc_
Merge
SortCost
(
Vec_IntArray
(
vWeight
),
c
);
assert
(
Vec_IntEntry
(
vWeight
,
pPerm
[
0
])
<=
Vec_IntEntry
(
vWeight
,
pPerm
[
c
-
1
])
);
printf
(
"Best SPFD = %d.
\n
"
,
Vec_IntEntry
(
vWeight
,
pPerm
[
c
-
1
])
);
...
...
src/misc/util/abc_global.h
View file @
596bbbe6
...
...
@@ -198,6 +198,8 @@ typedef ABC_UINT64_T word;
#define ABC_INFINITY (100000000)
#define ABC_SWAP(Type, a, b) { Type t = a; a = b; b = t; }
#define ABC_PRT(a,t) (printf("%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTr(a,t) (printf("%s = ", (a)), printf("%7.2f sec\r", (float)(t)/(float)(CLOCKS_PER_SEC)))
#define ABC_PRTn(a,t) (printf("%s = ", (a)), printf("%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC)))
...
...
@@ -322,8 +324,14 @@ static inline int Abc_PrimeCudd( unsigned int p )
}
// end of Cudd_Prime
extern
void
Abc_Sort
(
int
*
pInput
,
int
nSize
);
extern
int
*
Abc_SortCost
(
int
*
pCosts
,
int
nSize
);
// sorting
extern
void
Abc_MergeSort
(
int
*
pInput
,
int
nSize
);
extern
int
*
Abc_MergeSortCost
(
int
*
pCosts
,
int
nSize
);
extern
void
Abc_QuickSort1
(
word
*
pData
,
int
nSize
,
int
fDecrement
);
extern
void
Abc_QuickSort2
(
word
*
pData
,
int
nSize
,
int
fDecrement
);
extern
void
Abc_QuickSort3
(
word
*
pData
,
int
nSize
,
int
fDecrement
);
extern
void
Abc_QuickSortCostData
(
int
*
pCosts
,
int
nSize
,
int
fDecrement
,
word
*
pData
,
int
*
pResult
);
extern
int
*
Abc_QuickSortCost
(
int
*
pCosts
,
int
nSize
,
int
fDecrement
);
ABC_NAMESPACE_HEADER_END
...
...
src/misc/util/utilSort.c
View file @
596bbbe6
...
...
@@ -126,7 +126,7 @@ void Abc_Sort_rec( int * pInBeg, int * pInEnd, int * pOutBeg )
SeeAlso []
***********************************************************************/
void
Abc_Sort
(
int
*
pInput
,
int
nSize
)
void
Abc_
Merge
Sort
(
int
*
pInput
,
int
nSize
)
{
int
*
pOutput
;
if
(
nSize
<
2
)
...
...
@@ -149,7 +149,7 @@ void Abc_Sort( int * pInput, int nSize )
SeeAlso []
***********************************************************************/
void
Abc_SortCostMerge
(
int
*
p1Beg
,
int
*
p1End
,
int
*
p2Beg
,
int
*
p2End
,
int
*
pOut
)
void
Abc_
Merge
SortCostMerge
(
int
*
p1Beg
,
int
*
p1End
,
int
*
p2Beg
,
int
*
p2End
,
int
*
pOut
)
{
int
nEntries
=
(
p1End
-
p1Beg
)
+
(
p2End
-
p2Beg
);
int
*
pOutBeg
=
pOut
;
...
...
@@ -180,7 +180,7 @@ void Abc_SortCostMerge( int * p1Beg, int * p1End, int * p2Beg, int * p2End, int
SeeAlso []
***********************************************************************/
void
Abc_SortCost_rec
(
int
*
pInBeg
,
int
*
pInEnd
,
int
*
pOutBeg
)
void
Abc_
Merge
SortCost_rec
(
int
*
pInBeg
,
int
*
pInEnd
,
int
*
pOutBeg
)
{
int
nSize
=
(
pInEnd
-
pInBeg
)
/
2
;
assert
(
nSize
>
0
);
...
...
@@ -217,9 +217,9 @@ void Abc_SortCost_rec( int * pInBeg, int * pInEnd, int * pOutBeg )
}
else
{
Abc_SortCost_rec
(
pInBeg
,
pInBeg
+
2
*
(
nSize
/
2
),
pOutBeg
);
Abc_SortCost_rec
(
pInBeg
+
2
*
(
nSize
/
2
),
pInEnd
,
pOutBeg
+
2
*
(
nSize
/
2
)
);
Abc_SortCostMerge
(
pInBeg
,
pInBeg
+
2
*
(
nSize
/
2
),
pInBeg
+
2
*
(
nSize
/
2
),
pInEnd
,
pOutBeg
);
Abc_
Merge
SortCost_rec
(
pInBeg
,
pInBeg
+
2
*
(
nSize
/
2
),
pOutBeg
);
Abc_
Merge
SortCost_rec
(
pInBeg
+
2
*
(
nSize
/
2
),
pInEnd
,
pOutBeg
+
2
*
(
nSize
/
2
)
);
Abc_
Merge
SortCostMerge
(
pInBeg
,
pInBeg
+
2
*
(
nSize
/
2
),
pInBeg
+
2
*
(
nSize
/
2
),
pInEnd
,
pOutBeg
);
memcpy
(
pInBeg
,
pOutBeg
,
sizeof
(
int
)
*
2
*
nSize
);
}
}
...
...
@@ -235,7 +235,7 @@ void Abc_SortCost_rec( int * pInBeg, int * pInEnd, int * pOutBeg )
SeeAlso []
***********************************************************************/
int
*
Abc_SortCost
(
int
*
pCosts
,
int
nSize
)
int
*
Abc_
Merge
SortCost
(
int
*
pCosts
,
int
nSize
)
{
int
i
,
*
pResult
,
*
pInput
,
*
pOutput
;
pResult
=
(
int
*
)
calloc
(
sizeof
(
int
),
nSize
);
...
...
@@ -245,7 +245,7 @@ int * Abc_SortCost( int * pCosts, int nSize )
pOutput
=
(
int
*
)
malloc
(
sizeof
(
int
)
*
2
*
nSize
);
for
(
i
=
0
;
i
<
nSize
;
i
++
)
pInput
[
2
*
i
]
=
i
,
pInput
[
2
*
i
+
1
]
=
pCosts
[
i
];
Abc_SortCost_rec
(
pInput
,
pInput
+
2
*
nSize
,
pOutput
);
Abc_
Merge
SortCost_rec
(
pInput
,
pInput
+
2
*
nSize
,
pOutput
);
for
(
i
=
0
;
i
<
nSize
;
i
++
)
pResult
[
i
]
=
pInput
[
2
*
i
];
free
(
pOutput
);
...
...
@@ -269,7 +269,7 @@ int * Abc_SortCost( int * pCosts, int nSize )
SeeAlso []
***********************************************************************/
void Abc_SortCostMerge( int * p1Beg, int * p1End, int * p2Beg, int * p2End, int * pOut, int * pCost )
void Abc_
Merge
SortCostMerge( int * p1Beg, int * p1End, int * p2Beg, int * p2End, int * pOut, int * pCost )
{
int nEntries = (p1End - p1Beg) + (p2End - p2Beg);
int * pOutBeg = pOut;
...
...
@@ -300,7 +300,7 @@ void Abc_SortCostMerge( int * p1Beg, int * p1End, int * p2Beg, int * p2End, int
SeeAlso []
***********************************************************************/
void Abc_SortCost_rec( int * pInBeg, int * pInEnd, int * pOutBeg, int * pCost )
void Abc_
Merge
SortCost_rec( int * pInBeg, int * pInEnd, int * pOutBeg, int * pCost )
{
int nSize = pInEnd - pInBeg;
assert( nSize > 0 );
...
...
@@ -331,9 +331,9 @@ void Abc_SortCost_rec( int * pInBeg, int * pInEnd, int * pOutBeg, int * pCost )
}
else
{
Abc_SortCost_rec( pInBeg, pInBeg + nSize/2, pOutBeg, pCost );
Abc_SortCost_rec( pInBeg + nSize/2, pInEnd, pOutBeg + nSize/2, pCost );
Abc_SortCostMerge( pInBeg, pInBeg + nSize/2, pInBeg + nSize/2, pInEnd, pOutBeg, pCost );
Abc_
Merge
SortCost_rec( pInBeg, pInBeg + nSize/2, pOutBeg, pCost );
Abc_
Merge
SortCost_rec( pInBeg + nSize/2, pInEnd, pOutBeg + nSize/2, pCost );
Abc_
Merge
SortCostMerge( pInBeg, pInBeg + nSize/2, pInBeg + nSize/2, pInEnd, pOutBeg, pCost );
memcpy( pInBeg, pOutBeg, sizeof(int) * nSize );
}
}
...
...
@@ -349,7 +349,7 @@ void Abc_SortCost_rec( int * pInBeg, int * pInEnd, int * pOutBeg, int * pCost )
SeeAlso []
***********************************************************************/
int * Abc_SortCost( int * pCosts, int nSize )
int * Abc_
Merge
SortCost( int * pCosts, int nSize )
{
int i, * pInput, * pOutput;
pInput = (int *) malloc( sizeof(int) * nSize );
...
...
@@ -358,7 +358,7 @@ int * Abc_SortCost( int * pCosts, int nSize )
if ( nSize < 2 )
return pInput;
pOutput = (int *) malloc( sizeof(int) * nSize );
Abc_SortCost_rec( pInput, pInput + nSize, pOutput, pCosts );
Abc_
Merge
SortCost_rec( pInput, pInput + nSize, pOutput, pCosts );
free( pOutput );
return pInput;
}
...
...
@@ -413,7 +413,7 @@ void Abc_SortTest()
if
(
fUseCost
)
{
clk
=
clock
();
pPerm
=
Abc_SortCost
(
pArray
,
nSize
);
pPerm
=
Abc_
Merge
SortCost
(
pArray
,
nSize
);
Abc_PrintTime
(
1
,
"New sort"
,
clock
()
-
clk
);
// check
for
(
i
=
1
;
i
<
nSize
;
i
++
)
...
...
@@ -423,7 +423,7 @@ void Abc_SortTest()
else
{
clk
=
clock
();
Abc_Sort
(
pArray
,
nSize
);
Abc_
Merge
Sort
(
pArray
,
nSize
);
Abc_PrintTime
(
1
,
"New sort"
,
clock
()
-
clk
);
// check
for
(
i
=
1
;
i
<
nSize
;
i
++
)
...
...
@@ -443,6 +443,341 @@ void Abc_SortTest()
free
(
pArray
);
}
/**Function*************************************************************
Synopsis [QuickSort algorithm as implemented by qsort().]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Abc_QuickSort1CompareInc
(
word
*
p1
,
word
*
p2
)
{
if
(
(
unsigned
)(
*
p1
)
<
(
unsigned
)(
*
p2
)
)
return
-
1
;
if
(
(
unsigned
)(
*
p1
)
>
(
unsigned
)(
*
p2
)
)
return
1
;
return
0
;
}
int
Abc_QuickSort1CompareDec
(
word
*
p1
,
word
*
p2
)
{
if
(
(
unsigned
)(
*
p1
)
>
(
unsigned
)(
*
p2
)
)
return
-
1
;
if
(
(
unsigned
)(
*
p1
)
<
(
unsigned
)(
*
p2
)
)
return
1
;
return
0
;
}
void
Abc_QuickSort1
(
word
*
pData
,
int
nSize
,
int
fDecrement
)
{
int
i
,
fVerify
=
0
;
if
(
fDecrement
)
{
qsort
(
(
void
*
)
pData
,
nSize
,
sizeof
(
word
),
(
int
(
*
)(
const
void
*
,
const
void
*
))
Abc_QuickSort1CompareDec
);
if
(
fVerify
)
for
(
i
=
1
;
i
<
nSize
;
i
++
)
assert
(
(
unsigned
)
pData
[
i
-
1
]
>=
(
unsigned
)
pData
[
i
]
);
}
else
{
qsort
(
(
void
*
)
pData
,
nSize
,
sizeof
(
word
),
(
int
(
*
)(
const
void
*
,
const
void
*
))
Abc_QuickSort1CompareInc
);
if
(
fVerify
)
for
(
i
=
1
;
i
<
nSize
;
i
++
)
assert
(
(
unsigned
)
pData
[
i
-
1
]
<=
(
unsigned
)
pData
[
i
]
);
}
}
/**Function*************************************************************
Synopsis [QuickSort algorithm based on 2/3-way partitioning.]
Description [This code is based on the online presentation
"QuickSort is Optimal" by Robert Sedgewick and Jon Bentley.
http://www.sorting-algorithms.com/static/QuicksortIsOptimal.pdf
The first 32-bits of the input data contain values to be compared.
The last 32-bits contain the user's data. When sorting is finished,
the 64-bit words are ordered in the increasing order of their value ]
SideEffects []
SeeAlso []
***********************************************************************/
static
inline
void
Iso_SelectSortInc
(
word
*
pData
,
int
nSize
)
{
int
i
,
j
,
best_i
;
for
(
i
=
0
;
i
<
nSize
-
1
;
i
++
)
{
best_i
=
i
;
for
(
j
=
i
+
1
;
j
<
nSize
;
j
++
)
if
(
(
unsigned
)
pData
[
j
]
<
(
unsigned
)
pData
[
best_i
]
)
best_i
=
j
;
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
best_i
]
);
}
}
static
inline
void
Iso_SelectSortDec
(
word
*
pData
,
int
nSize
)
{
int
i
,
j
,
best_i
;
for
(
i
=
0
;
i
<
nSize
-
1
;
i
++
)
{
best_i
=
i
;
for
(
j
=
i
+
1
;
j
<
nSize
;
j
++
)
if
(
(
unsigned
)
pData
[
j
]
>
(
unsigned
)
pData
[
best_i
]
)
best_i
=
j
;
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
best_i
]
);
}
}
void
Abc_QuickSort2Inc_rec
(
word
*
pData
,
int
l
,
int
r
)
{
word
v
=
pData
[
r
];
int
i
=
l
-
1
,
j
=
r
;
if
(
l
>=
r
)
return
;
assert
(
l
<
r
);
if
(
r
-
l
<
10
)
{
Iso_SelectSortInc
(
pData
+
l
,
r
-
l
+
1
);
return
;
}
while
(
1
)
{
while
(
(
unsigned
)
pData
[
++
i
]
<
(
unsigned
)
v
);
while
(
(
unsigned
)
v
<
(
unsigned
)
pData
[
--
j
]
)
if
(
j
==
l
)
break
;
if
(
i
>=
j
)
break
;
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
j
]
);
}
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
r
]
);
Abc_QuickSort2Inc_rec
(
pData
,
l
,
i
-
1
);
Abc_QuickSort2Inc_rec
(
pData
,
i
+
1
,
r
);
}
void
Abc_QuickSort2Dec_rec
(
word
*
pData
,
int
l
,
int
r
)
{
word
v
=
pData
[
r
];
int
i
=
l
-
1
,
j
=
r
;
if
(
l
>=
r
)
return
;
assert
(
l
<
r
);
if
(
r
-
l
<
10
)
{
Iso_SelectSortDec
(
pData
+
l
,
r
-
l
+
1
);
return
;
}
while
(
1
)
{
while
(
(
unsigned
)
pData
[
++
i
]
>
(
unsigned
)
v
);
while
(
(
unsigned
)
v
>
(
unsigned
)
pData
[
--
j
]
)
if
(
j
==
l
)
break
;
if
(
i
>=
j
)
break
;
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
j
]
);
}
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
r
]
);
Abc_QuickSort2Dec_rec
(
pData
,
l
,
i
-
1
);
Abc_QuickSort2Dec_rec
(
pData
,
i
+
1
,
r
);
}
void
Abc_QuickSort3Inc_rec
(
word
*
pData
,
int
l
,
int
r
)
{
word
v
=
pData
[
r
];
int
k
,
i
=
l
-
1
,
j
=
r
,
p
=
l
-
1
,
q
=
r
;
if
(
l
>=
r
)
return
;
assert
(
l
<
r
);
if
(
r
-
l
<
10
)
{
Iso_SelectSortInc
(
pData
+
l
,
r
-
l
+
1
);
return
;
}
while
(
1
)
{
while
(
(
unsigned
)
pData
[
++
i
]
<
(
unsigned
)
v
);
while
(
(
unsigned
)
v
<
(
unsigned
)
pData
[
--
j
]
)
if
(
j
==
l
)
break
;
if
(
i
>=
j
)
break
;
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
j
]
);
if
(
(
unsigned
)
pData
[
i
]
==
(
unsigned
)
v
)
{
p
++
;
ABC_SWAP
(
word
,
pData
[
p
],
pData
[
i
]
);
}
if
(
(
unsigned
)
v
==
(
unsigned
)
pData
[
j
]
)
{
q
--
;
ABC_SWAP
(
word
,
pData
[
j
],
pData
[
q
]
);
}
}
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
r
]
);
j
=
i
-
1
;
i
=
i
+
1
;
for
(
k
=
l
;
k
<
p
;
k
++
,
j
--
)
ABC_SWAP
(
word
,
pData
[
k
],
pData
[
j
]
);
for
(
k
=
r
-
1
;
k
>
q
;
k
--
,
i
++
)
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
k
]
);
Abc_QuickSort3Inc_rec
(
pData
,
l
,
j
);
Abc_QuickSort3Inc_rec
(
pData
,
i
,
r
);
}
void
Abc_QuickSort3Dec_rec
(
word
*
pData
,
int
l
,
int
r
)
{
word
v
=
pData
[
r
];
int
k
,
i
=
l
-
1
,
j
=
r
,
p
=
l
-
1
,
q
=
r
;
if
(
l
>=
r
)
return
;
assert
(
l
<
r
);
if
(
r
-
l
<
10
)
{
Iso_SelectSortDec
(
pData
+
l
,
r
-
l
+
1
);
return
;
}
while
(
1
)
{
while
(
(
unsigned
)
pData
[
++
i
]
>
(
unsigned
)
v
);
while
(
(
unsigned
)
v
>
(
unsigned
)
pData
[
--
j
]
)
if
(
j
==
l
)
break
;
if
(
i
>=
j
)
break
;
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
j
]
);
if
(
(
unsigned
)
pData
[
i
]
==
(
unsigned
)
v
)
{
p
++
;
ABC_SWAP
(
word
,
pData
[
p
],
pData
[
i
]
);
}
if
(
(
unsigned
)
v
==
(
unsigned
)
pData
[
j
]
)
{
q
--
;
ABC_SWAP
(
word
,
pData
[
j
],
pData
[
q
]
);
}
}
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
r
]
);
j
=
i
-
1
;
i
=
i
+
1
;
for
(
k
=
l
;
k
<
p
;
k
++
,
j
--
)
ABC_SWAP
(
word
,
pData
[
k
],
pData
[
j
]
);
for
(
k
=
r
-
1
;
k
>
q
;
k
--
,
i
++
)
ABC_SWAP
(
word
,
pData
[
i
],
pData
[
k
]
);
Abc_QuickSort3Dec_rec
(
pData
,
l
,
j
);
Abc_QuickSort3Dec_rec
(
pData
,
i
,
r
);
}
void
Abc_QuickSort2
(
word
*
pData
,
int
nSize
,
int
fDecrement
)
{
int
i
,
fVerify
=
0
;
if
(
fDecrement
)
{
Abc_QuickSort2Dec_rec
(
pData
,
0
,
nSize
-
1
);
if
(
fVerify
)
for
(
i
=
1
;
i
<
nSize
;
i
++
)
assert
(
(
unsigned
)
pData
[
i
-
1
]
>=
(
unsigned
)
pData
[
i
]
);
}
else
{
Abc_QuickSort2Inc_rec
(
pData
,
0
,
nSize
-
1
);
if
(
fVerify
)
for
(
i
=
1
;
i
<
nSize
;
i
++
)
assert
(
(
unsigned
)
pData
[
i
-
1
]
<=
(
unsigned
)
pData
[
i
]
);
}
}
void
Abc_QuickSort3
(
word
*
pData
,
int
nSize
,
int
fDecrement
)
{
int
i
,
fVerify
=
0
;
if
(
fDecrement
)
{
Abc_QuickSort2Dec_rec
(
pData
,
0
,
nSize
-
1
);
if
(
fVerify
)
for
(
i
=
1
;
i
<
nSize
;
i
++
)
assert
(
(
unsigned
)
pData
[
i
-
1
]
>=
(
unsigned
)
pData
[
i
]
);
}
else
{
Abc_QuickSort2Inc_rec
(
pData
,
0
,
nSize
-
1
);
if
(
fVerify
)
for
(
i
=
1
;
i
<
nSize
;
i
++
)
assert
(
(
unsigned
)
pData
[
i
-
1
]
<=
(
unsigned
)
pData
[
i
]
);
}
}
/**Function*************************************************************
Synopsis [Wrapper around QuickSort to sort entries based on cost.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Abc_QuickSortCostData
(
int
*
pCosts
,
int
nSize
,
int
fDecrement
,
word
*
pData
,
int
*
pResult
)
{
int
i
;
for
(
i
=
0
;
i
<
nSize
;
i
++
)
pData
[
i
]
=
((
word
)
i
<<
32
)
|
pCosts
[
i
];
Abc_QuickSort3
(
pData
,
nSize
,
fDecrement
);
for
(
i
=
0
;
i
<
nSize
;
i
++
)
pResult
[
i
]
=
(
int
)(
pData
[
i
]
>>
32
);
}
int
*
Abc_QuickSortCost
(
int
*
pCosts
,
int
nSize
,
int
fDecrement
)
{
word
*
pData
=
ABC_ALLOC
(
word
,
nSize
);
int
*
pResult
=
ABC_ALLOC
(
int
,
nSize
);
Abc_QuickSortCostData
(
pCosts
,
nSize
,
fDecrement
,
pData
,
pResult
);
ABC_FREE
(
pData
);
return
pResult
;
}
// extern void Abc_QuickSortTest();
// Abc_QuickSortTest();
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Abc_QuickSortTest
()
{
int
nSize
=
1000000
;
int
fVerbose
=
0
;
word
*
pData1
,
*
pData2
;
int
i
,
clk
=
clock
();
// generate numbers
pData1
=
ABC_ALLOC
(
word
,
nSize
);
pData2
=
ABC_ALLOC
(
word
,
nSize
);
srand
(
1111
);
for
(
i
=
0
;
i
<
nSize
;
i
++
)
pData2
[
i
]
=
pData1
[
i
]
=
((
word
)
i
<<
32
)
|
rand
();
Abc_PrintTime
(
1
,
"Prepare "
,
clock
()
-
clk
);
// perform sorting
clk
=
clock
();
Abc_QuickSort3
(
pData1
,
nSize
,
1
);
Abc_PrintTime
(
1
,
"Sort new"
,
clock
()
-
clk
);
// print the result
if
(
fVerbose
)
{
for
(
i
=
0
;
i
<
nSize
;
i
++
)
printf
(
"(%d,%d) "
,
(
int
)(
pData1
[
i
]
>>
32
),
(
int
)
pData1
[
i
]
);
printf
(
"
\n
"
);
}
// create new numbers
clk
=
clock
();
Abc_QuickSort1
(
pData2
,
nSize
,
1
);
Abc_PrintTime
(
1
,
"Sort old"
,
clock
()
-
clk
);
// print the result
if
(
fVerbose
)
{
for
(
i
=
0
;
i
<
nSize
;
i
++
)
printf
(
"(%d,%d) "
,
(
int
)(
pData2
[
i
]
>>
32
),
(
int
)
pData2
[
i
]
);
printf
(
"
\n
"
);
}
ABC_FREE
(
pData1
);
ABC_FREE
(
pData2
);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
...
...
src/sat/bsat/satProof.c
View file @
596bbbe6
...
...
@@ -155,7 +155,7 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int f
Vec_IntFree
(
vStack
);
// Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk );
clk
=
clock
();
Abc_Sort
(
Vec_IntArray
(
vUsed
),
Vec_IntSize
(
vUsed
)
);
Abc_
Merge
Sort
(
Vec_IntArray
(
vUsed
),
Vec_IntSize
(
vUsed
)
);
// Abc_PrintTime( 1, "Postprocessing with sorting time", clock() - clk );
// verify topological order
if
(
fVerify
)
...
...
src/sat/bsat/satSolver2.c
View file @
596bbbe6
...
...
@@ -1416,7 +1416,7 @@ void sat_solver2_reducedb(sat_solver2* s)
// preserve 1/10 of most active clauses
pClaAct
=
veci_begin
(
&
s
->
claActs
)
+
1
;
nClaAct
=
veci_size
(
&
s
->
claActs
)
-
1
;
pPerm
=
Abc_SortCost
(
pClaAct
,
nClaAct
);
pPerm
=
Abc_
Merge
SortCost
(
pClaAct
,
nClaAct
);
assert
(
pClaAct
[
pPerm
[
0
]]
<=
pClaAct
[
pPerm
[
nClaAct
-
1
]]
);
ActCutOff
=
pClaAct
[
pPerm
[
nClaAct
*
9
/
10
]];
ABC_FREE
(
pPerm
);
...
...
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