25 int i, var, *paired, newvar;
26 int old_num_vars, old_num_binary_vars, old_size, old_mv_start;
27 int *new_part_size, new_num_vars, new_num_binary_vars, new_mv_start;
28 ppair pair = PLA->pair;
29 char scratch[1000], **oldlabel, *var1, *var1bar, *var2, *var2bar;
37 paired =
ALLOC(
bool,
cube.num_binary_vars);
38 for(var = 0; var <
cube.num_binary_vars; var++)
40 for(i = 0; i < pair->
cnt; i++)
41 if ((pair->
var1[i] > 0 && pair->
var1[i] <=
cube.num_binary_vars) &&
42 (pair->
var2[i] > 0 && pair->
var2[i] <=
cube.num_binary_vars)) {
46 fatal(
"can only pair binary-valued variables");
54 old_num_vars =
cube.num_vars;
55 old_num_binary_vars =
cube.num_binary_vars;
56 old_mv_start =
cube.first_part[
cube.num_binary_vars];
58 new_num_binary_vars = 0;
59 for(var = 0; var < old_num_binary_vars; var++)
60 new_num_binary_vars += (paired[var] ==
FALSE);
61 new_num_vars = new_num_binary_vars + pair->
cnt;
62 new_num_vars += old_num_vars - old_num_binary_vars;
63 new_part_size =
ALLOC(
int, new_num_vars);
64 for(var = 0; var < pair->
cnt; var++)
65 new_part_size[new_num_binary_vars + var] = 4;
66 for(var = 0; var < old_num_vars - old_num_binary_vars; var++)
67 new_part_size[new_num_binary_vars + pair->
cnt + var] =
68 cube.part_size[old_num_binary_vars + var];
71 cube.num_vars = new_num_vars;
72 cube.num_binary_vars = new_num_binary_vars;
73 cube.part_size = new_part_size;
78 oldlabel = PLA->label;
80 for(var = 0; var < pair->
cnt; var++) {
81 newvar =
cube.num_binary_vars*2 + var*4;
82 var1 = oldlabel[ (pair->
var1[var]-1) * 2 + 1];
83 var2 = oldlabel[ (pair->
var2[var]-1) * 2 + 1];
84 var1bar = oldlabel[ (pair->
var1[var]-1) * 2];
85 var2bar = oldlabel[ (pair->
var2[var]-1) * 2];
86 (void)
sprintf(scratch,
"%s+%s", var1bar, var2bar);
87 PLA->label[newvar] = util_strsav(scratch);
88 (void)
sprintf(scratch,
"%s+%s", var1bar, var2);
89 PLA->label[newvar+1] = util_strsav(scratch);
90 (void)
sprintf(scratch,
"%s+%s", var1, var2bar);
91 PLA->label[newvar+2] = util_strsav(scratch);
92 (void)
sprintf(scratch,
"%s+%s", var1, var2);
93 PLA->label[newvar+3] = util_strsav(scratch);
97 for(var = 0; var < old_num_binary_vars; var++) {
98 if (paired[var] ==
FALSE) {
99 PLA->label[2*i] = oldlabel[2*var];
100 PLA->label[2*i+1] = oldlabel[2*var+1];
101 oldlabel[2*var] = oldlabel[2*var+1] = (
char *) NULL;
106 new_mv_start =
cube.num_binary_vars*2 + pair->
cnt*4;
107 for(i = old_mv_start; i < old_size; i++) {
108 PLA->label[new_mv_start + i - old_mv_start] = oldlabel[i];
109 oldlabel[i] = (
char *) NULL;
112 for(i = 0; i < old_size; i++)
113 if (oldlabel[i] != (
char *) NULL)
119 for(var = 0; var < pair->
cnt; var++)
120 cube.sparse[
cube.num_binary_vars + var] = 0;
170 int run_length, var, offset = 0;
172 run =
FALSE; run_length = 0;
173 for(var = 0; var <
cube.num_binary_vars; var++)
176 run_length +=
cube.part_size[var];
179 first_run =
cube.first_part[var];
180 run_length =
cube.part_size[var];
184 A =
sf_delcol(A, first_run-offset, run_length);
186 offset += run_length;
189 A =
sf_delcol(A, first_run-offset, run_length);
267 int var1, var2, **cost_array;
269 int xnum_binary_vars = 0, xnum_vars = 0, *xpart_size = NULL, cost = 0;
271 pcover Fsave = NULL, Dsave = NULL, Rsave = NULL;
276 cost_array =
ALLOC(
int *,
cube.num_binary_vars);
277 for(i = 0; i <
cube.num_binary_vars; i++)
278 cost_array[i] =
ALLOC(
int,
cube.num_binary_vars);
279 for(i = 0; i <
cube.num_binary_vars; i++)
280 for(j = 0; j <
cube.num_binary_vars; j++)
281 cost_array[i][j] = 0;
287 for(var1 = 0; var1 <
cube.num_binary_vars-1; var1++) {
288 for(var2 = var1+1; var2 <
cube.num_binary_vars; var2++) {
297 xnum_binary_vars =
cube.num_binary_vars;
298 xnum_vars =
cube.num_vars;
300 for(i = 0; i <
cube.num_vars; i++)
301 xpart_size[i] =
cube.part_size[i];
304 PLA->pair->var1[0] = var1 + 1;
305 PLA->pair->var2[0] = var2 + 1;
315 cost = Fsave->count - PLA->F->count;
319 PLA->F =
espresso(PLA->F, PLA->D, PLA->R);
320 cost = Fsave->count - PLA->F->count;
324 PLA->F =
reduce(PLA->F, PLA->D);
327 cost = Fsave->count - PLA->F->count;
334 cost = PLA->F->count - T->count;
339 cost_array[var1][var2] = cost;
345 cube.num_binary_vars = xnum_binary_vars;
346 cube.num_vars = xnum_vars;
347 cube.part_size = xpart_size;
521 pcover Fsave, Dsave, Rsave;
522 int i, xnum_binary_vars, xnum_vars, *xpart_size;
525 Fsave =
sf_save(global_PLA->F);
526 Dsave =
sf_save(global_PLA->D);
527 Rsave =
sf_save(global_PLA->R);
530 xnum_binary_vars =
cube.num_binary_vars;
531 xnum_vars =
cube.num_vars;
533 for(i = 0; i <
cube.num_vars; i++)
534 xpart_size[i] =
cube.part_size[i];
537 global_PLA->pair = pair;
543 switch(pair_minim_strategy) {
547 printf(
"# phase is %s\n",
pc1(global_PLA->phase));
551 global_PLA->R, 1),
"EXACT ", global_PLA->F);
555 global_PLA->R),
"ESPRESSO ", global_PLA->F);
562 if (global_PLA->F->count < best_cost) {
563 best_cost = global_PLA->F->count;
565 best_phase = global_PLA->phase!=NULL?
set_save(global_PLA->phase):NULL;
566 if (best_F != NULL)
sf_free(best_F);
567 if (best_D != NULL)
sf_free(best_D);
568 if (best_R != NULL)
sf_free(best_R);
569 best_F =
sf_save(global_PLA->F);
570 best_D =
sf_save(global_PLA->D);
571 best_R =
sf_save(global_PLA->R);
577 cube.num_binary_vars = xnum_binary_vars;
578 cube.num_vars = xnum_vars;
579 cube.part_size = xpart_size;
586 global_PLA->F = Fsave;
587 global_PLA->D = Dsave;
588 global_PLA->R = Rsave;
589 global_PLA->pair = NULL;
590 global_PLA->phase = NULL;