diff options
Diffstat (limited to 'src/aig/fra')
-rw-r--r-- | src/aig/fra/fra.h | 1 | ||||
-rw-r--r-- | src/aig/fra/fraHot.c | 43 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 10 |
3 files changed, 54 insertions, 0 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index cc64b024..48588eb2 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -297,6 +297,7 @@ extern int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * extern int Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots ); extern void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots ); extern Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots ); +extern void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots ); /*=== fraImp.c ========================================================*/ extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr ); extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums ); diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c index 4a3f9b03..222f5bcc 100644 --- a/src/aig/fra/fraHot.c +++ b/src/aig/fra/fraHot.c @@ -420,6 +420,49 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots ) return pNew; } + +/**Function************************************************************* + + Synopsis [Assumes one-hot implications in the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +**********************************************************************/ +void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots ) +{ + Vec_Int_t * vGroup; + Aig_Obj_t * pObj1, * pObj2; + int k, i, j, Out1, Out2, pLits[2]; + // + // these constrants should be added to different timeframes! + // (also note that PIs follow first - then registers) + // + Vec_PtrForEachEntry( vOnehots, vGroup, k ) + { + Vec_IntForEachEntry( vGroup, Out1, i ) + Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 ) + { + pObj1 = Aig_ManPi( p->pManFraig, Out1 ); + pObj2 = Aig_ManPi( p->pManFraig, Out2 ); + pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 ); + pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 ); + // add contraint to solver + if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) ) + { + printf( "Fra_OneHotAddKnownConstraint(): Adding clause makes SAT solver unsat.\n" ); + sat_solver_delete( p->pSat ); + p->pSat = NULL; + return; + } + } + } +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 0715524e..7e0d080c 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -253,6 +253,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) int * pMapBack; int i, nCountPis, nCountRegs; int nClasses, nPartSize, fVerbose; + int clk = clock(); // save parameters nPartSize = pPars->nPartSize; pPars->nPartSize = 0; @@ -281,6 +282,9 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) Vec_PtrForEachEntry( vResult, vPart, i ) { pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack ); + // create the projection of 1-hot registers + if ( pAig->vOnehots ) + pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose ); // run SSW pNew = Fra_FraigInduction( pTemp, pPars ); nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack ); @@ -299,6 +303,10 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) Vec_VecFree( (Vec_Vec_t *)vResult ); pPars->nPartSize = nPartSize; pPars->fVerbose = fVerbose; + if ( fVerbose ) + { + PRT( "Total time", clock() - clk ); + } return pNew; } @@ -485,6 +493,8 @@ p->timeTrav += clock() - clk2; // add one-hotness clauses if ( p->pPars->fUse1Hot ) Fra_OneHotAssume( p, p->vOneHots ); +// if ( p->pManAig->vOnehots ) +// Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots ); // report the intermediate results if ( pPars->fVerbose ) |