From 8e5398c501a873dffcb562a11bc19e630872c931 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 5 Mar 2006 08:01:00 -0800 Subject: Version abc60305 --- abc.rc | 42 +- src/base/abc/abcRefs.c | 38 +- src/base/abci/abc.c | 123 +++- src/base/abci/abcReconv.c | 2 +- src/base/abci/abcResub.c | 1634 +++++++++++++++++++++++++++++++++++++-------- src/base/abci/abcVerify.c | 18 +- 6 files changed, 1564 insertions(+), 293 deletions(-) diff --git a/abc.rc b/abc.rc index 1be23c42..68a2a5a5 100644 --- a/abc.rc +++ b/abc.rc @@ -50,8 +50,10 @@ alias rw rewrite alias rwz rewrite -z alias rf refactor alias rfz refactor -z -alias rs restructure -alias rsz restructure -z +alias re restructure +alias rez restructure -z +alias rs resub +alias rsz resub -z alias sa set autoexec ps alias so source -x alias st strash @@ -65,19 +67,27 @@ alias wp write_pla alias wv write_verilog # standard scripts -alias opt "b; ren; b" -alias share "b; ren; fx; b" -alias sharem "b; ren -m; fx; b" -alias sharedsd "b; ren; dsd -g; sw; fx; b" -alias resyn "b; rw; rwz; b; rwz; b" -alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" -alias resyn3 "b; rs; rs -K 6; b; rsz; rsz -K 6; b; rsz -K 5; b" -alias compress "b -l; rw -l; rwz -l; b -l; rwz -l; b -l" -alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" -alias choice "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore" -alias choice2 "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore" -alias rwsat "st; rw -l; b -l; rw -l; rf -l" -alias rwsat2 "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l" -alias shake "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000" +alias opt "b; ren; b" +alias share "b; ren; fx; b" +alias sharem "b; ren -m; fx; b" +alias sharedsd "b; ren; dsd -g; sw; fx; b" +alias resyn "b; rw; rwz; b; rwz; b" +alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" +alias resyn3 "b; rs; rs -K 6; b; rsz; rsz -K 6; b; rsz -K 5; b" +alias compress "b -l; rw -l; rwz -l; b -l; rwz -l; b -l" +alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" +alias choice "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore" +alias choice2 "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore" +alias rwsat "st; rw -l; b -l; rw -l; rf -l" +alias rwsat2 "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l" +alias shake "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000" + +# resubstitution scripts for the IWLS paper +alias src_rw "st; rw -l; rwz -l; rwz -l" +alias src_rs1 "st; rs -K 6 -l; rs -K 9 -l; rs -K 12 -l" +alias src_rs2 "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l" +alias src_rws1 "st; rw -l; rs -K 6 -l; rwz -l; rs -K 9 -l; rwz -l; rs -K 12 -l" +alias src_rws2 "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" +alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c index 808bfae8..91f37e8f 100644 --- a/src/base/abc/abcRefs.c +++ b/src/base/abc/abcRefs.c @@ -271,14 +271,14 @@ void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * // add to the new support nodes if ( !fTopmost && (Abc_ObjIsCi(pNode) || pNode->vFanouts.nSize > 0) ) { - Vec_PtrPush( vSupp, pNode ); + if ( vSupp ) Vec_PtrPush( vSupp, pNode ); return; } // recur on the children Abc_ObjForEachFanin( pNode, pFanin, i ) Abc_NodeMffsConeSupp_rec( pFanin, vCone, vSupp, 0 ); // collect the internal node - Vec_PtrPush( vCone, pNode ); + if ( vCone ) Vec_PtrPush( vCone, pNode ); } /**Function************************************************************* @@ -296,8 +296,8 @@ void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSu { assert( Abc_ObjIsNode(pNode) ); assert( !Abc_ObjIsComplement(pNode) ); - Vec_PtrClear( vCone ); - Vec_PtrClear( vSupp ); + if ( vCone ) Vec_PtrClear( vCone ); + if ( vSupp ) Vec_PtrClear( vSupp ); Abc_NtkIncrementTravId( pNode->pNtk ); Abc_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 ); } @@ -326,6 +326,36 @@ void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode ) Vec_PtrFree( vSupp ); } +/**Function************************************************************* + + Synopsis [Collects the internal nodes of the MFFC limited by cut.] + + Description [] + + SideEffects [Increments the trav ID and marks visited nodes.] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside ) +{ + Abc_Obj_t * pObj; + int i, Count1, Count2; + // increment the fanout counters for the leaves + Vec_PtrForEachEntry( vLeaves, pObj, i ) + pObj->vFanouts.nSize++; + // dereference the node + Count1 = Abc_NodeDeref_rec( pNode ); + // collect the nodes inside the MFFC + Abc_NodeMffsConeSupp( pNode, vInside, NULL ); + // reference it back + Count2 = Abc_NodeRef_rec( pNode ); + assert( Count1 == Count2 ); + // remove the extra counters + Vec_PtrForEachEntry( vLeaves, pObj, i ) + pObj->vFanouts.nSize--; + return Count1; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8927279f..ffab5116 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -63,6 +63,7 @@ static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRestructure ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -165,6 +166,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "restructure", Abc_CommandRestructure, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "resub", Abc_CommandResubstitute, 1 ); // Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 ); Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 ); @@ -2574,7 +2576,7 @@ int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'K': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" ); goto usage; } nCutMax = atoi(argv[globalUtilOptind]); @@ -2638,6 +2640,125 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int RS_CUT_MIN = 4; + int RS_CUT_MAX = 16; + int c; + int nCutMax; + int nNodesMax; + bool fUpdateLevel; + bool fUseZeros; + bool fVerbose; + extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nNodesMax, bool fUpdateLevel, bool fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nCutMax = 8; + nNodesMax = 1; + fUpdateLevel = 1; + fUseZeros = 0; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "KNlzvh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nCutMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCutMax < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nNodesMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nNodesMax < 0 ) + goto usage; + break; + case 'l': + fUpdateLevel ^= 1; + break; + case 'z': + fUseZeros ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( nCutMax < RS_CUT_MIN || nCutMax > RS_CUT_MAX ) + { + fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", RS_CUT_MIN, RS_CUT_MAX ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command can only be applied to an AIG (run \"strash\").\n" ); + return 1; + } + if ( Abc_NtkGetChoiceNum(pNtk) ) + { + fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" ); + return 1; + } + + // modify the current network + if ( !Abc_NtkResubstitute( pNtk, nCutMax, nNodesMax, fUpdateLevel, fVerbose ) ) + { + fprintf( pErr, "Refactoring has failed.\n" ); + return 1; + } + return 0; + +usage: + fprintf( pErr, "usage: resub [-K num] [-N num] [-lzvh]\n" ); + fprintf( pErr, "\t performs technology-independent restructuring of the AIG\n" ); + fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n", RS_CUT_MIN, RS_CUT_MAX, nCutMax ); + fprintf( pErr, "\t-N num : the max number of nodes to add [default = %d]\n", nNodesMax ); + fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); + fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c index 100551c7..e5b9e024 100644 --- a/src/base/abci/abcReconv.c +++ b/src/base/abci/abcReconv.c @@ -587,7 +587,7 @@ Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNode p->vConeLeaves = Vec_PtrAlloc( 100 ); p->vVisited = Vec_PtrAlloc( 100 ); p->vLevels = Vec_VecAlloc( 100 ); - p->vNodesTfo = Vec_PtrAlloc( 100 ); + p->vNodesTfo = Vec_PtrAlloc( 100 ); p->nNodeSizeMax = nNodeSizeMax; p->nConeSizeMax = nConeSizeMax; p->nNodeFanStop = nNodeFanStop; diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index 30e2eca2..71a4466f 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -25,8 +25,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -typedef struct Abc_ResubMan_t_ Abc_ResubMan_t; -struct Abc_ResubMan_t_ +typedef struct Abc_ManRes_t_ Abc_ManRes_t; +struct Abc_ManRes_t_ { // paramers int nLeavesMax; // the max number of leaves in the cone @@ -36,6 +36,7 @@ struct Abc_ResubMan_t_ int nLeaves; // the number of leaves int nDivs; // the number of all divisor (including leaves) int nMffc; // the size of MFFC + int nLastGain; // the gain the number of nodes Vec_Ptr_t * vDivs; // the divisors // representation of the simulation info int nBits; // the number of simulation bits @@ -43,36 +44,189 @@ struct Abc_ResubMan_t_ Vec_Ptr_t * vSims; // simulation info unsigned * pInfo; // pointer to simulation info // internal divisor storage - Vec_Ptr_t * vDivs1U; // the single-node unate divisors + Vec_Ptr_t * vDivs1UP; // the single-node unate divisors + Vec_Ptr_t * vDivs1UN; // the single-node unate divisors Vec_Ptr_t * vDivs1B; // the single-node binate divisors - Vec_Ptr_t * vDivs2U0; // the double-node unate divisors - Vec_Ptr_t * vDivs2U1; // the double-node unate divisors + Vec_Ptr_t * vDivs2UP0; // the double-node unate divisors + Vec_Ptr_t * vDivs2UP1; // the double-node unate divisors + Vec_Ptr_t * vDivs2UN0; // the double-node unate divisors + Vec_Ptr_t * vDivs2UN1; // the double-node unate divisors // other data Vec_Ptr_t * vTemp; // temporary array of nodes + // runtime statistics + int timeCut; + int timeRes; + int timeDiv; + int timeMffc; + int timeSim; + int timeRes1; + int timeResD; + int timeRes2; + int timeRes3; + int timeNtk; + int timeTotal; + // improvement statistics + int nUsedNodeC; + int nUsedNode0; + int nUsedNode1Or; + int nUsedNode1And; + int nUsedNode2Or; + int nUsedNode2And; + int nUsedNode2OrAnd; + int nUsedNode2AndOr; + int nUsedNode3OrAnd; + int nUsedNode3AndOr; + int nUsedNodeTotal; + int nTotalDivs; + int nTotalLeaves; }; - // external procedures -extern Abc_ResubMan_t * Abc_ResubManStart( int nLeavesMax, int nDivsMax ); -extern void Abc_ResubManStop( Abc_ResubMan_t * p ); -extern Dec_Graph_t * Abc_ResubManEval( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps ); - - -static int Abc_ResubManCollectDivs( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves ); -static int Abc_ResubManMffc( Abc_ResubMan_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves ); -static void Abc_ResubManSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords ); - -static Dec_Graph_t * Abc_ResubManQuit( Abc_ResubMan_t * p ); -static Dec_Graph_t * Abc_ResubManDivs0( Abc_ResubMan_t * p ); -static Dec_Graph_t * Abc_ResubManDivs1( Abc_ResubMan_t * p ); -static Dec_Graph_t * Abc_ResubManDivsD( Abc_ResubMan_t * p ); -static Dec_Graph_t * Abc_ResubManDivs2( Abc_ResubMan_t * p ); -static Dec_Graph_t * Abc_ResubManDivs3( Abc_ResubMan_t * p ); +static Abc_ManRes_t* Abc_ManResubStart( int nLeavesMax, int nDivsMax ); +static void Abc_ManResubStop( Abc_ManRes_t * p ); +static Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps, bool fUpdateLevel, int fVerbose ); +static void Abc_ManResubCleanup( Abc_ManRes_t * p ); +static void Abc_ManResubPrint( Abc_ManRes_t * p ); + +// other procedures +static int Abc_ManResubCollectDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int Required ); +static int Abc_ManResubMffc( Abc_ManRes_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves ); +static void Abc_ManResubSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords ); + +static void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required ); +static void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ); +static Dec_Graph_t * Abc_ManResubQuit( Abc_ManRes_t * p ); +static Dec_Graph_t * Abc_ManResubDivs0( Abc_ManRes_t * p ); +static Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required ); +static Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required ); +static Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required ); +static Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required ); + +static Vec_Ptr_t * Abc_CutFactorLarge( Abc_Obj_t * pNode, int nLeavesMax ); +static int Abc_CutVolumeCheck( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Performs incremental resynthesis of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpdateLevel, bool fVerbose ) +{ + ProgressBar * pProgress; + Abc_ManRes_t * pManRes; + Abc_ManCut_t * pManCut; + Dec_Graph_t * pFForm; + Vec_Ptr_t * vLeaves; + Abc_Obj_t * pNode; + int clk, clkStart = clock(); + int i, nNodes; + + assert( Abc_NtkIsStrash(pNtk) ); + + // cleanup the AIG + Abc_AigCleanup(pNtk->pManFunc); + // start the managers + pManCut = Abc_NtkManCutStart( nCutMax, 10000, 100000, 100000 ); + pManRes = Abc_ManResubStart( nCutMax, 200 ); + + // compute the reverse levels if level update is requested + if ( fUpdateLevel ) + Abc_NtkStartReverseLevels( pNtk ); + + // resynthesize each node once + nNodes = Abc_NtkObjNumMax(pNtk); + pProgress = Extra_ProgressBarStart( stdout, nNodes ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // skip the constant node + if ( Abc_NodeIsConst(pNode) ) + continue; + // skip the nodes with many fanouts + if ( Abc_ObjFanoutNum(pNode) > 1000 ) + continue; + // stop if all nodes have been tried once + if ( i >= nNodes ) + break; + + // compute a reconvergence-driven cut +clk = clock(); + vLeaves = Abc_NodeFindCut( pManCut, pNode, 0 ); +// vLeaves = Abc_CutFactorLarge( pNode, nCutMax ); +pManRes->timeCut += clock() - clk; +/* + if ( fVerbose && vLeaves ) + printf( "Node %6d : Leaves = %3d. Volume = %3d.\n", pNode->Id, Vec_PtrSize(vLeaves), Abc_CutVolumeCheck(pNode, vLeaves) ); + if ( vLeaves == NULL ) + continue; +*/ + + // evaluate this cut +clk = clock(); + pFForm = Abc_ManResubEval( pManRes, pNode, vLeaves, nStepsMax, fUpdateLevel, fVerbose ); +// Vec_PtrFree( vLeaves ); +// Abc_ManResubCleanup( pManRes ); +pManRes->timeRes += clock() - clk; + if ( pFForm == NULL ) + continue; +/* + if ( pNode->Id % 25 == 0 ) + printf( "%6d : L = %2d. V = %2d. Mffc = %2d. Divs = %3d. Up = %3d. Un = %3d. B = %3d.\n", + pNode->Id, pManRes->nLeaves, Abc_CutVolumeCheck(pNode, vLeaves), pManRes->nMffc, pManRes->nDivs, + pManRes->vDivs1UP->nSize, pManRes->vDivs1UN->nSize, pManRes->vDivs1B->nSize ); +*/ + + // acceptable replacement found, update the graph +clk = clock(); + Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRes->nLastGain ); +pManRes->timeNtk += clock() - clk; + Dec_GraphFree( pFForm ); + } + Extra_ProgressBarStop( pProgress ); +pManRes->timeTotal = clock() - clkStart; + + // print statistics + if ( fVerbose ) + Abc_ManResubPrint( pManRes ); + + // delete the managers + Abc_ManResubStop( pManRes ); + Abc_NtkManCutStop( pManCut ); + + // clean the data field + Abc_NtkForEachObj( pNtk, pNode, i ) + pNode->pData = NULL; + + // put the nodes into the DFS order and reassign their IDs + Abc_NtkReassignIds( pNtk ); +// Abc_AigCheckFaninOrder( pNtk->pManFunc ); + // fix the levels + if ( fUpdateLevel ) + Abc_NtkStopReverseLevels( pNtk ); + else + Abc_NtkGetLevelNum( pNtk ); + // check + if ( !Abc_NtkCheck( pNtk ) ) + { + printf( "Abc_NtkRefactor: The network check has failed.\n" ); + return 0; + } + return 1; +} + + + + /**Function************************************************************* Synopsis [] @@ -84,19 +238,20 @@ static Dec_Graph_t * Abc_ResubManDivs3( Abc_ResubMan_t * p ); SeeAlso [] ***********************************************************************/ -Abc_ResubMan_t * Abc_ResubManStart( int nLeavesMax, int nDivsMax ) +Abc_ManRes_t * Abc_ManResubStart( int nLeavesMax, int nDivsMax ) { - Abc_ResubMan_t * p; + Abc_ManRes_t * p; unsigned * pData; int i, k; - p = ALLOC( Abc_ResubMan_t, 1 ); - memset( p, 0, sizeof(Abc_ResubMan_t) ); + assert( sizeof(unsigned) == 4 ); + p = ALLOC( Abc_ManRes_t, 1 ); + memset( p, 0, sizeof(Abc_ManRes_t) ); p->nLeavesMax = nLeavesMax; p->nDivsMax = nDivsMax; p->vDivs = Vec_PtrAlloc( p->nDivsMax ); // allocate simulation info p->nBits = (1 << p->nLeavesMax); - p->nWords = (p->nBits <= 32)? 1 : p->nBits / sizeof(unsigned) / 8; + p->nWords = (p->nBits <= 32)? 1 : (p->nBits / 32); p->pInfo = ALLOC( unsigned, p->nWords * p->nDivsMax ); memset( p->pInfo, 0, sizeof(unsigned) * p->nWords * p->nLeavesMax ); p->vSims = Vec_PtrAlloc( p->nDivsMax ); @@ -111,11 +266,14 @@ Abc_ResubMan_t * Abc_ResubManStart( int nLeavesMax, int nDivsMax ) pData[i/32] |= (1 << (i%32)); } // create the remaining divisors - p->vDivs1U = Vec_PtrAlloc( p->nDivsMax ); - p->vDivs1B = Vec_PtrAlloc( p->nDivsMax ); - p->vDivs2U0 = Vec_PtrAlloc( p->nDivsMax ); - p->vDivs2U1 = Vec_PtrAlloc( p->nDivsMax ); - p->vTemp = Vec_PtrAlloc( p->nDivsMax ); + p->vDivs1UP = Vec_PtrAlloc( p->nDivsMax ); + p->vDivs1UN = Vec_PtrAlloc( p->nDivsMax ); + p->vDivs1B = Vec_PtrAlloc( p->nDivsMax ); + p->vDivs2UP0 = Vec_PtrAlloc( p->nDivsMax ); + p->vDivs2UP1 = Vec_PtrAlloc( p->nDivsMax ); + p->vDivs2UN0 = Vec_PtrAlloc( p->nDivsMax ); + p->vDivs2UN1 = Vec_PtrAlloc( p->nDivsMax ); + p->vTemp = Vec_PtrAlloc( p->nDivsMax ); return p; } @@ -130,87 +288,87 @@ Abc_ResubMan_t * Abc_ResubManStart( int nLeavesMax, int nDivsMax ) SeeAlso [] ***********************************************************************/ -void Abc_ResubManStop( Abc_ResubMan_t * p ) +void Abc_ManResubStop( Abc_ManRes_t * p ) { Vec_PtrFree( p->vDivs ); Vec_PtrFree( p->vSims ); - Vec_PtrFree( p->vDivs1U ); + Vec_PtrFree( p->vDivs1UP ); + Vec_PtrFree( p->vDivs1UN ); Vec_PtrFree( p->vDivs1B ); - Vec_PtrFree( p->vDivs2U0 ); - Vec_PtrFree( p->vDivs2U1 ); + Vec_PtrFree( p->vDivs2UP0 ); + Vec_PtrFree( p->vDivs2UP1 ); + Vec_PtrFree( p->vDivs2UN0 ); + Vec_PtrFree( p->vDivs2UN1 ); Vec_PtrFree( p->vTemp ); free( p->pInfo ); free( p ); } - /**Function************************************************************* - Synopsis [Evaluates resubstution of one cut.] + Synopsis [] - Description [Returns the graph to add if any.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_ResubManEval( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps ) +void Abc_ManResubPrint( Abc_ManRes_t * p ) { - Dec_Graph_t * pGraph; - assert( nSteps >= 0 ); - assert( nSteps <= 3 ); - // get the number of leaves - p->pRoot = pRoot; - p->nLeaves = Vec_PtrSize(vLeaves); - // collect the divisor nodes - Abc_ResubManCollectDivs( p, pRoot, vLeaves ); - // quit if the number of divisors collected is too large - if ( Vec_PtrSize(p->vDivs) - p->nLeaves > p->nDivsMax - p->nLeavesMax ) - return NULL; - // get the number nodes in its MFFC (and reorder the nodes) - p->nMffc = Abc_ResubManMffc( p, p->vDivs, pRoot, p->nLeaves ); - assert( p->nMffc > 0 ); - // get the number of divisors - p->nDivs = Vec_PtrSize(p->vDivs) - p->nMffc; - // simulate the nodes - Abc_ResubManSimulate( p->vDivs, p->nLeaves, p->vSims, p->nLeavesMax, p->nWords ); + printf( "Used constants = %6d. ", p->nUsedNodeC ); PRT( "Cuts ", p->timeCut ); + printf( "Used replacements = %6d. ", p->nUsedNode0 ); PRT( "Resub ", p->timeRes ); + printf( "Used single ORs = %6d. ", p->nUsedNode1Or ); PRT( " Div ", p->timeDiv ); + printf( "Used single ANDs = %6d. ", p->nUsedNode1And ); PRT( " Mffc ", p->timeMffc ); + printf( "Used double ORs = %6d. ", p->nUsedNode2Or ); PRT( " Sim ", p->timeSim ); + printf( "Used double ANDs = %6d. ", p->nUsedNode2And ); PRT( " 1 ", p->timeRes1 ); + printf( "Used OR-AND = %6d. ", p->nUsedNode2OrAnd ); PRT( " D ", p->timeResD ); + printf( "Used AND-OR = %6d. ", p->nUsedNode2AndOr ); PRT( " 2 ", p->timeRes2 ); + printf( "Used OR-2ANDs = %6d. ", p->nUsedNode3OrAnd ); PRT( " 3 ", p->timeRes3 ); + printf( "Used AND-2ORs = %6d. ", p->nUsedNode3AndOr ); PRT( "AIG ", p->timeNtk ); + printf( "TOTAL = %6d. ", p->nUsedNodeC + + p->nUsedNode0 + + p->nUsedNode1Or + + p->nUsedNode1And + + p->nUsedNode2Or + + p->nUsedNode2And + + p->nUsedNode2OrAnd + + p->nUsedNode2AndOr + + p->nUsedNode3OrAnd + + p->nUsedNode3AndOr + ); PRT( "TOTAL ", p->timeTotal ); + printf( "Total leaves = %8d.\n", p->nTotalLeaves ); + printf( "Total divisors = %8d.\n", p->nTotalDivs ); + +} - // consider constants - if ( pGraph = Abc_ResubManQuit( p ) ) - return pGraph; - // consider equal nodes - if ( pGraph = Abc_ResubManDivs0( p ) ) - return pGraph; - if ( nSteps == 0 || p->nLeavesMax == 1 ) - return NULL; +/**Function************************************************************* - // consider one node - if ( pGraph = Abc_ResubManDivs1( p ) ) - return pGraph; - if ( nSteps == 1 || p->nLeavesMax == 2 ) - return NULL; + Synopsis [] - // get the two level divisors - Abc_ResubManDivsD( p ); + Description [] + + SideEffects [] - // consider two nodes - if ( pGraph = Abc_ResubManDivs2( p ) ) - return pGraph; - if ( nSteps == 2 || p->nLeavesMax == 3 ) - return NULL; + SeeAlso [] - // consider two nodes - if ( pGraph = Abc_ResubManDivs3( p ) ) - return pGraph; - if ( nSteps == 3 || p->nLeavesMax == 4 ) - return NULL; - return NULL; +***********************************************************************/ +void Abc_ManResubCollectDivs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vInternal ) +{ + // skip visited nodes + if ( Abc_NodeIsTravIdCurrent(pNode) ) + return; + Abc_NodeSetTravIdCurrent(pNode); + // collect the fanins + Abc_ManResubCollectDivs_rec( Abc_ObjFanin0(pNode), vInternal ); + Abc_ManResubCollectDivs_rec( Abc_ObjFanin1(pNode), vInternal ); + // collect the internal node + if ( pNode->fMarkA == 0 ) + Vec_PtrPush( vInternal, pNode ); } - - /**Function************************************************************* Synopsis [] @@ -222,11 +380,16 @@ Dec_Graph_t * Abc_ResubManEval( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t SeeAlso [] ***********************************************************************/ -int Abc_ResubManCollectDivs( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves ) +int Abc_ManResubCollectDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int Required ) { - Abc_Obj_t * pNode, * pFanout; - int i, k; - // collect the leaves of the cut + Abc_Obj_t * pNode, * pFanout;//, * pFanin; + int i, k, Limit, Counter; + + Vec_PtrClear( p->vDivs1UP ); + Vec_PtrClear( p->vDivs1UN ); + Vec_PtrClear( p->vDivs1B ); + + // add the leaves of the cuts to the divisors Vec_PtrClear( p->vDivs ); Abc_NtkIncrementTravId( pRoot->pNtk ); Vec_PtrForEachEntry( vLeaves, pNode, i ) @@ -234,44 +397,103 @@ int Abc_ResubManCollectDivs( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * Vec_PtrPush( p->vDivs, pNode ); Abc_NodeSetTravIdCurrent( pNode ); } - // explore the fanouts + + // mark nodes in the MFFC + Vec_PtrForEachEntry( p->vTemp, pNode, i ) + pNode->fMarkA = 1; + // collect the cone (without MFFC) + Abc_ManResubCollectDivs_rec( pRoot, p->vDivs ); + // unmark the current MFFC + Vec_PtrForEachEntry( p->vTemp, pNode, i ) + pNode->fMarkA = 0; + + // check if the number of divisors is not exceeded + if ( Vec_PtrSize(p->vDivs) - Vec_PtrSize(vLeaves) + Vec_PtrSize(p->vTemp) >= Vec_PtrSize(p->vSims) - p->nLeavesMax ) + return 0; + + // get the number of divisors to collect + Limit = Vec_PtrSize(p->vSims) - p->nLeavesMax - (Vec_PtrSize(p->vDivs) - Vec_PtrSize(vLeaves) + Vec_PtrSize(p->vTemp)); + + // explore the fanouts, which are not in the MFFC + Counter = 0; Vec_PtrForEachEntry( p->vDivs, pNode, i ) { + if ( Abc_ObjFanoutNum(pNode) > 100 ) + { +// printf( "%d ", Abc_ObjFanoutNum(pNode) ); + continue; + } // if the fanout has both fanins in the set, add it Abc_ObjForEachFanout( pNode, pFanout, k ) { - if ( Abc_NodeIsTravIdCurrent(pFanout) || Abc_ObjIsPo(pFanout) ) + if ( Abc_NodeIsTravIdCurrent(pFanout) || Abc_ObjIsCo(pFanout) || (int)pFanout->Level > Required ) continue; if ( Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pFanout)) && Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pFanout)) ) { + if ( Abc_ObjFanin0(pFanout) == pRoot || Abc_ObjFanin1(pFanout) == pRoot ) + continue; Vec_PtrPush( p->vDivs, pFanout ); - Abc_NodeSetTravIdCurrent( pFanout ); + Abc_NodeSetTravIdCurrent( pFanout ); + // quit computing divisors if there is too many of them + if ( ++Counter == Limit ) + goto Quits; } } } - return 1; -} -/**Function************************************************************* - - Synopsis [] +Quits : + // get the number of divisors + p->nDivs = Vec_PtrSize(p->vDivs); - Description [] - - SideEffects [] + // add the nodes in the MFFC + Vec_PtrForEachEntry( p->vTemp, pNode, i ) + Vec_PtrPush( p->vDivs, pNode ); + assert( pRoot == Vec_PtrEntryLast(p->vDivs) ); - SeeAlso [] + assert( Vec_PtrSize(p->vDivs) - Vec_PtrSize(vLeaves) <= Vec_PtrSize(p->vSims) - p->nLeavesMax ); -***********************************************************************/ -int Abc_ResubManMffc_rec( Abc_Obj_t * pNode ) +/* +if (pRoot->Id == 15281 ) { - if ( Abc_NodeIsTravIdCurrent(pNode) ) - return 0; - Abc_NodeSetTravIdCurrent( pNode ); - return 1 + Abc_ResubManMffc_rec( Abc_ObjFanin0(pNode) ) + - Abc_ResubManMffc_rec( Abc_ObjFanin1(pNode) ); + // print the nodes + Vec_PtrForEachEntry( p->vDivs, pNode, i ) + { + if ( i < Vec_PtrSize(vLeaves) ) + { + printf( "%6d : %c\n", pNode->Id, 'a'+i ); + continue; + } + printf( "%6d : %2d = ", pNode->Id, i ); + // find the first fanin + Vec_PtrForEachEntry( p->vDivs, pFanin, k ) + if ( Abc_ObjFanin0(pNode) == pFanin ) + break; + if ( k < Vec_PtrSize(vLeaves) ) + printf( "%c", 'a' + k ); + else + printf( "%d", k ); + printf( "%s ", Abc_ObjFaninC0(pNode)? "\'" : "" ); + // find the second fanin + Vec_PtrForEachEntry( p->vDivs, pFanin, k ) + if ( Abc_ObjFanin1(pNode) == pFanin ) + break; + if ( k < Vec_PtrSize(vLeaves) ) + printf( "%c", 'a' + k ); + else + printf( "%d", k ); + printf( "%s ", Abc_ObjFaninC1(pNode)? "\'" : "" ); + if ( pNode == pRoot ) + printf( " root" ); + printf( "\n" ); + } + printf( "\n" ); +} +*/ + + return 1; } + /**Function************************************************************* Synopsis [] @@ -283,21 +505,30 @@ int Abc_ResubManMffc_rec( Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -int Abc_ResubManMffc( Abc_ResubMan_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves ) +int Abc_ManResubMffc( Abc_ManRes_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves ) { Abc_Obj_t * pObj; int Counter, i, k; // increment the traversal ID for the leaves + // increment the fanout counters of the leaves Abc_NtkIncrementTravId( pRoot->pNtk ); - // label the leaves Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves ) + { + pObj->vFanouts.nSize++; Abc_NodeSetTravIdCurrent( pObj ); + } // make sure the node is in the cone and is no one of the leaves assert( Abc_NodeIsTravIdPrevious(pRoot) ); - Counter = Abc_ResubManMffc_rec( pRoot ); + Counter = Abc_NodeMffcLabel( pRoot ); + // remove the extra counters + Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves ) + pObj->vFanouts.nSize--; + + // sort the nodes by level!!! + // move the labeled nodes to the end Vec_PtrClear( p->vTemp ); - k = 0; + k = nLeaves; Vec_PtrForEachEntryStart( vDivs, pObj, i, nLeaves ) if ( Abc_NodeIsTravIdCurrent(pObj) ) Vec_PtrPush( p->vTemp, pObj ); @@ -322,21 +553,26 @@ int Abc_ResubManMffc( Abc_ResubMan_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, SeeAlso [] ***********************************************************************/ -void Abc_ResubManSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords ) +void Abc_ManResubSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords ) { Abc_Obj_t * pObj; unsigned * puData0, * puData1, * puData; int i, k; - // initialize random simulation data - Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves ) - pObj->pData = Vec_PtrEntry( vSims, i ); + assert( Vec_PtrSize(vDivs) - nLeaves <= Vec_PtrSize(vSims) - nLeavesMax ); // simulate - Vec_PtrForEachEntryStart( vDivs, pObj, i, nLeaves ) + Vec_PtrForEachEntry( vDivs, pObj, i ) { - pObj->pData = Vec_PtrEntry( vSims, i + nLeavesMax ); + if ( i < nLeaves ) + { // initialize the leaf + pObj->pData = Vec_PtrEntry( vSims, i ); + continue; + } + // set storage for the node's simulation info + pObj->pData = Vec_PtrEntry( vSims, i - nLeaves + nLeavesMax ); + // get pointer to the simulation info + puData = pObj->pData; puData0 = Abc_ObjFanin0(pObj)->pData; puData1 = Abc_ObjFanin1(pObj)->pData; - puData = pObj->pData; // simulate if ( Abc_ObjFaninC0(pObj) && Abc_ObjFaninC1(pObj) ) for ( k = 0; k < nWords; k++ ) @@ -351,7 +587,7 @@ void Abc_ResubManSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, in for ( k = 0; k < nWords; k++ ) puData[k] = puData0[k] & puData1[k]; } - // complement if needed + // normalize Vec_PtrForEachEntry( vDivs, pObj, i ) { puData = pObj->pData; @@ -374,18 +610,18 @@ void Abc_ResubManSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, in SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_ResubManQuit( Abc_ResubMan_t * p ) +Dec_Graph_t * Abc_ManResubQuit( Abc_ManRes_t * p ) { Dec_Graph_t * pGraph; unsigned * upData; int w; upData = p->pRoot->pData; for ( w = 0; w < p->nWords; w++ ) - if ( upData[0] == 0 ) + if ( upData[w] ) break; if ( w != p->nWords ) return NULL; - // get the graph if the node looks constant + // get constant node graph if ( p->pRoot->fPhase ) pGraph = Dec_GraphCreateConst1(); else @@ -404,7 +640,7 @@ Dec_Graph_t * Abc_ResubManQuit( Abc_ResubMan_t * p ) SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_ResubManQuit0( Abc_Obj_t * pRoot, Abc_Obj_t * pObj ) +Dec_Graph_t * Abc_ManResubQuit0( Abc_Obj_t * pRoot, Abc_Obj_t * pObj ) { Dec_Graph_t * pGraph; Dec_Edge_t eRoot; @@ -416,7 +652,7 @@ Dec_Graph_t * Abc_ResubManQuit0( Abc_Obj_t * pRoot, Abc_Obj_t * pObj ) Dec_GraphComplement( pGraph ); return pGraph; } - + /**Function************************************************************* Synopsis [] @@ -428,10 +664,11 @@ Dec_Graph_t * Abc_ResubManQuit0( Abc_Obj_t * pRoot, Abc_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_ResubManQuit1( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ) +Dec_Graph_t * Abc_ManResubQuit1( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, int fOrGate ) { Dec_Graph_t * pGraph; Dec_Edge_t eRoot, eNode0, eNode1; + assert( pObj0 != pObj1 ); assert( !Abc_ObjIsComplement(pObj0) ); assert( !Abc_ObjIsComplement(pObj1) ); pGraph = Dec_GraphCreate( 2 ); @@ -439,7 +676,52 @@ Dec_Graph_t * Abc_ResubManQuit1( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t Dec_GraphNode( pGraph, 1 )->pFunc = pObj1; eNode0 = Dec_EdgeCreate( 0, pObj0->fPhase ); eNode1 = Dec_EdgeCreate( 1, pObj1->fPhase ); - eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 ); + if ( fOrGate ) + eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 ); + else + eRoot = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 ); + Dec_GraphSetRoot( pGraph, eRoot ); + if ( pRoot->fPhase ) + Dec_GraphComplement( pGraph ); + return pGraph; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ManResubQuit21( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2, int fOrGate ) +{ + Dec_Graph_t * pGraph; + Dec_Edge_t eRoot, eNode0, eNode1, eNode2; + assert( pObj0 != pObj1 ); + assert( !Abc_ObjIsComplement(pObj0) ); + assert( !Abc_ObjIsComplement(pObj1) ); + assert( !Abc_ObjIsComplement(pObj2) ); + pGraph = Dec_GraphCreate( 3 ); + Dec_GraphNode( pGraph, 0 )->pFunc = pObj0; + Dec_GraphNode( pGraph, 1 )->pFunc = pObj1; + Dec_GraphNode( pGraph, 2 )->pFunc = pObj2; + eNode0 = Dec_EdgeCreate( 0, pObj0->fPhase ); + eNode1 = Dec_EdgeCreate( 1, pObj1->fPhase ); + eNode2 = Dec_EdgeCreate( 2, pObj2->fPhase ); + if ( fOrGate ) + { + eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 ); + eRoot = Dec_GraphAddNodeOr( pGraph, eNode2, eRoot ); + } + else + { + eRoot = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 ); + eRoot = Dec_GraphAddNodeAnd( pGraph, eNode2, eRoot ); + } Dec_GraphSetRoot( pGraph, eRoot ); if ( pRoot->fPhase ) Dec_GraphComplement( pGraph ); @@ -457,20 +739,35 @@ Dec_Graph_t * Abc_ResubManQuit1( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_ResubManQuit2( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2 ) +Dec_Graph_t * Abc_ManResubQuit2( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2, int fOrGate ) { Dec_Graph_t * pGraph; - Dec_Edge_t eRoot, eAnd, eNode0, eNode1, eNode2; + Dec_Edge_t eRoot, ePrev, eNode0, eNode1, eNode2; + assert( pObj0 != pObj1 ); + assert( pObj0 != pObj2 ); + assert( pObj1 != pObj2 ); assert( !Abc_ObjIsComplement(pObj0) ); pGraph = Dec_GraphCreate( 3 ); Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0); Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1); Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2); - eNode0 = Dec_EdgeCreate( 0, Abc_ObjIsComplement(pObj0) ^ pObj0->fPhase ); - eNode1 = Dec_EdgeCreate( 1, Abc_ObjIsComplement(pObj1) ^ pObj1->fPhase ); - eNode2 = Dec_EdgeCreate( 2, Abc_ObjIsComplement(pObj2) ^ pObj2->fPhase ); - eAnd = Dec_GraphAddNodeAnd( pGraph, eNode1, eNode2 ); - eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eAnd ); + eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ); + if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ); + eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ); + ePrev = Dec_GraphAddNodeOr( pGraph, eNode1, eNode2 ); + } + else + { + eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) ); + eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) ); + ePrev = Dec_GraphAddNodeAnd( pGraph, eNode1, eNode2 ); + } + if ( fOrGate ) + eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, ePrev ); + else + eRoot = Dec_GraphAddNodeAnd( pGraph, eNode0, ePrev ); Dec_GraphSetRoot( pGraph, eRoot ); if ( pRoot->fPhase ) Dec_GraphComplement( pGraph ); @@ -488,22 +785,57 @@ Dec_Graph_t * Abc_ResubManQuit2( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_ResubManQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2, Abc_Obj_t * pObj3 ) +Dec_Graph_t * Abc_ManResubQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2, Abc_Obj_t * pObj3, int fOrGate ) { Dec_Graph_t * pGraph; - Dec_Edge_t eRoot, eAnd0, eAnd1, eNode0, eNode1, eNode2, eNode3; + Dec_Edge_t eRoot, ePrev0, ePrev1, eNode0, eNode1, eNode2, eNode3; + assert( pObj0 != pObj1 ); + assert( pObj2 != pObj3 ); pGraph = Dec_GraphCreate( 4 ); Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0); Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1); Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2); Dec_GraphNode( pGraph, 3 )->pFunc = Abc_ObjRegular(pObj3); - eNode0 = Dec_EdgeCreate( 0, Abc_ObjIsComplement(pObj0) ^ pObj0->fPhase ); - eNode1 = Dec_EdgeCreate( 1, Abc_ObjIsComplement(pObj1) ^ pObj1->fPhase ); - eNode2 = Dec_EdgeCreate( 2, Abc_ObjIsComplement(pObj2) ^ pObj2->fPhase ); - eNode3 = Dec_EdgeCreate( 3, Abc_ObjIsComplement(pObj3) ^ pObj3->fPhase ); - eAnd0 = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 ); - eAnd1 = Dec_GraphAddNodeAnd( pGraph, eNode2, eNode3 ); - eRoot = Dec_GraphAddNodeOr( pGraph, eAnd0, eAnd1 ); + if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) ) + { + eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ); + eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ); + ePrev0 = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 ); + if ( Abc_ObjIsComplement(pObj2) && Abc_ObjIsComplement(pObj3) ) + { + eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ); + eNode3 = Dec_EdgeCreate( 3, Abc_ObjRegular(pObj3)->fPhase ); + ePrev1 = Dec_GraphAddNodeOr( pGraph, eNode2, eNode3 ); + } + else + { + eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) ); + eNode3 = Dec_EdgeCreate( 3, Abc_ObjRegular(pObj3)->fPhase ^ Abc_ObjIsComplement(pObj3) ); + ePrev1 = Dec_GraphAddNodeAnd( pGraph, eNode2, eNode3 ); + } + } + else + { + eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) ); + eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) ); + ePrev0 = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 ); + if ( Abc_ObjIsComplement(pObj2) && Abc_ObjIsComplement(pObj3) ) + { + eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ); + eNode3 = Dec_EdgeCreate( 3, Abc_ObjRegular(pObj3)->fPhase ); + ePrev1 = Dec_GraphAddNodeOr( pGraph, eNode2, eNode3 ); + } + else + { + eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) ); + eNode3 = Dec_EdgeCreate( 3, Abc_ObjRegular(pObj3)->fPhase ^ Abc_ObjIsComplement(pObj3) ); + ePrev1 = Dec_GraphAddNodeAnd( pGraph, eNode2, eNode3 ); + } + } + if ( fOrGate ) + eRoot = Dec_GraphAddNodeOr( pGraph, ePrev0, ePrev1 ); + else + eRoot = Dec_GraphAddNodeAnd( pGraph, ePrev0, ePrev1 ); Dec_GraphSetRoot( pGraph, eRoot ); if ( pRoot->fPhase ) Dec_GraphComplement( pGraph ); @@ -511,9 +843,11 @@ Dec_Graph_t * Abc_ResubManQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t } + + /**Function************************************************************* - Synopsis [Derives unate/binate divisors.] + Synopsis [Derives single-node unate/binate divisors.] Description [] @@ -522,36 +856,47 @@ Dec_Graph_t * Abc_ResubManQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_ResubManDivs0( Abc_ResubMan_t * p ) +void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required ) { Abc_Obj_t * pObj; unsigned * puData, * puDataR; int i, w; - Vec_PtrClear( p->vDivs1U ); + Vec_PtrClear( p->vDivs1UP ); + Vec_PtrClear( p->vDivs1UN ); Vec_PtrClear( p->vDivs1B ); puDataR = p->pRoot->pData; Vec_PtrForEachEntryStop( p->vDivs, pObj, i, p->nDivs ) { + if ( (int)pObj->Level > Required - 1 ) + continue; + puData = pObj->pData; + // check positive containment for ( w = 0; w < p->nWords; w++ ) - if ( puData[w] != puDataR[w] ) + if ( puData[w] & ~puDataR[w] ) break; if ( w == p->nWords ) - return Abc_ResubManQuit0( p->pRoot, pObj ); + { + Vec_PtrPush( p->vDivs1UP, pObj ); + continue; + } + // check negative containment for ( w = 0; w < p->nWords; w++ ) - if ( puData[w] & ~puDataR[w] ) + if ( ~puData[w] & puDataR[w] ) break; if ( w == p->nWords ) - Vec_PtrPush( p->vDivs1U, pObj ); - else - Vec_PtrPush( p->vDivs1B, pObj ); + { + Vec_PtrPush( p->vDivs1UN, pObj ); + continue; + } + // add the node to binates + Vec_PtrPush( p->vDivs1B, pObj ); } - return NULL; } /**Function************************************************************* - Synopsis [Derives unate/binate divisors.] + Synopsis [Derives double-node unate/binate divisors.] Description [] @@ -560,28 +905,109 @@ Dec_Graph_t * Abc_ResubManDivs0( Abc_ResubMan_t * p ) SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_ResubManDivs1( Abc_ResubMan_t * p ) +void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ) { Abc_Obj_t * pObj0, * pObj1; unsigned * puData0, * puData1, * puDataR; int i, k, w; + Vec_PtrClear( p->vDivs2UP0 ); + Vec_PtrClear( p->vDivs2UP1 ); + Vec_PtrClear( p->vDivs2UN0 ); + Vec_PtrClear( p->vDivs2UN1 ); puDataR = p->pRoot->pData; - Vec_PtrForEachEntry( p->vDivs1U, pObj0, i ) + Vec_PtrForEachEntry( p->vDivs1B, pObj0, i ) { + if ( (int)pObj0->Level > Required - 2 ) + continue; + puData0 = pObj0->pData; - Vec_PtrForEachEntryStart( p->vDivs1U, pObj1, k, i + 1 ) + Vec_PtrForEachEntryStart( p->vDivs1B, pObj1, k, i + 1 ) { + if ( (int)pObj1->Level > Required - 2 ) + continue; + puData1 = pObj1->pData; - for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] | puData1[w]) != puDataR[w] ) - break; - if ( w == p->nWords ) - return Abc_ResubManQuit1( p->pRoot, pObj0, pObj1 ); + + if ( Vec_PtrSize(p->vDivs2UP0) < 500 ) + { + // get positive unate divisors + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] & puData1[w]) & ~puDataR[w] ) + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs2UP0, pObj0 ); + Vec_PtrPush( p->vDivs2UP1, pObj1 ); + } + for ( w = 0; w < p->nWords; w++ ) + if ( (~puData0[w] & puData1[w]) & ~puDataR[w] ) + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs2UP0, Abc_ObjNot(pObj0) ); + Vec_PtrPush( p->vDivs2UP1, pObj1 ); + } + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] ) + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs2UP0, pObj0 ); + Vec_PtrPush( p->vDivs2UP1, Abc_ObjNot(pObj1) ); + } + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] | puData1[w]) & ~puDataR[w] ) + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs2UP0, Abc_ObjNot(pObj0) ); + Vec_PtrPush( p->vDivs2UP1, Abc_ObjNot(pObj1) ); + } + } + + if ( Vec_PtrSize(p->vDivs2UN0) < 500 ) + { + // get negative unate divisors + for ( w = 0; w < p->nWords; w++ ) + if ( ~(puData0[w] & puData1[w]) & puDataR[w] ) + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs2UN0, pObj0 ); + Vec_PtrPush( p->vDivs2UN1, pObj1 ); + } + for ( w = 0; w < p->nWords; w++ ) + if ( ~(~puData0[w] & puData1[w]) & puDataR[w] ) + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs2UN0, Abc_ObjNot(pObj0) ); + Vec_PtrPush( p->vDivs2UN1, pObj1 ); + } + for ( w = 0; w < p->nWords; w++ ) + if ( ~(puData0[w] & ~puData1[w]) & puDataR[w] ) + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs2UN0, pObj0 ); + Vec_PtrPush( p->vDivs2UN1, Abc_ObjNot(pObj1) ); + } + for ( w = 0; w < p->nWords; w++ ) + if ( ~(puData0[w] | puData1[w]) & puDataR[w] ) + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs2UN0, Abc_ObjNot(pObj0) ); + Vec_PtrPush( p->vDivs2UN1, Abc_ObjNot(pObj1) ); + } + } } } - return NULL; +// printf( "%d %d ", Vec_PtrSize(p->vDivs2UP0), Vec_PtrSize(p->vDivs2UN0) ); } + + /**Function************************************************************* Synopsis [Derives unate/binate divisors.] @@ -593,46 +1019,72 @@ Dec_Graph_t * Abc_ResubManDivs1( Abc_ResubMan_t * p ) SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_ResubManDivsD( Abc_ResubMan_t * p ) +Dec_Graph_t * Abc_ManResubDivs0( Abc_ManRes_t * p ) { - Abc_Obj_t * pObj0, * pObj1; - unsigned * puData0, * puData1, * puDataR; - int i, k, w; - Vec_PtrClear( p->vDivs2U0 ); - Vec_PtrClear( p->vDivs2U1 ); + Abc_Obj_t * pObj; + unsigned * puData, * puDataR; + int i, w; puDataR = p->pRoot->pData; - Vec_PtrForEachEntry( p->vDivs1U, pObj0, i ) + Vec_PtrForEachEntryStop( p->vDivs, pObj, i, p->nDivs ) { - puData0 = pObj0->pData; - Vec_PtrForEachEntryStart( p->vDivs1U, pObj1, k, i + 1 ) - { - puData1 = pObj1->pData; + puData = pObj->pData; + for ( w = 0; w < p->nWords; w++ ) + if ( puData[w] != puDataR[w] ) + break; + if ( w == p->nWords ) + return Abc_ManResubQuit0( p->pRoot, pObj ); + } + return NULL; +} - for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] & puData1[w]) & ~puDataR[w] ) - break; - if ( w == p->nWords ) - { - Vec_PtrPush( p->vDivs2U0, pObj0 ); - Vec_PtrPush( p->vDivs2U1, pObj1 ); - } +/**Function************************************************************* + Synopsis [Derives unate/binate divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required ) +{ + Abc_Obj_t * pObj0, * pObj1; + unsigned * puData0, * puData1, * puDataR; + int i, k, w; + puDataR = p->pRoot->pData; + // check positive unate divisors + Vec_PtrForEachEntry( p->vDivs1UP, pObj0, i ) + { + puData0 = pObj0->pData; + Vec_PtrForEachEntryStart( p->vDivs1UP, pObj1, k, i + 1 ) + { + puData1 = pObj1->pData; for ( w = 0; w < p->nWords; w++ ) - if ( (~puData0[w] & puData1[w]) & ~puDataR[w] ) + if ( (puData0[w] | puData1[w]) != puDataR[w] ) break; if ( w == p->nWords ) { - Vec_PtrPush( p->vDivs2U0, Abc_ObjNot(pObj0) ); - Vec_PtrPush( p->vDivs2U1, pObj1 ); + p->nUsedNode1Or++; + return Abc_ManResubQuit1( p->pRoot, pObj0, pObj1, 1 ); } - + } + } + // check negative unate divisors + Vec_PtrForEachEntry( p->vDivs1UN, pObj0, i ) + { + puData0 = pObj0->pData; + Vec_PtrForEachEntryStart( p->vDivs1UN, pObj1, k, i + 1 ) + { + puData1 = pObj1->pData; for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] ) + if ( (puData0[w] & puData1[w]) != puDataR[w] ) break; if ( w == p->nWords ) { - Vec_PtrPush( p->vDivs2U0, pObj0 ); - Vec_PtrPush( p->vDivs2U1, Abc_ObjNot(pObj1) ); + p->nUsedNode1And++; + return Abc_ManResubQuit1( p->pRoot, pObj0, pObj1, 0 ); } } } @@ -650,42 +1102,188 @@ Dec_Graph_t * Abc_ResubManDivsD( Abc_ResubMan_t * p ) SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_ResubManDivs2( Abc_ResubMan_t * p ) +Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required ) +{ + Abc_Obj_t * pObj0, * pObj1, * pObj2, * pObjMax, * pObjMin0, * pObjMin1; + unsigned * puData0, * puData1, * puData2, * puDataR; + int i, k, j, w, LevelMax; + puDataR = p->pRoot->pData; + // check positive unate divisors + Vec_PtrForEachEntry( p->vDivs1UP, pObj0, i ) + { + puData0 = pObj0->pData; + Vec_PtrForEachEntryStart( p->vDivs1UP, pObj1, k, i + 1 ) + { + puData1 = pObj1->pData; + Vec_PtrForEachEntryStart( p->vDivs1UP, pObj2, j, k + 1 ) + { + puData2 = pObj2->pData; + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + break; + if ( w == p->nWords ) + { + LevelMax = ABC_MAX( pObj0->Level, ABC_MAX(pObj1->Level, pObj2->Level) ); + assert( LevelMax <= Required - 1 ); + + pObjMax = NULL; + if ( (int)pObj0->Level == LevelMax ) + pObjMax = pObj0, pObjMin0 = pObj1, pObjMin1 = pObj2; + if ( (int)pObj1->Level == LevelMax ) + { + if ( pObjMax ) continue; + pObjMax = pObj1, pObjMin0 = pObj0, pObjMin1 = pObj2; + } + if ( (int)pObj2->Level == LevelMax ) + { + if ( pObjMax ) continue; + pObjMax = pObj2, pObjMin0 = pObj0, pObjMin1 = pObj1; + } + + p->nUsedNode2Or++; + return Abc_ManResubQuit21( p->pRoot, pObjMin0, pObjMin1, pObjMax, 1 ); + } + } + } + } + // check negative unate divisors + Vec_PtrForEachEntry( p->vDivs1UN, pObj0, i ) + { + puData0 = pObj0->pData; + Vec_PtrForEachEntryStart( p->vDivs1UN, pObj1, k, i + 1 ) + { + puData1 = pObj1->pData; + Vec_PtrForEachEntryStart( p->vDivs1UN, pObj2, j, k + 1 ) + { + puData2 = pObj2->pData; + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + break; + if ( w == p->nWords ) + { + LevelMax = ABC_MAX( pObj0->Level, ABC_MAX(pObj1->Level, pObj2->Level) ); + assert( LevelMax <= Required - 1 ); + + pObjMax = NULL; + if ( (int)pObj0->Level == LevelMax ) + pObjMax = pObj0, pObjMin0 = pObj1, pObjMin1 = pObj2; + if ( (int)pObj1->Level == LevelMax ) + { + if ( pObjMax ) continue; + pObjMax = pObj1, pObjMin0 = pObj0, pObjMin1 = pObj2; + } + if ( (int)pObj2->Level == LevelMax ) + { + if ( pObjMax ) continue; + pObjMax = pObj2, pObjMin0 = pObj0, pObjMin1 = pObj1; + } + + p->nUsedNode2And++; + return Abc_ManResubQuit21( p->pRoot, pObjMin0, pObjMin1, pObjMax, 0 ); + } + } + } + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Derives unate/binate divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required ) { Abc_Obj_t * pObj0, * pObj1, * pObj2; unsigned * puData0, * puData1, * puData2, * puDataR; int i, k, w; puDataR = p->pRoot->pData; - Vec_PtrForEachEntry( p->vDivs1U, pObj0, i ) + // check positive unate divisors + Vec_PtrForEachEntry( p->vDivs1UP, pObj0, i ) { puData0 = pObj0->pData; - Vec_PtrForEachEntryStart( p->vDivs2U0, pObj1, k, i + 1 ) + Vec_PtrForEachEntry( p->vDivs2UP0, pObj1, k ) { - pObj2 = Vec_PtrEntry( p->vDivs2U1, k ); + pObj2 = Vec_PtrEntry( p->vDivs2UP1, k ); + puData1 = Abc_ObjRegular(pObj1)->pData; puData2 = Abc_ObjRegular(pObj2)->pData; - - if ( !Abc_ObjFaninC0(pObj1) && !Abc_ObjFaninC1(pObj2) ) + if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) { for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] ) + if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] ) break; } - else if ( Abc_ObjFaninC0(pObj1) ) + else if ( Abc_ObjIsComplement(pObj1) ) { for ( w = 0; w < p->nWords; w++ ) if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] ) break; } - else if ( Abc_ObjFaninC1(pObj2) ) + else if ( Abc_ObjIsComplement(pObj2) ) { for ( w = 0; w < p->nWords; w++ ) if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] ) break; } - else assert( 0 ); + else + { + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] ) + break; + } + if ( w == p->nWords ) + { + p->nUsedNode2OrAnd++; + return Abc_ManResubQuit2( p->pRoot, pObj0, pObj1, pObj2, 1 ); + } + } + } + // check negative unate divisors + Vec_PtrForEachEntry( p->vDivs1UN, pObj0, i ) + { + puData0 = pObj0->pData; + Vec_PtrForEachEntry( p->vDivs2UN0, pObj1, k ) + { + pObj2 = Vec_PtrEntry( p->vDivs2UN1, k ); + + puData1 = Abc_ObjRegular(pObj1)->pData; + puData2 = Abc_ObjRegular(pObj2)->pData; + if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] ) + break; + } + else if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] ) + break; + } + else if ( Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] ) + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] ) + break; + } if ( w == p->nWords ) - return Abc_ResubManQuit2( p->pRoot, pObj0, pObj1, pObj2 ); + { + p->nUsedNode2AndOr++; + return Abc_ManResubQuit2( p->pRoot, pObj0, pObj1, pObj2, 0 ); + } } } return NULL; @@ -702,98 +1300,598 @@ Dec_Graph_t * Abc_ResubManDivs2( Abc_ResubMan_t * p ) SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_ResubManDivs3( Abc_ResubMan_t * p ) +Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required ) { Abc_Obj_t * pObj0, * pObj1, * pObj2, * pObj3; unsigned * puData0, * puData1, * puData2, * puData3, * puDataR; - int i, k, w; + int i, k, w, Flag; puDataR = p->pRoot->pData; - Vec_PtrForEachEntry( p->vDivs2U0, pObj0, i ) + // check positive unate divisors + Vec_PtrForEachEntry( p->vDivs2UP0, pObj0, i ) { - pObj1 = Vec_PtrEntry( p->vDivs2U1, i ); + pObj1 = Vec_PtrEntry( p->vDivs2UP1, i ); puData0 = Abc_ObjRegular(pObj0)->pData; puData1 = Abc_ObjRegular(pObj1)->pData; + Flag = (Abc_ObjIsComplement(pObj0) << 3) | (Abc_ObjIsComplement(pObj1) << 2); - Vec_PtrForEachEntryStart( p->vDivs2U0, pObj2, k, i + 1 ) + Vec_PtrForEachEntryStart( p->vDivs2UP0, pObj2, k, i + 1 ) { - pObj3 = Vec_PtrEntry( p->vDivs2U1, k ); + pObj3 = Vec_PtrEntry( p->vDivs2UP1, k ); puData2 = Abc_ObjRegular(pObj2)->pData; puData3 = Abc_ObjRegular(pObj3)->pData; - if ( !Abc_ObjFaninC0(pObj0) && !Abc_ObjFaninC1(pObj1) ) + Flag = (Flag & 12) | (Abc_ObjIsComplement(pObj2) << 1) | Abc_ObjIsComplement(pObj3); + assert( Flag < 16 ); + switch( Flag ) { - if ( !Abc_ObjFaninC0(pObj2) && !Abc_ObjFaninC1(pObj3) ) - { - for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) - break; - } - else if ( Abc_ObjFaninC0(pObj2) ) - { - for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) - break; - } - else if ( Abc_ObjFaninC0(pObj3) ) - { - for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) - break; - } - else assert( 0 ); + case 0: // 0000 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 1: // 0001 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) + break; + break; + case 2: // 0010 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 3: // 0011 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] ) + break; + break; + + case 4: // 0100 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 5: // 0101 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) + break; + break; + case 6: // 0110 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 7: // 0111 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & ~puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] ) + break; + break; + + case 8: // 1000 + for ( w = 0; w < p->nWords; w++ ) + if ( ((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 9: // 1001 + for ( w = 0; w < p->nWords; w++ ) + if ( ((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) + break; + break; + case 10: // 1010 + for ( w = 0; w < p->nWords; w++ ) + if ( ((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 11: // 1011 + for ( w = 0; w < p->nWords; w++ ) + if ( ((~puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] ) + break; + break; + + case 12: // 1100 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] | puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 13: // 1101 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] | puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) + break; + break; + case 14: // 1110 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] | puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 15: // 1111 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] | puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] ) + break; + break; + } - else if ( Abc_ObjFaninC0(pObj0) ) + if ( w == p->nWords ) { - if ( !Abc_ObjFaninC0(pObj2) && !Abc_ObjFaninC1(pObj3) ) - { - for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) - break; - } - else if ( Abc_ObjFaninC0(pObj2) ) - { - for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) - break; - } - else if ( Abc_ObjFaninC0(pObj3) ) - { - for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) - break; - } - else assert( 0 ); + p->nUsedNode3OrAnd++; + return Abc_ManResubQuit3( p->pRoot, pObj0, pObj1, pObj2, pObj3, 1 ); } - else if ( Abc_ObjFaninC1(pObj1) ) + } + } +/* + // check negative unate divisors + Vec_PtrForEachEntry( p->vDivs2UN0, pObj0, i ) + { + pObj1 = Vec_PtrEntry( p->vDivs2UN1, i ); + puData0 = Abc_ObjRegular(pObj0)->pData; + puData1 = Abc_ObjRegular(pObj1)->pData; + Flag = (Abc_ObjIsComplement(pObj0) << 3) | (Abc_ObjIsComplement(pObj1) << 2); + + Vec_PtrForEachEntryStart( p->vDivs2UN0, pObj2, k, i + 1 ) + { + pObj3 = Vec_PtrEntry( p->vDivs2UN1, k ); + puData2 = Abc_ObjRegular(pObj2)->pData; + puData3 = Abc_ObjRegular(pObj3)->pData; + + Flag = (Flag & 12) | (Abc_ObjIsComplement(pObj2) << 1) | Abc_ObjIsComplement(pObj3); + assert( Flag < 16 ); + switch( Flag ) { - if ( !Abc_ObjFaninC0(pObj2) && !Abc_ObjFaninC1(pObj3) ) - { - for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) - break; - } - else if ( Abc_ObjFaninC0(pObj2) ) - { - for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) - break; - } - else if ( Abc_ObjFaninC0(pObj3) ) - { - for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) - break; - } - else assert( 0 ); + case 0: // 0000 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 1: // 0001 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] ) + break; + break; + case 2: // 0010 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 3: // 0011 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] ) + break; + break; + + case 4: // 0100 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & ~puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 5: // 0101 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & ~puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] ) + break; + break; + case 6: // 0110 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & ~puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 7: // 0111 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] & ~puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] ) + break; + break; + + case 8: // 1000 + for ( w = 0; w < p->nWords; w++ ) + if ( ((~puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 9: // 1001 + for ( w = 0; w < p->nWords; w++ ) + if ( ((~puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] ) + break; + break; + case 10: // 1010 + for ( w = 0; w < p->nWords; w++ ) + if ( ((~puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 11: // 1011 + for ( w = 0; w < p->nWords; w++ ) + if ( ((~puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] ) + break; + break; + + case 12: // 1100 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] | puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 13: // 1101 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] | puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] ) + break; + break; + case 14: // 1110 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] | puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] ) + break; + break; + case 15: // 1111 + for ( w = 0; w < p->nWords; w++ ) + if ( ((puData0[w] | puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] ) + break; + break; + } - else assert( 0 ); if ( w == p->nWords ) - return Abc_ResubManQuit3( p->pRoot, pObj0, pObj1, pObj2, pObj3 ); + { + p->nUsedNode3AndOr++; + return Abc_ManResubQuit3( p->pRoot, pObj0, pObj1, pObj2, pObj3, 0 ); + } } } +*/ return NULL; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ManResubCleanup( Abc_ManRes_t * p ) +{ + Abc_Obj_t * pObj; + int i; + Vec_PtrForEachEntry( p->vDivs, pObj, i ) + pObj->pData = NULL; + Vec_PtrClear( p->vDivs ); + p->pRoot = NULL; +} + +/**Function************************************************************* + + Synopsis [Evaluates resubstution of one cut.] + + Description [Returns the graph to add if any.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps, bool fUpdateLevel, bool fVerbose ) +{ + extern int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside ); + Dec_Graph_t * pGraph; + int Required; + int clk; + + Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pRoot) : ABC_INFINITY; + + assert( nSteps >= 0 ); + assert( nSteps <= 3 ); + p->pRoot = pRoot; + p->nLeaves = Vec_PtrSize(vLeaves); + p->nLastGain = -1; + + // collect the MFFC +clk = clock(); + p->nMffc = Abc_NodeMffsInside( pRoot, vLeaves, p->vTemp ); +p->timeMffc += clock() - clk; + assert( p->nMffc > 0 ); + + // collect the divisor nodes +clk = clock(); + if ( !Abc_ManResubCollectDivs( p, pRoot, vLeaves, Required ) ) + return NULL; + p->timeDiv += clock() - clk; + + p->nTotalDivs += p->nDivs; + p->nTotalLeaves += p->nLeaves; + + // simulate the nodes +clk = clock(); + Abc_ManResubSimulate( p->vDivs, p->nLeaves, p->vSims, p->nLeavesMax, p->nWords ); +p->timeSim += clock() - clk; + +clk = clock(); + // consider constants + if ( pGraph = Abc_ManResubQuit( p ) ) + { + p->nUsedNodeC++; + p->nLastGain = p->nMffc; + return pGraph; + } + + // consider equal nodes + if ( pGraph = Abc_ManResubDivs0( p ) ) + { +p->timeRes1 += clock() - clk; + p->nUsedNode0++; + p->nLastGain = p->nMffc; + return pGraph; + } + if ( nSteps == 0 || p->nMffc == 1 ) + { +p->timeRes1 += clock() - clk; + return NULL; + } + + // get the one level divisors + Abc_ManResubDivsS( p, Required ); + + // consider one node + if ( pGraph = Abc_ManResubDivs1( p, Required ) ) + { +p->timeRes1 += clock() - clk; + p->nLastGain = p->nMffc - 1; + return pGraph; + } +p->timeRes1 += clock() - clk; + if ( nSteps == 1 || p->nMffc == 2 ) + return NULL; + +clk = clock(); + // consider triples + if ( pGraph = Abc_ManResubDivs12( p, Required ) ) + { +p->timeRes2 += clock() - clk; + p->nLastGain = p->nMffc - 2; + return pGraph; + } +p->timeRes2 += clock() - clk; + + // get the two level divisors +clk = clock(); + Abc_ManResubDivsD( p, Required ); +p->timeResD += clock() - clk; + + // consider two nodes +clk = clock(); + if ( pGraph = Abc_ManResubDivs2( p, Required ) ) + { +p->timeRes2 += clock() - clk; + p->nLastGain = p->nMffc - 2; + return pGraph; + } +p->timeRes2 += clock() - clk; + if ( nSteps == 2 || p->nMffc == 3 ) + return NULL; + + // consider two nodes +clk = clock(); + if ( pGraph = Abc_ManResubDivs3( p, Required ) ) + { +p->timeRes3 += clock() - clk; + p->nLastGain = p->nMffc - 3; + return pGraph; + } +p->timeRes3 += clock() - clk; + if ( nSteps == 3 || p->nLeavesMax == 4 ) + return NULL; + return NULL; +} + + + + +/**Function************************************************************* + + Synopsis [Computes the volume and checks if the cut is feasible.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CutVolumeCheck_rec( Abc_Obj_t * pObj ) +{ + // quit if the node is visited (or if it is a leaf) + if ( Abc_NodeIsTravIdCurrent(pObj) ) + return 0; + Abc_NodeSetTravIdCurrent(pObj); + // report the error + if ( Abc_ObjIsCi(pObj) ) + printf( "Abc_CutVolumeCheck() ERROR: The set of nodes is not a cut!\n" ); + // count the number of nodes in the leaves + return 1 + Abc_CutVolumeCheck_rec( Abc_ObjFanin0(pObj) ) + + Abc_CutVolumeCheck_rec( Abc_ObjFanin1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Computes the volume and checks if the cut is feasible.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CutVolumeCheck( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves ) +{ + Abc_Obj_t * pObj; + int i; + // mark the leaves + Abc_NtkIncrementTravId( pNode->pNtk ); + Vec_PtrForEachEntry( vLeaves, pObj, i ) + Abc_NodeSetTravIdCurrent( pObj ); + // traverse the nodes starting from the given one and count them + return Abc_CutVolumeCheck_rec( pNode ); +} + +/**Function************************************************************* + + Synopsis [Computes the factor cut of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_CutFactor_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves ) +{ + if ( pObj->fMarkA ) + return; + if ( Abc_ObjIsCi(pObj) || (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj)) ) + { + Vec_PtrPush( vLeaves, pObj ); + pObj->fMarkA = 1; + return; + } + Abc_CutFactor_rec( Abc_ObjFanin0(pObj), vLeaves ); + Abc_CutFactor_rec( Abc_ObjFanin1(pObj), vLeaves ); +} + +/**Function************************************************************* + + Synopsis [Computes the factor cut of the node.] + + Description [Factor-cut is the cut at a node in terms of factor-nodes. + Factor-nodes are roots of the node trees (MUXes/EXORs are counted as single nodes). + Factor-cut is unique for the given node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_CutFactor( Abc_Obj_t * pNode ) +{ + Vec_Ptr_t * vLeaves; + Abc_Obj_t * pObj; + int i; + assert( !Abc_ObjIsCi(pNode) ); + vLeaves = Vec_PtrAlloc( 10 ); + Abc_CutFactor_rec( Abc_ObjFanin0(pNode), vLeaves ); + Abc_CutFactor_rec( Abc_ObjFanin1(pNode), vLeaves ); + Vec_PtrForEachEntry( vLeaves, pObj, i ) + pObj->fMarkA = 0; + return vLeaves; +} + +/**Function************************************************************* + + Synopsis [Cut computation.] + + Description [This cut computation works as follows: + It starts with the factor cut at the node. If the factor-cut is large, quit. + It supports the set of leaves of the cut under construction and labels all nodes + in the cut under construction, including the leaves. + It computes the factor-cuts of the leaves and checks if it is easible to add any of them. + If it is, it randomly chooses one feasible and continues.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_CutFactorLarge( Abc_Obj_t * pNode, int nLeavesMax ) +{ + Vec_Ptr_t * vLeaves, * vFactors, * vFact, * vNext; + Vec_Int_t * vFeasible; + Abc_Obj_t * pLeaf, * pTemp; + int i, k, Counter, RandLeaf; + int BestCut, BestShare; + assert( Abc_ObjIsNode(pNode) ); + // get one factor-cut + vLeaves = Abc_CutFactor( pNode ); + if ( Vec_PtrSize(vLeaves) > nLeavesMax ) + { + Vec_PtrFree(vLeaves); + return NULL; + } + if ( Vec_PtrSize(vLeaves) == nLeavesMax ) + return vLeaves; + // initialize the factor cuts for the leaves + vFactors = Vec_PtrAlloc( nLeavesMax ); + Abc_NtkIncrementTravId( pNode->pNtk ); + Vec_PtrForEachEntry( vLeaves, pLeaf, i ) + { + Abc_NodeSetTravIdCurrent( pLeaf ); + if ( Abc_ObjIsCi(pLeaf) ) + Vec_PtrPush( vFactors, NULL ); + else + Vec_PtrPush( vFactors, Abc_CutFactor(pLeaf) ); + } + // construct larger factor cuts + vFeasible = Vec_IntAlloc( nLeavesMax ); + while ( 1 ) + { + BestCut = -1; + // find the next feasible cut to add + Vec_IntClear( vFeasible ); + Vec_PtrForEachEntry( vFactors, vFact, i ) + { + if ( vFact == NULL ) + continue; + // count the number of unmarked leaves of this factor cut + Counter = 0; + Vec_PtrForEachEntry( vFact, pTemp, k ) + Counter += !Abc_NodeIsTravIdCurrent(pTemp); + // if the number of new leaves is smaller than the diff, it is feasible + if ( Counter <= nLeavesMax - Vec_PtrSize(vLeaves) + 1 ) + { + Vec_IntPush( vFeasible, i ); + if ( BestCut == -1 || BestShare < Vec_PtrSize(vFact) - Counter ) + BestCut = i, BestShare = Vec_PtrSize(vFact) - Counter; + } + } + // quit if there is no feasible factor cuts + if ( Vec_IntSize(vFeasible) == 0 ) + break; + // randomly choose one leaf and get its factor cut +// RandLeaf = Vec_IntEntry( vFeasible, rand() % Vec_IntSize(vFeasible) ); + // choose the cut that has most sharing with the other cuts + RandLeaf = BestCut; + + pLeaf = Vec_PtrEntry( vLeaves, RandLeaf ); + vNext = Vec_PtrEntry( vFactors, RandLeaf ); + // unmark this leaf + Abc_NodeSetTravIdPrevious( pLeaf ); + // remove this cut from the leaves and factor cuts + for ( i = RandLeaf; i < Vec_PtrSize(vLeaves)-1; i++ ) + { + Vec_PtrWriteEntry( vLeaves, i, Vec_PtrEntry(vLeaves, i+1) ); + Vec_PtrWriteEntry( vFactors, i, Vec_PtrEntry(vFactors,i+1) ); + } + Vec_PtrShrink( vLeaves, Vec_PtrSize(vLeaves) -1 ); + Vec_PtrShrink( vFactors, Vec_PtrSize(vFactors)-1 ); + // add new leaves, compute their factor cuts + Vec_PtrForEachEntry( vNext, pLeaf, i ) + { + if ( Abc_NodeIsTravIdCurrent(pLeaf) ) + continue; + Abc_NodeSetTravIdCurrent( pLeaf ); + Vec_PtrPush( vLeaves, pLeaf ); + if ( Abc_ObjIsCi(pLeaf) ) + Vec_PtrPush( vFactors, NULL ); + else + Vec_PtrPush( vFactors, Abc_CutFactor(pLeaf) ); + } + Vec_PtrFree( vNext ); + assert( Vec_PtrSize(vLeaves) <= nLeavesMax ); + if ( Vec_PtrSize(vLeaves) == nLeavesMax ) + break; + } + + // remove temporary storage + Vec_PtrForEachEntry( vFactors, vFact, i ) + if ( vFact ) Vec_PtrFree( vFact ); + Vec_PtrFree( vFactors ); + Vec_IntFree( vFeasible ); + return vLeaves; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 718ad657..5456693b 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -112,8 +112,8 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI ***********************************************************************/ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ) { - Fraig_Params_t Params; - Fraig_Man_t * pMan; +// Fraig_Params_t Params; +// Fraig_Man_t * pMan; Abc_Ntk_t * pMiter; int RetValue; @@ -141,7 +141,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV Abc_NtkDelete( pMiter ); return; } - +/* // convert the miter into a FRAIG Fraig_ParamsSetDefault( &Params ); Params.fVerbose = fVerbose; @@ -169,6 +169,18 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV Fraig_ManFree( pMan ); // delete the miter Abc_NtkDelete( pMiter ); +*/ + // solve the CNF using the SAT solver + RetValue = Abc_NtkMiterProve( &pMiter, 0, 0, 1, 1, 0 ); + if ( RetValue == -1 ) + printf( "Networks are undecided (resource limits is reached).\n" ); + else if ( RetValue == 0 ) + printf( "Networks are NOT EQUIVALENT.\n" ); + else + printf( "Networks are equivalent.\n" ); + if ( pMiter->pModel ) + Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); + Abc_NtkDelete( pMiter ); } /**Function************************************************************* -- cgit v1.2.3