From c03f9b516bed2c06ec2bfc78617eba5fc9a11c32 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 20 Feb 2009 08:01:00 -0800 Subject: Version abc90220 --- src/aig/aig/aigUtil.c | 2 + src/aig/cec/cecSolve.c | 15 +- src/aig/gia/gia.h | 7 +- src/aig/gia/giaCSat0.c | 326 ++++++++++++++++++++++++ src/aig/gia/giaCSat1.c | 602 ++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/giaCSatA.c | 103 ++++++++ src/aig/gia/giaCSatB.c | 490 ++++++++++++++++++++++++++++++++++++ src/aig/gia/giaDup.c | 56 +++-- src/aig/gia/giaEmbed.c | 525 ++++++++++++++++++++++++++++++++------ src/aig/gia/giaForce.c | 4 +- src/aig/gia/giaGlitch.c | 92 +++++-- src/aig/gia/giaHash.c | 18 ++ src/aig/gia/giaSolver.c | 490 ------------------------------------ src/aig/gia/giaSolver_cnf.c | 103 -------- src/aig/gia/giaSort.c | 151 ++++++++++- src/aig/gia/module.make | 1 + src/aig/ssw/sswCore.c | 4 +- 17 files changed, 2265 insertions(+), 724 deletions(-) create mode 100644 src/aig/gia/giaCSat0.c create mode 100644 src/aig/gia/giaCSat1.c create mode 100644 src/aig/gia/giaCSatA.c create mode 100644 src/aig/gia/giaCSatB.c delete mode 100644 src/aig/gia/giaSolver.c delete mode 100644 src/aig/gia/giaSolver_cnf.c (limited to 'src/aig') diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index b5c7272b..1852ff03 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -1084,6 +1084,8 @@ char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix ) if ( (pDot = strrchr( Buffer, '.' )) ) *pDot = 0; strcat( Buffer, pSuffix ); + if ( (pDot = strrchr( Buffer, '\\' )) || (pDot = strrchr( Buffer, '/' )) ) + return pDot+1; return Buffer; } diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c index 0ec7df45..e4daf719 100644 --- a/src/aig/cec/cecSolve.c +++ b/src/aig/cec/cecSolve.c @@ -444,7 +444,8 @@ p->timeSatUnsat += clock() - clk; RetValue = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); assert( RetValue ); p->nSatUnsat++; - p->nConfUnsat += p->pSat->stats.conflicts - nConflicts; + p->nConfUnsat += p->pSat->stats.conflicts - nConflicts; +//printf( "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); return 1; } else if ( RetValue == l_True ) @@ -452,6 +453,7 @@ p->timeSatUnsat += clock() - clk; p->timeSatSat += clock() - clk; p->nSatSat++; p->nConfSat += p->pSat->stats.conflicts - nConflicts; +//printf( "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); return 0; } else // if ( RetValue == l_Undef ) @@ -459,6 +461,7 @@ p->timeSatSat += clock() - clk; p->timeSatUndec += clock() - clk; p->nSatUndec++; p->nConfUndec += p->pSat->stats.conflicts - nConflicts; +//printf( "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); return -1; } } @@ -477,10 +480,18 @@ p->timeSatUndec += clock() - clk; ***********************************************************************/ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ) { + static int Counter; +// char Buffer[1000]; + Bar_Progress_t * pProgress = NULL; Cec_ManSat_t * p; Gia_Obj_t * pObj; int i, status, clk = clock(); + +// sprintf( Buffer, "gia%03d.aig", Counter++ ); +//Gia_WriteAiger( pAig, Buffer, 0, 0 ); +//printf( "Dumpted slice into file \"%s\".\n", Buffer ); + // reset the manager if ( pPat ) { @@ -501,6 +512,8 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar pObj->fMark1 = 1; continue; } +//printf( "Output %6d : ", i ); + Bar_ProgressUpdate( pProgress, i, "SAT..." ); status = Cec_ManSatCheckNode( p, pObj ); pObj->fMark0 = (status == 0); diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 73940ffa..b77dd76f 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -24,7 +24,7 @@ //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// - + #include "aig.h" //////////////////////////////////////////////////////////////////////// @@ -303,6 +303,8 @@ static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCom for ( i = 1; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) #define Gia_ManForEachObjVec( vVec, p, pObj, i ) \ for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Vec_IntEntry(vVec,i))); i++ ) +#define Gia_ManForEachObjVecLit( vVec, p, pObj, fCompl, i ) \ + for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Gia_Lit2Var(Vec_IntEntry(vVec,i)))) && (((fCompl) = Gia_LitIsCompl(Vec_IntEntry(vVec,i))),1); 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_ManForEachCi( p, pObj, i ) \ @@ -373,11 +375,12 @@ extern void Gia_ManHashStart( Gia_Man_t * p ); extern void Gia_ManHashStop( Gia_Man_t * p ); extern int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 ); extern int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 ); +extern int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 ); extern int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 ); extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p ); /*=== giaLogic.c ===========================================================*/ extern void Gia_ManTestDistance( Gia_Man_t * p ); -extern void Gia_ManSolveProblem( Gia_Man_t * pGia, int nDims, int nSols ); +extern void Gia_ManSolveProblem( Gia_Man_t * pGia, int nDims, int nSols, int fCluster, int fDump, int fVerbose ); /*=== giaMan.c ===========================================================*/ extern Gia_Man_t * Gia_ManStart( int nObjsMax ); extern void Gia_ManStop( Gia_Man_t * p ); diff --git a/src/aig/gia/giaCSat0.c b/src/aig/gia/giaCSat0.c new file mode 100644 index 00000000..599ad43c --- /dev/null +++ b/src/aig/gia/giaCSat0.c @@ -0,0 +1,326 @@ +/**CFile**************************************************************** + + FileName [giaCsat0.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Circuit-based SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaCsat0.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Sat_ObjXValue( Gia_Obj_t * pObj ) { return (pObj->fMark1 << 1) | pObj->fMark0; } +static inline void Sat_ObjSetXValue( Gia_Obj_t * pObj, int v) { pObj->fMark0 = (v & 1); pObj->fMark1 = ((v >> 1) & 1); } + +static inline int Sat_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->Value > 0; } +static inline void Sat_VarAssign( Gia_Obj_t * pVar, int i ) { assert(!pVar->Value); pVar->Value = i; } +static inline void Sat_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->Value); pVar->Value = 0; } +static inline int Sat_VarValue( Gia_Obj_t * pVar ) { assert(pVar->Value); return pVar->fMark0; } +static inline void Sat_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->Value); pVar->fMark0 = v; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Collects nodes in the cone and initialized them to x.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_SatCollectCone_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisit ) +{ + if ( Sat_ObjXValue(pObj) == GIA_UND ) + return; + assert( pObj->Value == 0 ); + if ( Gia_ObjIsAnd(pObj) ) + { + Gia_SatCollectCone_rec( p, Gia_ObjFanin0(pObj), vVisit ); + Gia_SatCollectCone_rec( p, Gia_ObjFanin1(pObj), vVisit ); + } + assert( Sat_ObjXValue(pObj) == 0 ); + Sat_ObjSetXValue( pObj, GIA_UND ); + Vec_IntPush( vVisit, Gia_ObjId(p, pObj) ); +} + +/**Function************************************************************* + + Synopsis [Collects nodes in the cone and initialized them to x.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_SatCollectCone( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisit ) +{ + assert( !Gia_IsComplement(pObj) ); + assert( !Gia_ObjIsConst0(pObj) ); + assert( Sat_ObjXValue(pObj) == 0 ); + Vec_IntClear( vVisit ); + Gia_SatCollectCone_rec( p, pObj, vVisit ); +} + +/**Function************************************************************* + + Synopsis [Collects nodes in the cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit ) +{ + Gia_Obj_t * pObj; + int i, Entry, Value, Value0, Value1; + assert( Gia_ObjIsCo(pRoot) ); + assert( !Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) ); + // collect nodes and initialized them to x + Gia_SatCollectCone( p, Gia_ObjFanin0(pRoot), vVisit ); + // set binary values to nodes in the counter-example + Vec_IntForEachEntry( vCex, Entry, i ) + { + pObj = Gia_NotCond( Gia_ManObj( p, Gia_Lit2Var(Entry) ), Gia_LitIsCompl(Entry) ); + Sat_ObjSetXValue( Gia_Regular(pObj), Gia_IsComplement(pObj)? GIA_ZER : GIA_ONE ); + assert( Sat_ObjXValue(Gia_Regular(pObj)) == (Gia_IsComplement(pObj)? GIA_ZER : GIA_ONE) ); + } + // simulate + Gia_ManForEachObjVec( vVisit, p, pObj, i ) + { + if ( Gia_ObjIsCi(pObj) ) + continue; + assert( Gia_ObjIsAnd(pObj) ); + Value0 = Sat_ObjXValue( Gia_ObjFanin0(pObj) ); + Value1 = Sat_ObjXValue( Gia_ObjFanin1(pObj) ); + Value = Gia_XsimAndCond( Value0, Gia_ObjFaninC0(pObj), Value1, Gia_ObjFaninC1(pObj) ); + Sat_ObjSetXValue( pObj, Value ); + } + Value = Gia_XsimNotCond( Value, Gia_ObjFaninC0(pRoot) ); + if ( Value != GIA_ONE ) + printf( "Gia_SatVerifyPattern(): Verification failed.\n" ); + assert( Value == GIA_ONE ); + // clean the nodes + Gia_ManForEachObjVec( vVisit, p, pObj, i ) + Sat_ObjSetXValue( pObj, 0 ); +} + + +/**Function************************************************************* + + Synopsis [Undoes the assignment since the given value.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_SatUndo_rec( Gia_Obj_t * pObj, unsigned Value, Vec_Int_t * vCex ) +{ + if ( pObj->Value < Value ) + return; + pObj->Value = 0; + if ( Gia_ObjIsCi(pObj) ) + { + if ( vCex ) Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pObj), !pObj->fPhase) ); + return; + } + Gia_SatUndo_rec( Gia_ObjFanin0(pObj), Value, vCex ); + Gia_SatUndo_rec( Gia_ObjFanin1(pObj), Value, vCex ); +} + +/**Function************************************************************* + + Synopsis [Propagates assignments.] + + Description [Returns 1 if UNSAT, 0 if SAT.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_SatProp_rec( Gia_Obj_t * pObj, unsigned Phase, unsigned * pValue, int * pnConfs ) +{ + int Value = *pValue; + if ( pObj->Value ) + return pObj->fPhase != Phase; + if ( Gia_ObjIsCi(pObj) ) + { + pObj->Value = Value; + pObj->fPhase = Phase; + return 0; + } + if ( Phase ) // output of AND should be 1 + { + if ( Gia_SatProp_rec( Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), pValue, pnConfs ) ) + return 1; + if ( Gia_SatProp_rec( Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), pValue, pnConfs ) ) + { + Gia_SatUndo_rec( Gia_ObjFanin0(pObj), Value, NULL ); + return 1; + } +/* + if ( Gia_SatProp_rec( Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), pValue, pnConfs ) ) + return 1; + if ( Gia_SatProp_rec( Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), pValue, pnConfs ) ) + { + Gia_SatUndo_rec( Gia_ObjFanin1(pObj), Value, NULL ); + return 1; + } +*/ + pObj->Value = Value; + pObj->fPhase = 1; + return 0; + } + // output of AND should be 0 + + (*pValue)++; + if ( !Gia_SatProp_rec( Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj), pValue, pnConfs ) ) + { + pObj->Value = Value; + pObj->fPhase = 0; + return 0; + } + if ( !*pnConfs ) + return 1; + + (*pValue)++; + if ( !Gia_SatProp_rec( Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj), pValue, pnConfs ) ) + { + pObj->Value = Value; + pObj->fPhase = 0; + return 0; + } + if ( !*pnConfs ) + return 1; + // cannot be satisfied + (*pnConfs)--; + return 1; +} + +/**Function************************************************************* + + Synopsis [Procedure to solve SAT for the node.] + + Description [Returns 1 if UNSAT, 0 if SAT, and -1 if undecided.] + + SideEffects [Precondition: pObj->Value should be 0.] + + SeeAlso [] + +***********************************************************************/ +int Gia_SatSolve( Gia_Obj_t * pObj, unsigned Phase, int nConfsMax, Vec_Int_t * vCex ) +{ + int Value = 1; + int nConfs = nConfsMax? nConfsMax : (1<<30); + assert( !Gia_IsComplement(pObj) ); + assert( !Gia_ObjIsConst0(pObj) ); + assert( pObj->Value == 0 ); + if ( Gia_SatProp_rec( pObj, Phase, &Value, &nConfs ) ) + { +// if ( nConfs ) +// printf( "UNSAT after %d conflicts\n", nConfsMax - nConfs ); +// else +// printf( "UNDEC after %d conflicts\n", nConfsMax ); + return nConfs? 1 : -1; + } + Vec_IntClear( vCex ); + Gia_SatUndo_rec( pObj, 1, vCex ); +// printf( "SAT after %d conflicts\n", nConfsMax - nConfs ); + return 0; +} + + + +/**Function************************************************************* + + Synopsis [Procedure to test the new SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_SatSolveTest( Gia_Man_t * p ) +{ + int nConfsMax = 1000; + int CountUnsat, CountSat, CountUndec; + Vec_Int_t * vCex; + Vec_Int_t * vVisit; + Gia_Obj_t * pRoot; + int i, RetValue, clk = clock(); + // prepare AIG + Gia_ManCleanValue( p ); + Gia_ManCleanMark0( p ); + Gia_ManCleanMark1( p ); + vCex = Vec_IntAlloc( 100 ); + vVisit = Vec_IntAlloc( 100 ); + // solve for each output + CountUnsat = CountSat = CountUndec = 0; + Gia_ManForEachCo( p, pRoot, i ) + { + if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) ) + continue; +//printf( "Output %6d : ", i ); + RetValue = Gia_SatSolve( Gia_ObjFanin0(pRoot), !Gia_ObjFaninC0(pRoot), nConfsMax, vCex ); + if ( RetValue == 1 ) + CountUnsat++; + else if ( RetValue == -1 ) + CountUndec++; + else + { +// Gia_Obj_t * pTemp; +// int k; + assert( RetValue == 0 ); + CountSat++; +/* + Vec_IntForEachEntry( vCex, pTemp, k ) +// printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjCioId(Gia_Regular(pTemp)) ); + printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjId(p,Gia_Regular(pTemp)) ); + printf( "\n" ); +*/ +// Gia_SatVerifyPattern( p, pRoot, vCex, vVisit ); + } +// Gia_ManCheckMark0( p ); +// Gia_ManCheckMark1( p ); + } + Vec_IntFree( vCex ); + Vec_IntFree( vVisit ); + printf( "Unsat = %d. Sat = %d. Undec = %d. ", CountUnsat, CountSat, CountUndec ); + ABC_PRT( "Time", clock() - clk ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/gia/giaCSat1.c b/src/aig/gia/giaCSat1.c new file mode 100644 index 00000000..12b7071f --- /dev/null +++ b/src/aig/gia/giaCSat1.c @@ -0,0 +1,602 @@ +/**CFile**************************************************************** + + FileName [giaCsat1.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Circuit-based SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaCsat1.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +typedef struct Css_Fan_t_ Css_Fan_t; +struct Css_Fan_t_ +{ + unsigned iFan : 31; // ID of the fanin/fanout + unsigned fCompl : 1; // complemented attribute +}; + +typedef struct Css_Obj_t_ Css_Obj_t; +struct Css_Obj_t_ +{ + unsigned fCi : 1; // terminal node CI + unsigned fCo : 1; // terminal node CO + unsigned fAssign : 1; // assigned variable + unsigned fValue : 1; // variable value + unsigned fPhase : 1; // value under 000 pattern + unsigned nFanins : 5; // the number of fanins + unsigned nFanouts : 22; // total number of fanouts + unsigned hHandle; // application specific data + union { + unsigned iFanouts; // application specific data + int TravId; // ID of the node + }; + Css_Fan_t Fanios[0]; // the array of fanins/fanouts +}; + +typedef struct Css_Man_t_ Css_Man_t; +struct Css_Man_t_ +{ + Gia_Man_t * pGia; // the original AIG manager + Vec_Int_t * vCis; // the vector of CIs (PIs + LOs) + Vec_Int_t * vCos; // the vector of COs (POs + LIs) + int nObjs; // the number of objects + int nNodes; // the number of nodes + int * pObjData; // the logic network defined for the AIG + int nObjData; // the size of array to store the logic network + int * pLevels; // the linked lists of levels + int nLevels; // the max number of logic levels + int nTravIds; // traversal ID to mark the cones + Vec_Int_t * vTrail; // sequence of assignments + int nConfsMax; // max number of conflicts +}; + +static inline unsigned Gia_ObjHandle( Gia_Obj_t * pObj ) { return pObj->Value; } + +static inline int Css_ObjIsCi( Css_Obj_t * pObj ) { return pObj->fCi; } +static inline int Css_ObjIsCo( Css_Obj_t * pObj ) { return pObj->fCo; } +static inline int Css_ObjIsNode( Css_Obj_t * pObj ) { return!pObj->fCi &&!pObj->fCo && pObj->nFanins > 0; } +static inline int Css_ObjIsConst0( Css_Obj_t * pObj ) { return!pObj->fCi &&!pObj->fCo && pObj->nFanins == 0;} + +static inline int Css_ObjFaninNum( Css_Obj_t * pObj ) { return pObj->nFanins; } +static inline int Css_ObjFanoutNum( Css_Obj_t * pObj ) { return pObj->nFanouts; } +static inline int Css_ObjSize( Css_Obj_t * pObj ) { return sizeof(Css_Obj_t) / 4 + pObj->nFanins + pObj->nFanouts; } +static inline int Css_ObjId( Css_Obj_t * pObj ) { assert( 0 ); return -1; } + +static inline Css_Obj_t * Css_ManObj( Css_Man_t * p, unsigned iHandle ) { return (Css_Obj_t *)(p->pObjData + iHandle); } +static inline Css_Obj_t * Css_ObjFanin( Css_Obj_t * pObj, int i ) { return (Css_Obj_t *)(((int *)pObj) - pObj->Fanios[i].iFan); } +static inline Css_Obj_t * Css_ObjFanout( Css_Obj_t * pObj, int i ) { return (Css_Obj_t *)(((int *)pObj) + pObj->Fanios[pObj->nFanins+i].iFan); } +static inline int Css_ObjFaninC( Css_Obj_t * pObj, int i ) { return pObj->Fanios[i].fCompl; } +static inline int Css_ObjFanoutC( Css_Obj_t * pObj, int i ) { return pObj->Fanios[pObj->nFanins+i].fCompl; } + +static inline int Css_ManObjNum( Css_Man_t * p ) { return p->nObjs; } +static inline int Css_ManNodeNum( Css_Man_t * p ) { return p->nNodes; } + +static inline void Css_ManIncrementTravId( Css_Man_t * p ) { p->nTravIds++; } +static inline void Css_ObjSetTravId( Css_Obj_t * pObj, int TravId ) { pObj->TravId = TravId; } +static inline void Css_ObjSetTravIdCurrent( Css_Man_t * p, Css_Obj_t * pObj ) { pObj->TravId = p->nTravIds; } +static inline void Css_ObjSetTravIdPrevious( Css_Man_t * p, Css_Obj_t * pObj ) { pObj->TravId = p->nTravIds - 1; } +static inline int Css_ObjIsTravIdCurrent( Css_Man_t * p, Css_Obj_t * pObj ) { return ((int)pObj->TravId == p->nTravIds); } +static inline int Css_ObjIsTravIdPrevious( Css_Man_t * p, Css_Obj_t * pObj ) { return ((int)pObj->TravId == p->nTravIds - 1); } + +static inline int Css_VarIsAssigned( Css_Obj_t * pVar ) { return pVar->fAssign; } +static inline void Css_VarAssign( Css_Obj_t * pVar ) { assert(!pVar->fAssign); pVar->fAssign = 1; } +static inline void Css_VarUnassign( Css_Obj_t * pVar ) { assert(pVar->fAssign); pVar->fAssign = 0; } +static inline int Css_VarValue( Css_Obj_t * pVar ) { assert(pVar->fAssign); return pVar->fValue; } +static inline void Css_VarSetValue( Css_Obj_t * pVar, int v ) { assert(pVar->fAssign); pVar->fValue = v; } + +#define Css_ManForEachObj( p, pObj, i ) \ + for ( i = 0; (i < p->nObjData) && (pObj = Css_ManObj(p,i)); i += Css_ObjSize(pObj) ) +#define Css_ManForEachObjVecStart( vVec, p, pObj, i, iStart ) \ + for ( i = iStart; (i < Vec_IntSize(vVec)) && (pObj = Css_ManObj(p,Vec_IntEntry(vVec,i))); i++ ) +#define Css_ManForEachNode( p, pObj, i ) \ + for ( i = 0; (i < p->nObjData) && (pObj = Css_ManObj(p,i)); i += Css_ObjSize(pObj) ) if ( Css_ObjIsTerm(pObj) ) {} else +#define Css_ObjForEachFanin( pObj, pNext, i ) \ + for ( i = 0; (i < (int)pObj->nFanins) && (pNext = Css_ObjFanin(pObj,i)); i++ ) +#define Css_ObjForEachFanout( pObj, pNext, i ) \ + for ( i = 0; (i < (int)pObj->nFanouts) && (pNext = Css_ObjFanout(pObj,i)); i++ ) +#define Css_ObjForEachFaninLit( pObj, pNext, fCompl, i ) \ + for ( i = 0; (i < (int)pObj->nFanins) && (pNext = Css_ObjFanin(pObj,i)) && ((fCompl = Css_ObjFaninC(pObj,i)),1); i++ ) +#define Css_ObjForEachFanoutLit( pObj, pNext, fCompl, i ) \ + for ( i = 0; (i < (int)pObj->nFanouts) && (pNext = Css_ObjFanout(pObj,i)) && ((fCompl = Css_ObjFanoutC(pObj,i)),1); i++ ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates logic network isomorphic to the given AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Css_Man_t * Css_ManCreateLogicSimple( Gia_Man_t * pGia ) +{ + Css_Man_t * p; + Css_Obj_t * pObjLog, * pFanLog; + Gia_Obj_t * pObj; + int i, iHandle = 0; + p = ABC_CALLOC( Css_Man_t, 1 ); + p->pGia = pGia; + p->vCis = Vec_IntAlloc( Gia_ManCiNum(pGia) ); + p->vCos = Vec_IntAlloc( Gia_ManCoNum(pGia) ); + p->nObjData = (sizeof(Css_Obj_t) / 4) * Gia_ManObjNum(pGia) + 4 * Gia_ManAndNum(pGia) + 2 * Gia_ManCoNum(pGia); + p->pObjData = ABC_CALLOC( int, p->nObjData ); + ABC_FREE( pGia->pRefs ); + Gia_ManCreateRefs( pGia ); + Gia_ManForEachObj( pGia, pObj, i ) + { + pObj->Value = iHandle; + pObjLog = Css_ManObj( p, iHandle ); + pObjLog->nFanins = 0; + pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj ); + pObjLog->hHandle = iHandle; + pObjLog->iFanouts = 0; + if ( Gia_ObjIsAnd(pObj) ) + { + pFanLog = Css_ManObj( p, Gia_ObjHandle(Gia_ObjFanin0(pObj)) ); + pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts].iFan = + pObjLog->Fanios[pObjLog->nFanins].iFan = pObjLog->hHandle - pFanLog->hHandle; + pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts++].fCompl = + pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC0(pObj); + + pFanLog = Css_ManObj( p, Gia_ObjHandle(Gia_ObjFanin1(pObj)) ); + pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts].iFan = + pObjLog->Fanios[pObjLog->nFanins].iFan = pObjLog->hHandle - pFanLog->hHandle; + pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts++].fCompl = + pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC1(pObj); + + p->nNodes++; + } + else if ( Gia_ObjIsCo(pObj) ) + { + pFanLog = Css_ManObj( p, Gia_ObjHandle(Gia_ObjFanin0(pObj)) ); + pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts].iFan = + pObjLog->Fanios[pObjLog->nFanins].iFan = pObjLog->hHandle - pFanLog->hHandle; + pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts++].fCompl = + pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC0(pObj); + + pObjLog->fCo = 1; + Vec_IntPush( p->vCos, iHandle ); + } + else if ( Gia_ObjIsCi(pObj) ) + { + pObjLog->fCi = 1; + Vec_IntPush( p->vCis, iHandle ); + } + iHandle += Css_ObjSize( pObjLog ); + p->nObjs++; + } + assert( iHandle == p->nObjData ); + Gia_ManForEachObj( pGia, pObj, i ) + { + pObjLog = Css_ManObj( p, Gia_ObjHandle(pObj) ); + assert( pObjLog->nFanouts == pObjLog->iFanouts ); + pObjLog->TravId = 0; + } + p->nTravIds = 1; + p->vTrail = Vec_IntAlloc( 100 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Creates logic network isomorphic to the given AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Css_ManStop( Css_Man_t * p ) +{ + Vec_IntFree( p->vTrail ); + Vec_IntFree( p->vCis ); + Vec_IntFree( p->vCos ); + ABC_FREE( p->pObjData ); + ABC_FREE( p->pLevels ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Propagates implications for the net.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Css_ManImplyNet_rec( Css_Man_t * p, Css_Obj_t * pVar, unsigned Value ) +{ + static inline Css_ManImplyNode_rec( Css_Man_t * p, Css_Obj_t * pVar ); + Css_Obj_t * pNext; + int i; + if ( !Css_ObjIsTravIdCurrent(p, pVar) ) + return 0; + // assign the variable + assert( !Css_VarIsAssigned(pVar) ); + Css_VarAssign( pVar ); + Css_VarSetValue( pVar, Value ); + Vec_IntPush( p->vTrail, pVar->hHandle ); + // propagate fanouts, then fanins + Css_ObjForEachFanout( pVar, pNext, i ) + if ( Css_ManImplyNode_rec( p, pNext ) ) + return 1; + Css_ObjForEachFanin( pVar, pNext, i ) + if ( Css_ManImplyNode_rec( p, pNext ) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Propagates implications for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Css_ManImplyNode_rec( Css_Man_t * p, Css_Obj_t * pVar ) +{ + Css_Obj_t * pFan0, * pFan1; + if ( Css_ObjIsCi(pVar) ) + return 0; + pFan0 = Css_ObjFanin(pVar, 0); + pFan1 = Css_ObjFanin(pVar, 1); + if ( !Css_VarIsAssigned(pVar) ) + { + if ( Css_VarIsAssigned(pFan0) ) + { + if ( Css_VarValue(pFan0) == Css_ObjFaninC(pVar,0) ) // negative -> propagate + return Css_ManImplyNet_rec(p, pVar, 0); + // assigned positive + if ( Css_VarIsAssigned(pFan1) ) + { + if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> propagate + return Css_ManImplyNet_rec(p, pVar, 0); + // asigned positive -> propagate + return Css_ManImplyNet_rec(p, pVar, 1); + } + return 0; + } + if ( Css_VarIsAssigned(pFan1) ) + { + if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> propagate + return Css_ManImplyNet_rec(p, pVar, 0); + return 0; + } + assert( 0 ); + return 0; + } + if ( Css_VarValue(pVar) ) // positive + { + if ( Css_VarIsAssigned(pFan0) ) + { + if ( Css_VarValue(pFan0) == Css_ObjFaninC(pVar,0) ) // negative -> conflict + return 1; + // check second var + if ( Css_VarIsAssigned(pFan1) ) + { + if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> conflict + return 1; + // positive + positive -> nothing to do + return 0; + } + } + else + { + // pFan0 unassigned -> enqueue first var +// Css_ManEnqueue( p, pFan0, !Css_ObjFaninC(pVar,0) ); + if ( Css_ManImplyNet_rec( p, pFan0, !Css_ObjFaninC(pVar,0) ) ) + return 1; + // check second var + if ( Css_VarIsAssigned(pFan1) ) + { + if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> conflict + return 1; + // positive + positive -> nothing to do + return 0; + } + } + // unassigned -> enqueue second var +// Css_ManEnqueue( p, pFan1, !Css_ObjFaninC(pVar,1) ); + return Css_ManImplyNet_rec( p, pFan1, !Css_ObjFaninC(pVar,1) ); + } + else // negative + { + if ( Css_VarIsAssigned(pFan0) ) + { + if ( Css_VarValue(pFan0) == Css_ObjFaninC(pVar,0) ) // negative -> nothing to do + return 0; + if ( Css_VarIsAssigned(pFan1) ) + { + if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> nothing to do + return 0; + // positive + positive -> conflict + return 1; + } + // positive + unassigned -> enqueue second var +// Css_ManEnqueue( p, pFan1, Css_ObjFaninC(pVar,1) ); + return Css_ManImplyNet_rec( p, pFan1, Css_ObjFaninC(pVar,1) ); + } + else + { + if ( Css_VarIsAssigned(pFan1) ) + { + if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> nothing to do + return 0; + // unassigned + positive -> enqueue first var +// Css_ManEnqueue( p, pFan0, Css_ObjFaninC(pVar,0) ); + return Css_ManImplyNet_rec( p, pFan0, Css_ObjFaninC(pVar,0) ); + } + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Css_ManCancelUntil( Css_Man_t * p, int iBound, Vec_Int_t * vCex ) +{ + Css_Obj_t * pVar; + int i; + Css_ManForEachObjVecStart( p->vTrail, p, pVar, i, iBound ) + { + if ( vCex ) + Vec_IntPush( vCex, Gia_Var2Lit(Css_ObjId(pVar), !pVar->fValue) ); + Css_VarUnassign( pVar ); + } + Vec_IntShrink( p->vTrail, iBound ); +} + +/**Function************************************************************* + + Synopsis [Justifies assignments.] + + Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Css_ManJustify( Css_Man_t * p, int iBegin ) +{ + Css_Obj_t * pVar, * pFan0, * pFan1; + int iState, iThis; + if ( p->nConfsMax == 0 ) + return 1; + // get the next variable to justify + Css_ManForEachObjVecStart( p->vTrail, p, pVar, iThis, iBegin ) + { + assert( Css_VarIsAssigned(pVar) ); + if ( Css_VarValue(pVar) || Css_ObjIsCi(pVar) ) + continue; + pFan0 = Css_ObjFanin(pVar,0); + pFan1 = Css_ObjFanin(pVar,0); + if ( !Css_VarIsAssigned(pFan0) && !Css_VarIsAssigned(pFan1) ) + break; + } + if ( iThis == Vec_IntSize(p->vTrail) ) // could not find + return 0; + // found variable to justify + assert( !Css_VarValue(pVar) && !Css_VarIsAssigned(pFan0) && !Css_VarIsAssigned(pFan1) ); + // remember the state of the stack + iState = Vec_IntSize( p->vTrail ); + // try to justify by setting first fanin to 0 + if ( !Css_ManImplyNet_rec(p, pFan0, 0) && !Css_ManJustify(p, iThis) ) + return 0; + Css_ManCancelUntil( p, iState, NULL ); + if ( p->nConfsMax == 0 ) + return 1; + // try to justify by setting second fanin to 0 + if ( !Css_ManImplyNet_rec(p, pFan1, 0) && !Css_ManJustify(p, iThis) ) + return 0; + Css_ManCancelUntil( p, iState, NULL ); + if ( p->nConfsMax == 0 ) + return 1; + p->nConfsMax--; + return 1; +} + +/**Function************************************************************* + + Synopsis [Marsk logic cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Css_ManMarkCone_rec( Css_Man_t * p, Css_Obj_t * pVar ) +{ + if ( Css_ObjIsTravIdCurrent(p, pVar) ) + return; + Css_ObjSetTravIdCurrent(p, pVar); + assert( !Css_VarIsAssigned(pVar) ); + if ( Css_ObjIsCi(pVar) ) + return; + else + { + Css_Obj_t * pNext; + int i; + Css_ObjForEachFanin( pVar, pNext, i ) + Css_ManMarkCone_rec( p, pNext ); + } +} + +/**Function************************************************************* + + Synopsis [Runs one call to the SAT solver.] + + Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Css_ManPrepare( Css_Man_t * p, int * pLits, int nLits ) +{ + Css_Obj_t * pVar; + int i; + // mark the cone + Css_ManIncrementTravId( p ); + for ( i = 0; i < nLits; i++ ) + { + pVar = Css_ManObj( p, Gia_Lit2Var(pLits[i]) ); + Css_ManMarkCone_rec( p, pVar ); + } + // assign literals + Vec_IntClear( p->vTrail ); + for ( i = 0; i < nLits; i++ ) + { + pVar = Css_ManObj( p, Gia_Lit2Var(pLits[i]) ); + if ( Css_ManImplyNet_rec( p, pVar, !Gia_LitIsCompl(pLits[i]) ) ) + { + Css_ManCancelUntil( p, 0, NULL ); + return 1; + } + } + return 0; +} + + +/**Function************************************************************* + + Synopsis [Runs one call to the SAT solver.] + + Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Css_ManSolve( Css_Man_t * p, int * pLits, int nLits, int nConfsMax, Vec_Int_t * vCex ) +{ + // propagate the assignments + if ( Css_ManPrepare( p, pLits, nLits ) ) + return 1; + // justify the assignments + p->nConfsMax = nConfsMax; + if ( Css_ManJustify( p, 0 ) ) + return p->nConfsMax? 1 : -1; + // derive model and return the solver to the initial state + Vec_IntClear( vCex ); + Css_ManCancelUntil( p, 0, vCex ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Procedure to test the new SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_SatSolveTest2( Gia_Man_t * pGia ) +{ + extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit ); + int nConfsMax = 1000; + int CountUnsat, CountSat, CountUndec; + Css_Man_t * p; + Vec_Int_t * vCex; + Vec_Int_t * vVisit; + Gia_Obj_t * pRoot; + int i, RetValue, iLit, clk = clock(); + // create logic network + p = Css_ManCreateLogicSimple( pGia ); + // prepare AIG + Gia_ManCleanValue( pGia ); + Gia_ManCleanMark0( pGia ); + Gia_ManCleanMark1( pGia ); + vCex = Vec_IntAlloc( 100 ); + vVisit = Vec_IntAlloc( 100 ); + // solve for each output + CountUnsat = CountSat = CountUndec = 0; + Gia_ManForEachCo( pGia, pRoot, i ) + { + if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) ) + continue; +//printf( "Output %6d : ", i ); + iLit = Gia_Var2Lit( Gia_ObjHandle(Gia_ObjFanin0(pRoot)), Gia_ObjFaninC0(pRoot) ); + RetValue = Css_ManSolve( p, &iLit, 1, nConfsMax, vCex ); + if ( RetValue == 1 ) + CountUnsat++; + else if ( RetValue == -1 ) + CountUndec++; + else + { +// Gia_Obj_t * pTemp; +// int k; + assert( RetValue == 0 ); + CountSat++; +/* + Vec_PtrForEachEntry( vCex, pTemp, k ) +// printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjCioId(Gia_Regular(pTemp)) ); + printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjId(p,Gia_Regular(pTemp)) ); + printf( "\n" ); +*/ + Gia_SatVerifyPattern( pGia, pRoot, vCex, vVisit ); + } +// Gia_ManCheckMark0( p ); +// Gia_ManCheckMark1( p ); + } + Css_ManStop( p ); + Vec_IntFree( vCex ); + Vec_IntFree( vVisit ); + printf( "Unsat = %d. Sat = %d. Undec = %d. ", CountUnsat, CountSat, CountUndec ); + ABC_PRT( "Time", clock() - clk ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/gia/giaCSatA.c b/src/aig/gia/giaCSatA.c new file mode 100644 index 00000000..12f6895a --- /dev/null +++ b/src/aig/gia/giaCSatA.c @@ -0,0 +1,103 @@ +/**CFile**************************************************************** + + FileName [giaSolver.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Circuit-based SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaSolver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Sat_Cla_t_ Sat_Cla_t; +struct Sat_Cla_t_ +{ + unsigned hWatch0; // watched list for 0 literal + unsigned hWatch1; // watched list for 1 literal + int Activity; // activity of the clause + int nLits; // the number of literals + int pLits[0]; // the array of literals +}; + +typedef struct Sat_Fan_t_ Sat_Fan_t; +struct Sat_Fan_t_ +{ + unsigned iFan : 31; // ID of the fanin/fanout + unsigned fCompl : 1; // complemented attribute +}; + +typedef struct Sat_Obj_t_ Sat_Obj_t; +struct Sat_Obj_t_ +{ + unsigned hHandle; // node handle + unsigned fAssign : 1; // terminal node (CI/CO) + unsigned fValue : 1; // value under 000 pattern + unsigned fMark0 : 1; // first user-controlled mark + unsigned fMark1 : 1; // second user-controlled mark + unsigned nFanouuts : 28; // the number of fanouts + unsigned nFanins : 8; // the number of fanins + unsigned Level : 24; // logic level + unsigned hNext; // next one on this level + unsigned hWatch0; // watched list for 0 literal + unsigned hWatch1; // watched list for 1 literal + unsigned hReason; // reason for this variable + unsigned Depth; // decision depth + Sat_Fan_t Fanios[0]; // the array of fanins/fanouts +}; + +typedef struct Sat_Man_t_ Sat_Man_t; +struct Sat_Man_t_ +{ + Gia_Man_t * pGia; // the original AIG manager + // circuit + Vec_Int_t vCis; // the vector of CIs (PIs + LOs) + Vec_Int_t vObjs; // the vector of objects + // learned clauses + Vec_Int_t vClauses; // the vector of clauses + // solver data + Vec_Int_t vTrail; // variable queue + Vec_Int_t vTrailLim; // pointer into the trail + int iHead; // variable queue + int iTail; // variable queue + int iRootLevel; // first decision + // levelized order + int iLevelTop; // the largest unassigned level + Vec_Int_t vLevels; // the linked lists of levels +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/gia/giaCSatB.c b/src/aig/gia/giaCSatB.c new file mode 100644 index 00000000..e1f68c6f --- /dev/null +++ b/src/aig/gia/giaCSatB.c @@ -0,0 +1,490 @@ +/**CFile**************************************************************** + + FileName [giaSolver.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Circuit-based SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaSolver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Sat_Man_t_ Sat_Man_t; +struct Sat_Man_t_ +{ + Gia_Man_t * pGia; // the original AIG manager + Vec_Int_t * vModel; // satisfying PI assignment + int nConfs; // cur number of conflicts + int nConfsMax; // max number of conflicts + int iHead; // variable queue + int iTail; // variable queue + int iJust; // head of justification + int nTrail; // variable queue size + int pTrail[0]; // variable queue data +}; + +static inline int Sat_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; } +static inline void Sat_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; } +static inline void Sat_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; } +static inline int Sat_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; } +static inline void Sat_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; } + +extern void Cec_ManPatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat ); +extern void Cec_ManPatCleanMark0( Gia_Man_t * p, Gia_Obj_t * pObj ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sat_Man_t * Sat_ManCreate( Gia_Man_t * pGia ) +{ + Sat_Man_t * p; + p = (Sat_Man_t *)ABC_ALLOC( char, sizeof(Sat_Man_t) + sizeof(int)*Gia_ManObjNum(pGia) ); + memset( p, 0, sizeof(Sat_Man_t) ); + p->pGia = pGia; + p->nTrail = Gia_ManObjNum(pGia); + p->vModel = Vec_IntAlloc( 1000 ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_ManDelete( Sat_Man_t * p ) +{ + Vec_IntFree( p->vModel ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Sat_ManCancelUntil( Sat_Man_t * p, int iBound ) +{ + Gia_Obj_t * pVar; + int i; + for ( i = p->iTail-1; i >= iBound; i-- ) + { + pVar = Gia_ManObj( p->pGia, p->pTrail[i] ); + Sat_VarUnassign( pVar ); + } + p->iTail = p->iTail = iBound; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Sat_ManDeriveModel( Sat_Man_t * p ) +{ + Gia_Obj_t * pVar; + int i; + Vec_IntClear( p->vModel ); + for ( i = 0; i < p->iTail; i++ ) + { + pVar = Gia_ManObj( p->pGia, p->pTrail[i] ); + if ( Gia_ObjIsCi(pVar) ) + Vec_IntPush( p->vModel, Gia_ObjCioId(pVar) ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Sat_ManEnqueue( Sat_Man_t * p, Gia_Obj_t * pVar, int Value ) +{ + assert( p->iTail < p->nTrail ); + Sat_VarAssign( pVar ); + Sat_VarSetValue( pVar, Value ); + p->pTrail[p->iTail++] = Gia_ObjId(p->pGia, pVar); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Sat_ManAssume( Sat_Man_t * p, Gia_Obj_t * pVar, int Value ) +{ + assert( p->iHead == p->iTail ); + Sat_ManEnqueue( p, pVar, Value ); +} + +/**Function************************************************************* + + Synopsis [Propagates one assignment.] + + Description [Returns 1 if there is no conflict, 0 otherwise.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Sat_ManPropagateOne( Sat_Man_t * p, int iPos ) +{ + Gia_Obj_t * pVar, * pFan0, * pFan1; + pVar = Gia_ManObj( p->pGia, p->pTrail[iPos] ); + if ( Gia_ObjIsCi(pVar) ) + return 1; + pFan0 = Gia_ObjFanin0(pVar); + pFan1 = Gia_ObjFanin1(pVar); + if ( Sat_VarValue(pVar) ) // positive + { + if ( Sat_VarIsAssigned(pFan0) ) + { + if ( Sat_VarValue(pFan0) == Gia_ObjFaninC0(pVar) ) // negative -> conflict + return 0; + // check second var + if ( Sat_VarIsAssigned(pFan1) ) + { + if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> conflict + return 0; + // positive + positive -> nothing to do + return 1; + } + } + else + { + // pFan0 unassigned -> enqueue first var + Sat_ManEnqueue( p, pFan0, !Gia_ObjFaninC0(pVar) ); + // check second var + if ( Sat_VarIsAssigned(pFan1) ) + { + if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> conflict + return 0; + // positive + positive -> nothing to do + return 1; + } + } + // unassigned -> enqueue second var + Sat_ManEnqueue( p, pFan1, !Gia_ObjFaninC1(pVar) ); + } + else // negative + { + if ( Sat_VarIsAssigned(pFan0) ) + { + if ( Sat_VarValue(pFan0) == Gia_ObjFaninC0(pVar) ) // negative -> nothing to do + return 1; + if ( Sat_VarIsAssigned(pFan1) ) + { + if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> nothing to do + return 1; + // positive + positive -> conflict + return 0; + } + // positive + unassigned -> enqueue second var + Sat_ManEnqueue( p, pFan1, Gia_ObjFaninC1(pVar) ); + } + else + { + if ( Sat_VarIsAssigned(pFan1) ) + { + if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> nothing to do + return 1; + // unassigned + positive -> enqueue first var + Sat_ManEnqueue( p, pFan0, Gia_ObjFaninC0(pVar) ); + } + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Propagates assignments.] + + Description [Returns 1 if there is no conflict.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Sat_ManPropagate( Sat_Man_t * p ) +{ + assert( p->iHead <= p->iTail ); + for ( ; p->iHead < p->iTail; p->iHead++ ) + if ( !Sat_ManPropagateOne( p, p->pTrail[p->iHead] ) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Propagates one assignment.] + + Description [Returns 1 if justified, 0 if conflict, -1 if needs justification.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Sat_ManJustifyNextOne( Sat_Man_t * p, int iPos ) +{ + Gia_Obj_t * pVar, * pFan0, * pFan1; + pVar = Gia_ManObj( p->pGia, p->pTrail[iPos] ); + if ( Gia_ObjIsCi(pVar) ) + return 1; + pFan0 = Gia_ObjFanin0(pVar); + pFan1 = Gia_ObjFanin1(pVar); + if ( Sat_VarValue(pVar) ) // positive + return 1; + // nevative + if ( Sat_VarIsAssigned(pFan0) ) + { + if ( Sat_VarValue(pFan0) == Gia_ObjFaninC0(pVar) ) // negative -> already justified + return 1; + // positive + if ( Sat_VarIsAssigned(pFan1) ) + { + if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> already justified + return 1; + // positive -> conflict + return 0; + } + // unasigned -> propagate + Sat_ManAssume( p, pFan1, Gia_ObjFaninC1(pVar) ); + return Sat_ManPropagate(p); + } + if ( Sat_VarIsAssigned(pFan1) ) + { + if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> already justified + return 1; + // positive + assert( !Sat_VarIsAssigned(pFan0) ); + // unasigned -> propagate + Sat_ManAssume( p, pFan0, Gia_ObjFaninC0(pVar) ); + return Sat_ManPropagate(p); + } + return -1; +} + +/**Function************************************************************* + + Synopsis [Justifies assignments.] + + Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sat_ManJustify( Sat_Man_t * p ) +{ + Gia_Obj_t * pVar, * pFan0, * pFan1; + int RetValue, iState, iJustState; + if ( p->nConfs && p->nConfs >= p->nConfsMax ) + return -1; + // get the next variable to justify + assert( p->iJust <= p->iTail ); + iJustState = p->iJust; + for ( ; p->iJust < p->iTail; p->iJust++ ) + { + RetValue = Sat_ManJustifyNextOne( p, p->pTrail[p->iJust] ); + if ( RetValue == 0 ) + return 1; + if ( RetValue == -1 ) + break; + } + if ( p->iJust == p->iTail ) // could not find + return 0; + // found variable to justify + pVar = Gia_ManObj( p->pGia, p->pTrail[p->iJust] ); + pFan0 = Gia_ObjFanin0(pVar); + pFan1 = Gia_ObjFanin1(pVar); + assert( !Sat_VarValue(pVar) && !Sat_VarIsAssigned(pFan0) && !Sat_VarIsAssigned(pFan1) ); + // remember the state of the stack + iState = p->iHead; + // try to justify by setting first fanin to 0 + Sat_ManAssume( p, pFan0, Gia_ObjFaninC0(pVar) ); + if ( Sat_ManPropagate(p) ) + { + RetValue = Sat_ManJustify(p); + if ( RetValue != 1 ) + return RetValue; + } + Sat_ManCancelUntil( p, iState ); + // try to justify by setting second fanin to 0 + Sat_ManAssume( p, pFan1, Gia_ObjFaninC1(pVar) ); + if ( Sat_ManPropagate(p) ) + { + RetValue = Sat_ManJustify(p); + if ( RetValue != 1 ) + return RetValue; + } + Sat_ManCancelUntil( p, iState ); + p->iJust = iJustState; + p->nConfs++; + return 1; +} + +/**Function************************************************************* + + Synopsis [Runs one call to the SAT solver.] + + Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sat_ManPrepare( Sat_Man_t * p, int * pLits, int nLits, int nConfsMax ) +{ + Gia_Obj_t * pVar; + int i; + // double check that vars are unassigned + Gia_ManForEachObj( p->pGia, pVar, i ) + assert( !Sat_VarIsAssigned(pVar) ); + // prepare + p->iHead = p->iTail = p->iJust = 0; + p->nConfsMax = nConfsMax; + // assign literals + for ( i = 0; i < nLits; i++ ) + { + pVar = Gia_ManObj( p->pGia, Gia_Lit2Var(pLits[i]) ); + if ( Sat_VarIsAssigned(pVar) ) // assigned + { + if ( Sat_VarValue(pVar) != Gia_LitIsCompl(pLits[i]) ) // compatible assignment + continue; + } + else // unassigned + { + Sat_ManAssume( p, pVar, !Gia_LitIsCompl(pLits[i]) ); + if ( Sat_ManPropagate(p) ) + continue; + } + // conflict + Sat_ManCancelUntil( p, 0 ); + return 1; + } + assert( p->iHead == p->iTail ); + return 0; +} + + +/**Function************************************************************* + + Synopsis [Runs one call to the SAT solver.] + + Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sat_ManSolve( Sat_Man_t * p, int * pLits, int nLits, int nConfsMax ) +{ + int RetValue; + // propagate the assignments + if ( Sat_ManPrepare( p, pLits, nLits, nConfsMax ) ) + return 1; + // justify the assignments + RetValue = Sat_ManJustify( p ); + if ( RetValue == 0 ) // SAT + Sat_ManDeriveModel( p ); + // return the solver to the initial state + Sat_ManCancelUntil( p, 0 ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Testing the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sat_ManTest( Gia_Man_t * pGia, Gia_Obj_t * pObj, int nConfsMax ) +{ + Sat_Man_t * p; + int RetValue, iLit; + assert( Gia_ObjIsCo(pObj) ); + p = Sat_ManCreate( pGia ); + iLit = Gia_LitNot( Gia_ObjFaninLit0p(pGia, pObj) ); + RetValue = Sat_ManSolve( p, &iLit, 1, nConfsMax ); + if ( RetValue == 0 ) + { + Cec_ManPatVerifyPattern( pGia, pObj, p->vModel ); + Cec_ManPatCleanMark0( pGia, pObj ); + } + Sat_ManDelete( p ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index f8d759be..d5c0862f 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -417,39 +417,67 @@ Gia_Man_t * Gia_ManDupCofactored( Gia_Man_t * p, int iVar ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj, * pPivot; - int i; - assert( Gia_ManRegNum(p) == 0 ); - assert( iVar < Gia_ManObjNum(p) ); + int i, iCofVar = -1; + if ( !(iVar > 0 && iVar < Gia_ManObjNum(p)) ) + { + printf( "Gia_ManDupCofactored(): Variable %d is out of range (%d; %d).\n", iVar, 0, Gia_ManObjNum(p) ); + return NULL; + } + // find the cofactoring variable + pPivot = Gia_ManObj( p, iVar ); + if ( !(Gia_ObjIsCi(pPivot) || Gia_ObjIsAnd(pPivot)) ) + { + printf( "Gia_ManDupCofactored(): Variable %d should be a CI or an AND node.\n", iVar ); + return NULL; + } +// assert( Gia_ManRegNum(p) == 0 ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManConst0(p)->Value = 0; + // compute negative cofactor Gia_ManForEachCi( p, pObj, i ) + { pObj->Value = Gia_ManAppendCi(pNew); - // find the cofactoring variable - pPivot = Gia_ManObj(p, iVar); - // compute the negative cofactor - if ( Gia_ObjIsCi(pPivot) ) - pPivot->Value = Gia_Var2Lit( 0, 0 ); + if ( pObj == pPivot ) + { + iCofVar = pObj->Value; + pObj->Value = Gia_Var2Lit( 0, 0 ); + } + } Gia_ManForEachAnd( p, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); if ( pObj == pPivot ) - pPivot->Value = Gia_Var2Lit( 0, 0 ); + { + iCofVar = pObj->Value; + pObj->Value = Gia_Var2Lit( 0, 0 ); + } } Gia_ManForEachCo( p, pObj, i ) - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + pObj->Value = Gia_ObjFanin0Copy(pObj); // compute the positive cofactor - if ( Gia_ObjIsCi(pPivot) ) - pPivot->Value = Gia_Var2Lit( 0, 1 ); + Gia_ManForEachCi( p, pObj, i ) + { + pObj->Value = Gia_Var2Lit( Gia_ObjId(pNew, Gia_ManCi(pNew, i)), 0 ); + if ( pObj == pPivot ) + pObj->Value = Gia_Var2Lit( 0, 1 ); + } Gia_ManForEachAnd( p, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); if ( pObj == pPivot ) - pPivot->Value = Gia_Var2Lit( 0, 1 ); + pObj->Value = Gia_Var2Lit( 0, 1 ); } + // create MUXes + assert( iCofVar > 0 ); Gia_ManForEachCo( p, pObj, i ) - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + { + if ( pObj->Value == (unsigned)Gia_ObjFanin0Copy(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + else + pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashMux(pNew, iCofVar, Gia_ObjFanin0Copy(pObj), pObj->Value) ); + } Gia_ManHashStop( pNew ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); // rehash the result diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c index 0abaa55e..0469d1a4 100644 --- a/src/aig/gia/giaEmbed.c +++ b/src/aig/gia/giaEmbed.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [giaLogic.c] + FileName [giaEmbed.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: giaLogic.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: giaEmbed.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -24,13 +24,15 @@ /* The code is based on the paper by D. Harel and Y. Koren, "Graph drawing by high-dimensional embedding", - J. Graph Algs & Apps, Vol 8(2), pp. 195-217 (2004) + J. Graph Algs & Apps, Vol 8(2), pp. 195-217 (2004). */ //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +typedef float Emb_Dat_t; + typedef struct Emb_Obj_t_ Emb_Obj_t; struct Emb_Obj_t_ { @@ -63,12 +65,14 @@ struct Emb_Man_t_ int nTravIds; // traversal ID of the network int * pObjData; // the array containing data for objects int nObjData; // the size of array to store the logic network - unsigned char* pVecs; // array of vectors of size nObjs * nDims + int fVerbose; // verbose output flag + Emb_Dat_t * pVecs; // array of vectors of size nObjs * nDims int nReached; // the number of nodes reachable from the pivot int nDistMax; // the maximum distance from the node float ** pMatr; // covariance matrix nDims * nDims float ** pEigen; // the first several eigen values of the matrix float * pSols; // solutions to the problem nObjs * nSols; + unsigned short*pPlacement; // (x,y) coordinates for each cell }; static inline int Emb_ManRegNum( Emb_Man_t * p ) { return p->nRegs; } @@ -105,8 +109,8 @@ static inline void Emb_ObjSetTravIdPrevious( Emb_Man_t * p, Emb_Obj_t * p static inline int Emb_ObjIsTravIdCurrent( Emb_Man_t * p, Emb_Obj_t * pObj ) { return ((int)pObj->TravId == p->nTravIds); } static inline int Emb_ObjIsTravIdPrevious( Emb_Man_t * p, Emb_Obj_t * pObj ) { return ((int)pObj->TravId == p->nTravIds - 1); } -static inline unsigned char * Emb_ManVec( Emb_Man_t * p, int v ) { return p->pVecs + v * p->nObjs; } -static inline float * Emb_ManSol( Emb_Man_t * p, int v ) { return p->pSols + v * p->nObjs; } +static inline Emb_Dat_t * Emb_ManVec( Emb_Man_t * p, int v ) { return p->pVecs + v * p->nObjs; } +static inline float * Emb_ManSol( Emb_Man_t * p, int v ) { return p->pSols + v * p->nObjs; } #define Emb_ManForEachObj( p, pObj, i ) \ for ( i = 0; (i < p->nObjData) && (pObj = Emb_ManObj(p,i)); i += Emb_ObjSize(pObj) ) @@ -123,6 +127,136 @@ static inline float * Emb_ManSol( Emb_Man_t * p, int v ) /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Creates fanin/fanout pair.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Emb_ObjAddFanin( Emb_Obj_t * pObj, Emb_Obj_t * pFanin ) +{ + assert( pObj->iFanin < pObj->nFanins ); + assert( pFanin->iFanout < pFanin->nFanouts ); + pFanin->Fanios[pFanin->nFanins + pFanin->iFanout++] = + pObj->Fanios[pObj->iFanin++] = pObj->hHandle - pFanin->hHandle; +} + +/**Function************************************************************* + + Synopsis [Creates logic network isomorphic to the given AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia ) +{ + Emb_Man_t * p; + Emb_Obj_t * pObjLog, * pFanLog; + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + int i, nNodes, hHandle = 0; + // prepare the AIG + Gia_ManCreateRefs( pGia ); + // create logic network + p = ABC_CALLOC( Emb_Man_t, 1 ); + p->pGia = pGia; + p->nRegs = Gia_ManRegNum(pGia); + p->vCis = Vec_IntAlloc( Gia_ManCiNum(pGia) ); + p->vCos = Vec_IntAlloc( Gia_ManCoNum(pGia) ); + p->nObjData = (sizeof(Emb_Obj_t) / 4) * Gia_ManObjNum(pGia) + 2 * (2 * Gia_ManAndNum(pGia) + Gia_ManCoNum(pGia) + Gia_ManRegNum(pGia)); + p->pObjData = ABC_CALLOC( int, p->nObjData ); + // create constant node + Gia_ManConst0(pGia)->Value = hHandle; + pObjLog = Emb_ManObj( p, hHandle ); + pObjLog->hHandle = hHandle; + pObjLog->nFanins = 0; + pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) ); + // count objects + hHandle += Emb_ObjSize( pObjLog ); + nNodes = 1; + p->nObjs++; + // create the PIs + Gia_ManForEachCi( pGia, pObj, i ) + { + // create PI object + pObj->Value = hHandle; + Vec_IntPush( p->vCis, hHandle ); + pObjLog = Emb_ManObj( p, hHandle ); + pObjLog->hHandle = hHandle; + pObjLog->nFanins = Gia_ObjIsRo( pGia, pObj ); + pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj ); + pObjLog->fCi = 1; + // count objects + hHandle += Emb_ObjSize( pObjLog ); + p->nObjs++; + } + // create internal nodes + Gia_ManForEachAnd( pGia, pObj, i ) + { + assert( Gia_ObjRefs( pGia, pObj ) > 0 ); + // create node object + pObj->Value = hHandle; + pObjLog = Emb_ManObj( p, hHandle ); + pObjLog->hHandle = hHandle; + pObjLog->nFanins = 2; + pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj ); + // add fanins + pFanLog = Emb_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) ); + Emb_ObjAddFanin( pObjLog, pFanLog ); + pFanLog = Emb_ManObj( p, Gia_ObjValue(Gia_ObjFanin1(pObj)) ); + Emb_ObjAddFanin( pObjLog, pFanLog ); + // count objects + hHandle += Emb_ObjSize( pObjLog ); + nNodes++; + p->nObjs++; + } + // create the POs + Gia_ManForEachCo( pGia, pObj, i ) + { + // create PO object + pObj->Value = hHandle; + Vec_IntPush( p->vCos, hHandle ); + pObjLog = Emb_ManObj( p, hHandle ); + pObjLog->hHandle = hHandle; + pObjLog->nFanins = 1; + pObjLog->nFanouts = Gia_ObjIsRi( pGia, pObj ); + pObjLog->fCo = 1; + // add fanins + pFanLog = Emb_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) ); + Emb_ObjAddFanin( pObjLog, pFanLog ); + // count objects + hHandle += Emb_ObjSize( pObjLog ); + p->nObjs++; + } + // connect registers + Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, i ) + Emb_ObjAddFanin( Emb_ManObj(p,Gia_ObjValue(pObjRo)), Emb_ManObj(p,Gia_ObjValue(pObjRi)) ); + assert( nNodes == Emb_ManNodeNum(p) ); + assert( hHandle == p->nObjData ); + if ( hHandle != p->nObjData ) + printf( "Emb_ManStartSimple(): Fatal error in internal representation.\n" ); + // make sure the fanin/fanout counters are correct + Gia_ManForEachObj( pGia, pObj, i ) + { + if ( !~Gia_ObjValue(pObj) ) + continue; + pObjLog = Emb_ManObj( p, Gia_ObjValue(pObj) ); + assert( pObjLog->nFanins == pObjLog->iFanin ); + assert( pObjLog->nFanouts == pObjLog->iFanout ); + pObjLog->iFanin = pObjLog->iFanout = 0; + } + ABC_FREE( pGia->pRefs ); + return p; +} + /**Function************************************************************* Synopsis [Collect the fanin IDs.] @@ -332,25 +466,6 @@ void Emb_ManSetValue( Emb_Man_t * p ) } } -/**Function************************************************************* - - Synopsis [Creates fanin/fanout pair.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Emb_ObjAddFanin( Emb_Obj_t * pObj, Emb_Obj_t * pFanin ) -{ - assert( pObj->iFanin < pObj->nFanins ); - assert( pFanin->iFanout < pFanin->nFanouts ); - pFanin->Fanios[pFanin->nFanins + pFanin->iFanout++] = - pObj->Fanios[pObj->iFanin++] = pObj->hHandle - pFanin->hHandle; -} - /**Function************************************************************* Synopsis [Creates logic network isomorphic to the given AIG.] @@ -524,6 +639,7 @@ void Emb_ManStop( Emb_Man_t * p ) { Vec_IntFree( p->vCis ); Vec_IntFree( p->vCos ); + ABC_FREE( p->pPlacement ); ABC_FREE( p->pVecs ); ABC_FREE( p->pSols ); ABC_FREE( p->pMatr ); @@ -797,7 +913,7 @@ ABC_PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -Emb_Obj_t * Emb_ManFindDistances( Emb_Man_t * p, Vec_Int_t * vStart, unsigned char * pDist ) +Emb_Obj_t * Emb_ManFindDistances( Emb_Man_t * p, Vec_Int_t * vStart, Emb_Dat_t * pDist ) { Vec_Int_t * vThis, * vNext, * vTemp; Emb_Obj_t * pThis, * pNext, * pResult; @@ -818,9 +934,6 @@ Emb_Obj_t * Emb_ManFindDistances( Emb_Man_t * p, Vec_Int_t * vStart, unsigned ch Vec_IntClear( vNext ); Emb_ManForEachObjVec( vThis, p, pThis, i ) { - assert( p->nDistMax < 255 ); // current data-structure used unsigned char - if ( p->nDistMax > 254 ) - p->nDistMax = 254; if ( pDist ) pDist[pThis->Value] = p->nDistMax; Emb_ObjForEachFanin( pThis, pNext, k ) { @@ -862,7 +975,7 @@ Emb_Obj_t * Emb_ManRandomVertex( Emb_Man_t * p ) { Emb_Obj_t * pPivot; do { - int iNode = Aig_ManRandom( 0 ) % Gia_ManObjNum(p->pGia); + int iNode = (911 * Aig_ManRandom(0)) % Gia_ManObjNum(p->pGia); if ( ~Gia_ManObj(p->pGia, iNode)->Value ) pPivot = Emb_ManObj( p, Gia_ManObj(p->pGia, iNode)->Value ); else @@ -872,6 +985,36 @@ Emb_Obj_t * Emb_ManRandomVertex( Emb_Man_t * p ) return pPivot; } +/**Function************************************************************* + + Synopsis [Computes the distances from the given set of objects.] + + Description [Returns one of the most distant objects.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Emb_DumpGraphIntoFile( Emb_Man_t * p ) +{ + FILE * pFile; + Emb_Obj_t * pThis, * pNext; + int i, k; + pFile = fopen( "1.g", "w" ); + Emb_ManForEachObj( p, pThis, i ) + { + if ( !Emb_ObjIsTravIdCurrent(p, pThis) ) + continue; + Emb_ObjForEachFanout( pThis, pNext, k ) + { + assert( Emb_ObjIsTravIdCurrent(p, pNext) ); + fprintf( pFile, "%d %d\n", pThis->Value, pNext->Value ); + } + } + fclose( pFile ); +} + /**Function************************************************************* Synopsis [Computes dimentions of the graph.] @@ -890,16 +1033,21 @@ void Emb_ManComputeDimensions( Emb_Man_t * p, int nDims ) int d, nReached; int i, Counter; assert( p->pVecs == NULL ); - p->pVecs = ABC_FALLOC( unsigned char, p->nObjs * nDims ); + p->pVecs = ABC_ALLOC( Emb_Dat_t, p->nObjs * nDims ); + for ( i = 0; i < p->nObjs * nDims; i++ ) + p->pVecs[i] = ABC_INFINITY; vStart = Vec_IntAlloc( nDims ); // get the pivot vertex pRandom = Emb_ManRandomVertex( p ); Vec_IntPush( vStart, pRandom->hHandle ); // get the most distant vertex from the pivot pPivot = Emb_ManFindDistances( p, vStart, NULL ); +// Emb_DumpGraphIntoFile( p ); nReached = p->nReached; if ( nReached < Emb_ManObjNum(p) ) - printf( "Visited less objects (%d) than present (%d).\n", p->nReached, Emb_ManObjNum(p) ); + { + printf( "Considering a connected component with %d objects (out of %d).\n", p->nReached, Emb_ManObjNum(p) ); + } // start dimensions with this vertex Vec_IntClear( vStart ); for ( d = 0; d < nDims; d++ ) @@ -915,7 +1063,7 @@ void Emb_ManComputeDimensions( Emb_Man_t * p, int nDims ) // make sure the number of reached objects is correct Counter = 0; for ( i = 0; i < p->nObjs; i++ ) - if ( p->pVecs[i] < 255 ) + if ( p->pVecs[i] < ABC_INFINITY ) Counter++; assert( Counter == nReached ); } @@ -954,19 +1102,26 @@ float ** Emb_ManMatrAlloc( int nDims ) ***********************************************************************/ void Emb_ManComputeCovariance( Emb_Man_t * p, int nDims ) { - unsigned char * pOne, * pTwo; - float * pAves, * pCol; + Emb_Dat_t * pOne, * pTwo; + double Ave; + float * pRow; int d, i, k, v; - // compute averages of vectors - pAves = ABC_ALLOC( float, nDims ); + // average vectors for ( d = 0; d < nDims; d++ ) { - pAves[d] = 0.0; + // compute average + Ave = 0.0; pOne = Emb_ManVec( p, d ); for ( v = 0; v < p->nObjs; v++ ) - if ( pOne[v] < 255 ) - pAves[d] += pOne[v]; - pAves[d] /= p->nReached; + if ( pOne[v] < ABC_INFINITY ) + Ave += pOne[v]; + Ave /= p->nReached; + // update the vector + for ( v = 0; v < p->nObjs; v++ ) + if ( pOne[v] < ABC_INFINITY ) + pOne[v] -= Ave; + else + pOne[v] = 0.0; } // compute the matrix assert( p->pMatr == NULL ); @@ -976,17 +1131,15 @@ void Emb_ManComputeCovariance( Emb_Man_t * p, int nDims ) for ( i = 0; i < nDims; i++ ) { pOne = Emb_ManVec( p, i ); - pCol = p->pMatr[i]; + pRow = p->pMatr[i]; for ( k = 0; k < nDims; k++ ) { pTwo = Emb_ManVec( p, k ); - pCol[k] = 0.0; + pRow[k] = 0.0; for ( v = 0; v < p->nObjs; v++ ) - if ( pOne[i] < 255 && pOne[k] < 255 ) - pCol[k] += (pOne[i] - pAves[i])*(pOne[k] - pAves[k]); + pRow[k] += pOne[v]*pTwo[v]; } } - ABC_FREE( pAves ); } /**Function************************************************************* @@ -1080,9 +1233,9 @@ void Emb_ManVecCopyOne( float * pVecDest, float * pVecSour, int nDims ) ***********************************************************************/ void Emb_ManVecMultiply( float ** pMatr, float * pVec, int nDims, float * pRes ) { - int i; - for ( i = 0; i < nDims; i++ ) - pRes[i] = Emb_ManVecMultiplyOne( pMatr[i], pVec, nDims ); + int k; + for ( k = 0; k < nDims; k++ ) + pRes[k] = Emb_ManVecMultiplyOne( pMatr[k], pVec, nDims ); } /**Function************************************************************* @@ -1096,17 +1249,16 @@ void Emb_ManVecMultiply( float ** pMatr, float * pVec, int nDims, float * pRes ) SeeAlso [] ***********************************************************************/ -void Emb_ManVecOrthogonolize( float ** pEigen, int nVecs, float * pVec, int nDims ) +void Emb_ManVecOrthogonolizeOne( float * pEigen, float * pVecI, int nDims, float * pVecRes ) { - int i, k; - for ( k = 0; k < nVecs; k++ ) - for ( i = 0; i < nDims; i++ ) - pVec[i] -= pEigen[k][i] * Emb_ManVecMultiplyOne( pEigen[k], pVec, nDims ); + int k; + for ( k = 0; k < nDims; k++ ) + pVecRes[k] = pVecI[k] - pEigen[k] * Emb_ManVecMultiplyOne( pVecI, pEigen, nDims ); } /**Function************************************************************* - Synopsis [Computes the first eigen-vectors.] + Synopsis [Computes the first nSols eigen-vectors.] Description [] @@ -1115,32 +1267,226 @@ void Emb_ManVecOrthogonolize( float ** pEigen, int nVecs, float * pVec, int nDim SeeAlso [] ***********************************************************************/ -void Emb_ManComputeSolutions( Emb_Man_t * p, int nDims, int nSols ) +void Emb_ManComputeEigenvectors( Emb_Man_t * p, int nDims, int nSols ) { - float * pVecTemp, * pVecCur; - int i, k, j; + float * pVecUiHat, * pVecUi; + int i, j, k; assert( nSols < nDims ); - pVecTemp = p->pEigen[nSols]; + pVecUiHat = p->pEigen[nSols]; for ( i = 0; i < nSols; i++ ) { - pVecCur = p->pEigen[i]; - Emb_ManVecRandom( pVecTemp, nDims ); - Emb_ManVecNormal( pVecTemp, nDims ); + pVecUi = p->pEigen[i]; + Emb_ManVecRandom( pVecUiHat, nDims ); + Emb_ManVecNormal( pVecUiHat, nDims ); + k = 0; do { - Emb_ManVecCopyOne( pVecCur, pVecTemp, nDims ); + k++; + Emb_ManVecCopyOne( pVecUi, pVecUiHat, nDims ); for ( j = 0; j < i; j++ ) - Emb_ManVecOrthogonolize( p->pEigen, i, pVecCur, nDims ); - Emb_ManVecMultiply( p->pMatr, pVecCur, nDims, pVecTemp ); - Emb_ManVecNormal( pVecTemp, nDims ); - } while ( Emb_ManVecMultiplyOne(pVecTemp, pVecCur, nDims) < 0.999 ); - Emb_ManVecCopyOne( pVecCur, pVecTemp, nDims ); + { + Emb_ManVecOrthogonolizeOne( p->pEigen[j], pVecUi, nDims, pVecUiHat ); + Emb_ManVecCopyOne( pVecUi, pVecUiHat, nDims ); + } + Emb_ManVecMultiply( p->pMatr, pVecUi, nDims, pVecUiHat ); + Emb_ManVecNormal( pVecUiHat, nDims ); + } while ( Emb_ManVecMultiplyOne( pVecUiHat, pVecUi, nDims ) < 0.999 && k < 100 ); + Emb_ManVecCopyOne( pVecUi, pVecUiHat, nDims ); +// printf( "Converged after %d iterations.\n", k ); } +} + +/**Function************************************************************* + + Synopsis [Derives solutions from original vectors and eigenvectors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Emb_ManComputeSolutions( Emb_Man_t * p, int nDims, int nSols ) +{ + Emb_Dat_t * pX; + float * pY; + int i, j, k; assert( p->pSols == NULL ); p->pSols = ABC_CALLOC( float, p->nObjs * nSols ); + for ( i = 0; i < nDims; i++ ) + { + pX = Emb_ManVec( p, i ); + for ( j = 0; j < nSols; j++ ) + { + pY = Emb_ManSol( p, j ); + for ( k = 0; k < p->nObjs; k++ ) + pY[k] += pX[k] * p->pEigen[j][i]; + } + } +} + +/**Function************************************************************* + + Synopsis [Projects into square of size [0;0xffff] x [0;0xffff].] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols ) +{ + extern int * Gia_SortFloats( float * pArray, int nSize ); + float * pY0, * pY1, Max0, Max1, Min0, Min1, Str0, Str1; + int * pPerm0, * pPerm1; + int k; + if ( nSols != 2 ) + return; + // compute intervals + Min0 = ABC_INFINITY; + Max0 = -ABC_INFINITY; + pY0 = Emb_ManSol( p, 0 ); + for ( k = 0; k < p->nObjs; k++ ) + { + Min0 = ABC_MIN( Min0, pY0[k] ); + Max0 = ABC_MAX( Max0, pY0[k] ); + } + Str0 = 1.0*0xffff/(Max0 - Min0); + // update the coordinates + for ( k = 0; k < p->nObjs; k++ ) + pY0[k] = (pY0[k] != 0.0) ? ((pY0[k] - Min0) * Str0) : 0.0; + + // compute intervals + Min1 = ABC_INFINITY; + Max1 = -ABC_INFINITY; + pY1 = Emb_ManSol( p, 1 ); + for ( k = 0; k < p->nObjs; k++ ) + { + Min1 = ABC_MIN( Min1, pY1[k] ); + Max1 = ABC_MAX( Max1, pY1[k] ); + } + Str1 = 1.0*0xffff/(Max1 - Min1); + // update the coordinates + for ( k = 0; k < p->nObjs; k++ ) + pY1[k] = (pY1[k] != 0.0) ? ((pY1[k] - Min1) * Str1) : 0.0; + + // derive the order of these numbers + pPerm0 = Gia_SortFloats( pY0, p->nObjs ); + pPerm1 = Gia_SortFloats( pY1, p->nObjs ); + + // average solutions and project them into 32K by 32K square + p->pPlacement = ABC_ALLOC( unsigned short, 2 * p->nObjs ); + for ( k = 0; k < p->nObjs; k++ ) + { + p->pPlacement[2*pPerm0[k]+0] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs); + p->pPlacement[2*pPerm1[k]+1] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs); + } + ABC_FREE( pPerm0 ); + ABC_FREE( pPerm1 ); +} + +/**Function************************************************************* + + Synopsis [Derives solutions from original vectors and eigenvectors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Emb_ManPrintSolutions( Emb_Man_t * p, int nSols ) +{ + float * pSol; + int i, k; for ( i = 0; i < nSols; i++ ) - for ( k = 0; k < nDims; k++ ) - for ( j = 0; j < p->nObjs; j++ ) - Emb_ManSol(p, i)[j] += Emb_ManVec(p, k)[j] * p->pEigen[i][k]; + { + pSol = Emb_ManSol( p, i ); + for ( k = 0; k < p->nObjs; k++ ) + printf( "%4d ", (int)(100 * pSol[k]) ); + printf( "\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Derives solutions from original vectors and eigenvectors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Emb_ManDumpGnuplot( Emb_Man_t * p, int nSols, char * pName ) +{ + int fDumpImage = 1; +// char * pDirectory = "place\\"; + char * pDirectory = ""; + extern char * Ioa_TimeStamp(); + FILE * pFile; + char Buffer[1000]; + Emb_Obj_t * pThis, * pNext; + float * pSol0, * pSol1; + int i, k; + if ( nSols < 2 ) + return; + if ( p->pPlacement == NULL ) + { + printf( "Emb_ManDumpGnuplot(): Placement is not available.\n" ); + return; + } + pSol0 = Emb_ManSol( p, 0 ); + pSol1 = Emb_ManSol( p, 1 ); + sprintf( Buffer, "%s%s", pDirectory, Aig_FileNameGenericAppend(pName, ".plt") ); + pFile = fopen( Buffer, "w" ); + fprintf( pFile, "# This Gnuplot file was produced by ABC on %s\n", Ioa_TimeStamp() ); + fprintf( pFile, "\n" ); + if ( fDumpImage ) + { + fprintf( pFile, "set nokey\n" ); +// fprintf( pFile, "set terminal postscript\n" ); +// fprintf( pFile, "set output \'%s\'\n", Aig_FileNameGenericAppend(pName, ".ps") ); + fprintf( pFile, "set terminal gif font \'arial\' 10 size 800,600 xffffff x000000 x000000 x000000\n" ); + fprintf( pFile, "set output \'%s\'\n", Aig_FileNameGenericAppend(pName, ".gif") ); + fprintf( pFile, "\n" ); + } + fprintf( pFile, "set title \"%s : PI = %d PO = %d FF = %d Node = %d Obj = %d\\n", + pName, Emb_ManPiNum(p), Emb_ManPoNum(p), Emb_ManRegNum(p), Emb_ManNodeNum(p), Emb_ManObjNum(p) ); + fprintf( pFile, "(image generated by ABC and Gnuplot on %s)\"", Ioa_TimeStamp() ); + fprintf( pFile, "font \"Times, 12\"\n" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "plot [:] '-' w l\n" ); + fprintf( pFile, "\n" ); + Emb_ManForEachObj( p, pThis, i ) + { + if ( !Emb_ObjIsTravIdCurrent(p, pThis) ) + continue; + Emb_ObjForEachFanout( pThis, pNext, k ) + { + assert( Emb_ObjIsTravIdCurrent(p, pNext) ); +// fprintf( pFile, "%d %d\n", (int)pSol0[pThis->Value], (int)pSol1[pThis->Value] ); +// fprintf( pFile, "%d %d\n", (int)pSol0[pNext->Value], (int)pSol1[pNext->Value] ); +// fprintf( pFile, "%5.2f %5.2f\n", pSol0[pThis->Value], pSol1[pThis->Value] ); +// fprintf( pFile, "%5.2f %5.2f\n", pSol0[pNext->Value], pSol1[pNext->Value] ); + fprintf( pFile, "%5d %5d\n", p->pPlacement[2*pThis->Value+0], p->pPlacement[2*pThis->Value+1] ); + fprintf( pFile, "%5d %5d\n", p->pPlacement[2*pNext->Value+0], p->pPlacement[2*pNext->Value+1] ); + fprintf( pFile, "\n" ); + } + } + fprintf( pFile, "EOF\n" ); + fprintf( pFile, "\n" ); + if ( !fDumpImage ) + { + fprintf( pFile, "pause -1 \"Hit return to continue\"\n" ); + fprintf( pFile, "reset\n" ); + fprintf( pFile, "\n" ); + } + fclose( pFile ); } /**Function************************************************************* @@ -1154,34 +1500,55 @@ void Emb_ManComputeSolutions( Emb_Man_t * p, int nDims, int nSols ) SeeAlso [] ***********************************************************************/ -void Gia_ManSolveProblem( Gia_Man_t * pGia, int nDims, int nSols ) +void Gia_ManSolveProblem( Gia_Man_t * pGia, int nDims, int nSols, int fCluster, int fDump, int fVerbose ) { Emb_Man_t * p; - int clk; + int clk, clkSetup; // Gia_ManTestDistance( pGia ); + // transform AIG into internal data-structure clk = clock(); - p = Emb_ManStart( pGia ); + if ( fCluster ) + { + p = Emb_ManStart( pGia ); + if ( fVerbose ) + { + printf( "After clustering: " ); + Emb_ManPrintStats( p ); + } + } + else + p = Emb_ManStartSimple( pGia ); + p->fVerbose = fVerbose; // Emb_ManPrintFanio( p ); - Emb_ManPrintStats( p ); - Aig_ManRandom( 1 ); + + // prepare data-structure + Aig_ManRandom( 1 ); // reset random numbers for deterministic behavior Emb_ManResetTravId( p ); - // set all nodes to have their IDs Emb_ManSetValue( p ); -ABC_PRT( "Setup ", clock() - clk ); +clkSetup = clock() - clk; clk = clock(); Emb_ManComputeDimensions( p, nDims ); +if ( fVerbose ) +ABC_PRT( "Setup ", clkSetup ); +if ( fVerbose ) ABC_PRT( "Dimensions", clock() - clk ); clk = clock(); Emb_ManComputeCovariance( p, nDims ); +if ( fVerbose ) ABC_PRT( "Matrix ", clock() - clk ); clk = clock(); -// Emb_ManComputeSolutions( p, nDims, nSols ); + Emb_ManComputeEigenvectors( p, nDims, nSols ); + Emb_ManComputeSolutions( p, nDims, nSols ); + Emb_ManDerivePlacement( p, nSols ); +if ( fVerbose ) ABC_PRT( "Eigenvecs ", clock() - clk ); + if ( fDump ) + Emb_ManDumpGnuplot( p, nSols, pGia->pName ); Emb_ManStop( p ); } diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c index e5080e81..c2d2d33f 100644 --- a/src/aig/gia/giaForce.c +++ b/src/aig/gia/giaForce.c @@ -42,7 +42,7 @@ struct For_Man_t_ Gia_Man_t * pGia; // the original AIG manager int nObjs; // the number of objects int iObj; // the last added object - int * pPlace; // Placeing of objects + int * pPlace; // coordinates of objects int * piNext; // array of next pointers int * piRoot; // array of root pointers float * plEdge; // edge coordinates @@ -413,7 +413,7 @@ void For_ManSortObjects( For_Man_t * p ) p->piNext[i] = p->piRoot[iPlace]; p->piRoot[iPlace] = i; } - // recostruct the order + // reconstruct the order p->iObj = 0; pPrev = NULL; vArray = Vec_PtrAlloc( 100 ); diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c index 6da24083..443a1ae8 100644 --- a/src/aig/gia/giaGlitch.c +++ b/src/aig/gia/giaGlitch.c @@ -630,23 +630,38 @@ static inline unsigned Gli_ManUpdateRandomInput( unsigned uInfo, float PiTransPr SeeAlso [] ***********************************************************************/ -static inline void Gli_ManSimulateSeqOne( Gli_Man_t * p, float PiTransProb ) +void Gli_ManSimulateSeqPref( Gli_Man_t * p, int nPref ) { Gli_Obj_t * pObj, * pObjRi, * pObjRo; - int i; + int i, f; + // initialize simulation data Gli_ManForEachPi( p, pObj, i ) - pObj->uSimInfo = Gli_ManUpdateRandomInput( pObj->uSimInfo, PiTransProb ); - Gli_ManForEachNode( p, pObj, i ) - pObj->uSimInfo = Gli_ManSimulateSeqNode( p, pObj ); - Gli_ManForEachRi( p, pObj, i ) - pObj->uSimInfo = Gli_ObjFanin(pObj, 0)->uSimInfo; - Gli_ManForEachRiRo( p, pObjRi, pObjRo, i ) - pObjRo->uSimInfo = pObjRi->uSimInfo; + pObj->uSimInfo = Gli_ManUpdateRandomInput( pObj->uSimInfo, 0.5 ); + Gli_ManForEachRo( p, pObj, i ) + pObj->uSimInfo = 0; + for ( f = 0; f < nPref; f++ ) + { + // simulate one frame + Gli_ManForEachNode( p, pObj, i ) + pObj->uSimInfo = Gli_ManSimulateSeqNode( p, pObj ); + Gli_ManForEachRi( p, pObj, i ) + pObj->uSimInfo = Gli_ObjFanin(pObj, 0)->uSimInfo; + // initialize the next frame + Gli_ManForEachPi( p, pObj, i ) + pObj->uSimInfo = Gli_ManUpdateRandomInput( pObj->uSimInfo, 0.5 ); + Gli_ManForEachRiRo( p, pObjRi, pObjRo, i ) + pObjRo->uSimInfo = pObjRi->uSimInfo; + } + // save simulation data after nPref timeframes + if ( p->pSimInfoPrev == NULL ) + p->pSimInfoPrev = ABC_ALLOC( unsigned, Gli_ManCiNum(p) ); + Gli_ManForEachCi( p, pObj, i ) + p->pSimInfoPrev[i] = pObj->uSimInfo; } /**Function************************************************************* - Synopsis [Simulates sequential network randomly for the given number of frames.] + Synopsis [Initialized object values to be one pattern in the saved data.] Description [] @@ -655,19 +670,19 @@ static inline void Gli_ManSimulateSeqOne( Gli_Man_t * p, float PiTransProb ) SeeAlso [] ***********************************************************************/ -static inline void Gli_ManSaveCiInfo( Gli_Man_t * p ) +void Gli_ManSetDataSaved( Gli_Man_t * p, int iBit ) { Gli_Obj_t * pObj; int i; - if ( p->pSimInfoPrev == NULL ) - p->pSimInfoPrev = ABC_ALLOC( unsigned, Gli_ManCiNum(p) ); Gli_ManForEachCi( p, pObj, i ) - p->pSimInfoPrev[i] = pObj->uSimInfo; + pObj->fPhase = pObj->fPhase2 = ((p->pSimInfoPrev[i] >> iBit) & 1); + Gli_ManForEachNode( p, pObj, i ) + pObj->fPhase = pObj->fPhase2 = Gli_NodeComputeValue( pObj ); } /**Function************************************************************* - Synopsis [Simulates sequential network randomly for the given number of frames.] + Synopsis [Sets random info at the PIs and collects changed PIs.] Description [] @@ -676,14 +691,37 @@ static inline void Gli_ManSaveCiInfo( Gli_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Gli_ManSimulateSeqPref( Gli_Man_t * p, int nPref ) +void Gli_ManSetPiRandomSeq( Gli_Man_t * p, float PiTransProb ) { - Gli_Obj_t * pObj; - int i, f; - Gli_ManForEachRo( p, pObj, i ) - pObj->uSimInfo = 0; - for ( f = 0; f < nPref; f++ ) - Gli_ManSimulateSeqOne( p, 0.5 ); + Gli_Obj_t * pObj, * pObjRi; + float Multi = 1.0 / (1 << 16); + int i; + assert( 0.0 < PiTransProb && PiTransProb < 1.0 ); + // transfer data to the COs + Gli_ManForEachCo( p, pObj, i ) + pObj->fPhase = pObj->fPhase2 = Gli_ObjFanin(pObj, 0)->fPhase; + // set changed PIs + Vec_IntClear( p->vCisChanged ); + Gli_ManForEachPi( p, pObj, i ) + if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb ) + { + Vec_IntPush( p->vCisChanged, pObj->Handle ); + pObj->fPhase ^= 1; + pObj->fPhase2 ^= 1; + pObj->nSwitches++; + pObj->nGlitches++; + } + // set changed ROs + Gli_ManForEachRiRo( p, pObjRi, pObj, i ) + if ( pObjRi->fPhase != pObj->fPhase ) + { + Vec_IntPush( p->vCisChanged, pObj->Handle ); + pObj->fPhase ^= 1; + pObj->fPhase2 ^= 1; + pObj->nSwitches++; + pObj->nGlitches++; + } + } /**Function************************************************************* @@ -714,14 +752,14 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb } else { + int nIters = Aig_BitWordNum(nPatterns); Gli_ManSimulateSeqPref( p, 16 ); - for ( k = Aig_BitWordNum(nPatterns) - 1; k >= 0; k-- ) + for ( i = 0; i < 32; i++ ) { - Gli_ManSaveCiInfo( p ); - Gli_ManSimulateSeqOne( p, PiTransProb ); - for ( i = 0; i < 32; i++ ) + Gli_ManSetDataSaved( p, i ); + for ( k = 0; k < nIters; k++ ) { - Gli_ManSetPiFromSaved( p, i ); + Gli_ManSetPiRandomSeq( p, PiTransProb ); Gli_ManSwitching( p ); Gli_ManGlitching( p ); // Gli_ManVerify( p ); diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c index c2bde6ba..8bc38ed9 100644 --- a/src/aig/gia/giaHash.c +++ b/src/aig/gia/giaHash.c @@ -498,6 +498,24 @@ int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 ) return Gia_LitNotCond( Gia_ManHashAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), !fCompl ); } +/**Function************************************************************* + + Synopsis [Rehashes AIG with mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 ) +{ + int iTemp0 = Gia_ManHashAnd( p, Gia_LitNot(iCtrl), iData0 ); + int iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 ); + return Gia_LitNotCond( Gia_ManHashAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), 1 ); +} + /**Function************************************************************* Synopsis [Rehashes AIG with mapping.] diff --git a/src/aig/gia/giaSolver.c b/src/aig/gia/giaSolver.c deleted file mode 100644 index e1f68c6f..00000000 --- a/src/aig/gia/giaSolver.c +++ /dev/null @@ -1,490 +0,0 @@ -/**CFile**************************************************************** - - FileName [giaSolver.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Scalable AIG package.] - - Synopsis [Circuit-based SAT solver.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: giaSolver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "gia.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Sat_Man_t_ Sat_Man_t; -struct Sat_Man_t_ -{ - Gia_Man_t * pGia; // the original AIG manager - Vec_Int_t * vModel; // satisfying PI assignment - int nConfs; // cur number of conflicts - int nConfsMax; // max number of conflicts - int iHead; // variable queue - int iTail; // variable queue - int iJust; // head of justification - int nTrail; // variable queue size - int pTrail[0]; // variable queue data -}; - -static inline int Sat_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; } -static inline void Sat_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; } -static inline void Sat_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; } -static inline int Sat_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; } -static inline void Sat_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; } - -extern void Cec_ManPatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat ); -extern void Cec_ManPatCleanMark0( Gia_Man_t * p, Gia_Obj_t * pObj ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Sat_Man_t * Sat_ManCreate( Gia_Man_t * pGia ) -{ - Sat_Man_t * p; - p = (Sat_Man_t *)ABC_ALLOC( char, sizeof(Sat_Man_t) + sizeof(int)*Gia_ManObjNum(pGia) ); - memset( p, 0, sizeof(Sat_Man_t) ); - p->pGia = pGia; - p->nTrail = Gia_ManObjNum(pGia); - p->vModel = Vec_IntAlloc( 1000 ); - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sat_ManDelete( Sat_Man_t * p ) -{ - Vec_IntFree( p->vModel ); - ABC_FREE( p ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Sat_ManCancelUntil( Sat_Man_t * p, int iBound ) -{ - Gia_Obj_t * pVar; - int i; - for ( i = p->iTail-1; i >= iBound; i-- ) - { - pVar = Gia_ManObj( p->pGia, p->pTrail[i] ); - Sat_VarUnassign( pVar ); - } - p->iTail = p->iTail = iBound; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Sat_ManDeriveModel( Sat_Man_t * p ) -{ - Gia_Obj_t * pVar; - int i; - Vec_IntClear( p->vModel ); - for ( i = 0; i < p->iTail; i++ ) - { - pVar = Gia_ManObj( p->pGia, p->pTrail[i] ); - if ( Gia_ObjIsCi(pVar) ) - Vec_IntPush( p->vModel, Gia_ObjCioId(pVar) ); - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Sat_ManEnqueue( Sat_Man_t * p, Gia_Obj_t * pVar, int Value ) -{ - assert( p->iTail < p->nTrail ); - Sat_VarAssign( pVar ); - Sat_VarSetValue( pVar, Value ); - p->pTrail[p->iTail++] = Gia_ObjId(p->pGia, pVar); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Sat_ManAssume( Sat_Man_t * p, Gia_Obj_t * pVar, int Value ) -{ - assert( p->iHead == p->iTail ); - Sat_ManEnqueue( p, pVar, Value ); -} - -/**Function************************************************************* - - Synopsis [Propagates one assignment.] - - Description [Returns 1 if there is no conflict, 0 otherwise.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Sat_ManPropagateOne( Sat_Man_t * p, int iPos ) -{ - Gia_Obj_t * pVar, * pFan0, * pFan1; - pVar = Gia_ManObj( p->pGia, p->pTrail[iPos] ); - if ( Gia_ObjIsCi(pVar) ) - return 1; - pFan0 = Gia_ObjFanin0(pVar); - pFan1 = Gia_ObjFanin1(pVar); - if ( Sat_VarValue(pVar) ) // positive - { - if ( Sat_VarIsAssigned(pFan0) ) - { - if ( Sat_VarValue(pFan0) == Gia_ObjFaninC0(pVar) ) // negative -> conflict - return 0; - // check second var - if ( Sat_VarIsAssigned(pFan1) ) - { - if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> conflict - return 0; - // positive + positive -> nothing to do - return 1; - } - } - else - { - // pFan0 unassigned -> enqueue first var - Sat_ManEnqueue( p, pFan0, !Gia_ObjFaninC0(pVar) ); - // check second var - if ( Sat_VarIsAssigned(pFan1) ) - { - if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> conflict - return 0; - // positive + positive -> nothing to do - return 1; - } - } - // unassigned -> enqueue second var - Sat_ManEnqueue( p, pFan1, !Gia_ObjFaninC1(pVar) ); - } - else // negative - { - if ( Sat_VarIsAssigned(pFan0) ) - { - if ( Sat_VarValue(pFan0) == Gia_ObjFaninC0(pVar) ) // negative -> nothing to do - return 1; - if ( Sat_VarIsAssigned(pFan1) ) - { - if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> nothing to do - return 1; - // positive + positive -> conflict - return 0; - } - // positive + unassigned -> enqueue second var - Sat_ManEnqueue( p, pFan1, Gia_ObjFaninC1(pVar) ); - } - else - { - if ( Sat_VarIsAssigned(pFan1) ) - { - if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> nothing to do - return 1; - // unassigned + positive -> enqueue first var - Sat_ManEnqueue( p, pFan0, Gia_ObjFaninC0(pVar) ); - } - } - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Propagates assignments.] - - Description [Returns 1 if there is no conflict.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Sat_ManPropagate( Sat_Man_t * p ) -{ - assert( p->iHead <= p->iTail ); - for ( ; p->iHead < p->iTail; p->iHead++ ) - if ( !Sat_ManPropagateOne( p, p->pTrail[p->iHead] ) ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Propagates one assignment.] - - Description [Returns 1 if justified, 0 if conflict, -1 if needs justification.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Sat_ManJustifyNextOne( Sat_Man_t * p, int iPos ) -{ - Gia_Obj_t * pVar, * pFan0, * pFan1; - pVar = Gia_ManObj( p->pGia, p->pTrail[iPos] ); - if ( Gia_ObjIsCi(pVar) ) - return 1; - pFan0 = Gia_ObjFanin0(pVar); - pFan1 = Gia_ObjFanin1(pVar); - if ( Sat_VarValue(pVar) ) // positive - return 1; - // nevative - if ( Sat_VarIsAssigned(pFan0) ) - { - if ( Sat_VarValue(pFan0) == Gia_ObjFaninC0(pVar) ) // negative -> already justified - return 1; - // positive - if ( Sat_VarIsAssigned(pFan1) ) - { - if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> already justified - return 1; - // positive -> conflict - return 0; - } - // unasigned -> propagate - Sat_ManAssume( p, pFan1, Gia_ObjFaninC1(pVar) ); - return Sat_ManPropagate(p); - } - if ( Sat_VarIsAssigned(pFan1) ) - { - if ( Sat_VarValue(pFan1) == Gia_ObjFaninC1(pVar) ) // negative -> already justified - return 1; - // positive - assert( !Sat_VarIsAssigned(pFan0) ); - // unasigned -> propagate - Sat_ManAssume( p, pFan0, Gia_ObjFaninC0(pVar) ); - return Sat_ManPropagate(p); - } - return -1; -} - -/**Function************************************************************* - - Synopsis [Justifies assignments.] - - Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sat_ManJustify( Sat_Man_t * p ) -{ - Gia_Obj_t * pVar, * pFan0, * pFan1; - int RetValue, iState, iJustState; - if ( p->nConfs && p->nConfs >= p->nConfsMax ) - return -1; - // get the next variable to justify - assert( p->iJust <= p->iTail ); - iJustState = p->iJust; - for ( ; p->iJust < p->iTail; p->iJust++ ) - { - RetValue = Sat_ManJustifyNextOne( p, p->pTrail[p->iJust] ); - if ( RetValue == 0 ) - return 1; - if ( RetValue == -1 ) - break; - } - if ( p->iJust == p->iTail ) // could not find - return 0; - // found variable to justify - pVar = Gia_ManObj( p->pGia, p->pTrail[p->iJust] ); - pFan0 = Gia_ObjFanin0(pVar); - pFan1 = Gia_ObjFanin1(pVar); - assert( !Sat_VarValue(pVar) && !Sat_VarIsAssigned(pFan0) && !Sat_VarIsAssigned(pFan1) ); - // remember the state of the stack - iState = p->iHead; - // try to justify by setting first fanin to 0 - Sat_ManAssume( p, pFan0, Gia_ObjFaninC0(pVar) ); - if ( Sat_ManPropagate(p) ) - { - RetValue = Sat_ManJustify(p); - if ( RetValue != 1 ) - return RetValue; - } - Sat_ManCancelUntil( p, iState ); - // try to justify by setting second fanin to 0 - Sat_ManAssume( p, pFan1, Gia_ObjFaninC1(pVar) ); - if ( Sat_ManPropagate(p) ) - { - RetValue = Sat_ManJustify(p); - if ( RetValue != 1 ) - return RetValue; - } - Sat_ManCancelUntil( p, iState ); - p->iJust = iJustState; - p->nConfs++; - return 1; -} - -/**Function************************************************************* - - Synopsis [Runs one call to the SAT solver.] - - Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sat_ManPrepare( Sat_Man_t * p, int * pLits, int nLits, int nConfsMax ) -{ - Gia_Obj_t * pVar; - int i; - // double check that vars are unassigned - Gia_ManForEachObj( p->pGia, pVar, i ) - assert( !Sat_VarIsAssigned(pVar) ); - // prepare - p->iHead = p->iTail = p->iJust = 0; - p->nConfsMax = nConfsMax; - // assign literals - for ( i = 0; i < nLits; i++ ) - { - pVar = Gia_ManObj( p->pGia, Gia_Lit2Var(pLits[i]) ); - if ( Sat_VarIsAssigned(pVar) ) // assigned - { - if ( Sat_VarValue(pVar) != Gia_LitIsCompl(pLits[i]) ) // compatible assignment - continue; - } - else // unassigned - { - Sat_ManAssume( p, pVar, !Gia_LitIsCompl(pLits[i]) ); - if ( Sat_ManPropagate(p) ) - continue; - } - // conflict - Sat_ManCancelUntil( p, 0 ); - return 1; - } - assert( p->iHead == p->iTail ); - return 0; -} - - -/**Function************************************************************* - - Synopsis [Runs one call to the SAT solver.] - - Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sat_ManSolve( Sat_Man_t * p, int * pLits, int nLits, int nConfsMax ) -{ - int RetValue; - // propagate the assignments - if ( Sat_ManPrepare( p, pLits, nLits, nConfsMax ) ) - return 1; - // justify the assignments - RetValue = Sat_ManJustify( p ); - if ( RetValue == 0 ) // SAT - Sat_ManDeriveModel( p ); - // return the solver to the initial state - Sat_ManCancelUntil( p, 0 ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Testing the SAT solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Sat_ManTest( Gia_Man_t * pGia, Gia_Obj_t * pObj, int nConfsMax ) -{ - Sat_Man_t * p; - int RetValue, iLit; - assert( Gia_ObjIsCo(pObj) ); - p = Sat_ManCreate( pGia ); - iLit = Gia_LitNot( Gia_ObjFaninLit0p(pGia, pObj) ); - RetValue = Sat_ManSolve( p, &iLit, 1, nConfsMax ); - if ( RetValue == 0 ) - { - Cec_ManPatVerifyPattern( pGia, pObj, p->vModel ); - Cec_ManPatCleanMark0( pGia, pObj ); - } - Sat_ManDelete( p ); - return RetValue; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/gia/giaSolver_cnf.c b/src/aig/gia/giaSolver_cnf.c deleted file mode 100644 index 12f6895a..00000000 --- a/src/aig/gia/giaSolver_cnf.c +++ /dev/null @@ -1,103 +0,0 @@ -/**CFile**************************************************************** - - FileName [giaSolver.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Scalable AIG package.] - - Synopsis [Circuit-based SAT solver.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: giaSolver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "gia.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Sat_Cla_t_ Sat_Cla_t; -struct Sat_Cla_t_ -{ - unsigned hWatch0; // watched list for 0 literal - unsigned hWatch1; // watched list for 1 literal - int Activity; // activity of the clause - int nLits; // the number of literals - int pLits[0]; // the array of literals -}; - -typedef struct Sat_Fan_t_ Sat_Fan_t; -struct Sat_Fan_t_ -{ - unsigned iFan : 31; // ID of the fanin/fanout - unsigned fCompl : 1; // complemented attribute -}; - -typedef struct Sat_Obj_t_ Sat_Obj_t; -struct Sat_Obj_t_ -{ - unsigned hHandle; // node handle - unsigned fAssign : 1; // terminal node (CI/CO) - unsigned fValue : 1; // value under 000 pattern - unsigned fMark0 : 1; // first user-controlled mark - unsigned fMark1 : 1; // second user-controlled mark - unsigned nFanouuts : 28; // the number of fanouts - unsigned nFanins : 8; // the number of fanins - unsigned Level : 24; // logic level - unsigned hNext; // next one on this level - unsigned hWatch0; // watched list for 0 literal - unsigned hWatch1; // watched list for 1 literal - unsigned hReason; // reason for this variable - unsigned Depth; // decision depth - Sat_Fan_t Fanios[0]; // the array of fanins/fanouts -}; - -typedef struct Sat_Man_t_ Sat_Man_t; -struct Sat_Man_t_ -{ - Gia_Man_t * pGia; // the original AIG manager - // circuit - Vec_Int_t vCis; // the vector of CIs (PIs + LOs) - Vec_Int_t vObjs; // the vector of objects - // learned clauses - Vec_Int_t vClauses; // the vector of clauses - // solver data - Vec_Int_t vTrail; // variable queue - Vec_Int_t vTrailLim; // pointer into the trail - int iHead; // variable queue - int iTail; // variable queue - int iRootLevel; // first decision - // levelized order - int iLevelTop; // the largest unassigned level - Vec_Int_t vLevels; // the linked lists of levels -}; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/gia/giaSort.c b/src/aig/gia/giaSort.c index 6986bc47..aec98fd8 100644 --- a/src/aig/gia/giaSort.c +++ b/src/aig/gia/giaSort.c @@ -59,13 +59,13 @@ static void sort_rec(int* array, int size, int(*comp)(const void *, const void * if (size <= 15) selectionsort(array, size, comp); else{ - int * pivot = array + size/2; + int pivot = array[size/2]; int tmp; int i = -1; int j = size; for(;;){ - do i++; while(comp(array + i, pivot)); - do j--; while(comp(pivot, array + j)); + do i++; while(comp(array + i, &pivot)); + do j--; while(comp(&pivot, array + j)); if (i >= j) break; tmp = array[i]; array[i] = array[j]; array[j] = tmp; } @@ -79,6 +79,65 @@ void minisat_sort(int* array, int size, int(*comp)(const void *, const void *)) } +/**Function************************************************************* + + Synopsis [This is implementation of qsort in MiniSat.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void selectionsort2(int* array, int size) +{ + int i, j, best_i; + int tmp; + for (i = 0; i < size-1; i++){ + best_i = i; + for (j = i+1; j < size; j++){ + if (array[j] < array[best_i]) + best_i = j; + } + tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; + } +} +static void sort_rec2(int* array, int size) +{ + if (size <= 15) + selectionsort2(array, size); + else{ + int pivot = array[size/2]; + int tmp; + int i = -1; + int j = size; + for(;;){ + do i++; while(array[i] < pivot); + do j--; while(pivot < array[j]); + if (i >= j) break; + tmp = array[i]; array[i] = array[j]; array[j] = tmp; + } + sort_rec2(array , i ); + sort_rec2(&array[i], size-i); + } +} +void minisat_sort2(int* array, int size) +{ + sort_rec2(array,size); +} + +/**Function************************************************************* + + Synopsis [This is implementation of qsort in MiniSat.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int * Gia_SortGetTest( int nSize ) { int i, * pArray; @@ -96,10 +155,11 @@ void Gia_SortVerifySorted( int * pArray, int nSize ) } void Gia_SortTest() { - int nSize = 1000000; + int nSize = 100000000; int * pArray; int clk = clock(); + printf( "Sorting %d integers\n", nSize ); pArray = Gia_SortGetTest( nSize ); clk = clock(); qsort( pArray, nSize, 4, (int (*)(const void *, const void *)) num_cmp1 ); @@ -113,8 +173,91 @@ clk = clock(); ABC_PRT( "minisat", clock() - clk ); Gia_SortVerifySorted( pArray, nSize ); ABC_FREE( pArray ); + + pArray = Gia_SortGetTest( nSize ); +clk = clock(); + minisat_sort2( pArray, nSize ); +ABC_PRT( "minisat with inlined comparison", clock() - clk ); + Gia_SortVerifySorted( pArray, nSize ); + ABC_FREE( pArray ); +} + +/**Function************************************************************* + + Synopsis [This is implementation of qsort in MiniSat.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void selectionsort3(float* array, int* perm, int size) +{ + float tmpf; + int tmpi; + int i, j, best_i; + for (i = 0; i < size-1; i++){ + best_i = i; + for (j = i+1; j < size; j++){ + if (array[j] < array[best_i]) + best_i = j; + } + tmpf = array[i]; array[i] = array[best_i]; array[best_i] = tmpf; + tmpi = perm[i]; perm[i] = perm[best_i]; perm[best_i] = tmpi; + } +} +static void sort_rec3(float* array, int* perm, int size) +{ + if (size <= 15) + selectionsort3(array, perm, size); + else{ + float pivot = array[size/2]; + float tmpf; + int tmpi; + int i = -1; + int j = size; + for(;;){ + do i++; while(array[i] < pivot); + do j--; while(pivot < array[j]); + if (i >= j) break; + tmpf = array[i]; array[i] = array[j]; array[j] = tmpf; + tmpi = perm[i]; perm[i] = perm[j]; perm[j] = tmpi; + } + sort_rec3(array , perm, i ); + sort_rec3(&array[i], &perm[i], size-i); + } +} +void minisat_sort3(float* array, int* perm, int size) +{ + sort_rec3(array, perm, size); } +/**Function************************************************************* + + Synopsis [Sorts the array of floating point numbers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Gia_SortFloats( float * pArray, int nSize ) +{ + int i, * pPerm; + pPerm = ABC_ALLOC( int, nSize ); + for ( i = 0; i < nSize; i++ ) + pPerm[i] = i; + minisat_sort3( pArray, pPerm, nSize ); +// for ( i = 1; i < nSize; i++ ) +// assert( pArray[i-1] <= pArray[i] ); + return pPerm; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index d86d897f..7a68b554 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -14,6 +14,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaMan.c \ src/aig/gia/giaScl.c \ src/aig/gia/giaSim.c \ + src/aig/gia/giaSort.c \ src/aig/gia/giaSwitch.c \ src/aig/gia/giaTsim.c \ src/aig/gia/giaUtil.c diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 485a5146..16430ace 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -50,7 +50,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) p->nBTLimit = 1000; // conflict limit at a node p->nBTLimitGlobal = 5000000; // conflict limit for all runs p->nMinDomSize = 100; // min clock domain considered for optimization - p->nItersStop = 0; // stop after the given number of iterations + p->nItersStop = -1; // stop after the given number of iterations p->nResimDelta = 1000; // the internal of nodes to resimulate p->fPolarFlip = 0; // uses polarity adjustment p->fLatchCorr = 0; // performs register correspondence @@ -199,7 +199,7 @@ clk = clock(); if ( !RetValue ) break; - if ( p->pPars->nItersStop && p->pPars->nItersStop == nIter ) + if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter ) { Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p ); Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL ); -- cgit v1.2.3