525{
527 register int i, j;
528 int size,
var, npermute, *permute, *weight, noweight;
529
530 if ((
cube.num_vars -
cube.num_binary_vars) <= 1) {
531 return;
532 }
534
535 for(var=
cube.num_binary_vars; var <
cube.num_vars-1; var++) {
536
537
538 npermute =
cube.part_size[
var];
539 permute =
ALLOC(
int, npermute);
540 for(i=0; i < npermute; i++) {
541 permute[i] =
cube.first_part[
var] + i;
542 }
545
546
547
548 noweight = 0;
549 for(i = 0; i < A->
count; i++) {
551 if (size == 1 || size == A->
sf_size) {
553 noweight++;
554 }
555 }
556
557
558
560 for(i = 0; i < A->
count; i++) {
562 }
563 for(i = 0; i < A->
count; i++) {
564 weight[i] = 0;
566 weight[i] = 1;
567 for(j = i+1; j < A->
count; j++) {
569 weight[i]++;
571 }
572 }
573 }
574 }
575
576
577
578 if (! output_symbolic) {
579 (void) fprintf(fp,
580 "# Symbolic constraints for variable %d (Numeric form)\n", var);
581 (void) fprintf(fp, "# unconstrained weight = %d\n", noweight);
582 (void) fprintf(fp,
"num_codes=%d\n",
cube.part_size[var]);
583 for(i = 0; i < A->
count; i++) {
584 if (weight[i] > 0) {
585 (void) fprintf(fp, "weight=%d: ", weight[i]);
586 for(j = 0; j < A->
sf_size; j++) {
588 (void) fprintf(fp, " %d", j);
589 }
590 }
591 (void) fprintf(fp, "\n");
592 }
593 }
594 } else {
595 (void) fprintf(fp,
596 "# Symbolic constraints for variable %d (Symbolic form)\n", var);
597 for(i = 0; i < A->
count; i++) {
598 if (weight[i] > 0) {
599 (void) fprintf(fp, "# w=%d: (", weight[i]);
600 for(j = 0; j < A->
sf_size; j++) {
602 (void) fprintf(fp, " %s",
604 }
605 }
606 (void) fprintf(fp, " )\n");
607 }
608 }
610 }
611 }
612}
#define GETSET(family, index)
struct set_family * pset_family