diff options
Diffstat (limited to 'src/aig/fra/fraCore.c')
-rw-r--r-- | src/aig/fra/fraCore.c | 63 |
1 files changed, 60 insertions, 3 deletions
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 71e12a75..41d264bb 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -30,6 +30,63 @@ /**Function************************************************************* + Synopsis [Reports the status of the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_FraigMiterStatus( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pObjNew; + int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0; + if ( p->pData ) + return 0; + Aig_ManForEachPoSeq( p, pObj, i ) + { + pObjNew = Aig_ObjChild0(pObj); + // check if the output is constant 0 + if ( pObjNew == Aig_ManConst0(p) ) + { + CountConst0++; + continue; + } + // check if the output is constant 1 + if ( pObjNew == Aig_ManConst1(p) ) + { + CountNonConst0++; + continue; + } + // check if the output can be constant 0 + if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) ) + { + CountNonConst0++; + continue; + } + CountUndecided++; + } +/* + if ( p->pParams->fVerbose ) + { + printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) ); + printf( "Const0 = %d. ", CountConst0 ); + printf( "NonConst0 = %d. ", CountNonConst0 ); + printf( "Undecided = %d. ", CountUndecided ); + printf( "\n" ); + } +*/ + if ( CountNonConst0 ) + return 0; + if ( CountUndecided ) + return -1; + return 1; +} + +/**Function************************************************************* + Synopsis [Write speculative miter for one node.] Description [] @@ -121,9 +178,9 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) Vec_PtrPush( p->vTimeouts, pObj ); // simulate the counter-example and return the Fraig node Fra_Resimulate( p ); - assert( Fra_ClassObjRepr(pObj) != pObjRepr ); if ( Fra_ClassObjRepr(pObj) == pObjRepr ) printf( "Fra_FraigNode(): Error in class refinement!\n" ); + assert( Fra_ClassObjRepr(pObj) != pObjRepr ); } /**Function************************************************************* @@ -196,7 +253,7 @@ clk = clock(); Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 ); // collect initial states p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 ); - p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); + p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); p->nNodesBeg = Aig_ManNodeNum(pManAig); p->nRegsBeg = Aig_ManRegNum(pManAig); // perform fraig sweep @@ -228,7 +285,7 @@ p->timeTrav += clock() - clk2; } p->timeTotal = clock() - clk; // collect final stats - p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); + p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); p->nNodesEnd = Aig_ManNodeNum(pManAigNew); p->nRegsEnd = Aig_ManRegNum(pManAigNew); Fra_ManStop( p ); |