diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/llb/llb1Cluster.c | 2 | ||||
-rw-r--r-- | src/aig/llb/llb4Image.c | 2 | ||||
-rw-r--r-- | src/aig/llb/llb4Nonlin.c | 45 | ||||
-rw-r--r-- | src/aig/llb/llbInt.h | 8 | ||||
-rw-r--r-- | src/aig/llb/module.make | 4 |
5 files changed, 38 insertions, 23 deletions
diff --git a/src/aig/llb/llb1Cluster.c b/src/aig/llb/llb1Cluster.c index 8a41fe58..758994b5 100644 --- a/src/aig/llb/llb1Cluster.c +++ b/src/aig/llb/llb1Cluster.c @@ -11,7 +11,7 @@ Author [Alan Mishchenko] Affiliation [UC Berkeley] - + Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: llb1Cluster.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] diff --git a/src/aig/llb/llb4Image.c b/src/aig/llb/llb4Image.c index acc34b22..031c8830 100644 --- a/src/aig/llb/llb4Image.c +++ b/src/aig/llb/llb4Image.c @@ -847,7 +847,7 @@ Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vV //Extra_bddPrintSupport( p->dd, pPart->bFunc ); printf( "\n" ); } Llb_Nonlin4Free( p ); -Abc_PrintTime( 1, "Reparametrization time", clock() - clk ); +//Abc_PrintTime( 1, "Reparametrization time", clock() - clk ); return vGroups; } diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c index 5659f25a..b153c8af 100644 --- a/src/aig/llb/llb4Nonlin.c +++ b/src/aig/llb/llb4Nonlin.c @@ -675,15 +675,20 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) p->bBad = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder, p->pPars->fBackward ); Cudd_Ref( p->bBad ); } // create init state - p->bCurrent = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder ); - if ( p->bCurrent == NULL ) + if ( p->pPars->fCluster ) + p->bCurrent = p->dd->bFunc, p->dd->bFunc = NULL; + else { - if ( !p->pPars->fSilent ) - printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit ); - p->pPars->iFrame = -1; - return -1; + p->bCurrent = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder ); + if ( p->bCurrent == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit ); + p->pPars->iFrame = -1; + return -1; + } + Cudd_Ref( p->bCurrent ); } - Cudd_Ref( p->bCurrent ); // remap into the next states p->bCurrent = Cudd_bddVarMap( p->dd, bAux = p->bCurrent ); if ( p->bCurrent == NULL ) @@ -702,16 +707,23 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) // create bad state in the ring manager if ( !p->pPars->fSkipOutCheck ) { - p->bBad = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder ); - if ( p->bBad == NULL ) + if ( p->pPars->fCluster ) + p->bBad = p->dd->bFunc, p->dd->bFunc = NULL; + else { - if ( !p->pPars->fSilent ) - printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit ); - p->pPars->iFrame = -1; - return -1; + p->bBad = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder ); + if ( p->bBad == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit ); + p->pPars->iFrame = -1; + return -1; + } + Cudd_Ref( p->bBad ); } - Cudd_Ref( p->bBad ); } + else if ( p->dd->bFunc ) + Cudd_RecursiveDeref( p->dd, p->dd->bFunc ), p->dd->bFunc = NULL; // compute the starting set of states p->bCurrent = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder, p->pPars->fBackward ); Cudd_Ref( p->bCurrent ); } @@ -925,8 +937,9 @@ Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) if ( pPars->fCluster ) { - Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose ); - Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); +// Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose ); +// Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); + Llb4_Nonlin4Sweep( p->pAig, pPars->nBddMax, pPars->nClusterMax, &p->dd, &p->vOrder, &p->vRoots, pPars->fVerbose ); } else { diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h index 23eb455e..ce62f79b 100644 --- a/src/aig/llb/llbInt.h +++ b/src/aig/llb/llbInt.h @@ -136,7 +136,7 @@ extern void Llb_MtrVerifyMatrix( Llb_Mtr_t * p ); extern Llb_Mtr_t * Llb_MtrCreate( Llb_Man_t * p ); extern void Llb_MtrFree( Llb_Mtr_t * p ); extern void Llb_MtrPrint( Llb_Mtr_t * p, int fOrder ); -extern void Llb_MtrPrintMatrixStats( Llb_Mtr_t * p ); +extern void Llb_MtrPrintMatrixStats( Llb_Mtr_t * p ); /*=== llbPart.c ======================================================*/ extern Llb_Grp_t * Llb_ManGroupAlloc( Llb_Man_t * pMan ); extern void Llb_ManGroupStop( Llb_Grp_t * p ); @@ -188,7 +188,7 @@ extern DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * /*=== llb4Cex.c =======================================================*/ extern Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int fVerbose ); /*=== llb4Cluster.c =======================================================*/ -extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose ); +//extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose ); /*=== llb4Image.c =======================================================*/ extern DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q ); extern Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax ); @@ -196,7 +196,9 @@ extern Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec //extern Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin ); /*=== llb4Nonlin.c ======================================================*/ extern int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ); - +/*=== llb4Sweep.c ======================================================*/ +extern void Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nSweepMax, int nClusterMax, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int fVerbose ); + ABC_NAMESPACE_HEADER_END diff --git a/src/aig/llb/module.make b/src/aig/llb/module.make index 29b07700..1e8ea974 100644 --- a/src/aig/llb/module.make +++ b/src/aig/llb/module.make @@ -18,6 +18,6 @@ SRC += src/aig/llb/llb.c \ src/aig/llb/llb3Image.c \ src/aig/llb/llb3Nonlin.c \ src/aig/llb/llb4Cex.c \ - src/aig/llb/llb4Cluster.c \ src/aig/llb/llb4Image.c \ - src/aig/llb/llb4Nonlin.c + src/aig/llb/llb4Nonlin.c \ + src/aig/llb/llb4Sweep.c |