summaryrefslogtreecommitdiffstats
path: root/src/bool/dec/dec.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/bool/dec/dec.h')
-rw-r--r--src/bool/dec/dec.h725
1 files changed, 725 insertions, 0 deletions
diff --git a/src/bool/dec/dec.h b/src/bool/dec/dec.h
new file mode 100644
index 00000000..07bf9f6b
--- /dev/null
+++ b/src/bool/dec/dec.h
@@ -0,0 +1,725 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 18:32:11 +0000