summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/cut/cut.h5
-rw-r--r--src/opt/cut/cutNode.c184
-rw-r--r--src/opt/cut/cutTruth.c42
-rw-r--r--src/opt/dec/dec.h1
-rw-r--r--src/opt/dec/decAbc.c38
-rw-r--r--src/opt/fxu/fxuCreate.c16
6 files changed, 278 insertions, 8 deletions
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index f518e8c4..5c9b2e8e 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -69,6 +69,8 @@ struct Cut_CutStruct_t_
unsigned nVarsMax : 4; // the max number of vars [4-6]
unsigned nLeaves : 4; // the number of leaves [4-6]
unsigned uSign; // the signature
+ unsigned uCanon0; // the canonical form
+ unsigned uCanon1; // the canonical form
Cut_Cut_t * pNext; // the next cut in the list
int pLeaves[0]; // the array of leaves
};
@@ -113,6 +115,7 @@ extern int Cut_ManReadVarsMax( Cut_Man_t * p );
/*=== cutNode.c ==========================================================*/
extern Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv );
extern Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes );
+extern Cut_Cut_t * Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetNum, int fFirst );
/*=== cutSeq.c ==========================================================*/
extern void Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int nLat0, int nLat1, int fTriv, int CutSetNum );
extern void Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node );
@@ -126,6 +129,8 @@ extern int Cut_OracleReadDrop( Cut_Oracle_t * p );
extern void Cut_OracleNodeSetTriv( Cut_Oracle_t * p, int Node );
extern Cut_Cut_t * Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 );
extern void Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node );
+/*=== cutTruth.c ==========================================================*/
+extern void Cut_TruthCanonicize( Cut_Cut_t * pCut );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 80568d71..0268ba19 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -376,6 +376,7 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
// start with the elementary cut
if ( fTriv )
{
+// printf( "Creating trivial cut %d.\n", Node );
pTemp0 = Cut_CutCreateTriv( p, Node );
Cut_ListAdd( pSuper, pTemp0 );
p->nNodeCuts++;
@@ -542,6 +543,189 @@ p->timeUnion += clock() - clk;
return pList;
}
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts by unioning cuts at a choice node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetNum, int fFirst )
+{
+ Cut_List_t Super, * pSuper = &Super;
+ Cut_Cut_t * pList, * pListStart, * pCut, * pCut2, * pTop;
+ int i, k, Node, Root, Limit = p->pParams->nVarsMax;
+ int clk = clock();
+
+ // start the new list
+ Cut_ListStart( pSuper );
+
+ // remember the root node to save the resulting cuts
+ Root = Vec_IntEntry( vNodes, 0 );
+ p->nNodeCuts = 1;
+
+ // store the original lists for comparison
+ p->pCompareOld = Cut_NodeReadCutsOld( p, Root );
+ p->pCompareNew = (CutSetNum >= 0)? Cut_NodeReadCutsNew( p, Root ) : NULL;
+
+ // get the topmost cut
+ pTop = NULL;
+ if ( (pTop = Cut_NodeReadCutsOld( p, Root )) == NULL )
+ pTop = Cut_NodeReadCutsNew( p, Root );
+ assert( pTop != NULL );
+
+ // collect small cuts first
+ Vec_PtrClear( p->vTemp );
+ Vec_IntForEachEntry( vNodes, Node, i )
+ {
+ // get the cuts of this node
+ if ( i == 0 && CutSetNum >= 0 )
+ {
+ pList = Cut_NodeReadCutsTemp( p, CutSetNum );
+ Cut_NodeWriteCutsTemp( p, CutSetNum, NULL );
+ }
+ else
+ {
+ pList = Cut_NodeReadCutsNew( p, Node );
+ Cut_NodeWriteCutsNew( p, Node, NULL );
+ }
+ if ( pList == NULL )
+ continue;
+
+ // process the cuts
+ if ( fFirst )
+ {
+ // remember the starting point
+ pListStart = pList->pNext;
+ pList->pNext = NULL;
+ // save or recycle the elementary cut
+ if ( i == 0 )
+ Cut_ListAdd( pSuper, pList );
+ else
+ Cut_CutRecycle( p, pList );
+ }
+ else
+ pListStart = pList;
+
+ // save all the cuts that are smaller than the limit
+ Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
+ {
+ if ( pCut->nLeaves == (unsigned)Limit )
+ {
+ Vec_PtrPush( p->vTemp, pCut );
+ break;
+ }
+ // check containment
+// if ( p->pParams->fFilter && Cut_CutFilterOne( p, pSuper, pCut ) )
+// continue;
+ if ( p->pParams->fFilter )
+ {
+ if ( Cut_CutFilterOne(p, pSuper, pCut) )
+ continue;
+ if ( p->pParams->fSeq )
+ {
+ if ( p->pCompareOld && Cut_CutFilterOld(p, p->pCompareOld, pCut) )
+ continue;
+ if ( p->pCompareNew && Cut_CutFilterOld(p, p->pCompareNew, pCut) )
+ continue;
+ }
+ }
+
+ // set the complemented bit by comparing the first cut with the current cut
+ pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+ pListStart = pCut->pNext;
+ pCut->pNext = NULL;
+ // add to the list
+ Cut_ListAdd( pSuper, pCut );
+ if ( ++p->nNodeCuts == p->pParams->nKeepMax )
+ {
+ // recycle the rest of the cuts of this node
+ Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
+ Cut_CutRecycle( p, pCut );
+ // recycle all cuts of other nodes
+ Vec_IntForEachEntryStart( vNodes, Node, k, i+1 )
+ Cut_NodeFreeCuts( p, Node );
+ // recycle the saved cuts of other nodes
+ Vec_PtrForEachEntry( p->vTemp, pList, k )
+ Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+ Cut_CutRecycle( p, pCut );
+ goto finish;
+ }
+ }
+ }
+ // collect larger cuts next
+ Vec_PtrForEachEntry( p->vTemp, pList, i )
+ {
+ Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+ {
+ // check containment
+// if ( p->pParams->fFilter && Cut_CutFilterOne( p, pSuper, pCut ) )
+// continue;
+ if ( p->pParams->fFilter )
+ {
+ if ( Cut_CutFilterOne(p, pSuper, pCut) )
+ continue;
+ if ( p->pParams->fSeq )
+ {
+ if ( p->pCompareOld && Cut_CutFilterOld(p, p->pCompareOld, pCut) )
+ continue;
+ if ( p->pCompareNew && Cut_CutFilterOld(p, p->pCompareNew, pCut) )
+ continue;
+ }
+ }
+
+ // set the complemented bit
+ pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+ pListStart = pCut->pNext;
+ pCut->pNext = NULL;
+ // add to the list
+ Cut_ListAdd( pSuper, pCut );
+ if ( ++p->nNodeCuts == p->pParams->nKeepMax )
+ {
+ // recycle the rest of the cuts
+ Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
+ Cut_CutRecycle( p, pCut );
+ // recycle the saved cuts of other nodes
+ Vec_PtrForEachEntryStart( p->vTemp, pList, k, i+1 )
+ Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+ Cut_CutRecycle( p, pCut );
+ goto finish;
+ }
+ }
+ }
+finish :
+ // set the cuts at the node
+ pList = Cut_ListFinish( pSuper );
+
+ // set the lists at the node
+// assert( Cut_NodeReadCutsNew(p, Root) == NULL );
+// Cut_NodeWriteCutsNew( p, Root, pList );
+ if ( CutSetNum >= 0 )
+ {
+ assert( Cut_NodeReadCutsTemp(p, CutSetNum) == NULL );
+ Cut_NodeWriteCutsTemp( p, CutSetNum, pList );
+ }
+ else
+ {
+ assert( Cut_NodeReadCutsNew(p, Root) == NULL );
+ Cut_NodeWriteCutsNew( p, Root, pList );
+ }
+
+p->timeUnion += clock() - clk;
+ // filter the cuts
+//clk = clock();
+// if ( p->pParams->fFilter )
+// Cut_CutFilter( p, pList );
+//p->timeFilter += clock() - clk;
+// if ( fFirst )
+// p->nNodes -= vNodes->nSize - 1;
+ return pList;
+}
+
/**Function*************************************************************
diff --git a/src/opt/cut/cutTruth.c b/src/opt/cut/cutTruth.c
index 28984e5a..b65e5eff 100644
--- a/src/opt/cut/cutTruth.c
+++ b/src/opt/cut/cutTruth.c
@@ -107,6 +107,48 @@ void Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, i
}
}
+/**Function*************************************************************
+
+ Synopsis [Performs truth table computation.]
+
+ Description [This procedure cannot be used while recording oracle
+ because it will overwrite Num0 and Num1.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_TruthCanonicize( Cut_Cut_t * pCut )
+{
+ unsigned uTruth;
+ unsigned * uCanon2;
+ char * pPhases2;
+ assert( pCut->nVarsMax < 6 );
+
+ // get the direct truth table
+ uTruth = *Cut_CutReadTruth(pCut);
+
+ // compute the direct truth table
+ Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
+// uCanon[0] = uCanon2[0];
+// uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
+// uPhases[0] = pPhases2[0];
+ pCut->uCanon0 = uCanon2[0];
+ pCut->Num0 = pPhases2[0];
+
+ // get the complemented truth table
+ uTruth = ~*Cut_CutReadTruth(pCut);
+
+ // compute the direct truth table
+ Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
+// uCanon[0] = uCanon2[0];
+// uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
+// uPhases[0] = pPhases2[0];
+ pCut->uCanon1 = uCanon2[0];
+ pCut->Num1 = pPhases2[0];
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
index aa2a7039..b6b2524b 100644
--- a/src/opt/dec/dec.h
+++ b/src/opt/dec/dec.h
@@ -96,6 +96,7 @@ struct Dec_Man_t_
/*=== 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 ========================================================*/
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index 6782a02f..1416cf0d 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -63,6 +63,44 @@ Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * 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_NtkConst1(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
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index 24b86c95..02b7605c 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -24,11 +24,11 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_t * vFanins, int * pOrder );
+static void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder );
static int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY );
static void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext );
static Fxu_Cube * Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode );
-static Abc_Fan_t * s_pLits;
+static int * s_pLits;
extern int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
@@ -53,7 +53,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
Fxu_Var * pVar;
Fxu_Cube * pCubeFirst, * pCubeNew;
Fxu_Cube * pCube1, * pCube2;
- Vec_Fan_t * vFanins;
+ Vec_Int_t * vFanins;
char * pSopCover;
char * pSopCube;
int * pOrder, nBitsMax;
@@ -151,7 +151,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
pOrder[v] = v;
// reorder the fanins
qsort( (void *)pOrder, nFanins, sizeof(int),(int (*)(const void *, const void *))Fxu_CreateMatrixLitCompare);
- assert( s_pLits[ pOrder[0] ].iFan < s_pLits[ pOrder[nFanins-1] ].iFan );
+ assert( s_pLits[ pOrder[0] ] < s_pLits[ pOrder[nFanins-1] ] );
// create the corresponding cubes in the matrix
pCubeFirst = NULL;
c = 0;
@@ -214,7 +214,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
SeeAlso []
***********************************************************************/
-void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_t * vFanins, int * pOrder )
+void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder )
{
Fxu_Var * pVar;
int Value, i;
@@ -224,12 +224,12 @@ void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube,
Value = pSopCube[pOrder[i]];
if ( Value == '0' )
{
- pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]].iFan + 1 ]; // CST
+ pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] + 1 ]; // CST
Fxu_MatrixAddLiteral( p, pCube, pVar );
}
else if ( Value == '1' )
{
- pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]].iFan ]; // CST
+ pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] ]; // CST
Fxu_MatrixAddLiteral( p, pCube, pVar );
}
}
@@ -409,7 +409,7 @@ Fxu_Cube * Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iV
***********************************************************************/
int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY )
{
- return s_pLits[*ptrX].iFan - s_pLits[*ptrY].iFan;
+ return s_pLits[*ptrX] - s_pLits[*ptrY];
}
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-10 11:19:09 +0000