From d527f03a2789e2fc2d66bb055f4e880ca864b27d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 4 Jun 2014 11:13:40 -0700 Subject: Adding CEC command &splitprove. --- src/proof/cec/cecSplit.c | 111 +++++++++++++++++++++++++---------------------- 1 file changed, 59 insertions(+), 52 deletions(-) diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c index e8319159..6dedbe0f 100644 --- a/src/proof/cec/cecSplit.c +++ b/src/proof/cec/cecSplit.c @@ -115,6 +115,37 @@ void Gia_ManBuildBddTest( Gia_Man_t * p ) #endif // BDD code +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_GiaSplitExplore( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj, * pFan0, * pFan1; + int i, Counter = 0; + assert( p->pMuxes == NULL ); + ABC_FREE( p->pRefs ); + Gia_ManCreateRefs( p ); + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) + continue; + if ( Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) > 1 && + Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) > 1 ) + continue; + printf( "%5d : ", Counter++ ); + printf( "%2d %2d ", Gia_ObjRefNum(p, Gia_Regular(pFan0)), Gia_ObjRefNum(p, Gia_Regular(pFan1)) ); + printf( "%2d %2d \n", Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)), Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) ); + } +} + /**Function************************************************************* Synopsis [Permute primary inputs.] @@ -126,6 +157,18 @@ void Gia_ManBuildBddTest( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ +int Gia_SplitCofVar( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, iBest = -1, CostBest = -1; + if ( p->pRefs == NULL ) + Gia_ManCreateRefs( p ); + Gia_ManForEachPi( p, pObj, i ) + if ( CostBest < Gia_ObjRefNum(p, pObj) ) + iBest = i, CostBest = Gia_ObjRefNum(p, pObj); + assert( iBest >= 0 ); + return iBest; +} int * Gia_PermuteSpecialOrder( Gia_Man_t * p ) { Vec_Int_t * vPerm; @@ -150,40 +193,6 @@ Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p ) return pNew; } - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_GiaSplitExplore( Gia_Man_t * p ) -{ - Gia_Obj_t * pObj, * pFan0, * pFan1; - int i, Counter = 0; - assert( p->pMuxes == NULL ); - ABC_FREE( p->pRefs ); - Gia_ManCreateRefs( p ); - Gia_ManForEachAnd( p, pObj, i ) - { - if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) - continue; - if ( Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) > 1 && - Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) > 1 ) - continue; - printf( "%5d : ", Counter++ ); - printf( "%2d %2d ", Gia_ObjRefNum(p, Gia_Regular(pFan0)), Gia_ObjRefNum(p, Gia_Regular(pFan1)) ); - printf( "%2d %2d \n", Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)), Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) ); - } -} - - - /**Function************************************************************* Synopsis [] @@ -289,10 +298,20 @@ void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fSatUns printf( "SatVar =%10d ", nVars ); printf( "SatConf =%7d ", nConfs ); printf( "%s ", fSatUnsat ? "UNSAT " : "UNDECIDED" ); - printf( "Progress = %.9f ", Prog ); + printf( "Progress = %.10f ", Prog ); Abc_PrintTime( 1, "Time", clk ); //ABC_PRTr( "Time", Abc_Clock()-clk ); } +void Cec_GiaSplitPrintRefs( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i; + if ( p->pRefs == NULL ) + Gia_ManCreateRefs( p ); + Gia_ManForEachPi( p, pObj, i ) + printf( "%d ", Gia_ObjRefNum(p, pObj) ); + printf( "\n" ); +} /**Function************************************************************* @@ -309,25 +328,12 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose ) { abctime clk, clkTotal = Abc_Clock(); Gia_Man_t * pPart0, * pPart1, * pLast; - Gia_Obj_t * pObj; Vec_Ptr_t * vStack; - int * pOrder, RetValue = -1; int nSatVars, nSatConfs, fSatUnsat; - int i, nIter, iVar, Depth; + int nIter, iVar, Depth, RetValue = -1; double Progress = 0; // create local copy p = Gia_ManDup( p ); - // reorder variables - pOrder = Gia_PermuteSpecialOrder( p ); - if ( fVerbose ) - { - Gia_ManForEachPi( p, pObj, i ) - printf( "%d ", Gia_ObjRefNum(p, pObj) ); - printf( "\n" ); - Gia_ManForEachPi( p, pObj, i ) - printf( "%d ", Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])) ); - printf( "\n" ); - } // start cofactored variables assert( p->vCofVars == NULL ); p->vCofVars = Vec_IntAlloc( 100 ); @@ -345,8 +351,8 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose ) // get the last AIG pLast = (Gia_Man_t *)Vec_PtrPop( vStack ); // determine cofactoring variable + iVar = Gia_SplitCofVar( pLast ); Depth = Vec_IntSize(pLast->vCofVars); - iVar = pOrder[Depth]; // cofactor pPart0 = Gia_ManDupCofactor( pLast, iVar, 0 ); // create variable @@ -365,6 +371,8 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose ) fSatUnsat = (fSatUnsat == Vec_PtrSize(vStack)); if ( fSatUnsat ) Progress += 1.0 / pow(2, Depth + 1); + else + Cec_GiaSplitPrintRefs( pPart0 ); if ( fVerbose ) Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk ); // cofactor @@ -387,7 +395,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose ) Progress += 1.0 / pow(2, Depth + 1); if ( fVerbose ) Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk ); -// if ( Vec_PtrSize(vStack) > 2 ) +// if ( Vec_PtrSize(vStack) > 5 ) // break; } if ( Vec_PtrSize(vStack) == 0 ) @@ -401,7 +409,6 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose ) else if ( RetValue == -1 ) printf( "Problem is UNDECIDED " ); else assert( 0 ); - ABC_FREE( pOrder ); Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); return RetValue; } -- cgit v1.2.3