source: vis_dev/glu-2.3/src/calBdd/calTest.c @ 104

Last change on this file since 104 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 53.4 KB
RevLine 
[13]1/**CFile***********************************************************************
2
3  FileName    [calTest.c]
4
5  PackageName [cal]
6
7  Synopsis    [This file contains the test routines for the CAL package.]
8
9  Description [optional]
10
11  SeeAlso     [optional]
12
13  Author      [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu)
14               Jagesh Sanghavi  (sanghavi@eecs.berkeley.edu)
15               Modified and extended from the original version written
16               by David Long.
17              ]
18
19  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
20  All rights reserved.
21
22  Permission is hereby granted, without written agreement and without license
23  or royalty fees, to use, copy, modify, and distribute this software and its
24  documentation for any purpose, provided that the above copyright notice and
25  the following two paragraphs appear in all copies of this software.
26
27  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
28  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
29  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
30  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
31
32  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
33  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
34  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
35  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
36  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
37
38  Revision    [$Id: calTest.c,v 1.6 2002/08/28 19:26:39 fabio Exp $]
39
40******************************************************************************/
41
42#include "calInt.h"
43#include "time.h"
44#include <signal.h>
45
46/*---------------------------------------------------------------------------*/
47/* Constant declarations                                                     */
48/*---------------------------------------------------------------------------*/
49#define VARS 50
50#define TT_BITS 32              /* Size of tt in bits */
51#define MAX_TT_VARS 20
52#define ITERATIONS 50         /* Number of trials to run */
53#define BITS_PER_INT 32
54#define LG_BITS_PER_INT 5
55
56/*---------------------------------------------------------------------------*/
57/* Type declarations                                                         */
58/*---------------------------------------------------------------------------*/
59typedef unsigned long TruthTable_t;       /* "Truth table" */
60
61
62/*---------------------------------------------------------------------------*/
63/* Stucture declarations                                                     */
64/*---------------------------------------------------------------------------*/
65
66
67/*---------------------------------------------------------------------------*/
68/* Variable declarations                                                     */
69/*---------------------------------------------------------------------------*/
70static Cal_BddManager bddManager;
71static Cal_Bdd vars[VARS];
72static TruthTable_t cofactorMasks[]=
73{
74  0xffff0000,
75  0xff00ff00,
76  0xf0f0f0f0,
77  0xcccccccc,
78  0xaaaaaaaa,
79};
80static int TT_VARS;
81static CalAddress_t asDoubleSpace[2];
82
83
84/*---------------------------------------------------------------------------*/
85/* Macro declarations                                                        */
86/*---------------------------------------------------------------------------*/
87#define EncodingToBdd(table) (Decode(0, (table)))
88
89#if HAVE_STDARG_H
90static void Error(char *op, Cal_BddManager bddManager, Cal_Bdd result, Cal_Bdd expected, ...);
91#else
92static void Error();
93#endif
94
95/**AutomaticStart*************************************************************/
96
97/*---------------------------------------------------------------------------*/
98/* Static function prototypes                                                */
99/*---------------------------------------------------------------------------*/
100
101static double asDouble(CalAddress_t v1, CalAddress_t v2);
102static void asAddress(double n, CalAddress_t * r1, CalAddress_t * r2);
103static char * terminalIdFn(Cal_BddManager bddManager, CalAddress_t v1, CalAddress_t v2, Cal_Pointer_t pointer);
104static void PrintBdd(Cal_BddManager bddManager, Cal_Bdd f);
105static void Error(char *op, Cal_BddManager bddManager, Cal_Bdd result, Cal_Bdd expected, ...);
106static TruthTable_t Cofactor(TruthTable_t table, int var, int value);
107static Cal_Bdd Decode(int var, TruthTable_t table);
108static void TestAnd(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
109static void TestNand(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
110static void TestOr(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
111static void TestITE(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3);
112static void TestXor(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
113static void TestIdNot(Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table);
114static void TestCompose(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
115static void TestSubstitute(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3);
116static void TestVarSubstitute(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3);
117static void TestSwapVars(Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table);
118static void TestMultiwayAnd(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3);
119static void TestMultiwayOr(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3);
120static void TestMultiwayLarge(Cal_BddManager bddManager, int numBdds);
121static void TestArrayOp(Cal_BddManager bddManager, int numBdds);
122static void TestInterImpl(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
123static void TestQnt(Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table, int bfZeroBFPlusDFOne, int cacheExistsResultsFlag, int cacheOrResultsFlag);
124static void TestAssoc(Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table);
125static void TestRelProd(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, int bfZeroBFPlusDFOne, int cacheRelProdResultsFlag, int cacheAndResultsFlag, int cacheOrResultsFlag);
126static void TestReduce(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
127static void TestGenCof(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
128static void TestSize(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
129static void TestSatisfy(Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table);
130static void TestPipeline(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3);
131static void TestDump(Cal_BddManager bddManager, Cal_Bdd f);
132static void TestReorderBlock(Cal_BddManager bddManager, TruthTable_t table, Cal_Bdd f);
133static void TestReorder(Cal_BddManager bddManager, TruthTable_t table, Cal_Bdd f);
134static void handler(int ignored);
135static void RandomTests(int numVars, int iterations);
136
137/**AutomaticEnd***************************************************************/
138
139
140/*---------------------------------------------------------------------------*/
141/* Definition of exported functions                                          */
142/*---------------------------------------------------------------------------*/
143#ifdef TEST
144/**Function********************************************************************
145
146  Synopsis    [required]
147
148  Description [optional]
149
150  SideEffects [required]
151
152  SeeAlso     [optional]
153
154******************************************************************************/
155int
156main(int  argc, char ** argv)
157{
158  int numVars, iterations;
159  if(argc < 2){
160    iterations = ITERATIONS;
161  }
162  else{
163    iterations = atoi(argv[1]);
164  }
165  if(argc < 3){
166    TT_VARS = 5;
167  }
168  else {
169    TT_VARS = atoi(argv[2]);
170  }
171 
172  CalUtilSRandom((long)1);
173  numVars = TT_VARS;
174  RandomTests(numVars, iterations);
175  return 0;
176}
177#endif
178/*---------------------------------------------------------------------------*/
179/* Definition of internal functions                                          */
180/*---------------------------------------------------------------------------*/
181
182
183/*---------------------------------------------------------------------------*/
184/* Definition of static functions                                            */
185/*---------------------------------------------------------------------------*/
186/**Function********************************************************************
187
188  Synopsis    [required]
189
190  Description [optional]
191
192  SideEffects [required]
193
194  SeeAlso     [optional]
195
196******************************************************************************/
197static double
198asDouble(
199  CalAddress_t  v1,
200  CalAddress_t  v2)
201{
202  asDoubleSpace[0] = v1;
203  asDoubleSpace[1] = v2;
204  return (*(double *)asDoubleSpace);
205}
206
207/**Function********************************************************************
208
209  Synopsis    [required]
210
211  Description [optional]
212
213  SideEffects [required]
214
215  SeeAlso     [optional]
216
217******************************************************************************/
218static void
219asAddress(
220  double  n,
221  CalAddress_t * r1,
222  CalAddress_t * r2)
223{
224  (*(double *)asDoubleSpace)=n;
225  *r1 = asDoubleSpace[0];
226  *r2 = asDoubleSpace[1];
227}
228
229/**Function********************************************************************
230
231  Synopsis    [required]
232
233  Description [optional]
234
235  SideEffects [required]
236
237  SeeAlso     [optional]
238
239******************************************************************************/
240static char *
241terminalIdFn(
242  Cal_BddManager bddManager,
243  CalAddress_t  v1,
244  CalAddress_t  v2,
245  Cal_Pointer_t  pointer)
246{
247  static char result[100];
248  sprintf(result, "%g", asDouble(v1, v2));
249  return (result);
250}
251
252/**Function********************************************************************
253
254  Synopsis    [required]
255
256  Description [optional]
257
258  SideEffects [required]
259
260  SeeAlso     [optional]
261
262******************************************************************************/
263static void
264PrintBdd(
265  Cal_BddManager bddManager,
266  Cal_Bdd  f)
267{
268  Cal_BddPrintBdd(bddManager, f, Cal_BddNamingFnNone, 
269                  (Cal_TerminalIdFn_t) terminalIdFn,
270                  (Cal_Pointer_t)0, stderr); 
271}
272/**Function********************************************************************
273
274  Synopsis    [required]
275
276  Description [optional]
277
278  SideEffects [required]
279
280  SeeAlso     [optional]
281
282******************************************************************************/
283#if HAVE_STDARG_H
284static void
285Error(char *op, Cal_BddManager bddManager, Cal_Bdd result,
286      Cal_Bdd expected, ...)
287{
288  va_list ap;
289  Cal_Bdd userBdd;
290  int i;
291
292  va_start(ap, expected);
293#else
294static void
295Error(va_alist)
296va_dcl
297{
298  va_list ap;
299  char *op;
300  Cal_BddManager_t *bddManager;
301  Cal_Bdd result, expected;
302  Cal_Bdd userBdd;
303  int i;
304 
305  va_start(ap);
306  op   = va_arg(ap, char *);
307  bddManager = va_arg(ap, Cal_BddManager_t *);
308  result = va_arg(ap, Cal_Bdd);
309  expected = va_arg(ap, Cal_Bdd);
310#endif
311
312  fprintf(stderr, "\nError: operation %s:\n", op);
313  i=0;
314  while (1) {
315    if ((userBdd = va_arg(ap, Cal_Bdd))){
316          ++i;
317          fprintf(stderr, "Argument %d:\n", i);
318          Cal_BddFunctionPrint(bddManager, userBdd, "a");
319        }
320    else
321      break;
322  }
323  fprintf(stderr, "Expected result:\n");
324  Cal_BddFunctionPrint(bddManager, expected, "a");
325  fprintf(stderr, "Result:\n");
326  Cal_BddFunctionPrint(bddManager, result, "a");
327  va_end(ap);
328}
329
330/**Function********************************************************************
331
332  Synopsis    [required]
333
334  Description [optional]
335
336  SideEffects [required]
337
338  SeeAlso     [optional]
339
340******************************************************************************/
341static TruthTable_t
342Cofactor(TruthTable_t  table, int  var, int  value)
343{
344  int shift;
345 
346  shift = 1 << (TT_VARS-var-1);
347  if(value) {
348    table &= cofactorMasks[var];
349    table |= table >> shift;
350  }
351  else {
352    table &= ~cofactorMasks[var];
353    table |= table << shift;
354  }
355  return (table);
356}
357
358
359/**Function********************************************************************
360
361  Synopsis    [required]
362
363  Description [optional]
364
365  SideEffects [required]
366
367  SeeAlso     [optional]
368
369******************************************************************************/
370static Cal_Bdd
371Decode(int  var, TruthTable_t  table)
372{
373  Cal_Bdd temp1, temp2;
374  Cal_Bdd result;
375  Cal_Bdd left, right;
376  Cal_Bdd varBdd;
377
378  if(var == TT_VARS){
379    if(table & 0x1){
380      result = Cal_BddOne(bddManager);
381    }
382    else{
383      result = Cal_BddZero(bddManager);
384    }
385  }
386  else{
387    temp1 = Decode(var+1, table >> (1 << (TT_VARS-var-1)));
388    temp2 = Decode(var+1, table);
389    left = Cal_BddAnd(bddManager, vars[var], temp1);
390    varBdd = Cal_BddNot(bddManager, vars[var]);
391    right = Cal_BddAnd(bddManager, varBdd, temp2);
392    result = Cal_BddOr(bddManager, left, right);
393    /*
394    result = Cal_BddITE(bddManager, vars[var], temp1, temp2);
395    */
396    Cal_BddFree(bddManager, left);
397    Cal_BddFree(bddManager, right);
398    Cal_BddFree(bddManager, temp1);
399    Cal_BddFree(bddManager, temp2);
400    Cal_BddFree(bddManager, varBdd);
401  }
402  return (result);
403}
404
405/**Function********************************************************************
406
407  Synopsis    [required]
408
409  Description [optional]
410
411  SideEffects [required]
412
413  SeeAlso     [optional]
414
415******************************************************************************/
416static void
417TestAnd(Cal_BddManager bddManager, Cal_Bdd  f1, TruthTable_t  table1,
418        Cal_Bdd  f2, TruthTable_t  table2)
419{
420  Cal_Bdd result;
421  TruthTable_t resulttable;
422  Cal_Bdd expected;
423
424  result = Cal_BddAnd(bddManager, f1, f2);
425  resulttable = table1 & table2;
426  expected = EncodingToBdd(resulttable);
427  if(!Cal_BddIsEqual(bddManager, result, expected)){
428    Error("AND", bddManager, result, expected, f1, f2, (Cal_Bdd) 0);
429  }
430  Cal_BddFree(bddManager, result);
431  Cal_BddFree(bddManager, expected);
432}
433
434
435/**Function********************************************************************
436
437  Synopsis    [required]
438
439  Description [optional]
440
441  SideEffects [required]
442
443  SeeAlso     [optional]
444
445******************************************************************************/
446static void
447TestNand(Cal_BddManager bddManager, Cal_Bdd  f1, TruthTable_t  table1,
448        Cal_Bdd  f2, TruthTable_t  table2)
449{
450  Cal_Bdd result;
451  TruthTable_t resulttable;
452  Cal_Bdd expected;
453
454  result = Cal_BddNand(bddManager, f1, f2);
455  resulttable = ~(table1 & table2);
456  expected = EncodingToBdd(resulttable);
457  if(!Cal_BddIsEqual(bddManager, result, expected)){
458    Error("NAND", bddManager, result, expected, f1, f2, (Cal_Bdd) 0);
459  }
460  Cal_BddFree(bddManager, result);
461  Cal_BddFree(bddManager, expected);
462}
463/**Function********************************************************************
464
465  Synopsis    [required]
466
467  Description [optional]
468
469  SideEffects [required]
470
471  SeeAlso     [optional]
472
473******************************************************************************/
474static void
475TestOr(
476  Cal_BddManager bddManager,
477  Cal_Bdd  f1,
478  TruthTable_t  table1,
479  Cal_Bdd  f2,
480  TruthTable_t  table2)
481{
482  Cal_Bdd result;
483  TruthTable_t resulttable;
484  Cal_Bdd expected;
485
486  result = Cal_BddOr(bddManager, f1, f2);
487  resulttable = table1 | table2;
488  expected = EncodingToBdd(resulttable);
489  if(!Cal_BddIsEqual(bddManager, result, expected)){
490    Error("OR", bddManager,result, expected, f1, f2, (Cal_Bdd) 0);
491  }
492  Cal_BddFree(bddManager, result);
493  Cal_BddFree(bddManager, expected);
494}
495/**Function********************************************************************
496
497  Synopsis    [required]
498
499  Description [optional]
500
501  SideEffects [required]
502
503  SeeAlso     [optional]
504
505******************************************************************************/
506static void
507TestITE(
508  Cal_BddManager bddManager,
509  Cal_Bdd  f1,
510  TruthTable_t  table1,
511  Cal_Bdd  f2,
512  TruthTable_t  table2,
513  Cal_Bdd  f3,
514  TruthTable_t  table3)
515{
516  Cal_Bdd result;
517  TruthTable_t resultTable;
518  Cal_Bdd expected;
519
520  result = Cal_BddITE(bddManager, f1, f2, f3);
521  resultTable = (table1 & table2) | (~table1 & table3);
522  expected = EncodingToBdd(resultTable);
523  if(Cal_BddIsEqual(bddManager, result, expected) == 0){
524    Error("ITE", bddManager, result, expected, f1, f2, f3,
525          (Cal_Bdd) 0);
526  }
527  Cal_BddFree(bddManager, result);
528  Cal_BddFree(bddManager, expected);
529}
530/**Function********************************************************************
531
532  Synopsis    [required]
533
534  Description [optional]
535
536  SideEffects [required]
537
538  SeeAlso     [optional]
539
540******************************************************************************/
541static void
542TestXor(
543  Cal_BddManager bddManager,
544  Cal_Bdd  f1,
545  TruthTable_t  table1,
546  Cal_Bdd  f2,
547  TruthTable_t  table2)
548{
549  Cal_Bdd result;
550  TruthTable_t resulttable;
551  Cal_Bdd expected;
552
553  result = Cal_BddXor(bddManager, f1, f2);
554  resulttable = table1 ^ table2;
555  expected = EncodingToBdd(resulttable);
556  if(!Cal_BddIsEqual(bddManager, result, expected)){
557    Error("XOR", bddManager, result, expected, (Cal_Bdd) 0);
558  }
559  Cal_BddFree(bddManager, result);
560  Cal_BddFree(bddManager, expected);
561}
562
563
564/**Function********************************************************************
565
566  Synopsis    [required]
567
568  Description [optional]
569
570  SideEffects [required]
571
572  SeeAlso     [optional]
573
574******************************************************************************/
575static void
576TestIdNot(
577  Cal_BddManager bddManager,
578  Cal_Bdd  f,
579  TruthTable_t  table)
580{
581  Cal_Bdd result;
582  TruthTable_t resulttable;
583  Cal_Bdd expected;
584
585  result = Cal_BddNot(bddManager, f);
586  resulttable = ~table;
587  expected = EncodingToBdd(resulttable);
588  if(!Cal_BddIsEqual(bddManager, result, expected)){
589    Error("Not", bddManager, result, expected, (Cal_Bdd) 0);
590  }
591  Cal_BddFree(bddManager, result);
592  Cal_BddFree(bddManager, expected);
593  result = Cal_BddIdentity(bddManager, f);
594  resulttable = table;
595  expected = EncodingToBdd(resulttable);
596  if(!Cal_BddIsEqual(bddManager, result, expected)){
597    Error("Identity", bddManager, result, expected, (Cal_Bdd) 0);
598  }
599  Cal_BddFree(bddManager, result);
600  Cal_BddFree(bddManager, expected);
601 
602}
603
604
605/**Function********************************************************************
606
607  Synopsis    [required]
608
609  Description [optional]
610
611  SideEffects [required]
612
613  SeeAlso     [optional]
614
615******************************************************************************/
616static void
617TestCompose(
618  Cal_BddManager bddManager,
619  Cal_Bdd  f1,
620  TruthTable_t  table1,
621  Cal_Bdd  f2,
622  TruthTable_t  table2)
623{
624  int var;
625  Cal_Bdd result, expected;
626  TruthTable_t resulttable;
627 
628
629  var = (int)(((long)CalUtilRandom())%TT_VARS);
630
631  result = Cal_BddCompose(bddManager, vars[var], vars[var], Cal_BddOne(bddManager));
632  if(!Cal_BddIsEqual(bddManager, result, Cal_BddOne(bddManager))){
633    Cal_BddFunctionPrint(bddManager, result, "Compose"); 
634  }
635
636  result = Cal_BddCompose(bddManager, vars[var], vars[var], Cal_BddZero(bddManager));
637  if(!Cal_BddIsEqual(bddManager, result, Cal_BddZero(bddManager))){
638    Cal_BddFunctionPrint(bddManager, result, "Compose"); 
639  }
640
641  result = Cal_BddCompose(bddManager, f1, vars[var], Cal_BddOne(bddManager));
642  resulttable = Cofactor(table1, var, 1);
643  expected = EncodingToBdd(resulttable);
644  if(!Cal_BddIsEqual(bddManager, result,expected)){
645    Error("Restrict 1", bddManager, result, expected, f1, vars[var],
646          (Cal_Bdd) 0);
647  }
648  Cal_BddFree(bddManager, result);
649  Cal_BddFree(bddManager, expected);
650
651  result = Cal_BddCompose(bddManager, f1, vars[var], Cal_BddZero(bddManager));
652  resulttable = Cofactor(table1, var, 0);
653  expected = EncodingToBdd(resulttable);
654  if(!Cal_BddIsEqual(bddManager, result, expected)){
655    Error("Restrict 0", bddManager, result, expected, f1, vars[var],
656          (Cal_Bdd) 0);
657  }
658  Cal_BddFree(bddManager, result);
659  Cal_BddFree(bddManager, expected);
660
661  result = Cal_BddCompose(bddManager, f1, vars[var], f2);
662  resulttable = (table2 & Cofactor(table1, var, 1)) |
663      (~table2 & Cofactor(table1, var, 0));
664  expected = EncodingToBdd(resulttable);
665  if(!Cal_BddIsEqual(bddManager, result, expected)){
666    Error("Compose", bddManager, result, expected, f1, vars[var],
667          f2, (Cal_Bdd) 0);
668  }
669  Cal_BddFree(bddManager, result);
670  Cal_BddFree(bddManager, expected);
671}
672
673/**Function********************************************************************
674
675  Synopsis    [required]
676
677  Description [optional]
678
679  SideEffects [required]
680
681  SeeAlso     [optional]
682
683******************************************************************************/
684static void
685TestSubstitute(
686  Cal_BddManager bddManager,
687  Cal_Bdd  f1,
688  TruthTable_t  table1,
689  Cal_Bdd  f2,
690  TruthTable_t  table2,
691  Cal_Bdd  f3,
692  TruthTable_t  table3)
693{
694  int var1, var2;
695  Cal_Bdd associationInfo[6];
696  Cal_Bdd result;
697  TruthTable_t resulttable;
698  TruthTable_t temp1, temp2, temp3, temp4;
699  Cal_Bdd expected;
700  int assocId;
701 
702  var1 = (int)(((long)CalUtilRandom())%TT_VARS);
703  do{
704    var2 = (int)(((long)CalUtilRandom())%TT_VARS);
705  }while (var1 == var2);
706
707  associationInfo[0] = vars[var1];
708  associationInfo[1] = f2;
709  associationInfo[2] = vars[var2];
710  associationInfo[3] = f3;
711  associationInfo[4] = (Cal_Bdd) 0;
712  associationInfo[5] = (Cal_Bdd) 0;
713
714  assocId = Cal_AssociationInit(bddManager, associationInfo, 1);
715  Cal_AssociationSetCurrent(bddManager, assocId);
716
717  result = Cal_BddSubstitute(bddManager, f1);
718  temp1 = Cofactor(Cofactor(table1, var1, 1), var2, 1);
719  temp2 = Cofactor(Cofactor(table1, var1, 1), var2, 0);
720  temp3 = Cofactor(Cofactor(table1, var1, 0), var2, 1);
721  temp4 = Cofactor(Cofactor(table1, var1, 0), var2, 0);
722  resulttable = table2 & table3 & temp1;
723  resulttable |= table2 & ~table3 & temp2;
724  resulttable |= ~table2 & table3 & temp3;
725  resulttable |= ~table2 & ~table3 & temp4;
726  expected = EncodingToBdd(resulttable);
727  if(!Cal_BddIsEqual(bddManager, result, expected)){
728    Error("substitute", bddManager, result, expected,
729        f1, vars[var1], f2, vars[var2], f3, (Cal_Bdd) 0);
730  }
731  /*Cal_AssociationQuit(bddManager, assocId);*/
732  Cal_BddFree(bddManager, result);
733  Cal_BddFree(bddManager, expected);
734}
735
736/**Function********************************************************************
737
738  Synopsis    [required]
739
740  Description [optional]
741
742  SideEffects [required]
743
744  SeeAlso     [optional]
745
746******************************************************************************/
747static void
748TestVarSubstitute(
749  Cal_BddManager bddManager,
750  Cal_Bdd  f1,
751  TruthTable_t  table1,
752  Cal_Bdd  f2,
753  TruthTable_t  table2,
754  Cal_Bdd  f3,
755  TruthTable_t  table3)
756{
757  int var1, var2, var3, var4;
758  Cal_Bdd associationInfo[6];
759  Cal_Bdd result1, result2;
760  TruthTable_t resulttable;
761  TruthTable_t temp1, temp2, temp3, temp4;
762  Cal_Bdd expected;
763  int assocId;
764 
765  var1 = (int)(((long)CalUtilRandom())%TT_VARS);
766  do{
767    var3 = (int)(((long)CalUtilRandom())%TT_VARS);
768  }while (var1 == var3);
769
770  var2 = (int)(((long)CalUtilRandom())%TT_VARS);
771  do{
772    var4 = (int)(((long)CalUtilRandom())%TT_VARS);
773  }while (var2 == var4);
774
775  /*
776  f1 = vars[0];
777  table1 = cofactorMasks[0];
778  */
779  associationInfo[0] = vars[var1];
780  associationInfo[1] = vars[var3];
781  associationInfo[2] = vars[var2];
782  associationInfo[3] = vars[var4];
783  associationInfo[4] = (Cal_Bdd) 0;
784  associationInfo[5] = (Cal_Bdd) 0;
785
786  assocId = Cal_AssociationInit(bddManager, associationInfo, 1);
787  Cal_AssociationSetCurrent(bddManager, assocId);
788
789  result1 = Cal_BddVarSubstitute(bddManager, f1);
790  result2 = Cal_BddSubstitute(bddManager, f1);
791  temp1 = Cofactor(Cofactor(table1, var2, 1), var1, 1);
792  temp2 = Cofactor(Cofactor(table1, var2, 1), var1, 0);
793  temp3 = Cofactor(Cofactor(table1, var2, 0), var1, 1);
794  temp4 = Cofactor(Cofactor(table1, var2, 0), var1, 0);
795  resulttable = cofactorMasks[var3] & cofactorMasks[var4] & temp1;
796  resulttable |= ~cofactorMasks[var3] & cofactorMasks[var4] & temp2;
797  resulttable |= cofactorMasks[var3] & ~cofactorMasks[var4] & temp3;
798  resulttable |= ~cofactorMasks[var3] & ~cofactorMasks[var4] & temp4;
799  expected = EncodingToBdd(resulttable);
800  if(!Cal_BddIsEqual(bddManager, result1, result2)){
801    Error("var substitute and substitute differ", bddManager, result1, result2,
802        f1, vars[var1], vars[var3], vars[var2], vars[var4],
803          (Cal_Bdd) 0); 
804  }
805  if(!Cal_BddIsEqual(bddManager, result1, expected)){
806    Error("var substitute", bddManager, result1, expected,
807        f1, vars[var1], vars[var3], vars[var2], vars[var4],
808          (Cal_Bdd) 0); 
809  }
810  /*Cal_AssociationQuit(bddManager, assocId);*/
811  Cal_BddFree(bddManager, result1);
812  Cal_BddFree(bddManager, result2);
813  Cal_BddFree(bddManager, expected);
814}
815
816/**Function********************************************************************
817
818  Synopsis    [required]
819
820  Description [optional]
821
822  SideEffects [required]
823
824  SeeAlso     [optional]
825
826******************************************************************************/
827static void
828TestSwapVars(
829  Cal_BddManager bddManager,
830  Cal_Bdd  f,
831  TruthTable_t  table)
832{
833  int var1, var2;
834  Cal_Bdd result;
835  TruthTable_t resulttable;
836  TruthTable_t temp1, temp2, temp3, temp4;
837  Cal_Bdd expected;
838
839  var1 = (int)(((long)CalUtilRandom())%TT_VARS);
840  var2 = (int)(((long)CalUtilRandom())%TT_VARS);
841  result = Cal_BddSwapVars(bddManager, f, vars[var1], vars[var2]);
842  temp1 = Cofactor(Cofactor(table, var1, 1), var2, 1);
843  temp2 = Cofactor(Cofactor(table, var1, 1), var2, 0);
844  temp3 = Cofactor(Cofactor(table, var1, 0), var2, 1);
845  temp4 = Cofactor(Cofactor(table, var1, 0), var2, 0);
846  resulttable = cofactorMasks[var2] & cofactorMasks[var1] & temp1;
847  resulttable |= cofactorMasks[var2] & ~cofactorMasks[var1] & temp2;
848  resulttable |= ~cofactorMasks[var2] & cofactorMasks[var1] & temp3;
849  resulttable |= ~cofactorMasks[var2] & ~cofactorMasks[var1] & temp4;
850  expected = EncodingToBdd(resulttable);
851  if(!Cal_BddIsEqual(bddManager, result, expected)){
852    Error("swap variables", bddManager, result, expected, 
853        f, vars[var1], vars[var2], (Cal_Bdd) 0);
854  }
855  Cal_BddFree(bddManager, result);
856  Cal_BddFree(bddManager, expected);
857}
858
859/**Function********************************************************************
860
861  Synopsis    [required]
862
863  Description [optional]
864
865  SideEffects [required]
866
867  SeeAlso     [optional]
868
869******************************************************************************/
870static void
871TestMultiwayAnd(
872  Cal_BddManager bddManager,
873  Cal_Bdd  f1,
874  TruthTable_t  table1,
875  Cal_Bdd  f2,
876  TruthTable_t  table2,
877  Cal_Bdd  f3,
878  TruthTable_t  table3)
879{
880        Cal_Bdd result;
881        TruthTable_t resulttable;
882        Cal_Bdd expected;
883        Cal_Bdd *calBddArray;
884
885    calBddArray = Cal_MemAlloc(Cal_Bdd, 4);
886    calBddArray[0] = f1;
887    calBddArray[1] = f2;
888    calBddArray[2] = f3;
889    calBddArray[3] = (Cal_Bdd) 0;
890        result = Cal_BddMultiwayAnd(bddManager, calBddArray);
891        resulttable = table1 & table2 & table3;
892        expected = EncodingToBdd(resulttable);
893    if(!Cal_BddIsEqual(bddManager, result, expected)){
894      Error("Multiway And", bddManager, result, expected,
895            (Cal_Bdd) 0);
896    }
897  Cal_BddFree(bddManager, result);
898  Cal_BddFree(bddManager, expected);
899  Cal_MemFree(calBddArray);
900}
901
902/**Function********************************************************************
903
904  Synopsis    [required]
905
906  Description [optional]
907
908  SideEffects [required]
909
910  SeeAlso     [optional]
911
912******************************************************************************/
913static void
914TestMultiwayOr(
915  Cal_BddManager bddManager,
916  Cal_Bdd  f1,
917  TruthTable_t  table1,
918  Cal_Bdd  f2,
919  TruthTable_t  table2,
920  Cal_Bdd  f3,
921  TruthTable_t  table3)
922{
923  Cal_Bdd result;
924  TruthTable_t resulttable;
925  Cal_Bdd expected;
926  Cal_Bdd *calBddArray;
927 
928  calBddArray = Cal_MemAlloc(Cal_Bdd, 4);
929  calBddArray[0] = f1;
930  calBddArray[1] = f2;
931  calBddArray[2] = f3;
932  calBddArray[3] = (Cal_Bdd) 0;
933  result = Cal_BddMultiwayOr(bddManager, calBddArray);
934  resulttable = table1 | table2 | table3;
935        expected = EncodingToBdd(resulttable);
936  if(!Cal_BddIsEqual(bddManager, result, expected)){
937    Error("Multiway Or", bddManager, result, expected, (Cal_Bdd) 0);
938  }
939  Cal_BddFree(bddManager, result);
940  Cal_BddFree(bddManager, expected);
941  Cal_MemFree(calBddArray);
942}
943
944/**Function********************************************************************
945
946  Synopsis    [required]
947
948  Description [optional]
949
950  SideEffects [required]
951
952  SeeAlso     [optional]
953
954******************************************************************************/
955static void
956TestMultiwayLarge(
957  Cal_BddManager bddManager,
958  int  numBdds)
959{
960  TruthTable_t table, andResulttable, orResulttable;
961  Cal_Bdd f, andResult, orResult, andExpected, orExpected;
962  int i;
963  Cal_Bdd *calBddArray;
964 
965  andResulttable = ~0x0;
966  orResulttable = 0x0;
967  calBddArray = Cal_MemAlloc(Cal_Bdd, numBdds+1);
968  for (i=0; i<numBdds; i++){
969    table = (TruthTable_t)CalUtilRandom();
970    f = EncodingToBdd(table);
971    calBddArray[i] = f;
972    andResulttable &= table;
973    orResulttable |= table;
974  }
975  calBddArray[numBdds] = (Cal_Bdd) 0;
976  andResult = Cal_BddMultiwayAnd(bddManager, calBddArray);
977  orResult = Cal_BddMultiwayOr(bddManager, calBddArray);
978  andExpected = EncodingToBdd(andResulttable);
979  orExpected = EncodingToBdd(orResulttable);
980  if(!Cal_BddIsEqual(bddManager, andResult, andExpected)){
981    Error("Multiway And", bddManager, andResult, andExpected,
982          (Cal_Bdd) 0);
983  }
984  if(!Cal_BddIsEqual(bddManager, orResult, orExpected)){
985    Error("Multiway Or", bddManager, andResult, andExpected,
986          (Cal_Bdd) 0);
987  }
988  for (i=0; i<numBdds; i++) Cal_BddFree(bddManager, calBddArray[i]);
989  Cal_MemFree(calBddArray);
990  Cal_BddFree(bddManager, andResult);
991  Cal_BddFree(bddManager, andExpected);
992  Cal_BddFree(bddManager, orResult);
993  Cal_BddFree(bddManager, orExpected);
994}
995/**Function********************************************************************
996
997  Synopsis    [required]
998
999  Description [optional]
1000
1001  SideEffects [required]
1002
1003  SeeAlso     [optional]
1004
1005******************************************************************************/
1006static void
1007TestArrayOp(Cal_BddManager bddManager,  int  numBdds)
1008{
1009  TruthTable_t fTable, gTable;
1010  Cal_Bdd f, g, *andExpectedArray, *orExpectedArray, *calBddArray;
1011  Cal_Bdd *andResultArray, *orResultArray;
1012  int i;
1013 
1014  calBddArray = Cal_MemAlloc(Cal_Bdd, 2*numBdds+1);
1015  andExpectedArray = Cal_MemAlloc(Cal_Bdd, numBdds);
1016  orExpectedArray = Cal_MemAlloc(Cal_Bdd, numBdds);
1017  calBddArray[numBdds<<1] = (Cal_Bdd) 0;
1018
1019  for (i=0; i<numBdds; i++){
1020    fTable = (TruthTable_t)CalUtilRandom();
1021    gTable = (TruthTable_t)CalUtilRandom();
1022    f = EncodingToBdd(fTable);
1023    g = EncodingToBdd(gTable);
1024    calBddArray[i<<1] = f;
1025    calBddArray[(i<<1)+1] = g;
1026    andExpectedArray[i] = EncodingToBdd(fTable & gTable);
1027    orExpectedArray[i] = EncodingToBdd(fTable | gTable);
1028  }
1029 
1030  andResultArray = Cal_BddPairwiseAnd(bddManager, calBddArray);
1031  orResultArray = Cal_BddPairwiseOr(bddManager, calBddArray);
1032
1033  for (i=0; i<numBdds; i++){
1034    if(!Cal_BddIsEqual(bddManager, andResultArray[i], andExpectedArray[i])){
1035      Error("Array OR", bddManager, andResultArray[i], andExpectedArray[i],
1036            (Cal_Bdd) 0);
1037      break;
1038    }
1039  }
1040
1041  for (i=0; i<numBdds; i++){
1042    if(!Cal_BddIsEqual(bddManager, orResultArray[i], orExpectedArray[i])){
1043      Error("Array OR", bddManager, orResultArray[i], orExpectedArray[i],
1044            (Cal_Bdd) 0);
1045      break;
1046    }
1047  }
1048  for (i=0; i<numBdds; i++){
1049    Cal_BddFree(bddManager, calBddArray[i<<1]);
1050    Cal_BddFree(bddManager, calBddArray[(i<<1)+1]);
1051    Cal_BddFree(bddManager, andExpectedArray[i]);
1052    Cal_BddFree(bddManager, orExpectedArray[i]);
1053    Cal_BddFree(bddManager, andResultArray[i]);
1054    Cal_BddFree(bddManager, orResultArray[i]);
1055  }
1056  Cal_MemFree(calBddArray);
1057  Cal_MemFree(andExpectedArray);
1058  Cal_MemFree(orExpectedArray);
1059  Cal_MemFree(andResultArray);
1060  Cal_MemFree(orResultArray);
1061}
1062/**Function********************************************************************
1063
1064  Synopsis    [required]
1065
1066  Description [optional]
1067
1068  SideEffects [required]
1069
1070  SeeAlso     [optional]
1071
1072******************************************************************************/
1073static void
1074TestInterImpl(
1075  Cal_BddManager bddManager,
1076  Cal_Bdd  f1,
1077  TruthTable_t  table1,
1078  Cal_Bdd  f2,
1079  TruthTable_t  table2)
1080{
1081  Cal_Bdd result;
1082  TruthTable_t resulttable;
1083  Cal_Bdd expected;
1084  Cal_Bdd impliesResult;
1085
1086  result = Cal_BddIntersects(bddManager, f1, f2);
1087  resulttable = table1 & table2;
1088  expected = EncodingToBdd(resulttable);
1089  impliesResult = Cal_BddImplies(bddManager, result, expected);
1090  if(Cal_BddIsBddZero(bddManager, impliesResult) == 0){
1091    Error("intersection test", bddManager, result, expected, f1, f2,
1092          (Cal_Bdd) 0); 
1093  }
1094  Cal_BddFree(bddManager, impliesResult);
1095  Cal_BddFree(bddManager, result);
1096  Cal_BddFree(bddManager, expected);
1097}
1098/**Function********************************************************************
1099
1100  Synopsis    [required]
1101
1102  Description [optional]
1103
1104  SideEffects [required]
1105
1106  SeeAlso     [optional]
1107
1108******************************************************************************/
1109static void
1110TestQnt(Cal_BddManager bddManager, Cal_Bdd  f, TruthTable_t  table, int
1111        bfZeroBFPlusDFOne, int cacheExistsResultsFlag, int cacheOrResultsFlag)
1112{
1113  int var1, var2;
1114  Cal_Bdd assoc[3];
1115  Cal_Bdd result, expected;
1116  TruthTable_t  resultTable;
1117  int associationId;
1118 
1119  var1= (int)(((long)CalUtilRandom())%TT_VARS);
1120  do
1121    var2= (int)(((long)CalUtilRandom())%TT_VARS);
1122  while (var1 == var2);
1123  assoc[0] = vars[var1];
1124  assoc[1] = vars[var2];
1125  assoc[2] = (Cal_Bdd) 0;
1126  associationId = Cal_AssociationInit(bddManager, assoc, 0);
1127  Cal_AssociationSetCurrent(bddManager, associationId);
1128  result = Cal_BddExists(bddManager, f);
1129  resultTable = Cofactor(table, var1, 1) | Cofactor(table, var1, 0);
1130  resultTable = Cofactor(resultTable, var2, 1) | Cofactor(resultTable,
1131                                                          var2, 0); 
1132  expected = EncodingToBdd(resultTable);
1133  if(Cal_BddIsEqual(bddManager, result, expected) == 0){
1134    Error("quantification", bddManager, result, expected, f, vars[var1],
1135          vars[var2], (Cal_Bdd) 0);
1136  }
1137  /*Cal_AssociationQuit(bddManager, associationId);*/
1138  Cal_BddFree(bddManager, result);
1139  Cal_BddFree(bddManager, expected);
1140}
1141
1142/**Function********************************************************************
1143
1144  Synopsis    [required]
1145
1146  Description [optional]
1147
1148  SideEffects [required]
1149
1150  SeeAlso     [optional]
1151
1152******************************************************************************/
1153static void
1154TestAssoc(Cal_BddManager bddManager, Cal_Bdd  f, TruthTable_t  table)
1155{
1156  Cal_Bdd assoc[3];
1157  Cal_Bdd result, expected;
1158  int associationId;
1159 
1160  assoc[0] = (Cal_Bdd) 0;
1161  associationId = Cal_AssociationInit(bddManager, assoc, 0);
1162  Cal_AssociationSetCurrent(bddManager, associationId);
1163  result = Cal_BddExists(bddManager, f);
1164  expected = Cal_BddIdentity(bddManager, f);
1165  if(Cal_BddIsEqual(bddManager, result, expected) == 0){
1166    Error("quantification", bddManager, result, expected, (Cal_Bdd) 0);
1167  }
1168  Cal_BddFree(bddManager, result);
1169  Cal_BddFree(bddManager, expected);
1170}
1171
1172/**Function********************************************************************
1173
1174  Synopsis    [required]
1175
1176  Description [optional]
1177
1178  SideEffects [required]
1179
1180  SeeAlso     [optional]
1181
1182******************************************************************************/
1183static void
1184TestRelProd(Cal_BddManager bddManager, Cal_Bdd  f1, TruthTable_t
1185            table1, Cal_Bdd  f2, TruthTable_t  table2, int bfZeroBFPlusDFOne,
1186            int cacheRelProdResultsFlag, int cacheAndResultsFlag, int
1187            cacheOrResultsFlag) 
1188{
1189  int var1, var2;
1190  Cal_Bdd assoc[3];
1191  Cal_Bdd result;
1192  TruthTable_t resultTable;
1193  Cal_Bdd expected;
1194  int assocId;
1195 
1196  var1=(int)(((long)CalUtilRandom())%TT_VARS);
1197  do
1198    var2=(int)(((long)CalUtilRandom())%TT_VARS);
1199  while (var1 == var2);
1200  assoc[0] = vars[var1];
1201  assoc[1] = vars[var2];
1202  assoc[2] = (Cal_Bdd) 0;
1203  assocId = Cal_AssociationInit(bddManager, assoc, 0);
1204  Cal_AssociationSetCurrent(bddManager, assocId);
1205  result = Cal_BddRelProd(bddManager, f1, f2);
1206  table1 &= table2;
1207  resultTable = Cofactor(table1, var1, 1) | Cofactor(table1, var1, 0);
1208  resultTable = Cofactor(resultTable, var2, 1) | Cofactor(resultTable, var2, 0);
1209  expected = EncodingToBdd(resultTable);
1210  if(Cal_BddIsEqual(bddManager, result, expected) == 0){
1211    Error("relational product", bddManager, result, expected, f1, f2,
1212          vars[var1], vars[var2], (Cal_Bdd) 0);
1213  }
1214  /*Cal_AssociationQuit(bddManager, assocId);*/
1215  Cal_BddFree(bddManager, result);
1216  Cal_BddFree(bddManager, expected);
1217}
1218
1219/**Function********************************************************************
1220
1221  Synopsis    [required]
1222
1223  Description [optional]
1224
1225  SideEffects [required]
1226
1227  SeeAlso     [optional]
1228
1229******************************************************************************/
1230static void
1231TestReduce(
1232  Cal_BddManager bddManager,
1233  Cal_Bdd  f1,
1234  TruthTable_t  table1,
1235  Cal_Bdd  f2,
1236  TruthTable_t  table2)
1237{
1238  Cal_Bdd result;
1239  Cal_Bdd temp1, temp2, temp3;
1240
1241  result = Cal_BddReduce(bddManager, f1, f2);
1242  temp1 = Cal_BddXnor(bddManager, result, f1);
1243  temp2 = Cal_BddNot(bddManager, f2);
1244  temp3 = Cal_BddOr(bddManager, temp1, temp2);
1245  if(Cal_BddIsBddOne(bddManager, temp3) == 0){
1246    Error("d.c. comparison of reduce", bddManager, temp3,
1247          Cal_BddOne(bddManager), f1, f2, (Cal_Bdd) 0);
1248  }
1249  Cal_BddFree(bddManager, result);
1250  Cal_BddFree(bddManager, temp1);
1251  Cal_BddFree(bddManager, temp2);
1252  Cal_BddFree(bddManager, temp3);
1253}
1254
1255/**Function********************************************************************
1256
1257  Synopsis    [required]
1258
1259  Description [optional]
1260
1261  SideEffects [required]
1262
1263  SeeAlso     [optional]
1264
1265******************************************************************************/
1266static void
1267TestGenCof(
1268  Cal_BddManager bddManager,
1269  Cal_Bdd  f1,
1270  TruthTable_t  table1,
1271  Cal_Bdd  f2,
1272  TruthTable_t  table2)
1273{
1274  int var1, var2;
1275  Cal_Bdd result, temp1, temp2, temp3, expected;
1276  TruthTable_t resultTable;
1277
1278  result = Cal_BddCofactor(bddManager, f1, f2);
1279  temp1 = Cal_BddXnor(bddManager, result, f1);
1280  temp2 = Cal_BddNot(bddManager, f2);
1281  temp3 = Cal_BddOr(bddManager, temp1, temp2);
1282  if (Cal_BddIsBddOne(bddManager, temp3) == 0){
1283    Error("d.c. comparison of generalized cofactor", bddManager,
1284          temp3, Cal_BddOne(bddManager), f1, f2, (Cal_Bdd) 0);
1285  }
1286
1287  Cal_BddFree(bddManager, result);
1288  Cal_BddFree(bddManager, temp1);
1289  Cal_BddFree(bddManager, temp2);
1290  Cal_BddFree(bddManager, temp3);
1291  var1=(int)(((long)CalUtilRandom())%TT_VARS);
1292  do
1293    var2=(int)(((long)CalUtilRandom())%TT_VARS);
1294  while (var1 == var2);
1295  temp1 = Cal_BddNot(bddManager, vars[var2]);
1296  temp2 = Cal_BddAnd(bddManager, vars[var1], temp1);
1297  Cal_BddFree(bddManager, temp1);
1298  result = Cal_BddCofactor(bddManager, f1, temp2);
1299  resultTable = Cofactor(Cofactor(table1, var1, 1), var2, 0);
1300  expected = EncodingToBdd(resultTable);
1301  if (Cal_BddIsEqual(bddManager, result, expected) == 0){
1302    Error("generalized cofactor", bddManager, result, expected, f1,
1303          temp2, (Cal_Bdd) 0);
1304  }
1305  Cal_BddFree(bddManager, result);
1306  Cal_BddFree(bddManager, expected);
1307  Cal_BddFree(bddManager, temp2);
1308}
1309/**Function********************************************************************
1310
1311  Synopsis    [required]
1312
1313  Description [optional]
1314
1315  SideEffects [required]
1316
1317  SeeAlso     [optional]
1318
1319******************************************************************************/
1320static void
1321TestSize(
1322  Cal_BddManager bddManager,
1323  Cal_Bdd  f1,
1324  TruthTable_t  table1,
1325  Cal_Bdd  f2,
1326  TruthTable_t  table2)
1327{
1328  int i;
1329  long size;
1330  long profile[MAX_TT_VARS+1];
1331  Cal_Bdd fs[3];
1332
1333  size = Cal_BddSize(bddManager, f1, 1);
1334  Cal_BddProfile(bddManager, f1, profile, 1);
1335  for(i = 0; i < TT_VARS+1; i++){
1336    size -= profile[i];
1337  }
1338  if(size){
1339    fprintf(stderr, "\nError: size count vs. profile sum:\n");
1340    fprintf(stderr, "Argument:\n");
1341    Cal_BddFunctionPrint(bddManager, f1, "f1");
1342  }
1343
1344  size = Cal_BddSize(bddManager, f1, 0);
1345  Cal_BddProfile(bddManager, f1, profile, 0);
1346  for(i = 0; i < TT_VARS+1; i++){
1347    size -= profile[i];
1348  }
1349  if(size){
1350    fprintf(stderr, "\nError: no negout size count vs. profile sum:\n");
1351    fprintf(stderr, "Argument:\n");
1352    Cal_BddFunctionPrint(bddManager, f1, "f1");
1353  }
1354
1355
1356  fs[0] = f1;
1357  fs[1] = f2;
1358  fs[2] = (Cal_Bdd) 0;
1359
1360  size = Cal_BddSizeMultiple(bddManager, fs, 1);
1361  Cal_BddProfileMultiple(bddManager, fs, profile, 1);
1362  for(i = 0; i < TT_VARS+1; i++){
1363    size -= profile[i];
1364  }
1365  if(size){
1366    fprintf(stderr,"\nError: multiple size count vs. multiple profile sum:\n");
1367    fprintf(stderr, "Argument 1:\n");
1368    Cal_BddFunctionPrint(bddManager, f1, "f1");
1369    fprintf(stderr, "Argument 2:\n");
1370    Cal_BddFunctionPrint(bddManager, f2, "f2");
1371  }
1372
1373  size = Cal_BddSizeMultiple(bddManager, fs, 0);
1374  Cal_BddProfileMultiple(bddManager, fs, profile, 0);
1375  for(i = 0; i < TT_VARS+1; i++){
1376    size -= profile[i];
1377  }
1378  if(size){
1379    fprintf(stderr,"\nError: multiple no negout size count vs. multiple profile sum:\n");
1380    fprintf(stderr, "Argument 1:\n");
1381    Cal_BddFunctionPrint(bddManager, f1, "f1");
1382    fprintf(stderr, "Argument 2:\n");
1383    Cal_BddFunctionPrint(bddManager, f2, "f2");
1384  }
1385}
1386
1387/**Function********************************************************************
1388
1389  Synopsis    [required]
1390
1391  Description [optional]
1392
1393  SideEffects [required]
1394
1395  SeeAlso     [optional]
1396
1397******************************************************************************/
1398static void
1399TestSatisfy(
1400  Cal_BddManager bddManager,
1401  Cal_Bdd  f,
1402  TruthTable_t  table)
1403{
1404  int var1, var2;
1405  Cal_Bdd assoc[MAX_TT_VARS+1];
1406  Cal_Bdd result;
1407  Cal_Bdd temp1, temp2, temp3;
1408  int assocId;
1409 
1410  if(Cal_BddIsBddZero(bddManager, f)){
1411    return;
1412  }
1413  result = Cal_BddSatisfy(bddManager, f);
1414  temp1 = Cal_BddNot(bddManager, f);
1415  temp2 = Cal_BddIntersects(bddManager, temp1, result);
1416  if(!Cal_BddIsBddZero(bddManager, temp2)){
1417    Error("intersection of satisfy result with negated argument",
1418        bddManager, temp2, Cal_BddZero(bddManager), f, (Cal_Bdd) 0);
1419  }
1420  Cal_BddFree(bddManager, temp1);
1421  Cal_BddFree(bddManager, temp2);
1422
1423  var1 = (int)(((long)CalUtilRandom())%TT_VARS);
1424  do{
1425    var2 = (int)(((long)CalUtilRandom())%TT_VARS);
1426  }while (var1 == var2);
1427  assoc[0] = vars[var1];
1428  assoc[1] = vars[var2];
1429  assoc[2] = (Cal_Bdd) 0;
1430  assocId = Cal_AssociationInit(bddManager, assoc, 0);
1431  Cal_AssociationSetCurrent(bddManager, assocId);
1432  temp1 = Cal_BddSatisfySupport(bddManager, result);
1433  temp2 = Cal_BddNot(bddManager, result);
1434  temp3 = Cal_BddIntersects(bddManager, temp2, temp1);
1435  if(!Cal_BddIsBddZero(bddManager, temp3)){
1436    Error("intersection of satisfy support result with negated argument",
1437        bddManager, temp3, Cal_BddZero(bddManager), result,
1438        (Cal_Bdd) 0);
1439  }
1440  Cal_BddFree(bddManager, result);
1441  Cal_BddFree(bddManager, temp1);
1442  Cal_BddFree(bddManager, temp2);
1443  Cal_BddFree(bddManager, temp3);
1444  temp1 = Cal_BddCompose(bddManager, f, vars[var1], Cal_BddZero(bddManager));
1445  temp2 = Cal_BddCompose(bddManager, f, vars[var1], Cal_BddOne(bddManager));
1446  if(Cal_BddSatisfyingFraction(bddManager, temp1) + 
1447      Cal_BddSatisfyingFraction(bddManager, temp2) !=
1448      2.0 * Cal_BddSatisfyingFraction(bddManager, f)){
1449    fprintf(stderr, "\nError: operation satisfying fraction:\n");
1450    fprintf(stderr, "Argument:\n");
1451    Cal_BddFunctionPrint(bddManager, f, "f");
1452    fprintf(stderr, "Cofactor on:\n");
1453    Cal_BddFunctionPrint(bddManager, vars[var1], "var");
1454  }
1455  /*Cal_AssociationQuit(bddManager, assocId);*/
1456  Cal_BddFree(bddManager, temp1);
1457  Cal_BddFree(bddManager, temp2);
1458}
1459
1460/**Function********************************************************************
1461
1462  Synopsis    [required]
1463
1464  Description [optional]
1465
1466  SideEffects [required]
1467
1468  SeeAlso     [optional]
1469
1470******************************************************************************/
1471static void
1472TestPipeline(Cal_BddManager bddManager,
1473             Cal_Bdd  f1,
1474             TruthTable_t  table1,
1475             Cal_Bdd  f2,
1476             TruthTable_t  table2,
1477             Cal_Bdd  f3,
1478             TruthTable_t  table3)
1479{
1480  Cal_Bdd temp1, temp2, temp3, temp4, temp5, result, expected;
1481  TruthTable_t table;
1482
1483  Cal_PipelineInit(bddManager, CAL_AND);
1484  Cal_PipelineSetDepth(bddManager, 0);
1485  temp1 = Cal_PipelineCreateProvisionalBdd(bddManager, f1, f2);
1486  temp2 = Cal_PipelineCreateProvisionalBdd(bddManager, f1, f3);
1487  temp3 = Cal_PipelineCreateProvisionalBdd(bddManager, f1, temp1);
1488  temp4 = Cal_PipelineCreateProvisionalBdd(bddManager, f2, temp2);
1489  temp5 = Cal_PipelineCreateProvisionalBdd(bddManager, temp3, temp4);
1490  result = Cal_PipelineCreateProvisionalBdd(bddManager, temp4, temp5);
1491  Cal_PipelineExecute(bddManager);
1492  result = Cal_PipelineUpdateProvisionalBdd(bddManager, result);
1493  Cal_PipelineQuit(bddManager);
1494
1495  table = table1 & table2 & table3;
1496  expected = EncodingToBdd(table);
1497
1498  if (Cal_BddIsEqual(bddManager, result, expected) == 0){
1499    Error("pipeline", bddManager, result, expected, (Cal_Bdd) 0);
1500  }
1501  Cal_BddFree(bddManager, result);
1502  Cal_BddFree(bddManager, expected);
1503}
1504
1505/**Function********************************************************************
1506
1507  Synopsis    [required]
1508
1509  Description [optional]
1510
1511  SideEffects [required]
1512
1513  SeeAlso     [optional]
1514
1515******************************************************************************/
1516static void
1517TestDump(Cal_BddManager bddManager, Cal_Bdd f)
1518{
1519  FILE *fp;
1520  int i, j;
1521  Cal_Bdd dumpVars[MAX_TT_VARS];
1522  Cal_Bdd temp, result;
1523  int err;
1524
1525  if (!(fp=tmpfile()))
1526    {
1527      fprintf(stderr, "could not open temporary file\n");
1528      exit(1);
1529    }
1530  for (i=0; i < TT_VARS; ++i)
1531    dumpVars[i]=vars[i];
1532  dumpVars[i]= (Cal_Bdd) 0;
1533  for (i=0; i < TT_VARS-1; ++i)
1534    {
1535      j=i+(int)(((long)CalUtilRandom())%(TT_VARS-i));
1536      temp=dumpVars[i];
1537      dumpVars[i]=dumpVars[j];
1538      dumpVars[j]=temp;
1539    }
1540  if (!Cal_BddDumpBdd(bddManager, f, dumpVars, fp))
1541    {
1542      fprintf(stderr, "Error: dump failure:\n");
1543      fprintf(stderr, "Argument:\n");
1544      PrintBdd(bddManager, f);
1545      fclose(fp);
1546      return;
1547    }
1548  rewind(fp);
1549  if (!(result=Cal_BddUndumpBdd(bddManager, dumpVars, fp, &err)) || err)
1550    {
1551      fprintf(stderr, "Error: undump failure: code %d:\n", err);
1552      fprintf(stderr, "Argument:\n");
1553      PrintBdd(bddManager, f);
1554      fclose(fp);
1555      return;
1556    }
1557  fclose(fp);
1558  if (result != f)
1559    Error("dump/undump", bddManager, result, f, f, (Cal_Bdd) 0);
1560  Cal_BddFree(bddManager, result);
1561}
1562
1563
1564/**Function********************************************************************
1565
1566  Synopsis    [required]
1567
1568  Description [optional]
1569
1570  SideEffects [required]
1571
1572  SeeAlso     [optional]
1573
1574******************************************************************************/
1575static void
1576TestReorderBlock(Cal_BddManager bddManager, TruthTable_t table, Cal_Bdd f)
1577{
1578  Cal_Bdd newFunction;
1579  Cal_Block block1, block2, block3;
1580 
1581  /*if (CalUtilRandom()&0x1){*/
1582  if (1){
1583    fprintf(stdout, "Using Window\n");
1584    Cal_BddDynamicReordering(bddManager, CAL_REORDER_WINDOW);
1585  }
1586  else{
1587    fprintf(stdout, "Using Sift\n");
1588    Cal_BddDynamicReordering(bddManager, CAL_REORDER_SIFT);
1589  }
1590  /* Create some blocks */
1591  block1 = Cal_BddNewVarBlock(bddManager,
1592                              vars[bddManager->indexToId[0]-1],
1593                              4); 
1594  block2 = Cal_BddNewVarBlock(bddManager,
1595                              vars[bddManager->indexToId[4]-1],
1596                              4);
1597  block3 = Cal_BddNewVarBlock(bddManager,
1598                              vars[bddManager->indexToId[8]-1],
1599                              4);
1600  Cal_BddVarBlockReorderable(bddManager, block2, 1);
1601  Cal_BddReorder(bddManager);
1602  newFunction = EncodingToBdd(table);
1603  if (Cal_BddIsEqual(bddManager, f, newFunction) == 0){
1604    Error("Reordering (window)", bddManager, newFunction, f, (Cal_Bdd) 0);
1605  }
1606  Cal_BddFree(bddManager, newFunction);
1607}
1608
1609/**Function********************************************************************
1610
1611  Synopsis    [required]
1612
1613  Description [optional]
1614
1615  SideEffects [required]
1616
1617  SeeAlso     [optional]
1618
1619******************************************************************************/
1620static void
1621TestReorder(Cal_BddManager bddManager, TruthTable_t table, Cal_Bdd f)
1622{
1623  Cal_Bdd newFunction;
1624 
1625  if (CalUtilRandom()&0x1){
1626    fprintf(stdout, "Using Window\n");
1627    Cal_BddDynamicReordering(bddManager, CAL_REORDER_WINDOW);
1628  }
1629  else{
1630    fprintf(stdout, "Using Sift\n");
1631    Cal_BddDynamicReordering(bddManager, CAL_REORDER_SIFT);
1632  }
1633  if (CalUtilRandom()&0x1){
1634    bddManager->reorderMethod = CAL_REORDER_METHOD_BF;
1635  }
1636  else{
1637    bddManager->reorderMethod = CAL_REORDER_METHOD_DF;
1638  }
1639  Cal_BddReorder(bddManager);
1640  newFunction = EncodingToBdd(table);
1641  if (Cal_BddIsEqual(bddManager, f, newFunction) == 0){
1642    Error("Reordering (window)", bddManager, newFunction, f, (Cal_Bdd) 0);
1643  }
1644  Cal_BddFree(bddManager, newFunction);
1645}
1646
1647/**Function********************************************************************
1648
1649  Synopsis    [required]
1650
1651  Description [optional]
1652
1653  SideEffects [required]
1654
1655  SeeAlso     [optional]
1656
1657******************************************************************************/
1658static void
1659handler(int ignored)
1660{
1661  printf("arthimetic exception ############\n");
1662}
1663
1664
1665
1666
1667/**Function********************************************************************
1668
1669  Synopsis    [required]
1670
1671  Description [optional]
1672
1673  SideEffects [required]
1674
1675  SeeAlso     [optional]
1676
1677******************************************************************************/
1678static void
1679RandomTests(int numVars, int  iterations)
1680{
1681  int i, seed;
1682  TruthTable_t table1, table2, table3;
1683  Cal_Bdd f1, f2, f3/*, f4*/;
1684  CalAssociation_t *assoc, *nextAssoc;
1685  /* Cal_Block block1, block2; */
1686 
1687  signal(SIGFPE, handler);
1688 
1689  printf("Random operation tests...\n");
1690  bddManager  = Cal_BddManagerInit();
1691  seed = 1;
1692  /*
1693  (void) time((time_t *)&seed);
1694  */
1695  CalUtilSRandom((long)seed);
1696
1697  for(i = 0; i < numVars; ++i){
1698    vars[i] = Cal_BddManagerCreateNewVarLast(bddManager);
1699  }
1700 
1701  /*
1702  f1 = Cal_BddAnd(bddManager, vars[1], vars[2]);
1703  f2 = Cal_BddAnd(bddManager, vars[1], vars[0]);
1704  f3 = Cal_BddOr(bddManager, f1, f2);
1705  Cal_BddFree(bddManager, f1);
1706  Cal_BddFree(bddManager, f2);
1707  Cal_BddDynamicReordering(bddManager, Cal_BddReorderSift);
1708  fprintf(stdout,"Original function:\n");
1709  Cal_BddFunctionPrint(bddManager, f3, "a");
1710  Cal_BddReorderNew(bddManager);
1711  f1 = Cal_BddAnd(bddManager, vars[1], vars[2]);
1712  f2 = Cal_BddAnd(bddManager, vars[1], vars[0]);
1713  f4 = Cal_BddOr(bddManager, f1, f2);
1714  Cal_BddFree(bddManager, f1);
1715  Cal_BddFree(bddManager, f2);
1716  fprintf(stdout,"New function:\n");
1717  Cal_BddFunctionPrint(bddManager, f4, "a");
1718  Cal_Assert(Cal_BddIsEqual(bddManager, f3, f4));
1719  Cal_BddFree(bddManager, f3);
1720  Cal_BddFree(bddManager, f4);
1721  */
1722
1723/*
1724  block1 = Cal_BddNewVarBlock(bddManager,
1725                              vars[0], 2);
1726  block2 = Cal_BddNewVarBlock(bddManager, vars[3], 2);
1727  Cal_BddVarBlockReorderable(bddManager, block2, 1);
1728  */
1729  for (i = 0; i < iterations; i++){
1730    printf("Iteration %3d\n", i);
1731    table1 = (TruthTable_t)CalUtilRandom();
1732    table2 = (TruthTable_t)CalUtilRandom();
1733    table3 = (TruthTable_t)CalUtilRandom();
1734    f1 = EncodingToBdd(table1);
1735    f2 = EncodingToBdd(table2);
1736    f3 = EncodingToBdd(table3);
1737
1738    /* The following tests will fail if you do not use 5 variables */
1739    if (numVars == 5){
1740      TestGenCof(bddManager, f1, table1, f2, table2);
1741      TestSubstitute(bddManager, f1, table1, f2, table2, f3, table3);
1742      TestSwapVars(bddManager, f1, table1);
1743      TestCompose(bddManager, f1, table1, f2, table2);
1744      TestRelProd(bddManager, f1, table1, f2, table2, 0, 0, 0, 0);
1745      TestQnt(bddManager, f1, table1, 1, 1, 1);
1746      TestVarSubstitute(bddManager, f1, table1, f2, table2, f3,
1747                        table3);
1748    }
1749    /* The following can be tested for larger number of variables */
1750    TestAnd(bddManager,f1, table1, f2, table2);
1751    TestIdNot(bddManager, f1, table1);
1752    TestITE(bddManager, f1, table1, f2, table2, f3, table3);
1753    TestNand(bddManager,f1, table1, f2, table2);
1754    TestOr(bddManager, f1, table1, f2, table2);
1755    TestXor(bddManager,f1, table1, f2, table2);
1756    TestMultiwayOr(bddManager, f1, table1, f2, table2, f3, table3);
1757    TestMultiwayAnd(bddManager, f1, table1, f2, table2, f3, table3);
1758    TestArrayOp(bddManager, 10);
1759    TestInterImpl(bddManager, f1, table1, f2, table2);
1760    TestReduce(bddManager, f1, table1, f2, table2);
1761    TestSize(bddManager, f1, table1, f2, table2);
1762    TestSatisfy(bddManager, f1, table1);
1763    TestAssoc(bddManager, f1, table1);
1764    TestDump(bddManager, f1); 
1765    TestPipeline(bddManager, f1, table1, f2, table2, f3, table3);
1766    TestReorder(bddManager, table1, f1);
1767    Cal_BddFree(bddManager, f1);
1768    Cal_BddFree(bddManager, f2);
1769    Cal_BddFree(bddManager, f3);
1770        if (i && (i % 10 == 0)) {
1771      Cal_BddManagerGC(bddManager);
1772      (void)CalPackNodes(bddManager);
1773    }
1774  }
1775  for(i = 0; i < numVars; ++i){
1776    Cal_BddFree(bddManager, vars[i]);
1777  }
1778  Cal_BddStats(bddManager, stdout);
1779  for(assoc = bddManager->associationList;
1780      assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
1781    nextAssoc = assoc->next;
1782    for (i=1; i <= bddManager->numVars; i++){
1783      if (CalBddIsBddNull(bddManager, assoc->varAssociation[i]) == 0){
1784        CalBddDcrRefCount(assoc->varAssociation[i]);
1785        assoc->varAssociation[i] = bddManager->bddNull;
1786        assoc->lastBddIndex = -1;
1787      }
1788    }
1789  }
1790  /* fix temporary association */
1791  assoc = bddManager->tempAssociation;
1792  for (i=1; i <= bddManager->numVars; i++){
1793    if (CalBddIsBddNull(bddManager, assoc->varAssociation[i]) == 0){
1794      CalBddDcrRefCount(assoc->varAssociation[i]);
1795      assoc->varAssociation[i] = bddManager->bddNull;
1796      assoc->lastBddIndex = -1;
1797    }
1798  }
1799
1800  Cal_BddManagerGC(bddManager);
1801  Cal_BddStats(bddManager, stdout);
1802  /*CalUniqueTablePrint(bddManager);*/
1803  Cal_BddManagerQuit(bddManager);
1804}
Note: See TracBrowser for help on using the repository browser.