diff options
Diffstat (limited to 'src/aig/gia')
| -rw-r--r-- | src/aig/gia/gia.h | 21 | ||||
| -rw-r--r-- | src/aig/gia/giaDup.c | 85 | ||||
| -rw-r--r-- | src/aig/gia/giaHash.c | 31 | ||||
| -rw-r--r-- | src/aig/gia/giaMan.c | 4 | ||||
| -rw-r--r-- | src/aig/gia/giaSweeper.c | 169 | ||||
| -rw-r--r-- | src/aig/gia/giaUtil.c | 9 |
6 files changed, 161 insertions, 158 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 737f6a67..6dad5eb5 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -167,6 +167,12 @@ struct Gia_Man_t_ int iData2; // various user data int nAnd2Delay; // AND2 delay scaled to match delay numbers used int fVerbose; // verbose reports + // bit-parallel simulation + int iPatsPi; + Vec_Wrd_t * vSims; + Vec_Wrd_t * vSimsPi; + Vec_Int_t * vClassOld; + Vec_Int_t * vClassNew; // truth table computation for small functions int nTtVars; // truth table variables int nTtWords; // truth table words @@ -379,7 +385,7 @@ static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) ); } static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); } -static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); } +static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); } static inline int Gia_ObjLevelId( Gia_Man_t * p, int Id ) { return Vec_IntGetEntry(p->vLevels, Id); } static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjLevelId( p, Gia_ObjId(p,pObj) ); } @@ -423,6 +429,11 @@ static inline void Gia_ObjSetTimeArrivalObj( Gia_Man_t * p, Gia_Obj_t * static inline void Gia_ObjSetTimeRequiredObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeRequired( p, Gia_ObjId(p, pObj), t ); } static inline void Gia_ObjSetTimeSlackObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeSlack( p, Gia_ObjId(p, pObj), t ); } +static inline int Gia_ObjSimWords( Gia_Man_t * p ) { return Vec_WrdSize( p->vSimsPi ) / Gia_ManPiNum( p ); } +static inline word * Gia_ObjSimPi( Gia_Man_t * p, int PiId ) { return Vec_WrdEntryP( p->vSimsPi, PiId * Gia_ObjSimWords(p) ); } +static inline word * Gia_ObjSim( Gia_Man_t * p, int Id ) { return Vec_WrdEntryP( p->vSims, Id * Gia_ObjSimWords(p) ); } +static inline word * Gia_ObjSimObj( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjSim( p, Gia_ObjId(p, pObj) ); } + // AIG construction extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); static inline Gia_Obj_t * Gia_ManAppendObj( Gia_Man_t * p ) @@ -755,6 +766,8 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) #define Gia_ManForEachAnd( p, pObj, i ) \ for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else +#define Gia_ManForEachCand( p, pObj, i ) \ + for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsCand(pObj) ) {} else #define Gia_ManForEachAndReverse( p, pObj, i ) \ for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) if ( !Gia_ObjIsAnd(pObj) ) {} else #define Gia_ManForEachCi( p, pObj, i ) \ @@ -837,6 +850,7 @@ extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, int nFrames ); extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm ); extern void Gia_ManDupAppend( Gia_Man_t * p, Gia_Man_t * pTwo ); +extern void Gia_ManDupAppendShare( Gia_Man_t * p, Gia_Man_t * pTwo ); extern Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo ); extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ); @@ -859,6 +873,7 @@ extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ); extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ); extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ); +extern Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p ); /*=== giaEnable.c ==========================================================*/ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose ); @@ -921,6 +936,7 @@ extern int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash ); extern void Gia_ManHashProfile( Gia_Man_t * p ); extern int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 ); +extern int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits ); /*=== giaIf.c ===========================================================*/ extern void Gia_ManPrintMappingStats( Gia_Man_t * p ); extern void Gia_ManPrintPackingStats( Gia_Man_t * p ); @@ -1015,7 +1031,7 @@ extern int Gia_SweeperCheckEquiv( Gia_Man_t * p, int ProbeId1, i extern Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vInNames, Vec_Ptr_t * vOutNames ); extern Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime ); extern Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc ); -extern Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime ); +extern Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int nWords, int nConfs, int fVerbose ); /*=== giaSwitch.c ============================================================*/ extern float Gia_ManEvaluateSwitching( Gia_Man_t * p ); extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne ); @@ -1075,6 +1091,7 @@ extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ); extern void Gia_ManPrint( Gia_Man_t * p ); extern void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj ); extern void Gia_ManInvertConstraints( Gia_Man_t * pAig ); +extern void Gia_ManInvertPos( Gia_Man_t * pAig ); extern int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 ); extern void Gia_ManMarkFanoutDrivers( Gia_Man_t * p ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 74867eff..78aac33c 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -577,7 +577,7 @@ void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo ) if ( pNew->nRegs > 0 ) pNew->nRegs = 0; if ( pNew->pHTable == NULL ) - Gia_ManHashAlloc( pNew ); + Gia_ManHashStart( pNew ); Gia_ManConst0(pTwo)->Value = 0; Gia_ManForEachObj1( pTwo, pObj, i ) { @@ -589,19 +589,24 @@ void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); } } - - -/**Function************************************************************* - - Synopsis [Append second AIG on top of the first with the permutation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ +void Gia_ManDupAppendShare( Gia_Man_t * pNew, Gia_Man_t * pTwo ) +{ + Gia_Obj_t * pObj; + int i; + assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(pTwo) ); + if ( pNew->pHTable == NULL ) + Gia_ManHashStart( pNew ); + Gia_ManConst0(pTwo)->Value = 0; + Gia_ManForEachObj1( pTwo, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_Obj2Lit( pNew, Gia_ManCi( pNew, Gia_ObjCioId(pObj) ) ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } +} Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo ) { Gia_Man_t * pNew; @@ -2185,6 +2190,58 @@ Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ) } +/**Function************************************************************* + + Synopsis [Generates AIG representing 1-hot condition for N inputs.] + + Description [The condition is true of all POs are 0.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManOneHot( int nSkips, int nVars ) +{ + Gia_Man_t * p; + int i, b, Shift, iGiaLit, nLogVars = Abc_Base2Log( nVars ); + int * pTemp = ABC_CALLOC( int, (1 << nLogVars) ); + p = Gia_ManStart( nSkips + 4 * nVars + 1 ); + p->pName = Abc_UtilStrsav( "onehot" ); + for ( i = 0; i < nSkips; i++ ) + Gia_ManAppendCi( p ); + for ( i = 0; i < nVars; i++ ) + pTemp[i] = Gia_ManAppendCi( p ); + Gia_ManHashStart( p ); + for ( b = 0; b < nLogVars; b++ ) + for ( i = 0, Shift = (1<<b); i < (1 << nLogVars); i += 2*Shift ) + { + iGiaLit = Gia_ManHashAnd( p, pTemp[i], pTemp[i + Shift] ); + if ( iGiaLit ) + Gia_ManAppendCo( p, iGiaLit ); + pTemp[i] = Gia_ManHashOr( p, pTemp[i], pTemp[i + Shift] ); + } + Gia_ManHashStop( p ); + Gia_ManAppendCo( p, Abc_LitNot(pTemp[0]) ); + ABC_FREE( pTemp ); + assert( Gia_ManObjNum(p) <= nSkips + 4 * nVars + 1 ); + return p; +} +Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p ) +{ + Gia_Man_t * pOneHot, * pNew = Gia_ManDup( p ); + if ( Gia_ManRegNum(pNew) == 0 ) + { + Abc_Print( 0, "Appending 1-hotness constraints to the PIs.\n" ); + pOneHot = Gia_ManOneHot( 0, Gia_ManCiNum(pNew) ); + } + else + pOneHot = Gia_ManOneHot( Gia_ManPiNum(pNew), Gia_ManRegNum(pNew) ); + Gia_ManDupAppendShare( pNew, pOneHot ); + pNew->nConstrs += Gia_ManPoNum(pOneHot); + Gia_ManStop( pOneHot ); + return pNew; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c index 4ae01f06..81980b40 100644 --- a/src/aig/gia/giaHash.c +++ b/src/aig/gia/giaHash.c @@ -625,6 +625,37 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash ) } +/**Function************************************************************* + + Synopsis [Creates well-balanced AND gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits ) +{ + if ( Vec_IntSize(vLits) == 0 ) + return 0; + while ( Vec_IntSize(vLits) > 1 ) + { + int i, k = 0, Lit1, Lit2, LitRes; + Vec_IntForEachEntryDouble( vLits, Lit1, Lit2, i ) + { + LitRes = Gia_ManHashAnd( p, Lit1, Lit2 ); + Vec_IntWriteEntry( vLits, k++, LitRes ); + } + if ( Vec_IntSize(vLits) & 1 ) + Vec_IntWriteEntry( vLits, k++, Vec_IntEntryLast(vLits) ); + Vec_IntShrink( vLits, k ); + } + assert( Vec_IntSize(vLits) == 1 ); + return Vec_IntEntry(vLits, 0); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 732a5075..75a0f801 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -77,6 +77,10 @@ void Gia_ManStop( Gia_Man_t * p ) assert( p->pManTime == NULL ); Vec_PtrFreeFree( p->vNamesIn ); Vec_PtrFreeFree( p->vNamesOut ); + Vec_IntFreeP( &p->vClassNew ); + Vec_IntFreeP( &p->vClassOld ); + Vec_WrdFreeP( &p->vSims ); + Vec_WrdFreeP( &p->vSimsPi ); Vec_FltFreeP( &p->vTiming ); Vec_VecFreeP( &p->vClockDoms ); Vec_IntFreeP( &p->vLutConfigs ); diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c index 844c3e45..3f597982 100644 --- a/src/aig/gia/giaSweeper.c +++ b/src/aig/gia/giaSweeper.c @@ -21,6 +21,7 @@ #include "gia.h" #include "base/main/main.h" #include "sat/bsat/satSolver.h" +#include "proof/ssc/ssc.h" ABC_NAMESPACE_IMPL_START @@ -965,62 +966,6 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * /**Function************************************************************* - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_SweeperGen64Patterns( Gia_Man_t * pGiaCond, Vec_Wrd_t * vSim ) -{ - Vec_Int_t * vCex; - int i, k; - for ( i = 0; i < 64; i++ ) - { - if ( Gia_SweeperCondCheckUnsat( pGiaCond ) != 0 ) - return 0; - vCex = Gia_SweeperGetCex( pGiaCond ); - for ( k = 0; k < Gia_ManPiNum(pGiaCond); k++ ) - { - if ( Vec_IntEntry(vCex, k) ) - Abc_InfoXorBit( (unsigned *)Vec_WrdEntryP(vSim, i), k ); - printf( "%d", Vec_IntEntry(vCex, k) ); - } - printf( "\n" ); - } - return 1; -} -int Gia_SweeperSimulate( Gia_Man_t * p, Vec_Wrd_t * vSim ) -{ - Gia_Obj_t * pObj; - word Sim, Sim0, Sim1; - int i, Count = 0; - assert( Vec_WrdEntry(vSim, 0) == 0 ); -// assert( Vec_WrdEntry(vSim, 1) != 0 ); // may not hold - Gia_ManForEachAnd( p, pObj, i ) - { - Sim0 = Vec_WrdEntry( vSim, Gia_ObjFaninId0p( p, pObj ) ); - Sim1 = Vec_WrdEntry( vSim, Gia_ObjFaninId1p( p, pObj ) ); - Sim = (Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0) & (Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1); - Vec_WrdWriteEntry( vSim, i, Sim ); - if ( pObj->fMark0 == 1 ) // considered - continue; - if ( pObj->fMark1 == 1 ) // non-constant - continue; - if ( (pObj->fPhase ? ~Sim : Sim) != 0 ) - { - pObj->fMark1 = 1; - Count++; - } - } - return Count; -} - -/**Function************************************************************* - Synopsis [Performs conditional sweeping of the cone.] Description [Returns the result as a new GIA manager with as many inputs @@ -1031,16 +976,15 @@ int Gia_SweeperSimulate( Gia_Man_t * p, Vec_Wrd_t * vSim ) SeeAlso [] ***********************************************************************/ -void Gia_SweeperSweepInt( Gia_Man_t * pGiaCond, Gia_Man_t * pGiaOuts, Vec_Wrd_t * vSim ) -{ -} -Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts ) +Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords, int nConfs, int fVerbose ) { - Gia_Man_t * pGiaCond, * pGiaOuts; Vec_Int_t * vProbeConds; - Vec_Wrd_t * vSim; - Gia_Obj_t * pObj; - int i, Count; + Gia_Man_t * pGiaCond, * pGiaOuts, * pGiaRes; + Ssc_Pars_t Pars, * pPars = &Pars; + Ssc_ManSetDefaultParams( pPars ); + pPars->nWords = nWords; + pPars->nBTLimit = nConfs; + pPars->fVerbose = fVerbose; // sweeper is running assert( Gia_SweeperIsRunning(p) ); // extract conditions and logic cones @@ -1048,22 +992,11 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts ) pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL ); pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL ); Gia_ManSetPhase( pGiaOuts ); - // start the sweeper for the conditions - Gia_SweeperStart( pGiaCond ); - Gia_ManForEachPo( pGiaCond, pObj, i ) - Gia_SweeperCondPush( pGiaCond, Gia_SweeperProbeCreate(pGiaCond, Gia_ObjFaninLit0p(pGiaCond, pObj)) ); - // generate 64 patterns that satisfy the conditions - vSim = Vec_WrdStart( Gia_ManObjNum(pGiaOuts) ); - Gia_SweeperGen64Patterns( pGiaCond, vSim ); - Count = Gia_SweeperSimulate( pGiaOuts, vSim ); - printf( "Disproved %d nodes.\n", Count ); - - // consider the remaining ones -// Gia_SweeperSweepInt( pGiaCond, pGiaOuts, vSim ); - Vec_WrdFree( vSim ); + // perform sweeping under constraints + pGiaRes = Ssc_PerformSweeping( pGiaOuts, pGiaCond, pPars ); + Gia_ManStop( pGiaCond ); Gia_ManStop( pGiaOuts ); - Gia_SweeperStop( pGiaCond ); - return pGiaCond; + return pGiaRes; } /**Function************************************************************* @@ -1085,14 +1018,14 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime ) +Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int nWords, int nConfs, int fVerbose ) { Gia_Man_t * pNew; Vec_Int_t * vLits; // sweeper is running assert( Gia_SweeperIsRunning(p) ); // sweep the logic - pNew = Gia_SweeperSweep( p, vProbeIds ); + pNew = Gia_SweeperSweep( p, vProbeIds, nWords, nConfs, fVerbose ); // execute command line if ( pCommLime ) { @@ -1110,37 +1043,6 @@ Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pComm /**Function************************************************************* - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManCreateAndGate( Gia_Man_t * p, Vec_Int_t * vLits ) -{ - if ( Vec_IntSize(vLits) == 0 ) - return 0; - while ( Vec_IntSize(vLits) > 1 ) - { - int i, k = 0, Lit1, Lit2, LitRes; - Vec_IntForEachEntryDouble( vLits, Lit1, Lit2, i ) - { - LitRes = Gia_ManHashAnd( p, Lit1, Lit2 ); - Vec_IntWriteEntry( vLits, k++, LitRes ); - } - if ( Vec_IntSize(vLits) & 1 ) - Vec_IntWriteEntry( vLits, k++, Vec_IntEntryLast(vLits) ); - Vec_IntShrink( vLits, k ); - } - assert( Vec_IntSize(vLits) == 1 ); - return Vec_IntEntry(vLits, 0); -} - -/**Function************************************************************* - Synopsis [Sweeper sweeper test.] Description [] @@ -1150,43 +1052,30 @@ int Gia_ManCreateAndGate( Gia_Man_t * p, Vec_Int_t * vLits ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ) +Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * pInit, int nWords, int nConfs, int fVerbose ) { - Gia_Man_t * pGia; + Gia_Man_t * p, * pGia; Gia_Obj_t * pObj; - Vec_Int_t * vLits, * vOuts; - int i, k, Lit; - + Vec_Int_t * vOuts; + int i; + // add one-hotness constraints + p = Gia_ManDupOneHot( pInit ); // create sweeper Gia_SweeperStart( p ); - - // create 1-hot constraint - vLits = Vec_IntAlloc( 1000 ); - for ( i = 0; i < Gia_ManPiNum(p); i++ ) - for ( k = i+1; k < Gia_ManPiNum(p); k++ ) - { - int Lit0 = Gia_Obj2Lit(p, Gia_ManPi(p, i)); - int Lit1 = Gia_Obj2Lit(p, Gia_ManPi(p, k)); - Vec_IntPush( vLits, Abc_LitNot(Gia_ManHashAnd(p, Lit0, Lit1)) ); - } - Lit = 0; - for ( i = 0; i < Gia_ManPiNum(p); i++ ) - Lit = Gia_ManHashOr( p, Lit, Gia_Obj2Lit(p, Gia_ManPi(p, i)) ); - Vec_IntPush( vLits, Lit ); - Gia_SweeperCondPush( p, Gia_SweeperProbeCreate( p, Gia_ManCreateAndGate( p, vLits ) ) ); - Vec_IntFree( vLits ); -//Gia_ManPrint( p ); - - // create outputs + // collect outputs and create conditions vOuts = Vec_IntAlloc( Gia_ManPoNum(p) ); Gia_ManForEachPo( p, pObj, i ) - Vec_IntPush( vOuts, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) ); - + if ( i < Gia_ManPoNum(p) - p->nConstrs ) // this is the user's output + Vec_IntPush( vOuts, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) ); + else // this is a constraint + Gia_SweeperCondPush( p, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) ); // perform the sweeping - pGia = Gia_SweeperSweep( p, vOuts ); + pGia = Gia_SweeperSweep( p, vOuts, nWords, nConfs, fVerbose ); +// pGia = Gia_ManDup( p ); Vec_IntFree( vOuts ); - + // sop the sweeper Gia_SweeperStop( p ); + Gia_ManStop( p ); return pGia; } diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 5adf9ebd..6f4389a8 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1163,10 +1163,15 @@ void Gia_ManInvertConstraints( Gia_Man_t * pAig ) if ( Gia_ManConstrNum(pAig) == 0 ) return; Gia_ManForEachPo( pAig, pObj, i ) - { if ( i >= Gia_ManPoNum(pAig) - Gia_ManConstrNum(pAig) ) Gia_ObjFlipFaninC0( pObj ); - } +} +void Gia_ManInvertPos( Gia_Man_t * pAig ) +{ + Gia_Obj_t * pObj; + int i; + Gia_ManForEachPo( pAig, pObj, i ) + Gia_ObjFlipFaninC0( pObj ); } /**Function************************************************************* |