src/calBdd/calTest.c File Reference

#include "calInt.h"
#include "time.h"
#include <signal.h>

Include dependency graph for calTest.c:

Defines
#define	VARS 50
#define	TT_BITS 32
#define	MAX_TT_VARS 20
#define	ITERATIONS 50
#define	BITS_PER_INT 32
#define	LG_BITS_PER_INT 5
#define	EncodingToBdd(table) (Decode(0, (table)))
Typedefs
typedef unsigned long	TruthTable_t
Functions
static void	Error ()
static double	asDouble (CalAddress_t v1, CalAddress_t v2)
static void	asAddress (double n, CalAddress_t r1, CalAddress_t r2)
static char *	terminalIdFn (Cal_BddManager bddManager, CalAddress_t v1, CalAddress_t v2, Cal_Pointer_t pointer)
static void	PrintBdd (Cal_BddManager bddManager, Cal_Bdd f)
static void	Error (char *op, Cal_BddManager bddManager, Cal_Bdd result, Cal_Bdd expected,...)
static TruthTable_t	Cofactor (TruthTable_t table, int var, int value)
static Cal_Bdd	Decode (int var, TruthTable_t table)
static void	TestAnd (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2)
static void	TestNand (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2)
static void	TestOr (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2)
static void	TestITE (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3)
static void	TestXor (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2)
static void	TestIdNot (Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table)
static void	TestCompose (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2)
static void	TestSubstitute (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3)
static void	TestVarSubstitute (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3)
static void	TestSwapVars (Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table)
static void	TestMultiwayAnd (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3)
static void	TestMultiwayOr (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3)
static void	TestMultiwayLarge (Cal_BddManager bddManager, int numBdds)
static void	TestArrayOp (Cal_BddManager bddManager, int numBdds)
static void	TestInterImpl (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2)
static void	TestQnt (Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table, int bfZeroBFPlusDFOne, int cacheExistsResultsFlag, int cacheOrResultsFlag)
static void	TestAssoc (Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table)
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)
static void	TestReduce (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2)
static void	TestGenCof (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2)
static void	TestSize (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2)
static void	TestSatisfy (Cal_BddManager bddManager, Cal_Bdd f, TruthTable_t table)
static void	TestPipeline (Cal_BddManager bddManager, Cal_Bdd f1, TruthTable_t table1, Cal_Bdd f2, TruthTable_t table2, Cal_Bdd f3, TruthTable_t table3)
static void	TestDump (Cal_BddManager bddManager, Cal_Bdd f)
static void	TestReorderBlock (Cal_BddManager bddManager, TruthTable_t table, Cal_Bdd f)
static void	TestReorder (Cal_BddManager bddManager, TruthTable_t table, Cal_Bdd f)
static void	handler (int ignored)
static void	RandomTests (int numVars, int iterations)
static void	Error (va_alist)
Variables
static Cal_BddManager	bddManager
static Cal_Bdd	vars [VARS]
static TruthTable_t	cofactorMasks []
static int	TT_VARS
static CalAddress_t	asDoubleSpace [2]

Define Documentation

#define BITS_PER_INT 32

Definition at line 53 of file calTest.c.

#define EncodingToBdd ( table ) (Decode(0, (table)))

Definition at line 87 of file calTest.c.

#define ITERATIONS 50

Definition at line 52 of file calTest.c.

#define LG_BITS_PER_INT 5

Definition at line 54 of file calTest.c.

#define MAX_TT_VARS 20

Definition at line 51 of file calTest.c.

#define TT_BITS 32

Definition at line 50 of file calTest.c.

#define VARS 50

CFile***********************************************************************

FileName [calTest.c]

PackageName [cal]

Synopsis [This file contains the test routines for the CAL package.]

Description [optional]

SeeAlso [optional]

Author [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Modified and extended from the original version written by David Long. ]

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id: calTest.c,v 1.6 2002/08/28 19:26:39 fabio Exp

]

Definition at line 49 of file calTest.c.

Typedef Documentation

typedef unsigned long TruthTable_t

Definition at line 59 of file calTest.c.

Function Documentation

static void asAddress	(	double	n,
		CalAddress_t *	r1,
		CalAddress_t *	r2
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 219 of file calTest.c.

00223 {
00224   (*(double *)asDoubleSpace)=n;
00225   *r1 = asDoubleSpace[0];
00226   *r2 = asDoubleSpace[1];
00227 }

static double asDouble	(	CalAddress_t	v1,
		CalAddress_t	v2
	)			`[static]`

AutomaticStart

AutomaticEnd Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 198 of file calTest.c.

00201 {
00202   asDoubleSpace[0] = v1;
00203   asDoubleSpace[1] = v2;
00204   return (*(double *)asDoubleSpace);
00205 }

static TruthTable_t Cofactor	(	TruthTable_t	table,
		int	var,
		int	value
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 342 of file calTest.c.

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 }

static Cal_Bdd Decode	(	int	var,
		TruthTable_t	table
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 371 of file calTest.c.

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 }

static void Error ( va_alist ) [static]

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 295 of file calTest.c.

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 }

static void Error	(	char *	op,
		Cal_BddManager	bddManager,
		Cal_Bdd	result,
		Cal_Bdd	expected,
			...
	)			`[static]`

static void Error ( ) [static]

static void handler ( int ignored ) [static]

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1659 of file calTest.c.

01660 {
01661   printf("arthimetic exception ############\n");
01662 }

static void PrintBdd	(	Cal_BddManager	bddManager,
		Cal_Bdd	f
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 264 of file calTest.c.

00267 {
00268   Cal_BddPrintBdd(bddManager, f, Cal_BddNamingFnNone, 
00269                   (Cal_TerminalIdFn_t) terminalIdFn,
00270                   (Cal_Pointer_t)0, stderr); 
00271 }

static void RandomTests	(	int	numVars,
		int	iterations
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1679 of file calTest.c.

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 }

static char * terminalIdFn	(	Cal_BddManager	bddManager,
		CalAddress_t	v1,
		CalAddress_t	v2,
		Cal_Pointer_t	pointer
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 241 of file calTest.c.

00246 {
00247   static char result[100];
00248   sprintf(result, "%g", asDouble(v1, v2));
00249   return (result);
00250 }

static void TestAnd	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 417 of file calTest.c.

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 }

static void TestArrayOp	(	Cal_BddManager	bddManager,
		int	numBdds
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1007 of file calTest.c.

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 }

static void TestAssoc	(	Cal_BddManager	bddManager,
		Cal_Bdd	f,
		TruthTable_t	table
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1154 of file calTest.c.

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 }

static void TestCompose	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 617 of file calTest.c.

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 }

static void TestDump	(	Cal_BddManager	bddManager,
		Cal_Bdd	f
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1517 of file calTest.c.

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 }

static void TestGenCof	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1267 of file calTest.c.

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 }

static void TestIdNot	(	Cal_BddManager	bddManager,
		Cal_Bdd	f,
		TruthTable_t	table
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 576 of file calTest.c.

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 }

static void TestInterImpl	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1074 of file calTest.c.

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 }

static void TestITE	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2,
		Cal_Bdd	f3,
		TruthTable_t	table3
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 507 of file calTest.c.

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 }

static void TestMultiwayAnd	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2,
		Cal_Bdd	f3,
		TruthTable_t	table3
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 871 of file calTest.c.

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 }

static void TestMultiwayLarge	(	Cal_BddManager	bddManager,
		int	numBdds
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 956 of file calTest.c.

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 }

static void TestMultiwayOr	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2,
		Cal_Bdd	f3,
		TruthTable_t	table3
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 914 of file calTest.c.

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 }

static void TestNand	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 447 of file calTest.c.

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 }

static void TestOr	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 475 of file calTest.c.

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 }

static void TestPipeline	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2,
		Cal_Bdd	f3,
		TruthTable_t	table3
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1472 of file calTest.c.

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 }

static void TestQnt	(	Cal_BddManager	bddManager,
		Cal_Bdd	f,
		TruthTable_t	table,
		int	bfZeroBFPlusDFOne,
		int	cacheExistsResultsFlag,
		int	cacheOrResultsFlag
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1110 of file calTest.c.

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 }

static void TestReduce	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1231 of file calTest.c.

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 }

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
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1184 of file calTest.c.

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 }

static void TestReorder	(	Cal_BddManager	bddManager,
		TruthTable_t	table,
		Cal_Bdd	f
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1621 of file calTest.c.

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 }

static void TestReorderBlock	(	Cal_BddManager	bddManager,
		TruthTable_t	table,
		Cal_Bdd	f
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1576 of file calTest.c.

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 }

static void TestSatisfy	(	Cal_BddManager	bddManager,
		Cal_Bdd	f,
		TruthTable_t	table
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1399 of file calTest.c.

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 }

static void TestSize	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1321 of file calTest.c.

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 }

static void TestSubstitute	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2,
		Cal_Bdd	f3,
		TruthTable_t	table3
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 685 of file calTest.c.

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 }

static void TestSwapVars	(	Cal_BddManager	bddManager,
		Cal_Bdd	f,
		TruthTable_t	table
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 828 of file calTest.c.

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 }

static void TestVarSubstitute	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2,
		Cal_Bdd	f3,
		TruthTable_t	table3
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 748 of file calTest.c.

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 }

static void TestXor	(	Cal_BddManager	bddManager,
		Cal_Bdd	f1,
		TruthTable_t	table1,
		Cal_Bdd	f2,
		TruthTable_t	table2
	)			`[static]`

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 542 of file calTest.c.

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 }

Variable Documentation

CalAddress_t asDoubleSpace[2] [static]

Definition at line 81 of file calTest.c.

Cal_BddManager bddManager [static]

Definition at line 70 of file calTest.c.

TruthTable_t cofactorMasks[] [static]

Initial value:

{
  0xffff0000,
  0xff00ff00,
  0xf0f0f0f0,
  0xcccccccc,
  0xaaaaaaaa,
}

Definition at line 72 of file calTest.c.

int TT_VARS [static]

Definition at line 80 of file calTest.c.

Cal_Bdd vars[VARS] [static]

Definition at line 71 of file calTest.c.

src/calBdd/calTest.c File Reference

Defines

Typedefs

Functions

Variables

Define Documentation

Typedef Documentation

Function Documentation

Variable Documentation