abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
msatSort.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [msatSort.c]
4 
5  PackageName [A C version of SAT solver MINISAT, originally developed
6  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of
7  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
8 
9  Synopsis [Sorting clauses.]
10 
11  Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - January 1, 2004.]
16 
17  Revision [$Id: msatSort.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "msatInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static int Msat_SolverSortCompare( Msat_Clause_t ** ppC1, Msat_Clause_t ** ppC2 );
31 
32 // Returns a random float 0 <= x < 1. Seed must never be 0.
33 static double drand(double seed) {
34  int q;
35  seed *= 1389796;
36  q = (int)(seed / 2147483647);
37  seed -= (double)q * 2147483647;
38  return seed / 2147483647; }
39 
40 // Returns a random integer 0 <= x < size. Seed must never be 0.
41 static int irand(double seed, int size) {
42  return (int)(drand(seed) * size); }
43 
44 static void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed );
45 
46 ////////////////////////////////////////////////////////////////////////
47 /// FUNCTION DEFINITIONS ///
48 ////////////////////////////////////////////////////////////////////////
49 
50 /**Function*************************************************************
51 
52  Synopsis [Msat_SolverSort the learned clauses in the increasing order of activity.]
53 
54  Description []
55 
56  SideEffects []
57 
58  SeeAlso []
59 
60 ***********************************************************************/
61 void Msat_SolverSortDB( Msat_Solver_t * p )
62 {
63  Msat_ClauseVec_t * pVecClauses;
64  Msat_Clause_t ** pLearned;
65  int nLearned;
66  // read the parameters
67  pVecClauses = Msat_SolverReadLearned( p );
68  nLearned = Msat_ClauseVecReadSize( pVecClauses );
69  pLearned = Msat_ClauseVecReadArray( pVecClauses );
70  // Msat_SolverSort the array
71 // qMsat_SolverSort( (void *)pLearned, nLearned, sizeof(Msat_Clause_t *),
72 // (int (*)(const void *, const void *)) Msat_SolverSortCompare );
73 // printf( "Msat_SolverSorting.\n" );
74  Msat_SolverSort( pLearned, nLearned, 91648253 );
75 /*
76  if ( nLearned > 2 )
77  {
78  printf( "Clause 1: %0.20f\n", Msat_ClauseReadActivity(pLearned[0]) );
79  printf( "Clause 2: %0.20f\n", Msat_ClauseReadActivity(pLearned[1]) );
80  printf( "Clause 3: %0.20f\n", Msat_ClauseReadActivity(pLearned[2]) );
81  }
82 */
83 }
84 
85 /**Function*************************************************************
86 
87  Synopsis [Comparison procedure for two clauses.]
88 
89  Description []
90 
91  SideEffects []
92 
93  SeeAlso []
94 
95 ***********************************************************************/
96 int Msat_SolverSortCompare( Msat_Clause_t ** ppC1, Msat_Clause_t ** ppC2 )
97 {
98  float Value1 = Msat_ClauseReadActivity( *ppC1 );
99  float Value2 = Msat_ClauseReadActivity( *ppC2 );
100  if ( Value1 < Value2 )
101  return -1;
102  if ( Value1 > Value2 )
103  return 1;
104  return 0;
105 }
106 
107 
108 /**Function*************************************************************
109 
110  Synopsis [Selection sort for small array size.]
111 
112  Description []
113 
114  SideEffects []
115 
116  SeeAlso []
117 
118 ***********************************************************************/
119 void Msat_SolverSortSelection( Msat_Clause_t ** array, int size )
120 {
121  Msat_Clause_t * tmp;
122  int i, j, best_i;
123  for ( i = 0; i < size-1; i++ )
124  {
125  best_i = i;
126  for (j = i+1; j < size; j++)
127  {
128  if ( Msat_ClauseReadActivity(array[j]) < Msat_ClauseReadActivity(array[best_i]) )
129  best_i = j;
130  }
131  tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
132  }
133 }
134 
135 /**Function*************************************************************
136 
137  Synopsis [The original MiniSat sorting procedure.]
138 
139  Description [This procedure is used to preserve trace-equivalence
140  with the orignal C++ implemenation of the solver.]
141 
142  SideEffects []
143 
144  SeeAlso []
145 
146 ***********************************************************************/
147 void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed )
148 {
149  if (size <= 15)
150  Msat_SolverSortSelection( array, size );
151  else
152  {
153  Msat_Clause_t * pivot = array[irand(seed, size)];
154  Msat_Clause_t * tmp;
155  int i = -1;
156  int j = size;
157 
158  for(;;)
159  {
160  do i++; while( Msat_ClauseReadActivity(array[i]) < Msat_ClauseReadActivity(pivot) );
161  do j--; while( Msat_ClauseReadActivity(pivot) < Msat_ClauseReadActivity(array[j]) );
162 
163  if ( i >= j ) break;
164 
165  tmp = array[i]; array[i] = array[j]; array[j] = tmp;
166  }
167  Msat_SolverSort(array , i , seed);
168  Msat_SolverSort(&array[i], size-i, seed);
169  }
170 }
171 
172 ////////////////////////////////////////////////////////////////////////
173 /// END OF FILE ///
174 ////////////////////////////////////////////////////////////////////////
175 
176 
177 ABC_NAMESPACE_IMPL_END
178 
Msat_SolverSortSelection
void Msat_SolverSortSelection(Msat_Clause_t **array, int size)
Definition: msatSort.c:119
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
drand
static double drand(double seed)
Definition: msatSort.c:33
Msat_SolverReadLearned
Msat_ClauseVec_t * Msat_SolverReadLearned(Msat_Solver_t *p)
Definition: msatSolverApi.c:54
Msat_Clause_t
typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_ Msat_Clause_t
INCLUDES ///.
Definition: msatInt.h:57
Msat_ClauseVecReadSize
int Msat_ClauseVecReadSize(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:101
irand
static int irand(double seed, int size)
Definition: msatSort.c:41
Msat_SolverSortCompare
static ABC_NAMESPACE_IMPL_START int Msat_SolverSortCompare(Msat_Clause_t **ppC1, Msat_Clause_t **ppC2)
DECLARATIONS ///.
Definition: msatSort.c:96
Msat_ClauseVecReadArray
Msat_Clause_t ** Msat_ClauseVecReadArray(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:85
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Msat_SolverSortDB
void Msat_SolverSortDB(Msat_Solver_t *p)
FUNCTION DEFINITIONS ///.
Definition: msatSort.c:61
size
static int size
Definition: cuddSign.c:86
Msat_SolverSort
static void Msat_SolverSort(Msat_Clause_t **array, int size, double seed)
Definition: msatSort.c:147
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Msat_ClauseVec_t_
Definition: msatInt.h:155
Msat_Solver_t
typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_ Msat_Solver_t
INCLUDES ///.
Definition: msat.h:42
Msat_ClauseReadActivity
float Msat_ClauseReadActivity(Msat_Clause_t *pC)
Definition: msatClause.c:295