ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
sharp.c File Reference
#include "espresso.h"
Include dependency graph for sharp.c:

Go to the source code of this file.

Macros

#define MAGIC   500 /* save 500 cubes before containment */
 

Functions

pcover cv_sharp (pcover A, pcover B)
 
pcover cb_sharp (pcube c, pcover T)
 
pcover cb_recur_sharp (pcube c, pcover T, int first, int last, int level)
 
pcover sharp (pcube a, pcube b)
 
pcover make_disjoint (pcover A)
 
pcover cv_dsharp (pcover A, pcover B)
 
pcover cb1_dsharp (pcover T, pcube c)
 
pcover cb_dsharp (pcube c, pcover T)
 
pcover dsharp (pcube a, pcube b)
 
pcover cv_intersect (pcover A, pcover B)
 

Variables

ABC_NAMESPACE_IMPL_START long start_time
 

Macro Definition Documentation

◆ MAGIC

#define MAGIC   500 /* save 500 cubes before containment */

Definition at line 214 of file sharp.c.

Function Documentation

◆ cb1_dsharp()

pcover cb1_dsharp ( pcover T,
pcube c )

Definition at line 133 of file sharp.c.

136{
137 pcube last, p;
138 pcover R;
139
140 R = new_cover(T->count);
141 foreach_set(T, last, p) {
142 R = sf_union(R, dsharp(p, c));
143 }
144 return R;
145}
#define pcover
Definition espresso.h:264
pcover dsharp()
#define pcube
Definition espresso.h:261
pset_family sf_union()
#define foreach_set(R, last, p)
Definition espresso.h:135
#define new_cover(i)
Definition espresso.h:265
Cube * p
Definition exorList.c:222
Here is the call graph for this function:

◆ cb_dsharp()

pcover cb_dsharp ( pcube c,
pcover T )

Definition at line 149 of file sharp.c.

152{
153 pcube last, p;
154 pcover Y, Y1;
155
156 if (T->count == 0) {
157 Y = sf_addset(new_cover(1), c);
158 } else {
159 Y = new_cover(T->count);
160 set_copy(GETSET(Y,Y->count++), c);
161 foreach_set(T, last, p) {
162 Y1 = cb1_dsharp(Y, p);
163 free_cover(Y);
164 Y = Y1;
165 }
166 }
167 return Y;
168}
pset_family sf_addset()
pcover cb1_dsharp()
#define free_cover(r)
Definition espresso.h:266
#define GETSET(family, index)
Definition espresso.h:161
pset set_copy()
Here is the call graph for this function:

◆ cb_recur_sharp()

pcover cb_recur_sharp ( pcube c,
pcover T,
int first,
int last,
int level )

Definition at line 52 of file sharp.c.

56{
57 pcover temp, left, right;
58 int middle;
59
60 if (first == last) {
61 temp = sharp(c, GETSET(T, first));
62 } else {
63 middle = (first + last) / 2;
64 left = cb_recur_sharp(c, T, first, middle, level+1);
65 right = cb_recur_sharp(c, T, middle+1, last, level+1);
66 temp = cv_intersect(left, right);
67 if ((debug & SHARP) && level < 4) {
68 printf("# SHARP[%d]: %4d = %4d x %4d, time = %s\n",
69 level, temp->count, left->count, right->count,
71 (void) fflush(stdout);
72 }
73 free_cover(left);
74 free_cover(right);
75 }
76 return temp;
77}
pcover sharp()
#define print_time(t)
Definition espresso.h:22
pcover cv_intersect()
pcover cb_recur_sharp()
unsigned int debug
Definition globals.c:19
#define SHARP
Definition espresso.h:364
ABC_NAMESPACE_IMPL_START long start_time
Definition sharp.c:19
#define ptime()
Definition util_old.h:283
Here is the call graph for this function:

◆ cb_sharp()

pcover cb_sharp ( pcube c,
pcover T )

Definition at line 37 of file sharp.c.

40{
41 if (T->count == 0) {
42 T = sf_addset(new_cover(1), c);
43 } else {
44 start_time = ptime();
45 T = cb_recur_sharp(c, T, 0, T->count-1, 0);
46 }
47 return T;
48}
Here is the call graph for this function:

◆ cv_dsharp()

pcover cv_dsharp ( pcover A,
pcover B )

Definition at line 118 of file sharp.c.

120{
121 register pcube last, p;
122 pcover T;
123
124 T = new_cover(0);
125 foreach_set(A, last, p) {
126 T = sf_union(T, cb_dsharp(p, B));
127 }
128 return T;
129}
pcover cb_dsharp()
Here is the call graph for this function:

◆ cv_intersect()

pcover cv_intersect ( pcover A,
pcover B )

Definition at line 216 of file sharp.c.

218{
219 register pcube pi, pj, lasti, lastj, pt;
220 pcover T, Tsave = NULL;
221
222 /* How large should each temporary result cover be ? */
223 T = new_cover(MAGIC);
224 pt = T->data;
225
226 /* Form pairwise intersection of each cube of A with each cube of B */
227 foreach_set(A, lasti, pi) {
228 foreach_set(B, lastj, pj) {
229 if (cdist0(pi, pj)) {
230 (void) set_and(pt, pi, pj);
231 if (++T->count >= T->capacity) {
232 if (Tsave == NULL)
233 Tsave = sf_contain(T);
234 else
235 Tsave = sf_union(Tsave, sf_contain(T));
236 T = new_cover(MAGIC);
237 pt = T->data;
238 } else
239 pt += T->wsize;
240 }
241 }
242 }
243
244
245 if (Tsave == NULL)
246 Tsave = sf_contain(T);
247 else
248 Tsave = sf_union(Tsave, sf_contain(T));
249 return Tsave;
250}
pset set_and()
pset_family sf_contain()
bool cdist0()
#define MAGIC
Definition sharp.c:214
Here is the call graph for this function:

◆ cv_sharp()

pcover cv_sharp ( pcover A,
pcover B )

Definition at line 23 of file sharp.c.

25{
26 pcube last, p;
27 pcover T;
28
29 T = new_cover(0);
30 foreach_set(A, last, p)
31 T = sf_union(T, cb_sharp(p, B));
32 return T;
33}
pcover cb_sharp()
Here is the call graph for this function:

◆ dsharp()

pcover dsharp ( pcube a,
pcube b )

Definition at line 172 of file sharp.c.

174{
175 register pcube mask, diff, and, temp, temp1 = cube.temp[0];
176 int var;
177 pcover r;
178
179 r = new_cover(cube.num_vars);
180
181 if (cdist0(a, b)) {
182 diff = set_diff(new_cube(), a, b);
183 and = set_and(new_cube(), a, b);
184 mask = new_cube();
185 for(var = 0; var < cube.num_vars; var++) {
186 /* check if position var of "a and not b" is not empty */
187 if (! setp_disjoint(diff, cube.var_mask[var])) {
188
189 /* coordinate var equals the difference between a and b */
190 temp = GETSET(r, r->count++);
191 (void) set_and(temp, diff, cube.var_mask[var]);
192
193 /* coordinates 0 ... var-1 equal the intersection */
194 INLINEset_and(temp1, and, mask);
195 INLINEset_or(temp, temp, temp1);
196
197 /* coordinates var+1 .. cube.num_vars equal a */
198 set_or(mask, mask, cube.var_mask[var]);
199 INLINEset_diff(temp1, a, mask);
200 INLINEset_or(temp, temp, temp1);
201 }
202 }
203 free_cube(diff);
204 free_cube(and);
205 free_cube(mask);
206 } else {
207 r = sf_addset(r, a);
208 }
209 return r;
210}
#define new_cube()
Definition espresso.h:262
#define INLINEset_diff(r, a, b)
Definition espresso.h:208
#define INLINEset_or(r, a, b)
Definition espresso.h:205
bool setp_disjoint()
pset set_diff()
#define free_cube(r)
Definition espresso.h:263
#define INLINEset_and(r, a, b)
Definition espresso.h:202
pset set_or()
unsigned short var
Definition giaNewBdd.h:35
Definition exor.h:123
Here is the call graph for this function:

◆ make_disjoint()

pcover make_disjoint ( pcover A)

Definition at line 102 of file sharp.c.

104{
105 pcover R, new;
106 register pset last, p;
107
108 R = new_cover(0);
109 foreach_set(A, last, p) {
110 new = cb_dsharp(p, R);
111 R = sf_append(R, new);
112 }
113 return R;
114}
unsigned int * pset
Definition espresso.h:73
pset_family sf_append()
Here is the call graph for this function:

◆ sharp()

pcover sharp ( pcube a,
pcube b )

Definition at line 81 of file sharp.c.

83{
84 register int var;
85 register pcube d=cube.temp[0], temp=cube.temp[1], temp1=cube.temp[2];
86 pcover r = new_cover(cube.num_vars);
87
88 if (cdist0(a, b)) {
89 set_diff(d, a, b);
90 for(var = 0; var < cube.num_vars; var++) {
91 if (! setp_empty(set_and(temp, d, cube.var_mask[var]))) {
92 set_diff(temp1, a, cube.var_mask[var]);
93 set_or(GETSET(r, r->count++), temp, temp1);
94 }
95 }
96 } else {
97 r = sf_addset(r, a);
98 }
99 return r;
100}
bool setp_empty()
Here is the call graph for this function:

Variable Documentation

◆ start_time

ABC_NAMESPACE_IMPL_START long start_time

Definition at line 19 of file sharp.c.