ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
espresso.h
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 * espresso.h -- header file for Espresso-mv
12 */
13
14//#include "port.h"
15//#include "utility.h"
16#include "sparse.h"
17#include "mincov.h"
18
19#include "util_hack.h" // added
20
21#define ABC__misc__espresso__espresso_h
22#define print_time(t) util_print_time(t)
23
24#ifdef IBM_WATC
25#define void int
26#include "short.h"
27#endif
28
29#ifdef IBMPC /* set default options for IBM/PC */
30#define NO_INLINE
31#define BPI 16
32#endif
33
34/*-----THIS USED TO BE set.h----- */
35
36/*
37 * set.h -- definitions for packed arrays of bits
38 *
39 * This header file describes the data structures which comprise a
40 * facility for efficiently implementing packed arrays of bits
41 * (otherwise known as sets, cf. Pascal).
42 *
43 * A set is a vector of bits and is implemented here as an array of
44 * unsigned integers. The low order bits of set[0] give the index of
45 * the last word of set data. The higher order bits of set[0] are
46 * used to store data associated with the set. The set data is
47 * contained in elements set[1] ... set[LOOP(set)] as a packed bit
48 * array.
49 *
50 * A family of sets is a two-dimensional matrix of bits and is
51 * implemented with the data type "set_family".
52 *
53 * BPI == 32 and BPI == 16 have been tested and work.
54 */
55
56
57/* Define host machine characteristics of "unsigned int" */
58#ifndef ABC__misc__espresso__espresso_h
59#define BPI
60
61
63 32 /* # bits per integer */
64#endif
65
66#if BPI == 32
67#define LOGBPI 5 /* log(BPI)/log(2) */
68#else
69#define LOGBPI 4 /* log(BPI)/log(2) */
70#endif
71
72/* Define the set type */
73typedef unsigned int *pset;
74
75/* Define the set family type -- an array of sets */
76typedef struct set_family {
77 int wsize; /* Size of each set in 'ints' */
78 int sf_size; /* User declared set size */
79 int capacity; /* Number of sets allocated */
80 int count; /* The number of sets in the family */
81 int active_count; /* Number of "active" sets */
82 pset data; /* Pointer to the set data */
83 struct set_family *next; /* For garbage collection */
85
86/* Macros to set and test single elements */
87#define WHICH_WORD(element) (((element) >> LOGBPI) + 1)
88#define WHICH_BIT(element) ((element) & (BPI-1))
89
90/* # of ints needed to allocate a set with "size" elements */
91#if BPI == 32
92#define SET_SIZE(size) ((size) <= BPI ? 2 : (WHICH_WORD((size)-1) + 1))
93#else
94#define SET_SIZE(size) ((size) <= BPI ? 3 : (WHICH_WORD((size)-1) + 2))
95#endif
96
97/*
98 * Three fields are maintained in the first word of the set
99 * LOOP is the index of the last word used for set data
100 * LOOPCOPY is the index of the last word in the set
101 * SIZE is available for general use (e.g., recording # elements in set)
102 * NELEM retrieves the number of elements in the set
103 */
104#define LOOP(set) (set[0] & 0x03ff)
105#define PUTLOOP(set, i) (set[0] &= ~0x03ff, set[0] |= (i))
106#if BPI == 32
107#define LOOPCOPY(set) LOOP(set)
108#define SIZE(set) (set[0] >> 16)
109#define PUTSIZE(set, size) (set[0] &= 0xffff, set[0] |= ((size) << 16))
110#else
111#define LOOPCOPY(set) (LOOP(set) + 1)
112#define SIZE(set) (set[LOOP(set)+1])
113#define PUTSIZE(set, size) ((set[LOOP(set)+1]) = (size))
114#endif
115
116#define NELEM(set) (BPI * LOOP(set))
117#define LOOPINIT(size) ((size <= BPI) ? 1 : WHICH_WORD((size)-1))
118
119/*
120 * FLAGS store general information about the set
121 */
122#define SET(set, flag) (set[0] |= (flag))
123#define RESET(set, flag) (set[0] &= ~ (flag))
124#define TESTP(set, flag) (set[0] & (flag))
125
126/* Flag definitions are ... */
127#define PRIME 0x8000 /* cube is prime */
128#define NONESSEN 0x4000 /* cube cannot be essential prime */
129#define ACTIVE 0x2000 /* cube is still active */
130#define REDUND 0x1000 /* cube is redundant(at this point) */
131#define COVERED 0x0800 /* cube has been covered */
132#define RELESSEN 0x0400 /* cube is relatively essential */
133
134/* Most efficient way to look at all members of a set family */
135#define foreach_set(R, last, p)\
136 for(p=R->data,last=p+R->count*R->wsize;p<last;p+=R->wsize)
137#define foreach_remaining_set(R, last, pfirst, p)\
138 for(p=pfirst+R->wsize,last=R->data+R->count*R->wsize;p<last;p+=R->wsize)
139#define foreach_active_set(R, last, p)\
140 foreach_set(R,last,p) if (TESTP(p, ACTIVE))
141
142/* Another way that also keeps the index of the current set member in i */
143#define foreachi_set(R, i, p)\
144 for(p=R->data,i=0;i<R->count;p+=R->wsize,i++)
145#define foreachi_active_set(R, i, p)\
146 foreachi_set(R,i,p) if (TESTP(p, ACTIVE))
147
148/* Looping over all elements in a set:
149 * foreach_set_element(pset p, int i, unsigned val, int base) {
150 * .
151 * .
152 * .
153 * }
154 */
155#define foreach_set_element(p, i, val, base) \
156 for(i = LOOP(p); i > 0; ) \
157 for(val = p[i], base = --i << LOGBPI; val != 0; base++, val >>= 1) \
158 if (val & 1)
159
160/* Return a pointer to a given member of a set family */
161#define GETSET(family, index) ((family)->data + (family)->wsize * (index))
162
163/* Allocate and deallocate sets */
164#define set_new(size) set_clear(ALLOC(unsigned int, SET_SIZE(size)), size)
165#define set_full(size) set_fill(ALLOC(unsigned int, SET_SIZE(size)), size)
166#define set_save(r) set_copy(ALLOC(unsigned int, SET_SIZE(NELEM(r))), r)
167#define set_free(r) FREE(r)
168
169/* Check for set membership, remove set element and insert set element */
170#define is_in_set(set, e) (set[WHICH_WORD(e)] & (1 << WHICH_BIT(e)))
171#define set_remove(set, e) (set[WHICH_WORD(e)] &= ~ (1 << WHICH_BIT(e)))
172#define set_insert(set, e) (set[WHICH_WORD(e)] |= 1 << WHICH_BIT(e))
173
174/* Inline code substitution for those places that REALLY need it on a VAX */
175#ifdef NO_INLINE
176#define INLINEset_copy(r, a) (void) set_copy(r,a)
177#define INLINEset_clear(r, size) (void) set_clear(r, size)
178#define INLINEset_fill(r, size) (void) set_fill(r, size)
179#define INLINEset_and(r, a, b) (void) set_and(r, a, b)
180#define INLINEset_or(r, a, b) (void) set_or(r, a, b)
181#define INLINEset_diff(r, a, b) (void) set_diff(r, a, b)
182#define INLINEset_ndiff(r, a, b, f) (void) set_ndiff(r, a, b, f)
183#define INLINEset_xor(r, a, b) (void) set_xor(r, a, b)
184#define INLINEset_xnor(r, a, b, f) (void) set_xnor(r, a, b, f)
185#define INLINEset_merge(r, a, b, mask) (void) set_merge(r, a, b, mask)
186#define INLINEsetp_implies(a, b, when_false) \
187 if (! setp_implies(a,b)) when_false
188#define INLINEsetp_disjoint(a, b, when_false) \
189 if (! setp_disjoint(a,b)) when_false
190#define INLINEsetp_equal(a, b, when_false) \
191 if (! setp_equal(a,b)) when_false
192
193#else
194
195#define INLINEset_copy(r, a)\
196 {register int i_=LOOPCOPY(a); do r[i_]=a[i_]; while (--i_>=0);}
197#define INLINEset_clear(r, size)\
198 {register int i_=LOOPINIT(size); *r=i_; do r[i_] = 0; while (--i_ > 0);}
199#define INLINEset_fill(r, size)\
200 {register int i_=LOOPINIT(size); *r=i_; \
201 r[i_]=((unsigned int)(~0))>>(i_*BPI-size); while(--i_>0) r[i_]=~0;}
202#define INLINEset_and(r, a, b)\
203 {register int i_=LOOP(a); PUTLOOP(r,i_);\
204 do r[i_] = a[i_] & b[i_]; while (--i_>0);}
205#define INLINEset_or(r, a, b)\
206 {register int i_=LOOP(a); PUTLOOP(r,i_);\
207 do r[i_] = a[i_] | b[i_]; while (--i_>0);}
208#define INLINEset_diff(r, a, b)\
209 {register int i_=LOOP(a); PUTLOOP(r,i_);\
210 do r[i_] = a[i_] & ~ b[i_]; while (--i_>0);}
211#define INLINEset_ndiff(r, a, b, fullset)\
212 {register int i_=LOOP(a); PUTLOOP(r,i_);\
213 do r[i_] = fullset[i_] & (a[i_] | ~ b[i_]); while (--i_>0);}
214#ifdef IBM_WATC
215#define INLINEset_xor(r, a, b) (void) set_xor(r, a, b)
216#define INLINEset_xnor(r, a, b, f) (void) set_xnor(r, a, b, f)
217#else
218#define INLINEset_xor(r, a, b)\
219 {register int i_=LOOP(a); PUTLOOP(r,i_);\
220 do r[i_] = a[i_] ^ b[i_]; while (--i_>0);}
221#define INLINEset_xnor(r, a, b, fullset)\
222 {register int i_=LOOP(a); PUTLOOP(r,i_);\
223 do r[i_] = fullset[i_] & ~ (a[i_] ^ b[i_]); while (--i_>0);}
224#endif
225#define INLINEset_merge(r, a, b, mask)\
226 {register int i_=LOOP(a); PUTLOOP(r,i_);\
227 do r[i_] = (a[i_]&mask[i_]) | (b[i_]&~mask[i_]); while (--i_>0);}
228#define INLINEsetp_implies(a, b, when_false)\
229 {register int i_=LOOP(a); do if (a[i_]&~b[i_]) break; while (--i_>0);\
230 if (i_ != 0) when_false;}
231#define INLINEsetp_disjoint(a, b, when_false)\
232 {register int i_=LOOP(a); do if (a[i_]&b[i_]) break; while (--i_>0);\
233 if (i_ != 0) when_false;}
234#define INLINEsetp_equal(a, b, when_false)\
235 {register int i_=LOOP(a); do if (a[i_]!=b[i_]) break; while (--i_>0);\
236 if (i_ != 0) when_false;}
237
238#endif
239
240#if BPI == 32
241#define count_ones(v)\
242 (bit_count[v & 255] + bit_count[(v >> 8) & 255]\
243 + bit_count[(v >> 16) & 255] + bit_count[(v >> 24) & 255])
244#else
245#define count_ones(v) (bit_count[v & 255] + bit_count[(v >> 8) & 255])
246#endif
247
248/* Table for efficient bit counting */
249extern int bit_count[256];
250/*----- END OF set.h ----- */
251
252
253/* Define a boolean type */
254#define bool int
255#define FALSE 0
256#define TRUE 1
257#define MAYBE 2
258#define print_bool(x) ((x) == 0 ? "FALSE" : ((x) == 1 ? "TRUE" : "MAYBE"))
259
260/* Map many cube/cover types/routines into equivalent set types/routines */
261#define pcube pset
262#define new_cube() set_new(cube.size)
263#define free_cube(r) set_free(r)
264#define pcover pset_family
265#define new_cover(i) sf_new(i, cube.size)
266#define free_cover(r) sf_free(r)
267#define free_cubelist(T) FREE(T[0]); FREE(T);
268
269
270/* cost_t describes the cost of a cover */
271typedef struct cost_struct {
272 int cubes; /* number of cubes in the cover */
273 int in; /* transistor count, binary-valued variables */
274 int out; /* transistor count, output part */
275 int mv; /* transistor count, multiple-valued vars */
276 int total; /* total number of transistors */
277 int primes; /* number of prime cubes */
279
280
281/* pair_t describes bit-paired variables */
282typedef struct pair_struct {
283 int cnt;
284 int *var1;
285 int *var2;
287
288
289/* symbolic_list_t describes a single ".symbolic" line */
295
296
297/* symbolic_list_t describes a single ".symbolic" line */
302
303
304/* symbolic_t describes a linked list of ".symbolic" lines */
305typedef struct symbolic_struct {
306 symbolic_list_t *symbolic_list; /* linked list of items */
307 int symbolic_list_length; /* length of symbolic_list list */
308 symbolic_label_t *symbolic_label; /* linked list of new names */
309 int symbolic_label_length; /* length of symbolic_label list */
312
313
314/* PLA_t stores the logical representation of a PLA */
315typedef struct {
316 pcover F, D, R; /* on-set, off-set and dc-set */
317 char *filename; /* filename */
318 int pla_type; /* logical PLA format */
319 pcube phase; /* phase to split into on-set and off-set */
320 ppair pair; /* how to pair variables */
321 char **label; /* labels for the columns */
322 symbolic_t *symbolic; /* allow binary->symbolic mapping */
323 symbolic_t *symbolic_output;/* allow symbolic output mapping */
325
326#define equal(a,b) (strcmp(a,b) == 0)
327
328/* This is a hack which I wish I hadn't done, but too painful to change */
329#define CUBELISTSIZE(T) (((pcube *) T[1] - T) - 3)
330
331/* For documentation purposes */
332#define IN
333#define OUT
334#define INOUT
335
336/* The pla_type field describes the input and output format of the PLA */
337#define F_type 1
338#define D_type 2
339#define R_type 4
340#define PLEASURE_type 8 /* output format */
341#define EQNTOTT_type 16 /* output format algebraic eqns */
342#define KISS_type 128 /* output format kiss */
343#define CONSTRAINTS_type 256 /* output the constraints (numeric) */
344#define SYMBOLIC_CONSTRAINTS_type 512 /* output the constraints (symbolic) */
345#define FD_type (F_type | D_type)
346#define FR_type (F_type | R_type)
347#define DR_type (D_type | R_type)
348#define FDR_type (F_type | D_type | R_type)
349
350/* Definitions for the debug variable */
351#define COMPL 0x0001
352#define ESSEN 0x0002
353#define EXPAND 0x0004
354#define EXPAND1 0x0008
355#define GASP 0x0010
356#define IRRED 0x0020
357#define REDUCE 0x0040
358#define REDUCE1 0x0080
359#define SPARSE 0x0100
360#define TAUT 0x0200
361#define EXACT 0x0400
362#define MINCOV 0x0800
363#define MINCOV1 0x1000
364#define SHARP 0x2000
365#define IRRED1 0x4000
366
367#define VERSION\
368 "UC Berkeley, Espresso Version #2.3, Release date 01/31/88"
369
370/* Define constants used for recording program statistics */
371#define TIME_COUNT 16
372#define READ_TIME 0
373#define COMPL_TIME 1
374#define ONSET_TIME 2
375#define ESSEN_TIME 3
376#define EXPAND_TIME 4
377#define IRRED_TIME 5
378#define REDUCE_TIME 6
379#define GEXPAND_TIME 7
380#define GIRRED_TIME 8
381#define GREDUCE_TIME 9
382#define PRIMES_TIME 10
383#define MINCOV_TIME 11
384#define MV_REDUCE_TIME 12
385#define RAISE_IN_TIME 13
386#define VERIFY_TIME 14
387#define WRITE_TIME 15
388
389
390/* For those who like to think about PLAs, macros to get at inputs/outputs */
391#define NUMINPUTS cube.num_binary_vars
392#define NUMOUTPUTS cube.part_size[cube.num_vars - 1]
393
394#define POSITIVE_PHASE(pos)\
395 (is_in_set(PLA->phase, cube.first_part[cube.output]+pos) != 0)
396
397#define INLABEL(var) PLA->label[cube.first_part[var] + 1]
398#define OUTLABEL(pos) PLA->label[cube.first_part[cube.output] + pos]
399
400#define GETINPUT(c, pos)\
401 ((c[WHICH_WORD(2*pos)] >> WHICH_BIT(2*pos)) & 3)
402#define GETOUTPUT(c, pos)\
403 (is_in_set(c, cube.first_part[cube.output] + pos) != 0)
404
405#define PUTINPUT(c, pos, value)\
406 c[WHICH_WORD(2*pos)] = (c[WHICH_WORD(2*pos)] & ~(3 << WHICH_BIT(2*pos)))\
407 | (value << WHICH_BIT(2*pos))
408#define PUTOUTPUT(c, pos, value)\
409 c[WHICH_WORD(pos)] = (c[WHICH_WORD(pos)] & ~(1 << WHICH_BIT(pos)))\
410 | (value << WHICH_BIT(pos))
411
412#define TWO 3
413#define DASH 3
414#define ONE 2
415#define ZERO 1
416
417
418#define EXEC(fct, name, S)\
419 {long t=ptime();fct;if(trace)print_trace(S,name,ptime()-t);}
420#define EXEC_S(fct, name, S)\
421 {long t=ptime();fct;if(summary)print_trace(S,name,ptime()-t);}
422#define EXECUTE(fct,i,S,cost)\
423 {long t=ptime();fct;totals(t,i,S,&(cost));}
424
425/*
426 * Global Variable Declarations
427 */
428
429extern unsigned int debug; /* debug parameter */
430extern bool verbose_debug; /* -v: whether to print a lot */
431extern char *total_name[TIME_COUNT]; /* basic function names */
432extern long total_time[TIME_COUNT]; /* time spent in basic fcts */
433extern int total_calls[TIME_COUNT]; /* # calls to each fct */
434
435extern bool echo_comments; /* turned off by -eat option */
436extern bool echo_unknown_commands; /* always true ?? */
437extern bool force_irredundant; /* -nirr command line option */
438extern bool skip_make_sparse;
439extern bool kiss; /* -kiss command line option */
440extern bool pos; /* -pos command line option */
441extern bool print_solution; /* -x command line option */
442extern bool recompute_onset; /* -onset command line option */
443extern bool remove_essential; /* -ness command line option */
444extern bool single_expand; /* -fast command line option */
445extern bool summary; /* -s command line option */
446extern bool trace; /* -t command line option */
447extern bool unwrap_onset; /* -nunwrap command line option */
448extern bool use_random_order; /* -random command line option */
449extern bool use_super_gasp; /* -strong command line option */
450extern char *filename; /* filename PLA was read from */
451extern bool debug_exact_minimization; /* dumps info for -do exact */
452
453
454/*
455 * pla_types are the input and output types for reading/writing a PLA
456 */
458 char *key;
459 int value;
460};
461
462
463/*
464 * The cube structure is a global structure which contains information
465 * on how a set maps into a cube -- i.e., number of parts per variable,
466 * number of variables, etc. Also, many fields are pre-computed to
467 * speed up various primitive operations.
468 */
469#define CUBE_TEMP 10
470
472 int size; /* set size of a cube */
473 int num_vars; /* number of variables in a cube */
474 int num_binary_vars; /* number of binary variables */
475 int *first_part; /* first element of each variable */
476 int *last_part; /* first element of each variable */
477 int *part_size; /* number of elements in each variable */
478 int *first_word; /* first word for each variable */
479 int *last_word; /* last word for each variable */
480 pset binary_mask; /* Mask to extract binary variables */
481 pset mv_mask; /* mask to get mv parts */
482 pset *var_mask; /* mask to extract a variable */
483 pset *temp; /* an array of temporary sets */
484 pset fullset; /* a full cube */
485 pset emptyset; /* an empty cube */
486 unsigned int inmask; /* mask to get odd word of binary part */
487 int inword; /* which word number for above */
488 int *sparse; /* should this variable be sparse? */
489 int num_mv_vars; /* number of multiple-valued variables */
490 int output; /* which variable is "output" (-1 if none) */
491};
492
494 int *part_zeros; /* count of zeros for each element */
495 int *var_zeros; /* count of zeros for each variable */
496 int *parts_active; /* number of "active" parts for each var */
497 bool *is_unate; /* indicates given var is unate */
498 int vars_active; /* number of "active" variables */
499 int vars_unate; /* number of unate variables */
500 int best; /* best "binate" variable */
501};
502
503
504extern struct pla_types_struct pla_types[];
505extern struct cube_struct cube, temp_cube_save;
506extern struct cdata_struct cdata, temp_cdata_save;
507
508#ifdef lint
509#define DISJOINT 0x5555
510#else
511#if BPI == 32
512#define DISJOINT 0x55555555
513#else
514#define DISJOINT 0x5555
515#endif
516
517
519
520#endif
521
522/* function declarations */
523
524/* cofactor.c */ extern int binate_split_select();
525/* cofactor.c */ extern pcover cubeunlist();
526/* cofactor.c */ extern pcube *cofactor();
527/* cofactor.c */ extern pcube *cube1list();
528/* cofactor.c */ extern pcube *cube2list();
529/* cofactor.c */ extern pcube *cube3list();
530/* cofactor.c */ extern pcube *scofactor();
531/* cofactor.c */ extern void massive_count();
532/* compl.c */ extern pcover complement();
533/* compl.c */ extern pcover simplify();
534/* compl.c */ extern void simp_comp();
535/* contain.c */ extern int d1_rm_equal();
536/* contain.c */ extern int rm2_contain();
537/* contain.c */ extern int rm2_equal();
538/* contain.c */ extern int rm_contain();
539/* contain.c */ extern int rm_equal();
540/* contain.c */ extern int rm_rev_contain();
541/* contain.c */ extern pset *sf_list();
542/* contain.c */ extern pset *sf_sort();
543/* contain.c */ extern pset_family d1merge();
544/* contain.c */ extern pset_family dist_merge();
545/* contain.c */ extern pset_family sf_contain();
546/* contain.c */ extern pset_family sf_dupl();
547/* contain.c */ extern pset_family sf_ind_contain();
548/* contain.c */ extern pset_family sf_ind_unlist();
549/* contain.c */ extern pset_family sf_merge();
550/* contain.c */ extern pset_family sf_rev_contain();
551/* contain.c */ extern pset_family sf_union();
552/* contain.c */ extern pset_family sf_unlist();
553/* cubestr.c */ extern void cube_setup();
554/* cubestr.c */ extern void restore_cube_struct();
555/* cubestr.c */ extern void save_cube_struct();
556/* cubestr.c */ extern void setdown_cube();
557/* cvrin.c */ extern void PLA_labels();
558/* cvrin.c */ extern char *get_word();
559/* cvrin.c */ extern int label_index();
560/* cvrin.c */ extern int read_pla();
561/* cvrin.c */ extern int read_symbolic();
562/* cvrin.c */ extern pPLA new_PLA();
563/* cvrin.c */ extern void PLA_summary();
564/* cvrin.c */ extern void free_PLA();
565/* cvrin.c */ extern void parse_pla();
566/* cvrin.c */ extern void read_cube();
567/* cvrin.c */ extern void skip_line();
568/* cvrm.c */ extern void foreach_output_function();
569/* cvrm.c */ extern int cubelist_partition();
570/* cvrm.c */ extern int so_both_do_espresso();
571/* cvrm.c */ extern int so_both_do_exact();
572/* cvrm.c */ extern int so_both_save();
573/* cvrm.c */ extern int so_do_espresso();
574/* cvrm.c */ extern int so_do_exact();
575/* cvrm.c */ extern int so_save();
576/* cvrm.c */ extern pcover cof_output();
577/* cvrm.c */ extern pcover lex_sort();
578/* cvrm.c */ extern pcover mini_sort();
579/* cvrm.c */ extern pcover random_order();
580/* cvrm.c */ extern pcover size_sort();
581/* cvrm.c */ extern pcover sort_reduce();
582/* cvrm.c */ extern pcover uncof_output();
583/* cvrm.c */ extern pcover unravel();
584/* cvrm.c */ extern pcover unravel_range();
585/* cvrm.c */ extern void so_both_espresso();
586/* cvrm.c */ extern void so_espresso();
587/* cvrmisc.c */ extern char *fmt_cost();
588/* cvrmisc.c */ extern char *print_cost();
589/* cvrmisc.c */ extern char *strsav();
590/* cvrmisc.c */ extern void copy_cost();
591/* cvrmisc.c */ extern void cover_cost();
592/* cvrmisc.c */ extern void fatal();
593/* cvrmisc.c */ extern void print_trace();
594/* cvrmisc.c */ extern void size_stamp();
595/* cvrmisc.c */ extern void totals();
596/* cvrout.c */ extern char *fmt_cube();
597/* cvrout.c */ extern char *fmt_expanded_cube();
598/* cvrout.c */ extern char *pc1();
599/* cvrout.c */ extern char *pc2();
600/* cvrout.c */ extern char *pc3();
601/* cvrout.c */ extern void makeup_labels();
602/* cvrout.c */ extern void kiss_output();
603/* cvrout.c */ extern void kiss_print_cube();
604/* cvrout.c */ extern void output_symbolic_constraints();
605/* cvrout.c */ extern void cprint();
606/* cvrout.c */ extern void debug1_print();
607/* cvrout.c */ extern void debug_print();
608/* cvrout.c */ extern void eqn_output();
609/* cvrout.c */ extern void fpr_header();
610/* cvrout.c */ extern void fprint_pla();
611/* cvrout.c */ extern void pls_group();
612/* cvrout.c */ extern void pls_label();
613/* cvrout.c */ extern void pls_output();
614/* cvrout.c */ extern void print_cube();
615/* cvrout.c */ extern void print_expanded_cube();
616/* cvrout.c */ extern void sf_debug_print();
617/* equiv.c */ extern void find_equiv_outputs();
618/* equiv.c */ extern int check_equiv();
619/* espresso.c */ extern pcover espresso();
620/* essen.c */ extern bool essen_cube();
621/* essen.c */ extern pcover cb_consensus();
622/* essen.c */ extern pcover cb_consensus_dist0();
623/* essen.c */ extern pcover essential();
624/* exact.c */ extern pcover minimize_exact();
625/* exact.c */ extern pcover minimize_exact_literals();
626/* expand.c */ extern bool feasibly_covered();
627/* expand.c */ extern int most_frequent();
628/* expand.c */ extern pcover all_primes();
629/* expand.c */ extern pcover expand();
630/* expand.c */ extern pcover find_all_primes();
631/* expand.c */ extern void elim_lowering();
632/* expand.c */ extern void essen_parts();
633/* expand.c */ extern void essen_raising();
634/* expand.c */ extern void expand1();
635/* expand.c */ extern void mincov();
636/* expand.c */ extern void select_feasible();
637/* expand.c */ extern void setup_BB_CC();
638/* gasp.c */ extern pcover expand_gasp();
639/* gasp.c */ extern pcover irred_gasp();
640/* gasp.c */ extern pcover last_gasp();
641/* gasp.c */ extern pcover super_gasp();
642/* gasp.c */ extern void expand1_gasp();
643/* getopt.c */ extern int util_getopt();
644/* hack.c */ extern void find_dc_inputs();
645/* hack.c */ extern void find_inputs();
646/* hack.c */ extern void form_bitvector();
647/* hack.c */ extern void map_dcset();
648/* hack.c */ extern void map_output_symbolic();
649/* hack.c */ extern void map_symbolic();
650/* hack.c */ extern pcover map_symbolic_cover();
651/* hack.c */ extern void symbolic_hack_labels();
652/* irred.c */ extern bool cube_is_covered();
653/* irred.c */ extern bool taut_special_cases();
654/* irred.c */ extern bool tautology();
655/* irred.c */ extern pcover irredundant();
656/* irred.c */ extern void mark_irredundant();
657/* irred.c */ extern void irred_split_cover();
658/* irred.c */ extern sm_matrix *irred_derive_table();
659/* map.c */ extern pset minterms();
660/* map.c */ extern void explode();
661/* map.c */ extern void map();
662/* opo.c */ extern void output_phase_setup();
663/* opo.c */ extern pPLA set_phase();
664/* opo.c */ extern pcover opo();
665/* opo.c */ extern pcube find_phase();
666/* opo.c */ extern pset_family find_covers();
667/* opo.c */ extern pset_family form_cover_table();
668/* opo.c */ extern pset_family opo_leaf();
669/* opo.c */ extern pset_family opo_recur();
670/* opo.c */ extern void opoall();
671/* opo.c */ extern void phase_assignment();
672/* opo.c */ extern void repeated_phase_assignment();
673/* pair.c */ extern void generate_all_pairs();
674/* pair.c */ extern int **find_pairing_cost();
675/* pair.c */ extern void find_best_cost();
676/* pair.c */ extern int greedy_best_cost();
677/* pair.c */ extern void minimize_pair();
678/* pair.c */ extern void pair_free();
679/* pair.c */ extern void pair_all();
680/* pair.c */ extern pcover delvar();
681/* pair.c */ extern pcover pairvar();
682/* pair.c */ extern ppair pair_best_cost();
683/* pair.c */ extern ppair pair_new();
684/* pair.c */ extern ppair pair_save();
685/* pair.c */ extern void print_pair();
686/* pair.c */ extern void find_optimal_pairing();
687/* pair.c */ extern void set_pair();
688/* pair.c */ extern void set_pair1();
689/* primes.c */ extern pcover primes_consensus();
690/* reduce.c */ extern bool sccc_special_cases();
691/* reduce.c */ extern pcover reduce();
692/* reduce.c */ extern pcube reduce_cube();
693/* reduce.c */ extern pcube sccc();
694/* reduce.c */ extern pcube sccc_cube();
695/* reduce.c */ extern pcube sccc_merge();
696/* set.c */ extern bool set_andp();
697/* set.c */ extern bool set_orp();
698/* set.c */ extern bool setp_disjoint();
699/* set.c */ extern bool setp_empty();
700/* set.c */ extern bool setp_equal();
701/* set.c */ extern bool setp_full();
702/* set.c */ extern bool setp_implies();
703/* set.c */ extern char *pbv1();
704/* set.c */ extern char *ps1();
705/* set.c */ extern int *sf_count();
706/* set.c */ extern int *sf_count_restricted();
707/* set.c */ extern int bit_index();
708/* set.c */ extern int set_dist();
709/* set.c */ extern int set_ord();
710/* set.c */ extern void set_adjcnt();
711/* set.c */ extern pset set_and();
712/* set.c */ extern pset set_clear();
713/* set.c */ extern pset set_copy();
714/* set.c */ extern pset set_diff();
715/* set.c */ extern pset set_fill();
716/* set.c */ extern pset set_merge();
717/* set.c */ extern pset set_or();
718/* set.c */ extern pset set_xor();
719/* set.c */ extern pset sf_and();
720/* set.c */ extern pset sf_or();
721/* set.c */ extern pset_family sf_active();
722/* set.c */ extern pset_family sf_addcol();
723/* set.c */ extern pset_family sf_addset();
724/* set.c */ extern pset_family sf_append();
725/* set.c */ extern pset_family sf_bm_read();
726/* set.c */ extern pset_family sf_compress();
727/* set.c */ extern pset_family sf_copy();
728/* set.c */ extern pset_family sf_copy_col();
729/* set.c */ extern pset_family sf_delc();
730/* set.c */ extern pset_family sf_delcol();
731/* set.c */ extern pset_family sf_inactive();
732/* set.c */ extern pset_family sf_join();
733/* set.c */ extern pset_family sf_new();
734/* set.c */ extern pset_family sf_permute();
735/* set.c */ extern pset_family sf_read();
736/* set.c */ extern pset_family sf_save();
737/* set.c */ extern pset_family sf_transpose();
738/* set.c */ extern void set_write();
739/* set.c */ extern void sf_bm_print();
740/* set.c */ extern void sf_cleanup();
741/* set.c */ extern void sf_delset();
742/* set.c */ extern void sf_free();
743/* set.c */ extern void sf_print();
744/* set.c */ extern void sf_write();
745/* setc.c */ extern bool ccommon();
746/* setc.c */ extern bool cdist0();
747/* setc.c */ extern bool full_row();
748/* setc.c */ extern int ascend();
749/* setc.c */ extern int cactive();
750/* setc.c */ extern int cdist();
751/* setc.c */ extern int cdist01();
752/* setc.c */ extern int cvolume();
753/* setc.c */ extern int d1_order();
754/* setc.c */ extern int d1_order_size();
755/* setc.c */ extern int desc1();
756/* setc.c */ extern int descend();
757/* setc.c */ extern int lex_order();
758/* setc.c */ extern int lex_order1();
759/* setc.c */ extern pset force_lower();
760/* setc.c */ extern void consensus();
761/* sharp.c */ extern pcover cb1_dsharp();
762/* sharp.c */ extern pcover cb_dsharp();
763/* sharp.c */ extern pcover cb_recur_dsharp();
764/* sharp.c */ extern pcover cb_recur_sharp();
765/* sharp.c */ extern pcover cb_sharp();
766/* sharp.c */ extern pcover cv_dsharp();
767/* sharp.c */ extern pcover cv_intersect();
768/* sharp.c */ extern pcover cv_sharp();
769/* sharp.c */ extern pcover dsharp();
770/* sharp.c */ extern pcover make_disjoint();
771/* sharp.c */ extern pcover sharp();
772/* sminterf.c */pset do_sm_minimum_cover();
773/* sparse.c */ extern pcover make_sparse();
774/* sparse.c */ extern pcover mv_reduce();
776/* unate.c */ extern pcover map_cover_to_unate();
777/* unate.c */ extern pcover map_unate_to_cover();
778/* unate.c */ extern pset_family exact_minimum_cover();
779/* unate.c */ extern pset_family gen_primes();
780/* unate.c */ extern pset_family unate_compl();
781/* unate.c */ extern pset_family unate_complement();
782/* unate.c */ extern pset_family unate_intersect();
783/* verify.c */ extern void PLA_permute();
784/* verify.c */ extern bool PLA_verify();
785/* verify.c */ extern bool check_consistency();
786/* verify.c */ extern bool verify();
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
int lex_order()
#define pcover
Definition espresso.h:264
void parse_pla()
pset_family sf_bm_read()
pset_family sf_addset()
struct cost_struct * pcost
bool full_row()
int bit_index()
char * pc1()
int ascend()
void setup_BB_CC()
pset_family opo_leaf()
void setdown_cube()
Definition cubestr.c:95
struct cube_struct cube temp_cube_save
Definition globals.c:67
pset_family find_covers()
void PLA_summary()
void find_equiv_outputs()
pset set_merge()
struct symbolic_label_struct symbolic_label_t
void fpr_header()
int util_getopt()
void mark_irredundant()
void sf_bm_print()
void skip_line()
pcover expand()
void mincov()
void explode()
pcover all_primes()
void essen_parts()
pset_family unate_complement()
pset_family sf_inactive()
void copy_cost()
void totals()
pcube * scofactor()
void sf_write()
pcube sccc()
pcover make_sparse()
int so_save()
int d1_order()
pcover map_unate_to_cover()
pset_family sf_copy_col()
pcover minimize_exact_literals()
pset_family sf_read()
pcover size_sort()
void simp_comp()
struct PLA_t * pPLA
void output_symbolic_constraints()
void select_feasible()
void form_bitvector()
void elim_lowering()
void opoall()
void debug1_print()
pset_family sf_new()
int so_do_exact()
void generate_all_pairs()
pcover expand_gasp()
struct cost_struct cost_t
pset_family gen_primes()
void PLA_permute()
void print_cube()
void print_expanded_cube()
bool recompute_onset
Definition globals.c:32
bool setp_disjoint()
pset_family exact_minimum_cover()
void map()
pcover dsharp()
pset_family opo_recur()
pset set_and()
pcover irred_gasp()
void essen_raising()
pset force_lower()
void sf_print()
pcover cb_consensus()
void consensus()
int * sf_count()
pset_family sf_contain()
void print_pair()
pcover sharp()
bool echo_unknown_commands
Definition globals.c:26
bool sccc_special_cases()
void fatal()
pset_family d1merge()
pset_family sf_ind_unlist()
pcover cv_intersect()
void save_cube_struct()
Definition cubestr.c:134
pcover cb_dsharp()
pcover random_order()
bool PLA_verify()
bool debug_exact_minimization
pcube * cube2list()
void expand1()
pset_family sf_delcol()
void cprint()
void debug_print()
bool essen_cube()
int ** find_pairing_cost()
pcover cubeunlist()
pcover mini_sort()
void massive_count()
pcover map_symbolic_cover()
void pls_group()
void so_both_espresso()
pset sf_or()
pcover cv_sharp()
int d1_order_size()
pcube sccc_merge()
bool kiss
Definition globals.c:29
pcover cb1_dsharp()
pset_family sf_dupl()
int total_calls[TIME_COUNT]
Definition globals.c:23
bool taut_special_cases()
void sf_free()
ppair pair_save()
void free_PLA()
#define TIME_COUNT
Definition espresso.h:371
void map_output_symbolic()
pcover sort_reduce()
void sf_cleanup()
Definition set.c:374
pset_family sf_active()
int greedy_best_cost()
#define pcube
Definition espresso.h:261
int check_equiv()
void find_inputs()
ABC_NAMESPACE_HEADER_END int binate_split_select()
struct pla_types_struct pla_types[]
Definition globals.c:42
struct cdata_struct cdata temp_cdata_save
Definition globals.c:68
void set_write()
bool single_expand
Definition globals.c:34
pcover make_disjoint()
void pair_all()
pset_family sf_unlist()
void print_trace()
void minimize_pair()
int rm_equal()
char * pc3()
pcover pairvar()
pcover super_gasp()
void map_dcset()
pset_family sf_permute()
char * fmt_expanded_cube()
bool trace
Definition globals.c:36
pcover cb_recur_sharp()
ppair pair_best_cost()
int so_both_do_espresso()
long total_time[TIME_COUNT]
Definition globals.c:22
void restore_cube_struct()
Definition cubestr.c:151
int read_pla()
int desc1()
pset_family sf_compress()
pcover unravel()
pset minterms()
int cvolume()
pcover uncof_output()
void PLA_labels()
char * ps1()
pPLA set_phase()
pset set_diff()
pset_family sf_union()
pcover map_cover_to_unate()
bool verify()
void sf_debug_print()
pcover espresso()
pcover essential()
char * strsav()
pset_family sf_save()
pcover opo()
int rm_contain()
bool print_solution
Definition globals.c:31
int so_do_espresso()
char * pc2()
void find_optimal_pairing()
int descend()
bool skip_make_sparse
Definition globals.c:28
char * fmt_cost()
pset sf_and()
char * print_cost()
pset_family sf_ind_contain()
pPLA new_PLA()
Definition cvrin.c:648
pset set_fill()
char * fmt_cube()
struct set_family * pset_family
pcover reduce()
struct symbolic_list_struct symbolic_list_t
pcube * cofactor()
pcube * cube3list()
pset_family unate_compl()
bool summary
Definition globals.c:35
unsigned int debug
Definition globals.c:19
pset_family dist_merge()
bool verbose_debug
Definition globals.c:20
bool remove_essential
Definition globals.c:33
pcover minimize_exact()
int rm2_contain()
pset_family sf_merge()
int so_both_save()
void read_cube()
bool setp_full()
void eqn_output()
char * get_word()
pcover cb_sharp()
void sf_delset()
void irred_split_cover()
ppair pair_new()
int rm2_equal()
int set_ord()
int lex_order1()
pcover find_all_minimal_covers_petrick()
void pls_output()
pcube reduce_cube()
void find_dc_inputs()
pcover cv_dsharp()
void find_best_cost()
void so_espresso()
sm_matrix * irred_derive_table()
pcube find_phase()
pset_family sf_rev_contain()
pset_family sf_addcol()
void set_pair()
bool setp_empty()
bool setp_implies()
pcover unravel_range()
void cube_setup()
Definition cubestr.c:27
void cover_cost()
int cdist()
bool use_super_gasp
Definition globals.c:39
int most_frequent()
void size_stamp()
void set_adjcnt()
pset set_clear()
pcover lex_sort()
void pls_label()
int read_symbolic()
void phase_assignment()
bool feasibly_covered()
bool force_irredundant
Definition globals.c:27
int cubelist_partition()
pcover irredundant()
pset_family form_cover_table()
pcover cof_output()
pcover last_gasp()
pset do_sm_minimum_cover()
unsigned int * pset
Definition espresso.h:73
bool cube_is_covered()
int cdist01()
bool use_random_order
Definition globals.c:38
bool set_andp()
pset set_or()
pset_family unate_intersect()
bool set_orp()
struct pair_struct * ppair
void map_symbolic()
bool tautology()
int rm_rev_contain()
bool check_consistency()
bool pos
Definition globals.c:30
struct symbolic_struct symbolic_t
pcover cb_consensus_dist0()
pset * sf_sort()
pset_family sf_append()
void expand1_gasp()
bool setp_equal()
char * total_name[TIME_COUNT]
Definition globals.c:21
void fprint_pla()
struct set_family set_family_t
pcover find_all_primes()
pset_family sf_delc()
void output_phase_setup()
pcube sccc_cube()
int d1_rm_equal()
pset * sf_list()
pcover simplify()
int so_both_do_exact()
bool cdist0()
void set_pair1()
char * pbv1()
bool unwrap_onset
Definition globals.c:37
pcover mv_reduce()
pset_family sf_join()
pset set_copy()
pset_family sf_transpose()
struct pair_struct pair_t
int * sf_count_restricted()
pcover cb_recur_dsharp()
char * filename
Definition globals.c:40
void kiss_print_cube()
void kiss_output()
int cactive()
bool echo_comments
Definition globals.c:25
pcube * cube1list()
pcover delvar()
void repeated_phase_assignment()
pset_family sf_copy()
pcover primes_consensus()
void pair_free()
pset set_xor()
bool ccommon()
pcover complement()
void foreach_output_function()
int set_dist()
void symbolic_hack_labels()
void makeup_labels()
int label_index()
struct sm_matrix_struct sm_matrix
Definition sparse.h:24
char ** label
Definition espresso.h:321
pcover D
Definition espresso.h:316
ppair pair
Definition espresso.h:320
pcover R
Definition espresso.h:316
char * filename
Definition espresso.h:317
pcube phase
Definition espresso.h:319
symbolic_t * symbolic_output
Definition espresso.h:323
pcover F
Definition espresso.h:316
int pla_type
Definition espresso.h:318
symbolic_t * symbolic
Definition espresso.h:322
bool * is_unate
Definition espresso.h:497
int * var_zeros
Definition espresso.h:495
int * parts_active
Definition espresso.h:496
int vars_active
Definition espresso.h:498
int * part_zeros
Definition espresso.h:494
int * sparse
Definition espresso.h:488
pset emptyset
Definition espresso.h:485
int * part_size
Definition espresso.h:477
int * last_word
Definition espresso.h:479
unsigned int inmask
Definition espresso.h:486
pset fullset
Definition espresso.h:484
pset mv_mask
Definition espresso.h:481
int * last_part
Definition espresso.h:476
pset * temp
Definition espresso.h:483
int num_binary_vars
Definition espresso.h:474
int * first_word
Definition espresso.h:478
int num_mv_vars
Definition espresso.h:489
pset binary_mask
Definition espresso.h:480
pset * var_mask
Definition espresso.h:482
int * first_part
Definition espresso.h:475
Definition exor.h:123
int * var1
Definition espresso.h:284
int * var2
Definition espresso.h:285
struct set_family * next
Definition espresso.h:83
int count
Definition espresso.h:80
int capacity
Definition espresso.h:79
pset data
Definition espresso.h:82
int wsize
Definition espresso.h:77
int active_count
Definition espresso.h:81
int sf_size
Definition espresso.h:78
struct symbolic_label_struct * next
Definition espresso.h:300
struct symbolic_list_struct * next
Definition espresso.h:293
symbolic_label_t * symbolic_label
Definition espresso.h:308
struct symbolic_struct * next
Definition espresso.h:310
symbolic_list_t * symbolic_list
Definition espresso.h:306
int symbolic_list_length
Definition espresso.h:307
int symbolic_label_length
Definition espresso.h:309