4632049834

Build # 4632049834

Build Type

github

Committed by GitHub

Commit Message

Merge 1c8923f4b into db898586b

Pull Request Pull Request #437: Bool bump factor

Run Details

2 of 2 new or added lines in 1 file covered. (100.0%)

76436 of 119004 relevant lines covered (64.23%)

1025652.22 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

89.31

/src/mcsat/variable_queue.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */
 
#include "mcsat/variable_queue.h"

#include "utils/dprng.h"

#include <float.h>

#define VAR_DECAY_FACTOR              (0.95)
#define VAR_ACTIVITY_THRESHOLD        (1e100)
#define INV_VAR_ACTIVITY_THRESHOLD    (1e-100)
#define INIT_VAR_ACTIVITY_INCREMENT   (1.0)

#define VAR_QUEUE_INITIAL_SIZE        (100)

void var_queue_construct(var_queue_t *queue) {
  uint32_t i;
  double *tmp;

  tmp = (double *) safe_malloc((VAR_QUEUE_INITIAL_SIZE+2) * sizeof(double));
  queue->activity = tmp + 2;
  queue->heap_index = (int32_t *) safe_malloc(VAR_QUEUE_INITIAL_SIZE * sizeof(int32_t));
  queue->heap = (variable_t *) safe_malloc((VAR_QUEUE_INITIAL_SIZE+1) * sizeof(variable_t));

  for (i=0; i<VAR_QUEUE_INITIAL_SIZE; i++) {
    queue->heap_index[i] = -1;
    queue->activity[i] = 0.0;
  }

  queue->activity[-2] = -1.0;
  queue->activity[-1] = DBL_MAX;
  queue->heap[0] = -1;

  queue->heap_last = 0;
  queue->size = VAR_QUEUE_INITIAL_SIZE;
  queue->vmax = 0;

  queue->act_increment = INIT_VAR_ACTIVITY_INCREMENT;
  queue->inv_act_decay = 1/VAR_DECAY_FACTOR;
}

void var_queue_extend(var_queue_t *queue, uint32_t n) {
  uint32_t old_size, i;
  double *tmp;

  old_size = queue->size;
  assert(old_size < n);
  tmp = queue->activity - 2;
  tmp = (double *) safe_realloc(tmp, (n+2) * sizeof(double));
  queue->activity = tmp + 2;
  queue->heap_index = (int32_t *) safe_realloc(queue->heap_index, n * sizeof(int32_t));
  queue->heap = (int32_t *) safe_realloc(queue->heap, (n+1) * sizeof(int32_t));
  queue->size = n;

  for (i=old_size; i<n; i++) {
    queue->heap_index[i] = -1;
    queue->activity[i] = 0.0;
  }
}

void var_queue_destruct(var_queue_t *queue) {
  safe_free(queue->activity - 2);
  safe_free(queue->heap_index);
  safe_free(queue->heap);
}

static
void var_queue_update_up(var_queue_t *queue, variable_t x, uint32_t i) {
  double ax, *act;
  int32_t *index;
  variable_t *h, y;
  uint32_t j;

  h = queue->heap;
  index = queue->heap_index;
  act = queue->activity;

  ax = act[x];

  for (;;) {
    j = i >> 1;    // parent of i
    y = h[j];      // variable at position j in the heap

    // The loop terminates since act[h[0]] = DBL_MAX
    if (act[y] >= ax) break;

    // move y down, into position i
    h[i] = y;
    index[y] = i;

    // move i up
    i = j;
  }

  // i is the new position for variable x
  h[i] = x;
  index[x] = i;
}

static
void var_queue_update_down(var_queue_t *queue) {
  double *act;
  int32_t *index;
  variable_t *h;
  variable_t x, y, z;
  double ax, ay, az;
  uint32_t i, j, last;

  last = queue->heap_last;
  queue->heap_last = last - 1;
  if (last <= 1 ) { // empty heap.
    assert(queue->heap_last == 0);
    return;
  }

  h = queue->heap;
  index = queue->heap_index;
  act = queue->activity;

  z = h[last];   // last element
  h[last] = -2;  // set end marker: act[-2] is negative
  az = act[z];   // activity of the last element

  i = 1;      // root
  j = 2;      // left child of i
  while (j < last) {
    /*
     * find child of i with highest activity.
     * Since h[last] = -2, we don't check j+1 < last
     */
    x = h[j];
    y = h[j+1];
    ax = act[x];
    ay = act[y];
    if (ay > ax) {
      j++;
      x = y;
      ax = ay;
    }

    // x = child of node i of highest activity
    // j = position of x in the heap (j = 2i or j = 2i+1)
    if (az >= ax) break;

    // move x up, into heap[i]
    h[i] = x;
    index[x] = i;

    // go down one step.
    i = j;
    j <<= 1;
  }

  h[i] = z;
  index[z] = i;
}

/**
 * Insert x into the heap, using its current activity.
 * No effect if x is already in the heap.
 * - x must be between 0 and nvars - 1
 */
void var_queue_insert(var_queue_t *queue, variable_t x) {
  assert(x >= 0);
  assert(x < queue->size);
  if (queue->heap_index[x] < 0) {
    // x not in the heap
    queue->heap_last ++;
    var_queue_update_up(queue, x, queue->heap_last);
  }
}


/** Check whether the heap is empty. */
bool var_queue_is_empty(var_queue_t *queue) {
  return queue->heap_last == 0;
}


/** Get and remove top element (the heap must not be empty) */
variable_t var_queue_pop(var_queue_t *queue) {
  variable_t top;

  assert(queue->heap_last > 0);

  // remove top element
  top = queue->heap[1];
  queue->heap_index[top] = -1;

  // repair the heap
  var_queue_update_down(queue);

  return top;
}

/** Get random element (the heap must not be empty) */
variable_t var_queue_random(var_queue_t *queue, double* seed) {
  assert(queue->heap_last > 0);
  return queue->heap[irand(seed, queue->heap_last)+1];
}

/** Rescale variable activities: divide by VAR_ACTIVITY_THRESHOLD. */
void var_queue_rescale_activities(var_queue_t *queue) {
  uint32_t i, n;
  double *act;

  n = queue->size;
  act = queue->activity;
  for (i=0; i<n; i++) {
    act[i] *= INV_VAR_ACTIVITY_THRESHOLD;
  }
  queue->act_increment *= INV_VAR_ACTIVITY_THRESHOLD;
}


/** Increase activity of variable x (factor times). */
void var_queue_bump_variable(var_queue_t *heap, variable_t x, uint32_t factor) {
  int32_t i;

  assert(factor > 0);
  assert(x < heap->size);

  if ((heap->activity[x] += factor * heap->act_increment) > VAR_ACTIVITY_THRESHOLD) {
    var_queue_rescale_activities(heap);
  }

  // move x up if it's in the heap
  i = heap->heap_index[x];
  if (i >= 0) {
    var_queue_update_up(heap, x, i);
  }
}

double var_queue_get_activity(const var_queue_t* queue, variable_t x) {
  assert(x < queue->size);
  return queue->activity[x];
}

void var_queue_set_activity(var_queue_t* queue, variable_t x, double a) {
  assert(x < queue->size);
  assert(queue->heap_index[x] < 0);
  queue->activity[x] = a;
}

int var_queue_cmp_variables(var_queue_t *queue, variable_t x, variable_t y) {
  assert(x < queue->size);
  assert(y < queue->size);

  double diff = queue->activity[x] - queue->activity[y];

  if (diff < 0) {
    return -1;
  }
  if (diff > 0) {
    return 1;
  }

  return 0;
}

/** Decay. */
void var_queue_decay_activities(var_queue_t *queue) {
  queue->act_increment *= queue->inv_act_decay;
}

/** Sweep the variables */
void var_queue_gc_sweep(var_queue_t* queue, const gc_info_t* gc_vars) {

  ivector_t vars;
  init_ivector(&vars, 0);

  assert(gc_vars->is_id);

  // pop all the variable and put them back in
  while (!var_queue_is_empty(queue)) {
    variable_t x = var_queue_pop(queue);
    if (gc_info_get_reloc(gc_vars, x) != variable_null) {
      ivector_push(&vars, x);
    }
  }
  uint32_t var_i;
  for (var_i = 0; var_i < vars.size; ++ var_i) {
    variable_t x = vars.data[var_i];
    var_queue_insert(queue, x);
  }

  delete_ivector(&vars);
}

1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2017 SRI International.
4	*
5	* Yices is free software: you can redistribute it and/or modify
6	* it under the terms of the GNU General Public License as published by
7	* the Free Software Foundation, either version 3 of the License, or
8	* (at your option) any later version.
9	*
10	* Yices is distributed in the hope that it will be useful,
11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13	* GNU General Public License for more details.
14	*
15	* You should have received a copy of the GNU General Public License
16	* along with Yices. If not, see <http://www.gnu.org/licenses/>.
17	*/
18
19	#include "mcsat/variable_queue.h"
20
21	#include "utils/dprng.h"
22
23	#include <float.h>
24
25	#define VAR_DECAY_FACTOR (0.95)
26	#define VAR_ACTIVITY_THRESHOLD (1e100)
27	#define INV_VAR_ACTIVITY_THRESHOLD (1e-100)
28	#define INIT_VAR_ACTIVITY_INCREMENT (1.0)
29
30	#define VAR_QUEUE_INITIAL_SIZE (100)
31
32	void var_queue_construct(var_queue_t *queue) {	613✔
33	uint32_t i;
34	double *tmp;
35
36	tmp = (double ) safe_malloc((VAR_QUEUE_INITIAL_SIZE+2) sizeof(double));	613✔
37	queue->activity = tmp + 2;	613✔
38	queue->heap_index = (int32_t ) safe_malloc(VAR_QUEUE_INITIAL_SIZE sizeof(int32_t));	613✔
39	queue->heap = (variable_t ) safe_malloc((VAR_QUEUE_INITIAL_SIZE+1) sizeof(variable_t));	613✔
40
41	for (i=0; i<VAR_QUEUE_INITIAL_SIZE; i++) {	61,913✔
42	queue->heap_index[i] = -1;	61,300✔
43	queue->activity[i] = 0.0;	61,300✔
44	}
45
46	queue->activity[-2] = -1.0;	613✔
47	queue->activity[-1] = DBL_MAX;	613✔
48	queue->heap[0] = -1;	613✔
49
50	queue->heap_last = 0;	613✔
51	queue->size = VAR_QUEUE_INITIAL_SIZE;	613✔
52	queue->vmax = 0;	613✔
53
54	queue->act_increment = INIT_VAR_ACTIVITY_INCREMENT;	613✔
55	queue->inv_act_decay = 1/VAR_DECAY_FACTOR;	613✔
56	}	613✔
57
58	void var_queue_extend(var_queue_t *queue, uint32_t n) {	459✔
59	uint32_t old_size, i;
60	double *tmp;
61
62	old_size = queue->size;	459✔
63	assert(old_size < n);
64	tmp = queue->activity - 2;	459✔
65	tmp = (double ) safe_realloc(tmp, (n+2) sizeof(double));	459✔
66	queue->activity = tmp + 2;	459✔
67	queue->heap_index = (int32_t ) safe_realloc(queue->heap_index, n sizeof(int32_t));	459✔
68	queue->heap = (int32_t ) safe_realloc(queue->heap, (n+1) sizeof(int32_t));	459✔
69	queue->size = n;	459✔
70
71	for (i=old_size; i<n; i++) {	181,979✔
72	queue->heap_index[i] = -1;	181,520✔
73	queue->activity[i] = 0.0;	181,520✔
74	}
75	}	459✔
76
77	void var_queue_destruct(var_queue_t *queue) {	613✔
78	safe_free(queue->activity - 2);	613✔
79	safe_free(queue->heap_index);	613✔
80	safe_free(queue->heap);	613✔
81	}	613✔
82
83	static
84	void var_queue_update_up(var_queue_t *queue, variable_t x, uint32_t i) {	6,367,237✔
85	double ax, *act;
86	int32_t *index;
87	variable_t *h, y;
88	uint32_t j;
89
90	h = queue->heap;	6,367,237✔
91	index = queue->heap_index;	6,367,237✔
92	act = queue->activity;	6,367,237✔
93
94	ax = act[x];	6,367,237✔
95
96	for (;;) {
97	j = i >> 1; // parent of i	19,609,010✔
98	y = h[j]; // variable at position j in the heap	19,609,010✔
99
100	// The loop terminates since act[h[0]] = DBL_MAX
101	if (act[y] >= ax) break;	19,609,010✔
102
103	// move y down, into position i
104	h[i] = y;	13,241,773✔
105	index[y] = i;	13,241,773✔
106
107	// move i up
108	i = j;	13,241,773✔
109	}
110
111	// i is the new position for variable x
112	h[i] = x;	6,367,237✔
113	index[x] = i;	6,367,237✔
114	}	6,367,237✔
115
116	static
117	void var_queue_update_down(var_queue_t *queue) {	2,619,686✔
118	double *act;
119	int32_t *index;
120	variable_t *h;
121	variable_t x, y, z;
122	double ax, ay, az;
123	uint32_t i, j, last;
124
125	last = queue->heap_last;	2,619,686✔
126	queue->heap_last = last - 1;	2,619,686✔
127	if (last <= 1 ) { // empty heap.	2,619,686✔
128	assert(queue->heap_last == 0);
129	return;	1,088✔
130	}
131
132	h = queue->heap;	2,618,598✔
133	index = queue->heap_index;	2,618,598✔
134	act = queue->activity;	2,618,598✔
135
136	z = h[last]; // last element	2,618,598✔
137	h[last] = -2; // set end marker: act[-2] is negative	2,618,598✔
138	az = act[z]; // activity of the last element	2,618,598✔
139
140	i = 1; // root	2,618,598✔
141	j = 2; // left child of i	2,618,598✔
142	while (j < last) {	23,944,306✔
143	/*
144	* find child of i with highest activity.
145	* Since h[last] = -2, we don't check j+1 < last
146	*/
147	x = h[j];	22,262,861✔
148	y = h[j+1];	22,262,861✔
149	ax = act[x];	22,262,861✔
150	ay = act[y];	22,262,861✔
151	if (ay > ax) {	22,262,861✔
152	j++;	10,750,821✔
153	x = y;	10,750,821✔
154	ax = ay;	10,750,821✔
155	}
156
157	// x = child of node i of highest activity
158	// j = position of x in the heap (j = 2i or j = 2i+1)
159	if (az >= ax) break;	22,262,861✔
160
161	// move x up, into heap[i]
162	h[i] = x;	21,325,708✔
163	index[x] = i;	21,325,708✔
164
165	// go down one step.
166	i = j;	21,325,708✔
167	j <<= 1;	21,325,708✔
168	}
169
170	h[i] = z;	2,618,598✔
171	index[z] = i;	2,618,598✔
172	}
173
174	/**
175	* Insert x into the heap, using its current activity.
176	* No effect if x is already in the heap.
177	* - x must be between 0 and nvars - 1
178	*/
179	void var_queue_insert(var_queue_t *queue, variable_t x) {	11,844,527✔
180	assert(x >= 0);
181	assert(x < queue->size);
182	if (queue->heap_index[x] < 0) {	11,844,527✔
183	// x not in the heap
184	queue->heap_last ++;	2,638,606✔
185	var_queue_update_up(queue, x, queue->heap_last);	2,638,606✔
186	}
187	}	11,844,527✔
188
189
190	/** Check whether the heap is empty. */
191	bool var_queue_is_empty(var_queue_t *queue) {	3,397,978✔
192	return queue->heap_last == 0;	3,397,978✔
193	}
194
195
196	/** Get and remove top element (the heap must not be empty) */
197	variable_t var_queue_pop(var_queue_t *queue) {	2,619,686✔
198	variable_t top;
199
200	assert(queue->heap_last > 0);
201
202	// remove top element
203	top = queue->heap[1];	2,619,686✔
204	queue->heap_index[top] = -1;	2,619,686✔
205
206	// repair the heap
207	var_queue_update_down(queue);	2,619,686✔
208
209	return top;	2,619,686✔
210	}
211
212	/** Get random element (the heap must not be empty) */
213	variable_t var_queue_random(var_queue_t queue, double seed) {	×
214	assert(queue->heap_last > 0);
215	return queue->heap[irand(seed, queue->heap_last)+1];	×
216	}
217
218	/** Rescale variable activities: divide by VAR_ACTIVITY_THRESHOLD. */
219	void var_queue_rescale_activities(var_queue_t *queue) {	14✔
220	uint32_t i, n;
221	double *act;
222
223	n = queue->size;	14✔
224	act = queue->activity;	14✔
225	for (i=0; i<n; i++) {	25,777✔
226	act[i] *= INV_VAR_ACTIVITY_THRESHOLD;	25,763✔
227	}
228	queue->act_increment *= INV_VAR_ACTIVITY_THRESHOLD;	14✔
229	}	14✔
230
231
232	/** Increase activity of variable x (factor times). */
233	void var_queue_bump_variable(var_queue_t *heap, variable_t x, uint32_t factor) {	6,739,391✔
234	int32_t i;
235
236	assert(factor > 0);
237	assert(x < heap->size);
238
239	if ((heap->activity[x] += factor * heap->act_increment) > VAR_ACTIVITY_THRESHOLD) {	6,739,391✔
240	var_queue_rescale_activities(heap);	14✔
241	}
242
243	// move x up if it's in the heap
244	i = heap->heap_index[x];	6,739,391✔
245	if (i >= 0) {	6,739,391✔
246	var_queue_update_up(heap, x, i);	3,728,631✔
247	}
248	}	6,739,391✔
249
250	double var_queue_get_activity(const var_queue_t* queue, variable_t x) {	×
251	assert(x < queue->size);
252	return queue->activity[x];	×
253	}
254
255	void var_queue_set_activity(var_queue_t* queue, variable_t x, double a) {	×
256	assert(x < queue->size);
257	assert(queue->heap_index[x] < 0);
258	queue->activity[x] = a;	×
259	}	×
260
261	int var_queue_cmp_variables(var_queue_t *queue, variable_t x, variable_t y) {	×
262	assert(x < queue->size);
263	assert(y < queue->size);
264
265	double diff = queue->activity[x] - queue->activity[y];	×
266
267	if (diff < 0) {	×
268	return -1;	×
269	}
270	if (diff > 0) {	×
271	return 1;	×
272	}
273
274	return 0;	×
275	}
276
277	/** Decay. */
278	void var_queue_decay_activities(var_queue_t *queue) {	120,070✔
279	queue->act_increment *= queue->inv_act_decay;	120,070✔
280	}	120,070✔
281
282	/** Sweep the variables */
283	void var_queue_gc_sweep(var_queue_t* queue, const gc_info_t* gc_vars) {	491✔
284
285	ivector_t vars;
286	init_ivector(&vars, 0);	491✔
287
288	assert(gc_vars->is_id);
289
290	// pop all the variable and put them back in
291	while (!var_queue_is_empty(queue)) {	208,774✔
292	variable_t x = var_queue_pop(queue);	208,283✔
293	if (gc_info_get_reloc(gc_vars, x) != variable_null) {	208,283✔
294	ivector_push(&vars, x);	192,882✔
295	}
296	}
297	uint32_t var_i;
298	for (var_i = 0; var_i < vars.size; ++ var_i) {	193,373✔
299	variable_t x = vars.data[var_i];	192,882✔
300	var_queue_insert(queue, x);	192,882✔
301	}
302
303	delete_ivector(&vars);	491✔
304	}	491✔

SRI-CSL / yices2 / 4632049834

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous