source: vis_dev/cusp-1.1/src/sat/util.c @ 43

Last change on this file since 43 was 12, checked in by cecile, 13 years ago

cusp added

File size: 11.3 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [util.h]
4 
5  PackageName [sat]
6
7  Synopsis    []
8 
9  Author      [Hoonsang Jin, Hyojung Han]
10
11  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
12
13  All rights reserved.
14
15  Redistribution and use in source and binary forms, with or without
16  modification, are permitted provided that the following conditions
17  are met:
18
19  Redistributions of source code must retain the above copyright
20  notice, this list of conditions and the following disclaimer.
21
22  Redistributions in binary form must reproduce the above copyright
23  notice, this list of conditions and the following disclaimer in the
24  documentation and/or other materials provided with the distribution.
25
26  Neither the name of the University of Colorado nor the names of its
27  contributors may be used to endorse or promote products derived from
28  this software without specific prior written permission.
29
30  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
31  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
32  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
33  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
34  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
35  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
36  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
37  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
38  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
39  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
40  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
41  POSSIBILITY OF SUCH DAMAGE.]
42 
43******************************************************************************/
44
45#include <string.h>
46#include "sat.h"
47#include "stdio.h"
48#include "malloc.h"
49/*#include "mm.h" */
50
51#define heap_left(i)    ((i<<1)+1)
52#define heap_right(i)   ((i+1)<<1)
53#define heap_parent(i)  ((i-1)>>1)
54
55/**
56static int
57sat_compare_activity(satManager_t *m, long x, long y)
58{
59  return(m->activity[x] > m->activity[y]);
60}
61**/
62
63void
64sat_heap_remove_var_assigned_level_zero(satManager_t *m, satHeap_t *h)
65{
66long i, j;
67 
68  for(i=j=0; i<h->size; i++) {
69    if(m->levels[h->heap[i]]) {
70      h->heap[j] = h->heap[i];
71      h->indices[h->heap[i]] = j++;
72    }
73    else {
74      h->indices[h->heap[i]] = -1;
75    }
76  }
77  h->size -= (i-j);
78
79  for(i=h->size/2-1; i>=0; i--) 
80    sat_heap_down(m, h, i);
81}
82
83void 
84sat_heap_up(satManager_t *m, satHeap_t *h, long i)
85{
86long *heap;
87long x;
88
89  heap = h->heap;
90  x = heap[i];
91  while(i!=0 && h->compare(m->activity, (const void*)x, (const void*)heap[heap_parent(i)])) {
92    heap[i] = heap[heap_parent(i)];
93    h->indices[heap[i]] = i;
94    i = heap_parent(i);
95  }
96  h->heap[i] = x;
97  h->indices[x] = i;
98}
99
100void
101sat_heap_down(satManager_t *m, satHeap_t *h, long i)
102{
103long *heap;
104long x, c;
105
106  heap = h->heap;
107  x = heap[i];
108  while(heap_left(i) < h->size) {
109    c = (heap_right(i) < h->size && 
110        h->compare(m->activity, (const void *)heap[heap_right(i)], (const void *)heap[heap_left(i)])) ?
111        heap_right(i) : heap_left(i);
112    if(!h->compare(m->activity, (const void *)heap[c], (const void *)x))        break;
113    heap[i] = heap[c];
114    h->indices[heap[i]] = i;
115    i = c;
116  }
117  heap[i] = x;
118  h->indices[x] = i;
119}
120
121long
122sat_heap_remove_min(satManager_t *m, satHeap_t *h)
123{
124long x;
125 
126  x = h->heap[0];
127  h->heap[0] = h->heap[h->size-1];
128  h->indices[h->heap[0]] = 0;
129  h->indices[x] = -1;
130  h->size--;
131  if(h->size > 1)       
132    sat_heap_down(m, h, 0);
133
134  return(x);
135}
136
137void
138sat_heap_clear(satHeap_t *h)
139{
140long i;
141 
142  for(i=0; i<h->size; i++)
143    h->indices[h->heap[i]] = -1;
144  h->size = 0;
145}
146
147void
148sat_heap_update(satManager_t *m, satHeap_t *h, long n)
149{
150 
151  if(h->indices[n] < 0)
152    sat_heap_insert(m, h, n);
153  else {
154    sat_heap_up(m, h, h->indices[n]);
155    sat_heap_down(m, h, h->indices[n]);
156  }
157}
158
159satHeap_t *
160sat_heap_init(satManager_t *m, int (*compare_heap)(void *, const void *, const void *))
161{
162satHeap_t *h;
163long nVars, i;
164 
165
166  h = (satHeap_t *)malloc(sizeof(satHeap_t));
167  h->size = 0;
168
169  nVars = m->nVars+1;
170  h->heap = (long *)malloc(sizeof(long)*nVars);
171  h->indices = (long *)malloc(sizeof(long)*nVars);
172  for(i=0; i<nVars; i++) h->indices[i] = -1;
173  h->compare = compare_heap;
174
175  return(h);
176}
177
178void
179sat_heap_resize(satManager_t *m, satHeap_t *h, long prenVars)
180{
181long nVars, i;
182 
183  nVars = m->nVars+1;
184  h->heap = (long *)realloc(h->heap, sizeof(long)*nVars);
185  h->indices = (long *)realloc(h->indices, sizeof(long)*nVars);
186  for(i=prenVars; i<nVars; i++) h->indices[i] = -1;
187}
188
189void
190sat_heap_print(satManager_t *m, satHeap_t *h)
191{
192int i;
193
194  h = m->variableHeap;
195  for(i=0; i<=m->nVars; i++) {
196    fprintf(stdout, "%d ", i);
197    fprintf(stdout, "%ld ", h->heap[i]);
198    fprintf(stdout, "%10g", m->activity[h->heap[i]]);
199    fprintf(stdout, "\n");
200  }
201}
202
203void
204sat_heap_free(satHeap_t *h)
205{
206  if(h) {
207    free(h->heap);
208    free(h->indices);
209    free(h);
210  }
211}
212
213int
214sat_heap_check(satManager_t *m, satHeap_t *h, long i)
215{
216  if(i >= h->size) return(1);
217
218  if(i==0 || !sat_compare_activity(m, (const void *)h->heap[i], (const void *)h->heap[heap_parent(i)])) {
219    return( sat_heap_check(m, h, heap_left(i)) && sat_heap_check(m, h, heap_right(i)));
220  }
221  return(0);
222     
223}
224
225
226void
227sat_heap_insert(satManager_t *m, satHeap_t *h, long n)
228{
229
230  h->indices[n] = h->size;
231  h->heap[h->size++] = n;
232  sat_heap_up(m, h, h->indices[n]);
233}
234
235satArray_t *
236sat_array_alloc(long num)
237{
238satArray_t *arr;
239   arr = (satArray_t *)malloc(sizeof(satArray_t) + sizeof(long)*num);
240   if(arr == 0) return(0);
241   arr->total = num;
242   arr->size = 0;
243   return(arr); 
244}
245
246satArray_t *
247sat_array_insert(satArray_t *arr, long datum)
248{
249satArray_t *nArr;
250
251   if(arr->size < arr->total) {
252       arr->space[arr->size++] = datum;
253   }
254   else {
255       nArr = sat_array_alloc(arr->total<<1);
256       memcpy(&(nArr->space[0]), &(arr->space[0]), sizeof(long)*arr->total);
257       nArr->size = arr->size;
258       free(arr);
259       arr = nArr;
260       arr->space[arr->size++] = datum;
261   }
262   return(arr);
263} 
264
265satArray_t *
266sat_array_realloc(satArray_t *arr, long size)
267{
268satArray_t *nArr;
269
270   if(size >= arr->total) {
271     nArr = sat_array_alloc(size);
272     nArr->total = size;
273     memcpy(&(nArr->space[0]), &(arr->space[0]), sizeof(long)*arr->total);
274     nArr->size = arr->size;
275     free(arr);
276     arr = nArr;
277   }
278   return(arr);
279} 
280
281satArray_t *
282sat_array_alloc_insert(satArray_t *arr, long datum)
283{
284satArray_t *nArr;
285
286   if(arr == 0) arr = sat_array_alloc(4);
287
288   if(arr->size < arr->total) {
289       arr->space[arr->size++] = datum;
290   }
291   else {
292     nArr = sat_array_alloc(arr->total<<1);
293     memcpy(&(nArr->space[0]), &(arr->space[0]), sizeof(long)*arr->total);
294     nArr->size = arr->size;
295     free(arr);
296     arr = nArr;
297     arr->space[arr->size++] = datum;
298   }
299   return(arr);
300} 
301
302satArray_t *
303sat_array_copy(satArray_t *arr1, satArray_t *arr2)
304{
305satArray_t *nArr;
306
307  if(arr2 == 0) {
308    arr2 = (satArray_t *)malloc(sizeof(satArray_t) + sizeof(long)*arr1->size);
309    if(arr2 == 0) return(0);
310    arr2->total = arr1->size;
311    arr2->size = 0;
312  }
313  if(arr1->size > arr2->total) {
314    nArr = sat_array_alloc(arr1->size);
315    free(arr2);
316    arr2 = nArr;
317  }
318  memcpy(&(arr2->space[0]), &(arr1->space[0]), sizeof(long)*arr1->size);
319  arr2->size = arr1->size;
320  return(arr2);
321}
322
323void
324sat_array_delete_elem(satArray_t *arr, long elem)
325{
326int i, index;
327
328  for(i=0; i<arr->size && arr->space[i] != elem; i++);
329  index = arr->size-1;
330  for(; i<index; i++)   arr->space[i] = arr->space[i+1];
331  arr->size--;
332}
333
334
335void
336sat_sort_clause_array(satArray_t *arr, int (*compare_sort)(const void *, const void *))
337{
338
339  sat_sort_clause_array_aux(&(arr->space[0]), arr->size, compare_sort);
340}
341
342void
343sat_sort_clause_array_aux(long *carr, long size,  int (*compare_sort)(const void *, const void *))
344{
345long i, j, tmp, bi;
346satClause_t *pivot;
347satClause_t *x, *y;
348
349  if(size <=15) {
350    for(i=0; i<size-1; i++) {
351      bi = i;
352      for(j=i+1; j<size; j++) {
353        x = ((satClause_t *)(carr[j]));
354        y = ((satClause_t *)(carr[bi]));
355        /**
356        if((SATSizeClause(x)) > 2 && ((SATSizeClause(y)) == 2 || x->info.activity < y->info.activity))
357        **/
358        if((*(compare_sort))(x, y))
359          bi = j;
360      }
361      tmp = carr[i];
362      carr[i] = carr[bi];
363      carr[bi] = tmp;
364    }
365  }
366  else {
367    pivot = (satClause_t *)carr[(size>>1)];
368    i = -1;
369    j = size;
370
371    while(1) {
372        /**
373      do i++; while( (SATSizeClause(((satClause_t *)(carr[i])))) > 2 && (SATSizeClause(pivot) == 2 ||
374              ((satClause_t *)(carr[i]))->info.activity < pivot->info.activity));
375      do j--; while( (SATSizeClause(pivot)) > 2 && ((SATSizeClause(((satClause_t *)(carr[j])))) == 2 ||
376              pivot->info.activity < ((satClause_t *)(carr[j]))->info.activity));
377              **/
378      do i++; while( (*(compare_sort))((const void *)carr[i], (const void *)pivot));
379      do j--; while( (*(compare_sort))((const void *)pivot, (const void *)carr[j]));
380      if(i>=j)  break;
381      tmp = carr[i];
382      carr[i] = carr[j];
383      carr[j] = tmp;
384    }
385    sat_sort_clause_array_aux(carr, i, compare_sort);
386    sat_sort_clause_array_aux(&(carr[i]), size-i, compare_sort);
387  }
388}
389
390void
391sat_sort_clause_literal(satClause_t *c)
392{
393long csize;
394
395  csize = SATSizeClause(c);
396  sat_sort_literal_aux(&(c->lits[0]), csize);
397}
398
399void
400sat_literal_array_sort(satArray_t *arr)
401{
402
403  sat_sort_literal_aux(&(arr->space[0]), arr->size);
404}
405
406
407void
408sat_sort_literal_aux(long *lits, long size)
409{
410long i, j, tmp, bi;
411long pivot;
412
413  if(size <=15) {
414    for(i=0; i<size-1; i++) {
415      bi = i;
416      for(j=i+1; j<size; j++) {
417        if(lits[j] < lits[bi])
418          bi = j;
419      }
420      tmp = lits[i];
421      lits[i] = lits[bi];
422      lits[bi] = tmp;
423    }
424  }
425  else {
426    pivot = lits[size>>1];
427    i = -1;
428    j = size;
429
430    while(1) {
431      do i++; while(lits[i] < pivot);
432      do j--; while(pivot < lits[j]);
433      if(i>=j)  break;
434      tmp = lits[i];
435      lits[i] = lits[j];
436      lits[j] = tmp;
437    }
438    sat_sort_literal_aux(lits, i);
439    sat_sort_literal_aux(&(lits[i]), size-i);
440  }
441}
442
443/** HHJ : remove duplicates **/
444/*
445satQueue_t *
446sat_queue_alloc(long num)
447{
448satArray_t *arr;
449satQueue_t *q;
450
451   arr = (satArray_t *)malloc(sizeof(satArray_t) + sizeof(long)*num);
452   if(arr == 0) return(0);
453   arr->total = num;
454   arr->size = 0;
455   q = (satQueue_t *)malloc(sizeof(satQueue_t));
456   q->arr = arr;
457   q->first = 0;
458   return(q);
459}
460
461void
462sat_queue_insert(satQueue_t *q, long datum)
463{
464   q->arr = sat_array_insert(q->arr, datum);
465}
466
467long
468sat_queue_pop(satQueue_t *q)
469{
470long datum;
471int i, j;
472satArray_t *arr;
473
474   arr = q->arr;
475   if(q->first > 1024) {
476     for(i=q->first,j=0; i<arr->size; i++) {
477       arr->space[j++] = arr->space[i];
478     }
479     arr->size = arr->size - q->first;
480     q->first = 0;
481   }
482   datum = arr->space[q->first];
483   q->first++;
484   return(datum);
485}
486
487long
488sat_queue_size(satQueue_t *q)
489{
490  return(q->arr->size - q->first);
491}
492
493void
494sat_queue_free(satQueue_t *q)
495{
496  free(q->arr);
497  free(q);
498}
499*/
500
501int
502sat_compress_clause(satManager_t *m, satClause_t *c)
503{
504long i, j, csize;
505long lit, v, preLit;
506int sign, value;
507
508  preLit = 0;
509  csize = SATSizeClause(c);
510  for (i=j=0; i<csize; i++) {
511    lit = c->lits[i];
512    v = lit >> 1;   
513    value = m->values[v];
514    sign = lit & 1;
515    if (lit == (preLit^1)) 
516      return 1;
517    else if (lit != preLit)
518      c->lits[j++] = preLit = c->lits[i]; 
519  }
520  c->size = ((csize - i + j) << SATCsizeShift) | (c->size & SATCMask); 
521  return 0; 
522}
523
524
Note: See TracBrowser for help on using the repository browser.