Functions for the detection of essential variables. More...

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

Include dependency graph for cuddEssent.c:

Data Structures
struct	DdTlcInfo
	This structure holds the set of clauses for a node. More...

struct	TlClause
	This structure is for temporary representation of sets of clauses. More...

Macros
#define	BPL 64

#define	LOGBPL 6

Typedefs
typedef ptruint	BitVector

typedef struct TlClause	TlClause

Functions
DdNode *	Cudd_FindEssential (DdManager dd, DdNode f)
	Finds the essential variables of a DD. More...

int	Cudd_bddIsVarEssential (DdManager manager, DdNode f, int id, int phase)
	Determines whether a given variable is essential with a given phase in a BDD. More...

DdTlcInfo *	Cudd_FindTwoLiteralClauses (DdManager dd, DdNode f)
	Finds the two literal clauses of a DD. More...

int	Cudd_ReadIthClause (DdTlcInfo tlc, int i, unsigned var1, unsigned var2, int phase1, int *phase2)
	Accesses the i-th clause of a DD. More...

int	Cudd_PrintTwoLiteralClauses (DdManager dd, DdNode f, char *names, FILE fp)
	Prints the one- and two-literal clauses of a DD. More...

void	Cudd_tlcInfoFree (DdTlcInfo *t)
	Frees a DdTlcInfo Structure. More...

static DdNode *	ddFindEssentialRecur (DdManager dd, DdNode f)
	Implements the recursive step of Cudd_FindEssential. More...

static DdTlcInfo *	ddFindTwoLiteralClausesRecur (DdManager dd, DdNode f, st_table table, BitVector Tolv, BitVector Tolp, BitVector Eolv, BitVector *Eolp)
	Implements the recursive step of Cudd_FindTwoLiteralClauses. More...

static DdTlcInfo *	computeClauses (DdTlcInfo Tres, DdTlcInfo Eres, DdHalfWord label, int size, BitVector Tolv, BitVector Tolp, BitVector Eolv, BitVector Eolp)
	Computes the two-literal clauses for a node. More...

static DdTlcInfo *	computeClausesWithUniverse (DdTlcInfo *Cres, DdHalfWord label, short phase)
	Computes the two-literal clauses for a node. More...

static DdTlcInfo *	emptyClauseSet (void)
	Returns an enpty set of clauses. More...

static int	sentinelp (DdHalfWord var1, DdHalfWord var2)
	Returns true iff the argument is the sentinel clause. More...

static int	equalp (DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b)
	Returns true iff the two arguments are identical clauses. More...

static int	beforep (DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b)
	Returns true iff the first argument precedes the second in the clause order. More...

static int	oneliteralp (DdHalfWord var)
	Returns true iff the argument is a one-literal clause. More...

static int	impliedp (DdHalfWord var1, short phase1, DdHalfWord var2, short phase2, BitVector olv, BitVector olp)
	Returns true iff either literal of a clause is in a set of literals. More...

static BitVector *	bitVectorAlloc (int size)
	Allocates a bit vector. More...

static void	bitVectorClear (BitVector *vector, int size)
	Clears a bit vector. More...

static void	bitVectorFree (BitVector *vector)
	Frees a bit vector. More...

static short	bitVectorRead (BitVector *vector, int i)
	Returns the i-th entry of a bit vector. More...

static void	bitVectorSet (BitVector *vector, int i, short val)
	Sets the i-th entry of a bit vector to a value. More...

static DdTlcInfo *	tlcInfoAlloc (void)
	Allocates a DdTlcInfo Structure. More...

Detailed Description

Functions for the detection of essential 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.

Function Documentation

◆ beforep()

static int beforep	(	DdHalfWord	var1a,
		short	phase1a,
		DdHalfWord	var1b,
		short	phase1b,
		DdHalfWord	var2a,
		short	phase2a,
		DdHalfWord	var2b,
		short	phase2b
	)

static

Returns true iff the first argument precedes the second in the clause order.

A clause precedes another if its first lieral precedes the first literal of the other, or if the first literals are the same, and its second literal precedes the second literal of the other clause. A literal precedes another if it has a higher index, of if it has the same index, but it has lower phase. Phase 0 is the positive phase, and it is lower than Phase 1 (negative phase).

Side effects None

See also: equalp

◆ bitVectorAlloc()

static BitVector* bitVectorAlloc ( int size )

static

Allocates a bit vector.

The parameter size gives the number of bits. This procedure allocates enough words to hold the specified number of bits.

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

Side effects None

See also: bitVectorClear bitVectorFree

◆ bitVectorClear()

static void bitVectorClear	(	BitVector *	vector,
		int	size
	)

static

Clears a bit vector.

The parameter size gives the number of bits.

Side effects None

See also: bitVectorAlloc

◆ bitVectorFree()

static void bitVectorFree ( BitVector * vector )

static

Frees a bit vector.

Side effects None

See also: bitVectorAlloc

◆ bitVectorRead()

static short bitVectorRead	(	BitVector *	vector,
		int	i
	)

static

Returns the i-th entry of a bit vector.

Side effects None

See also: bitVectorSet

◆ bitVectorSet()

static void bitVectorSet	(	BitVector *	vector,
		int	i,
		short	val
	)

static

Sets the i-th entry of a bit vector to a value.

Side effects None

See also: bitVectorRead

◆ computeClauses()

static DdTlcInfo* computeClauses	(	DdTlcInfo *	Tres,
		DdTlcInfo *	Eres,
		DdHalfWord	label,
		int	size,
		BitVector *	Tolv,
		BitVector *	Tolp,
		BitVector *	Eolv,
		BitVector *	Eolp
	)

static

Computes the two-literal clauses for a node.

Computes the two-literal clauses for a node given the clauses for its children and the label of the node.

Returns: a pointer to a TclInfo structure if successful; NULL otherwise.

Side effects None

See also: computeClausesWithUniverse

Parameters

Tres	list of clauses for T child
Eres	list of clauses for E child
label	variable labeling the current node
size	number of variables in the manager
Tolv	variable bit vector for T child
Tolp	phase bit vector for T child
Eolv	variable bit vector for E child
Eolp	phase bit vector for E child

◆ computeClausesWithUniverse()

static DdTlcInfo* computeClausesWithUniverse	(	DdTlcInfo *	Cres,
		DdHalfWord	label,
		short	phase
	)

static

Computes the two-literal clauses for a node.

Computes the two-literal clauses for a node with a zero child, given the clauses for its other child and the label of the node.

Returns: a pointer to a TclInfo structure if successful; NULL otherwise.

Side effects None

See also: computeClauses

◆ Cudd_bddIsVarEssential()

int Cudd_bddIsVarEssential	(	DdManager *	manager,
		DdNode *	f,
		int	id,
		int	phase
	)

Determines whether a given variable is essential with a given phase in a BDD.

Uses Cudd_bddIteConstant. Returns 1 if phase == 1 and f–>x_id, or if phase == 0 and f–>x_id'.

Side effects None

See also: Cudd_FindEssential

◆ Cudd_FindEssential()

DdNode* Cudd_FindEssential	(	DdManager *	dd,
		DdNode *	f
	)

Finds the essential variables of a DD.

Returns the cube of the essential variables. A positive literal means that the variable must be set to 1 for the function to be

A negative literal means that the variable must be set to 0 for the function to be 1.

Returns: a pointer to the cube BDD if successful; NULL otherwise.

Side effects None

See also: Cudd_bddIsVarEssential

◆ Cudd_FindTwoLiteralClauses()

DdTlcInfo* Cudd_FindTwoLiteralClauses	(	DdManager *	dd,
		DdNode *	f
	)

Finds the two literal clauses of a DD.

Returns the one- and two-literal clauses of a DD. For a constant DD, the empty set of clauses is returned. This is obviously correct for a non-zero constant. For the constant zero, it is based on the assumption that only those clauses containing variables in the support of the function are considered. Since the support of a constant function is empty, no clauses are returned.

Returns: a pointer to the structure holding the clauses if successful; NULL otherwise.

Side effects None

See also: Cudd_FindEssential

◆ Cudd_PrintTwoLiteralClauses()

int Cudd_PrintTwoLiteralClauses	(	DdManager *	dd,
		DdNode *	f,
		char **	names,
		FILE *	fp
	)

Prints the one- and two-literal clauses of a DD.

The argument "names" can be NULL, in which case the variable indices are printed.

Returns: 1 if successful; 0 otherwise.

Side effects None

See also: Cudd_FindTwoLiteralClauses

◆ Cudd_ReadIthClause()

int Cudd_ReadIthClause	(	DdTlcInfo *	tlc,
		int	i,
		unsigned *	var1,
		unsigned *	var2,
		int *	phase1,
		int *	phase2
	)

Accesses the i-th clause of a DD.

Accesses the i-th clause of a DD given the clause set which must be already computed.

Returns: 1 if successful; 0 if i is out of range, or in case of error.

Side effects the four components of a clause are returned as side effects.

See also: Cudd_FindTwoLiteralClauses

◆ Cudd_tlcInfoFree()

void Cudd_tlcInfoFree ( DdTlcInfo * t )

Frees a DdTlcInfo Structure.

Also frees the memory pointed by it.

Side effects None

◆ ddFindEssentialRecur()

static DdNode* ddFindEssentialRecur	(	DdManager *	dd,
		DdNode *	f
	)

static

Implements the recursive step of Cudd_FindEssential.

Returns: a pointer to the cube BDD if successful; NULL otherwise.

Side effects None

◆ ddFindTwoLiteralClausesRecur()

static DdTlcInfo* ddFindTwoLiteralClausesRecur	(	DdManager *	dd,
		DdNode *	f,
		st_table *	table,
		BitVector *	Tolv,
		BitVector *	Tolp,
		BitVector *	Eolv,
		BitVector *	Eolp
	)

static

Implements the recursive step of Cudd_FindTwoLiteralClauses.

The DD node is assumed to be not constant.

Returns: a pointer to a set of clauses if successful; NULL otherwise.

Side effects None

See also: Cudd_FindTwoLiteralClauses

◆ emptyClauseSet()

static DdTlcInfo* emptyClauseSet ( void )

static

Returns an enpty set of clauses.

No bit vector for the phases is allocated.

Returns: a pointer to an empty set of clauses if successful; NULL otherwise.

Side effects None

◆ equalp()

static int equalp	(	DdHalfWord	var1a,
		short	phase1a,
		DdHalfWord	var1b,
		short	phase1b,
		DdHalfWord	var2a,
		short	phase2a,
		DdHalfWord	var2b,
		short	phase2b
	)

static

Returns true iff the two arguments are identical clauses.

Since literals are sorted, we only need to compare literals in the same position.

Side effects None

See also: beforep

◆ impliedp()

static int impliedp	(	DdHalfWord	var1,
		short	phase1,
		DdHalfWord	var2,
		short	phase2,
		BitVector *	olv,
		BitVector *	olp
	)

static

Returns true iff either literal of a clause is in a set of literals.

The first four arguments specify the clause. The remaining two arguments specify the literal set.

Side effects None

◆ oneliteralp()

static int oneliteralp ( DdHalfWord var )

static

Returns true iff the argument is a one-literal clause.

A one-litaral clause has the constant FALSE as second literal. Since the constant TRUE is never used, it is sufficient to test for a constant.

Side effects None

◆ sentinelp()

static int sentinelp	(	DdHalfWord	var1,
		DdHalfWord	var2
	)

static

Returns true iff the argument is the sentinel clause.

A sentinel clause has both variables equal to 0.

Side effects None

◆ tlcInfoAlloc()

static DdTlcInfo* tlcInfoAlloc ( void )

static

Allocates a DdTlcInfo Structure.

Returns: a pointer to a DdTlcInfo Structure if successful; NULL otherwise.

Side effects None

See also: Cudd_tlcInfoFree

Data Structures

Macros

Typedefs

Functions

Detailed Description

Function Documentation

◆ beforep()

◆ bitVectorAlloc()

◆ bitVectorClear()

◆ bitVectorFree()

◆ bitVectorRead()

◆ bitVectorSet()

◆ computeClauses()

◆ computeClausesWithUniverse()

◆ Cudd_bddIsVarEssential()

◆ Cudd_FindEssential()

◆ Cudd_FindTwoLiteralClauses()

◆ Cudd_PrintTwoLiteralClauses()

◆ Cudd_ReadIthClause()

◆ Cudd_tlcInfoFree()

◆ ddFindEssentialRecur()

◆ ddFindTwoLiteralClausesRecur()

◆ emptyClauseSet()

◆ equalp()

◆ impliedp()

◆ oneliteralp()

◆ sentinelp()

◆ tlcInfoAlloc()