#include "misc/util/util_hack.h"
#include "cuddInt.h"

Functions
static int	getMaxBinomial (int n)

static DdHalfWord **	getMatrix (int rows, int cols)

static void	freeMatrix (DdHalfWord **matrix)

static int	getLevelKeys (DdManager *table, int l)

static int	ddShuffle (DdManager table, DdHalfWord permutation, int lower, int upper)

static int	ddSiftUp (DdManager *table, int x, int xLow)

static int	updateUB (DdManager table, int oldBound, DdHalfWord bestOrder, int lower, int upper)

static int	ddCountRoots (DdManager *table, int lower, int upper)

static void	ddClearGlobal (DdManager *table, int lower, int maxlevel)

static int	computeLB (DdManager table, DdHalfWord order, int roots, int cost, int lower, int upper, int level)

static int	updateEntry (DdManager table, DdHalfWord order, int level, int cost, DdHalfWord *orders, int costs, int subsets, char *mask, int lower, int upper)

static void	pushDown (DdHalfWord *order, int j, int level)

static DdHalfWord *	initSymmInfo (DdManager *table, int lower, int upper)

static int	checkSymmInfo (DdManager table, DdHalfWord symmInfo, int index, int level)

int	cuddExact (DdManager *table, int lower, int upper)

Variables
static ABC_NAMESPACE_IMPL_START char rcsid[]	DD_UNUSED = "$Id: cuddExact.c,v 1.28 2009/02/19 16:19:19 fabio Exp $"

Function Documentation

static int checkSymmInfo	(	DdManager *	table,
		DdHalfWord *	symmInfo,
		int	index,
		int	level
	)

static

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

Synopsis [Check symmetry condition.]

Description [Returns 1 if a variable is the one with the highest index among those belonging to a symmetry group that are in the top part of the BDD. The top part is given by level.]

SideEffects [None]

SeeAlso [initSymmInfo]

Definition at line 1008 of file cuddExact.c.

 {
     int i;
 
     i = symmInfo[index];
     while (i != index) {
         if (index < i && table->perm[i] <= level)
             return(0);
         i = symmInfo[i];
     }
     return(1);
 
 } /* end of checkSymmInfo */

static int computeLB	(	DdManager *	table,
		DdHalfWord *	order,
		int	roots,
		int	cost,
		int	lower,
		int	upper,
		int	level
	)

static

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

Synopsis [Computes a lower bound on the size of a BDD.]

Description [Computes a lower bound on the size of a BDD from the following factors:

size of the lower part of it;
size of the part of the upper part not subjected to reordering;
number of roots in the part of the BDD subjected to reordering;
variable in the support of the roots in the upper part of the BDD subjected to reordering.
SideEffects [None]

SeeAlso []

Definition at line 813 of file cuddExact.c.

 {
     int i;
     int lb = cost;
     int lb1 = 0;
     int lb2;
     int support;
     DdHalfWord ref;
 
     /* The levels not involved in reordering are not going to change.
     ** Add their sizes to the lower bound.
     */
     for (i = 0; i < lower; i++) {
         lb += getLevelKeys(table,i);
     }
     /* If a variable is in the support, then there is going
     ** to be at least one node labeled by that variable.
     */
     for (i = lower; i <= lower+level; i++) {
         support = table->subtables[i].keys > 1 ||
             table->vars[order[i-lower]]->ref > 1;
         lb1 += support;
     }
 
     /* Estimate the number of nodes required to connect the roots to
     ** the nodes in the bottom part. */
     if (lower+level+1 < table->size) {
         if (lower+level < upper)
             ref = table->vars[order[level+1]]->ref;
         else
             ref = table->vars[table->invperm[upper+1]]->ref;
         lb2 = table->subtables[lower+level+1].keys -
             (ref > (DdHalfWord) 1) - roots;
     } else {
         lb2 = 0;
     }
 
     lb += lb1 > lb2 ? lb1 : lb2;
 
     return(lb);
 
 } /* end of computeLB */

int cuddExact	(	DdManager *	table,
		int	lower,
		int	upper
	)

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

Synopsis [Exact variable ordering algorithm.]

Description [Exact variable ordering algorithm. Finds an optimum order for the variables between lower and upper. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 153 of file cuddExact.c.

 {
     int k, i, j;
     int maxBinomial, oldSubsets, newSubsets;
     int subsetCost;
     int size;                   /* number of variables to be reordered */
     int unused, nvars, level, result;
     int upperBound, lowerBound, cost;
     int roots;
     char *mask = NULL;
     DdHalfWord  *symmInfo = NULL;
     DdHalfWord **newOrder = NULL;
     DdHalfWord **oldOrder = NULL;
     int *newCost = NULL;
     int *oldCost = NULL;
     DdHalfWord **tmpOrder;
     int *tmpCost;
     DdHalfWord *bestOrder = NULL;
     DdHalfWord *order;
 #ifdef DD_STATS
     int  ddTotalSubsets;
 #endif
 
     /* Restrict the range to be reordered by excluding unused variables
     ** at the two ends. */
     while (table->subtables[lower].keys == 1 &&
            table->vars[table->invperm[lower]]->ref == 1 &&
            lower < upper)
         lower++;
     while (table->subtables[upper].keys == 1 &&
            table->vars[table->invperm[upper]]->ref == 1 &&
            lower < upper)
         upper--;
     if (lower == upper) return(1); /* trivial problem */
 
     /* Apply symmetric sifting to get a good upper bound and to extract
     ** symmetry information. */
     result = cuddSymmSiftingConv(table,lower,upper);
     if (result == 0) goto cuddExactOutOfMem;
 
 #ifdef DD_STATS
     (void) fprintf(table->out,"\n");
     ddTotalShuffles = 0;
     ddTotalSubsets = 0;
 #endif
 
     /* Initialization. */
     nvars = table->size;
     size = upper - lower + 1;
     /* Count unused variable among those to be reordered.  This is only
     ** used to compute maxBinomial. */
     unused = 0;
     for (i = lower + 1; i < upper; i++) {
         if (table->subtables[i].keys == 1 &&
             table->vars[table->invperm[i]]->ref == 1)
             unused++;
     }
 
     /* Find the maximum number of subsets we may have to store. */
     maxBinomial = getMaxBinomial(size - unused);
     if (maxBinomial == -1) goto cuddExactOutOfMem;
 
     newOrder = getMatrix(maxBinomial, size);
     if (newOrder == NULL) goto cuddExactOutOfMem;
 
     newCost = ABC_ALLOC(int, maxBinomial);
     if (newCost == NULL) goto cuddExactOutOfMem;
 
     oldOrder = getMatrix(maxBinomial, size);
     if (oldOrder == NULL) goto cuddExactOutOfMem;
 
     oldCost = ABC_ALLOC(int, maxBinomial);
     if (oldCost == NULL) goto cuddExactOutOfMem;
 
     bestOrder = ABC_ALLOC(DdHalfWord, size);
     if (bestOrder == NULL) goto cuddExactOutOfMem;
 
     mask = ABC_ALLOC(char, nvars);
     if (mask == NULL) goto cuddExactOutOfMem;
 
     symmInfo = initSymmInfo(table, lower, upper);
     if (symmInfo == NULL) goto cuddExactOutOfMem;
 
     roots = ddCountRoots(table, lower, upper);
 
     /* Initialize the old order matrix for the empty subset and the best
     ** order to the current order. The cost for the empty subset includes
     ** the cost of the levels between upper and the constants. These levels
     ** are not going to change. Hence, we count them only once.
     */
     oldSubsets = 1;
     for (i = 0; i < size; i++) {
         oldOrder[0][i] = bestOrder[i] = (DdHalfWord) table->invperm[i+lower];
     }
     subsetCost = table->constants.keys;
     for (i = upper + 1; i < nvars; i++)
         subsetCost += getLevelKeys(table,i);
     oldCost[0] = subsetCost;
     /* The upper bound is initialized to the current size of the BDDs. */
     upperBound = table->keys - table->isolated;
 
     /* Now consider subsets of increasing size. */
     for (k = 1; k <= size; k++) {
 #ifdef DD_STATS
         (void) fprintf(table->out,"Processing subsets of size %d\n", k);
         fflush(table->out);
 #endif
         newSubsets = 0;
         level = size - k;               /* offset of first bottom variable */
 
         for (i = 0; i < oldSubsets; i++) { /* for each subset of size k-1 */
             order = oldOrder[i];
             cost = oldCost[i];
             lowerBound = computeLB(table, order, roots, cost, lower, upper,
                                    level);
             if (lowerBound >= upperBound)
                 continue;
             /* Impose new order. */
             result = ddShuffle(table, order, lower, upper);
             if (result == 0) goto cuddExactOutOfMem;
             upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
             /* For each top bottom variable. */
             for (j = level; j >= 0; j--) {
                 /* Skip unused variables. */
                 if (table->subtables[j+lower-1].keys == 1 &&
                     table->vars[table->invperm[j+lower-1]]->ref == 1) continue;
                 /* Find cost under this order. */
                 subsetCost = cost + getLevelKeys(table, lower + level);
                 newSubsets = updateEntry(table, order, level, subsetCost,
                                          newOrder, newCost, newSubsets, mask,
                                          lower, upper);
                 if (j == 0)
                     break;
                 if (checkSymmInfo(table, symmInfo, order[j-1], level) == 0)
                     continue;
                 pushDown(order,j-1,level);
                 /* Impose new order. */
                 result = ddShuffle(table, order, lower, upper);
                 if (result == 0) goto cuddExactOutOfMem;
                 upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
             } /* for each bottom variable */
         } /* for each subset of size k */
 
         /* New orders become old orders in preparation for next iteration. */
         tmpOrder = oldOrder; tmpCost = oldCost;
         oldOrder = newOrder; oldCost = newCost;
         newOrder = tmpOrder; newCost = tmpCost;
 #ifdef DD_STATS
         ddTotalSubsets += newSubsets;
 #endif
         oldSubsets = newSubsets;
     }
     result = ddShuffle(table, bestOrder, lower, upper);
     if (result == 0) goto cuddExactOutOfMem;
 #ifdef DD_STATS
 #ifdef DD_VERBOSE
     (void) fprintf(table->out,"\n");
 #endif
     (void) fprintf(table->out,"#:S_EXACT   %8d: total subsets\n",
                    ddTotalSubsets);
     (void) fprintf(table->out,"#:H_EXACT   %8d: total shuffles",
                    ddTotalShuffles);
 #endif
 
     freeMatrix(newOrder);
     freeMatrix(oldOrder);
     ABC_FREE(bestOrder);
     ABC_FREE(oldCost);
     ABC_FREE(newCost);
     ABC_FREE(symmInfo);
     ABC_FREE(mask);
     return(1);
 
 cuddExactOutOfMem:
 
     if (newOrder != NULL) freeMatrix(newOrder);
     if (oldOrder != NULL) freeMatrix(oldOrder);
     if (bestOrder != NULL) ABC_FREE(bestOrder);
     if (oldCost != NULL) ABC_FREE(oldCost);
     if (newCost != NULL) ABC_FREE(newCost);
     if (symmInfo != NULL) ABC_FREE(symmInfo);
     if (mask != NULL) ABC_FREE(mask);
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
 
 } /* end of cuddExact */

static void ddClearGlobal	(	DdManager *	table,
		int	lower,
		int	maxlevel
	)

static

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

Synopsis [Scans the DD and clears the LSB of the next pointers.]

Description [Scans the DD and clears the LSB of the next pointers. The LSB of the next pointers are used as markers to tell whether a node was reached. Once the roots are counted, these flags are reset.]

SideEffects [None]

SeeAlso [ddCountRoots]

Definition at line 767 of file cuddExact.c.

 {
     int i,j;
     DdNode *f;
     DdNodePtr *nodelist;
     DdNode *sentinel = &(table->sentinel);
     int slots;
 
     for (i = lower; i <= maxlevel; i++) {
         nodelist = table->subtables[i].nodelist;
         slots = table->subtables[i].slots;
         for (j = 0; j < slots; j++) {
             f = nodelist[j];
             while (f != sentinel) {
                 f->next = Cudd_Regular(f->next);
                 f = f->next;
             }
         }
     }
 
 } /* end of ddClearGlobal */

static int ddCountRoots	(	DdManager *	table,
		int	lower,
		int	upper
	)

static

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

Synopsis [Counts the number of roots.]

Description [Counts the number of roots at the levels between lower and upper. The computation is based on breadth-first search. A node is a root if it is not reachable from any previously visited node. (All the nodes at level lower are therefore considered roots.) The visited flag uses the LSB of the next pointer. Returns the root count. The roots that are constant nodes are always ignored.]

SideEffects [None]

SeeAlso [ddClearGlobal]

Definition at line 700 of file cuddExact.c.

 {
     int i,j;
     DdNode *f;
     DdNodePtr *nodelist;
     DdNode *sentinel = &(table->sentinel);
     int slots;
     int roots = 0;
     int maxlevel = lower;
 
     for (i = lower; i <= upper; i++) {
         nodelist = table->subtables[i].nodelist;
         slots = table->subtables[i].slots;
         for (j = 0; j < slots; j++) {
             f = nodelist[j];
             while (f != sentinel) {
                 /* A node is a root of the DAG if it cannot be
                 ** reached by nodes above it. If a node was never
                 ** reached during the previous depth-first searches,
                 ** then it is a root, and we start a new depth-first
                 ** search from it.
                 */
                 if (!Cudd_IsComplement(f->next)) {
                     if (f != table->vars[f->index]) {
                         roots++;
                     }
                 }
                 if (!Cudd_IsConstant(cuddT(f))) {
                     cuddT(f)->next = Cudd_Complement(cuddT(f)->next);
                     if (table->perm[cuddT(f)->index] > maxlevel)
                         maxlevel = table->perm[cuddT(f)->index];
                 }
                 if (!Cudd_IsConstant(cuddE(f))) {
                     Cudd_Regular(cuddE(f))->next =
                         Cudd_Complement(Cudd_Regular(cuddE(f))->next);
                     if (table->perm[Cudd_Regular(cuddE(f))->index] > maxlevel)
                         maxlevel = table->perm[Cudd_Regular(cuddE(f))->index];
                 }
                 f = Cudd_Regular(f->next);
             }
         }
     }
     ddClearGlobal(table, lower, maxlevel);
 
     return(roots);
 
 } /* end of ddCountRoots */

static int ddShuffle	(	DdManager *	table,
		DdHalfWord *	permutation,
		int	lower,
		int	upper
	)

static

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

Synopsis [Reorders variables according to a given permutation.]

Description [Reorders variables according to a given permutation. The i-th permutation array contains the index of the variable that should be brought to the i-th level. ddShuffle assumes that no dead nodes are present and that the interaction matrix is properly initialized. The reordering is achieved by a series of upward sifts. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 541 of file cuddExact.c.

 {
     DdHalfWord  index;
     int         level;
     int         position;
 #if 0
     int         numvars;
 #endif
     int         result;
 #ifdef DD_STATS
     long        localTime;
     int         initialSize;
 #ifdef DD_VERBOSE
     int         finalSize;
 #endif
     int         previousSize;
 #endif
 
 #ifdef DD_STATS
     localTime = util_cpu_time();
     initialSize = table->keys - table->isolated;
 #endif
 
 #if 0
     numvars = table->size;
 
     (void) fprintf(table->out,"%d:", ddTotalShuffles);
     for (level = 0; level < numvars; level++) {
         (void) fprintf(table->out," %d", table->invperm[level]);
     }
     (void) fprintf(table->out,"\n");
 #endif
 
     for (level = 0; level <= upper - lower; level++) {
         index = permutation[level];
         position = table->perm[index];
 #ifdef DD_STATS
         previousSize = table->keys - table->isolated;
 #endif
         result = ddSiftUp(table,position,level+lower);
         if (!result) return(0);
     }
 
 #ifdef DD_STATS
     ddTotalShuffles++;
 #ifdef DD_VERBOSE
     finalSize = table->keys - table->isolated;
     if (finalSize < initialSize) {
         (void) fprintf(table->out,"-");
     } else if (finalSize > initialSize) {
         (void) fprintf(table->out,"+");
     } else {
         (void) fprintf(table->out,"=");
     }
     if ((ddTotalShuffles & 63) == 0) (void) fprintf(table->out,"\n");
     fflush(table->out);
 #endif
 #endif
 
     return(1);
 
 } /* end of ddShuffle */

static int ddSiftUp	(	DdManager *	table,
		int	x,
		int	xLow
	)

static

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

Synopsis [Moves one variable up.]

Description [Takes a variable from position x and sifts it up to position xLow; xLow should be less than or equal to x. Returns 1 if successful; 0 otherwise]

SideEffects [None]

SeeAlso []

Definition at line 623 of file cuddExact.c.

 {
     int        y;
     int        size;
 
     y = cuddNextLow(table,x);
     while (y >= xLow) {
         size = cuddSwapInPlace(table,y,x);
         if (size == 0) {
             return(0);
         }
         x = y;
         y = cuddNextLow(table,x);
     }
     return(1);
 
 } /* end of ddSiftUp */

static void freeMatrix ( DdHalfWord ** matrix )

static

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

Synopsis [Frees a two-dimensional matrix allocated by getMatrix.]

Description []

SideEffects [None]

SeeAlso [getMatrix]

Definition at line 486 of file cuddExact.c.

 {
     ABC_FREE(matrix[0]);
     ABC_FREE(matrix);
     return;
 
 } /* end of freeMatrix */

static int getLevelKeys	(	DdManager *	table,
		int	l
	)

static

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

Synopsis [Returns the number of nodes at one level of a unique table.]

Description [Returns the number of nodes at one level of a unique table. The projection function, if isolated, is not counted.]

SideEffects [None]

SeeAlso []

Definition at line 509 of file cuddExact.c.

 {
     int isolated;
     int x;        /* x is an index */
 
     x = table->invperm[l];
     isolated = table->vars[x]->ref == 1;
 
     return(table->subtables[l].keys - isolated);
 
 } /* end of getLevelKeys */

static DdHalfWord ** getMatrix	(	int	rows,
		int	cols
	)

static

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

Synopsis [Allocates a two-dimensional matrix of ints.]

Description [Allocates a two-dimensional matrix of ints. Returns the pointer to the matrix if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [freeMatrix]

Definition at line 451 of file cuddExact.c.

 {
     DdHalfWord **matrix;
     int i;
 
     if (cols*rows == 0) return(NULL);
     matrix = ABC_ALLOC(DdHalfWord *, rows);
     if (matrix == NULL) return(NULL);
     matrix[0] = ABC_ALLOC(DdHalfWord, cols*rows);
     if (matrix[0] == NULL) {
         ABC_FREE(matrix);
         return(NULL);
     }
     for (i = 1; i < rows; i++) {
         matrix[i] = matrix[i-1] + cols;
     }
     return(matrix);
 
 } /* end of getMatrix */

static int getMaxBinomial ( int n )

static

AutomaticStart

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

Synopsis [Returns the maximum value of (n choose k) for a given n.]

Description [Computes the maximum value of (n choose k) for a given n. The maximum value occurs for k = n/2 when n is even, or k = (n-1)/2 when n is odd. The algorithm used in this procedure avoids intermediate overflow problems. It is based on the identity

  binomial(n,k) = n/k * binomial(n-1,k-1).

Returns the computed value if successful; -1 if out of range.]

SideEffects [None]

SeeAlso []

Definition at line 363 of file cuddExact.c.

 {
     double i, j, result;
 
     if (n < 0 || n > 33) return(-1); /* error */
     if (n < 2) return(1);
 
     for (result = (double)((n+3)/2), i = result+1, j=2; i <= n; i++, j++) {
         result *= i;
         result /= j;
     }
 
     return((int)result);
 
 } /* end of getMaxBinomial */

static DdHalfWord * initSymmInfo	(	DdManager *	table,
		int	lower,
		int	upper
	)

static

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

Synopsis [Gathers symmetry information.]

Description [Translates the symmetry information stored in the next field of each subtable from level to indices. This procedure is called immediately after symmetric sifting, so that the next fields are correct. By translating this informaton in terms of indices, we make it independent of subsequent reorderings. The format used is that of the next fields: a circular list where each variable points to the next variable in the same symmetry group. Only the entries between lower and upper are considered. The procedure returns a pointer to an array holding the symmetry information if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [checkSymmInfo]

Definition at line 972 of file cuddExact.c.

 {
     int level, index, next, nextindex;
     DdHalfWord *symmInfo;
 
     symmInfo =  ABC_ALLOC(DdHalfWord, table->size);
     if (symmInfo == NULL) return(NULL);
 
     for (level = lower; level <= upper; level++) {
         index = table->invperm[level];
         next =  table->subtables[level].next;
         nextindex = table->invperm[next];
         symmInfo[index] = nextindex;
     }
     return(symmInfo);
 
 } /* end of initSymmInfo */

static void pushDown	(	DdHalfWord *	order,
		int	j,
		int	level
	)

static

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

Synopsis [Pushes a variable in the order down to position "level."]

Description []

SideEffects [None]

SeeAlso []

Definition at line 934 of file cuddExact.c.

 {
     int i;
     DdHalfWord tmp;
 
     tmp = order[j];
     for (i = j; i < level; i++) {
         order[i] = order[i+1];
     }
     order[level] = tmp;
     return;
 
 } /* end of pushDown */

static int updateEntry	(	DdManager *	table,
		DdHalfWord *	order,
		int	level,
		int	cost,
		DdHalfWord **	orders,
		int *	costs,
		int	subsets,
		char *	mask,
		int	lower,
		int	upper
	)

static

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

Synopsis [Updates entry for a subset.]

Description [Updates entry for a subset. Finds the subset, if it exists. If the new order for the subset has lower cost, or if the subset did not exist, it stores the new order and cost. Returns the number of subsets currently in the table.]

SideEffects [None]

SeeAlso []

Definition at line 880 of file cuddExact.c.

 {
     int i, j;
     int size = upper - lower + 1;
 
     /* Build a mask that says what variables are in this subset. */
     for (i = lower; i <= upper; i++)
         mask[table->invperm[i]] = 0;
     for (i = level; i < size; i++)
         mask[order[i]] = 1;
 
     /* Check each subset until a match is found or all subsets are examined. */
     for (i = 0; i < subsets; i++) {
         DdHalfWord *subset = orders[i];
         for (j = level; j < size; j++) {
             if (mask[subset[j]] == 0)
                 break;
         }
         if (j == size)          /* no mismatches: success */
             break;
     }
     if (i == subsets || cost < costs[i]) {              /* add or replace */
         for (j = 0; j < size; j++)
             orders[i][j] = order[j];
         costs[i] = cost;
         subsets += (i == subsets);
     }
     return(subsets);
 
 } /* end of updateEntry */

static int updateUB	(	DdManager *	table,
		int	oldBound,
		DdHalfWord *	bestOrder,
		int	lower,
		int	upper
	)

static

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

Synopsis [Updates the upper bound and saves the best order seen so far.]

Description [Updates the upper bound and saves the best order seen so far. Returns the current value of the upper bound.]

SideEffects [None]

SeeAlso []

Definition at line 658 of file cuddExact.c.

 {
     int i;
     int newBound = table->keys - table->isolated;
 
     if (newBound < oldBound) {
 #ifdef DD_STATS
         (void) fprintf(table->out,"New upper bound = %d\n", newBound);
         fflush(table->out);
 #endif
         for (i = lower; i <= upper; i++)
             bestOrder[i-lower] = (DdHalfWord) table->invperm[i];
         return(newBound);
     } else {
         return(oldBound);
     }
 
 } /* end of updateUB */

Variable Documentation

ABC_NAMESPACE_IMPL_START char rcsid [] DD_UNUSED = "$Id: cuddExact.c,v 1.28 2009/02/19 16:19:19 fabio Exp $"

static

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

FileName [cuddExact.c]

PackageName [cudd]

Synopsis [Functions for exact variable reordering.]

Description [External procedures included in this file:

Internal procedures included in this module:

cuddExact()

Static procedures included in this module:

]

Author [Cheng Hua, Fabio Somenzi]

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 95 of file cuddExact.c.

Functions

Variables

Function Documentation

Variable Documentation