diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-03-05 16:17:12 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-03-05 16:17:12 -0800 |
| commit | badbb5a6cc8a794bfd7c5adef62b0d6c2e583e42 (patch) | |
| tree | 2d284e41076944c65c14d0e9ab399e72b0822296 /src/aig/llb | |
| parent | edcb769b3e09cea8a8058a2abacc10c243323c7b (diff) | |
| download | abc-badbb5a6cc8a794bfd7c5adef62b0d6c2e583e42.tar.gz abc-badbb5a6cc8a794bfd7c5adef62b0d6c2e583e42.tar.bz2 abc-badbb5a6cc8a794bfd7c5adef62b0d6c2e583e42.zip | |
Fixing bugs in the new procedures added to the library.
Diffstat (limited to 'src/aig/llb')
| -rw-r--r-- | src/aig/llb/llb3Nonlin.c | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c index 1cdd2c96..6a0c871e 100644 --- a/src/aig/llb/llb3Nonlin.c +++ b/src/aig/llb/llb3Nonlin.c @@ -529,6 +529,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) clk3 = clock(); Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 ); p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) ); +// p->ddG->bFunc2 = Extra_bddAndPermute( p->ddG, Cudd_Not(p->ddG->bFunc), p->dd, bNext, Vec_IntArray(p->vNs2Glo) ); if ( p->ddG->bFunc2 == NULL ) { if ( !p->pPars->fSilent ) @@ -552,6 +553,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) p->ddLocGrbs += Cudd_ReadGarbageCollections(p->dd); Llb_NonlinImageQuit(); p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 0 ); + //Extra_TestAndPerm( p->ddG, Cudd_Not(p->ddG->bFunc), p->ddG->bFunc2 ); // derive new states clk3 = clock(); @@ -567,9 +569,12 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) } Cudd_Ref( p->ddG->bFunc2 ); Cudd_RecursiveDeref( p->ddG, bTemp ); + p->timeGloba += clock() - clk3; + if ( Cudd_IsConstant(p->ddG->bFunc2) ) break; // add to the reached set + clk3 = clock(); p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 ); if ( p->ddG->bFunc == NULL ) { |