ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
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
20void fprint_pla(fp, PLA, output_type)
21INOUT FILE *fp;
22IN pPLA PLA;
23IN int output_type;
24{
25 int num;
26 register pcube last, p;
27
28 if ((output_type & CONSTRAINTS_type) != 0) {
30 output_type &= ~ CONSTRAINTS_type;
31 if (output_type == 0) {
32 return;
33 }
34 }
35
36 if ((output_type & SYMBOLIC_CONSTRAINTS_type) != 0) {
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
86void fpr_header(fp, PLA, output_type)
87FILE *fp;
88pPLA PLA;
89int 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
169void pls_output(PLA)
170IN 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
186void pls_group(PLA, fp)
187pPLA PLA;
188FILE *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
210void pls_label(PLA, fp)
211pPLA PLA;
212FILE *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*/
234void eqn_output(PLA)
235pPLA 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
284char *fmt_cube(c, out_map, s)
285register pcube c;
286register 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
311void print_cube(fp, c, out_map)
312register FILE *fp;
313register pcube c;
314register 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
342void print_expanded_cube(fp, c, phase)
343register FILE *fp;
344register pcube c;
345pcube 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
379char *pc1(c) pcube c;
380{static char s1[256];return fmt_cube(c, "01", s1);}
381char *pc2(c) pcube c;
382{static char s2[256];return fmt_cube(c, "01", s2);}
383
384
385void debug_print(T, name, level)
386pcube *T;
387char *name;
388int 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
407void debug1_print(T, name, num)
408pcover T;
409char *name;
410int 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
424void cprint(T)
425pcover T;
426{
427 register pcube p, last;
428
429 foreach_set(T, last, p)
430 (void) printf("%s\n", pc1(p));
431}
432
433
435pPLA 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
459void kiss_output(fp, PLA)
460FILE *fp;
461pPLA 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
474void kiss_print_cube(fp, PLA, p, out_string)
475FILE *fp;
476pPLA PLA;
477pcube p;
478char *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
521void output_symbolic_constraints(fp, PLA, output_symbolic)
522FILE *fp;
523pPLA PLA;
524int 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
#define TRUE
Definition abcBm.c:38
#define FALSE
Definition abcBm.c:37
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define ALLOC(type, num)
Definition avl.h:27
#define NIL(type)
Definition avl.h:25
#define FREE(obj)
Definition avl.h:31
#define pcover
Definition espresso.h:264
#define new_cube()
Definition espresso.h:262
char * pc1()
void fpr_header()
#define EQNTOTT_type
Definition espresso.h:341
struct PLA_t * pPLA
void output_symbolic_constraints()
#define is_in_set(set, e)
Definition espresso.h:170
void debug1_print()
#define TESTP(set, flag)
Definition espresso.h:124
#define PLEASURE_type
Definition espresso.h:340
void print_cube()
void print_expanded_cube()
void fatal()
#define KISS_type
Definition espresso.h:342
void cprint()
void debug_print()
#define F_type
Definition espresso.h:337
void pls_group()
#define INOUT
Definition espresso.h:334
#define DASH
Definition espresso.h:413
#define COVERED
Definition espresso.h:131
#define pcube
Definition espresso.h:261
pset_family sf_permute()
#define INLABEL(var)
Definition espresso.h:397
#define SYMBOLIC_CONSTRAINTS_type
Definition espresso.h:344
void PLA_labels()
#define GETSET(family, index)
Definition espresso.h:161
#define free_cube(r)
Definition espresso.h:263
pset_family sf_save()
char * pc2()
#define CONSTRAINTS_type
Definition espresso.h:343
char * fmt_cube()
#define R_type
Definition espresso.h:339
struct set_family * pset_family
#define foreach_set(R, last, p)
Definition espresso.h:135
#define SET(set, flag)
Definition espresso.h:122
bool verbose_debug
Definition globals.c:20
void eqn_output()
void sf_delset()
#define D_type
Definition espresso.h:338
#define OUTLABEL(pos)
Definition espresso.h:398
int set_ord()
void pls_output()
bool setp_implies()
#define IN
Definition espresso.h:332
#define ZERO
Definition espresso.h:415
#define RESET(set, flag)
Definition espresso.h:123
void pls_label()
unsigned int * pset
Definition espresso.h:73
pset set_or()
bool setp_equal()
void fprint_pla()
#define GETINPUT(c, pos)
Definition espresso.h:400
void kiss_print_cube()
void kiss_output()
#define CUBELISTSIZE(T)
Definition espresso.h:329
void makeup_labels()
Cube * p
Definition exorList.c:222
char * name
Definition main.h:24
char ** label
Definition espresso.h:321
pcover D
Definition espresso.h:316
pcube phase
Definition espresso.h:319
pcover F
Definition espresso.h:316
Definition exor.h:123
int count
Definition espresso.h:80
int sf_size
Definition espresso.h:78
int strlen()
char * sprintf()