ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
exact.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#include "espresso.h"
11
13
14
15
16static void dump_irredundant();
17static pcover do_minimize();
18
19
20/*
21 * minimize_exact -- main entry point for exact minimization
22 *
23 * Global flags which affect this routine are:
24 *
25 * debug
26 * skip_make_sparse
27 */
28
30minimize_exact(F, D, R, exact_cover)
31pcover F, D, R;
32int exact_cover;
33{
34 return do_minimize(F, D, R, exact_cover, /*weighted*/ 0);
35}
36
37
39minimize_exact_literals(F, D, R, exact_cover)
40pcover F, D, R;
41int exact_cover;
42{
43 return do_minimize(F, D, R, exact_cover, /*weighted*/ 1);
44}
45
46
47
48static pcover
49do_minimize(F, D, R, exact_cover, weighted)
50pcover F, D, R;
51int exact_cover;
52int weighted;
53{
54 pcover newF, E, Rt, Rp;
55 pset p, last;
56 int heur, level, *weights, i;
57 sm_matrix *table;
58 sm_row *cover;
59 sm_element *pe;
60 int debug_save = debug;
61
62 if (debug & EXACT) {
63 debug |= (IRRED | MINCOV);
64 }
65#if defined(sun) || defined(bsd4_2) /* hack ... */
66 if (debug & MINCOV) {
67 setlinebuf(stdout);
68 }
69#endif
70 level = (debug & MINCOV) ? 4 : 0;
71 heur = ! exact_cover;
72
73 /* Generate all prime implicants */
74 EXEC(F = primes_consensus(cube2list(F, D)), "PRIMES ", F);
75
76 /* Setup the prime implicant table */
77 EXEC(irred_split_cover(F, D, &E, &Rt, &Rp), "ESSENTIALS ", E);
78 EXEC(table = irred_derive_table(D, E, Rp), "PI-TABLE ", Rp);
79
80 /* Solve either a weighted or nonweighted covering problem */
81 if (weighted) {
82 /* correct only for all 2-valued variables */
83 weights = ALLOC(int, F->count);
84 foreach_set(Rp, last, p) {
85 weights[SIZE(p)] = cube.size - set_ord(p);
86 /* We have added the 0's in the output part instead of the 1's.
87 This loop corrects the literal count. */
88 for (i = cube.first_part[cube.output];
89 i <= cube.last_part[cube.output]; i++) {
90 is_in_set(p, i) ? weights[SIZE(p)]++ : weights[SIZE(p)]--;
91 }
92 }
93 } else {
94 weights = NIL(int);
95 }
96 EXEC(cover=sm_minimum_cover(table,weights,heur,level), "MINCOV ", F);
97 if (weights != 0) {
98 FREE(weights);
99 }
100
101 if (debug & EXACT) {
102 dump_irredundant(E, Rt, Rp, table);
103 }
104
105 /* Form the result cover */
106 newF = new_cover(100);
107 foreach_set(E, last, p) {
108 newF = sf_addset(newF, p);
109 }
110 sm_foreach_row_element(cover, pe) {
111 newF = sf_addset(newF, GETSET(F, pe->col_num));
112 }
113
114 free_cover(E);
115 free_cover(Rt);
116 free_cover(Rp);
117 sm_free(table);
118 sm_row_free(cover);
119 free_cover(F);
120
121 /* Attempt to make the results more sparse */
122 debug &= ~ (IRRED | SHARP | MINCOV);
123 if (! skip_make_sparse && R != 0) {
124 newF = make_sparse(newF, D, R);
125 }
126
127 debug = debug_save;
128 return newF;
129}
130
131static void
132dump_irredundant(E, Rt, Rp, table)
133pcover E, Rt, Rp;
134sm_matrix *table;
135{
136 FILE *fp_pi_table, *fp_primes;
137 pPLA PLA;
138 pset last, p;
139 char *file;
140
141 if (filename == 0 || strcmp(filename, "(stdin)") == 0) {
142 fp_pi_table = fp_primes = stdout;
143 } else {
144 file = ALLOC(char, strlen(filename)+20);
145 (void) sprintf(file, "%s.primes", filename);
146 if ((fp_primes = fopen(file, "w")) == NULL) {
147 (void) fprintf(stderr, "espresso: Unable to open %s\n", file);
148 fp_primes = stdout;
149 }
150 (void) sprintf(file, "%s.pi", filename);
151 if ((fp_pi_table = fopen(file, "w")) == NULL) {
152 (void) fprintf(stderr, "espresso: Unable to open %s\n", file);
153 fp_pi_table = stdout;
154 }
155 FREE(file);
156 }
157
158 PLA = new_PLA();
159 PLA_labels(PLA);
160
161 fpr_header(fp_primes, PLA, F_type);
162 free_PLA(PLA);
163
164 (void) fprintf(fp_primes, "# Essential primes are\n");
165 foreach_set(E, last, p) {
166 (void) fprintf(fp_primes, "%s\n", pc1(p));
167 }
168 (void) fprintf(fp_primes, "# Totally redundant primes are\n");
169 foreach_set(Rt, last, p) {
170 (void) fprintf(fp_primes, "%s\n", pc1(p));
171 }
172 (void) fprintf(fp_primes, "# Partially redundant primes are\n");
173 foreach_set(Rp, last, p) {
174 (void) fprintf(fp_primes, "%s\n", pc1(p));
175 }
176 if (fp_primes != stdout) {
177 (void) fclose(fp_primes);
178 }
179
180 sm_write(fp_pi_table, table);
181 if (fp_pi_table != stdout) {
182 (void) fclose(fp_pi_table);
183 }
184}
186
#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
pPLA new_PLA()
Definition cvrin.c:648
#define pcover
Definition espresso.h:264
pset_family sf_addset()
char * pc1()
void fpr_header()
pcover make_sparse()
pcover minimize_exact_literals()
struct PLA_t * pPLA
#define is_in_set(set, e)
Definition espresso.h:170
#define MINCOV
Definition espresso.h:362
pcube * cube2list()
#define F_type
Definition espresso.h:337
void free_PLA()
#define free_cover(r)
Definition espresso.h:266
void PLA_labels()
#define GETSET(family, index)
Definition espresso.h:161
bool skip_make_sparse
Definition globals.c:28
#define foreach_set(R, last, p)
Definition espresso.h:135
unsigned int debug
Definition globals.c:19
#define SIZE(set)
Definition espresso.h:112
pcover minimize_exact()
void irred_split_cover()
int set_ord()
sm_matrix * irred_derive_table()
#define SHARP
Definition espresso.h:364
unsigned int * pset
Definition espresso.h:73
#define EXEC(fct, name, S)
Definition espresso.h:418
char * filename
Definition globals.c:40
#define EXACT
Definition espresso.h:361
pcover primes_consensus()
#define new_cover(i)
Definition espresso.h:265
#define IRRED
Definition espresso.h:356
Cube * p
Definition exorList.c:222
sm_row * sm_minimum_cover()
typedefABC_NAMESPACE_HEADER_START struct sm_element_struct sm_element
Definition sparse.h:21
void sm_write()
void sm_row_free()
void sm_free()
#define sm_foreach_row_element(prow, p)
Definition sparse.h:103
struct sm_matrix_struct sm_matrix
Definition sparse.h:24
struct sm_row_struct sm_row
Definition sparse.h:22
Definition exor.h:123
Definition file.h:23
int strlen()
int strcmp()
char * sprintf()