summaryrefslogtreecommitdiffstats
path: root/src/opt/res/resCore.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/res/resCore.c')
-rw-r--r--src/opt/res/resCore.c259
1 files changed, 210 insertions, 49 deletions
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index 17d1c62e..6340b175 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -19,7 +19,7 @@
***********************************************************************/
#include "abc.h"
-#include "res.h"
+#include "resInt.h"
#include "kit.h"
#include "satStore.h"
@@ -27,12 +27,120 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+typedef struct Res_Man_t_ Res_Man_t;
+struct Res_Man_t_
+{
+ // general parameters
+ Res_Par_t * pPars;
+ // specialized manager
+ Res_Win_t * pWin; // windowing manager
+ Abc_Ntk_t * pAig; // the strashed window
+ Res_Sim_t * pSim; // simulation manager
+ Sto_Man_t * pCnf; // the CNF of the SAT problem
+ Int_Man_t * pMan; // interpolation manager;
+ Vec_Int_t * vMem; // memory for intermediate SOPs
+ Vec_Vec_t * vResubs; // resubstitution candidates
+ Vec_Vec_t * vLevels; // levelized structure for updating
+ // statistics
+ int nWins; // the number of windows tried
+ int nWinNodes; // the total number of window nodes
+ int nDivNodes; // the total number of divisors
+ int nCandSets; // the total number of candidates
+ int nProvedSets; // the total number of proved groups
+ int nSimEmpty; // the empty simulation info
+ // runtime
+ int timeWin; // windowing
+ int timeDiv; // divisors
+ int timeAig; // strashing
+ int timeSim; // simulation
+ int timeCand; // resubstitution candidates
+ int timeSat; // SAT solving
+ int timeInt; // interpolation
+ int timeUpd; // updating
+ int timeTotal; // total runtime
+};
+
+extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
+ Synopsis [Allocate resynthesis manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
+{
+ Res_Man_t * p;
+ p = ALLOC( Res_Man_t, 1 );
+ memset( p, 0, sizeof(Res_Man_t) );
+ assert( pPars->nWindow > 0 && pPars->nWindow < 100 );
+ assert( pPars->nCands > 0 && pPars->nCands < 100 );
+ p->pPars = pPars;
+ p->pWin = Res_WinAlloc();
+ p->pSim = Res_SimAlloc( pPars->nSimWords );
+ p->pMan = Int_ManAlloc( 512 );
+ p->vMem = Vec_IntAlloc( 0 );
+ p->vResubs = Vec_VecStart( pPars->nCands );
+ p->vLevels = Vec_VecStart( 32 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocate resynthesis manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_ManFree( Res_Man_t * p )
+{
+ if ( p->pPars->fVerbose )
+ {
+ printf( "Winds = %d. ", p->nWins );
+ printf( "Nodes = %d. (Ave = %5.1f) ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins );
+ printf( "Divs = %d. (Ave = %5.1f) ", p->nDivNodes, 1.0*p->nDivNodes/p->nWins );
+ printf( "\n" );
+ printf( "SimEmpt = %d. ", p->nSimEmpty );
+ printf( "Cands = %d. ", p->nCandSets );
+ printf( "Proved = %d. ", p->nProvedSets );
+ printf( "\n" );
+
+ PRT( "Windowing ", p->timeWin );
+ PRT( "Divisors ", p->timeDiv );
+ PRT( "Strashing ", p->timeAig );
+ PRT( "Simulation ", p->timeSim );
+ PRT( "Candidates ", p->timeCand );
+ PRT( "SAT solver ", p->timeSat );
+ PRT( "Interpol ", p->timeInt );
+ PRT( "Undating ", p->timeUpd );
+ PRT( "TOTAL ", p->timeTotal );
+ }
+ Res_WinFree( p->pWin );
+ if ( p->pAig ) Abc_NtkDelete( p->pAig );
+ Res_SimFree( p->pSim );
+ if ( p->pCnf ) Sto_ManFree( p->pCnf );
+ Int_ManFree( p->pMan );
+ Vec_IntFree( p->vMem );
+ Vec_VecFree( p->vResubs );
+ Vec_VecFree( p->vLevels );
+ free( p );
+}
+
+/**Function*************************************************************
+
Synopsis [Entrace into the resynthesis package.]
Description []
@@ -42,31 +150,23 @@
SeeAlso []
***********************************************************************/
-int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerbose, int fVeryVerbose )
+int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
{
- Int_Man_t * pMan;
- Sto_Man_t * pCnf;
- Res_Win_t * pWin;
- Res_Sim_t * pSim;
- Abc_Ntk_t * pAig;
+ Res_Man_t * p;
Abc_Obj_t * pObj;
Hop_Obj_t * pFunc;
Kit_Graph_t * pGraph;
- Vec_Vec_t * vResubs;
Vec_Ptr_t * vFanins;
- Vec_Int_t * vMemory;
unsigned * puTruth;
- int i, k, nNodesOld, nFanins;
+ int i, k, RetValue, nNodesOld, nFanins;
+ int clk, clkTotal = clock();
assert( Abc_NtkHasAig(pNtk) );
- assert( nWindow > 0 && nWindow < 100 );
- vMemory = Vec_IntAlloc(0);
- // start the interpolation manager
- pMan = Int_ManAlloc( 512 );
- // start the window
- pWin = Res_WinAlloc();
- pSim = Res_SimAlloc( nSimWords );
+
+ // start the manager
+ p = Res_ManAlloc( pPars );
// set the number of levels
Abc_NtkLevel( pNtk );
+
// try resynthesizing nodes in the topological order
nNodesOld = Abc_NtkObjNumMax(pNtk);
Abc_NtkForEachObj( pNtk, pObj, i )
@@ -75,52 +175,113 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerb
continue;
if ( pObj->Id > nNodesOld )
break;
+
// create the window for this node
- if ( !Res_WinCompute(pObj, nWindow/10, nWindow%10, pWin) )
+clk = clock();
+ RetValue = Res_WinCompute( pObj, p->pPars->nWindow/10, p->pPars->nWindow%10, p->pWin );
+p->timeWin += clock() - clk;
+ if ( !RetValue )
continue;
+
+ p->nWins++;
+ p->nWinNodes += Vec_VecSizeSize( p->pWin->vLevels );
+
// collect the divisors
- Res_WinDivisors( pWin, pObj->Level - 1 );
+clk = clock();
+ Res_WinDivisors( p->pWin, pObj->Level - 1 );
+p->timeDiv += clock() - clk;
+ p->nDivNodes += Vec_PtrSize( p->pWin->vDivs );
+
// create the AIG for the window
- pAig = Res_WndStrash( pWin );
+clk = clock();
+ if ( p->pAig ) Abc_NtkDelete( p->pAig );
+ p->pAig = Res_WndStrash( p->pWin );
+p->timeAig += clock() - clk;
+
+ if ( p->pPars->fVeryVerbose )
+ {
+ printf( "%5d : ", pObj->Id );
+ printf( "Win = %3d/%4d/%3d ", Vec_PtrSize(p->pWin->vLeaves), Vec_VecSizeSize(p->pWin->vLevels), Vec_PtrSize(p->pWin->vRoots) );
+ printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
+ printf( "D+ = %3d ", p->pWin->nDivsPlus );
+ printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) );
+ printf( "\n" );
+ }
+
// prepare simulation info
- if ( !Res_SimPrepare( pSim, pAig ) )
+clk = clock();
+ RetValue = Res_SimPrepare( p->pSim, p->pAig );
+p->timeSim += clock() - clk;
+ if ( !RetValue )
{
- Abc_NtkDelete( pAig );
+ p->nSimEmpty++;
continue;
}
+
// find resub candidates for the node
- vResubs = Res_FilterCandidates( pWin, pSim );
- if ( vResubs )
+clk = clock();
+ RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs );
+p->timeCand += clock() - clk;
+ p->nCandSets += RetValue;
+ if ( RetValue == 0 )
+ continue;
+
+ // iterate through candidate resubstitutions
+ Vec_VecForEachLevel( p->vResubs, vFanins, k )
{
- // iterate through the resubstitutions
- Vec_VecForEachLevel( vResubs, vFanins, k )
- {
- extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
- pCnf = Res_SatProveUnsat( pAig, vFanins );
- if ( pCnf == NULL )
- continue;
- // interplate this proof
- nFanins = Int_ManInterpolate( pMan, pCnf, fVerbose, &puTruth );
- assert( nFanins == Vec_PtrSize(vFanins) - 2 );
- Sto_ManFree( pCnf );
- // transform interpolant into the AIG
- pGraph = Kit_TruthToGraph( puTruth, nFanins, vMemory );
- // derive the AIG for the decomposition tree
- pFunc = Kit_GraphToHop( pNtk->pManFunc, pGraph );
- Kit_GraphFree( pGraph );
- // update the network
- if ( pFunc == NULL )
- Res_UpdateNetwork( pObj, vFanins, pFunc, pWin->vLevels );
+ if ( Vec_PtrSize(vFanins) == 0 )
break;
+
+ // solve the SAT problem and get clauses
+clk = clock();
+ if ( p->pCnf ) Sto_ManFree( p->pCnf );
+ p->pCnf = Res_SatProveUnsat( p->pAig, vFanins );
+p->timeSat += clock() - clk;
+ if ( p->pCnf == NULL )
+ {
+// printf( " Sat\n" );
+ continue;
+ }
+// printf( " Unsat\n" );
+
+ // write it into a file
+// Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
+
+ p->nProvedSets++;
+
+ // interplate the problem if it was UNSAT
+clk = clock();
+ RetValue = Int_ManInterpolate( p->pMan, p->pCnf, p->pPars->fVerbose, &puTruth );
+p->timeInt += clock() - clk;
+ assert( RetValue == Vec_PtrSize(vFanins) - 2 );
+
+ if ( puTruth )
+ {
+ Extra_PrintBinary( stdout, puTruth, 1 << RetValue );
+ printf( "\n" );
}
- Vec_VecFree( vResubs );
+
+ continue;
+
+ // transform interpolant into the AIG
+ pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
+
+ // derive the AIG for the decomposition tree
+ pFunc = Kit_GraphToHop( pNtk->pManFunc, pGraph );
+ Kit_GraphFree( pGraph );
+
+ // update the network
+clk = clock();
+ Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels );
+p->timeUpd += clock() - clk;
+ break;
}
- Abc_NtkDelete( pAig );
}
- Res_WinFree( pWin );
- Res_SimFree( pSim );
- Int_ManFree( pMan );
- Vec_IntFree( vMemory );
+
+ // quit resubstitution manager
+p->timeTotal = clock() - clkTotal;
+ Res_ManFree( p );
+
// check the resulting network
if ( !Abc_NtkCheck( pNtk ) )
{
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-20 08:52:37 +0000