summaryrefslogtreecommitdiffstats
path: root/src/opt/dec
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/dec')
-rw-r--r--src/opt/dec/dec.h719
-rw-r--r--src/opt/dec/decAbc.c305
-rw-r--r--src/opt/dec/decFactor.c392
-rw-r--r--src/opt/dec/decMan.c83
-rw-r--r--src/opt/dec/decPrint.c284
-rw-r--r--src/opt/dec/decUtil.c134
-rw-r--r--src/opt/dec/module.make5
7 files changed, 1922 insertions, 0 deletions
diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
new file mode 100644
index 00000000..41d22649
--- /dev/null
+++ b/src/opt/dec/dec.h
@@ -0,0 +1,719 @@
+/**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 __DEC_H__
+#define __DEC_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// 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
+ 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 ========================================================*/
+extern Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
+extern Abc_Obj_t * Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
+extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
+extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
+/*=== 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 DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
+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 eEdge )
+{
+ return *(unsigned *)&eEdge;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts unsigned integer into the edge.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+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 = 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 = 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 = 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 = 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 )
+{
+ FREE( pGraph->pNodes );
+ free( pGraph );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the graph is a constant.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph )
+{
+ return pGraph->fConst;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the graph is constant 0.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline bool 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 bool 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 bool 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 bool 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 bool 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 = 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;
+}
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
new file mode 100644
index 00000000..bd960c14
--- /dev/null
+++ b/src/opt/dec/decAbc.c
@@ -0,0 +1,305 @@
+/**CFile****************************************************************
+
+ FileName [decAbc.c]
+
+ PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+ Synopsis [Interface between the decomposition package and ABC network.]
+
+ Author [MVSIS Group]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - February 1, 2003.]
+
+ Revision [$Id: decAbc.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dec.h"
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the decomposition graph into the AIG.]
+
+ Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+ of the leaves of the graph before calling this procedure.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph )
+{
+ Abc_Obj_t * pAnd0, * pAnd1;
+ Dec_Node_t * pNode;
+ int i;
+ // check for constant function
+ if ( Dec_GraphIsConst(pGraph) )
+ return Abc_ObjNotCond( Abc_AigConst1(pNtk), Dec_GraphIsComplement(pGraph) );
+ // check for a literal
+ if ( Dec_GraphIsVar(pGraph) )
+ return Abc_ObjNotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+ // build the AIG nodes corresponding to the AND gates of the graph
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ pAnd0 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ pAnd1 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+ pNode->pFunc = Abc_AigAnd( pNtk->pManFunc, pAnd0, pAnd1 );
+ }
+ // complement the result if necessary
+ return Abc_ObjNotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the decomposition graph into the AIG.]
+
+ Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+ of the leaves of the graph before calling this procedure.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph )
+{
+ Abc_Obj_t * pAnd, * pAnd0, * pAnd1;
+ Dec_Node_t * pNode;
+ int i;
+ // check for constant function
+ if ( Dec_GraphIsConst(pGraph) )
+ return Abc_ObjNotCond( Abc_AigConst1(pNtk), Dec_GraphIsComplement(pGraph) );
+ // check for a literal
+ if ( Dec_GraphIsVar(pGraph) )
+ return Abc_ObjNotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+ // build the AIG nodes corresponding to the AND gates of the graph
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ pAnd0 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ pAnd1 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+// pNode->pFunc = Abc_AigAnd( pNtk->pManFunc, pAnd0, pAnd1 );
+ pAnd = Abc_NtkCreateNode( pNtk );
+ Abc_ObjAddFanin( pAnd, pAnd0 );
+ Abc_ObjAddFanin( pAnd, pAnd1 );
+ pNode->pFunc = pAnd;
+ }
+ // complement the result if necessary
+ return Abc_ObjNotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of new nodes added when using this graph.]
+
+ Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+ of the leaves of the graph before calling this procedure.
+ Returns -1 if the number of nodes and levels exceeded the given limit or
+ the number of levels exceeded the maximum allowed level.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax )
+{
+ Abc_Aig_t * pMan = pRoot->pNtk->pManFunc;
+ Dec_Node_t * pNode, * pNode0, * pNode1;
+ Abc_Obj_t * pAnd, * pAnd0, * pAnd1;
+ int i, Counter, LevelNew, LevelOld;
+ // check for constant function or a literal
+ if ( Dec_GraphIsConst(pGraph) || Dec_GraphIsVar(pGraph) )
+ return 0;
+ // set the levels of the leaves
+ Dec_GraphForEachLeaf( pGraph, pNode, i )
+ pNode->Level = Abc_ObjRegular(pNode->pFunc)->Level;
+ // compute the AIG size after adding the internal nodes
+ Counter = 0;
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ // get the children of this node
+ pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node );
+ pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node );
+ // get the AIG nodes corresponding to the children
+ pAnd0 = pNode0->pFunc;
+ pAnd1 = pNode1->pFunc;
+ if ( pAnd0 && pAnd1 )
+ {
+ // if they are both present, find the resulting node
+ pAnd0 = Abc_ObjNotCond( pAnd0, pNode->eEdge0.fCompl );
+ pAnd1 = Abc_ObjNotCond( pAnd1, pNode->eEdge1.fCompl );
+ pAnd = Abc_AigAndLookup( pMan, pAnd0, pAnd1 );
+ // return -1 if the node is the same as the original root
+ if ( Abc_ObjRegular(pAnd) == pRoot )
+ return -1;
+ }
+ else
+ pAnd = NULL;
+ // count the number of added nodes
+ if ( pAnd == NULL || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pAnd)) )
+ {
+ if ( ++Counter > NodeMax )
+ return -1;
+ }
+ // count the number of new levels
+ LevelNew = 1 + ABC_MAX( pNode0->Level, pNode1->Level );
+ if ( pAnd )
+ {
+ if ( Abc_ObjRegular(pAnd) == Abc_AigConst1(pRoot->pNtk) )
+ LevelNew = 0;
+ else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd0) )
+ LevelNew = (int)Abc_ObjRegular(pAnd0)->Level;
+ else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd1) )
+ LevelNew = (int)Abc_ObjRegular(pAnd1)->Level;
+ LevelOld = (int)Abc_ObjRegular(pAnd)->Level;
+// assert( LevelNew == LevelOld );
+ }
+ if ( LevelNew > LevelMax )
+ return -1;
+ pNode->pFunc = pAnd;
+ pNode->Level = LevelNew;
+ }
+ return Counter;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Replaces MFFC of the node by the new factored form.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain )
+{
+ Abc_Obj_t * pRootNew;
+ Abc_Ntk_t * pNtk = pRoot->pNtk;
+ int nNodesNew, nNodesOld;
+ nNodesOld = Abc_NtkNodeNum(pNtk);
+ // create the new structure of nodes
+ pRootNew = Dec_GraphToNetwork( pNtk, pGraph );
+ // remove the old nodes
+ Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew, fUpdateLevel );
+ // compare the gains
+ nNodesNew = Abc_NtkNodeNum(pNtk);
+ assert( nGain <= nNodesOld - nNodesNew );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the decomposition graph into the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Hop_Obj_t * Dec_GraphToNetworkAig( Hop_Man_t * pMan, Dec_Graph_t * pGraph )
+{
+ Dec_Node_t * pNode;
+ Hop_Obj_t * pAnd0, * pAnd1;
+ int i;
+ // check for constant function
+ if ( Dec_GraphIsConst(pGraph) )
+ return Hop_NotCond( Hop_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
+ // check for a literal
+ if ( Dec_GraphIsVar(pGraph) )
+ return Hop_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+ // build the AIG nodes corresponding to the AND gates of the graph
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ pAnd0 = Hop_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ pAnd1 = Hop_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+ pNode->pFunc = Hop_And( pMan, pAnd0, pAnd1 );
+ }
+ // complement the result if necessary
+ return Hop_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Strashes one logic node using its SOP.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Hop_Obj_t * Dec_GraphFactorSop( Hop_Man_t * pMan, char * pSop )
+{
+ Hop_Obj_t * pFunc;
+ Dec_Graph_t * pFForm;
+ Dec_Node_t * pNode;
+ int i;
+ // perform factoring
+ pFForm = Dec_Factor( pSop );
+ // collect the fanins
+ Dec_GraphForEachLeaf( pFForm, pNode, i )
+ pNode->pFunc = Hop_IthVar( pMan, i );
+ // perform strashing
+ pFunc = Dec_GraphToNetworkAig( pMan, pFForm );
+ Dec_GraphFree( pFForm );
+ return pFunc;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the decomposition graph into the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph )
+{
+ Dec_Node_t * pNode;
+ Ivy_Obj_t * pAnd0, * pAnd1;
+ int i;
+ // check for constant function
+ if ( Dec_GraphIsConst(pGraph) )
+ return Ivy_NotCond( Ivy_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
+ // check for a literal
+ if ( Dec_GraphIsVar(pGraph) )
+ return Ivy_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+ // build the AIG nodes corresponding to the AND gates of the graph
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+ pNode->pFunc = Ivy_And( pMan, pAnd0, pAnd1 );
+ }
+ // complement the result if necessary
+ return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c
new file mode 100644
index 00000000..dca422ea
--- /dev/null
+++ b/src/opt/dec/decFactor.c
@@ -0,0 +1,392 @@
+/**CFile****************************************************************
+
+ FileName [ftFactor.c]
+
+ PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+ Synopsis [Procedures for algebraic factoring.]
+
+ Author [MVSIS Group]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - February 1, 2003.]
+
+ Revision [$Id: ftFactor.c,v 1.3 2003/09/01 04:56:43 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "main.h"
+#include "mvc.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static Dec_Edge_t Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover );
+static Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple );
+static Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover );
+static Dec_Edge_t Dec_FactorTrivialCube( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits );
+static Dec_Edge_t Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr );
+static int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm );
+static Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Factors the cover.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Graph_t * Dec_Factor( char * pSop )
+{
+ Mvc_Cover_t * pCover;
+ Dec_Graph_t * pFForm;
+ Dec_Edge_t eRoot;
+
+ // derive the cover from the SOP representation
+ pCover = Dec_ConvertSopToMvc( pSop );
+
+ // make sure the cover is CCS free (should be done before CST)
+ Mvc_CoverContain( pCover );
+ // check for trivial functions
+ if ( Mvc_CoverIsEmpty(pCover) )
+ {
+ Mvc_CoverFree( pCover );
+ return Dec_GraphCreateConst0();
+ }
+ if ( Mvc_CoverIsTautology(pCover) )
+ {
+ Mvc_CoverFree( pCover );
+ return Dec_GraphCreateConst1();
+ }
+
+ // perform CST
+ Mvc_CoverInverse( pCover ); // CST
+ // start the factored form
+ pFForm = Dec_GraphCreate( Abc_SopGetVarNum(pSop) );
+ // factor the cover
+ eRoot = Dec_Factor_rec( pFForm, pCover );
+ // finalize the factored form
+ Dec_GraphSetRoot( pFForm, eRoot );
+ // complement the factored form if SOP is complemented
+ if ( Abc_SopIsComplement(pSop) )
+ Dec_GraphComplement( pFForm );
+ // verify the factored form
+// if ( !Dec_FactorVerify( pSop, pFForm ) )
+// printf( "Verification has failed.\n" );
+// Mvc_CoverInverse( pCover ); // undo CST
+ Mvc_CoverFree( pCover );
+ return pFForm;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Internal recursive factoring procedure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Edge_t Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
+{
+ Mvc_Cover_t * pDiv, * pQuo, * pRem, * pCom;
+ Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
+ Dec_Edge_t eNodeAnd, eNode;
+
+ // make sure the cover contains some cubes
+ assert( Mvc_CoverReadCubeNum(pCover) );
+
+ // get the divisor
+ pDiv = Mvc_CoverDivisor( pCover );
+ if ( pDiv == NULL )
+ return Dec_FactorTrivial( pFForm, pCover );
+
+ // divide the cover by the divisor
+ Mvc_CoverDivideInternal( pCover, pDiv, &pQuo, &pRem );
+ assert( Mvc_CoverReadCubeNum(pQuo) );
+
+ Mvc_CoverFree( pDiv );
+ Mvc_CoverFree( pRem );
+
+ // check the trivial case
+ if ( Mvc_CoverReadCubeNum(pQuo) == 1 )
+ {
+ eNode = Dec_FactorLF_rec( pFForm, pCover, pQuo );
+ Mvc_CoverFree( pQuo );
+ return eNode;
+ }
+
+ // make the quotient cube free
+ Mvc_CoverMakeCubeFree( pQuo );
+
+ // divide the cover by the quotient
+ Mvc_CoverDivideInternal( pCover, pQuo, &pDiv, &pRem );
+
+ // check the trivial case
+ if ( Mvc_CoverIsCubeFree( pDiv ) )
+ {
+ eNodeDiv = Dec_Factor_rec( pFForm, pDiv );
+ eNodeQuo = Dec_Factor_rec( pFForm, pQuo );
+ Mvc_CoverFree( pDiv );
+ Mvc_CoverFree( pQuo );
+ eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
+ if ( Mvc_CoverReadCubeNum(pRem) == 0 )
+ {
+ Mvc_CoverFree( pRem );
+ return eNodeAnd;
+ }
+ else
+ {
+ eNodeRem = Dec_Factor_rec( pFForm, pRem );
+ Mvc_CoverFree( pRem );
+ return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
+ }
+ }
+
+ // get the common cube
+ pCom = Mvc_CoverCommonCubeCover( pDiv );
+ Mvc_CoverFree( pDiv );
+ Mvc_CoverFree( pQuo );
+ Mvc_CoverFree( pRem );
+
+ // solve the simple problem
+ eNode = Dec_FactorLF_rec( pFForm, pCover, pCom );
+ Mvc_CoverFree( pCom );
+ return eNode;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Internal recursive factoring procedure for the leaf case.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Edge_t Dec_FactorLF_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple )
+{
+ Dec_Man_t * pManDec = Abc_FrameReadManDec();
+ Vec_Int_t * vEdgeLits = pManDec->vLits;
+ Mvc_Cover_t * pDiv, * pQuo, * pRem;
+ Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
+ Dec_Edge_t eNodeAnd;
+
+ // get the most often occurring literal
+ pDiv = Mvc_CoverBestLiteralCover( pCover, pSimple );
+ // divide the cover by the literal
+ Mvc_CoverDivideByLiteral( pCover, pDiv, &pQuo, &pRem );
+ // get the node pointer for the literal
+ eNodeDiv = Dec_FactorTrivialCube( pFForm, pDiv, Mvc_CoverReadCubeHead(pDiv), vEdgeLits );
+ Mvc_CoverFree( pDiv );
+ // factor the quotient and remainder
+ eNodeQuo = Dec_Factor_rec( pFForm, pQuo );
+ Mvc_CoverFree( pQuo );
+ eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
+ if ( Mvc_CoverReadCubeNum(pRem) == 0 )
+ {
+ Mvc_CoverFree( pRem );
+ return eNodeAnd;
+ }
+ else
+ {
+ eNodeRem = Dec_Factor_rec( pFForm, pRem );
+ Mvc_CoverFree( pRem );
+ return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
+ }
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Factoring the cover, which has no algebraic divisors.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
+{
+ Dec_Man_t * pManDec = Abc_FrameReadManDec();
+ Vec_Int_t * vEdgeCubes = pManDec->vCubes;
+ Vec_Int_t * vEdgeLits = pManDec->vLits;
+ Mvc_Manager_t * pMem = pManDec->pMvcMem;
+ Dec_Edge_t eNode;
+ Mvc_Cube_t * pCube;
+ // create the factored form for each cube
+ Vec_IntClear( vEdgeCubes );
+ Mvc_CoverForEachCube( pCover, pCube )
+ {
+ eNode = Dec_FactorTrivialCube( pFForm, pCover, pCube, vEdgeLits );
+ Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) );
+ }
+ // balance the factored forms
+ return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeCubes->pArray, vEdgeCubes->nSize, 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Factoring the cube.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Edge_t Dec_FactorTrivialCube( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits )
+{
+ Dec_Edge_t eNode;
+ int iBit, Value;
+ // create the factored form for each literal
+ Vec_IntClear( vEdgeLits );
+ Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
+ if ( Value )
+ {
+ eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
+ Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
+ }
+ // balance the factored forms
+ return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Create the well-balanced tree of nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Edge_t Dec_FactorTrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr )
+{
+ Dec_Edge_t eNode1, eNode2;
+ int nNodes1, nNodes2;
+
+ if ( nNodes == 1 )
+ return peNodes[0];
+
+ // split the nodes into two parts
+ nNodes1 = nNodes/2;
+ nNodes2 = nNodes - nNodes1;
+// nNodes2 = nNodes/2;
+// nNodes1 = nNodes - nNodes2;
+
+ // recursively construct the tree for the parts
+ eNode1 = Dec_FactorTrivialTree_rec( pFForm, peNodes, nNodes1, fNodeOr );
+ eNode2 = Dec_FactorTrivialTree_rec( pFForm, peNodes + nNodes1, nNodes2, fNodeOr );
+
+ if ( fNodeOr )
+ return Dec_GraphAddNodeOr( pFForm, eNode1, eNode2 );
+ else
+ return Dec_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Converts SOP into MVC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
+{
+ Dec_Man_t * pManDec = Abc_FrameReadManDec();
+ Mvc_Manager_t * pMem = pManDec->pMvcMem;
+ Mvc_Cover_t * pMvc;
+ Mvc_Cube_t * pMvcCube;
+ char * pCube;
+ int nVars, Value, v;
+
+ // start the cover
+ nVars = Abc_SopGetVarNum(pSop);
+ pMvc = Mvc_CoverAlloc( pMem, nVars * 2 );
+ // check the logic function of the node
+ Abc_SopForEachCube( pSop, nVars, pCube )
+ {
+ // create and add the cube
+ pMvcCube = Mvc_CubeAlloc( pMvc );
+ Mvc_CoverAddCubeTail( pMvc, pMvcCube );
+ // fill in the literals
+ Mvc_CubeBitFill( pMvcCube );
+ Abc_CubeForEachVar( pCube, Value, v )
+ {
+ if ( Value == '0' )
+ Mvc_CubeBitRemove( pMvcCube, v * 2 + 1 );
+ else if ( Value == '1' )
+ Mvc_CubeBitRemove( pMvcCube, v * 2 );
+ }
+ }
+ return pMvc;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Verifies that the factoring is correct.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
+{
+ DdManager * dd = Abc_FrameReadManDd();
+ DdNode * bFunc1, * bFunc2;
+ int RetValue;
+ bFunc1 = Abc_ConvertSopToBdd( dd, pSop ); Cudd_Ref( bFunc1 );
+ bFunc2 = Dec_GraphDeriveBdd( dd, pFForm ); Cudd_Ref( bFunc2 );
+//Extra_bddPrint( dd, bFunc1 ); printf("\n");
+//Extra_bddPrint( dd, bFunc2 ); printf("\n");
+ RetValue = (bFunc1 == bFunc2);
+ if ( bFunc1 != bFunc2 )
+ {
+ int s;
+ Extra_bddPrint( dd, bFunc1 ); printf("\n");
+ Extra_bddPrint( dd, bFunc2 ); printf("\n");
+ s = 0;
+ }
+ Cudd_RecursiveDeref( dd, bFunc1 );
+ Cudd_RecursiveDeref( dd, bFunc2 );
+ return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/dec/decMan.c b/src/opt/dec/decMan.c
new file mode 100644
index 00000000..65857461
--- /dev/null
+++ b/src/opt/dec/decMan.c
@@ -0,0 +1,83 @@
+/**CFile****************************************************************
+
+ FileName [decMan.c]
+
+ PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+ Synopsis [Decomposition manager.]
+
+ Author [MVSIS Group]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - February 1, 2003.]
+
+ Revision [$Id: decMan.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "mvc.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Start the MVC manager used in the factoring package.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Man_t * Dec_ManStart()
+{
+ Dec_Man_t * p;
+ int clk = clock();
+ p = ALLOC( Dec_Man_t, 1 );
+ p->pMvcMem = Mvc_ManagerStart();
+ p->vCubes = Vec_IntAlloc( 8 );
+ p->vLits = Vec_IntAlloc( 8 );
+ // canonical forms, phases, perms
+ Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
+//PRT( "NPN classes precomputation time", clock() - clk );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the MVC maanager used in the factoring package.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dec_ManStop( Dec_Man_t * p )
+{
+ Mvc_ManagerFree( p->pMvcMem );
+ Vec_IntFree( p->vCubes );
+ Vec_IntFree( p->vLits );
+ free( p->puCanons );
+ free( p->pPhases );
+ free( p->pPerms );
+ free( p->pMap );
+ free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/dec/decPrint.c b/src/opt/dec/decPrint.c
new file mode 100644
index 00000000..2d8f09b3
--- /dev/null
+++ b/src/opt/dec/decPrint.c
@@ -0,0 +1,284 @@
+/**CFile****************************************************************
+
+ FileName [decPrint.c]
+
+ PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+ Synopsis [Procedures to print the decomposition graphs (factored forms).]
+
+ Author [MVSIS Group]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - February 1, 2003.]
+
+ Revision [$Id: decPrint.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax );
+static int Dec_GraphPrintGetLeafName( FILE * pFile, int iLeaf, int fCompl, char * pNamesIn[] );
+static void Dec_GraphPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax );
+static int Dec_GraphPrintOutputName( FILE * pFile, char * pNameOut, int fCompl );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Prints the decomposition graph.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char * pNameOut )
+{
+ Vec_Ptr_t * vNamesIn = NULL;
+ int LitSizeMax, LitSizeCur, Pos, i;
+
+ // create the names if not given by the user
+ if ( pNamesIn == NULL )
+ {
+ vNamesIn = Abc_NodeGetFakeNames( Dec_GraphLeaveNum(pGraph) );
+ pNamesIn = (char **)vNamesIn->pArray;
+ }
+ if ( pNameOut == NULL )
+ pNameOut = "F";
+
+ // get the size of the longest literal
+ LitSizeMax = 0;
+ for ( i = 0; i < Dec_GraphLeaveNum(pGraph); i++ )
+ {
+ LitSizeCur = strlen(pNamesIn[i]);
+ if ( LitSizeMax < LitSizeCur )
+ LitSizeMax = LitSizeCur;
+ }
+ if ( LitSizeMax > 50 )
+ LitSizeMax = 20;
+
+ // write the decomposition graph (factored form)
+ if ( Dec_GraphIsConst(pGraph) ) // constant
+ {
+ Pos = Dec_GraphPrintOutputName( pFile, pNameOut, 0 );
+ fprintf( pFile, "Constant %d", !Dec_GraphIsComplement(pGraph) );
+ }
+ else if ( Dec_GraphIsVar(pGraph) ) // literal
+ {
+ Pos = Dec_GraphPrintOutputName( pFile, pNameOut, 0 );
+ Dec_GraphPrintGetLeafName( pFile, Dec_GraphVarInt(pGraph), Dec_GraphIsComplement(pGraph), pNamesIn );
+ }
+ else
+ {
+ Pos = Dec_GraphPrintOutputName( pFile, pNameOut, Dec_GraphIsComplement(pGraph) );
+ Dec_GraphPrint_rec( pFile, pGraph, Dec_GraphNodeLast(pGraph), 0, pNamesIn, &Pos, LitSizeMax );
+ }
+ fprintf( pFile, "\n" );
+
+ if ( vNamesIn )
+ Abc_NodeFreeNames( vNamesIn );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dec_GraphPrint2_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax )
+{
+ Dec_Node_t * pNode0, * pNode1;
+ pNode0 = Dec_GraphNode(pGraph, pNode->eEdge0.Node);
+ pNode1 = Dec_GraphNode(pGraph, pNode->eEdge1.Node);
+ if ( Dec_GraphNodeIsVar(pGraph, pNode) ) // FT_NODE_LEAF )
+ {
+ (*pPos) += Dec_GraphPrintGetLeafName( pFile, Dec_GraphNodeInt(pGraph,pNode), fCompl, pNamesIn );
+ return;
+ }
+ if ( !pNode->fNodeOr ) // FT_NODE_AND )
+ {
+ if ( !pNode0->fNodeOr ) // != FT_NODE_OR )
+ Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax );
+ else
+ {
+ fprintf( pFile, "(" );
+ (*pPos)++;
+ Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax );
+ fprintf( pFile, ")" );
+ (*pPos)++;
+ }
+ fprintf( pFile, " " );
+ (*pPos)++;
+
+ Dec_GraphPrintUpdatePos( pFile, pPos, LitSizeMax );
+
+ if ( !pNode1->fNodeOr ) // != FT_NODE_OR )
+ Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax );
+ else
+ {
+ fprintf( pFile, "(" );
+ (*pPos)++;
+ Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax );
+ fprintf( pFile, ")" );
+ (*pPos)++;
+ }
+ return;
+ }
+ if ( pNode->fNodeOr ) // FT_NODE_OR )
+ {
+ Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax );
+ fprintf( pFile, " + " );
+ (*pPos) += 3;
+
+ Dec_GraphPrintUpdatePos( pFile, pPos, LitSizeMax );
+
+ Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax );
+ return;
+ }
+ assert( 0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax )
+{
+ Dec_Node_t * pNode0, * pNode1;
+ Dec_Node_t * pNode00, * pNode01, * pNode10, * pNode11;
+ pNode0 = Dec_GraphNode(pGraph, pNode->eEdge0.Node);
+ pNode1 = Dec_GraphNode(pGraph, pNode->eEdge1.Node);
+ if ( Dec_GraphNodeIsVar(pGraph, pNode) ) // FT_NODE_LEAF )
+ {
+ (*pPos) += Dec_GraphPrintGetLeafName( pFile, Dec_GraphNodeInt(pGraph,pNode), fCompl, pNamesIn );
+ return;
+ }
+ if ( !Dec_GraphNodeIsVar(pGraph, pNode0) && !Dec_GraphNodeIsVar(pGraph, pNode1) )
+ {
+ pNode00 = Dec_GraphNode(pGraph, pNode0->eEdge0.Node);
+ pNode01 = Dec_GraphNode(pGraph, pNode0->eEdge1.Node);
+ pNode10 = Dec_GraphNode(pGraph, pNode1->eEdge0.Node);
+ pNode11 = Dec_GraphNode(pGraph, pNode1->eEdge1.Node);
+ if ( (pNode00 == pNode10 || pNode00 == pNode11) && (pNode01 == pNode10 || pNode01 == pNode11) )
+ {
+ fprintf( pFile, "(" );
+ (*pPos)++;
+ Dec_GraphPrint_rec( pFile, pGraph, pNode00, pNode00->fCompl0, pNamesIn, pPos, LitSizeMax );
+ fprintf( pFile, " # " );
+ (*pPos) += 3;
+ Dec_GraphPrint_rec( pFile, pGraph, pNode01, pNode01->fCompl1, pNamesIn, pPos, LitSizeMax );
+ fprintf( pFile, ")" );
+ (*pPos)++;
+ return;
+ }
+ }
+ if ( fCompl )
+ {
+ fprintf( pFile, "(" );
+ (*pPos)++;
+ Dec_GraphPrint_rec( pFile, pGraph, pNode0, !pNode->fCompl0, pNamesIn, pPos, LitSizeMax );
+ fprintf( pFile, " + " );
+ (*pPos) += 3;
+ Dec_GraphPrint_rec( pFile, pGraph, pNode1, !pNode->fCompl1, pNamesIn, pPos, LitSizeMax );
+ fprintf( pFile, ")" );
+ (*pPos)++;
+ }
+ else
+ {
+ fprintf( pFile, "(" );
+ (*pPos)++;
+ Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax );
+ Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax );
+ fprintf( pFile, ")" );
+ (*pPos)++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dec_GraphPrintGetLeafName( FILE * pFile, int iLeaf, int fCompl, char * pNamesIn[] )
+{
+ static char Buffer[100];
+ sprintf( Buffer, "%s%s", pNamesIn[iLeaf], fCompl? "\'" : "" );
+ fprintf( pFile, "%s", Buffer );
+ return strlen( Buffer );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dec_GraphPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax )
+{
+ int i;
+ if ( *pPos + LitSizeMax < 77 )
+ return;
+ fprintf( pFile, "\n" );
+ for ( i = 0; i < 10; i++ )
+ fprintf( pFile, " " );
+ *pPos = 10;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the printout for a decomposition graph.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dec_GraphPrintOutputName( FILE * pFile, char * pNameOut, int fCompl )
+{
+ if ( pNameOut == NULL )
+ return 0;
+ fprintf( pFile, "%6s%s = ", pNameOut, fCompl? "\'" : " " );
+ return 10;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/dec/decUtil.c b/src/opt/dec/decUtil.c
new file mode 100644
index 00000000..463bc7e2
--- /dev/null
+++ b/src/opt/dec/decUtil.c
@@ -0,0 +1,134 @@
+/**CFile****************************************************************
+
+ FileName [decUtil.c]
+
+ PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
+
+ Synopsis [Decomposition unitilies.]
+
+ Author [MVSIS Group]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - February 1, 2003.]
+
+ Revision [$Id: decUtil.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dec.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Converts graph to BDD.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph )
+{
+ DdNode * bFunc, * bFunc0, * bFunc1;
+ Dec_Node_t * pNode;
+ int i;
+
+ // sanity checks
+ assert( Dec_GraphLeaveNum(pGraph) >= 0 );
+ assert( Dec_GraphLeaveNum(pGraph) <= pGraph->nSize );
+
+ // check for constant function
+ if ( Dec_GraphIsConst(pGraph) )
+ return Cudd_NotCond( b1, Dec_GraphIsComplement(pGraph) );
+ // check for a literal
+ if ( Dec_GraphIsVar(pGraph) )
+ return Cudd_NotCond( Cudd_bddIthVar(dd, Dec_GraphVarInt(pGraph)), Dec_GraphIsComplement(pGraph) );
+
+ // assign the elementary variables
+ Dec_GraphForEachLeaf( pGraph, pNode, i )
+ pNode->pFunc = Cudd_bddIthVar( dd, i );
+
+ // compute the function for each internal node
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ bFunc0 = Cudd_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ bFunc1 = Cudd_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+ pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( pNode->pFunc );
+ }
+
+ // deref the intermediate results
+ bFunc = pNode->pFunc; Cudd_Ref( bFunc );
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ Cudd_RecursiveDeref( dd, pNode->pFunc );
+ Cudd_Deref( bFunc );
+
+ // complement the result if necessary
+ return Cudd_NotCond( bFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Dec_GraphDeriveTruth( Dec_Graph_t * pGraph )
+{
+ unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+ unsigned uTruth, uTruth0, uTruth1;
+ Dec_Node_t * pNode;
+ int i;
+
+ // sanity checks
+ assert( Dec_GraphLeaveNum(pGraph) >= 0 );
+ assert( Dec_GraphLeaveNum(pGraph) <= pGraph->nSize );
+ assert( Dec_GraphLeaveNum(pGraph) <= 5 );
+
+ // check for constant function
+ if ( Dec_GraphIsConst(pGraph) )
+ return Dec_GraphIsComplement(pGraph)? 0 : ~((unsigned)0);
+ // check for a literal
+ if ( Dec_GraphIsVar(pGraph) )
+ return Dec_GraphIsComplement(pGraph)? ~uTruths[Dec_GraphVarInt(pGraph)] : uTruths[Dec_GraphVarInt(pGraph)];
+
+ // assign the elementary variables
+ Dec_GraphForEachLeaf( pGraph, pNode, i )
+ pNode->pFunc = (void *)uTruths[i];
+
+ // compute the function for each internal node
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ uTruth0 = (unsigned)Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
+ uTruth1 = (unsigned)Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
+ uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0;
+ uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1;
+ uTruth = uTruth0 & uTruth1;
+ pNode->pFunc = (void *)uTruth;
+ }
+
+ // complement the result if necessary
+ return Dec_GraphIsComplement(pGraph)? ~uTruth : uTruth;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/dec/module.make b/src/opt/dec/module.make
new file mode 100644
index 00000000..1e0722d5
--- /dev/null
+++ b/src/opt/dec/module.make
@@ -0,0 +1,5 @@
+SRC += src/opt/dec/decAbc.c \
+ src/opt/dec/decFactor.c \
+ src/opt/dec/decMan.c \
+ src/opt/dec/decPrint.c \
+ src/opt/dec/decUtil.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 16:02:08 +0000