glu-2.2: src/calBdd/calTest.c Source File

00001 
00042 #include "calInt.h"
00043 #include "time.h"
00044 #include <signal.h>
00045 
00046 /*---------------------------------------------------------------------------*/
00047 /* Constant declarations                                                     */
00048 /*---------------------------------------------------------------------------*/
00049 #define VARS 50
00050 #define TT_BITS 32              /* Size of tt in bits */
00051 #define MAX_TT_VARS 20
00052 #define ITERATIONS 50         /* Number of trials to run */
00053 #define BITS_PER_INT 32
00054 #define LG_BITS_PER_INT 5
00055 
00056 /*---------------------------------------------------------------------------*/
00057 /* Type declarations                                                         */
00058 /*---------------------------------------------------------------------------*/
00059 typedef unsigned long TruthTable_t;       /* "Truth table" */
00060 
00061 
00062 /*---------------------------------------------------------------------------*/
00063 /* Stucture declarations                                                     */
00064 /*---------------------------------------------------------------------------*/
00065 
00066 
00067 /*---------------------------------------------------------------------------*/
00068 /* Variable declarations                                                     */
00069 /*---------------------------------------------------------------------------*/
00070 static Cal_BddManager bddManager;
00071 static Cal_Bdd vars[VARS];
00072 static TruthTable_t cofactorMasks[]=
00073 {
00074   0xffff0000,
00075   0xff00ff00,
00076   0xf0f0f0f0,
00077   0xcccccccc,
00078   0xaaaaaaaa,
00079 };
00080 static int TT_VARS;
00081 static CalAddress_t asDoubleSpace[2];
00082 
00083 
00084 /*---------------------------------------------------------------------------*/
00085 /* Macro declarations                                                        */
00086 /*---------------------------------------------------------------------------*/
00087 #define EncodingToBdd(table) (Decode(0, (table)))
00088 
00089 #if HAVE_STDARG_H
00090 static void Error(char *op, Cal_BddManager bddManager, Cal_Bdd result, Cal_Bdd expected, ...);
00091 #else
00092 static void Error();
00093 #endif
00094 
00097 /*---------------------------------------------------------------------------*/
00098 /* Static function prototypes                                                */
00099 /*---------------------------------------------------------------------------*/
00100 
00101 static double asDouble(CalAddress_t v1, CalAddress_t v2);
00102 static void asAddress(double n, CalAddress_t * r1, CalAddress_t * r2);
00103 static char * terminalIdFn(Cal_BddManager bddManager, CalAddress_t v1, CalAddress_t v2, Cal_Pointer_t pointer);
00104 static void PrintBdd(Cal_BddManager bddManager, Cal_Bdd f);
00105 static void Error(char *op, Cal_BddManager bddManager, Cal_Bdd result, Cal_Bdd expected, ...);
00106 static TruthTable_t Cofactor(TruthTable_t table, int var, int value);
00107 static Cal_Bdd Decode(int var, TruthTable_t table);
00108 static void TestAnd(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
00109 static void TestNand(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
00110 static void TestOr(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
00111 static void TestITE(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3);
00112 static void TestXor(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
00113 static void TestIdNot(Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table);
00114 static void TestCompose(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
00115 static void TestSubstitute(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3);
00116 static void TestVarSubstitute(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3);
00117 static void TestSwapVars(Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table);
00118 static void TestMultiwayAnd(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3);
00119 static void TestMultiwayOr(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3);
00120 static void TestMultiwayLarge(Cal_BddManager bddManager, int numBdds);
00121 static void TestArrayOp(Cal_BddManager bddManager, int numBdds);
00122 static void TestInterImpl(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
00123 static void TestQnt(Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table, int bfZeroBFPlusDFOne, int cacheExistsResultsFlag, int cacheOrResultsFlag);
00124 static void TestAssoc(Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table);
00125 static 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);
00126 static void TestReduce(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
00127 static void TestGenCof(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
00128 static void TestSize(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2);
00129 static void TestSatisfy(Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table);
00130 static void TestPipeline(Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3);
00131 static void TestDump(Cal_BddManager bddManager, Cal_Bdd f);
00132 static void TestReorderBlock(Cal_BddManager bddManager, TruthTable_t table, Cal_Bdd f);
00133 static void TestReorder(Cal_BddManager bddManager, TruthTable_t table, Cal_Bdd f);
00134 static void handler(int ignored);
00135 static void RandomTests(int numVars, int iterations);
00136 
00140 /*---------------------------------------------------------------------------*/
00141 /* Definition of exported functions                                          */
00142 /*---------------------------------------------------------------------------*/
00143 #ifdef TEST
00144 
00155 int
00156 main(int  argc, char ** argv)
00157 {
00158   int numVars, iterations;
00159   if(argc < 2){
00160     iterations = ITERATIONS;
00161   }
00162   else{
00163     iterations = atoi(argv[1]);
00164   }
00165   if(argc < 3){
00166     TT_VARS = 5;
00167   }
00168   else {
00169     TT_VARS = atoi(argv[2]);
00170   }
00171   
00172   CalUtilSRandom((long)1);
00173   numVars = TT_VARS;
00174   RandomTests(numVars, iterations);
00175   return 0;
00176 }
00177 #endif
00178 /*---------------------------------------------------------------------------*/
00179 /* Definition of internal functions                                          */
00180 /*---------------------------------------------------------------------------*/
00181 
00182 
00183 /*---------------------------------------------------------------------------*/
00184 /* Definition of static functions                                            */
00185 /*---------------------------------------------------------------------------*/
00197 static double
00198 asDouble(
00199   CalAddress_t  v1,
00200   CalAddress_t  v2)
00201 {
00202   asDoubleSpace[0] = v1;
00203   asDoubleSpace[1] = v2;
00204   return (*(double *)asDoubleSpace);
00205 }
00206 
00218 static void
00219 asAddress(
00220   double  n,
00221   CalAddress_t * r1,
00222   CalAddress_t * r2)
00223 {
00224   (*(double *)asDoubleSpace)=n;
00225   *r1 = asDoubleSpace[0];
00226   *r2 = asDoubleSpace[1];
00227 }
00228 
00240 static char *
00241 terminalIdFn(
00242   Cal_BddManager bddManager,
00243   CalAddress_t  v1,
00244   CalAddress_t  v2,
00245   Cal_Pointer_t  pointer)
00246 {
00247   static char result[100];
00248   sprintf(result, "%g", asDouble(v1, v2));
00249   return (result);
00250 }
00251 
00263 static void
00264 PrintBdd(
00265   Cal_BddManager bddManager,
00266   Cal_Bdd  f)
00267 {
00268   Cal_BddPrintBdd(bddManager, f, Cal_BddNamingFnNone, 
00269                   (Cal_TerminalIdFn_t) terminalIdFn,
00270                   (Cal_Pointer_t)0, stderr); 
00271 }
00283 #if HAVE_STDARG_H
00284 static void
00285 Error(char *op, Cal_BddManager bddManager, Cal_Bdd result,
00286       Cal_Bdd expected, ...)
00287 {
00288   va_list ap;
00289   Cal_Bdd userBdd;
00290   int i;
00291 
00292   va_start(ap, expected);
00293 #else
00294 static void
00295 Error(va_alist)
00296 va_dcl
00297 {
00298   va_list ap;
00299   char *op;
00300   Cal_BddManager_t *bddManager;
00301   Cal_Bdd result, expected;
00302   Cal_Bdd userBdd;
00303   int i;
00304   
00305   va_start(ap);
00306   op   = va_arg(ap, char *);
00307   bddManager = va_arg(ap, Cal_BddManager_t *);
00308   result = va_arg(ap, Cal_Bdd);
00309   expected = va_arg(ap, Cal_Bdd);
00310 #endif
00311 
00312   fprintf(stderr, "\nError: operation %s:\n", op);
00313   i=0;
00314   while (1) {
00315     if ((userBdd = va_arg(ap, Cal_Bdd))){
00316           ++i;
00317           fprintf(stderr, "Argument %d:\n", i);
00318           Cal_BddFunctionPrint(bddManager, userBdd, "a");
00319         }
00320     else
00321       break;
00322   }
00323   fprintf(stderr, "Expected result:\n");
00324   Cal_BddFunctionPrint(bddManager, expected, "a");
00325   fprintf(stderr, "Result:\n");
00326   Cal_BddFunctionPrint(bddManager, result, "a");
00327   va_end(ap);
00328 }
00329 
00341 static TruthTable_t
00342 Cofactor(TruthTable_t  table, int  var, int  value)
00343 {
00344   int shift;
00345   
00346   shift = 1 << (TT_VARS-var-1);
00347   if(value) {
00348     table &= cofactorMasks[var];
00349     table |= table >> shift;
00350   }
00351   else {
00352     table &= ~cofactorMasks[var];
00353     table |= table << shift;
00354   }
00355   return (table);
00356 }
00357 
00358 
00370 static Cal_Bdd
00371 Decode(int  var, TruthTable_t  table)
00372 {
00373   Cal_Bdd temp1, temp2;
00374   Cal_Bdd result;
00375   Cal_Bdd left, right;
00376   Cal_Bdd varBdd;
00377 
00378   if(var == TT_VARS){
00379     if(table & 0x1){
00380       result = Cal_BddOne(bddManager);
00381     }
00382     else{
00383       result = Cal_BddZero(bddManager);
00384     }
00385   }
00386   else{
00387     temp1 = Decode(var+1, table >> (1 << (TT_VARS-var-1)));
00388     temp2 = Decode(var+1, table);
00389     left = Cal_BddAnd(bddManager, vars[var], temp1);
00390     varBdd = Cal_BddNot(bddManager, vars[var]);
00391     right = Cal_BddAnd(bddManager, varBdd, temp2);
00392     result = Cal_BddOr(bddManager, left, right);
00393     /*
00394     result = Cal_BddITE(bddManager, vars[var], temp1, temp2);
00395     */
00396     Cal_BddFree(bddManager, left);
00397     Cal_BddFree(bddManager, right);
00398     Cal_BddFree(bddManager, temp1);
00399     Cal_BddFree(bddManager, temp2);
00400     Cal_BddFree(bddManager, varBdd);
00401   }
00402   return (result);
00403 }
00404 
00416 static void
00417 TestAnd(Cal_BddManager bddManager, Cal_Bdd  f1, TruthTable_t  table1,
00418         Cal_Bdd  f2, TruthTable_t  table2)
00419 {
00420   Cal_Bdd result;
00421   TruthTable_t resulttable;
00422   Cal_Bdd expected;
00423 
00424   result = Cal_BddAnd(bddManager, f1, f2);
00425   resulttable = table1 & table2;
00426   expected = EncodingToBdd(resulttable);
00427   if(!Cal_BddIsEqual(bddManager, result, expected)){
00428     Error("AND", bddManager, result, expected, f1, f2, (Cal_Bdd) 0);
00429   }
00430   Cal_BddFree(bddManager, result);
00431   Cal_BddFree(bddManager, expected);
00432 }
00433 
00434 
00446 static void
00447 TestNand(Cal_BddManager bddManager, Cal_Bdd  f1, TruthTable_t  table1,
00448         Cal_Bdd  f2, TruthTable_t  table2)
00449 {
00450   Cal_Bdd result;
00451   TruthTable_t resulttable;
00452   Cal_Bdd expected;
00453 
00454   result = Cal_BddNand(bddManager, f1, f2);
00455   resulttable = ~(table1 & table2);
00456   expected = EncodingToBdd(resulttable);
00457   if(!Cal_BddIsEqual(bddManager, result, expected)){
00458     Error("NAND", bddManager, result, expected, f1, f2, (Cal_Bdd) 0);
00459   }
00460   Cal_BddFree(bddManager, result);
00461   Cal_BddFree(bddManager, expected);
00462 }
00474 static void
00475 TestOr(
00476   Cal_BddManager bddManager,
00477   Cal_Bdd  f1,
00478   TruthTable_t  table1,
00479   Cal_Bdd  f2,
00480   TruthTable_t  table2)
00481 {
00482   Cal_Bdd result;
00483   TruthTable_t resulttable;
00484   Cal_Bdd expected;
00485 
00486   result = Cal_BddOr(bddManager, f1, f2);
00487   resulttable = table1 | table2;
00488   expected = EncodingToBdd(resulttable);
00489   if(!Cal_BddIsEqual(bddManager, result, expected)){
00490     Error("OR", bddManager,result, expected, f1, f2, (Cal_Bdd) 0);
00491   }
00492   Cal_BddFree(bddManager, result);
00493   Cal_BddFree(bddManager, expected);
00494 }
00506 static void
00507 TestITE(
00508   Cal_BddManager bddManager,
00509   Cal_Bdd  f1,
00510   TruthTable_t  table1,
00511   Cal_Bdd  f2,
00512   TruthTable_t  table2,
00513   Cal_Bdd  f3,
00514   TruthTable_t  table3)
00515 {
00516   Cal_Bdd result;
00517   TruthTable_t resultTable;
00518   Cal_Bdd expected;
00519 
00520   result = Cal_BddITE(bddManager, f1, f2, f3);
00521   resultTable = (table1 & table2) | (~table1 & table3);
00522   expected = EncodingToBdd(resultTable);
00523   if(Cal_BddIsEqual(bddManager, result, expected) == 0){
00524     Error("ITE", bddManager, result, expected, f1, f2, f3,
00525           (Cal_Bdd) 0);
00526   }
00527   Cal_BddFree(bddManager, result);
00528   Cal_BddFree(bddManager, expected);
00529 }
00541 static void
00542 TestXor(
00543   Cal_BddManager bddManager,
00544   Cal_Bdd  f1,
00545   TruthTable_t  table1,
00546   Cal_Bdd  f2,
00547   TruthTable_t  table2)
00548 {
00549   Cal_Bdd result;
00550   TruthTable_t resulttable;
00551   Cal_Bdd expected;
00552 
00553   result = Cal_BddXor(bddManager, f1, f2);
00554   resulttable = table1 ^ table2;
00555   expected = EncodingToBdd(resulttable);
00556   if(!Cal_BddIsEqual(bddManager, result, expected)){
00557     Error("XOR", bddManager, result, expected, (Cal_Bdd) 0);
00558   }
00559   Cal_BddFree(bddManager, result);
00560   Cal_BddFree(bddManager, expected);
00561 }
00562 
00563 
00575 static void
00576 TestIdNot(
00577   Cal_BddManager bddManager,
00578   Cal_Bdd  f,
00579   TruthTable_t  table)
00580 {
00581   Cal_Bdd result;
00582   TruthTable_t resulttable;
00583   Cal_Bdd expected;
00584 
00585   result = Cal_BddNot(bddManager, f);
00586   resulttable = ~table;
00587   expected = EncodingToBdd(resulttable);
00588   if(!Cal_BddIsEqual(bddManager, result, expected)){
00589     Error("Not", bddManager, result, expected, (Cal_Bdd) 0);
00590   }
00591   Cal_BddFree(bddManager, result);
00592   Cal_BddFree(bddManager, expected);
00593   result = Cal_BddIdentity(bddManager, f);
00594   resulttable = table;
00595   expected = EncodingToBdd(resulttable);
00596   if(!Cal_BddIsEqual(bddManager, result, expected)){
00597     Error("Identity", bddManager, result, expected, (Cal_Bdd) 0);
00598   }
00599   Cal_BddFree(bddManager, result);
00600   Cal_BddFree(bddManager, expected);
00601   
00602 }
00603 
00604 
00616 static void
00617 TestCompose(
00618   Cal_BddManager bddManager,
00619   Cal_Bdd  f1,
00620   TruthTable_t  table1,
00621   Cal_Bdd  f2,
00622   TruthTable_t  table2)
00623 {
00624   int var;
00625   Cal_Bdd result, expected;
00626   TruthTable_t resulttable;
00627   
00628 
00629   var = (int)(((long)CalUtilRandom())%TT_VARS);
00630 
00631   result = Cal_BddCompose(bddManager, vars[var], vars[var], Cal_BddOne(bddManager));
00632   if(!Cal_BddIsEqual(bddManager, result, Cal_BddOne(bddManager))){
00633     Cal_BddFunctionPrint(bddManager, result, "Compose"); 
00634   }
00635 
00636   result = Cal_BddCompose(bddManager, vars[var], vars[var], Cal_BddZero(bddManager));
00637   if(!Cal_BddIsEqual(bddManager, result, Cal_BddZero(bddManager))){
00638     Cal_BddFunctionPrint(bddManager, result, "Compose"); 
00639   }
00640 
00641   result = Cal_BddCompose(bddManager, f1, vars[var], Cal_BddOne(bddManager));
00642   resulttable = Cofactor(table1, var, 1);
00643   expected = EncodingToBdd(resulttable);
00644   if(!Cal_BddIsEqual(bddManager, result,expected)){
00645     Error("Restrict 1", bddManager, result, expected, f1, vars[var],
00646           (Cal_Bdd) 0);
00647   }
00648   Cal_BddFree(bddManager, result);
00649   Cal_BddFree(bddManager, expected);
00650 
00651   result = Cal_BddCompose(bddManager, f1, vars[var], Cal_BddZero(bddManager));
00652   resulttable = Cofactor(table1, var, 0);
00653   expected = EncodingToBdd(resulttable);
00654   if(!Cal_BddIsEqual(bddManager, result, expected)){
00655     Error("Restrict 0", bddManager, result, expected, f1, vars[var],
00656           (Cal_Bdd) 0);
00657   }
00658   Cal_BddFree(bddManager, result);
00659   Cal_BddFree(bddManager, expected);
00660 
00661   result = Cal_BddCompose(bddManager, f1, vars[var], f2);
00662   resulttable = (table2 & Cofactor(table1, var, 1)) |
00663       (~table2 & Cofactor(table1, var, 0));
00664   expected = EncodingToBdd(resulttable);
00665   if(!Cal_BddIsEqual(bddManager, result, expected)){
00666     Error("Compose", bddManager, result, expected, f1, vars[var],
00667           f2, (Cal_Bdd) 0);
00668   }
00669   Cal_BddFree(bddManager, result);
00670   Cal_BddFree(bddManager, expected);
00671 }
00672 
00684 static void
00685 TestSubstitute(
00686   Cal_BddManager bddManager,
00687   Cal_Bdd  f1,
00688   TruthTable_t  table1,
00689   Cal_Bdd  f2,
00690   TruthTable_t  table2,
00691   Cal_Bdd  f3,
00692   TruthTable_t  table3)
00693 {
00694   int var1, var2;
00695   Cal_Bdd associationInfo[6];
00696   Cal_Bdd result;
00697   TruthTable_t resulttable;
00698   TruthTable_t temp1, temp2, temp3, temp4;
00699   Cal_Bdd expected;
00700   int assocId;
00701   
00702   var1 = (int)(((long)CalUtilRandom())%TT_VARS);
00703   do{
00704     var2 = (int)(((long)CalUtilRandom())%TT_VARS);
00705   }while (var1 == var2);
00706 
00707   associationInfo[0] = vars[var1];
00708   associationInfo[1] = f2;
00709   associationInfo[2] = vars[var2];
00710   associationInfo[3] = f3;
00711   associationInfo[4] = (Cal_Bdd) 0;
00712   associationInfo[5] = (Cal_Bdd) 0;
00713 
00714   assocId = Cal_AssociationInit(bddManager, associationInfo, 1);
00715   Cal_AssociationSetCurrent(bddManager, assocId);
00716 
00717   result = Cal_BddSubstitute(bddManager, f1);
00718   temp1 = Cofactor(Cofactor(table1, var1, 1), var2, 1);
00719   temp2 = Cofactor(Cofactor(table1, var1, 1), var2, 0);
00720   temp3 = Cofactor(Cofactor(table1, var1, 0), var2, 1);
00721   temp4 = Cofactor(Cofactor(table1, var1, 0), var2, 0);
00722   resulttable = table2 & table3 & temp1;
00723   resulttable |= table2 & ~table3 & temp2;
00724   resulttable |= ~table2 & table3 & temp3;
00725   resulttable |= ~table2 & ~table3 & temp4;
00726   expected = EncodingToBdd(resulttable);
00727   if(!Cal_BddIsEqual(bddManager, result, expected)){
00728     Error("substitute", bddManager, result, expected,
00729         f1, vars[var1], f2, vars[var2], f3, (Cal_Bdd) 0);
00730   }
00731   /*Cal_AssociationQuit(bddManager, assocId);*/
00732   Cal_BddFree(bddManager, result);
00733   Cal_BddFree(bddManager, expected);
00734 }
00735 
00747 static void
00748 TestVarSubstitute(
00749   Cal_BddManager bddManager,
00750   Cal_Bdd  f1,
00751   TruthTable_t  table1,
00752   Cal_Bdd  f2,
00753   TruthTable_t  table2,
00754   Cal_Bdd  f3,
00755   TruthTable_t  table3)
00756 {
00757   int var1, var2, var3, var4;
00758   Cal_Bdd associationInfo[6];
00759   Cal_Bdd result1, result2;
00760   TruthTable_t resulttable;
00761   TruthTable_t temp1, temp2, temp3, temp4;
00762   Cal_Bdd expected;
00763   int assocId;
00764   
00765   var1 = (int)(((long)CalUtilRandom())%TT_VARS);
00766   do{
00767     var3 = (int)(((long)CalUtilRandom())%TT_VARS);
00768   }while (var1 == var3);
00769 
00770   var2 = (int)(((long)CalUtilRandom())%TT_VARS);
00771   do{
00772     var4 = (int)(((long)CalUtilRandom())%TT_VARS);
00773   }while (var2 == var4);
00774 
00775   /*
00776   f1 = vars[0];
00777   table1 = cofactorMasks[0];
00778   */
00779   associationInfo[0] = vars[var1];
00780   associationInfo[1] = vars[var3];
00781   associationInfo[2] = vars[var2];
00782   associationInfo[3] = vars[var4];
00783   associationInfo[4] = (Cal_Bdd) 0;
00784   associationInfo[5] = (Cal_Bdd) 0;
00785 
00786   assocId = Cal_AssociationInit(bddManager, associationInfo, 1);
00787   Cal_AssociationSetCurrent(bddManager, assocId);
00788 
00789   result1 = Cal_BddVarSubstitute(bddManager, f1);
00790   result2 = Cal_BddSubstitute(bddManager, f1);
00791   temp1 = Cofactor(Cofactor(table1, var2, 1), var1, 1);
00792   temp2 = Cofactor(Cofactor(table1, var2, 1), var1, 0);
00793   temp3 = Cofactor(Cofactor(table1, var2, 0), var1, 1);
00794   temp4 = Cofactor(Cofactor(table1, var2, 0), var1, 0);
00795   resulttable = cofactorMasks[var3] & cofactorMasks[var4] & temp1;
00796   resulttable |= ~cofactorMasks[var3] & cofactorMasks[var4] & temp2;
00797   resulttable |= cofactorMasks[var3] & ~cofactorMasks[var4] & temp3;
00798   resulttable |= ~cofactorMasks[var3] & ~cofactorMasks[var4] & temp4;
00799   expected = EncodingToBdd(resulttable);
00800   if(!Cal_BddIsEqual(bddManager, result1, result2)){
00801     Error("var substitute and substitute differ", bddManager, result1, result2,
00802         f1, vars[var1], vars[var3], vars[var2], vars[var4],
00803           (Cal_Bdd) 0); 
00804   }
00805   if(!Cal_BddIsEqual(bddManager, result1, expected)){
00806     Error("var substitute", bddManager, result1, expected,
00807         f1, vars[var1], vars[var3], vars[var2], vars[var4],
00808           (Cal_Bdd) 0); 
00809   }
00810   /*Cal_AssociationQuit(bddManager, assocId);*/
00811   Cal_BddFree(bddManager, result1);
00812   Cal_BddFree(bddManager, result2);
00813   Cal_BddFree(bddManager, expected);
00814 }
00815 
00827 static void
00828 TestSwapVars(
00829   Cal_BddManager bddManager,
00830   Cal_Bdd  f,
00831   TruthTable_t  table)
00832 {
00833   int var1, var2;
00834   Cal_Bdd result;
00835   TruthTable_t resulttable;
00836   TruthTable_t temp1, temp2, temp3, temp4;
00837   Cal_Bdd expected;
00838 
00839   var1 = (int)(((long)CalUtilRandom())%TT_VARS);
00840   var2 = (int)(((long)CalUtilRandom())%TT_VARS);
00841   result = Cal_BddSwapVars(bddManager, f, vars[var1], vars[var2]);
00842   temp1 = Cofactor(Cofactor(table, var1, 1), var2, 1);
00843   temp2 = Cofactor(Cofactor(table, var1, 1), var2, 0);
00844   temp3 = Cofactor(Cofactor(table, var1, 0), var2, 1);
00845   temp4 = Cofactor(Cofactor(table, var1, 0), var2, 0);
00846   resulttable = cofactorMasks[var2] & cofactorMasks[var1] & temp1;
00847   resulttable |= cofactorMasks[var2] & ~cofactorMasks[var1] & temp2;
00848   resulttable |= ~cofactorMasks[var2] & cofactorMasks[var1] & temp3;
00849   resulttable |= ~cofactorMasks[var2] & ~cofactorMasks[var1] & temp4;
00850   expected = EncodingToBdd(resulttable);
00851   if(!Cal_BddIsEqual(bddManager, result, expected)){
00852     Error("swap variables", bddManager, result, expected, 
00853         f, vars[var1], vars[var2], (Cal_Bdd) 0);
00854   }
00855   Cal_BddFree(bddManager, result);
00856   Cal_BddFree(bddManager, expected);
00857 }
00858 
00870 static void
00871 TestMultiwayAnd(
00872   Cal_BddManager bddManager,
00873   Cal_Bdd  f1,
00874   TruthTable_t  table1,
00875   Cal_Bdd  f2,
00876   TruthTable_t  table2,
00877   Cal_Bdd  f3,
00878   TruthTable_t  table3)
00879 {
00880         Cal_Bdd result;
00881         TruthTable_t resulttable;
00882         Cal_Bdd expected;
00883         Cal_Bdd *calBddArray;
00884 
00885     calBddArray = Cal_MemAlloc(Cal_Bdd, 4);
00886     calBddArray[0] = f1;
00887     calBddArray[1] = f2;
00888     calBddArray[2] = f3;
00889     calBddArray[3] = (Cal_Bdd) 0;
00890         result = Cal_BddMultiwayAnd(bddManager, calBddArray);
00891         resulttable = table1 & table2 & table3;
00892         expected = EncodingToBdd(resulttable);
00893     if(!Cal_BddIsEqual(bddManager, result, expected)){
00894       Error("Multiway And", bddManager, result, expected,
00895             (Cal_Bdd) 0);
00896     }
00897   Cal_BddFree(bddManager, result);
00898   Cal_BddFree(bddManager, expected);
00899   Cal_MemFree(calBddArray);
00900 }
00901 
00913 static void
00914 TestMultiwayOr(
00915   Cal_BddManager bddManager,
00916   Cal_Bdd  f1,
00917   TruthTable_t  table1,
00918   Cal_Bdd  f2,
00919   TruthTable_t  table2,
00920   Cal_Bdd  f3,
00921   TruthTable_t  table3)
00922 {
00923   Cal_Bdd result;
00924   TruthTable_t resulttable;
00925   Cal_Bdd expected;
00926   Cal_Bdd *calBddArray;
00927   
00928   calBddArray = Cal_MemAlloc(Cal_Bdd, 4);
00929   calBddArray[0] = f1;
00930   calBddArray[1] = f2;
00931   calBddArray[2] = f3;
00932   calBddArray[3] = (Cal_Bdd) 0;
00933   result = Cal_BddMultiwayOr(bddManager, calBddArray);
00934   resulttable = table1 | table2 | table3;
00935         expected = EncodingToBdd(resulttable);
00936   if(!Cal_BddIsEqual(bddManager, result, expected)){
00937     Error("Multiway Or", bddManager, result, expected, (Cal_Bdd) 0);
00938   }
00939   Cal_BddFree(bddManager, result);
00940   Cal_BddFree(bddManager, expected);
00941   Cal_MemFree(calBddArray);
00942 }
00943 
00955 static void
00956 TestMultiwayLarge(
00957   Cal_BddManager bddManager,
00958   int  numBdds)
00959 {
00960   TruthTable_t table, andResulttable, orResulttable;
00961   Cal_Bdd f, andResult, orResult, andExpected, orExpected;
00962   int i;
00963   Cal_Bdd *calBddArray;
00964   
00965   andResulttable = ~0x0;
00966   orResulttable = 0x0;
00967   calBddArray = Cal_MemAlloc(Cal_Bdd, numBdds+1);
00968   for (i=0; i<numBdds; i++){
00969     table = (TruthTable_t)CalUtilRandom();
00970     f = EncodingToBdd(table);
00971     calBddArray[i] = f;
00972     andResulttable &= table;
00973     orResulttable |= table;
00974   }
00975   calBddArray[numBdds] = (Cal_Bdd) 0;
00976   andResult = Cal_BddMultiwayAnd(bddManager, calBddArray);
00977   orResult = Cal_BddMultiwayOr(bddManager, calBddArray);
00978   andExpected = EncodingToBdd(andResulttable);
00979   orExpected = EncodingToBdd(orResulttable);
00980   if(!Cal_BddIsEqual(bddManager, andResult, andExpected)){
00981     Error("Multiway And", bddManager, andResult, andExpected,
00982           (Cal_Bdd) 0);
00983   }
00984   if(!Cal_BddIsEqual(bddManager, orResult, orExpected)){
00985     Error("Multiway Or", bddManager, andResult, andExpected,
00986           (Cal_Bdd) 0);
00987   }
00988   for (i=0; i<numBdds; i++) Cal_BddFree(bddManager, calBddArray[i]);
00989   Cal_MemFree(calBddArray);
00990   Cal_BddFree(bddManager, andResult);
00991   Cal_BddFree(bddManager, andExpected);
00992   Cal_BddFree(bddManager, orResult);
00993   Cal_BddFree(bddManager, orExpected);
00994 }
01006 static void
01007 TestArrayOp(Cal_BddManager bddManager,  int  numBdds)
01008 {
01009   TruthTable_t fTable, gTable;
01010   Cal_Bdd f, g, *andExpectedArray, *orExpectedArray, *calBddArray;
01011   Cal_Bdd *andResultArray, *orResultArray;
01012   int i;
01013   
01014   calBddArray = Cal_MemAlloc(Cal_Bdd, 2*numBdds+1);
01015   andExpectedArray = Cal_MemAlloc(Cal_Bdd, numBdds);
01016   orExpectedArray = Cal_MemAlloc(Cal_Bdd, numBdds);
01017   calBddArray[numBdds<<1] = (Cal_Bdd) 0;
01018 
01019   for (i=0; i<numBdds; i++){
01020     fTable = (TruthTable_t)CalUtilRandom();
01021     gTable = (TruthTable_t)CalUtilRandom();
01022     f = EncodingToBdd(fTable);
01023     g = EncodingToBdd(gTable);
01024     calBddArray[i<<1] = f;
01025     calBddArray[(i<<1)+1] = g;
01026     andExpectedArray[i] = EncodingToBdd(fTable & gTable);
01027     orExpectedArray[i] = EncodingToBdd(fTable | gTable);
01028   }
01029   
01030   andResultArray = Cal_BddPairwiseAnd(bddManager, calBddArray);
01031   orResultArray = Cal_BddPairwiseOr(bddManager, calBddArray);
01032 
01033   for (i=0; i<numBdds; i++){
01034     if(!Cal_BddIsEqual(bddManager, andResultArray[i], andExpectedArray[i])){
01035       Error("Array OR", bddManager, andResultArray[i], andExpectedArray[i],
01036             (Cal_Bdd) 0);
01037       break;
01038     }
01039   }
01040 
01041   for (i=0; i<numBdds; i++){
01042     if(!Cal_BddIsEqual(bddManager, orResultArray[i], orExpectedArray[i])){
01043       Error("Array OR", bddManager, orResultArray[i], orExpectedArray[i],
01044             (Cal_Bdd) 0);
01045       break;
01046     }
01047   }
01048   for (i=0; i<numBdds; i++){
01049     Cal_BddFree(bddManager, calBddArray[i<<1]);
01050     Cal_BddFree(bddManager, calBddArray[(i<<1)+1]);
01051     Cal_BddFree(bddManager, andExpectedArray[i]);
01052     Cal_BddFree(bddManager, orExpectedArray[i]);
01053     Cal_BddFree(bddManager, andResultArray[i]);
01054     Cal_BddFree(bddManager, orResultArray[i]);
01055   }
01056   Cal_MemFree(calBddArray);
01057   Cal_MemFree(andExpectedArray);
01058   Cal_MemFree(orExpectedArray);
01059   Cal_MemFree(andResultArray);
01060   Cal_MemFree(orResultArray);
01061 }
01073 static void
01074 TestInterImpl(
01075   Cal_BddManager bddManager,
01076   Cal_Bdd  f1,
01077   TruthTable_t  table1,
01078   Cal_Bdd  f2,
01079   TruthTable_t  table2)
01080 {
01081   Cal_Bdd result;
01082   TruthTable_t resulttable;
01083   Cal_Bdd expected;
01084   Cal_Bdd impliesResult;
01085 
01086   result = Cal_BddIntersects(bddManager, f1, f2);
01087   resulttable = table1 & table2;
01088   expected = EncodingToBdd(resulttable);
01089   impliesResult = Cal_BddImplies(bddManager, result, expected);
01090   if(Cal_BddIsBddZero(bddManager, impliesResult) == 0){
01091     Error("intersection test", bddManager, result, expected, f1, f2,
01092           (Cal_Bdd) 0); 
01093   }
01094   Cal_BddFree(bddManager, impliesResult);
01095   Cal_BddFree(bddManager, result);
01096   Cal_BddFree(bddManager, expected);
01097 }
01109 static void
01110 TestQnt(Cal_BddManager bddManager, Cal_Bdd  f, TruthTable_t  table, int
01111         bfZeroBFPlusDFOne, int cacheExistsResultsFlag, int cacheOrResultsFlag)
01112 {
01113   int var1, var2;
01114   Cal_Bdd assoc[3];
01115   Cal_Bdd result, expected;
01116   TruthTable_t  resultTable;
01117   int associationId;
01118   
01119   var1= (int)(((long)CalUtilRandom())%TT_VARS);
01120   do
01121     var2= (int)(((long)CalUtilRandom())%TT_VARS);
01122   while (var1 == var2);
01123   assoc[0] = vars[var1];
01124   assoc[1] = vars[var2];
01125   assoc[2] = (Cal_Bdd) 0;
01126   associationId = Cal_AssociationInit(bddManager, assoc, 0);
01127   Cal_AssociationSetCurrent(bddManager, associationId);
01128   result = Cal_BddExists(bddManager, f);
01129   resultTable = Cofactor(table, var1, 1) | Cofactor(table, var1, 0);
01130   resultTable = Cofactor(resultTable, var2, 1) | Cofactor(resultTable,
01131                                                           var2, 0); 
01132   expected = EncodingToBdd(resultTable);
01133   if(Cal_BddIsEqual(bddManager, result, expected) == 0){
01134     Error("quantification", bddManager, result, expected, f, vars[var1],
01135           vars[var2], (Cal_Bdd) 0);
01136   }
01137   /*Cal_AssociationQuit(bddManager, associationId);*/
01138   Cal_BddFree(bddManager, result);
01139   Cal_BddFree(bddManager, expected);
01140 }
01141 
01153 static void
01154 TestAssoc(Cal_BddManager bddManager, Cal_Bdd  f, TruthTable_t  table)
01155 {
01156   Cal_Bdd assoc[3];
01157   Cal_Bdd result, expected;
01158   int associationId;
01159   
01160   assoc[0] = (Cal_Bdd) 0;
01161   associationId = Cal_AssociationInit(bddManager, assoc, 0);
01162   Cal_AssociationSetCurrent(bddManager, associationId);
01163   result = Cal_BddExists(bddManager, f);
01164   expected = Cal_BddIdentity(bddManager, f);
01165   if(Cal_BddIsEqual(bddManager, result, expected) == 0){
01166     Error("quantification", bddManager, result, expected, (Cal_Bdd) 0);
01167   }
01168   Cal_BddFree(bddManager, result);
01169   Cal_BddFree(bddManager, expected);
01170 }
01171 
01183 static void
01184 TestRelProd(Cal_BddManager bddManager, Cal_Bdd  f1, TruthTable_t
01185             table1, Cal_Bdd  f2, TruthTable_t  table2, int bfZeroBFPlusDFOne,
01186             int cacheRelProdResultsFlag, int cacheAndResultsFlag, int
01187             cacheOrResultsFlag) 
01188 {
01189   int var1, var2;
01190   Cal_Bdd assoc[3];
01191   Cal_Bdd result;
01192   TruthTable_t resultTable;
01193   Cal_Bdd expected;
01194   int assocId;
01195   
01196   var1=(int)(((long)CalUtilRandom())%TT_VARS);
01197   do
01198     var2=(int)(((long)CalUtilRandom())%TT_VARS);
01199   while (var1 == var2);
01200   assoc[0] = vars[var1];
01201   assoc[1] = vars[var2];
01202   assoc[2] = (Cal_Bdd) 0;
01203   assocId = Cal_AssociationInit(bddManager, assoc, 0);
01204   Cal_AssociationSetCurrent(bddManager, assocId);
01205   result = Cal_BddRelProd(bddManager, f1, f2);
01206   table1 &= table2;
01207   resultTable = Cofactor(table1, var1, 1) | Cofactor(table1, var1, 0);
01208   resultTable = Cofactor(resultTable, var2, 1) | Cofactor(resultTable, var2, 0);
01209   expected = EncodingToBdd(resultTable);
01210   if(Cal_BddIsEqual(bddManager, result, expected) == 0){
01211     Error("relational product", bddManager, result, expected, f1, f2,
01212           vars[var1], vars[var2], (Cal_Bdd) 0);
01213   }
01214   /*Cal_AssociationQuit(bddManager, assocId);*/
01215   Cal_BddFree(bddManager, result);
01216   Cal_BddFree(bddManager, expected);
01217 }
01218 
01230 static void
01231 TestReduce(
01232   Cal_BddManager bddManager,
01233   Cal_Bdd  f1,
01234   TruthTable_t  table1,
01235   Cal_Bdd  f2,
01236   TruthTable_t  table2)
01237 {
01238   Cal_Bdd result;
01239   Cal_Bdd temp1, temp2, temp3;
01240 
01241   result = Cal_BddReduce(bddManager, f1, f2);
01242   temp1 = Cal_BddXnor(bddManager, result, f1);
01243   temp2 = Cal_BddNot(bddManager, f2);
01244   temp3 = Cal_BddOr(bddManager, temp1, temp2);
01245   if(Cal_BddIsBddOne(bddManager, temp3) == 0){
01246     Error("d.c. comparison of reduce", bddManager, temp3,
01247           Cal_BddOne(bddManager), f1, f2, (Cal_Bdd) 0);
01248   }
01249   Cal_BddFree(bddManager, result);
01250   Cal_BddFree(bddManager, temp1);
01251   Cal_BddFree(bddManager, temp2);
01252   Cal_BddFree(bddManager, temp3);
01253 }
01254 
01266 static void
01267 TestGenCof(
01268   Cal_BddManager bddManager,
01269   Cal_Bdd  f1,
01270   TruthTable_t  table1,
01271   Cal_Bdd  f2,
01272   TruthTable_t  table2)
01273 {
01274   int var1, var2;
01275   Cal_Bdd result, temp1, temp2, temp3, expected;
01276   TruthTable_t resultTable;
01277 
01278   result = Cal_BddCofactor(bddManager, f1, f2);
01279   temp1 = Cal_BddXnor(bddManager, result, f1);
01280   temp2 = Cal_BddNot(bddManager, f2);
01281   temp3 = Cal_BddOr(bddManager, temp1, temp2);
01282   if (Cal_BddIsBddOne(bddManager, temp3) == 0){
01283     Error("d.c. comparison of generalized cofactor", bddManager,
01284           temp3, Cal_BddOne(bddManager), f1, f2, (Cal_Bdd) 0);
01285   }
01286 
01287   Cal_BddFree(bddManager, result);
01288   Cal_BddFree(bddManager, temp1);
01289   Cal_BddFree(bddManager, temp2);
01290   Cal_BddFree(bddManager, temp3);
01291   var1=(int)(((long)CalUtilRandom())%TT_VARS);
01292   do
01293     var2=(int)(((long)CalUtilRandom())%TT_VARS);
01294   while (var1 == var2);
01295   temp1 = Cal_BddNot(bddManager, vars[var2]);
01296   temp2 = Cal_BddAnd(bddManager, vars[var1], temp1);
01297   Cal_BddFree(bddManager, temp1);
01298   result = Cal_BddCofactor(bddManager, f1, temp2);
01299   resultTable = Cofactor(Cofactor(table1, var1, 1), var2, 0);
01300   expected = EncodingToBdd(resultTable);
01301   if (Cal_BddIsEqual(bddManager, result, expected) == 0){
01302     Error("generalized cofactor", bddManager, result, expected, f1,
01303           temp2, (Cal_Bdd) 0);
01304   }
01305   Cal_BddFree(bddManager, result);
01306   Cal_BddFree(bddManager, expected);
01307   Cal_BddFree(bddManager, temp2);
01308 }
01320 static void
01321 TestSize(
01322   Cal_BddManager bddManager,
01323   Cal_Bdd  f1,
01324   TruthTable_t  table1,
01325   Cal_Bdd  f2,
01326   TruthTable_t  table2)
01327 {
01328   int i;
01329   long size;
01330   long profile[MAX_TT_VARS+1];
01331   Cal_Bdd fs[3];
01332 
01333   size = Cal_BddSize(bddManager, f1, 1);
01334   Cal_BddProfile(bddManager, f1, profile, 1);
01335   for(i = 0; i < TT_VARS+1; i++){
01336     size -= profile[i];
01337   }
01338   if(size){
01339     fprintf(stderr, "\nError: size count vs. profile sum:\n");
01340     fprintf(stderr, "Argument:\n");
01341     Cal_BddFunctionPrint(bddManager, f1, "f1");
01342   }
01343 
01344   size = Cal_BddSize(bddManager, f1, 0);
01345   Cal_BddProfile(bddManager, f1, profile, 0);
01346   for(i = 0; i < TT_VARS+1; i++){
01347     size -= profile[i];
01348   }
01349   if(size){
01350     fprintf(stderr, "\nError: no negout size count vs. profile sum:\n");
01351     fprintf(stderr, "Argument:\n");
01352     Cal_BddFunctionPrint(bddManager, f1, "f1");
01353   }
01354 
01355 
01356   fs[0] = f1;
01357   fs[1] = f2;
01358   fs[2] = (Cal_Bdd) 0;
01359 
01360   size = Cal_BddSizeMultiple(bddManager, fs, 1);
01361   Cal_BddProfileMultiple(bddManager, fs, profile, 1);
01362   for(i = 0; i < TT_VARS+1; i++){
01363     size -= profile[i];
01364   }
01365   if(size){
01366     fprintf(stderr,"\nError: multiple size count vs. multiple profile sum:\n");
01367     fprintf(stderr, "Argument 1:\n");
01368     Cal_BddFunctionPrint(bddManager, f1, "f1");
01369     fprintf(stderr, "Argument 2:\n");
01370     Cal_BddFunctionPrint(bddManager, f2, "f2");
01371   }
01372 
01373   size = Cal_BddSizeMultiple(bddManager, fs, 0);
01374   Cal_BddProfileMultiple(bddManager, fs, profile, 0);
01375   for(i = 0; i < TT_VARS+1; i++){
01376     size -= profile[i];
01377   }
01378   if(size){
01379     fprintf(stderr,"\nError: multiple no negout size count vs. multiple profile sum:\n");
01380     fprintf(stderr, "Argument 1:\n");
01381     Cal_BddFunctionPrint(bddManager, f1, "f1");
01382     fprintf(stderr, "Argument 2:\n");
01383     Cal_BddFunctionPrint(bddManager, f2, "f2");
01384   }
01385 }
01386 
01398 static void
01399 TestSatisfy(
01400   Cal_BddManager bddManager,
01401   Cal_Bdd  f,
01402   TruthTable_t  table)
01403 {
01404   int var1, var2;
01405   Cal_Bdd assoc[MAX_TT_VARS+1];
01406   Cal_Bdd result;
01407   Cal_Bdd temp1, temp2, temp3;
01408   int assocId;
01409   
01410   if(Cal_BddIsBddZero(bddManager, f)){
01411     return;
01412   }
01413   result = Cal_BddSatisfy(bddManager, f);
01414   temp1 = Cal_BddNot(bddManager, f);
01415   temp2 = Cal_BddIntersects(bddManager, temp1, result);
01416   if(!Cal_BddIsBddZero(bddManager, temp2)){
01417     Error("intersection of satisfy result with negated argument",
01418         bddManager, temp2, Cal_BddZero(bddManager), f, (Cal_Bdd) 0);
01419   }
01420   Cal_BddFree(bddManager, temp1);
01421   Cal_BddFree(bddManager, temp2);
01422 
01423   var1 = (int)(((long)CalUtilRandom())%TT_VARS);
01424   do{
01425     var2 = (int)(((long)CalUtilRandom())%TT_VARS);
01426   }while (var1 == var2);
01427   assoc[0] = vars[var1];
01428   assoc[1] = vars[var2];
01429   assoc[2] = (Cal_Bdd) 0;
01430   assocId = Cal_AssociationInit(bddManager, assoc, 0);
01431   Cal_AssociationSetCurrent(bddManager, assocId);
01432   temp1 = Cal_BddSatisfySupport(bddManager, result);
01433   temp2 = Cal_BddNot(bddManager, result);
01434   temp3 = Cal_BddIntersects(bddManager, temp2, temp1);
01435   if(!Cal_BddIsBddZero(bddManager, temp3)){
01436     Error("intersection of satisfy support result with negated argument",
01437         bddManager, temp3, Cal_BddZero(bddManager), result,
01438         (Cal_Bdd) 0);
01439   }
01440   Cal_BddFree(bddManager, result);
01441   Cal_BddFree(bddManager, temp1);
01442   Cal_BddFree(bddManager, temp2);
01443   Cal_BddFree(bddManager, temp3);
01444   temp1 = Cal_BddCompose(bddManager, f, vars[var1], Cal_BddZero(bddManager));
01445   temp2 = Cal_BddCompose(bddManager, f, vars[var1], Cal_BddOne(bddManager));
01446   if(Cal_BddSatisfyingFraction(bddManager, temp1) + 
01447       Cal_BddSatisfyingFraction(bddManager, temp2) !=
01448       2.0 * Cal_BddSatisfyingFraction(bddManager, f)){
01449     fprintf(stderr, "\nError: operation satisfying fraction:\n");
01450     fprintf(stderr, "Argument:\n");
01451     Cal_BddFunctionPrint(bddManager, f, "f");
01452     fprintf(stderr, "Cofactor on:\n");
01453     Cal_BddFunctionPrint(bddManager, vars[var1], "var");
01454   }
01455   /*Cal_AssociationQuit(bddManager, assocId);*/
01456   Cal_BddFree(bddManager, temp1);
01457   Cal_BddFree(bddManager, temp2);
01458 }
01459 
01471 static void
01472 TestPipeline(Cal_BddManager bddManager,
01473              Cal_Bdd  f1,
01474              TruthTable_t  table1,
01475              Cal_Bdd  f2,
01476              TruthTable_t  table2,
01477              Cal_Bdd  f3,
01478              TruthTable_t  table3)
01479 {
01480   Cal_Bdd temp1, temp2, temp3, temp4, temp5, result, expected;
01481   TruthTable_t table;
01482 
01483   Cal_PipelineInit(bddManager, CAL_AND);
01484   Cal_PipelineSetDepth(bddManager, 0);
01485   temp1 = Cal_PipelineCreateProvisionalBdd(bddManager, f1, f2);
01486   temp2 = Cal_PipelineCreateProvisionalBdd(bddManager, f1, f3);
01487   temp3 = Cal_PipelineCreateProvisionalBdd(bddManager, f1, temp1);
01488   temp4 = Cal_PipelineCreateProvisionalBdd(bddManager, f2, temp2);
01489   temp5 = Cal_PipelineCreateProvisionalBdd(bddManager, temp3, temp4);
01490   result = Cal_PipelineCreateProvisionalBdd(bddManager, temp4, temp5);
01491   Cal_PipelineExecute(bddManager);
01492   result = Cal_PipelineUpdateProvisionalBdd(bddManager, result);
01493   Cal_PipelineQuit(bddManager);
01494 
01495   table = table1 & table2 & table3;
01496   expected = EncodingToBdd(table);
01497 
01498   if (Cal_BddIsEqual(bddManager, result, expected) == 0){
01499     Error("pipeline", bddManager, result, expected, (Cal_Bdd) 0);
01500   }
01501   Cal_BddFree(bddManager, result);
01502   Cal_BddFree(bddManager, expected);
01503 }
01504 
01516 static void
01517 TestDump(Cal_BddManager bddManager, Cal_Bdd f)
01518 {
01519   FILE *fp;
01520   int i, j;
01521   Cal_Bdd dumpVars[MAX_TT_VARS];
01522   Cal_Bdd temp, result;
01523   int err;
01524 
01525   if (!(fp=tmpfile()))
01526     {
01527       fprintf(stderr, "could not open temporary file\n");
01528       exit(1);
01529     }
01530   for (i=0; i < TT_VARS; ++i)
01531     dumpVars[i]=vars[i];
01532   dumpVars[i]= (Cal_Bdd) 0;
01533   for (i=0; i < TT_VARS-1; ++i)
01534     {
01535       j=i+(int)(((long)CalUtilRandom())%(TT_VARS-i));
01536       temp=dumpVars[i];
01537       dumpVars[i]=dumpVars[j];
01538       dumpVars[j]=temp;
01539     }
01540   if (!Cal_BddDumpBdd(bddManager, f, dumpVars, fp))
01541     {
01542       fprintf(stderr, "Error: dump failure:\n");
01543       fprintf(stderr, "Argument:\n");
01544       PrintBdd(bddManager, f);
01545       fclose(fp);
01546       return;
01547     }
01548   rewind(fp);
01549   if (!(result=Cal_BddUndumpBdd(bddManager, dumpVars, fp, &err)) || err)
01550     {
01551       fprintf(stderr, "Error: undump failure: code %d:\n", err);
01552       fprintf(stderr, "Argument:\n");
01553       PrintBdd(bddManager, f);
01554       fclose(fp);
01555       return;
01556     }
01557   fclose(fp);
01558   if (result != f)
01559     Error("dump/undump", bddManager, result, f, f, (Cal_Bdd) 0);
01560   Cal_BddFree(bddManager, result);
01561 }
01562 
01563 
01575 static void
01576 TestReorderBlock(Cal_BddManager bddManager, TruthTable_t table, Cal_Bdd f)
01577 {
01578   Cal_Bdd newFunction;
01579   Cal_Block block1, block2, block3;
01580   
01581   /*if (CalUtilRandom()&0x1){*/
01582   if (1){
01583     fprintf(stdout, "Using Window\n");
01584     Cal_BddDynamicReordering(bddManager, CAL_REORDER_WINDOW);
01585   }
01586   else{
01587     fprintf(stdout, "Using Sift\n");
01588     Cal_BddDynamicReordering(bddManager, CAL_REORDER_SIFT);
01589   }
01590   /* Create some blocks */
01591   block1 = Cal_BddNewVarBlock(bddManager,
01592                               vars[bddManager->indexToId[0]-1],
01593                               4); 
01594   block2 = Cal_BddNewVarBlock(bddManager,
01595                               vars[bddManager->indexToId[4]-1],
01596                               4);
01597   block3 = Cal_BddNewVarBlock(bddManager,
01598                               vars[bddManager->indexToId[8]-1],
01599                               4);
01600   Cal_BddVarBlockReorderable(bddManager, block2, 1);
01601   Cal_BddReorder(bddManager);
01602   newFunction = EncodingToBdd(table);
01603   if (Cal_BddIsEqual(bddManager, f, newFunction) == 0){
01604     Error("Reordering (window)", bddManager, newFunction, f, (Cal_Bdd) 0);
01605   }
01606   Cal_BddFree(bddManager, newFunction);
01607 }
01608 
01620 static void
01621 TestReorder(Cal_BddManager bddManager, TruthTable_t table, Cal_Bdd f)
01622 {
01623   Cal_Bdd newFunction;
01624   
01625   if (CalUtilRandom()&0x1){
01626     fprintf(stdout, "Using Window\n");
01627     Cal_BddDynamicReordering(bddManager, CAL_REORDER_WINDOW);
01628   }
01629   else{
01630     fprintf(stdout, "Using Sift\n");
01631     Cal_BddDynamicReordering(bddManager, CAL_REORDER_SIFT);
01632   }
01633   if (CalUtilRandom()&0x1){
01634     bddManager->reorderMethod = CAL_REORDER_METHOD_BF;
01635   }
01636   else{
01637     bddManager->reorderMethod = CAL_REORDER_METHOD_DF;
01638   }
01639   Cal_BddReorder(bddManager);
01640   newFunction = EncodingToBdd(table);
01641   if (Cal_BddIsEqual(bddManager, f, newFunction) == 0){
01642     Error("Reordering (window)", bddManager, newFunction, f, (Cal_Bdd) 0);
01643   }
01644   Cal_BddFree(bddManager, newFunction);
01645 }
01646 
01658 static void
01659 handler(int ignored)
01660 {
01661   printf("arthimetic exception ############\n");
01662 }
01663 
01664 
01665 
01666 
01678 static void
01679 RandomTests(int numVars, int  iterations)
01680 {
01681   int i, seed;
01682   TruthTable_t table1, table2, table3;
01683   Cal_Bdd f1, f2, f3/*, f4*/;
01684   CalAssociation_t *assoc, *nextAssoc;
01685   /* Cal_Block block1, block2; */
01686   
01687   signal(SIGFPE, handler);
01688   
01689   printf("Random operation tests...\n");
01690   bddManager  = Cal_BddManagerInit();
01691   seed = 1;
01692   /*
01693   (void) time((time_t *)&seed);
01694   */
01695   CalUtilSRandom((long)seed);
01696 
01697   for(i = 0; i < numVars; ++i){
01698     vars[i] = Cal_BddManagerCreateNewVarLast(bddManager);
01699   }
01700   
01701   /*
01702   f1 = Cal_BddAnd(bddManager, vars[1], vars[2]);
01703   f2 = Cal_BddAnd(bddManager, vars[1], vars[0]);
01704   f3 = Cal_BddOr(bddManager, f1, f2);
01705   Cal_BddFree(bddManager, f1);
01706   Cal_BddFree(bddManager, f2);
01707   Cal_BddDynamicReordering(bddManager, Cal_BddReorderSift);
01708   fprintf(stdout,"Original function:\n");
01709   Cal_BddFunctionPrint(bddManager, f3, "a");
01710   Cal_BddReorderNew(bddManager);
01711   f1 = Cal_BddAnd(bddManager, vars[1], vars[2]);
01712   f2 = Cal_BddAnd(bddManager, vars[1], vars[0]);
01713   f4 = Cal_BddOr(bddManager, f1, f2);
01714   Cal_BddFree(bddManager, f1);
01715   Cal_BddFree(bddManager, f2);
01716   fprintf(stdout,"New function:\n");
01717   Cal_BddFunctionPrint(bddManager, f4, "a");
01718   Cal_Assert(Cal_BddIsEqual(bddManager, f3, f4));
01719   Cal_BddFree(bddManager, f3);
01720   Cal_BddFree(bddManager, f4);
01721   */
01722 
01723 /*
01724   block1 = Cal_BddNewVarBlock(bddManager,
01725                               vars[0], 2);
01726   block2 = Cal_BddNewVarBlock(bddManager, vars[3], 2);
01727   Cal_BddVarBlockReorderable(bddManager, block2, 1);
01728   */
01729   for (i = 0; i < iterations; i++){
01730     printf("Iteration %3d\n", i);
01731     table1 = (TruthTable_t)CalUtilRandom();
01732     table2 = (TruthTable_t)CalUtilRandom();
01733     table3 = (TruthTable_t)CalUtilRandom();
01734     f1 = EncodingToBdd(table1);
01735     f2 = EncodingToBdd(table2);
01736     f3 = EncodingToBdd(table3);
01737 
01738     /* The following tests will fail if you do not use 5 variables */
01739     if (numVars == 5){
01740       TestGenCof(bddManager, f1, table1, f2, table2);
01741       TestSubstitute(bddManager, f1, table1, f2, table2, f3, table3);
01742       TestSwapVars(bddManager, f1, table1);
01743       TestCompose(bddManager, f1, table1, f2, table2);
01744       TestRelProd(bddManager, f1, table1, f2, table2, 0, 0, 0, 0);
01745       TestQnt(bddManager, f1, table1, 1, 1, 1);
01746       TestVarSubstitute(bddManager, f1, table1, f2, table2, f3,
01747                         table3);
01748     }
01749     /* The following can be tested for larger number of variables */
01750     TestAnd(bddManager,f1, table1, f2, table2);
01751     TestIdNot(bddManager, f1, table1);
01752     TestITE(bddManager, f1, table1, f2, table2, f3, table3);
01753     TestNand(bddManager,f1, table1, f2, table2);
01754     TestOr(bddManager, f1, table1, f2, table2);
01755     TestXor(bddManager,f1, table1, f2, table2);
01756     TestMultiwayOr(bddManager, f1, table1, f2, table2, f3, table3);
01757     TestMultiwayAnd(bddManager, f1, table1, f2, table2, f3, table3);
01758     TestArrayOp(bddManager, 10);
01759     TestInterImpl(bddManager, f1, table1, f2, table2);
01760     TestReduce(bddManager, f1, table1, f2, table2);
01761     TestSize(bddManager, f1, table1, f2, table2);
01762     TestSatisfy(bddManager, f1, table1);
01763     TestAssoc(bddManager, f1, table1);
01764     TestDump(bddManager, f1); 
01765     TestPipeline(bddManager, f1, table1, f2, table2, f3, table3);
01766     TestReorder(bddManager, table1, f1);
01767     Cal_BddFree(bddManager, f1);
01768     Cal_BddFree(bddManager, f2);
01769     Cal_BddFree(bddManager, f3);
01770         if (i && (i % 10 == 0)) {
01771       Cal_BddManagerGC(bddManager);
01772       (void)CalPackNodes(bddManager);
01773     }
01774   }
01775   for(i = 0; i < numVars; ++i){
01776     Cal_BddFree(bddManager, vars[i]);
01777   }
01778   Cal_BddStats(bddManager, stdout);
01779   for(assoc = bddManager->associationList;
01780       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
01781     nextAssoc = assoc->next;
01782     for (i=1; i <= bddManager->numVars; i++){
01783       if (CalBddIsBddNull(bddManager, assoc->varAssociation[i]) == 0){
01784         CalBddDcrRefCount(assoc->varAssociation[i]);
01785         assoc->varAssociation[i] = bddManager->bddNull;
01786         assoc->lastBddIndex = -1;
01787       }
01788     }
01789   }
01790   /* fix temporary association */
01791   assoc = bddManager->tempAssociation;
01792   for (i=1; i <= bddManager->numVars; i++){
01793     if (CalBddIsBddNull(bddManager, assoc->varAssociation[i]) == 0){
01794       CalBddDcrRefCount(assoc->varAssociation[i]);
01795       assoc->varAssociation[i] = bddManager->bddNull;
01796       assoc->lastBddIndex = -1;
01797     }
01798   }
01799 
01800   Cal_BddManagerGC(bddManager);
01801   Cal_BddStats(bddManager, stdout);
01802   /*CalUniqueTablePrint(bddManager);*/
01803   Cal_BddManagerQuit(bddManager);
01804 }