diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-02-19 13:16:51 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-02-19 13:16:51 -0800 |
| commit | 596bbbe6dc3f8311a5166269d651d50ec6b2dff8 (patch) | |
| tree | bb8c164a318fba0ce751d7a2ca68c004b646ea78 /src/sat/bsat | |
| parent | 9aab58f6013a2f7973ac8fd5ac017f4f71a82cef (diff) | |
| download | abc-596bbbe6dc3f8311a5166269d651d50ec6b2dff8.tar.gz abc-596bbbe6dc3f8311a5166269d651d50ec6b2dff8.tar.bz2 abc-596bbbe6dc3f8311a5166269d651d50ec6b2dff8.zip | |
Added QuickSort based on 3-way partitioning.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satProof.c | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 223c830b..d61dea4f 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -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_MergeSort( Vec_IntArray(vUsed), Vec_IntSize(vUsed) ); // Abc_PrintTime( 1, "Postprocessing with sorting time", clock() - clk ); // verify topological order if ( fVerify ) diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index a17c4762..484c5f8f 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -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_MergeSortCost( pClaAct, nClaAct ); assert( pClaAct[pPerm[0]] <= pClaAct[pPerm[nClaAct-1]] ); ActCutOff = pClaAct[pPerm[nClaAct*9/10]]; ABC_FREE( pPerm ); |