cudd/cuddEssent.c File Reference

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...

Defines

#define BPL   32
#define LOGBPL   5

Typedefs

typedef ptruint BitVector
typedef struct TlClause TlClause

Functions

DdNodeCudd_FindEssential (DdManager *dd, DdNode *f)
 Finds the essential variables of a DD.
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.
DdTlcInfoCudd_FindTwoLiteralClauses (DdManager *dd, DdNode *f)
 Finds the two literal clauses of a DD.
int Cudd_ReadIthClause (DdTlcInfo *tlc, int i, unsigned *var1, unsigned *var2, int *phase1, int *phase2)
 Accesses the i-th clause of a DD.
int Cudd_PrintTwoLiteralClauses (DdManager *dd, DdNode *f, char **names, FILE *fp)
 Prints the one- and two-literal clauses of a DD.
void Cudd_tlcInfoFree (DdTlcInfo *t)
 Frees a DdTlcInfo Structure.
static DdNodeddFindEssentialRecur (DdManager *dd, DdNode *f)
 Implements the recursive step of Cudd_FindEssential.
static DdTlcInfoddFindTwoLiteralClausesRecur (DdManager *dd, DdNode *f, st_table *table, BitVector *Tolv, BitVector *Tolp, BitVector *Eolv, BitVector *Eolp)
 Implements the recursive step of Cudd_FindTwoLiteralClauses.
static DdTlcInfocomputeClauses (DdTlcInfo *Tres, DdTlcInfo *Eres, DdHalfWord label, int size, BitVector *Tolv, BitVector *Tolp, BitVector *Eolv, BitVector *Eolp)
 Computes the two-literal clauses for a node.
static DdTlcInfocomputeClausesWithUniverse (DdTlcInfo *Cres, DdHalfWord label, short phase)
 Computes the two-literal clauses for a node.
static DdTlcInfoemptyClauseSet (void)
 Returns an enpty set of clauses.
static int sentinelp (DdHalfWord var1, DdHalfWord var2)
 Returns true iff the argument is the sentinel clause.
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.
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.
static int oneliteralp (DdHalfWord var)
 Returns true iff the argument is a one-literal clause.
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.
static BitVector * bitVectorAlloc (int size)
 Allocates a bit vector.
static void bitVectorClear (BitVector *vector, int size)
 Clears a bit vector.
static void bitVectorFree (BitVector *vector)
 Frees a bit vector.
static short bitVectorRead (BitVector *vector, int i)
 Returns the i-th entry of a bit vector.
static void bitVectorSet (BitVector *vector, int i, short val)
 Sets the i-th entry of a bit vector to a value.
static DdTlcInfotlcInfoAlloc (void)
 Allocates a DdTlcInfo Structure.

Detailed Description

Functions for the detection of essential variables.

Author:
Fabio Somenzi

Copyright (c) 1995-2015, Regents of the University of Colorado

All rights reserved.

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

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
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
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
static void bitVectorFree ( BitVector *  vector  )  [static]

Frees a bit vector.

Side effects
None
See also:
bitVectorAlloc
static short bitVectorRead ( BitVector *  vector,
int  i 
) [static]

Returns the i-th entry of a bit vector.

Side effects
None
See also:
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
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
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
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
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 1. 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
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
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
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
void Cudd_tlcInfoFree ( DdTlcInfo t  ) 

Frees a DdTlcInfo Structure.

Also frees the memory pointed by it.

Side effects
None
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
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
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
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
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
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
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
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
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1