summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abc.rc42
-rw-r--r--src/base/abc/abcRefs.c38
-rw-r--r--src/base/abci/abc.c123
-rw-r--r--src/base/abci/abcReconv.c2
-rw-r--r--src/base/abci/abcResub.c1618
-rw-r--r--src/base/abci/abcVerify.c18
6 files changed, 1556 insertions, 285 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,31 +44,66 @@ 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 ///
@@ -75,6 +111,124 @@ static Dec_Graph_t * Abc_ResubManDivs3( Abc_ResubMan_t * p );
/**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 []
Description []
@@ -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,25 +905,135 @@ 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) );
+ }
+ }
}
}
+// printf( "%d %d ", Vec_PtrSize(p->vDivs2UP0), Vec_PtrSize(p->vDivs2UN0) );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Derives unate/binate divisors.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Graph_t * Abc_ManResubDivs0( Abc_ManRes_t * p )
+{
+ Abc_Obj_t * pObj;
+ unsigned * puData, * puDataR;
+ int i, w;
+ puDataR = p->pRoot->pData;
+ Vec_PtrForEachEntryStop( p->vDivs, pObj, i, p->nDivs )
+ {
+ 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;
}
@@ -593,46 +1048,139 @@ Dec_Graph_t * Abc_ResubManDivs1( Abc_ResubMan_t * p )
SeeAlso []
***********************************************************************/
-Dec_Graph_t * Abc_ResubManDivsD( Abc_ResubMan_t * p )
+Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required )
{
Abc_Obj_t * pObj0, * pObj1;
unsigned * puData0, * puData1, * puDataR;
int i, k, w;
- Vec_PtrClear( p->vDivs2U0 );
- Vec_PtrClear( p->vDivs2U1 );
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->vDivs1U, pObj1, k, i + 1 )
+ 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, 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, Abc_ObjNot(pObj0) );
- Vec_PtrPush( p->vDivs2U1, pObj1 );
+ p->nUsedNode1And++;
+ return Abc_ManResubQuit1( p->pRoot, pObj0, pObj1, 0 );
}
+ }
+ }
+ return NULL;
+}
- for ( w = 0; w < p->nWords; w++ )
- if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] )
- break;
- if ( w == p->nWords )
+/**Function*************************************************************
+
+ Synopsis [Derives unate/binate divisors.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+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 )
{
- Vec_PtrPush( p->vDivs2U0, pObj0 );
- Vec_PtrPush( p->vDivs2U1, Abc_ObjNot(pObj1) );
+ 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 );
+ }
}
}
}
@@ -650,42 +1198,92 @@ Dec_Graph_t * Abc_ResubManDivsD( Abc_ResubMan_t * p )
SeeAlso []
***********************************************************************/
-Dec_Graph_t * Abc_ResubManDivs2( Abc_ResubMan_t * p )
+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*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 04:41:45 +0000