#include "msatInt.h"
Go to the source code of this file.
Functions | |
static int | Msat_SolverSortCompare (Msat_Clause_t **ppC1, Msat_Clause_t **ppC2) |
static double | drand (double seed) |
static int | irand (double seed, int size) |
static void | Msat_SolverSort (Msat_Clause_t **array, int size, double seed) |
void | Msat_SolverSortDB (Msat_Solver_t *p) |
void | Msat_SolverSortSelection (Msat_Clause_t **array, int size) |
static double drand | ( | double | seed | ) | [static] |
Definition at line 30 of file msatSort.c.
static int irand | ( | double | seed, | |
int | size | |||
) | [static] |
Definition at line 38 of file msatSort.c.
void Msat_SolverSort | ( | Msat_Clause_t ** | array, | |
int | size, | |||
double | seed | |||
) | [static] |
Function*************************************************************
Synopsis [The original MiniSat sorting procedure.]
Description [This procedure is used to preserve trace-equivalence with the orignal C++ implemenation of the solver.]
SideEffects []
SeeAlso []
Definition at line 144 of file msatSort.c.
00145 { 00146 if (size <= 15) 00147 Msat_SolverSortSelection( array, size ); 00148 else 00149 { 00150 Msat_Clause_t * pivot = array[irand(seed, size)]; 00151 Msat_Clause_t * tmp; 00152 int i = -1; 00153 int j = size; 00154 00155 for(;;) 00156 { 00157 do i++; while( Msat_ClauseReadActivity(array[i]) < Msat_ClauseReadActivity(pivot) ); 00158 do j--; while( Msat_ClauseReadActivity(pivot) < Msat_ClauseReadActivity(array[j]) ); 00159 00160 if ( i >= j ) break; 00161 00162 tmp = array[i]; array[i] = array[j]; array[j] = tmp; 00163 } 00164 Msat_SolverSort(array , i , seed); 00165 Msat_SolverSort(&array[i], size-i, seed); 00166 } 00167 }
int Msat_SolverSortCompare | ( | Msat_Clause_t ** | ppC1, | |
Msat_Clause_t ** | ppC2 | |||
) | [static] |
CFile****************************************************************
FileName [msatSort.c]
PackageName [A C version of SAT solver MINISAT, originally developed in C++ by Niklas Een and Niklas Sorensson, Chalmers University of Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
Synopsis [Sorting clauses.]
Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 1, 2004.]
Revision [
] DECLARATIONS ///
Function*************************************************************
Synopsis [Comparison procedure for two clauses.]
Description []
SideEffects []
SeeAlso []
Definition at line 93 of file msatSort.c.
00094 { 00095 float Value1 = Msat_ClauseReadActivity( *ppC1 ); 00096 float Value2 = Msat_ClauseReadActivity( *ppC2 ); 00097 if ( Value1 < Value2 ) 00098 return -1; 00099 if ( Value1 > Value2 ) 00100 return 1; 00101 return 0; 00102 }
void Msat_SolverSortDB | ( | Msat_Solver_t * | p | ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Msat_SolverSort the learned clauses in the increasing order of activity.]
Description []
SideEffects []
SeeAlso []
Definition at line 58 of file msatSort.c.
00059 { 00060 Msat_ClauseVec_t * pVecClauses; 00061 Msat_Clause_t ** pLearned; 00062 int nLearned; 00063 // read the parameters 00064 pVecClauses = Msat_SolverReadLearned( p ); 00065 nLearned = Msat_ClauseVecReadSize( pVecClauses ); 00066 pLearned = Msat_ClauseVecReadArray( pVecClauses ); 00067 // Msat_SolverSort the array 00068 // qMsat_SolverSort( (void *)pLearned, nLearned, sizeof(Msat_Clause_t *), 00069 // (int (*)(const void *, const void *)) Msat_SolverSortCompare ); 00070 // printf( "Msat_SolverSorting.\n" ); 00071 Msat_SolverSort( pLearned, nLearned, 91648253 ); 00072 /* 00073 if ( nLearned > 2 ) 00074 { 00075 printf( "Clause 1: %0.20f\n", Msat_ClauseReadActivity(pLearned[0]) ); 00076 printf( "Clause 2: %0.20f\n", Msat_ClauseReadActivity(pLearned[1]) ); 00077 printf( "Clause 3: %0.20f\n", Msat_ClauseReadActivity(pLearned[2]) ); 00078 } 00079 */ 00080 }
void Msat_SolverSortSelection | ( | Msat_Clause_t ** | array, | |
int | size | |||
) |
Function*************************************************************
Synopsis [Selection sort for small array size.]
Description []
SideEffects []
SeeAlso []
Definition at line 116 of file msatSort.c.
00117 { 00118 Msat_Clause_t * tmp; 00119 int i, j, best_i; 00120 for ( i = 0; i < size-1; i++ ) 00121 { 00122 best_i = i; 00123 for (j = i+1; j < size; j++) 00124 { 00125 if ( Msat_ClauseReadActivity(array[j]) < Msat_ClauseReadActivity(array[best_i]) ) 00126 best_i = j; 00127 } 00128 tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; 00129 } 00130 }