summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/dec/dec.h543
-rw-r--r--src/opt/dec/decAbc.c170
-rw-r--r--src/opt/dec/decFactor.c393
-rw-r--r--src/opt/dec/decMan.c83
-rw-r--r--src/opt/dec/decPrint.c221
-rw-r--r--src/opt/dec/decUtil.c134
-rw-r--r--src/opt/dec/module.make6
-rw-r--r--src/opt/rwr/rwr.h5
-rw-r--r--src/opt/rwr/rwrDec.c156
-rw-r--r--src/opt/rwr/rwrEva.c55
-rw-r--r--src/opt/rwr/rwrMan.c39
11 files changed, 1489 insertions, 316 deletions
diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
index 26af6b1c..6ecc9678 100644
--- a/src/opt/dec/dec.h
+++ b/src/opt/dec/dec.h
@@ -33,83 +33,89 @@
/// 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_
{
- // the first child
- unsigned fCompl0 : 1; // complemented attribute of the first fanin
- unsigned iFanin0 : 11; // the number of the first fanin
- // the second child
- unsigned fCompl1 : 1; // complemented attribute of the second fanin
- unsigned iFanin1 : 11; // the number of the second fanin
+ Dec_Edge_t eEdge0; // the left child of the node
+ Dec_Edge_t eEdge1; // the right child of the node
// other info
- unsigned fIntern : 1; // marks all internal nodes (to distinquish them from elementary vars)
- unsigned fConst : 1; // marks the constant 1 function (topmost node only)
- unsigned fCompl : 1; // marks the complement of topmost node (topmost node only)
- // printing info (factored forms only)
- unsigned fNodeOr : 1; // marks the original OR node
- unsigned fEdge0 : 1; // marks the original complemented edge
- unsigned fEdge1 : 1; // marks the original complemented edge
- // some bits are left unused
+ void * pFunc; // the function of the node (BDD or AIG)
+ unsigned Level : 16; // 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
+};
+
+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
};
-/*
- The decomposition tree data structure is designed to represent relatively small
- (up to 100 nodes) AIGs used for factoring, rewriting, and decomposition.
-
- For simplicity, the nodes of the decomposition tree are written in DFS order
- into an integer vector (Vec_Int_t). The decomposition node (Dec_Node_t)
- is typecast into an integer when written into the array.
-
- This representation can be readily translated into the main AIG represented
- in the ABC network. Because of the linear order of the decomposition nodes
- in the array, it is easy to put the existing AIG nodes in correspondence with
- them. This process begins by first putting leaves of the decomposition tree
- in correpondence with the fanins of the cut used to derive the function,
- which was decomposed. Next for each internal node of the decomposition tree,
- we find or create a corresponding node in the AIG. Finally, the root node of
- the tree replaces the original root node of the cut, which was decomposed.
-
- To achieve the above scenario, we reserve the first n entries for the array
- to the fanins of the cut (the number of fanins is n). These entries are left
- empty in the array (that is, they are represented by 0 integer). Each entry
- after the fanins is an internal node (flag fIntern is set to 1). The internal
- nodes can have complemented inputs (denoted by flags fComp0 and fCompl1).
- The last node can be complemented (fCompl), which is true if the root node
- of the decomposition tree is represented by a complemented AIG node.
-
- Two cases have to be specially considered: a constant function and a function
- equal to an elementary variables (possibly complemented). In these two cases,
- the decomposition tree/array has exactly n+1 nodes, where n in the number of
- fanins. (A constant function may depend on n variable, in which case these
- are redundant variables. Similarly, a function can be a function in n-D space
- but in fact depend only on one variable in this space.)
-
- When the function is a constant, the last node has a flag fConst set to 1.
- In this case the complemented flag (fCompl) shows the value of the constant.
- (fCompl = 0 means costant 1; fCompl = 1 means constant 0).
- When the function if an elementary variable, the last node has both pointers
- pointing to the same elementary node, while the complemented flag (fCompl)
- shows whether the variable is complemented. For example: x' = Not( AND(x, x) ).
-
- When manipulating the decomposition tree, it is convenient to return the
- intermediate results of decomposition as an integer, which includes the number
- of the Dec_Node_t in the array of decomposition nodes and the complemented flag.
- Factoring is a special case of decomposition, which demonstrates this kind
- of manipulation.
-*/
////////////////////////////////////////////////////////////////////////
-/// MACRO DEFITIONS ///
+/// 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_Aig_t * pMan, 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, 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 DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
/**Function*************************************************************
- Synopsis [Cleans the decomposition node.]
+ Synopsis [Creates an edge pointing to the node in the given polarity.]
Description []
@@ -117,12 +123,16 @@ struct Dec_Node_t_
SeeAlso []
-***********************************************************************/
-static inline void Dec_NodeClean( Dec_Node_t * pNode ) { *((int *)pNode) = 0; }
+***********************************************************************/
+static inline Dec_Edge_t Dec_EdgeCreate( int Node, int fCompl )
+{
+ Dec_Edge_t eEdge = { fCompl, Node };
+ return eEdge;
+}
/**Function*************************************************************
- Synopsis [Convert between an interger and an decomposition node.]
+ Synopsis [Converts the edge into unsigned integer.]
Description []
@@ -131,12 +141,14 @@ static inline void Dec_NodeClean( Dec_Node_t * pNode ) { *((int *
SeeAlso []
***********************************************************************/
-static inline Dec_Node_t Dec_Int2Node( int Num ) { return *((Dec_Node_t *)&Num); }
-static inline int Dec_Node2Int( Dec_Node_t Node ) { return *((int *)&Node); }
+static inline unsigned Dec_EdgeToInt( Dec_Edge_t eEdge )
+{
+ return (eEdge.Node << 1) | eEdge.fCompl;
+}
/**Function*************************************************************
- Synopsis [Returns the pointer to the i-th decomposition node.]
+ Synopsis [Converts unsigned integer into the edge.]
Description []
@@ -145,11 +157,14 @@ static inline int Dec_Node2Int( Dec_Node_t Node ) { return *
SeeAlso []
***********************************************************************/
-static inline Dec_Node_t * Dec_NodeRead( Vec_Int_t * vDec, int i ) { return (Dec_Node_t *)vDec->pArray + i; }
+static inline Dec_Edge_t Dec_IntToEdge( unsigned Edge )
+{
+ return Dec_EdgeCreate( Edge >> 1, Edge & 1 );
+}
/**Function*************************************************************
- Synopsis [Returns the pointer to the last decomposition node.]
+ Synopsis [Converts the edge into unsigned integer.]
Description []
@@ -158,11 +173,14 @@ static inline Dec_Node_t * Dec_NodeRead( Vec_Int_t * vDec, int i ) { return (
SeeAlso []
***********************************************************************/
-static inline Dec_Node_t * Dec_NodeReadLast( Vec_Int_t * vDec ) { return (Dec_Node_t *)vDec->pArray + vDec->nSize - 1; }
+static inline unsigned Dec_EdgeToInt_( Dec_Edge_t eEdge )
+{
+ return *(unsigned *)&eEdge;
+}
/**Function*************************************************************
- Synopsis [Returns the pointer to the fanins of the i-th decomposition node.]
+ Synopsis [Converts unsigned integer into the edge.]
Description []
@@ -171,12 +189,14 @@ static inline Dec_Node_t * Dec_NodeReadLast( Vec_Int_t * vDec ) { return (
SeeAlso []
***********************************************************************/
-static inline Dec_Node_t * Dec_NodeFanin0( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (Dec_Node_t *)vDec->pArray + Dec_NodeRead(vDec,i)->iFanin0; }
-static inline Dec_Node_t * Dec_NodeFanin1( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (Dec_Node_t *)vDec->pArray + Dec_NodeRead(vDec,i)->iFanin1; }
+static inline Dec_Edge_t Dec_IntToEdge_( unsigned Edge )
+{
+ return *(Dec_Edge_t *)&Edge;
+}
/**Function*************************************************************
- Synopsis [Returns the complemented attributes of the i-th decomposition node.]
+ Synopsis [Creates a graph with the given number of leaves.]
Description []
@@ -185,12 +205,22 @@ static inline Dec_Node_t * Dec_NodeFanin1( Vec_Int_t * vDec, int i ) { assert( D
SeeAlso []
***********************************************************************/
-static inline bool Dec_NodeFaninC0( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (bool)Dec_NodeRead(vDec,i)->fCompl0; }
-static inline bool Dec_NodeFaninC1( Vec_Int_t * vDec, int i ) { assert( Dec_NodeRead(vDec,i)->fIntern ); return (bool)Dec_NodeRead(vDec,i)->fCompl1; }
+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 [Returns the number of leaf variables.]
+ Synopsis [Creates constant 0 graph.]
Description []
@@ -199,18 +229,19 @@ static inline bool Dec_NodeFaninC1( Vec_Int_t * vDec, int i ) { assert(
SeeAlso []
***********************************************************************/
-static inline int Dec_TreeNumVars( Vec_Int_t * vDec )
+static inline Dec_Graph_t * Dec_GraphCreateConst0()
{
- int i;
- for ( i = 0; i < vDec->nSize; i++ )
- if ( vDec->pArray[i] )
- break;
- return i;
+ 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 [Returns the number of AND nodes in the tree.]
+ Synopsis [Creates constant 1 graph.]
Description []
@@ -219,20 +250,56 @@ static inline int Dec_TreeNumVars( Vec_Int_t * vDec )
SeeAlso []
***********************************************************************/
-static int Dec_TreeNumAnds( Vec_Int_t * vDec )
+static inline Dec_Graph_t * Dec_GraphCreateConst1()
{
- Dec_Node_t * pNode;
- pNode = Dec_NodeReadLast(vDec);
- if ( pNode->fConst ) // constant
- return 0;
- if ( pNode->iFanin0 == pNode->iFanin1 ) // literal
- return 0;
- return vDec->nSize - Dec_TreeNumVars(vDec);
+ 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 the number of literals in the factored form.]
+ Synopsis [Returns 1 if the graph is a constant.]
Description []
@@ -241,16 +308,30 @@ static int Dec_TreeNumAnds( Vec_Int_t * vDec )
SeeAlso []
***********************************************************************/
-static inline int Dec_TreeNumFFLits( Vec_Int_t * vDec )
+static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph )
{
- return 1 + Dec_TreeNumAnds( vDec );
+ 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 [Checks if the output node of the decomposition tree is complemented.]
+ Synopsis [Returns 1 if the graph is constant 1.]
Description []
@@ -259,11 +340,14 @@ static inline int Dec_TreeNumFFLits( Vec_Int_t * vDec )
SeeAlso []
***********************************************************************/
-static inline bool Dec_TreeIsComplement( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fCompl; }
+static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph )
+{
+ return pGraph->fConst && !pGraph->eRoot.fCompl;
+}
/**Function*************************************************************
- Synopsis [Complements the output node of the decomposition tree.]
+ Synopsis [Returns 1 if the graph is complemented.]
Description []
@@ -272,12 +356,31 @@ static inline bool Dec_TreeIsComplement( Vec_Int_t * vForm ) { return Dec_NodeR
SeeAlso []
***********************************************************************/
-static inline void Dec_TreeComplement( Vec_Int_t * vForm ) { Dec_NodeReadLast(vForm)->fCompl ^= 1; }
+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 [Checks if the output node is a constant.]
+ Synopsis [Returns the number of leaves.]
Description []
@@ -286,13 +389,14 @@ static inline void Dec_TreeComplement( Vec_Int_t * vForm ) { Dec_NodeReadLas
SeeAlso []
***********************************************************************/
-static inline bool Dec_TreeIsConst( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fConst; }
-static inline bool Dec_TreeIsConst0( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fConst && Dec_NodeReadLast(vForm)->fCompl; }
-static inline bool Dec_TreeIsConst1( Vec_Int_t * vForm ) { return Dec_NodeReadLast(vForm)->fConst && !Dec_NodeReadLast(vForm)->fCompl; }
+static inline int Dec_GraphLeaveNum( Dec_Graph_t * pGraph )
+{
+ return pGraph->nLeaves;
+}
/**Function*************************************************************
- Synopsis [Creates a constant 0 decomposition tree.]
+ Synopsis [Returns the number of internal nodes.]
Description []
@@ -301,23 +405,14 @@ static inline bool Dec_TreeIsConst1( Vec_Int_t * vForm ) { return D
SeeAlso []
***********************************************************************/
-static inline Vec_Int_t * Dec_TreeCreateConst0()
+static inline int Dec_GraphNodeNum( Dec_Graph_t * pGraph )
{
- Vec_Int_t * vForm;
- Dec_Node_t * pNode;
- // create the constant node
- vForm = Vec_IntAlloc( 1 );
- Vec_IntPush( vForm, 0 );
- pNode = Dec_NodeReadLast( vForm );
- pNode->fIntern = 1;
- pNode->fConst = 1;
- pNode->fCompl = 1;
- return vForm;
+ return pGraph->nSize - pGraph->nLeaves;
}
/**Function*************************************************************
- Synopsis [Creates a constant 1 decomposition tree.]
+ Synopsis [Returns the pointer to the node.]
Description []
@@ -326,24 +421,30 @@ static inline Vec_Int_t * Dec_TreeCreateConst0()
SeeAlso []
***********************************************************************/
-static inline Vec_Int_t * Dec_TreeCreateConst1()
+static inline Dec_Node_t * Dec_GraphNode( Dec_Graph_t * pGraph, int i )
{
- Vec_Int_t * vForm;
- Dec_Node_t * pNode;
- // create the constant node
- vForm = Vec_IntAlloc( 1 );
- Vec_IntPush( vForm, 0 );
- pNode = Dec_NodeReadLast( vForm );
- pNode->fIntern = 1;
- pNode->fConst = 1;
- pNode->fCompl = 0;
- return vForm;
+ 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 [Checks if the decomposition tree is an elementary var.]
+ Synopsis [Returns the number of the given node.]
Description []
@@ -352,14 +453,14 @@ static inline Vec_Int_t * Dec_TreeCreateConst1()
SeeAlso []
***********************************************************************/
-static inline bool Dec_TreeIsVar( Vec_Int_t * vForm )
+static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
{
- return Dec_NodeReadLast(vForm)->iFanin0 == Dec_NodeReadLast(vForm)->iFanin1;
+ return pNode - pGraph->pNodes;
}
/**Function*************************************************************
- Synopsis [Creates the decomposition tree to represent an elementary var.]
+ Synopsis [Check if the graph represents elementary variable.]
Description []
@@ -368,19 +469,177 @@ static inline bool Dec_TreeIsVar( Vec_Int_t * vForm )
SeeAlso []
***********************************************************************/
-static inline Vec_Int_t * Dec_TreeCreateVar( int iVar, int nVars, int fCompl )
+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 )
{
- Vec_Int_t * vForm;
Dec_Node_t * pNode;
- // create the elementary variable node
- vForm = Vec_IntAlloc( nVars + 1 );
- Vec_IntFill( vForm, nVars + 1, 0 );
- pNode = Dec_NodeReadLast( vForm );
- pNode->iFanin0 = iVar;
- pNode->iFanin1 = iVar;
- pNode->fIntern = 1;
- pNode->fCompl = fCompl;
- return vForm;
+ // 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 )
+{
+ Dec_Edge_t eNode0, eNode1;
+ // derive the first AND
+ eEdge0.fCompl = !eEdge0.fCompl;
+ eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
+ eEdge0.fCompl = !eEdge0.fCompl;
+ // derive the second AND
+ eEdge1.fCompl = !eEdge1.fCompl;
+ eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
+ eEdge1.fCompl = !eEdge1.fCompl;
+ // derive the final OR
+ return Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
new file mode 100644
index 00000000..9931b136
--- /dev/null
+++ b/src/opt/dec/decAbc.c
@@ -0,0 +1,170 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**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_Aig_t * pMan, 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(pMan), 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( pMan, pAnd0, pAnd1 );
+ }
+ // 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(pMan) )
+ 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, 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->pManFunc, pGraph );
+ // remove the old nodes
+ Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew );
+ // compare the gains
+ nNodesNew = Abc_NtkNodeNum(pNtk);
+ assert( nGain <= nNodesOld - nNodesNew );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c
new file mode 100644
index 00000000..f6654476
--- /dev/null
+++ b/src/opt/dec/decFactor.c
@@ -0,0 +1,393 @@
+/**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 DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**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(Abc_FrameGetGlobalFrame());
+ 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(Abc_FrameGetGlobalFrame());
+ 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) );
+ Vec_IntPush( vEdgeLits, iBit );
+ }
+ // 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(Abc_FrameGetGlobalFrame());
+ 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( Abc_FrameGetGlobalFrame() );
+ 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..1d44d5cb
--- /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 DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**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..6fb20327
--- /dev/null
+++ b/src/opt/dec/decPrint.c
@@ -0,0 +1,221 @@
+/**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 DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**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_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;
+ 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 []
+
+***********************************************************************/
+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..02c3346e
--- /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 DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**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
index d6d908e7..1e0722d5 100644
--- a/src/opt/dec/module.make
+++ b/src/opt/dec/module.make
@@ -1 +1,5 @@
-SRC +=
+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
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index b9bab47f..6d1a6c06 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -63,7 +63,7 @@ struct Rwr_Man_t_
int nClasses; // the number of NN classes
// the result of resynthesis
int fCompl; // indicates if the output of FF should be complemented
- Vec_Int_t * vForm; // the decomposition tree (temporary)
+ void * pGraph; // the decomposition tree (temporary)
Vec_Ptr_t * vFanins; // the fanins array (temporary)
Vec_Ptr_t * vFaninsCur; // the fanins array (temporary)
Vec_Int_t * vLevNums; // the array of levels (temporary)
@@ -125,8 +125,7 @@ extern void Rwr_ManIncTravId( Rwr_Man_t * p );
extern Rwr_Man_t * Rwr_ManStart( bool fPrecompute );
extern void Rwr_ManStop( Rwr_Man_t * p );
extern void Rwr_ManPrintStats( Rwr_Man_t * p );
-extern Vec_Ptr_t * Rwr_ManReadFanins( Rwr_Man_t * p );
-extern Vec_Int_t * Rwr_ManReadDecs( Rwr_Man_t * p );
+extern void * Rwr_ManReadDecs( Rwr_Man_t * p );
extern int Rwr_ManReadCompl( Rwr_Man_t * p );
extern void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
extern void Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time );
diff --git a/src/opt/rwr/rwrDec.c b/src/opt/rwr/rwrDec.c
index 9cfc9659..d072879d 100644
--- a/src/opt/rwr/rwrDec.c
+++ b/src/opt/rwr/rwrDec.c
@@ -19,15 +19,14 @@
***********************************************************************/
#include "rwr.h"
-#include "ft.h"
+#include "dec.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static Vec_Int_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode );
-static int Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Vec_Int_t * vForm );
-static void Rwr_FactorVerify( Vec_Int_t * vForm, unsigned uTruth );
+static Dec_Graph_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode );
+static Dec_Edge_t Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Dec_Graph_t * pGraph );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@@ -46,6 +45,7 @@ static void Rwr_FactorVerify( Vec_Int_t * vForm, unsigned uTruth );
***********************************************************************/
void Rwr_ManPreprocess( Rwr_Man_t * p )
{
+ Dec_Graph_t * pGraph;
Rwr_Node_t * pNode;
int i, k;
// put the nodes into the structure
@@ -62,9 +62,13 @@ void Rwr_ManPreprocess( Rwr_Man_t * p )
Vec_VecPush( p->vClasses, p->pMap[pNode->uTruth], pNode );
}
}
- // compute decomposition forms for each node
+ // compute decomposition forms for each node and verify them
Vec_VecForEachEntry( p->vClasses, pNode, i, k )
- pNode->pNext = (Rwr_Node_t *)Rwr_NodePreprocess( p, pNode );
+ {
+ pGraph = Rwr_NodePreprocess( p, pNode );
+ pNode->pNext = (Rwr_Node_t *)pGraph;
+ assert( pNode->uTruth == (Dec_GraphDeriveTruth(pGraph) & 0xFFFF) );
+ }
}
/**Function*************************************************************
@@ -78,28 +82,24 @@ void Rwr_ManPreprocess( Rwr_Man_t * p )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode )
+Dec_Graph_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode )
{
- Vec_Int_t * vForm;
- int i, Root;
+ Dec_Graph_t * pGraph;
+ Dec_Edge_t eRoot;
+ assert( !Rwr_IsComplement(pNode) );
// consider constant
if ( pNode->uTruth == 0 )
- return Ft_FactorConst( 0 );
+ return Dec_GraphCreateConst0();
// consider the case of elementary var
if ( pNode->uTruth == 0x00FF )
- return Ft_FactorVar( 3, 4, 1 );
- // start the factored form
- vForm = Vec_IntAlloc( 10 );
- for ( i = 0; i < 4; i++ )
- Vec_IntPush( vForm, 0 );
+ return Dec_GraphCreateLeaf( 3, 4, 1 );
+ // start the subgraphs
+ pGraph = Dec_GraphCreate( 4 );
// collect the nodes
Rwr_ManIncTravId( p );
- Root = Rwr_TravCollect_rec( p, pNode, vForm );
- if ( Root & 1 )
- Ft_FactorComplement( vForm );
- // verify the factored form
- Rwr_FactorVerify( vForm, pNode->uTruth );
- return vForm;
+ eRoot = Rwr_TravCollect_rec( p, pNode, pGraph );
+ Dec_GraphSetRoot( pGraph, eRoot );
+ return pGraph;
}
/**Function*************************************************************
@@ -113,115 +113,31 @@ Vec_Int_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode )
SeeAlso []
***********************************************************************/
-int Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Vec_Int_t * vForm )
+Dec_Edge_t Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Dec_Graph_t * pGraph )
{
- Ft_Node_t Node, NodeA, NodeB;
- int Node0, Node1;
+ Dec_Edge_t eNode0, eNode1, eNode;
// elementary variable
if ( pNode->fUsed )
- return ((pNode->Id - 1) << 1);
+ return Dec_EdgeCreate( pNode->Id - 1, 0 );
// previously visited node
if ( pNode->TravId == p->nTravIds )
- return pNode->Volume;
+ return Dec_IntToEdge( pNode->Volume );
pNode->TravId = p->nTravIds;
// solve for children
- Node0 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p0), vForm );
- Node1 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p1), vForm );
+ eNode0 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p0), pGraph );
+ if ( Rwr_IsComplement(pNode->p0) )
+ eNode0.fCompl = !eNode0.fCompl;
+ eNode1 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p1), pGraph );
+ if ( Rwr_IsComplement(pNode->p1) )
+ eNode1.fCompl = !eNode1.fCompl;
// create the decomposition node(s)
if ( pNode->fExor )
- {
- assert( !Rwr_IsComplement(pNode->p0) );
- assert( !Rwr_IsComplement(pNode->p1) );
- NodeA.fIntern = 1;
- NodeA.fConst = 0;
- NodeA.fCompl = 0;
- NodeA.fCompl0 = !(Node0 & 1);
- NodeA.fCompl1 = (Node1 & 1);
- NodeA.iFanin0 = (Node0 >> 1);
- NodeA.iFanin1 = (Node1 >> 1);
- Vec_IntPush( vForm, Ft_Node2Int(NodeA) );
-
- NodeB.fIntern = 1;
- NodeB.fConst = 0;
- NodeB.fCompl = 0;
- NodeB.fCompl0 = (Node0 & 1);
- NodeB.fCompl1 = !(Node1 & 1);
- NodeB.iFanin0 = (Node0 >> 1);
- NodeB.iFanin1 = (Node1 >> 1);
- Vec_IntPush( vForm, Ft_Node2Int(NodeB) );
-
- Node.fIntern = 1;
- Node.fConst = 0;
- Node.fCompl = 0;
- Node.fCompl0 = 1;
- Node.fCompl1 = 1;
- Node.iFanin0 = vForm->nSize - 2;
- Node.iFanin1 = vForm->nSize - 1;
- Vec_IntPush( vForm, Ft_Node2Int(Node) );
- }
+ eNode = Dec_GraphAddNodeXor( pGraph, eNode0, eNode1 );
else
- {
- Node.fIntern = 1;
- Node.fConst = 0;
- Node.fCompl = 0;
- Node.fCompl0 = Rwr_IsComplement(pNode->p0) ^ (Node0 & 1);
- Node.fCompl1 = Rwr_IsComplement(pNode->p1) ^ (Node1 & 1);
- Node.iFanin0 = (Node0 >> 1);
- Node.iFanin1 = (Node1 >> 1);
- Vec_IntPush( vForm, Ft_Node2Int(Node) );
- }
- // save the number of this node
- pNode->Volume = ((vForm->nSize - 1) << 1) | pNode->fExor;
- return pNode->Volume;
-}
-
-/**Function*************************************************************
-
- Synopsis [Verifies the factored form.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Rwr_FactorVerify( Vec_Int_t * vForm, unsigned uTruthGold )
-{
- Ft_Node_t * pFtNode;
- Vec_Int_t * vTruths;
- unsigned uTruth, uTruth0, uTruth1;
- int i;
-
- vTruths = Vec_IntAlloc( vForm->nSize );
- Vec_IntPush( vTruths, 0xAAAA );
- Vec_IntPush( vTruths, 0xCCCC );
- Vec_IntPush( vTruths, 0xF0F0 );
- Vec_IntPush( vTruths, 0xFF00 );
-
- assert( Ft_FactorGetNumVars( vForm ) == 4 );
- for ( i = 4; i < vForm->nSize; i++ )
- {
- pFtNode = Ft_NodeRead( vForm, i );
- // make sure there are no elementary variables
- assert( pFtNode->iFanin0 != pFtNode->iFanin1 );
-
- uTruth0 = vTruths->pArray[pFtNode->iFanin0];
- uTruth0 = pFtNode->fCompl0? ~uTruth0 : uTruth0;
-
- uTruth1 = vTruths->pArray[pFtNode->iFanin1];
- uTruth1 = pFtNode->fCompl1? ~uTruth1 : uTruth1;
-
- uTruth = uTruth0 & uTruth1;
- Vec_IntPush( vTruths, uTruth );
- }
- // complement if necessary
- if ( pFtNode->fCompl )
- uTruth = ~uTruth;
- uTruth &= 0xFFFF;
- if ( uTruth != uTruthGold )
- printf( "Verification failed\n" );
- Vec_IntFree( vTruths );
+ eNode = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
+ // save the result
+ pNode->Volume = Dec_EdgeToInt( eNode );
+ return eNode;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index 735232af..c934dfd8 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -19,13 +19,13 @@
***********************************************************************/
#include "rwr.h"
-#include "ft.h"
+#include "dec.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest );
+static Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@@ -40,8 +40,8 @@ static Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t
structures precomputed and stored in the RWR manager.
Determines the best rewriting and computes the gain in the number of AIG
nodes in the final network. In the end, p->vFanins contains information
- about the best cut that can be used for rewriting, while p->vForm gives
- the decomposition tree (represented using factored form data structure).
+ about the best cut that can be used for rewriting, while p->pGraph gives
+ the decomposition dag (represented using decomposition graph data structure).
Returns gain in the number of nodes or -1 if node cannot be rewritten.]
SideEffects []
@@ -52,14 +52,14 @@ static Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t
int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros )
{
int fVeryVerbose = 0;
- Vec_Int_t * vForm;
+ Dec_Graph_t * pGraph;
Cut_Cut_t * pCut;
Abc_Obj_t * pFanin;
unsigned uPhase, uTruthBest;
char * pPerm;
int Required, nNodesSaved;
int i, GainCur, GainBest = -1;
- int clk;
+ int clk, clk2;
p->nNodesConsidered++;
// get the required times
@@ -109,14 +109,16 @@ clk = clock();
Abc_ObjRegular(pFanin)->vFanouts.nSize--;
// evaluate the cut
- vForm = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur );
+clk2 = clock();
+ pGraph = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur );
+p->timeEval += clock() - clk2;
// check if the cut is better than the current best one
- if ( vForm != NULL && GainBest < GainCur )
+ if ( pGraph != NULL && GainBest < GainCur )
{
// save this form
GainBest = GainCur;
- p->vForm = vForm;
+ p->pGraph = pGraph;
p->fCompl = ((uPhase & (1<<4)) > 0);
uTruthBest = pCut->uTruth;
// collect fanins in the
@@ -127,8 +129,12 @@ clk = clock();
}
p->timeRes += clock() - clk;
- if ( GainBest == -1 || GainBest == 0 && !fUseZeros )
- return GainBest;
+ if ( GainBest == -1 )
+ return -1;
+
+ // copy the leaves
+ Vec_PtrForEachEntry( p->vFanins, pFanin, i )
+ Dec_GraphNode(p->pGraph, i)->pFunc = pFanin;
p->nScores[p->pMap[uTruthBest]]++;
p->nNodesRewritten++;
@@ -139,7 +145,7 @@ p->timeRes += clock() - clk;
{
printf( "Node %6s : ", Abc_ObjName(pNode) );
printf( "Fanins = %d. ", p->vFanins->nSize );
- printf( "Cone = %2d. ", p->vForm->nSize - 4 );
+ printf( "Cone = %2d. ", Dec_GraphNodeNum(p->pGraph) );
printf( "GAIN = %2d. ", GainBest );
printf( "\n" );
}
@@ -157,37 +163,40 @@ p->timeRes += clock() - clk;
SeeAlso []
***********************************************************************/
-Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest )
+Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest )
{
Vec_Ptr_t * vSubgraphs;
- Vec_Int_t * vFormBest;
- Rwr_Node_t * pNode;
- int nNodesAdded, GainBest = -1, i;
- int clk = clock();
+ Dec_Graph_t * pGraphBest, * pGraphCur;
+ Rwr_Node_t * pNode, * pFanin;
+ int nNodesAdded, GainBest, i, k;
// find the matching class of subgraphs
vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[pCut->uTruth] );
p->nSubgraphs += vSubgraphs->nSize;
// determine the best subgraph
+ GainBest = -1;
Vec_PtrForEachEntry( vSubgraphs, pNode, i )
{
+ // get the current graph
+ pGraphCur = (Dec_Graph_t *)pNode->pNext;
+ // copy the leaves
+ Vec_PtrForEachEntry( vFaninsCur, pFanin, k )
+ Dec_GraphNode(pGraphCur, k)->pFunc = pFanin;
// detect how many unlabeled nodes will be reused
- nNodesAdded = Abc_NodeStrashDecCount( pRoot->pNtk->pManFunc, pRoot, vFaninsCur,
- (Vec_Int_t *)pNode->pNext, p->vLevNums, nNodesSaved, LevelMax );
+ nNodesAdded = Dec_GraphToNetworkCount( pRoot, pGraphCur, nNodesSaved, LevelMax );
if ( nNodesAdded == -1 )
continue;
assert( nNodesSaved >= nNodesAdded );
// count the gain at this node
if ( GainBest < nNodesSaved - nNodesAdded )
{
- GainBest = nNodesSaved - nNodesAdded;
- vFormBest = (Vec_Int_t *)pNode->pNext;
+ GainBest = nNodesSaved - nNodesAdded;
+ pGraphBest = pGraphCur;
}
}
-p->timeEval += clock() - clk;
if ( GainBest == -1 )
return NULL;
*pGainBest = GainBest;
- return vFormBest;
+ return pGraphBest;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index d4772812..e7d6fec6 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -19,6 +19,8 @@
***********************************************************************/
#include "rwr.h"
+#include "main.h"
+#include "dec.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -41,15 +43,18 @@
***********************************************************************/
Rwr_Man_t * Rwr_ManStart( bool fPrecompute )
{
+ Dec_Man_t * pManDec;
Rwr_Man_t * p;
int clk = clock();
+clk = clock();
p = ALLOC( Rwr_Man_t, 1 );
memset( p, 0, sizeof(Rwr_Man_t) );
p->nFuncs = (1<<16);
- // canonical forms, phases, perms
-clk = clock();
- Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
-//PRT( "NPN classes precomputation time", clock() - clk );
+ pManDec = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
+ p->puCanons = pManDec->puCanons;
+ p->pPhases = pManDec->pPhases;
+ p->pPerms = pManDec->pPerms;
+ p->pMap = pManDec->pMap;
// initialize practical NPN classes
p->pPractical = Rwr_ManGetPractical( p );
// create the table
@@ -104,7 +109,7 @@ void Rwr_ManStop( Rwr_Man_t * p )
Rwr_Node_t * pNode;
int i, k;
Vec_VecForEachEntry( p->vClasses, pNode, i, k )
- Vec_IntFree( (Vec_Int_t *)pNode->pNext );
+ Dec_GraphFree( (Dec_Graph_t *)pNode->pNext );
}
if ( p->vClasses ) Vec_VecFree( p->vClasses );
Vec_PtrFree( p->vForest );
@@ -115,10 +120,6 @@ void Rwr_ManStop( Rwr_Man_t * p )
free( p->pTable );
free( p->pPractical );
free( p->pPerms4 );
- free( p->puCanons );
- free( p->pPhases );
- free( p->pPerms );
- free( p->pMap );
free( p );
}
@@ -173,25 +174,9 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
SeeAlso []
***********************************************************************/
-Vec_Ptr_t * Rwr_ManReadFanins( Rwr_Man_t * p )
-{
- return p->vFanins;
-}
-
-/**Function*************************************************************
-
- Synopsis [Stops the resynthesis manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Int_t * Rwr_ManReadDecs( Rwr_Man_t * p )
+void * Rwr_ManReadDecs( Rwr_Man_t * p )
{
- return p->vForm;
+ return p->pGraph;
}
/**Function*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 01:08:51 +0000