Functions for cache insertion and lookup. More...

#include "util.h"
#include "cuddInt.h"

Include dependency graph for cuddCache.c:

Functions
int	cuddInitCache (DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize)
	Initializes the computed table. More...

void	cuddCacheInsert (DdManager table, ptruint op, DdNode f, DdNode g, DdNode h, DdNode *data)
	Inserts a result in the cache for a function with three operands. More...

void	cuddCacheInsert2 (DdManager table, DD_CTFP op, DdNode f, DdNode g, DdNode data)
	Inserts a result in the cache for a function with two operands. More...

void	cuddCacheInsert1 (DdManager table, DD_CTFP1 op, DdNode f, DdNode *data)
	Inserts a result in the cache for a function with two operands. More...

DdNode *	cuddCacheLookup (DdManager table, ptruint op, DdNode f, DdNode g, DdNode h)
	Looks up in the cache for the result of op applied to f, g, and h. More...

DdNode *	cuddCacheLookupZdd (DdManager table, ptruint op, DdNode f, DdNode g, DdNode h)
	Looks up in the cache for the result of op applied to f, g, and h. More...

DdNode *	cuddCacheLookup2 (DdManager table, DD_CTFP op, DdNode f, DdNode *g)
	Looks up in the cache for the result of op applied to f and g. More...

DdNode *	cuddCacheLookup1 (DdManager table, DD_CTFP1 op, DdNode f)
	Looks up in the cache for the result of op applied to f. More...

DdNode *	cuddCacheLookup2Zdd (DdManager table, DD_CTFP op, DdNode f, DdNode *g)
	Looks up in the cache for the result of op applied to f and g. More...

DdNode *	cuddCacheLookup1Zdd (DdManager table, DD_CTFP1 op, DdNode f)
	Looks up in the cache for the result of op applied to f. More...

DdNode *	cuddConstantLookup (DdManager table, ptruint op, DdNode f, DdNode g, DdNode h)
	Looks up in the cache for the result of op applied to f, g, and h. More...

int	cuddCacheProfile (DdManager table, FILE fp)
	Computes and prints a profile of the cache usage. More...

void	cuddCacheResize (DdManager *table)
	Resizes the cache. More...

void	cuddCacheFlush (DdManager *table)
	Flushes the cache. More...

int	cuddComputeFloorLog2 (unsigned int value)
	Returns the floor of the logarithm to the base 2. More...

Detailed Description

Functions for cache insertion and lookup.

Author: Fabio Somenzi

Copyright

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.

Function Documentation

◆ cuddCacheFlush()

void cuddCacheFlush ( DdManager * table )

Flushes the cache.

Side effects None

◆ cuddCacheInsert()

void cuddCacheInsert	(	DdManager *	table,
		ptruint	op,
		DdNode *	f,
		DdNode *	g,
		DdNode *	h,
		DdNode *	data
	)

Inserts a result in the cache for a function with three operands.

The operator tag (see cuddInt.h for details) is split and stored into unused bits of the first two pointers.

Side effects None

See also: cuddCacheInsert2 cuddCacheInsert1

◆ cuddCacheInsert1()

void cuddCacheInsert1	(	DdManager *	table,
		DD_CTFP1	op,
		DdNode *	f,
		DdNode *	data
	)

Inserts a result in the cache for a function with two operands.

Side effects None

See also: cuddCacheInsert cuddCacheInsert2

◆ cuddCacheInsert2()

void cuddCacheInsert2	(	DdManager *	table,
		DD_CTFP	op,
		DdNode *	f,
		DdNode *	g,
		DdNode *	data
	)

Inserts a result in the cache for a function with two operands.

Side effects None

See also: cuddCacheInsert cuddCacheInsert1

◆ cuddCacheLookup()

DdNode* cuddCacheLookup	(	DdManager *	table,
		ptruint	op,
		DdNode *	f,
		DdNode *	g,
		DdNode *	h
	)

Looks up in the cache for the result of op applied to f, g, and h.

Returns: the result if found; it returns NULL if no result is found.

Side effects None

See also: cuddCacheLookup2 cuddCacheLookup1

◆ cuddCacheLookup1()

DdNode* cuddCacheLookup1	(	DdManager *	table,
		DD_CTFP1	op,
		DdNode *	f
	)

Looks up in the cache for the result of op applied to f.

Returns: the result if found; it returns NULL if no result is found.

Side effects None

See also: cuddCacheLookup cuddCacheLookup2

◆ cuddCacheLookup1Zdd()

DdNode* cuddCacheLookup1Zdd	(	DdManager *	table,
		DD_CTFP1	op,
		DdNode *	f
	)

Looks up in the cache for the result of op applied to f.

Returns: the result if found; it returns NULL if no result is found.

Side effects None

See also: cuddCacheLookupZdd cuddCacheLookup2Zdd

◆ cuddCacheLookup2()

DdNode* cuddCacheLookup2	(	DdManager *	table,
		DD_CTFP	op,
		DdNode *	f,
		DdNode *	g
	)

Looks up in the cache for the result of op applied to f and g.

Returns: the result if found; it returns NULL if no result is found.

Side effects None

See also: cuddCacheLookup cuddCacheLookup1

◆ cuddCacheLookup2Zdd()

DdNode* cuddCacheLookup2Zdd	(	DdManager *	table,
		DD_CTFP	op,
		DdNode *	f,
		DdNode *	g
	)

Looks up in the cache for the result of op applied to f and g.

Returns: the result if found; it returns NULL if no result is found.

Side effects None

See also: cuddCacheLookupZdd cuddCacheLookup1Zdd

◆ cuddCacheLookupZdd()

DdNode* cuddCacheLookupZdd	(	DdManager *	table,
		ptruint	op,
		DdNode *	f,
		DdNode *	g,
		DdNode *	h
	)

Looks up in the cache for the result of op applied to f, g, and h.

Returns: the result if found; it returns NULL if no result is found.

Side effects None

See also: cuddCacheLookup2Zdd cuddCacheLookup1Zdd

◆ cuddCacheProfile()

int cuddCacheProfile	(	DdManager *	table,
		FILE *	fp
	)

Computes and prints a profile of the cache usage.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ cuddCacheResize()

void cuddCacheResize ( DdManager * table )

Resizes the cache.

Side effects None

◆ cuddComputeFloorLog2()

int cuddComputeFloorLog2 ( unsigned int value )

Returns the floor of the logarithm to the base 2.

The input value is assumed to be greater than 0.

Side effects None

◆ cuddConstantLookup()

DdNode* cuddConstantLookup	(	DdManager *	table,
		ptruint	op,
		DdNode *	f,
		DdNode *	g,
		DdNode *	h
	)

Looks up in the cache for the result of op applied to f, g, and h.

Assumes that the calling procedure (e.g., Cudd_bddIteConstant) is only interested in whether the result is constant or not.

Returns: the result if found (possibly DD_NON_CONSTANT); otherwise it returns NULL.

Side effects None

See also: cuddCacheLookup

◆ cuddInitCache()

int cuddInitCache	(	DdManager *	unique,
		unsigned int	cacheSize,
		unsigned int	maxCacheSize
	)

Initializes the computed table.

It is called by Cudd_Init.

Returns: 1 in case of success; 0 otherwise.

Side effects None

See also: Cudd_Init

Parameters

unique	unique table
cacheSize	initial size of the cache
maxCacheSize	cache size beyond which no resizing occurs