diff options
Diffstat (limited to 'src/aig/fra/fraInd.c')
-rw-r--r-- | src/aig/fra/fraInd.c | 56 |
1 files changed, 40 insertions, 16 deletions
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 4a7d7b7e..76cadd0f 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -198,13 +198,14 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter ) +Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ) { Fra_Man_t * p; Fra_Par_t Pars, * pPars = &Pars; Aig_Obj_t * pObj; Cnf_Dat_t * pCnf; Aig_Man_t * pManAigNew; +// Vec_Int_t * vImps; int nIter, i, clk = clock(), clk2; if ( Aig_ManNodeNum(pManAig) == 0 ) @@ -223,15 +224,26 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, pPars->fVerbose = fVerbose; pPars->fRewrite = fRewrite; pPars->fLatchCorr = fLatchCorr; + pPars->fUseImps = fUseImps; // start the fraig manager for this run p = Fra_ManStart( pManAig, pPars ); // derive and refine e-classes using K initialized frames -// if ( fLatchCorr ) -// Fra_ClassesLatchCorr( p ); -// else - Fra_Simulate( p, 1 ); - // refine e-classes using sequential simulation? +// p->pSml = Fra_SmlStart( pManAig, pPars->nFramesK + 1, pPars->nSimWords ); +// Fra_SmlSimulate( p, 1 ); + + // remember that strange bug: r iscas/blif/s5378.blif ; st; ssw -F 4; sec -F 10 + // refine the classes with more simulation rounds + p->pSml = Fra_SmlSimulateSeq( pManAig, 32, 2 ); + Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr ); +// Fra_ClassesPostprocess( p->pCla ); + // allocate new simulation manager for simulating counter-examples + Fra_SmlStop( p->pSml ); + p->pSml = Fra_SmlStart( pManAig, pPars->nFramesK + 1, pPars->nSimWords ); + + // select the most expressive implications + if ( pPars->fUseImps ) + p->pCla->vImps = Fra_ImpDerive( p, 5000000, 5000, pPars->fLatchCorr ); p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 ); p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); @@ -251,18 +263,13 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, // perform AIG rewriting if ( p->pPars->fRewrite ) Fra_FraigInductionRewrite( p ); - // report the intermediate results - if ( fVerbose ) - { - printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. N = %6d. NR = %6d.\n", - nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), - Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts, - Aig_ManNodeNum(p->pManAig), Aig_ManNodeNum(p->pManFraig) ); - } + // bug: r iscas/blif/s1238.blif ; st; ssw -v // convert the manager to SAT solver (the last nLatches outputs are inputs) -// pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); - pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); + if ( pPars->fUseImps ) + pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); + else + pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); p->pSat = Cnf_DataWriteIntoSolver( pCnf ); @@ -270,6 +277,12 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, assert( p->pSat != NULL ); if ( p->pSat == NULL ) printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" ); + if ( pPars->fUseImps ) + { + Fra_ImpAddToSolver( p, p->pCla->vImps, pCnf->pVarNums ); + if ( p->pSat == NULL ) + printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" ); + } // set the pointers to the manager Aig_ManForEachObj( p->pManFraig, pObj, i ) @@ -295,9 +308,20 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, } Cnf_DataFree( pCnf ); */ + // report the intermediate results + if ( fVerbose ) + { + printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. I = %6d. NR = %6d.\n", + nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), + Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts, + p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0, Aig_ManNodeNum(p->pManFraig) ); + } // perform sweeping + p->nSatCallsRecent = 0; + p->nSatCallsSkipped = 0; Fra_FraigSweep( p ); +// printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped ); assert( p->vTimeouts == NULL ); if ( p->vTimeouts ) printf( "Fra_FraigInduction(): SAT solver timed out!\n" ); |