Blame view

src/constraints/sum_var.c 14.2 KB
94b2b13d   Pedro Roque   PHACT source
1
2
3
4
/*
 * sum_var.c
 *
 *  Created on: 14/03/2017
4d26a735   Pedro Roque   Increased recogni...
5
 *      Author: pedro
94b2b13d   Pedro Roque   PHACT source
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
 */

#ifndef __OPENCL_VERSION__

#include <stddef.h>
#include <stdio.h>

#include "sum_var.h"

#include "../bitmaps.h"
#include "../config.h"
#include "../variables.h"

#endif

#include "../kernels/cl_aux_functions.h"
#if CL_D_TYPE == CL_BITMAP
#include "../kernels/cl_bitmaps.h"
#elif CL_D_TYPE == CL_INTERVAL
#include  "../kernels/cl_intervals.h"
#endif
#include "../kernels/cl_constraints.h"
#include "../kernels/cl_variables.h"
#include "../kernels/cl_ttl.h"

#ifndef __OPENCL_VERSION__

/*
4d26a735   Pedro Roque   Increased recogni...
34
 * Creates a new constraint of the sum_var_ type and return the constraint ID
94b2b13d   Pedro Roque   PHACT source
35
36
37
38
39
 * sum(X, y)
 * X_ids - vector with the ID of the variables that may contain the value of y
 * n_vs - maximum number of variables in X vector
 * y_id - ID of the variable that contains the sum of all the variables in X
 */
4d26a735   Pedro Roque   Increased recogni...
40
unsigned int c_sum_var(unsigned int* X_ids, unsigned int n_vs, unsigned int y_id) {
94b2b13d   Pedro Roque   PHACT source
41
42
43
44
45
46
47
	unsigned int i;

	// set to include in kernel compilation
	USE_CS[SUM_VAR] = 1;
	USE_NON_CS_REIFI[SUM_VAR] = 1;
	REV = 1;

4d26a735   Pedro Roque   Increased recogni...
48
	unsigned int* c_vs = malloc((n_vs + 1) * sizeof(unsigned int));
94b2b13d   Pedro Roque   PHACT source
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76

	for (i = 0; i < n_vs; i++) {
		c_vs[i] = X_ids[i];
	}
	c_vs[n_vs] = y_id;

	// creates a new generic constraint
	unsigned int c_id = c_new(c_vs, n_vs + 1, NULL, 0, -1);

	// pointers to this type of constraint functions
	CS[c_id].kind = SUM_VAR;
	CS[c_id].check_sol_f = &sum_var_check;
	CS[c_id].constant_val = 0;

	CS[c_id].boolean = true;
	for (i = 0; i < n_vs; i++) {

		if (!VS[c_vs[i]].boolean) {
			CS[c_id].boolean = false;
		}
	}

	free(c_vs);

	return c_id;
}

/*
4d26a735   Pedro Roque   Increased recogni...
77
 * Creates a new reified constraint of the sum_var_ type and return the constraint ID
94b2b13d   Pedro Roque   PHACT source
78
79
80
81
82
83
 * sum(X, y)
 * X_ids - vector with the ID of the variables that may contain the value of y
 * n_vs - maximum number of variables in X vector
 * y_id - ID of the variable that contains the sum of all the variables in X
 * reif_v_id - ID of the reification variable
 */
4d26a735   Pedro Roque   Increased recogni...
84
unsigned int c_sum_var_reif(unsigned int* X_ids, unsigned int n_vs, unsigned int y_id, int reif_v_id) {
94b2b13d   Pedro Roque   PHACT source
85
86
87
88
89
90
	unsigned int i;

	if (VS[reif_v_id].max > 1) {
		v_del_gt(&VS[reif_v_id], 1);

		if (VS[reif_v_id].n_vals == 0) {
4d26a735   Pedro Roque   Increased recogni...
91
92
93
94
95
96
97
98
			fprintf(stderr, "\nError: Constraint SUM_VAR_REIF makes model inconsistent at creation:\n");
			exit(-1);
		}
	}

	// set to include in kernel compilation
	USE_CS[SUM_VAR] = 1;
	USE_CS_REIFI[SUM_VAR] = 1;
94b2b13d   Pedro Roque   PHACT source
99
100
101
102
103
104
105
106
	REV = 1;

	unsigned int* c_vs = malloc((n_vs + 1) * sizeof(unsigned int));

	for (i = 0; i < n_vs; i++) {
		c_vs[i] = X_ids[i];
	}
	c_vs[n_vs] = y_id;
4d26a735   Pedro Roque   Increased recogni...
107

94b2b13d   Pedro Roque   PHACT source
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
	// creates a new generic constraint
	unsigned int c_id = c_new(c_vs, n_vs + 1, NULL, 0, reif_v_id);

	// pointers to this type of constraint functions
	CS[c_id].kind = SUM_VAR;
	CS[c_id].check_sol_f = &sum_var_check;
	CS[c_id].constant_val = 0;

	free(c_vs);

	return c_id;
}

/*
 * Return true if the sum_var_ constraint is respected or false if not
 * sum(X, y)
 * c - constraint to check if is respected
 * explored - if the CSP was already explored, which mean that all the variables must already be singletons
 * */
bool sum_var_check(constr* c, bool explored) {
4d26a735   Pedro Roque   Increased recogni...
128
	var** X = c->c_vs;
94b2b13d   Pedro Roque   PHACT source
129
130
131
132
	var* y = c->c_vs[c->n_c_vs - 1];
	var* x;
	int sum = 0;
	int i;
4d26a735   Pedro Roque   Increased recogni...
133
134
135
136

	for (i = 0; i < c->n_c_vs - 1; i++) {
		x = X[i];

94b2b13d   Pedro Roque   PHACT source
137
138
139
#if CHECK_SOL_N_VALS
		if (x->to_label && x->n_vals != 1) {
			if (explored) {
4d26a735   Pedro Roque   Increased recogni...
140
141
142
143
				fprintf(stderr, "\nError: Constraint SUM_VAR (%d) not respected:\n", c->c_id);
				for (i = 0; i < c->n_c_vs; i++) {
					fprintf(stderr, "Variable ID=%u -> minimum=%u, maximum=%u, number of values=%u\n\n", c->c_vs[i]->v_id, b_get_min_val(&c->c_vs[i]->domain_b),
							b_get_max_val(&c->c_vs[i]->domain_b), b_cnt_vals(&c->c_vs[i]->domain_b));
94b2b13d   Pedro Roque   PHACT source
144
				}
4d26a735   Pedro Roque   Increased recogni...
145
146
147
148
149
150
			}
			return false;
		}
#endif
		sum += x->min;
	}
94b2b13d   Pedro Roque   PHACT source
151
152

	if (
4d26a735   Pedro Roque   Increased recogni...
153
154
155
156
157
#if CHECK_SOL_N_VALS
			(y->to_label && y->n_vals != 1) ||
#endif
			sum != y->min) {
		if (explored) {
94b2b13d   Pedro Roque   PHACT source
158
159
160
			fprintf(stderr, "\nError: Constraint SUM_VAR (%d) not respected:\n", c->c_id);

			for (i = 0; i < c->n_c_vs; i++) {
4d26a735   Pedro Roque   Increased recogni...
161
162
				fprintf(stderr, "Variable ID=%u -> minimum=%u, maximum=%u, number of values=%u\n\n", c->c_vs[i]->v_id, b_get_min_val(&c->c_vs[i]->domain_b),
						b_get_max_val(&c->c_vs[i]->domain_b), b_cnt_vals(&c->c_vs[i]->domain_b));
94b2b13d   Pedro Roque   PHACT source
163
			}
4d26a735   Pedro Roque   Increased recogni...
164
165
166
167
168
169
170
171
172
		}
		return false;
	}

	return true;
}

#endif

94b2b13d   Pedro Roque   PHACT source
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
#if CS_SUM_VAR == 1
/*
 * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID sum_var constraint
 * sum(X, y)
 * prop_ok will be set to 1 if success or to 0 if any domain became empty
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * vs_prop_ - all CSP variables with current step values
 * prop_v_id - variable ID to propagate
 * current_cs - constraint that should be propagated for the variable with prop_v_id ID
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
 */
CUDA_FUNC void sum_var_prop(CL_INTS_MEM int* vs_per_c_idx, CL_MEMORY VARS_PROP* vs_prop_, CL_CS_MEM cl_constr* current_cs, CL_MEMORY unsigned short* vs_id_to_prop_,
		bool* prop_ok, __global int* terms_mem CS_IGNORE_FUNC TTL_CTR) {

	int y_idx = current_cs->n_c_vs - 1;
	int y_id = vs_per_c_idx[y_idx];
	int x_id;
	__global int* mins = terms_mem;
94b2b13d   Pedro Roque   PHACT source
191
192
	__global int* maxs = &terms_mem[current_cs->n_c_vs];
	int min, max;
94b2b13d   Pedro Roque   PHACT source
193
194
	int val_to_rmv;
	bool changed = 0;
4d26a735   Pedro Roque   Increased recogni...
195
196
	int i;

94b2b13d   Pedro Roque   PHACT source
197
	mins[y_idx] = V_MIN(vs_prop_[y_id]);
4d26a735   Pedro Roque   Increased recogni...
198
199
	maxs[y_idx] = V_MAX(vs_prop_[y_id]);

94b2b13d   Pedro Roque   PHACT source
200
201
202
203
	// if the sum of the minimums of x is greater than maximum of y
	// if the sum of the maximums of x is lesser than the minimum of y
	min = 0;
	max = 0;
4d26a735   Pedro Roque   Increased recogni...
204
205
	for (i = 0; i < y_idx; i++) {
		CHECK_TTL(ttl_ctr, 96)
94b2b13d   Pedro Roque   PHACT source
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
		x_id = vs_per_c_idx[i];
		min += mins[i] = V_MIN(vs_prop_[x_id]);
		max += maxs[i] = V_MAX(vs_prop_[x_id]);
	}


	if (min > maxs[y_idx] || max < mins[y_idx]) {
		*prop_ok = 0;
		return;
	}

	// set all X because their min values sum is equal to the y max
	if (min == maxs[y_idx]) {
		for (i = 0; i < y_idx; i++) {
			CHECK_TTL(ttl_ctr, 167)
			x_id = vs_per_c_idx[i];

			if (V_N_VALS(vs_prop_[x_id]) > 1) {
				cl_v_del_all_except_val_m(&changed, &vs_prop_[x_id], mins[i] TTL_CTR_V);
94b2b13d   Pedro Roque   PHACT source
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
				v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);
			}
		}
		if (V_N_VALS(vs_prop_[y_id]) > 1) {
			cl_v_del_all_except_val_m(&changed, &vs_prop_[y_id], maxs[y_idx] TTL_CTR_V);
			v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
		}

#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif

		return;
	}

	// set all X because their max values sum is equal to the y min
	if (max == mins[y_idx]) {
		for (i = 0; i < y_idx; ++i) {
			CHECK_TTL(ttl_ctr, 168)
			x_id = vs_per_c_idx[i];

			if (V_N_VALS(vs_prop_[x_id]) > 1) {
				cl_v_del_all_except_val_m(&changed, &vs_prop_[x_id], maxs[i] TTL_CTR_V);
				v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);
			}
		}
		if (V_N_VALS(vs_prop_[y_id]) > 1) {
			cl_v_del_all_except_val_m(&changed, &vs_prop_[y_id], mins[y_idx] TTL_CTR_V);
			v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
		}
4d26a735   Pedro Roque   Increased recogni...
255

94b2b13d   Pedro Roque   PHACT source
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif

		return;
	}

	// remove bounds from all x
#if CL_BOOLEAN_VS
	if (current_cs->boolean == 0) {	// not all X are boolean
#endif
		for (i = 0; i < y_idx; i++) {
			CHECK_TTL(ttl_ctr, 98)
			x_id = vs_per_c_idx[i];

			changed = 0;
			if (V_N_VALS(vs_prop_[x_id]) > 1) {

				val_to_rmv = mins[i] + maxs[y_idx] - min;
				if (val_to_rmv < maxs[i]) {

4d26a735   Pedro Roque   Increased recogni...
277
					min -= mins[i];
94b2b13d   Pedro Roque   PHACT source
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
					max -= maxs[i];

					cl_v_del_gt_m(&changed, &vs_prop_[x_id], val_to_rmv TTL_CTR_V);

					if (V_IS_EMPTY(vs_prop_[x_id])) {
						*prop_ok = 0;
						return;
					}
					v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);

					min += mins[i] = V_MIN(vs_prop_[x_id]);
					max += maxs[i] = V_MAX(vs_prop_[x_id]);
				}

				val_to_rmv = maxs[i] - (max - mins[y_idx]);
				if (val_to_rmv > mins[i]) {

					min -= mins[i];
					max -= maxs[i];

					cl_v_del_lt_m(&changed, &vs_prop_[x_id], val_to_rmv TTL_CTR_V);

					if (V_IS_EMPTY(vs_prop_[x_id])) {
						*prop_ok = 0;
						return;
					}
					v_add_to_prop(vs_id_to_prop_, vs_prop_, x_id);

					min += mins[i] = V_MIN(vs_prop_[x_id]);
					max += maxs[i] = V_MAX(vs_prop_[x_id]);
				}
			}
		}
#if CL_BOOLEAN_VS
	}
#endif

	if (min > mins[y_idx]) {
		cl_v_del_lt_m(&changed, &vs_prop_[y_id], min TTL_CTR_V);

		if (V_IS_EMPTY(vs_prop_[y_id])) {
			*prop_ok = 0;
			return;
		}
		v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
	}
4d26a735   Pedro Roque   Increased recogni...
324

94b2b13d   Pedro Roque   PHACT source
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
	if (max < maxs[y_idx]) {
		cl_v_del_gt_m(&changed, &vs_prop_[y_id], max TTL_CTR_V);

		if (V_IS_EMPTY(vs_prop_[y_id])) {
			*prop_ok = 0;
			return;
		}
		v_add_to_prop(vs_id_to_prop_, vs_prop_, y_id);
	}
}

#if CS_R_SUM_VAR == 1
/*
 * Validate sum_var constraint to be normally propagated, when reified
 * sum(X, y)
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * vs_prop_ - all CSP variables with current step values
 * current_cs - constraint that should be propagated for the variable with prop_v_id ID
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
 */
CUDA_FUNC void sum_var_reif( CL_INTS_MEM int* vs_per_c_idx, CL_MEMORY VARS_PROP* vs_prop_, CL_CS_MEM cl_constr* current_cs, CL_MEMORY unsigned short* vs_id_to_prop_,
		__global int* terms_mem	CS_IGNORE_FUNC TTL_CTR) {

	int sum = current_cs->n_c_vs - 1;
	int y_id = vs_per_c_idx[sum];
	VARS_PROP y;
	int x_id;
	VARS_PROP x;
	__global int* mins = terms_mem;
	__global int* maxs = &terms_mem[current_cs->n_c_vs];
	int min, max;
	bool changed = 0;
4d26a735   Pedro Roque   Increased recogni...
357
	bool all_singl = true;
94b2b13d   Pedro Roque   PHACT source
358
	int i;
4d26a735   Pedro Roque   Increased recogni...
359
360

	mins[sum] = V_MIN(vs_prop_[y_id]);
94b2b13d   Pedro Roque   PHACT source
361
362
363
364
365
366
	maxs[sum] = V_MAX(vs_prop_[y_id]);

	// if the sum of the minimums of x is greater than maximum of y
	min = 0;
	for (i = 0; i < sum; i++) {
		CHECK_TTL(ttl_ctr, 99)
4d26a735   Pedro Roque   Increased recogni...
367
368
		min += mins[i] = V_MIN(vs_prop_[i]);

94b2b13d   Pedro Roque   PHACT source
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
		if (V_N_VALS(vs_prop_[i]) != 1) {
			all_singl = false;
		}

		if (min > maxs[sum]) {
			cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 1 TTL_CTR_V);
			v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));

#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif
			return;
		}
	}

	if (V_N_VALS(vs_prop_[y_id]) == 1 && all_singl && min == V_MIN(vs_prop_[y_id])) {
		cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 0 TTL_CTR_V);
		v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));

#if CL_CS_IGNORE
4d26a735   Pedro Roque   Increased recogni...
389
		cs_ignore[current_cs->c_id] = 1;
94b2b13d   Pedro Roque   PHACT source
390
391
#endif
		return;
4d26a735   Pedro Roque   Increased recogni...
392
	}
94b2b13d   Pedro Roque   PHACT source
393
394
395
396
397
398
399

	// if the sum of the maximums of x is lesser than the minimum of y
	max = 0;
	for (i = 0; i < sum; i++) {
		CHECK_TTL(ttl_ctr, 100)
		max += maxs[i] = V_MAX(vs_prop_[i]);
	}
4d26a735   Pedro Roque   Increased recogni...
400

94b2b13d   Pedro Roque   PHACT source
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
	if (max < mins[sum]) {
		cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 1 TTL_CTR_V);
		v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));

#if CL_CS_IGNORE
		cs_ignore[current_cs->c_id] = 1;
#endif
		return;
	}

	// remove bounds from all x
#if CL_BOOLEAN_VS
	if (current_cs->boolean == 0) {	// not all X are boolean
#endif
		for (i = 0; i < sum; i++) {
			CHECK_TTL(ttl_ctr, 101)
4d26a735   Pedro Roque   Increased recogni...
417
			x_id = vs_per_c_idx[i];
94b2b13d   Pedro Roque   PHACT source
418
419
420
421
422
423
424
425
			cl_v_copy_pm(&x, &vs_prop_[x_id] TTL_CTR_V);
			changed = 0;

			if (V_N_VALS(vs_prop_[x_id]) > 1) {
				if (mins[i] + maxs[sum] - min < maxs[i]) {
					cl_v_del_gt_n(&changed, &x, mins[i] + maxs[sum] - min TTL_CTR_V);

					changed = 1;
4d26a735   Pedro Roque   Increased recogni...
426
				}
94b2b13d   Pedro Roque   PHACT source
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442

				if (maxs[i] - (max - mins[sum]) > mins[i]) {
					cl_v_del_lt_n(&changed, &x, maxs[i] - (max - mins[sum]) TTL_CTR_V);

					changed = 1;
				}

				if (V_IS_EMPTY(x)) {
					cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 1 TTL_CTR_V);
					v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
					return;
				}
			}
		}
#if CL_BOOLEAN_VS
	}
4d26a735   Pedro Roque   Increased recogni...
443
#endif
94b2b13d   Pedro Roque   PHACT source
444
445
446
447
448
449

	cl_v_copy_pm(&y, &vs_prop_[y_id] TTL_CTR_V);
	if (min > mins[sum]) {
		cl_v_del_lt_n(&changed, &y, min TTL_CTR_V);

		if (V_IS_EMPTY(y)) {
4d26a735   Pedro Roque   Increased recogni...
450
			cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 1 TTL_CTR_V);
94b2b13d   Pedro Roque   PHACT source
451
452
453
454
			v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
			return;
		}
	}
4d26a735   Pedro Roque   Increased recogni...
455

94b2b13d   Pedro Roque   PHACT source
456
457
458
459
460
461
462
463
464
	if (max < maxs[sum]) {
		cl_v_del_gt_n(&changed, &y, max TTL_CTR_V);

		if (V_IS_EMPTY(y)) {
			cl_v_bool_del_val_m(&vs_prop_[current_cs->reif_var_id], 1 TTL_CTR_V);
			v_add_to_prop(vs_id_to_prop_, vs_prop_, convert_int(current_cs->reif_var_id));
		}
	}
}
4d26a735   Pedro Roque   Increased recogni...
465

94b2b13d   Pedro Roque   PHACT source
466
467
468
469
470
471
472
473
474
/*
 * Propagate the domain of the variable with the ID prop_v_id through all the other variables on the same c_numb ID sum_var opposite constraint
 * !sum(X, y)
 * vs_per_c_idx - vector with all constrained variables ID per constraint, per constraint ID order
 * vs_prop_ - all CSP variables with current step values
 * prop_v_id - variable ID to propagate
 * current_cs - constraint that should be propagated for the variable with prop_v_id ID
 * vs_id_to_prop_ - circular vector with the ids of the variables to propagate
 */
4d26a735   Pedro Roque   Increased recogni...
475
CUDA_FUNC void sum_var_prop_opposite(CL_INTS_MEM int* vs_per_c_idx, CL_MEMORY VARS_PROP* vs_prop_, CL_CS_MEM cl_constr* current_cs, bool* prop_ok, __global int* terms_mem TTL_CTR) {
94b2b13d   Pedro Roque   PHACT source
476
477
478
479
480
481
482
483
484

	int sum = current_cs->n_c_vs - 1;
	int y_id = vs_per_c_idx[sum];
	__global int* mins = terms_mem;
	int min, max;
	int i;

	mins[sum] = V_MIN(vs_prop_[y_id]);

94b2b13d   Pedro Roque   PHACT source
485
	// if the sum of the minimums of x is equal to y
4d26a735   Pedro Roque   Increased recogni...
486
487
	min = 0;
	max = 0;
94b2b13d   Pedro Roque   PHACT source
488
	for (i = 0; i < sum; i++) {
4d26a735   Pedro Roque   Increased recogni...
489
490
		CHECK_TTL(ttl_ctr, 228)
		min += V_MIN(vs_prop_[i]);
94b2b13d   Pedro Roque   PHACT source
491
492
493
		max += V_MAX(vs_prop_[i]);
	}

4d26a735   Pedro Roque   Increased recogni...
494
	if (min == max && min == mins[sum] && V_N_VALS(vs_prop_[y_id]) == 1) {
94b2b13d   Pedro Roque   PHACT source
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
		*prop_ok = 0;
		return;
	}
}

#endif

CUDA_FUNC void sum_var_propagate(CL_INTS_MEM int* vs_per_c_idx, CL_MEMORY VARS_PROP* vs_prop_, CL_CS_MEM cl_constr* current_cs, CL_MEMORY unsigned short* vs_id_to_prop_,
		bool* prop_ok, __global int* terms_mem PROPAGATED_FUNC CS_IGNORE_FUNC TTL_CTR) {

#if CS_R_SUM_VAR == 0
	sum_var_prop(vs_per_c_idx, vs_prop_, current_cs, vs_id_to_prop_, prop_ok, terms_mem CS_IGNORE_CALL TTL_CTR_V);

#if CL_STATS == 1
	*propagated = true;
#endif

#elif CS_R_SUM_VAR == 1
	if (current_cs->reified == 1) {
		if (V_N_VALS(vs_prop_[current_cs->reif_var_id]) > 1) {
			sum_var_reif(vs_per_c_idx, vs_prop_, current_cs, vs_id_to_prop_, terms_mem CS_IGNORE_CALL TTL_CTR_V);

4d26a735   Pedro Roque   Increased recogni...
517
518
519
520
521
522
523
524
525
526
527
		} else {
			if (V_MIN(vs_prop_[current_cs->reif_var_id]) == 1) {
				sum_var_prop(vs_per_c_idx, vs_prop_, current_cs, vs_id_to_prop_, prop_ok, terms_mem CS_IGNORE_CALL TTL_CTR_V);
			} else {
				sum_var_prop_opposite(vs_per_c_idx, vs_prop_, current_cs, prop_ok, terms_mem TTL_CTR_V);
			}
#if CL_STATS == 1
			*propagated = true;
#endif
		}
	} else {
94b2b13d   Pedro Roque   PHACT source
528
529
530
		sum_var_prop(vs_per_c_idx, vs_prop_, current_cs, vs_id_to_prop_, prop_ok, terms_mem CS_IGNORE_CALL TTL_CTR_V);
#if CL_STATS == 1
		*propagated = true;
94b2b13d   Pedro Roque   PHACT source
531
532
533
534
535
536
#endif
	}
#endif
}

#endif