ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
extraBddThresh.c
Go to the documentation of this file.
1
20
21#include <stdio.h>
22#include <stdlib.h>
23#include <string.h>
24#include <assert.h>
25#include "base/main/main.h"
26#include "misc/extra/extra.h"
27#include "bdd/cudd/cudd.h"
28#include "bool/kit/kit.h"
29
30#include "misc/vec/vec.h"
31#include "misc/util/utilTruth.h"
32
33ABC_NAMESPACE_IMPL_START
34
38
42
54void Extra_ThreshPrintChow(int Chow0, int * pChow, int nVars) {
55 int i;
56 for (i = 0; i < nVars; i++)
57 printf("%d ", pChow[i]);
58 printf(" %d\n", Chow0);
59}
60int Extra_ThreshComputeChow(word * t, int nVars, int * pChow) {
61 int i, k, Chow0 = 0, nMints = (1 << nVars);
62 memset(pChow, 0, sizeof(int) * nVars);
63 // compute Chow coefs
64 for (i = 0; i < nMints; i++)
65 if (Abc_TtGetBit(t, i))
66 for (Chow0++, k = 0; k < nVars; k++)
67 if ((i >> k) & 1)
68 pChow[k]++;
69 // compute modified Chow coefs
70 for (k = 0; k < nVars; k++)
71 pChow[k] = 2 * pChow[k] - Chow0;
72 return Chow0 - (1 << (nVars - 1));
73}
74void Extra_ThreshSortByChow(word * t, int nVars, int * pChow) {
75 int i, nWords = Abc_TtWordNum(nVars);
76 //sort the variables by Chow in ascending order
77 while (1) {
78 int fChange = 0;
79 for (i = 0; i < nVars - 1; i++) {
80 if (pChow[i] >= pChow[i + 1])
81 continue;
82 ABC_SWAP(int, pChow[i], pChow[i + 1]);
83 Abc_TtSwapAdjacent(t, nWords, i);
84 fChange = 1;
85 }
86 if (!fChange)
87 return;
88 }
89}
90void Extra_ThreshSortByChowInverted(word * t, int nVars, int * pChow) {
91 int i, nWords = Abc_TtWordNum(nVars);
92 //sort the variables by Chow in descending order
93 while (1) {
94 int fChange = 0;
95 for (i = 0; i < nVars - 1; i++) {
96 if (pChow[i] <= pChow[i + 1])
97 continue;
98 ABC_SWAP(int, pChow[i], pChow[i + 1]);
99 Abc_TtSwapAdjacent(t, nWords, i);
100 fChange = 1;
101 }
102 if (!fChange)
103 return;
104 }
105}
106int Extra_ThreshInitializeChow(int nVars, int * pChow) {
107 int i = 0, Aux[16], nChows = 0;
108 //group the variables which have the same Chow
109 for (i = 0; i < nVars; i++) {
110 if (i == 0 || (pChow[i] == pChow[i - 1]))
111 Aux[i] = nChows;
112 else {
113 nChows++;
114 Aux[i] = nChows;
115 }
116 }
117 for (i = 0; i < nVars; i++)
118 pChow[i] = Aux[i];
119 nChows++;
120 return nChows;
121
122}
123static inline int Extra_ThreshWeightedSum(int * pW, int nVars, int m) {
124 int i, Cost = 0;
125 for (i = 0; i < nVars; i++)
126 if ((m >> i) & 1)
127 Cost += pW[i];
128 return Cost;
129}
130static inline int Extra_ThreshCubeWeightedSum1(int * pWofChow, int * pChow,
131 char * pIsop, int nVars, int j) {
132 int k, Cost = 0;
133 for (k = j; k < j + nVars; k++)
134 if (pIsop[k] == '1')
135 Cost += pWofChow[pChow[k - j]];
136 return Cost;
137}
138static inline int Extra_ThreshCubeWeightedSum2(int * pWofChow, int * pChow,
139 char * pIsop, int nVars, int j) {
140 int k, Cost = 0;
141 for (k = j; k < j + nVars; k++)
142 if (pIsop[k] == '-')
143 Cost += pWofChow[pChow[k - j]];
144 return Cost;
145}
146
147static inline int Extra_ThreshCubeWeightedSum3(int * pWofChow, int nChows,
148 unsigned long ** pGreaters, int j) {
149 int i, Cost = 0;
150 for (i = 0; i < nChows; i++)
151 Cost += pWofChow[i] * pGreaters[j][i];
152 return Cost;
153}
154static inline int Extra_ThreshCubeWeightedSum4(int * pWofChow, int nChows,
155 unsigned long ** pSmallers, int j) {
156 int i, Cost = 0;
157 for (i = 0; i < nChows; i++)
158 Cost += pWofChow[i] * pSmallers[j][i];
159 return Cost;
160}
161int Extra_ThreshSelectWeights3(word * t, int nVars, int * pW) {
162 int m, Lmin, Lmax, nMints = (1 << nVars);
163 assert(nVars == 3);
164 for (pW[2] = 1; pW[2] <= nVars; pW[2]++)
165 for (pW[1] = pW[2]; pW[1] <= nVars; pW[1]++)
166 for (pW[0] = pW[1]; pW[0] <= nVars; pW[0]++) {
167 Lmin = 10000;
168 Lmax = 0;
169 for (m = 0; m < nMints; m++) {
170 if (Abc_TtGetBit(t, m))
171 Lmin = Abc_MinInt(Lmin,
172 Extra_ThreshWeightedSum(pW, nVars, m));
173 else
174 Lmax = Abc_MaxInt(Lmax,
175 Extra_ThreshWeightedSum(pW, nVars, m));
176 if (Lmax >= Lmin)
177 break;
178// printf( "%c%d ", Abc_TtGetBit(t, m) ? '+' : '-', Extra_ThreshWeightedSum(pW, nVars, m) );
179 }
180// printf( " -%d +%d\n", Lmax, Lmin );
181 if (m < nMints)
182 continue;
183 assert(Lmax < Lmin);
184 return Lmin;
185 }
186 return 0;
187}
188int Extra_ThreshSelectWeights4(word * t, int nVars, int * pW) {
189 int m, Lmin, Lmax, nMints = (1 << nVars);
190 assert(nVars == 4);
191 for (pW[3] = 1; pW[3] <= nVars; pW[3]++)
192 for (pW[2] = pW[3]; pW[2] <= nVars; pW[2]++)
193 for (pW[1] = pW[2]; pW[1] <= nVars; pW[1]++)
194 for (pW[0] = pW[1]; pW[0] <= nVars; pW[0]++) {
195 Lmin = 10000;
196 Lmax = 0;
197 for (m = 0; m < nMints; m++) {
198 if (Abc_TtGetBit(t, m))
199 Lmin = Abc_MinInt(Lmin,
200 Extra_ThreshWeightedSum(pW, nVars, m));
201 else
202 Lmax = Abc_MaxInt(Lmax,
203 Extra_ThreshWeightedSum(pW, nVars, m));
204 if (Lmax >= Lmin)
205 break;
206 }
207 if (m < nMints)
208 continue;
209 assert(Lmax < Lmin);
210 return Lmin;
211 }
212 return 0;
213}
214int Extra_ThreshSelectWeights5(word * t, int nVars, int * pW) {
215 int m, Lmin, Lmax, nMints = (1 << nVars), Limit = nVars + 0;
216 assert(nVars == 5);
217 for (pW[4] = 1; pW[4] <= Limit; pW[4]++)
218 for (pW[3] = pW[4]; pW[3] <= Limit; pW[3]++)
219 for (pW[2] = pW[3]; pW[2] <= Limit; pW[2]++)
220 for (pW[1] = pW[2]; pW[1] <= Limit; pW[1]++)
221 for (pW[0] = pW[1]; pW[0] <= Limit; pW[0]++) {
222 Lmin = 10000;
223 Lmax = 0;
224 for (m = 0; m < nMints; m++) {
225 if (Abc_TtGetBit(t, m))
226 Lmin = Abc_MinInt(Lmin,
227 Extra_ThreshWeightedSum(pW, nVars, m));
228 else
229 Lmax = Abc_MaxInt(Lmax,
230 Extra_ThreshWeightedSum(pW, nVars, m));
231 if (Lmax >= Lmin)
232 break;
233 }
234 if (m < nMints)
235 continue;
236 assert(Lmax < Lmin);
237 return Lmin;
238 }
239 return 0;
240}
241int Extra_ThreshSelectWeights6(word * t, int nVars, int * pW) {
242 int m, Lmin, Lmax, nMints = (1 << nVars), Limit = nVars + 3;
243 assert(nVars == 6);
244 for (pW[5] = 1; pW[5] <= Limit; pW[5]++)
245 for (pW[4] = pW[5]; pW[4] <= Limit; pW[4]++)
246 for (pW[3] = pW[4]; pW[3] <= Limit; pW[3]++)
247 for (pW[2] = pW[3]; pW[2] <= Limit; pW[2]++)
248 for (pW[1] = pW[2]; pW[1] <= Limit; pW[1]++)
249 for (pW[0] = pW[1]; pW[0] <= Limit; pW[0]++) {
250 Lmin = 10000;
251 Lmax = 0;
252 for (m = 0; m < nMints; m++) {
253 if (Abc_TtGetBit(t, m))
254 Lmin = Abc_MinInt(Lmin,
255 Extra_ThreshWeightedSum(pW, nVars,
256 m));
257 else
258 Lmax = Abc_MaxInt(Lmax,
259 Extra_ThreshWeightedSum(pW, nVars,
260 m));
261 if (Lmax >= Lmin)
262 break;
263 }
264 if (m < nMints)
265 continue;
266 assert(Lmax < Lmin);
267 return Lmin;
268 }
269 return 0;
270}
271int Extra_ThreshSelectWeights7(word * t, int nVars, int * pW) {
272 int m, Lmin, Lmax, nMints = (1 << nVars), Limit = nVars + 6;
273 assert(nVars == 7);
274 for (pW[6] = 1; pW[6] <= Limit; pW[6]++)
275 for (pW[5] = pW[6]; pW[5] <= Limit; pW[5]++)
276 for (pW[4] = pW[5]; pW[4] <= Limit; pW[4]++)
277 for (pW[3] = pW[4]; pW[3] <= Limit; pW[3]++)
278 for (pW[2] = pW[3]; pW[2] <= Limit; pW[2]++)
279 for (pW[1] = pW[2]; pW[1] <= Limit; pW[1]++)
280 for (pW[0] = pW[1]; pW[0] <= Limit; pW[0]++) {
281 Lmin = 10000;
282 Lmax = 0;
283 for (m = 0; m < nMints; m++) {
284 if (Abc_TtGetBit(t, m))
285 Lmin = Abc_MinInt(Lmin,
286 Extra_ThreshWeightedSum(pW,
287 nVars, m));
288 else
289 Lmax = Abc_MaxInt(Lmax,
290 Extra_ThreshWeightedSum(pW,
291 nVars, m));
292 if (Lmax >= Lmin)
293 break;
294 }
295 if (m < nMints)
296 continue;
297 assert(Lmax < Lmin);
298 return Lmin;
299 }
300 return 0;
301}
302int Extra_ThreshSelectWeights8(word * t, int nVars, int * pW) {
303 int m, Lmin, Lmax, nMints = (1 << nVars), Limit = nVars + 1; // <<-- incomplete detection to save runtime!
304 assert(nVars == 8);
305 for (pW[7] = 1; pW[7] <= Limit; pW[7]++)
306 for (pW[6] = pW[7]; pW[6] <= Limit; pW[6]++)
307 for (pW[5] = pW[6]; pW[5] <= Limit; pW[5]++)
308 for (pW[4] = pW[5]; pW[4] <= Limit; pW[4]++)
309 for (pW[3] = pW[4]; pW[3] <= Limit; pW[3]++)
310 for (pW[2] = pW[3]; pW[2] <= Limit; pW[2]++)
311 for (pW[1] = pW[2]; pW[1] <= Limit; pW[1]++)
312 for (pW[0] = pW[1]; pW[0] <= Limit; pW[0]++) {
313 Lmin = 10000;
314 Lmax = 0;
315 for (m = 0; m < nMints; m++) {
316 if (Abc_TtGetBit(t, m))
317 Lmin = Abc_MinInt(Lmin,
318 Extra_ThreshWeightedSum(pW,
319 nVars, m));
320 else
321 Lmax = Abc_MaxInt(Lmax,
322 Extra_ThreshWeightedSum(pW,
323 nVars, m));
324 if (Lmax >= Lmin)
325 break;
326 }
327 if (m < nMints)
328 continue;
329 assert(Lmax < Lmin);
330 return Lmin;
331 }
332 return 0;
333}
334int Extra_ThreshSelectWeights(word * t, int nVars, int * pW) {
335 if (nVars <= 2)
336 return (t[0] & 0xF) != 6 && (t[0] & 0xF) != 9;
337 if (nVars == 3)
338 return Extra_ThreshSelectWeights3(t, nVars, pW);
339 if (nVars == 4)
340 return Extra_ThreshSelectWeights4(t, nVars, pW);
341 if (nVars == 5)
342 return Extra_ThreshSelectWeights5(t, nVars, pW);
343 if (nVars == 6)
344 return Extra_ThreshSelectWeights6(t, nVars, pW);
345 if (nVars == 7)
346 return Extra_ThreshSelectWeights7(t, nVars, pW);
347 if (nVars == 8)
348 return Extra_ThreshSelectWeights8(t, nVars, pW);
349 return 0;
350}
351void Extra_ThreshIncrementWeights(int nChows, int * pWofChow, int i) {
352 int k;
353 for (k = i; k < nChows; k++) {
354 pWofChow[k]++;
355 }
356}
357void Extra_ThreshDecrementWeights(int nChows, int * pWofChow, int i) {
358 int k;
359 for (k = i; k < nChows; k++) {
360 pWofChow[k]--;
361 }
362}
363void Extra_ThreshPrintInequalities(unsigned long ** pGreaters,
364 unsigned long ** pSmallers, int nChows, int nInequalities) {
365 int i = 0, k = 0;
366 for (k = 0; k < nInequalities; k++) {
367 printf("\n Inequality [%d] = ", k);
368 for (i = 0; i < nChows; i++) {
369 printf("%ld ", pGreaters[k][i]);
370 }
371 printf(" > ");
372
373 for (i = 0; i < nChows; i++) {
374 printf("%ld ", pSmallers[k][i]);
375 }
376 }
377}
378void Extra_ThreshCreateInequalities(char * pIsop, char * pIsopFneg, int nVars,
379 int * pWofChow, int * pChow, int nChows, int nInequalities,
380 unsigned long ** pGreaters, unsigned long ** pSmallers) {
381 int i = 0, j = 0, k = 0, m = 0;
382
383 int nCubesIsop = strlen(pIsop) / (nVars + 3);
384 int nCubesIsopFneg = strlen(pIsopFneg) / (nVars + 3);
385
386 for (k = 0; k < nCubesIsop * nCubesIsopFneg; k++)
387 for (i = 0; i < nChows; i++) {
388 pGreaters[k][i] = 0;
389 pSmallers[k][i] = 0;
390 }
391 m = 0;
392 for (i = 0; i < (int)strlen(pIsop); i += (nVars + 3))
393 for (j = 0; j < nCubesIsopFneg; j++) {
394 for (k = 0; k < nVars; k++)
395 if (pIsop[i + k] == '1')
396 pGreaters[m][pChow[k]] = pGreaters[m][(pChow[k])] + 1;
397
398 m++;
399 }
400 m = 0;
401 for (i = 0; i < nCubesIsop; i++)
402 for (j = 0; j < (int)strlen(pIsopFneg); j += (nVars + 3)) {
403 for (k = 0; k < nVars; k++)
404 if (pIsopFneg[j + k] == '-')
405 pSmallers[m][pChow[k]] = pSmallers[m][pChow[k]] + 1;
406 m++;
407 }
408// Extra_ThreshPrintInequalities( pGreaters, pSmallers, nChows, nInequalities);
409// printf( "\nInequalities was Created \n");
410}
411
412void Extra_ThreshSimplifyInequalities(int nInequalities, int nChows,
413 unsigned long ** pGreaters, unsigned long ** pSmallers) {
414 int i = 0, k = 0;
415
416 for (k = 0; k < nInequalities; k++) {
417 for (i = 0; i < nChows; i++) {
418 if ((pGreaters[k][i]) == (pSmallers[k][i])) {
419 pGreaters[k][i] = 0;
420 pSmallers[k][i] = 0;
421 } else if ((pGreaters[k][i]) > (pSmallers[k][i])) {
422 pGreaters[k][i] = pGreaters[k][i] - pSmallers[k][i];
423 pSmallers[k][i] = 0;
424 } else {
425 pSmallers[k][i] = pSmallers[k][i] - pGreaters[k][i];
426 ;
427 pGreaters[k][i] = 0;
428 }
429 }
430 }
431// Extra_ThreshPrintInequalities( pGreaters, pSmallers, nChows, nInequalities);
432// printf( "\nInequalities was Siplified \n");
433}
434int Extra_ThreshAssignWeights(word * t, char * pIsop, char * pIsopFneg,
435 int nVars, int * pW, int * pChow, int nChows, int Wmin) {
436
437 int i = 0, j = 0, Lmin = 1000, Lmax = 0, Limit = nVars * 2, delta = 0,
438 deltaOld = -1000, fIncremented = 0;
439 //******************************
440 int * pWofChow = ABC_ALLOC( int, nChows );
441 int nCubesIsop = strlen(pIsop) / (nVars + 3);
442 int nCubesIsopFneg = strlen(pIsopFneg) / (nVars + 3);
443 int nInequalities = nCubesIsop * nCubesIsopFneg;
444 unsigned long **pGreaters;
445 unsigned long **pSmallers;
446
447 pGreaters = (unsigned long **)malloc(nCubesIsop * nCubesIsopFneg * sizeof *pGreaters);
448 for (i = 0; i < nCubesIsop * nCubesIsopFneg; i++) {
449 pGreaters[i] = (unsigned long *)malloc(nChows * sizeof *pGreaters[i]);
450 }
451 pSmallers = (unsigned long **)malloc(nCubesIsop * nCubesIsopFneg * sizeof *pSmallers);
452 for (i = 0; i < nCubesIsop * nCubesIsopFneg; i++) {
453 pSmallers[i] = (unsigned long *)malloc(nChows * sizeof *pSmallers[i]);
454 }
455
456 //******************************
457 Extra_ThreshCreateInequalities(pIsop, pIsopFneg, nVars, pWofChow, pChow,
458 nChows, nInequalities, pGreaters, pSmallers);
459 Extra_ThreshSimplifyInequalities(nInequalities, nChows, pGreaters,
460 pSmallers);
461
462 //initializes the weights
463 pWofChow[0] = Wmin;
464 for (i = 1; i < nChows; i++) {
465 pWofChow[i] = pWofChow[i - 1] + 1;
466 }
467 i = 0;
468
469 //assign the weights respecting the inequalities
470 while (i < nChows && pWofChow[nChows - 1] <= Limit) {
471 Lmin = 1000;
472 Lmax = 0;
473
474 while (j < nInequalities) {
475 if (pGreaters[j][i] != 0) {
476 Lmin = Extra_ThreshCubeWeightedSum3(pWofChow, nChows, pGreaters,
477 j);
478 Lmax = Extra_ThreshCubeWeightedSum4(pWofChow, nChows, pSmallers,
479 j);
480 delta = Lmin - Lmax;
481
482 if (delta > 0) {
483 if (fIncremented == 1) {
484 j = 0;
485 fIncremented = 0;
486 deltaOld = -1000;
487 } else
488 j++;
489 continue;
490 }
491 if (delta > deltaOld) {
492 Extra_ThreshIncrementWeights(nChows, pWofChow, i);
493 deltaOld = delta;
494 fIncremented = 1;
495 } else if (fIncremented == 1) {
496 Extra_ThreshDecrementWeights(nChows, pWofChow, i);
497 j++;
498 deltaOld = -1000;
499 fIncremented = 0;
500 continue;
501 } else
502 j++;
503 } else
504 j++;
505
506 }
507 i++;
508 j = 0;
509 }
510
511 //******************************
512 for (i = 0; i < nCubesIsop * nCubesIsopFneg; i++) {
513 free(pGreaters[i]);
514 }
515 free(pGreaters);
516 for (i = 0; i < nCubesIsop * nCubesIsopFneg; i++) {
517 free(pSmallers[i]);
518 }
519 free(pSmallers);
520 //******************************
521
522 i = 0;
523 Lmin = 1000;
524 Lmax = 0;
525
526 //check the assigned weights in the original system
527 for (j = 0; j < (int)strlen(pIsop); j += (nVars + 3))
528 Lmin = Abc_MinInt(Lmin,
529 Extra_ThreshCubeWeightedSum1(pWofChow, pChow, pIsop, nVars, j));
530 for (j = 0; j < (int)strlen(pIsopFneg); j += (nVars + 3))
531 Lmax = Abc_MaxInt(Lmax,
532 Extra_ThreshCubeWeightedSum2(pWofChow, pChow, pIsopFneg, nVars,
533 j));
534
535 for (i = 0; i < nVars; i++) {
536 pW[i] = pWofChow[pChow[i]];
537 }
538
539 ABC_FREE( pWofChow );
540 if (Lmin > Lmax)
541 return Lmin;
542 else
543 return 0;
544}
545void Extra_ThreshPrintWeights(int T, int * pW, int nVars) {
546 int i;
547
548 if (T == 0)
549 fprintf( stdout, "\nHeuristic method: is not TLF\n\n");
550 else {
551 fprintf( stdout, "\nHeuristic method: Weights and threshold value:\n");
552 for (i = 0; i < nVars; i++)
553 printf("%d ", pW[i]);
554 printf(" %d\n", T);
555 }
556}
557
570int Extra_ThreshCheck(word * t, int nVars, int * pW) {
571 int Chow0, Chow[16];
572 if (!Abc_TtIsUnate(t, nVars))
573 return 0;
574 Abc_TtMakePosUnate(t, nVars);
575 Chow0 = Extra_ThreshComputeChow(t, nVars, Chow);
576 Extra_ThreshSortByChow(t, nVars, Chow);
577 return Extra_ThreshSelectWeights(t, nVars, pW);
578}
579
592int Extra_ThreshHeuristic(word * t, int nVars, int * pW) {
593
594 extern char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
595 int Chow0, Chow[16], nChows, i, T = 0;
596 DdManager * dd;
597 Vec_Str_t * vCube;
598 DdNode * ddNode, * ddNodeFneg;
599 char * pIsop, * pIsopFneg;
600 if (nVars <= 1)
601 return 1;
602 if (!Abc_TtIsUnate(t, nVars))
603 return 0;
604 Abc_TtMakePosUnate(t, nVars);
605 Chow0 = Extra_ThreshComputeChow(t, nVars, Chow);
606 Extra_ThreshSortByChowInverted(t, nVars, Chow);
607 nChows = Extra_ThreshInitializeChow(nVars, Chow);
608
609 dd = (DdManager *) Abc_FrameReadManDd();
610 vCube = Vec_StrAlloc(nVars);
611 for (i = 0; i < nVars; i++)
612 Cudd_bddIthVar(dd, i);
613 ddNode = Kit_TruthToBdd(dd, (unsigned *) t, nVars, 0);
614 Cudd_Ref(ddNode);
615 pIsop = Abc_ConvertBddToSop( NULL, dd, ddNode, ddNode, nVars, 1,
616 vCube, 1);
617
618 Abc_TtNot(t, Abc_TruthWordNum(nVars));
619 ddNodeFneg = Kit_TruthToBdd(dd, (unsigned *) t, nVars, 0);
620 Cudd_Ref(ddNodeFneg);
621
622 pIsopFneg = Abc_ConvertBddToSop( NULL, dd, ddNodeFneg, ddNodeFneg,
623 nVars, 1, vCube, 1);
624
625 Cudd_RecursiveDeref(dd, ddNode);
626 Cudd_RecursiveDeref(dd, ddNodeFneg);
627
628 T = Extra_ThreshAssignWeights(t, pIsop, pIsopFneg, nVars, pW, Chow, nChows,
629 1);
630
631 for (i = 2; (i < 4) && (T == 0) && (nVars >= 6); i++)
632 T = Extra_ThreshAssignWeights(t, pIsop, pIsopFneg, nVars, pW, Chow,
633 nChows, i);
634
635 free(pIsop);
636 free(pIsopFneg);
637 Vec_StrFree(vCube);
638
639 return T;
640}
641
653void Extra_ThreshCheckTest() {
654 int nVars = 6;
655 int T, Chow0, Chow[16], Weights[16];
656// word t = s_Truths6[0] & s_Truths6[1] & s_Truths6[2] & s_Truths6[3] & s_Truths6[4];
657// word t = (s_Truths6[0] & s_Truths6[1]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[3]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[4]);
658// word t = (s_Truths6[2] & s_Truths6[1])
659// | (s_Truths6[2] & s_Truths6[0] & s_Truths6[3])
660// | (s_Truths6[2] & s_Truths6[0] & ~s_Truths6[4]);
661 word t = (s_Truths6[0] & s_Truths6[1] & s_Truths6[2])| (s_Truths6[0] & s_Truths6[1] & s_Truths6[3]) | (s_Truths6[0] & s_Truths6[1] & s_Truths6[4] & s_Truths6[5]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[3] & s_Truths6[4] & s_Truths6[5]);
662// word t = (s_Truths6[0] & s_Truths6[1]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[3]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[2] & s_Truths6[3]);
663// word t = (s_Truths6[0] & s_Truths6[1]) | (s_Truths6[0] & s_Truths6[2]) | (s_Truths6[0] & s_Truths6[3] & s_Truths6[4] & s_Truths6[5]) |
664// (s_Truths6[1] & s_Truths6[2] & s_Truths6[3]) | (s_Truths6[1] & s_Truths6[2] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[2] & s_Truths6[5]);
665 int i;
666 assert(nVars <= 8);
667 for (i = 0; i < nVars; i++)
668 printf("%d %d %d\n", i, Abc_TtPosVar(&t, nVars, i),
669 Abc_TtNegVar(&t, nVars, i));
670// word t = s_Truths6[0] & s_Truths6[1] & s_Truths6[2];
671 Chow0 = Extra_ThreshComputeChow(&t, nVars, Chow);
672 if ((T = Extra_ThreshCheck(&t, nVars, Weights)))
673 Extra_ThreshPrintChow(T, Weights, nVars);
674 else
675 printf("No threshold\n");
676}
677void Extra_ThreshHeuristicTest() {
678 int nVars = 6;
679 int T, Weights[16];
680
681 // word t = 19983902376700760000;
682 word t = (s_Truths6[0] & s_Truths6[1] & s_Truths6[2])| (s_Truths6[0] & s_Truths6[1] & s_Truths6[3]) | (s_Truths6[0] & s_Truths6[1] & s_Truths6[4] & s_Truths6[5]) | (s_Truths6[0] & s_Truths6[2] & s_Truths6[3] & s_Truths6[4] & s_Truths6[5]);
683 word * pT = &t;
684 T = Extra_ThreshHeuristic(pT, nVars, Weights);
685 Extra_ThreshPrintWeights(T, Weights, nVars);
686
687}
688
691
692ABC_NAMESPACE_IMPL_END
693
nWords
int nWords
Definition abcNpn.c:127
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Abc_FrameReadManDd
ABC_DLL void * Abc_FrameReadManDd()
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Extra_ThreshHeuristicTest
void Extra_ThreshHeuristicTest()
Definition extraBddThresh.c:677
Extra_ThreshCreateInequalities
void Extra_ThreshCreateInequalities(char *pIsop, char *pIsopFneg, int nVars, int *pWofChow, int *pChow, int nChows, int nInequalities, unsigned long **pGreaters, unsigned long **pSmallers)
Definition extraBddThresh.c:378
Extra_ThreshAssignWeights
int Extra_ThreshAssignWeights(word *t, char *pIsop, char *pIsopFneg, int nVars, int *pW, int *pChow, int nChows, int Wmin)
Definition extraBddThresh.c:434
Extra_ThreshDecrementWeights
void Extra_ThreshDecrementWeights(int nChows, int *pWofChow, int i)
Definition extraBddThresh.c:357
Extra_ThreshSelectWeights7
int Extra_ThreshSelectWeights7(word *t, int nVars, int *pW)
Definition extraBddThresh.c:271
Extra_ThreshPrintWeights
void Extra_ThreshPrintWeights(int T, int *pW, int nVars)
Definition extraBddThresh.c:545
Extra_ThreshSelectWeights6
int Extra_ThreshSelectWeights6(word *t, int nVars, int *pW)
Definition extraBddThresh.c:241
Extra_ThreshCheckTest
void Extra_ThreshCheckTest()
Definition extraBddThresh.c:653
Extra_ThreshInitializeChow
int Extra_ThreshInitializeChow(int nVars, int *pChow)
Definition extraBddThresh.c:106
Extra_ThreshCheck
int Extra_ThreshCheck(word *t, int nVars, int *pW)
Definition extraBddThresh.c:570
Extra_ThreshSelectWeights5
int Extra_ThreshSelectWeights5(word *t, int nVars, int *pW)
Definition extraBddThresh.c:214
Extra_ThreshSelectWeights
int Extra_ThreshSelectWeights(word *t, int nVars, int *pW)
Definition extraBddThresh.c:334
Extra_ThreshHeuristic
int Extra_ThreshHeuristic(word *t, int nVars, int *pW)
Definition extraBddThresh.c:592
Extra_ThreshSelectWeights4
int Extra_ThreshSelectWeights4(word *t, int nVars, int *pW)
Definition extraBddThresh.c:188
Extra_ThreshIncrementWeights
void Extra_ThreshIncrementWeights(int nChows, int *pWofChow, int i)
Definition extraBddThresh.c:351
Extra_ThreshPrintInequalities
void Extra_ThreshPrintInequalities(unsigned long **pGreaters, unsigned long **pSmallers, int nChows, int nInequalities)
Definition extraBddThresh.c:363
Extra_ThreshSortByChow
void Extra_ThreshSortByChow(word *t, int nVars, int *pChow)
Definition extraBddThresh.c:74
Extra_ThreshComputeChow
int Extra_ThreshComputeChow(word *t, int nVars, int *pChow)
Definition extraBddThresh.c:60
Extra_ThreshPrintChow
ABC_NAMESPACE_IMPL_START void Extra_ThreshPrintChow(int Chow0, int *pChow, int nVars)
DECLARATIONS ///.
Definition extraBddThresh.c:54
Extra_ThreshSelectWeights3
int Extra_ThreshSelectWeights3(word *t, int nVars, int *pW)
Definition extraBddThresh.c:161
Extra_ThreshSimplifyInequalities
void Extra_ThreshSimplifyInequalities(int nInequalities, int nChows, unsigned long **pGreaters, unsigned long **pSmallers)
Definition extraBddThresh.c:412
Extra_ThreshSortByChowInverted
void Extra_ThreshSortByChowInverted(word *t, int nVars, int *pChow)
Definition extraBddThresh.c:90
Extra_ThreshSelectWeights8
int Extra_ThreshSelectWeights8(word *t, int nVars, int *pW)
Definition extraBddThresh.c:302
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Mem_Flex_t
struct Mem_Flex_t_ Mem_Flex_t
Definition mem.h:34
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
strlen
int strlen()
free
VOID_HACK free()
malloc
char * malloc()