abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cvrout.c
Go to the documentation of this file.
1 /*
2  * Revision Control Information
3  *
4  * $Source$
5  * $Author$
6  * $Revision$
7  * $Date$
8  *
9  */
10 /*
11  module: cvrout.c
12  purpose: cube and cover output routines
13 */
14 
15 #include "espresso.h"
16 
18 
19 
20 void fprint_pla(fp, PLA, output_type)
21 INOUT FILE *fp;
22 IN pPLA PLA;
23 IN int output_type;
24 {
25  int num;
26  register pcube last, p;
27 
28  if ((output_type & CONSTRAINTS_type) != 0) {
29  output_symbolic_constraints(fp, PLA, 0);
30  output_type &= ~ CONSTRAINTS_type;
31  if (output_type == 0) {
32  return;
33  }
34  }
35 
36  if ((output_type & SYMBOLIC_CONSTRAINTS_type) != 0) {
37  output_symbolic_constraints(fp, PLA, 1);
38  output_type &= ~ SYMBOLIC_CONSTRAINTS_type;
39  if (output_type == 0) {
40  return;
41  }
42  }
43 
44  if (output_type == PLEASURE_type) {
45  pls_output(PLA);
46  } else if (output_type == EQNTOTT_type) {
47  eqn_output(PLA);
48  } else if (output_type == KISS_type) {
49  kiss_output(fp, PLA);
50  } else {
51  fpr_header(fp, PLA, output_type);
52 
53  num = 0;
54  if (output_type & F_type) num += (PLA->F)->count;
55  if (output_type & D_type) num += (PLA->D)->count;
56  if (output_type & R_type) num += (PLA->R)->count;
57  (void) fprintf(fp, ".p %d\n", num);
58 
59  /* quick patch 01/17/85 to support TPLA ! */
60  if (output_type == F_type) {
61  foreach_set(PLA->F, last, p) {
62  print_cube(fp, p, "01");
63  }
64  (void) fprintf(fp, ".e\n");
65  } else {
66  if (output_type & F_type) {
67  foreach_set(PLA->F, last, p) {
68  print_cube(fp, p, "~1");
69  }
70  }
71  if (output_type & D_type) {
72  foreach_set(PLA->D, last, p) {
73  print_cube(fp, p, "~2");
74  }
75  }
76  if (output_type & R_type) {
77  foreach_set(PLA->R, last, p) {
78  print_cube(fp, p, "~0");
79  }
80  }
81  (void) fprintf(fp, ".end\n");
82  }
83  }
84 }
85 
86 void fpr_header(fp, PLA, output_type)
87 FILE *fp;
88 pPLA PLA;
89 int output_type;
90 {
91  register int i, var;
92  int first, last;
93 
94  /* .type keyword gives logical type */
95  if (output_type != F_type) {
96  (void) fprintf(fp, ".type ");
97  if (output_type & F_type) putc('f', fp);
98  if (output_type & D_type) putc('d', fp);
99  if (output_type & R_type) putc('r', fp);
100  putc('\n', fp);
101  }
102 
103  /* Check for binary or multiple-valued labels */
104  if (cube.num_mv_vars <= 1) {
105  (void) fprintf(fp, ".i %d\n", cube.num_binary_vars);
106  if (cube.output != -1)
107  (void) fprintf(fp, ".o %d\n", cube.part_size[cube.output]);
108  } else {
109  (void) fprintf(fp, ".mv %d %d", cube.num_vars, cube.num_binary_vars);
110  for(var = cube.num_binary_vars; var < cube.num_vars; var++)
111  (void) fprintf(fp, " %d", cube.part_size[var]);
112  (void) fprintf(fp, "\n");
113  }
114 
115  /* binary valued labels */
116  if (PLA->label != NIL(char *) && PLA->label[1] != NIL(char)
117  && cube.num_binary_vars > 0) {
118  (void) fprintf(fp, ".ilb");
119  for(var = 0; var < cube.num_binary_vars; var++)
120  /* see (NIL) OUTLABELS comment below */
121  if(INLABEL(var) == NIL(char)){
122  (void) fprintf(fp, " (null)");
123  }
124  else{
125  (void) fprintf(fp, " %s", INLABEL(var));
126  }
127  putc('\n', fp);
128  }
129 
130  /* output-part (last multiple-valued variable) labels */
131  if (PLA->label != NIL(char *) &&
132  PLA->label[cube.first_part[cube.output]] != NIL(char)
133  && cube.output != -1) {
134  (void) fprintf(fp, ".ob");
135  for(i = 0; i < cube.part_size[cube.output]; i++)
136  /* (NIL) OUTLABELS caused espresso to segfault under solaris */
137  if(OUTLABEL(i) == NIL(char)){
138  (void) fprintf(fp, " (null)");
139  }
140  else{
141  (void) fprintf(fp, " %s", OUTLABEL(i));
142  }
143  putc('\n', fp);
144  }
145 
146  /* multiple-valued labels */
147  for(var = cube.num_binary_vars; var < cube.num_vars-1; var++) {
148  first = cube.first_part[var];
149  last = cube.last_part[var];
150  if (PLA->label != NULL && PLA->label[first] != NULL) {
151  (void) fprintf(fp, ".label var=%d", var);
152  for(i = first; i <= last; i++) {
153  (void) fprintf(fp, " %s", PLA->label[i]);
154  }
155  putc('\n', fp);
156  }
157  }
158 
159  if (PLA->phase != (pcube) NULL) {
160  first = cube.first_part[cube.output];
161  last = cube.last_part[cube.output];
162  (void) fprintf(fp, "#.phase ");
163  for(i = first; i <= last; i++)
164  putc(is_in_set(PLA->phase,i) ? '1' : '0', fp);
165  (void) fprintf(fp, "\n");
166  }
167 }
168 
169 void pls_output(PLA)
170 IN pPLA PLA;
171 {
172  register pcube last, p;
173 
174  (void) printf(".option unmerged\n");
175  makeup_labels(PLA);
176  pls_label(PLA, stdout);
177  pls_group(PLA, stdout);
178  (void) printf(".p %d\n", PLA->F->count);
179  foreach_set(PLA->F, last, p) {
180  print_expanded_cube(stdout, p, PLA->phase);
181  }
182  (void) printf(".end\n");
183 }
184 
185 
186 void pls_group(PLA, fp)
187 pPLA PLA;
188 FILE *fp;
189 {
190  int var, i, col, len;
191 
192  (void) fprintf(fp, "\n.group");
193  col = 6;
194  for(var = 0; var < cube.num_vars-1; var++) {
195  (void) fprintf(fp, " ("), col += 2;
196  for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
197  len = strlen(PLA->label[i]);
198  if (col + len > 75)
199  (void) fprintf(fp, " \\\n"), col = 0;
200  else if (i != 0)
201  putc(' ', fp), col += 1;
202  (void) fprintf(fp, "%s", PLA->label[i]), col += len;
203  }
204  (void) fprintf(fp, ")"), col += 1;
205  }
206  (void) fprintf(fp, "\n");
207 }
208 
209 
210 void pls_label(PLA, fp)
211 pPLA PLA;
212 FILE *fp;
213 {
214  int var, i, col, len;
215 
216  (void) fprintf(fp, ".label");
217  col = 6;
218  for(var = 0; var < cube.num_vars; var++)
219  for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
220  len = strlen(PLA->label[i]);
221  if (col + len > 75)
222  (void) fprintf(fp, " \\\n"), col = 0;
223  else
224  putc(' ', fp), col += 1;
225  (void) fprintf(fp, "%s", PLA->label[i]), col += len;
226  }
227 }
228 
229 
230 
231 /*
232  eqntott output mode -- output algebraic equations
233 */
234 void eqn_output(PLA)
235 pPLA PLA;
236 {
237  register pcube p, last;
238  register int i, var, col, len;
239  int x;
240  bool firstand, firstor;
241 
242  if (cube.output == -1)
243  fatal("Cannot have no-output function for EQNTOTT output mode");
244  if (cube.num_mv_vars != 1)
245  fatal("Must have binary-valued function for EQNTOTT output mode");
246  makeup_labels(PLA);
247 
248  /* Write a single equation for each output */
249  for(i = 0; i < cube.part_size[cube.output]; i++) {
250  (void) printf("%s = ", OUTLABEL(i));
251  col = strlen(OUTLABEL(i)) + 3;
252  firstor = TRUE;
253 
254  /* Write product terms for each cube in this output */
255  foreach_set(PLA->F, last, p)
256  if (is_in_set(p, i + cube.first_part[cube.output])) {
257  if (firstor)
258  (void) printf("("), col += 1;
259  else
260  (void) printf(" | ("), col += 4;
261  firstor = FALSE;
262  firstand = TRUE;
263 
264  /* print out a product term */
265  for(var = 0; var < cube.num_binary_vars; var++)
266  if ((x=GETINPUT(p, var)) != DASH) {
267  len = strlen(INLABEL(var));
268  if (col+len > 72)
269  (void) printf("\n "), col = 4;
270  if (! firstand)
271  (void) printf("&"), col += 1;
272  firstand = FALSE;
273  if (x == ZERO)
274  (void) printf("!"), col += 1;
275  (void) printf("%s", INLABEL(var)), col += len;
276  }
277  (void) printf(")"), col += 1;
278  }
279  (void) printf(";\n\n");
280  }
281 }
282 
283 
284 char *fmt_cube(c, out_map, s)
285 register pcube c;
286 register char *out_map, *s;
287 {
288  register int i, var, last, len = 0;
289 
290  for(var = 0; var < cube.num_binary_vars; var++) {
291  s[len++] = "?01-" [GETINPUT(c, var)];
292  }
293  for(var = cube.num_binary_vars; var < cube.num_vars - 1; var++) {
294  s[len++] = ' ';
295  for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
296  s[len++] = "01" [is_in_set(c, i) != 0];
297  }
298  }
299  if (cube.output != -1) {
300  last = cube.last_part[cube.output];
301  s[len++] = ' ';
302  for(i = cube.first_part[cube.output]; i <= last; i++) {
303  s[len++] = out_map [is_in_set(c, i) != 0];
304  }
305  }
306  s[len] = '\0';
307  return s;
308 }
309 
310 
311 void print_cube(fp, c, out_map)
312 register FILE *fp;
313 register pcube c;
314 register char *out_map;
315 {
316  register int i, var, ch;
317  int last;
318 
319  for(var = 0; var < cube.num_binary_vars; var++) {
320  ch = "?01-" [GETINPUT(c, var)];
321  putc(ch, fp);
322  }
323  for(var = cube.num_binary_vars; var < cube.num_vars - 1; var++) {
324  putc(' ', fp);
325  for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
326  ch = "01" [is_in_set(c, i) != 0];
327  putc(ch, fp);
328  }
329  }
330  if (cube.output != -1) {
331  last = cube.last_part[cube.output];
332  putc(' ', fp);
333  for(i = cube.first_part[cube.output]; i <= last; i++) {
334  ch = out_map [is_in_set(c, i) != 0];
335  putc(ch, fp);
336  }
337  }
338  putc('\n', fp);
339 }
340 
341 
343 register FILE *fp;
344 register pcube c;
345 pcube phase;
346 {
347  register int i, var, ch;
348  char *out_map;
349 
350  for(var = 0; var < cube.num_binary_vars; var++) {
351  for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
352  ch = "~1" [is_in_set(c, i) != 0];
353  putc(ch, fp);
354  }
355  }
356  for(var = cube.num_binary_vars; var < cube.num_vars - 1; var++) {
357  for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
358  ch = "1~" [is_in_set(c, i) != 0];
359  putc(ch, fp);
360  }
361  }
362  if (cube.output != -1) {
363  var = cube.num_vars - 1;
364  putc(' ', fp);
365  for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
366  if (phase == (pcube) NULL || is_in_set(phase, i)) {
367  out_map = "~1";
368  } else {
369  out_map = "~0";
370  }
371  ch = out_map[is_in_set(c, i) != 0];
372  putc(ch, fp);
373  }
374  }
375  putc('\n', fp);
376 }
377 
378 
379 char *pc1(c) pcube c;
380 {static char s1[256];return fmt_cube(c, "01", s1);}
381 char *pc2(c) pcube c;
382 {static char s2[256];return fmt_cube(c, "01", s2);}
383 
384 
385 void debug_print(T, name, level)
386 pcube *T;
387 char *name;
388 int level;
389 {
390  register pcube *T1, p, temp;
391  register int cnt;
392 
393  cnt = CUBELISTSIZE(T);
394  temp = new_cube();
395  if (verbose_debug && level == 0)
396  (void) printf("\n");
397  (void) printf("%s[%d]: ord(T)=%d\n", name, level, cnt);
398  if (verbose_debug) {
399  (void) printf("cofactor=%s\n", pc1(T[0]));
400  for(T1 = T+2, cnt = 1; (p = *T1++) != (pcube) NULL; cnt++)
401  (void) printf("%4d. %s\n", cnt, pc1(set_or(temp, p, T[0])));
402  }
403  free_cube(temp);
404 }
405 
406 
407 void debug1_print(T, name, num)
408 pcover T;
409 char *name;
410 int num;
411 {
412  register int cnt = 1;
413  register pcube p, last;
414 
415  if (verbose_debug && num == 0)
416  (void) printf("\n");
417  (void) printf("%s[%d]: ord(T)=%d\n", name, num, T->count);
418  if (verbose_debug)
419  foreach_set(T, last, p)
420  (void) printf("%4d. %s\n", cnt++, pc1(p));
421 }
422 
423 
424 void cprint(T)
425 pcover T;
426 {
427  register pcube p, last;
428 
429  foreach_set(T, last, p)
430  (void) printf("%s\n", pc1(p));
431 }
432 
433 
434 void makeup_labels(PLA)
435 pPLA PLA;
436 {
437  int var, i, ind;
438 
439  if (PLA->label == (char **) NULL)
440  PLA_labels(PLA);
441 
442  for(var = 0; var < cube.num_vars; var++)
443  for(i = 0; i < cube.part_size[var]; i++) {
444  ind = cube.first_part[var] + i;
445  if (PLA->label[ind] == (char *) NULL) {
446  PLA->label[ind] = ALLOC(char, 15);
447  if (var < cube.num_binary_vars)
448  if ((i % 2) == 0)
449  (void) sprintf(PLA->label[ind], "v%d.bar", var);
450  else
451  (void) sprintf(PLA->label[ind], "v%d", var);
452  else
453  (void) sprintf(PLA->label[ind], "v%d.%d", var, i);
454  }
455  }
456 }
457 
458 
459 void kiss_output(fp, PLA)
460 FILE *fp;
461 pPLA PLA;
462 {
463  register pset last, p;
464 
465  foreach_set(PLA->F, last, p) {
466  kiss_print_cube(fp, PLA, p, "~1");
467  }
468  foreach_set(PLA->D, last, p) {
469  kiss_print_cube(fp, PLA, p, "~2");
470  }
471 }
472 
473 
474 void kiss_print_cube(fp, PLA, p, out_string)
475 FILE *fp;
476 pPLA PLA;
477 pcube p;
478 char *out_string;
479 {
480  register int i, var;
481  int part, x;
482 
483  for(var = 0; var < cube.num_binary_vars; var++) {
484  x = "?01-" [GETINPUT(p, var)];
485  putc(x, fp);
486  }
487 
488  for(var = cube.num_binary_vars; var < cube.num_vars - 1; var++) {
489  putc(' ', fp);
490  if (setp_implies(cube.var_mask[var], p)) {
491  putc('-', fp);
492  } else {
493  part = -1;
494  for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
495  if (is_in_set(p, i)) {
496  if (part != -1) {
497  fatal("more than 1 part in a symbolic variable\n");
498  }
499  part = i;
500  }
501  }
502  if (part == -1) {
503  putc('~', fp); /* no parts, hope its an output ... */
504  } else {
505  (void) fputs(PLA->label[part], fp);
506  }
507  }
508  }
509 
510  if ((var = cube.output) != -1) {
511  putc(' ', fp);
512  for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
513  x = out_string [is_in_set(p, i) != 0];
514  putc(x, fp);
515  }
516  }
517 
518  putc('\n', fp);
519 }
520 
521 void output_symbolic_constraints(fp, PLA, output_symbolic)
522 FILE *fp;
523 pPLA PLA;
524 int output_symbolic;
525 {
526  pset_family A;
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  }
533  makeup_labels(PLA);
534 
535  for(var=cube.num_binary_vars; var < cube.num_vars-1; var++) {
536 
537  /* pull out the columns for variable "var" */
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  }
543  A = sf_permute(sf_save(PLA->F), permute, npermute);
544  FREE(permute);
545 
546 
547  /* Delete the singletons and the full sets */
548  noweight = 0;
549  for(i = 0; i < A->count; i++) {
550  size = set_ord(GETSET(A,i));
551  if (size == 1 || size == A->sf_size) {
552  sf_delset(A, i--);
553  noweight++;
554  }
555  }
556 
557 
558  /* Count how many times each is duplicated */
559  weight = ALLOC(int, A->count);
560  for(i = 0; i < A->count; i++) {
561  RESET(GETSET(A, i), COVERED);
562  }
563  for(i = 0; i < A->count; i++) {
564  weight[i] = 0;
565  if (! TESTP(GETSET(A,i), COVERED)) {
566  weight[i] = 1;
567  for(j = i+1; j < A->count; j++) {
568  if (setp_equal(GETSET(A,i), GETSET(A,j))) {
569  weight[i]++;
570  SET(GETSET(A,j), COVERED);
571  }
572  }
573  }
574  }
575 
576 
577  /* Print out the constraints */
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++) {
587  if (is_in_set(GETSET(A,i), 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++) {
601  if (is_in_set(GETSET(A,i), j)) {
602  (void) fprintf(fp, " %s",
603  PLA->label[cube.first_part[var]+j]);
604  }
605  }
606  (void) fprintf(fp, " )\n");
607  }
608  }
609  FREE(weight);
610  }
611  }
612 }
614 
pset set_or()
void PLA_labels(pPLA PLA)
Definition: cvrin.c:665
void fatal(char *s)
Definition: cvrmisc.c:140
#define FALSE
Definition: cudd.h:91
#define new_cube()
Definition: espresso.h:262
char * pc1(pcube c)
Definition: cvrout.c:379
#define OUTLABEL(pos)
Definition: espresso.h:398
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define pcover
Definition: espresso.h:264
char * fmt_cube(pcube c, char *out_map, char *s)
Definition: cvrout.c:284
int var(Lit p)
Definition: SolverTypes.h:62
void print_cube(FILE *fp, pcube c, char *out_map)
Definition: cvrout.c:311
int count
Definition: espresso.h:80
void cprint(pcover T)
Definition: cvrout.c:424
char * pc2(pcube c)
Definition: cvrout.c:381
#define free_cube(r)
Definition: espresso.h:263
#define SET(set, flag)
Definition: espresso.h:122
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define RESET(set, flag)
Definition: espresso.h:123
#define ZERO
Definition: espresso.h:415
#define GETINPUT(c, pos)
Definition: espresso.h:400
#define INOUT
Definition: espresso.h:334
#define IN
Definition: espresso.h:332
#define EQNTOTT_type
Definition: espresso.h:341
bool setp_equal()
#define NIL(type)
Definition: avl.h:25
#define INLABEL(var)
Definition: espresso.h:397
#define CUBELISTSIZE(T)
Definition: espresso.h:329
void kiss_print_cube(FILE *fp, pPLA PLA, pcube p, char *out_string)
Definition: cvrout.c:474
#define ALLOC(type, num)
Definition: avl.h:27
#define COVERED
Definition: espresso.h:131
pset_family sf_permute()
void output_symbolic_constraints(FILE *fp, pPLA PLA, int output_symbolic)
Definition: cvrout.c:521
void pls_group(pPLA PLA, FILE *fp)
Definition: cvrout.c:186
char * name
int sf_size
Definition: espresso.h:78
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define FREE(obj)
Definition: avl.h:31
#define is_in_set(set, e)
Definition: espresso.h:170
#define CONSTRAINTS_type
Definition: espresso.h:343
static int size
Definition: cuddSign.c:86
unsigned int * pset
Definition: espresso.h:73
char * sprintf()
void pls_label(pPLA PLA, FILE *fp)
Definition: cvrout.c:210
static char s1[largest_string]
Definition: set.c:514
pcover F
Definition: espresso.h:316
ABC_NAMESPACE_IMPL_START void fprint_pla(INOUT FILE *fp, IN pPLA PLA, IN int output_type)
Definition: cvrout.c:20
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
#define SYMBOLIC_CONSTRAINTS_type
Definition: espresso.h:344
#define TRUE
Definition: cudd.h:88
void sf_delset()
void kiss_output(FILE *fp, pPLA PLA)
Definition: cvrout.c:459
static pcube phase
Definition: cvrm.c:405
void debug_print(pcube *T, char *name, int level)
Definition: cvrout.c:385
pcube phase
Definition: espresso.h:319
bool verbose_debug
Definition: globals.c:20
#define GETSET(family, index)
Definition: espresso.h:161
pcover D
Definition: espresso.h:316
void pls_output(IN pPLA PLA)
Definition: cvrout.c:169
void eqn_output(pPLA PLA)
Definition: cvrout.c:234
bool setp_implies()
void makeup_labels(pPLA PLA)
Definition: cvrout.c:434
#define D_type
Definition: espresso.h:338
#define DASH
Definition: espresso.h:413
#define TESTP(set, flag)
Definition: espresso.h:124
char ** label
Definition: espresso.h:321
#define F_type
Definition: espresso.h:337
int strlen()
void debug1_print(pcover T, char *name, int num)
Definition: cvrout.c:407
#define KISS_type
Definition: espresso.h:342
#define R_type
Definition: espresso.h:339
void print_expanded_cube(FILE *fp, pcube c, pcube phase)
Definition: cvrout.c:342
#define pcube
Definition: espresso.h:261
pset_family sf_save()
#define PLEASURE_type
Definition: espresso.h:340
int set_ord()
void fpr_header(FILE *fp, pPLA PLA, int output_type)
Definition: cvrout.c:86