Arbitrary precision arithmetic functions. More...

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

Include dependency graph for cuddApa.c:

Macros
#define	DD_APA_BITS ((int) sizeof(DdApaDigit) * 8)

#define	DD_APA_BASE ((DdApaDoubleDigit) 1 << DD_APA_BITS)

#define	DD_APA_MASK (DD_APA_BASE - 1)

#define	DD_LSDIGIT(x) ((x) & DD_APA_MASK)
	Extract the least significant digit of a double digit. More...

#define	DD_MSDIGIT(x) ((x) >> DD_APA_BITS)
	Extract the most significant digit of a double digit. More...

Typedefs
typedef uint64_t	DdApaDoubleDigit
	Type used for intermediate results.

Functions
int	Cudd_ApaNumberOfDigits (int binaryDigits)
	Returns the number of digits for an arbitrary precision integer. More...

DdApaNumber	Cudd_NewApaNumber (int digits)
	Allocates memory for an arbitrary precision integer. More...

void	Cudd_FreeApaNumber (DdApaNumber number)
	Frees an arbitrary precision integer. More...

void	Cudd_ApaCopy (int digits, DdConstApaNumber source, DdApaNumber dest)
	Makes a copy of an arbitrary precision integer. More...

DdApaDigit	Cudd_ApaAdd (int digits, DdConstApaNumber a, DdConstApaNumber b, DdApaNumber sum)
	Adds two arbitrary precision integers. More...

DdApaDigit	Cudd_ApaSubtract (int digits, DdConstApaNumber a, DdConstApaNumber b, DdApaNumber diff)
	Subtracts two arbitrary precision integers. More...

DdApaDigit	Cudd_ApaShortDivision (int digits, DdConstApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient)
	Divides an arbitrary precision integer by a digit. More...

unsigned int	Cudd_ApaIntDivision (int digits, DdConstApaNumber dividend, unsigned int divisor, DdApaNumber quotient)
	Divides an arbitrary precision integer by an integer. More...

void	Cudd_ApaShiftRight (int digits, DdApaDigit in, DdConstApaNumber a, DdApaNumber b)
	Shifts right an arbitrary precision integer by one binary place. More...

void	Cudd_ApaSetToLiteral (int digits, DdApaNumber number, DdApaDigit literal)
	Sets an arbitrary precision integer to a one-digit literal. More...

void	Cudd_ApaPowerOfTwo (int digits, DdApaNumber number, int power)
	Sets an arbitrary precision integer to a power of two. More...

int	Cudd_ApaCompare (int digitsFirst, DdConstApaNumber first, int digitsSecond, DdConstApaNumber second)
	Compares two arbitrary precision integers. More...

int	Cudd_ApaCompareRatios (int digitsFirst, DdConstApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdConstApaNumber secondNum, unsigned int secondDen)
	Compares the ratios of two arbitrary precision integers to two unsigned ints. More...

int	Cudd_ApaPrintHex (FILE *fp, int digits, DdConstApaNumber number)
	Prints an arbitrary precision integer in hexadecimal format. More...

int	Cudd_ApaPrintDecimal (FILE *fp, int digits, DdConstApaNumber number)
	Prints an arbitrary precision integer in decimal format. More...

char *	Cudd_ApaStringDecimal (int digits, DdConstApaNumber number)
	converts an arbitrary precision integer to a string in decimal format. More...

int	Cudd_ApaPrintExponential (FILE *fp, int digits, DdConstApaNumber number, int precision)
	Prints an arbitrary precision integer in exponential format. More...

DdApaNumber	Cudd_ApaCountMinterm (DdManager const manager, DdNode node, int nvars, int *digits)
	Counts the number of minterms of a DD. More...

int	Cudd_ApaPrintMinterm (FILE fp, DdManager const dd, DdNode *node, int nvars)
	Prints the number of minterms of a BDD or ADD using arbitrary precision arithmetic. More...

int	Cudd_ApaPrintMintermExp (FILE fp, DdManager const dd, DdNode *node, int nvars, int precision)
	Prints the number of minterms of a BDD or ADD in exponential format using arbitrary precision arithmetic. More...

int	Cudd_ApaPrintDensity (FILE fp, DdManager dd, DdNode *node, int nvars)
	Prints the density of a BDD or ADD using arbitrary precision arithmetic. More...

static DdApaNumber	cuddApaCountMintermAux (DdManager const manager, DdNode node, int digits, DdApaNumber mmax, DdApaNumber mmin, st_table *table)
	Performs the recursive step of Cudd_ApaCountMinterm. More...

static enum st_retval	cuddApaStCountfree (void key, void value, void *arg)
	Frees the memory used to store the minterm counts recorded in the visited table. More...

Detailed Description

Arbitrary precision arithmetic functions.

This file provides just enough functionality as needed by CUDD to compute the number of minterms of functions with many variables.

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.

Macro Definition Documentation

◆ DD_LSDIGIT

#define DD_LSDIGIT ( x ) ((x) & DD_APA_MASK)

Extract the least significant digit of a double digit.

Side effects None

See also: DD_MSDIGIT

◆ DD_MSDIGIT

#define DD_MSDIGIT ( x ) ((x) >> DD_APA_BITS)

Extract the most significant digit of a double digit.

Side effects None

See also: DD_LSDIGIT

Function Documentation

◆ Cudd_ApaAdd()

DdApaDigit Cudd_ApaAdd	(	int	digits,
		DdConstApaNumber	a,
		DdConstApaNumber	b,
		DdApaNumber	sum
	)

Adds two arbitrary precision integers.

Returns: the carry out of the most significant digit.

Side effects The result of the sum is stored in parameter sum.

◆ Cudd_ApaCompare()

int Cudd_ApaCompare	(	int	digitsFirst,
		DdConstApaNumber	first,
		int	digitsSecond,
		DdConstApaNumber	second
	)

Compares two arbitrary precision integers.

Returns: 1 if the first number is larger; 0 if they are equal; -1 if the second number is larger.

Side effects None

◆ Cudd_ApaCompareRatios()

int Cudd_ApaCompareRatios	(	int	digitsFirst,
		DdConstApaNumber	firstNum,
		unsigned int	firstDen,
		int	digitsSecond,
		DdConstApaNumber	secondNum,
		unsigned int	secondDen
	)

Compares the ratios of two arbitrary precision integers to two unsigned ints.

Returns: 1 if the first number is larger; 0 if they are equal; -1 if the second number is larger.

Side effects None

◆ Cudd_ApaCopy()

void Cudd_ApaCopy	(	int	digits,
		DdConstApaNumber	source,
		DdApaNumber	dest
	)

Makes a copy of an arbitrary precision integer.

Side effects Changes parameter dest.

◆ Cudd_ApaCountMinterm()

DdApaNumber Cudd_ApaCountMinterm	(	DdManager const *	manager,
		DdNode *	node,
		int	nvars,
		int *	digits
	)

Counts the number of minterms of a DD.

The function is assumed to depend on nvars variables. The minterm count is represented as an arbitrary precision unsigned integer, to allow for any number of variables CUDD supports.

Returns: a pointer to the array representing the number of minterms of the function rooted at node if successful; NULL otherwise.

Side effects The number of digits of the result is returned in: parameter digits.

See also: Cudd_CountMinterm

◆ Cudd_ApaIntDivision()

unsigned int Cudd_ApaIntDivision	(	int	digits,
		DdConstApaNumber	dividend,
		unsigned int	divisor,
		DdApaNumber	quotient
	)

Divides an arbitrary precision integer by an integer.

Divides an arbitrary precision integer by a 32-bit unsigned integer. This procedure relies on the assumption that the number of bits of a DdApaDigit plus the number of bits of an unsigned int is less the number of bits of the mantissa of a double. This guarantees that the product of a DdApaDigit and an unsigned int can be represented without loss of precision by a double. On machines where this assumption is not satisfied, this procedure will malfunction.

Returns: the remainder.

Side effects The quotient is returned in parameter quotient.

Deprecated:: The assumption on which the correctness of this function rests is not satisfied by modern-day 64-bit CPUs.

See also: Cudd_ApaShortDivision

◆ Cudd_ApaNumberOfDigits()

int Cudd_ApaNumberOfDigits ( int binaryDigits )

Returns the number of digits for an arbitrary precision integer.

Finds the number of digits for an arbitrary precision integer given the maximum number of binary digits. The number of binary digits should be positive.

Side effects None

◆ Cudd_ApaPowerOfTwo()

void Cudd_ApaPowerOfTwo	(	int	digits,
		DdApaNumber	number,
		int	power
	)

Sets an arbitrary precision integer to a power of two.

If the power of two is too large to be represented, the number is set to 0.

Side effects The result is returned in parameter number.

◆ Cudd_ApaPrintDecimal()

int Cudd_ApaPrintDecimal	(	FILE *	fp,
		int	digits,
		DdConstApaNumber	number
	)

Prints an arbitrary precision integer in decimal format.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_ApaPrintHex Cudd_ApaPrintExponential

◆ Cudd_ApaPrintDensity()

int Cudd_ApaPrintDensity	(	FILE *	fp,
		DdManager *	dd,
		DdNode *	node,
		int	nvars
	)

Prints the density of a BDD or ADD using arbitrary precision arithmetic.

Returns: 1 if successful; 0 otherwise.

Side effects None

◆ Cudd_ApaPrintExponential()

int Cudd_ApaPrintExponential	(	FILE *	fp,
		int	digits,
		DdConstApaNumber	number,
		int	precision
	)

Prints an arbitrary precision integer in exponential format.

Prints as an integer if precision is at least the number of digits to be printed. If precision does not allow printing of all digits, rounds to nearest breaking ties so that the last printed digit is even.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_ApaPrintHex Cudd_ApaPrintDecimal

< readable false
< readable true

◆ Cudd_ApaPrintHex()

int Cudd_ApaPrintHex	(	FILE *	fp,
		int	digits,
		DdConstApaNumber	number
	)

Prints an arbitrary precision integer in hexadecimal format.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_ApaPrintDecimal Cudd_ApaPrintExponential

◆ Cudd_ApaPrintMinterm()

int Cudd_ApaPrintMinterm	(	FILE *	fp,
		DdManager const *	dd,
		DdNode *	node,
		int	nvars
	)

Prints the number of minterms of a BDD or ADD using arbitrary precision arithmetic.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_ApaPrintMintermExp

◆ Cudd_ApaPrintMintermExp()

int Cudd_ApaPrintMintermExp	(	FILE *	fp,
		DdManager const *	dd,
		DdNode *	node,
		int	nvars,
		int	precision
	)

Prints the number of minterms of a BDD or ADD in exponential format using arbitrary precision arithmetic.

Parameter precision controls the number of signficant digits printed.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_ApaPrintMinterm

◆ Cudd_ApaSetToLiteral()

void Cudd_ApaSetToLiteral	(	int	digits,
		DdApaNumber	number,
		DdApaDigit	literal
	)

Sets an arbitrary precision integer to a one-digit literal.

Side effects The result is returned in parameter number.

◆ Cudd_ApaShiftRight()

void Cudd_ApaShiftRight	(	int	digits,
		DdApaDigit	in,
		DdConstApaNumber	a,
		DdApaNumber	b
	)

Shifts right an arbitrary precision integer by one binary place.

The most significant binary digit of the result is taken from parameter in.

Side effects The result is returned in parameter b.

◆ Cudd_ApaShortDivision()

DdApaDigit Cudd_ApaShortDivision	(	int	digits,
		DdConstApaNumber	dividend,
		DdApaDigit	divisor,
		DdApaNumber	quotient
	)

Divides an arbitrary precision integer by a digit.

Returns: the remainder digit.

Side effects The quotient is returned in parameter quotient.

◆ Cudd_ApaStringDecimal()

char* Cudd_ApaStringDecimal	(	int	digits,
		DdConstApaNumber	number
	)

converts an arbitrary precision integer to a string in decimal format.

Returns: the string if successful; NULL otherwise.

Side effects None

See also: Cudd_ApaPrintDecimal

◆ Cudd_ApaSubtract()

DdApaDigit Cudd_ApaSubtract	(	int	digits,
		DdConstApaNumber	a,
		DdConstApaNumber	b,
		DdApaNumber	diff
	)

Subtracts two arbitrary precision integers.

Returns: the borrow out of the most significant digit.

Side effects The result of the subtraction is stored in parameter: diff.

◆ Cudd_FreeApaNumber()

void Cudd_FreeApaNumber ( DdApaNumber number )

Frees an arbitrary precision integer.

Side effects None

See also: Cudd_NewApaNumber

◆ Cudd_NewApaNumber()

DdApaNumber Cudd_NewApaNumber ( int digits )

Allocates memory for an arbitrary precision integer.

Returns: a pointer to the allocated memory if successful; NULL otherwise.

Side effects None

See also: Cudd_FreeApaNumber

◆ cuddApaCountMintermAux()

static DdApaNumber cuddApaCountMintermAux	(	DdManager const *	manager,
		DdNode *	node,
		int	digits,
		DdApaNumber	mmax,
		DdApaNumber	mmin,
		st_table *	table
	)

static

Performs the recursive step of Cudd_ApaCountMinterm.

It is based on the following identity. Let |f| be the number of minterms of f. Then:

|f| = (|f0|+|f1|)/2

where f0 and f1 are the two cofactors of f. Uses the identity |f'| = mmax - |f|. The procedure expects the argument "node" to be a regular pointer, and guarantees this condition is met in the recursive calls. For efficiency, the result of a call is cached only if the node has a reference count greater than 1.

Returns: the number of minterms of the function rooted at node.

Side effects None

◆ cuddApaStCountfree()

static enum st_retval cuddApaStCountfree	(	void *	key,
		void *	value,
		void *	arg
	)