/**CFile****************************************************************
FileName [dec.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [A simple decomposition tree/node data structure and its APIs.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: dec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__opt__dec__dec_h
#define ABC__opt__dec__dec_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Dec_Edge_t_ Dec_Edge_t;
struct Dec_Edge_t_
{
unsigned fCompl : 1; // the complemented bit
unsigned Node : 30; // the decomposition node pointed by the edge
};
typedef struct Dec_Node_t_ Dec_Node_t;
struct Dec_Node_t_
{
Dec_Edge_t eEdge0; // the left child of the node
Dec_Edge_t eEdge1; // the right child of the node
// other info
union { int iFunc; // the literal of the node (AIG)
void * pFunc; }; // the function of the node (BDD or AIG)
unsigned Level : 14; // the level of this node in the global AIG
// printing info
unsigned fNodeOr : 1; // marks the original OR node
unsigned fCompl0 : 1; // marks the original complemented edge
unsigned fCompl1 : 1; // marks the original complemented edge
// latch info
unsigned nLat0 : 5; // the number of latches on the first edge
unsigned nLat1 : 5; // the number of latches on the second edge
unsigned nLat2 : 5; // the number of latches on the output edge
};
typedef struct Dec_Graph_t_ Dec_Graph_t;
struct Dec_Graph_t_
{
int fConst; // marks the constant 1 graph
int nLeaves; // the number of leaves
int nSize; // the number of nodes (including the leaves)
int nCap; // the number of allocated nodes
Dec_Node_t * pNodes; // the array of leaves and internal nodes
Dec_Edge_t eRoot; // the pointer to the topmost node
};
typedef struct Dec_Man_t_ Dec_Man_t;
struct Dec_Man_t_
{
void * pMvcMem; // memory manager for MVC cover (used for factoring)
Vec_Int_t * vCubes; // storage for cubes
Vec_Int_t * vLits; // storage for literals
// precomputation information about 4-variable functions
unsigned short * puCanons; // canonical forms
char * pPhases; // canonical phases
char * pPerms; // canonical permutations
unsigned char * pMap; // mapping of functions into class numbers
};
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
// interator throught the leaves
#define Dec_GraphForEachLeaf( pGraph, pLeaf, i ) \
for ( i = 0; (i < (pGraph)->nLeaves) && (((pLeaf) = Dec_GraphNode(pGraph, i)), 1); i++ )
// interator throught the internal nodes
#define Dec_GraphForEachNode( pGraph, pAnd, i ) \
for ( i = (pGraph)->nLeaves; (i < (pGraph)->nSize) && (((pAnd) = Dec_GraphNode(pGraph, i)), 1); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== decAbc.c ========================================================*/
/*=== decFactor.c ========================================================*/
extern Dec_Graph_t * Dec_Factor( char * pSop );
/*=== decMan.c ========================================================*/
extern Dec_Man_t * Dec_ManStart();
extern void Dec_ManStop( Dec_Man_t * p );
/*=== decPrint.c ========================================================*/
extern void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char * pNameOut );
/*=== decUtil.c ========================================================*/
extern unsigned Dec_GraphDeriveTruth( Dec_Graph_t * pGraph );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creates an edge pointing to the node in the given polarity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_EdgeCreate( int Node, int fCompl )
{
Dec_Edge_t eEdge = { fCompl, Node };
return eEdge;
}
/**Function*************************************************************
Synopsis [Converts the edge into unsigned integer.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline unsigned Dec_EdgeToInt( Dec_Edge_t eEdge )
{
return (eEdge.Node << 1) | eEdge.fCompl;
}
/**Function*************************************************************
Synopsis [Converts unsigned integer into the edge.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_IntToEdge( unsigned Edge )
{
return Dec_EdgeCreate( Edge >> 1, Edge & 1 );
}
/**Function*************************************************************
Synopsis [Converts the edge into unsigned integer.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline unsigned Dec_EdgeToInt_( Dec_Edge_t m ) { union { Dec_Edge_t x; unsigned y; } v; v.x = m; return v.y; }
/*
static inline unsigned Dec_EdgeToInt_( Dec_Edge_t eEdge )
{
return *(unsigned *)&eEdge;
}
*/
/**Function*************************************************************
Synopsis [Converts unsigned integer into the edge.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_IntToEdge_( unsigned m ) { union { Dec_Edge_t x; unsigned y; } v; v.y = m; return v.x; }
/*
static inline Dec_Edge_t Dec_IntToEdge_( unsigned Edge )
{
return *(Dec_Edge_t *)&Edge;
}
*/
/**Function*************************************************************
Synopsis [Creates a graph with the given number of leaves.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Graph_t * Dec_GraphCreate( int nLeaves )
{
Dec_Graph_t * pGraph;
pGraph = ABC_ALLOC( Dec_Graph_t, 1 );
memset( pGraph, 0, sizeof(Dec_Graph_t) );
pGraph->nLeaves = nLeaves;
pGraph->nSize = nLeaves;
pGraph->nCap = 2 * nLeaves + 50;
pGraph->pNodes = ABC_ALLOC( Dec_Node_t, pGraph->nCap );
memset( pGraph->pNodes, 0, sizeof(Dec_Node_t) * pGraph->nSize );
return pGraph;
}
/**Function*************************************************************
Synopsis [Creates constant 0 graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Graph_t * Dec_GraphCreateConst0()
{
Dec_Graph_t * pGraph;
pGraph = ABC_ALLOC( Dec_Graph_t, 1 );
memset( pGraph, 0, sizeof(Dec_Graph_t) );
pGraph->fConst = 1;
pGraph->eRoot.fCompl = 1;
return pGraph;
}
/**Function*************************************************************
Synopsis [Creates constant 1 graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Graph_t * Dec_GraphCreateConst1()
{
Dec_Graph_t * pGraph;
pGraph = ABC_ALLOC( Dec_Graph_t, 1 );
memset( pGraph, 0, sizeof(Dec_Graph_t) );
pGraph->fConst = 1;
return pGraph;
}
/**Function*************************************************************
Synopsis [Creates the literal graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Graph_t * Dec_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl )
{
Dec_Graph_t * pGraph;
assert( 0 <= iLeaf && iLeaf < nLeaves );
pGraph = Dec_GraphCreate( nLeaves );
pGraph->eRoot.Node = iLeaf;
pGraph->eRoot.fCompl = fCompl;
return pGraph;
}
/**Function*************************************************************
Synopsis [Creates a graph with the given number of leaves.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dec_GraphFree( Dec_Graph_t * pGraph )
{
ABC_FREE( pGraph->pNodes );
ABC_FREE( pGraph );
}
/**Function*************************************************************
Synopsis [Returns 1 if the graph is a constant.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphIsConst( Dec_Graph_t * pGraph )
{
return pGraph->fConst;
}
/**Function*************************************************************
Synopsis [Returns 1 if the graph is constant 0.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphIsConst0( Dec_Graph_t * pGraph )
{
return pGraph->fConst && pGraph->eRoot.fCompl;
}
/**Function*************************************************************
Synopsis [Returns 1 if the graph is constant 1.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphIsConst1( Dec_Graph_t * pGraph )
{
return pGraph->fConst && !pGraph->eRoot.fCompl;
}
/**Function*************************************************************
Synopsis [Returns 1 if the graph is complemented.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphIsComplement( Dec_Graph_t * pGraph )
{
return pGraph->eRoot.fCompl;
}
/**Function*************************************************************
Synopsis [Checks if the graph is complemented.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dec_GraphComplement( Dec_Graph_t * pGraph )
{
pGraph->eRoot.fCompl ^= 1;
}
/**Function*************************************************************
Synopsis [Returns the number of leaves.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphLeaveNum( Dec_Graph_t * pGraph )
{
return pGraph->nLeaves;
}
/**Function*************************************************************
Synopsis [Returns the number of internal nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphNodeNum( Dec_Graph_t * pGraph )
{
return pGraph->nSize - pGraph->nLeaves;
}
/**Function*************************************************************
Synopsis [Returns the pointer to the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Node_t * Dec_GraphNode( Dec_Graph_t * pGraph, int i )
{
return pGraph->pNodes + i;
}
/**Function*************************************************************
Synopsis [Returns the pointer to the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Node_t * Dec_GraphNodeLast( Dec_Graph_t * pGraph )
{
return pGraph->pNodes + pGraph->nSize - 1;
}
/**Function*************************************************************
Synopsis [Returns the number of the given node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
{
return pNode - pGraph->pNodes;
}
/**Function*************************************************************
Synopsis [Check if the graph represents elementary variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphIsVar( Dec_Graph_t * pGraph )
{
return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves;
}
/**Function*************************************************************
Synopsis [Check if the graph represents elementary variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
{
return Dec_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves;
}
/**Function*************************************************************
Synopsis [Returns the elementary variable elementary variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Node_t * Dec_GraphVar( Dec_Graph_t * pGraph )
{
assert( Dec_GraphIsVar( pGraph ) );
return Dec_GraphNode( pGraph, pGraph->eRoot.Node );
}
/**Function*************************************************************
Synopsis [Returns the number of the elementary variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphVarInt( Dec_Graph_t * pGraph )
{
assert( Dec_GraphIsVar( pGraph ) );
return Dec_GraphNodeInt( pGraph, Dec_GraphVar(pGraph) );
}
/**Function*************************************************************
Synopsis [Sets the root of the graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dec_GraphSetRoot( Dec_Graph_t * pGraph, Dec_Edge_t eRoot )
{
pGraph->eRoot = eRoot;
}
/**Function*************************************************************
Synopsis [Appends a new node to the graph.]
Description [This procedure is meant for internal use.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Node_t * Dec_GraphAppendNode( Dec_Graph_t * pGraph )
{
Dec_Node_t * pNode;
if ( pGraph->nSize == pGraph->nCap )
{
pGraph->pNodes = ABC_REALLOC( Dec_Node_t, pGraph->pNodes, 2 * pGraph->nCap );
pGraph->nCap = 2 * pGraph->nCap;
}
pNode = pGraph->pNodes + pGraph->nSize++;
memset( pNode, 0, sizeof(Dec_Node_t) );
return pNode;
}
/**Function*************************************************************
Synopsis [Creates an AND node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_GraphAddNodeAnd( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 )
{
Dec_Node_t * pNode;
// get the new node
pNode = Dec_GraphAppendNode( pGraph );
// set the inputs and other info
pNode->eEdge0 = eEdge0;
pNode->eEdge1 = eEdge1;
pNode->fCompl0 = eEdge0.fCompl;
pNode->fCompl1 = eEdge1.fCompl;
return Dec_EdgeCreate( pGraph->nSize - 1, 0 );
}
/**Function*************************************************************
Synopsis [Creates an OR node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_GraphAddNodeOr( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 )
{
Dec_Node_t * pNode;
// get the new node
pNode = Dec_GraphAppendNode( pGraph );
// set the inputs and other info
pNode->eEdge0 = eEdge0;
pNode->eEdge1 = eEdge1;
pNode->fCompl0 = eEdge0.fCompl;
pNode->fCompl1 = eEdge1.fCompl;
// make adjustments for the OR gate
pNode->fNodeOr = 1;
pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl;
pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl;
return Dec_EdgeCreate( pGraph->nSize - 1, 1 );
}
/**Function*************************************************************
Synopsis [Creates an XOR node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_GraphAddNodeXor( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1, int Type )
{
Dec_Edge_t eNode0, eNode1, eNode;
if ( Type == 0 )
{
// derive the first AND
eEdge0.fCompl ^= 1;
eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
eEdge0.fCompl ^= 1;
// derive the second AND
eEdge1.fCompl ^= 1;
eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
// derive the final OR
eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
}
else
{
// derive the first AND
eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
// derive the second AND
eEdge0.fCompl ^= 1;
eEdge1.fCompl ^= 1;
eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
// derive the final OR
eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
eNode.fCompl ^= 1;
}
return eNode;
}
/**Function*************************************************************
Synopsis [Creates an XOR node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_GraphAddNodeMux( Dec_Graph_t * pGraph, Dec_Edge_t eEdgeC, Dec_Edge_t eEdgeT, Dec_Edge_t eEdgeE, int Type )
{
Dec_Edge_t eNode0, eNode1, eNode;
if ( Type == 0 )
{
// derive the first AND
eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
// derive the second AND
eEdgeC.fCompl ^= 1;
eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
// derive the final OR
eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
}
else
{
// complement the arguments
eEdgeT.fCompl ^= 1;
eEdgeE.fCompl ^= 1;
// derive the first AND
eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
// derive the second AND
eEdgeC.fCompl ^= 1;
eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
// derive the final OR
eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
eNode.fCompl ^= 1;
}
return eNode;
}
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////