From 23fd11037a006089898cb13494305e402a11ec76 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 29 Mar 2009 08:01:00 -0700 Subject: Version abc90329 --- src/aig/gia/gia.h | 35 +- src/aig/gia/giaAiger.c | 140 +++++++- src/aig/gia/giaCSat.c | 886 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/giaCSat0.c | 328 ------------------ src/aig/gia/giaCSat1.c | 602 -------------------------------- src/aig/gia/giaCSat2.c | 745 ---------------------------------------- src/aig/gia/giaCSatA.c | 103 ------ src/aig/gia/giaCSatB.c | 490 -------------------------- src/aig/gia/giaCof.c | 4 +- src/aig/gia/giaDup.c | 222 +++++++++++- src/aig/gia/giaEmbed.c | 32 +- src/aig/gia/giaEquiv.c | 27 +- src/aig/gia/giaHash.c | 30 +- src/aig/gia/giaMan.c | 49 ++- src/aig/gia/giaPat.c | 129 +++++++ src/aig/gia/giaSwitch.c | 105 +++++- src/aig/gia/module.make | 2 + 17 files changed, 1614 insertions(+), 2315 deletions(-) create mode 100644 src/aig/gia/giaCSat.c delete mode 100644 src/aig/gia/giaCSat0.c delete mode 100644 src/aig/gia/giaCSat1.c delete mode 100644 src/aig/gia/giaCSat2.c delete mode 100644 src/aig/gia/giaCSatA.c delete mode 100644 src/aig/gia/giaCSatB.c create mode 100644 src/aig/gia/giaPat.c (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 28d610e9..87c85516 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -52,6 +52,15 @@ struct Gia_Rpr_t_ unsigned fColorB : 1; // marks cone of B }; +typedef struct Gia_Plc_t_ Gia_Plc_t; +struct Gia_Plc_t_ +{ + unsigned fFixed : 1; // the placement of this object is fixed + unsigned xCoord : 15; // x-ooordinate of the placement + unsigned fUndef : 1; // the placement of this object is not assigned + unsigned yCoord : 15; // y-ooordinate of the placement +}; + typedef struct Gia_Obj_t_ Gia_Obj_t; struct Gia_Obj_t_ { @@ -117,6 +126,8 @@ struct Gia_Man_t_ Gia_Cex_t * pCexComb; // combinational counter-example int * pCopies; // intermediate copies Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc + unsigned char* pSwitching; // switching activity for each object + Gia_Plc_t * pPlacement; // placement of the objects }; @@ -247,7 +258,7 @@ static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Gia_Lit2Var(iLit)), Gia_LitIsCompl(iLit) ); } -static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_Var2Lit( Gia_ObjId(p, pObj), Gia_IsComplement(pObj) ); } +static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); } static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); } static inline int Gia_ObjValue( Gia_Obj_t * pObj ) { return pObj->Value; } @@ -375,8 +386,10 @@ static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; } static inline int Gia_ObjIsHead( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; } -static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0; } -static inline int Gia_ObjIsClass( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0; } +static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0; } +static inline int Gia_ObjIsClass( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0; } +static inline int Gia_ObjHasSameRepr( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjRepr(p, i) == Gia_ObjRepr(p, k) && Gia_ObjRepr(p, i) != GIA_VOID) : Gia_ObjRepr(p, k) == 0; } +static inline int Gia_ObjIsFailedPair( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjFailed(p, i) || Gia_ObjFailed(p, k)) : Gia_ObjFailed(p, k); } #define Gia_ManForEachConst( p, i ) \ for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else @@ -419,6 +432,8 @@ static inline int * Gia_ObjGateFanins( Gia_Man_t * p, int Id ) { re for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ ) #define Gia_ManForEachCo( p, pObj, i ) \ for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((pObj) = Gia_ManCo(p, i)); i++ ) +#define Gia_ManForEachCoReverse( p, pObj, i ) \ + for ( i = Vec_IntSize(p->vCos) - 1; (i >= 0) && ((pObj) = Gia_ManCo(p, i)); i-- ) #define Gia_ManForEachCoDriver( p, pObj, i ) \ for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((pObj) = Gia_ObjFanin0(Gia_ManCo(p, i))); i++ ) #define Gia_ManForEachPi( p, pObj, i ) \ @@ -443,7 +458,9 @@ extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p ); /*=== giaAiger.c ===========================================================*/ extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ); extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact ); +extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits ); /*=== giaCsat.c ============================================================*/ +extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus ); /*=== giaCof.c =============================================================*/ extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes ); extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar ); @@ -455,6 +472,10 @@ extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int extern int Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes ); extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes ); /*=== giaDup.c ============================================================*/ +extern Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ); + extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ); @@ -508,19 +529,22 @@ 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 ); +extern void Gia_ManHashProfile( Gia_Man_t * p ); /*=== giaLogic.c ===========================================================*/ extern void Gia_ManTestDistance( Gia_Man_t * p ); extern void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars ); /*=== giaMan.c ===========================================================*/ extern Gia_Man_t * Gia_ManStart( int nObjsMax ); extern void Gia_ManStop( Gia_Man_t * p ); -extern void Gia_ManPrintStats( Gia_Man_t * p ); +extern void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ); extern void Gia_ManPrintStatsShort( Gia_Man_t * p ); extern void Gia_ManPrintMiterStatus( Gia_Man_t * p ); extern void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs ); extern void Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew ); /*=== giaMap.c ===========================================================*/ extern void Gia_ManPrintMappingStats( Gia_Man_t * p ); +/*=== giaPat.c ===========================================================*/ +extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit ); /*=== giaRetime.c ===========================================================*/ extern Gia_Man_t * Gia_ManRetimeForward( Gia_Man_t * p, int nMaxIters, int fVerbose ); /*=== giaSat.c ============================================================*/ @@ -535,6 +559,9 @@ extern Gia_Man_t * Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int extern int * Gia_SortFloats( float * pArray, int * pPerm, int nSize ); /*=== giaSim.c ============================================================*/ extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ); +/*=== giaSwitch.c ============================================================*/ +extern float Gia_ManEvaluateSwitching( Gia_Man_t * p ); +extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne ); /*=== giaTsim.c ============================================================*/ extern Gia_Man_t * Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose ); /*=== giaUtil.c ===========================================================*/ diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index da1a8c9f..adc58e6c 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -192,6 +192,25 @@ int Gia_ReadInt( unsigned char * pPos ) return Value; } +/**Function************************************************************* + + Synopsis [Reads decoded value.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Gia_ReadDiffValue( char ** ppPos, int iPrev ) +{ + int Item = Gia_ReadAigerDecode( ppPos ); + if ( Item & 1 ) + return iPrev + (Item >> 1); + return iPrev - (Item >> 1); +} + /**Function************************************************************* Synopsis [Read equivalence classes from the string.] @@ -238,7 +257,7 @@ Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize ) /**Function************************************************************* - Synopsis [Reads decoded value.] + Synopsis [Read flop classes from the string.] Description [] @@ -247,12 +266,13 @@ Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize ) SeeAlso [] ***********************************************************************/ -unsigned Gia_ReadDiffValue( char ** ppPos, int iPrev ) +void Gia_ReadFlopClasses( unsigned char ** ppPos, Vec_Int_t * vClasses, int nSize ) { - int Item = Gia_ReadAigerDecode( ppPos ); - if ( Item & 1 ) - return iPrev + (Item >> 1); - return iPrev - (Item >> 1); + int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4; + assert( nAlloc/4 == nSize ); + assert( Vec_IntSize(vClasses) == nSize ); + memcpy( Vec_IntArray(vClasses), *ppPos, 4*nSize ); + *ppPos += 4 * nSize; } /**Function************************************************************* @@ -288,6 +308,50 @@ int * Gia_ReadMapping( unsigned char ** ppPos, int nSize ) return pMapping; } +/**Function************************************************************* + + Synopsis [Read switching from the string.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned char * Gia_ReadSwitching( unsigned char ** ppPos, int nSize ) +{ + unsigned char * pSwitching; + int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4; + assert( nAlloc == nSize ); + pSwitching = ABC_ALLOC( unsigned char, nSize ); + memcpy( pSwitching, *ppPos, nSize ); + *ppPos += nSize; + return pSwitching; +} + +/**Function************************************************************* + + Synopsis [Read placement from the string.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Plc_t * Gia_ReadPlacement( unsigned char ** ppPos, int nSize ) +{ + Gia_Plc_t * pPlacement; + int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4; + assert( nAlloc/4 == nSize ); + pPlacement = ABC_ALLOC( Gia_Plc_t, nSize ); + memcpy( pPlacement, *ppPos, 4*nSize ); + *ppPos += 4 * nSize; + return pPlacement; +} + /**Function************************************************************* Synopsis [Reads the AIG in the binary AIGER format.] @@ -455,6 +519,13 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ) pNew->pReprs = Gia_ReadEquivClasses( &pCur, Gia_ManObjNum(pNew) ); pNew->pNexts = Gia_ManDeriveNexts( pNew ); } + if ( *pCur == 'f' ) + { + pCur++; + // read flop classes + pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) ); + Gia_ReadFlopClasses( &pCur, pNew->vFlopClasses, Gia_ManRegNum(pNew) ); + } if ( *pCur == 'm' ) { pCur++; @@ -465,6 +536,13 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ) { pCur++; // read placement + pNew->pPlacement = Gia_ReadPlacement( &pCur, Gia_ManObjNum(pNew) ); + } + if ( *pCur == 's' ) + { + pCur++; + // read switching activity + pNew->pSwitching = Gia_ReadSwitching( &pCur, Gia_ManObjNum(pNew) ); } if ( *pCur == 'n' ) { @@ -762,7 +840,10 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int // create normalized AIG if ( !Gia_ManIsNormalized(pInit) ) + { + printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" ); p = Gia_ManDupNormalized( pInit ); + } else p = pInit; @@ -831,6 +912,15 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fwrite( pEquivs, 1, nEquivSize, pFile ); ABC_FREE( pEquivs ); } + // write flop classes + if ( p->vFlopClasses ) + { + char Buffer[10]; + int nSize = 4*Gia_ManRegNum(p); + fprintf( pFile, "f" ); + fwrite( Buffer, 1, 4, pFile ); + fwrite( Vec_IntArray(p->vFlopClasses), 1, nSize, pFile ); + } // write mapping if ( p->pMapping ) { @@ -841,6 +931,26 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int ABC_FREE( pMaps ); } // write placement + if ( p->pPlacement ) + { + char Buffer[10]; + int nSize = 4*Gia_ManObjNum(p); + Gia_WriteInt( Buffer, nSize ); + fprintf( pFile, "p" ); + fwrite( Buffer, 1, 4, pFile ); + fwrite( p->pPlacement, 1, nSize, pFile ); + } + // write flop classes + if ( p->pSwitching ) + { + char Buffer[10]; + int nSize = Gia_ManObjNum(p); + Gia_WriteInt( Buffer, nSize ); + fprintf( pFile, "s" ); + fwrite( Buffer, 1, 4, pFile ); + fwrite( p->pSwitching, 1, nSize, pFile ); + } + // write name if ( p->pName ) fprintf( pFile, "n%s%c", p->pName, '\0' ); fprintf( pFile, "\nThis file was produced by the GIA package in ABC on %s\n", Gia_TimeStamp() ); @@ -850,6 +960,24 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int Gia_ManStop( p ); } +/**Function************************************************************* + + Synopsis [Writes the AIG in the binary AIGER format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits ) +{ + char Buffer[100]; + sprintf( Buffer, "%s%0*d.aig", pFilePrefix, nFileNumDigits, iFileNum ); + Gia_WriteAiger( p, Buffer, 0, 0 ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c new file mode 100644 index 00000000..5fa9f40f --- /dev/null +++ b/src/aig/gia/giaCSat.c @@ -0,0 +1,886 @@ +/**CFile**************************************************************** + + FileName [giaCSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [A simple circuit-based solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaCSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Cbs_Par_t_ Cbs_Par_t; +struct Cbs_Par_t_ +{ + // conflict limits + int nBTLimit; // limit on the number of conflicts + int nJustLimit; // limit on the size of justification queue + // current parameters + int nBTThis; // number of conflicts + int nJustThis; // max size of the frontier + int nBTTotal; // total number of conflicts + int nJustTotal; // total size of the frontier + // decision heuristics + int fUseHighest; // use node with the highest ID + int fUseLowest; // use node with the highest ID + int fUseMaxFF; // use node with the largest fanin fanout + // other + int fVerbose; +}; + +typedef struct Cbs_Que_t_ Cbs_Que_t; +struct Cbs_Que_t_ +{ + int iHead; // beginning of the queue + int iTail; // end of the queue + int nSize; // allocated size + Gia_Obj_t ** pData; // nodes stored in the queue +}; + +typedef struct Cbs_Man_t_ Cbs_Man_t; +struct Cbs_Man_t_ +{ + Cbs_Par_t Pars; // parameters + Gia_Man_t * pAig; // AIG manager + Cbs_Que_t pProp; // propagation queue + Cbs_Que_t pJust; // justification queue + Vec_Int_t * vModel; // satisfying assignment + // SAT calls statistics + int nSatUnsat; // the number of proofs + int nSatSat; // the number of failure + int nSatUndec; // the number of timeouts + int nSatTotal; // the number of calls + // conflicts + int nConfUnsat; // conflicts in unsat problems + int nConfSat; // conflicts in sat problems + int nConfUndec; // conflicts in undec problems + // runtime stats + int timeSatUnsat; // unsat + int timeSatSat; // sat + int timeSatUndec; // undecided + int timeTotal; // total runtime +}; + +static inline int Cbs_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; } +static inline void Cbs_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; } +static inline void Cbs_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; } +static inline int Cbs_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; } +static inline void Cbs_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; } +static inline int Cbs_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)); } +static inline int Cbs_VarFanin0Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); } +static inline int Cbs_VarFanin1Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); } + +#define Cbs_QueForEachEntry( Que, pObj, i ) \ + for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Sets default values of the parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cbs_SetDefaultParams( Cbs_Par_t * pPars ) +{ + memset( pPars, 0, sizeof(Cbs_Par_t) ); + pPars->nBTLimit = 1000; // limit on the number of conflicts + pPars->nJustLimit = 100; // limit on the size of justification queue + pPars->fUseHighest = 1; // use node with the highest ID + pPars->fUseLowest = 0; // use node with the highest ID + pPars->fUseMaxFF = 0; // use node with the largest fanin fanout + pPars->fVerbose = 1; // print detailed statistics +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cbs_Man_t * Cbs_ManAlloc() +{ + Cbs_Man_t * p; + p = ABC_CALLOC( Cbs_Man_t, 1 ); + p->pProp.nSize = p->pJust.nSize = 10000; + p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize ); + p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize ); + p->vModel = Vec_IntAlloc( 1000 ); + Cbs_SetDefaultParams( &p->Pars ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cbs_ManStop( Cbs_Man_t * p ) +{ + Vec_IntFree( p->vModel ); + ABC_FREE( p->pProp.pData ); + ABC_FREE( p->pJust.pData ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Returns satisfying assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Cbs_ReadModel( Cbs_Man_t * p ) +{ + return p->vModel; +} + + + + +/**Function************************************************************* + + Synopsis [Returns 1 if the solver is out of limits.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Cbs_ManCheckLimits( Cbs_Man_t * p ) +{ + return p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit; +} + +/**Function************************************************************* + + Synopsis [Saves the satisfying assignment as an array of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Cbs_ManSaveModel( Cbs_Man_t * p, Vec_Int_t * vCex ) +{ + Gia_Obj_t * pVar; + int i; + Vec_IntClear( vCex ); + p->pProp.iHead = 0; + Cbs_QueForEachEntry( p->pProp, pVar, i ) + if ( Gia_ObjIsCi(pVar) ) +// Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) ); + Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Cbs_VarValue(pVar)) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Cbs_QueIsEmpty( Cbs_Que_t * p ) +{ + return p->iHead == p->iTail; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Cbs_QuePush( Cbs_Que_t * p, Gia_Obj_t * pObj ) +{ + if ( p->iTail == p->nSize ) + { + p->nSize *= 2; + p->pData = ABC_REALLOC( Gia_Obj_t *, p->pData, p->nSize ); + } + p->pData[p->iTail++] = pObj; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the object in the queue.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Cbs_QueHasNode( Cbs_Que_t * p, Gia_Obj_t * pObj ) +{ + Gia_Obj_t * pTemp; + int i; + Cbs_QueForEachEntry( *p, pTemp, i ) + if ( pTemp == pObj ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Cbs_QueStore( Cbs_Que_t * p, int * piHeadOld, int * piTailOld ) +{ + int i; + *piHeadOld = p->iHead; + *piTailOld = p->iTail; + for ( i = *piHeadOld; i < *piTailOld; i++ ) + Cbs_QuePush( p, p->pData[i] ); + p->iHead = *piTailOld; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Cbs_QueRestore( Cbs_Que_t * p, int iHeadOld, int iTailOld ) +{ + p->iHead = iHeadOld; + p->iTail = iTailOld; +} + + +/**Function************************************************************* + + Synopsis [Max number of fanins fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Cbs_VarFaninFanoutMax( Cbs_Man_t * p, Gia_Obj_t * pObj ) +{ + int Count0, Count1; + assert( !Gia_IsComplement(pObj) ); + assert( Gia_ObjIsAnd(pObj) ); + Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) ); + Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) ); + return ABC_MAX( Count0, Count1 ); +} + +/**Function************************************************************* + + Synopsis [Find variable with the highest ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Gia_Obj_t * Cbs_ManDecideHighest( Cbs_Man_t * p ) +{ + Gia_Obj_t * pObj, * pObjMax = NULL; + int i; + Cbs_QueForEachEntry( p->pJust, pObj, i ) + if ( pObjMax == NULL || pObjMax < pObj ) + pObjMax = pObj; + return pObjMax; +} + +/**Function************************************************************* + + Synopsis [Find variable with the lowest ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Gia_Obj_t * Cbs_ManDecideLowest( Cbs_Man_t * p ) +{ + Gia_Obj_t * pObj, * pObjMin = NULL; + int i; + Cbs_QueForEachEntry( p->pJust, pObj, i ) + if ( pObjMin == NULL || pObjMin > pObj ) + pObjMin = pObj; + return pObjMin; +} + +/**Function************************************************************* + + Synopsis [Find variable with the maximum number of fanin fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Gia_Obj_t * Cbs_ManDecideMaxFF( Cbs_Man_t * p ) +{ + Gia_Obj_t * pObj, * pObjMax = NULL; + int i, iMaxFF = 0, iCurFF; + assert( p->pAig->pRefs != NULL ); + Cbs_QueForEachEntry( p->pJust, pObj, i ) + { + iCurFF = Cbs_VarFaninFanoutMax( p, pObj ); + assert( iCurFF > 0 ); + if ( iMaxFF < iCurFF ) + { + iMaxFF = iCurFF; + pObjMax = pObj; + } + } + return pObjMax; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound ) +{ + Gia_Obj_t * pVar; + int i; + assert( iBound <= p->pProp.iTail ); + p->pProp.iHead = iBound; + Cbs_QueForEachEntry( p->pProp, pVar, i ) + Cbs_VarUnassign( pVar ); + p->pProp.iTail = iBound; +} + +/**Function************************************************************* + + Synopsis [Assigns the variables a value.] + + Description [Returns 1 if conflict; 0 if no conflict.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj ) +{ + Gia_Obj_t * pObjR = Gia_Regular(pObj); + assert( Gia_ObjIsCand(pObjR) ); + assert( !Cbs_VarIsAssigned(pObjR) ); + Cbs_VarAssign( pObjR ); + Cbs_VarSetValue( pObjR, !Gia_IsComplement(pObj) ); + Cbs_QuePush( &p->pProp, pObjR ); +} + +/**Function************************************************************* + + Synopsis [Propagates a variable.] + + Description [Returns 1 if conflict; 0 if no conflict.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar ) +{ + int Value0, Value1; + assert( !Gia_IsComplement(pVar) ); + assert( Cbs_VarIsAssigned(pVar) ); + if ( Gia_ObjIsCi(pVar) ) + return 0; + assert( Gia_ObjIsAnd(pVar) ); + Value0 = Cbs_VarFanin0Value(pVar); + Value1 = Cbs_VarFanin1Value(pVar); + if ( Cbs_VarValue(pVar) ) + { // value is 1 + if ( Value0 == 0 || Value1 == 0 ) // one is 0 + return 1; + if ( Value0 == 2 ) // first is unassigned + Cbs_ManAssign( p, Gia_ObjChild0(pVar) ); + if ( Value1 == 2 ) // first is unassigned + Cbs_ManAssign( p, Gia_ObjChild1(pVar) ); + return 0; + } + // value is 0 + if ( Value0 == 0 || Value1 == 0 ) // one is 0 + return 0; + if ( Value0 == 1 && Value1 == 1 ) // both are 1 + return 1; + if ( Value0 == 1 || Value1 == 1 ) // one is 1 + { + if ( Value0 == 2 ) // first is unassigned + Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) ); + if ( Value1 == 2 ) // first is unassigned + Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) ); + return 0; + } + assert( Cbs_VarIsJust(pVar) ); + assert( !Cbs_QueHasNode( &p->pJust, pVar ) ); + Cbs_QuePush( &p->pJust, pVar ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Propagates a variable.] + + Description [Returns 1 if conflict; 0 if no conflict.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar ) +{ + int Value0, Value1; + assert( !Gia_IsComplement(pVar) ); + assert( Gia_ObjIsAnd(pVar) ); + assert( Cbs_VarIsAssigned(pVar) ); + assert( !Cbs_VarValue(pVar) ); + Value0 = Cbs_VarFanin0Value(pVar); + Value1 = Cbs_VarFanin1Value(pVar); + // value is 0 + if ( Value0 == 0 || Value1 == 0 ) // one is 0 + return 0; + if ( Value0 == 1 && Value1 == 1 ) // both are 1 + return 1; + assert( Value0 == 1 || Value1 == 1 ); + if ( Value0 == 2 ) // first is unassigned + Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) ); + if ( Value1 == 2 ) // first is unassigned + Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Propagates all variables.] + + Description [Returns 1 if conflict; 0 if no conflict.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cbs_ManPropagate( Cbs_Man_t * p ) +{ + Gia_Obj_t * pVar; + int i, k; + while ( 1 ) + { + Cbs_QueForEachEntry( p->pProp, pVar, i ) + { + if ( Cbs_ManPropagateOne( p, pVar ) ) + return 1; + } + p->pProp.iHead = p->pProp.iTail; + k = p->pJust.iHead; + Cbs_QueForEachEntry( p->pJust, pVar, i ) + { + if ( Cbs_VarIsJust( pVar ) ) + p->pJust.pData[k++] = pVar; + else if ( Cbs_ManPropagateTwo( p, pVar ) ) + return 1; + } + if ( k == p->pJust.iTail ) + break; + p->pJust.iTail = k; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Solve the problem recursively.] + + Description [Returns 1 if unsat or undecided; 0 if satisfiable.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cbs_ManSolve_rec( Cbs_Man_t * p ) +{ + Gia_Obj_t * pVar; + int iPropHead, iJustHead, iJustTail; + // propagate assignments + assert( !Cbs_QueIsEmpty(&p->pProp) ); + if ( Cbs_ManPropagate( p ) ) + return 1; + // check for satisfying assignment + assert( Cbs_QueIsEmpty(&p->pProp) ); + if ( Cbs_QueIsEmpty(&p->pJust) ) + return 0; + // quit using resource limits + p->Pars.nBTThis++; + p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead ); + if ( Cbs_ManCheckLimits( p ) ) + return 1; + // remember the state before branching + iPropHead = p->pProp.iHead; + Cbs_QueStore( &p->pJust, &iJustHead, &iJustTail ); + // find the decision variable + if ( p->Pars.fUseHighest ) + pVar = Cbs_ManDecideHighest( p ); + else if ( p->Pars.fUseLowest ) + pVar = Cbs_ManDecideLowest( p ); + else if ( p->Pars.fUseMaxFF ) + pVar = Cbs_ManDecideMaxFF( p ); + else assert( 0 ); + assert( Cbs_VarIsJust( pVar ) ); + // decide using fanout count! + if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) < Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) ) + { + // decide on first fanin + Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) ); + if ( !Cbs_ManSolve_rec( p ) ) + return 0; + if ( Cbs_ManCheckLimits( p ) ) + return 1; + Cbs_ManCancelUntil( p, iPropHead ); + Cbs_QueRestore( &p->pJust, iJustHead, iJustTail ); + // decide on second fanin + Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) ); + } + else + { + // decide on first fanin + Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) ); + if ( !Cbs_ManSolve_rec( p ) ) + return 0; + if ( Cbs_ManCheckLimits( p ) ) + return 1; + Cbs_ManCancelUntil( p, iPropHead ); + Cbs_QueRestore( &p->pJust, iJustHead, iJustTail ); + // decide on second fanin + Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) ); + } + if ( !Cbs_ManSolve_rec( p ) ) + return 0; + if ( Cbs_ManCheckLimits( p ) ) + return 1; + return 1; +} + +/**Function************************************************************* + + Synopsis [Looking for a satisfying assignment of the node.] + + Description [Assumes that each node has flag pObj->fMark0 set to 0. + Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided. + The node may be complemented. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ) +{ +// Gia_Obj_t * pTemp; +// int i; + int RetValue; +// Gia_ManForEachObj( p->pAig, pTemp, i ) +// assert( pTemp->fMark0 == 0 ); + assert( !p->pProp.iHead && !p->pProp.iTail ); + assert( !p->pJust.iHead && !p->pJust.iTail ); + p->Pars.nBTThis = p->Pars.nJustThis = 0; + Cbs_ManAssign( p, pObj ); + RetValue = Cbs_ManSolve_rec( p ); + if ( RetValue == 0 ) + Cbs_ManSaveModel( p, p->vModel ); + Cbs_ManCancelUntil( p, 0 ); + p->pJust.iHead = p->pJust.iTail = 0; + p->Pars.nBTTotal += p->Pars.nBTThis; + p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis ); + if ( Cbs_ManCheckLimits( p ) ) + return -1; + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Procedure to test the new SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cbs_ManSolveTest( 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; + Cbs_Man_t * p; + Vec_Int_t * vCex; + Vec_Int_t * vVisit; + Gia_Obj_t * pRoot; + int i, RetValue, clk = clock(); + Gia_ManCreateRefs( pGia ); + // create logic network + p = Cbs_ManAlloc(); + p->pAig = 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; + +// Gia_ManIncrementTravId( pGia ); + +//printf( "Output %6d : ", i ); +// iLit = Gia_Var2Lit( Gia_ObjHandle(Gia_ObjFanin0(pRoot)), Gia_ObjFaninC0(pRoot) ); +// RetValue = Cbs_ManSolve( p, &iLit, 1, nConfsMax, vCex ); + RetValue = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) ); + if ( RetValue == 1 ) + CountUnsat++; + else if ( RetValue == -1 ) + CountUndec++; + else + { +// int iLit, k; + vCex = Cbs_ReadModel( p ); + +// printf( "complemented = %d. ", Gia_ObjFaninC0(pRoot) ); +//printf( "conflicts = %6d max-frontier = %6d \n", p->Pars.nBTThis, p->Pars.nJustThis ); +// Vec_IntForEachEntry( vCex, iLit, k ) +// printf( "%s%d ", Gia_LitIsCompl(iLit)? "!": "", Gia_ObjCioId(Gia_ManObj(pGia,Gia_Lit2Var(iLit))) ); +// printf( "\n" ); + + Gia_SatVerifyPattern( pGia, pRoot, vCex, vVisit ); + assert( RetValue == 0 ); + CountSat++; + } +// Gia_ManCheckMark0( p ); +// Gia_ManCheckMark1( p ); + } + Cbs_ManStop( p ); +// Vec_IntFree( vCex ); + Vec_IntFree( vVisit ); + printf( "Unsat = %d. Sat = %d. Undec = %d. ", CountUnsat, CountSat, CountUndec ); + ABC_PRT( "Time", clock() - clk ); +} + + +/**Function************************************************************* + + Synopsis [Prints statistics of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cbs_ManSatPrintStats( Cbs_Man_t * p ) +{ + printf( "CO = %6d ", Gia_ManCoNum(p->pAig) ); + printf( "Conf = %5d ", p->Pars.nBTLimit ); + printf( "JustMax = %5d ", p->Pars.nJustLimit ); + printf( "\n" ); + printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ", + p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 ); + ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal ); + printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ", + p->nSatSat, 100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 ); + ABC_PRTP( "Time", p->timeSatSat, p->timeTotal ); + printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ", + p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 ); + ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal ); + ABC_PRT( "Total time", p->timeTotal ); +} + +/**Function************************************************************* + + Synopsis [Procedure to test the new SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus ) +{ + extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out ); + Cbs_Man_t * p; + Vec_Int_t * vCex, * vVisit, * vCexStore; + Vec_Str_t * vStatus; + Gia_Obj_t * pRoot; + int i, status, clk, clkTotal = clock(); + assert( Gia_ManRegNum(pAig) == 0 ); + // prepare AIG + Gia_ManCreateRefs( pAig ); + Gia_ManCleanMark0( pAig ); + Gia_ManCleanMark1( pAig ); + // create logic network + p = Cbs_ManAlloc(); + p->Pars.nBTLimit = nConfs; + p->pAig = pAig; + // create resulting data-structures + vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) ); + vCexStore = Vec_IntAlloc( 10000 ); + vVisit = Vec_IntAlloc( 100 ); + vCex = Cbs_ReadModel( p ); + // solve for each output + Gia_ManForEachCo( pAig, pRoot, i ) + { + Vec_IntClear( vCex ); + if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) ) + { + if ( Gia_ObjFaninC0(pRoot) ) + { + printf( "Constant 1 output of SRM!!!\n" ); + Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example + Vec_StrPush( vStatus, 0 ); + } + else + { + printf( "Constant 0 output of SRM!!!\n" ); + Vec_StrPush( vStatus, 1 ); + } + continue; + } + clk = clock(); + p->Pars.fUseHighest = 1; + p->Pars.fUseLowest = 0; + status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) ); + if ( status == -1 ) + { + p->Pars.fUseHighest = 0; + p->Pars.fUseLowest = 1; + status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) ); + } + Vec_StrPush( vStatus, (char)status ); + if ( status == -1 ) + { + p->nSatUndec++; + p->nConfUndec += p->Pars.nBTThis; + Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout + p->timeSatUndec += clock() - clk; + continue; + } + if ( status == 1 ) + { + p->nSatUnsat++; + p->nConfUnsat += p->Pars.nBTThis; + p->timeSatUnsat += clock() - clk; + continue; + } + p->nSatSat++; + p->nConfUnsat += p->Pars.nBTThis; +// Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit ); + Cec_ManSatAddToStore( vCexStore, vCex, i ); + p->timeSatSat += clock() - clk; + } + Vec_IntFree( vVisit ); + p->nSatTotal = Gia_ManPoNum(pAig); + p->timeTotal = clock() - clkTotal; +// Cbs_ManSatPrintStats( p ); + Cbs_ManStop( p ); + *pvStatus = vStatus; +// printf( "Total number of cex literals = %d. (Ave = %d)\n", +// Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat, +// (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat ); + return vCexStore; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/gia/giaCSat0.c b/src/aig/gia/giaCSat0.c deleted file mode 100644 index a0d567a2..00000000 --- a/src/aig/gia/giaCSat0.c +++ /dev/null @@ -1,328 +0,0 @@ -/**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" ); -// else -// printf( "Gia_SatVerifyPattern(): Verification succeeded.\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 deleted file mode 100644 index 12b7071f..00000000 --- a/src/aig/gia/giaCSat1.c +++ /dev/null @@ -1,602 +0,0 @@ -/**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/giaCSat2.c b/src/aig/gia/giaCSat2.c deleted file mode 100644 index 1e7cc949..00000000 --- a/src/aig/gia/giaCSat2.c +++ /dev/null @@ -1,745 +0,0 @@ -/**CFile**************************************************************** - - FileName [giaCSat2.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Scalable AIG package.] - - Synopsis [A simple circuit-based solver.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: giaCSat2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "gia.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Cbs_Par_t_ Cbs_Par_t; -struct Cbs_Par_t_ -{ - // conflict limits - int nBTLimit; // limit on the number of conflicts - int nJustLimit; // limit on the size of justification queue - // current parameters - int nBTThis; // number of conflicts - int nJustThis; // max size of the frontier - int nBTTotal; // total number of conflicts - int nJustTotal; // total size of the frontier - // decision heuristics - int fUseHighest; // use node with the highest ID - int fUseLowest; // use node with the highest ID - int fUseMaxFF; // use node with the largest fanin fanout - // other - int fVerbose; -}; - -typedef struct Cbs_Que_t_ Cbs_Que_t; -struct Cbs_Que_t_ -{ - int iHead; // beginning of the queue - int iTail; // end of the queue - int nSize; // allocated size - Gia_Obj_t ** pData; // nodes stored in the queue -}; - -typedef struct Cbs_Man_t_ Cbs_Man_t; -struct Cbs_Man_t_ -{ - Cbs_Par_t Pars; // parameters - Gia_Man_t * pAig; // AIG manager - Cbs_Que_t pProp; // propagation queue - Cbs_Que_t pJust; // justification queue - Vec_Int_t * vModel; // satisfying assignment -}; - -static inline int Cbs_VarIsAssigned( Gia_Obj_t * pVar ) { return pVar->fMark0; } -static inline void Cbs_VarAssign( Gia_Obj_t * pVar ) { assert(!pVar->fMark0); pVar->fMark0 = 1; } -static inline void Cbs_VarUnassign( Gia_Obj_t * pVar ) { assert(pVar->fMark0); pVar->fMark0 = 0; pVar->fMark1 = 0; } -static inline int Cbs_VarValue( Gia_Obj_t * pVar ) { assert(pVar->fMark0); return pVar->fMark1; } -static inline void Cbs_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0); pVar->fMark1 = v; } -static inline int Cbs_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)); } -static inline int Cbs_VarFanin0Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); } -static inline int Cbs_VarFanin1Value( Gia_Obj_t * pVar ) { return !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); } - -#define Cbs_QueForEachEntry( Que, pObj, i ) \ - for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ ) - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Sets default values of the parameters.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cbs_SetDefaultParams( Cbs_Par_t * pPars ) -{ - memset( pPars, 0, sizeof(Cbs_Par_t) ); - pPars->nBTLimit = 1000; // limit on the number of conflicts - pPars->nJustLimit = 100; // limit on the size of justification queue - pPars->fUseHighest = 1; // use node with the highest ID - pPars->fUseLowest = 0; // use node with the highest ID - pPars->fUseMaxFF = 0; // use node with the largest fanin fanout - pPars->fVerbose = 1; // print detailed statistics -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cbs_Man_t * Cbs_ManAlloc() -{ - Cbs_Man_t * p; - p = ABC_CALLOC( Cbs_Man_t, 1 ); - p->pProp.nSize = p->pJust.nSize = 10000; - p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize ); - p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize ); - p->vModel = Vec_IntAlloc( 1000 ); - Cbs_SetDefaultParams( &p->Pars ); - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cbs_ManStop( Cbs_Man_t * p ) -{ - Vec_IntFree( p->vModel ); - ABC_FREE( p->pProp.pData ); - ABC_FREE( p->pJust.pData ); - ABC_FREE( p ); -} - -/**Function************************************************************* - - Synopsis [Returns satisfying assignment.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Cbs_ReadModel( Cbs_Man_t * p ) -{ - return p->vModel; -} - - - - -/**Function************************************************************* - - Synopsis [Returns 1 if the solver is out of limits.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Cbs_ManCheckLimits( Cbs_Man_t * p ) -{ - return p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit; -} - -/**Function************************************************************* - - Synopsis [Saves the satisfying assignment as an array of literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Cbs_ManSaveModel( Cbs_Man_t * p, Vec_Int_t * vCex ) -{ - Gia_Obj_t * pVar; - int i; - Vec_IntClear( vCex ); - p->pProp.iHead = 0; - Cbs_QueForEachEntry( p->pProp, pVar, i ) - if ( Gia_ObjIsCi(pVar) ) - Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Cbs_QueIsEmpty( Cbs_Que_t * p ) -{ - return p->iHead == p->iTail; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Cbs_QuePush( Cbs_Que_t * p, Gia_Obj_t * pObj ) -{ - if ( p->iTail == p->nSize ) - { - p->nSize *= 2; - p->pData = ABC_REALLOC( Gia_Obj_t *, p->pData, p->nSize ); - } - p->pData[p->iTail++] = pObj; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if the object in the queue.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Cbs_QueHasNode( Cbs_Que_t * p, Gia_Obj_t * pObj ) -{ - Gia_Obj_t * pTemp; - int i; - Cbs_QueForEachEntry( *p, pTemp, i ) - if ( pTemp == pObj ) - return 1; - return 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Cbs_QueStore( Cbs_Que_t * p, int * piHeadOld, int * piTailOld ) -{ - int i; - *piHeadOld = p->iHead; - *piTailOld = p->iTail; - for ( i = *piHeadOld; i < *piTailOld; i++ ) - Cbs_QuePush( p, p->pData[i] ); - p->iHead = *piTailOld; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Cbs_QueRestore( Cbs_Que_t * p, int iHeadOld, int iTailOld ) -{ - p->iHead = iHeadOld; - p->iTail = iTailOld; -} - - -/**Function************************************************************* - - Synopsis [Max number of fanins fanouts.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Cbs_VarFaninFanoutMax( Cbs_Man_t * p, Gia_Obj_t * pObj ) -{ - int Count0, Count1; - assert( !Gia_IsComplement(pObj) ); - assert( Gia_ObjIsAnd(pObj) ); - Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) ); - Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) ); - return ABC_MAX( Count0, Count1 ); -} - -/**Function************************************************************* - - Synopsis [Find variable with the highest ID.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Gia_Obj_t * Cbs_ManDecideHighest( Cbs_Man_t * p ) -{ - Gia_Obj_t * pObj, * pObjMax = NULL; - int i; - Cbs_QueForEachEntry( p->pJust, pObj, i ) - if ( pObjMax == NULL || pObjMax < pObj ) - pObjMax = pObj; - return pObjMax; -} - -/**Function************************************************************* - - Synopsis [Find variable with the lowest ID.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Gia_Obj_t * Cbs_ManDecideLowest( Cbs_Man_t * p ) -{ - Gia_Obj_t * pObj, * pObjMin = NULL; - int i; - Cbs_QueForEachEntry( p->pJust, pObj, i ) - if ( pObjMin == NULL || pObjMin > pObj ) - pObjMin = pObj; - return pObjMin; -} - -/**Function************************************************************* - - Synopsis [Find variable with the maximum number of fanin fanouts.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Gia_Obj_t * Cbs_ManDecideMaxFF( Cbs_Man_t * p ) -{ - Gia_Obj_t * pObj, * pObjMax = NULL; - int i, iMaxFF = 0, iCurFF; - assert( p->pAig->pRefs != NULL ); - Cbs_QueForEachEntry( p->pJust, pObj, i ) - { - iCurFF = Cbs_VarFaninFanoutMax( p, pObj ); - assert( iCurFF > 0 ); - if ( iMaxFF < iCurFF ) - { - iMaxFF = iCurFF; - pObjMax = pObj; - } - } - return pObjMax; -} - - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound ) -{ - Gia_Obj_t * pVar; - int i; - assert( iBound <= p->pProp.iTail ); - p->pProp.iHead = iBound; - Cbs_QueForEachEntry( p->pProp, pVar, i ) - Cbs_VarUnassign( pVar ); - p->pProp.iTail = iBound; -} - -/**Function************************************************************* - - Synopsis [Assigns the variables a value.] - - Description [Returns 1 if conflict; 0 if no conflict.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj ) -{ - Gia_Obj_t * pObjR = Gia_Regular(pObj); - assert( Gia_ObjIsCand(pObjR) ); - assert( !Cbs_VarIsAssigned(pObjR) ); - Cbs_VarAssign( pObjR ); - Cbs_VarSetValue( pObjR, !Gia_IsComplement(pObj) ); - Cbs_QuePush( &p->pProp, pObjR ); -} - -/**Function************************************************************* - - Synopsis [Propagates a variable.] - - Description [Returns 1 if conflict; 0 if no conflict.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar ) -{ - int Value0, Value1; - assert( !Gia_IsComplement(pVar) ); - assert( Cbs_VarIsAssigned(pVar) ); - if ( Gia_ObjIsCi(pVar) ) - return 0; - assert( Gia_ObjIsAnd(pVar) ); - Value0 = Cbs_VarFanin0Value(pVar); - Value1 = Cbs_VarFanin1Value(pVar); - if ( Cbs_VarValue(pVar) ) - { // value is 1 - if ( Value0 == 0 || Value1 == 0 ) // one is 0 - return 1; - if ( Value0 == 2 ) // first is unassigned - Cbs_ManAssign( p, Gia_ObjChild0(pVar) ); - if ( Value1 == 2 ) // first is unassigned - Cbs_ManAssign( p, Gia_ObjChild1(pVar) ); - return 0; - } - // value is 0 - if ( Value0 == 0 || Value1 == 0 ) // one is 0 - return 0; - if ( Value0 == 1 && Value1 == 1 ) // both are 1 - return 1; - if ( Value0 == 1 || Value1 == 1 ) // one is 1 - { - if ( Value0 == 2 ) // first is unassigned - Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) ); - if ( Value1 == 2 ) // first is unassigned - Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) ); - return 0; - } - assert( Cbs_VarIsJust(pVar) ); - assert( !Cbs_QueHasNode( &p->pJust, pVar ) ); - Cbs_QuePush( &p->pJust, pVar ); - return 0; -} - -/**Function************************************************************* - - Synopsis [Propagates a variable.] - - Description [Returns 1 if conflict; 0 if no conflict.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar ) -{ - int Value0, Value1; - assert( !Gia_IsComplement(pVar) ); - assert( Gia_ObjIsAnd(pVar) ); - assert( Cbs_VarIsAssigned(pVar) ); - assert( !Cbs_VarValue(pVar) ); - Value0 = Cbs_VarFanin0Value(pVar); - Value1 = Cbs_VarFanin1Value(pVar); - // value is 0 - if ( Value0 == 0 || Value1 == 0 ) // one is 0 - return 0; - if ( Value0 == 1 && Value1 == 1 ) // both are 1 - return 1; - assert( Value0 == 1 || Value1 == 1 ); - if ( Value0 == 2 ) // first is unassigned - Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) ); - if ( Value1 == 2 ) // first is unassigned - Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) ); - return 0; -} - -/**Function************************************************************* - - Synopsis [Propagates all variables.] - - Description [Returns 1 if conflict; 0 if no conflict.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cbs_ManPropagate( Cbs_Man_t * p ) -{ - Gia_Obj_t * pVar; - int i, k; - while ( 1 ) - { - Cbs_QueForEachEntry( p->pProp, pVar, i ) - { - if ( Cbs_ManPropagateOne( p, pVar ) ) - return 1; - } - p->pProp.iHead = p->pProp.iTail; - k = p->pJust.iHead; - Cbs_QueForEachEntry( p->pJust, pVar, i ) - { - if ( Cbs_VarIsJust( pVar ) ) - p->pJust.pData[k++] = pVar; - else if ( Cbs_ManPropagateTwo( p, pVar ) ) - return 1; - } - if ( k == p->pJust.iTail ) - break; - p->pJust.iTail = k; - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Solve the problem recursively.] - - Description [Returns 1 if unsat or undecided; 0 if satisfiable.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cbs_ManSolve_rec( Cbs_Man_t * p ) -{ - Gia_Obj_t * pVar; - int iPropHead, iJustHead, iJustTail; - // propagate assignments - assert( !Cbs_QueIsEmpty(&p->pProp) ); - if ( Cbs_ManPropagate( p ) ) - return 1; - // check for satisfying assignment - assert( Cbs_QueIsEmpty(&p->pProp) ); - if ( Cbs_QueIsEmpty(&p->pJust) ) - return 0; - // quit using resource limits - p->Pars.nBTThis++; - p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead ); - if ( Cbs_ManCheckLimits( p ) ) - return 1; - // remember the state before branching - iPropHead = p->pProp.iHead; - Cbs_QueStore( &p->pJust, &iJustHead, &iJustTail ); - // find the decision variable - if ( p->Pars.fUseHighest ) - pVar = Cbs_ManDecideHighest( p ); - else if ( p->Pars.fUseLowest ) - pVar = Cbs_ManDecideLowest( p ); - else if ( p->Pars.fUseMaxFF ) - pVar = Cbs_ManDecideMaxFF( p ); - else assert( 0 ); - assert( Cbs_VarIsJust( pVar ) ); - // decide using fanout count! - if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) < Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) ) - { - // decide on first fanin - Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) ); - if ( !Cbs_ManSolve_rec( p ) ) - return 0; - if ( Cbs_ManCheckLimits( p ) ) - return 1; - Cbs_ManCancelUntil( p, iPropHead ); - Cbs_QueRestore( &p->pJust, iJustHead, iJustTail ); - // decide on second fanin - Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) ); - } - else - { - // decide on first fanin - Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) ); - if ( !Cbs_ManSolve_rec( p ) ) - return 0; - if ( Cbs_ManCheckLimits( p ) ) - return 1; - Cbs_ManCancelUntil( p, iPropHead ); - Cbs_QueRestore( &p->pJust, iJustHead, iJustTail ); - // decide on second fanin - Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) ); - } - if ( !Cbs_ManSolve_rec( p ) ) - return 0; - if ( Cbs_ManCheckLimits( p ) ) - return 1; - return 1; -} - -/**Function************************************************************* - - Synopsis [Looking for a satisfying assignment of the node.] - - Description [Assumes that each node has flag pObj->fMark0 set to 0. - Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided. - The node may be complemented. ] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ) -{ -// Gia_Obj_t * pTemp; -// int i; - int RetValue; -// Gia_ManForEachObj( p->pAig, pTemp, i ) -// assert( pTemp->fMark0 == 0 ); - assert( !p->pProp.iHead && !p->pProp.iTail ); - assert( !p->pJust.iHead && !p->pJust.iTail ); - p->Pars.nBTThis = p->Pars.nJustThis = 0; - Cbs_ManAssign( p, pObj ); - RetValue = Cbs_ManSolve_rec( p ); - if ( RetValue == 0 ) - Cbs_ManSaveModel( p, p->vModel ); - Cbs_ManCancelUntil( p, 0 ); - p->pJust.iHead = p->pJust.iTail = 0; - p->Pars.nBTTotal += p->Pars.nBTThis; - p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis ); - if ( Cbs_ManCheckLimits( p ) ) - return -1; - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Procedure to test the new SAT solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cbs_ManSolveTest( 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; - Cbs_Man_t * p; - Vec_Int_t * vCex; - Vec_Int_t * vVisit; - Gia_Obj_t * pRoot; - int i, RetValue, clk = clock(); - Gia_ManCreateRefs( pGia ); - // create logic network - p = Cbs_ManAlloc(); - p->pAig = 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; - -// Gia_ManIncrementTravId( pGia ); - -//printf( "Output %6d : ", i ); -// iLit = Gia_Var2Lit( Gia_ObjHandle(Gia_ObjFanin0(pRoot)), Gia_ObjFaninC0(pRoot) ); -// RetValue = Cbs_ManSolve( p, &iLit, 1, nConfsMax, vCex ); - RetValue = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) ); - if ( RetValue == 1 ) - CountUnsat++; - else if ( RetValue == -1 ) - CountUndec++; - else - { - int iLit, k; - vCex = Cbs_ReadModel( p ); - -// printf( "complemented = %d. ", Gia_ObjFaninC0(pRoot) ); -//printf( "conflicts = %6d max-frontier = %6d \n", p->Pars.nBTThis, p->Pars.nJustThis ); -// Vec_IntForEachEntry( vCex, iLit, k ) -// printf( "%s%d ", Gia_LitIsCompl(iLit)? "!": "", Gia_ObjCioId(Gia_ManObj(pGia,Gia_Lit2Var(iLit))) ); -// printf( "\n" ); - - Gia_SatVerifyPattern( pGia, pRoot, vCex, vVisit ); - assert( RetValue == 0 ); - CountSat++; - } -// Gia_ManCheckMark0( p ); -// Gia_ManCheckMark1( p ); - } - Cbs_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 deleted file mode 100644 index 12f6895a..00000000 --- a/src/aig/gia/giaCSatA.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/giaCSatB.c b/src/aig/gia/giaCSatB.c deleted file mode 100644 index e1f68c6f..00000000 --- a/src/aig/gia/giaCSatB.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/giaCof.c b/src/aig/gia/giaCof.c index c5efa839..b256100c 100644 --- a/src/aig/gia/giaCof.c +++ b/src/aig/gia/giaCof.c @@ -859,7 +859,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose if ( fVerbose ) { printf( "Cofactoring %d signals.\n", Vec_IntSize(vSigs) ); - Gia_ManPrintStats( p ); + Gia_ManPrintStats( p, 0 ); } if ( Vec_IntSize( vSigs ) > 200 ) { @@ -885,7 +885,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose if ( fVerbose ) printf( "Cofactored variable %d.\n", iVar ); if ( fVerbose ) - Gia_ManPrintStats( pAig ); + Gia_ManPrintStats( pAig, 0 ); } Vec_IntFree( vSigsNew ); return pAig; diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 0c536dab..2510f572 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -28,6 +28,226 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Removes pointers to the unmarked nodes..] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupRemapEquiv( Gia_Man_t * pNew, Gia_Man_t * p ) +{ + Vec_Int_t * vClass; + int i, k, iNode, iRepr, iPrev; + if ( p->pReprs == NULL ) + return; + assert( pNew->pReprs == NULL && pNew->pNexts == NULL ); + // start representatives + pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) ); + for ( i = 0; i < Gia_ManObjNum(pNew); i++ ) + Gia_ObjSetRepr( pNew, i, GIA_VOID ); + // iterate over constant candidates + Gia_ManForEachConst( p, i ) + Gia_ObjSetRepr( pNew, Gia_Lit2Var(Gia_ManObj(p, i)->Value), 0 ); + // iterate over class candidates + vClass = Vec_IntAlloc( 100 ); + Gia_ManForEachClass( p, i ) + { + Vec_IntClear( vClass ); + Gia_ClassForEachObj( p, i, k ) + Vec_IntPushUnique( vClass, Gia_Lit2Var(Gia_ManObj(p, k)->Value) ); + assert( Vec_IntSize( vClass ) > 1 ); + Vec_IntSort( vClass, 0 ); + iRepr = iPrev = Vec_IntEntry( vClass, 0 ); + Vec_IntForEachEntryStart( vClass, iNode, k, 1 ) + { + Gia_ObjSetRepr( pNew, iNode, iRepr ); + assert( iPrev < iNode ); + iPrev = iNode; + } + } + Vec_IntFree( vClass ); + pNew->pNexts = Gia_ManDeriveNexts( pNew ); +} + +/**Function************************************************************* + + Synopsis [Remaps combinational inputs when objects are DFS ordered.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupRemapCis( Gia_Man_t * pNew, Gia_Man_t * p ) +{ + Gia_Obj_t * pObj, * pObjNew; + int i; + assert( Vec_IntSize(p->vCis) == Vec_IntSize(pNew->vCis) ); + Gia_ManForEachCi( p, pObj, i ) + { + assert( Gia_ObjCioId(pObj) == i ); + pObjNew = Gia_ObjFromLit( pNew, pObj->Value ); + assert( !Gia_IsComplement(pObjNew) ); + Vec_IntWriteEntry( pNew->vCis, i, Gia_ObjId(pNew, pObjNew) ); + Gia_ObjSetCioId( pObjNew, i ); + } +} + +/**Function************************************************************* + + Synopsis [Remaps combinational outputs when objects are DFS ordered.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupRemapCos( Gia_Man_t * pNew, Gia_Man_t * p ) +{ + Gia_Obj_t * pObj, * pObjNew; + int i; + assert( Vec_IntSize(p->vCos) == Vec_IntSize(pNew->vCos) ); + Gia_ManForEachCo( p, pObj, i ) + { + assert( Gia_ObjCioId(pObj) == i ); + pObjNew = Gia_ObjFromLit( pNew, pObj->Value ); + assert( !Gia_IsComplement(pObjNew) ); + Vec_IntWriteEntry( pNew->vCos, i, Gia_ObjId(pNew, pObjNew) ); + Gia_ObjSetCioId( pObjNew, i ); + } +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManDupOrderDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return pObj->Value; + if ( Gia_ObjIsCi(pObj) ) + return pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + if ( Gia_ObjIsCo(pObj) ) + return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin1(pObj) ); + return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG while putting objects in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCo( p, pObj, i ) + Gia_ManDupOrderDfs_rec( pNew, p, pObj ); + Gia_ManForEachCi( p, pObj, i ) + if ( !~pObj->Value ) + pObj->Value = Gia_ManAppendCi(pNew); + assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) ); + Gia_ManDupRemapCis( pNew, p ); + Gia_ManDupRemapEquiv( pNew, p ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG while putting objects in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCoReverse( p, pObj, i ) + Gia_ManDupOrderDfs_rec( pNew, p, pObj ); + Gia_ManForEachCi( p, pObj, i ) + if ( !~pObj->Value ) + pObj->Value = Gia_ManAppendCi(pNew); + assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) ); + Gia_ManDupRemapCis( pNew, p ); + Gia_ManDupRemapCos( pNew, p ); + Gia_ManDupRemapEquiv( pNew, p ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG while putting first PIs, then nodes, then POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManDupRemapEquiv( pNew, p ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + assert( Gia_ManIsNormalized(pNew) ); + return pNew; +} + + + /**Function************************************************************* Synopsis [Duplicates AIG without any changes.] @@ -296,7 +516,7 @@ int Gia_ManDupDfs2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) if ( pNew->pHTable ) return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); -} +} /**Function************************************************************* diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c index 6c2f00df..fa172f70 100644 --- a/src/aig/gia/giaEmbed.c +++ b/src/aig/gia/giaEmbed.c @@ -36,6 +36,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define GIA_PLACE_SIZE 0x7fff +// objects will be placed in box [0, GIA_PLACE_SIZE] x [0, GIA_PLACE_SIZE] typedef float Emb_Dat_t; @@ -247,6 +249,7 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia ) Emb_ObjAddFanin( Emb_ManObj(p,Gia_ObjValue(pObjRo)), Emb_ManObj(p,Gia_ObjValue(pObjRi)) ); assert( nNodes == Emb_ManNodeNum(p) ); assert( hHandle == p->nObjData ); + assert( p->nObjs == Gia_ManObjNum(pGia) ); if ( hHandle != p->nObjData ) printf( "Emb_ManStartSimple(): Fatal error in internal representation.\n" ); // make sure the fanin/fanout counters are correct @@ -1407,7 +1410,7 @@ void Emb_ManComputeSolutions( Emb_Man_t * p, int nDims, int nSols ) /**Function************************************************************* - Synopsis [Projects into square of size [0;0xffff] x [0;0xffff].] + Synopsis [Projects into square of size [0;GIA_PLACE_SIZE] x [0;GIA_PLACE_SIZE].] Description [] @@ -1432,7 +1435,7 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols ) Min0 = ABC_MIN( Min0, pY0[k] ); Max0 = ABC_MAX( Max0, pY0[k] ); } - Str0 = 1.0*0xffff/(Max0 - Min0); + Str0 = 1.0*GIA_PLACE_SIZE/(Max0 - Min0); // update the coordinates for ( k = 0; k < p->nObjs; k++ ) pY0[k] = (pY0[k] != 0.0) ? ((pY0[k] - Min0) * Str0) : 0.0; @@ -1446,7 +1449,7 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols ) Min1 = ABC_MIN( Min1, pY1[k] ); Max1 = ABC_MAX( Max1, pY1[k] ); } - Str1 = 1.0*0xffff/(Max1 - Min1); + Str1 = 1.0*GIA_PLACE_SIZE/(Max1 - Min1); // update the coordinates for ( k = 0; k < p->nObjs; k++ ) pY1[k] = (pY1[k] != 0.0) ? ((pY1[k] - Min1) * Str1) : 0.0; @@ -1455,12 +1458,12 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols ) pPerm0 = Gia_SortFloats( pY0, NULL, p->nObjs ); pPerm1 = Gia_SortFloats( pY1, NULL, p->nObjs ); - // average solutions and project them into square [0;0xffff] x [0;0xffff] + // average solutions and project them into square [0;GIA_PLACE_SIZE] x [0;GIA_PLACE_SIZE] 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); + p->pPlacement[2*pPerm0[k]+0] = (unsigned short)(int)(1.0 * k * GIA_PLACE_SIZE / p->nObjs); + p->pPlacement[2*pPerm1[k]+1] = (unsigned short)(int)(1.0 * k * GIA_PLACE_SIZE / p->nObjs); } ABC_FREE( pPerm0 ); ABC_FREE( pPerm1 ); @@ -1568,8 +1571,8 @@ void Emb_ManPlacementRefine( Emb_Man_t * p, int nIters, int fVerbose ) pPermY = Gia_SortFloats( pVertY, NULL, p->nObjs ); for ( k = 0; k < p->nObjs; k++ ) { - p->pPlacement[2*pPermX[k]+0] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs); - p->pPlacement[2*pPermY[k]+1] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs); + p->pPlacement[2*pPermX[k]+0] = (unsigned short)(int)(1.0 * k * GIA_PLACE_SIZE / p->nObjs); + p->pPlacement[2*pPermY[k]+1] = (unsigned short)(int)(1.0 * k * GIA_PLACE_SIZE / p->nObjs); } ABC_FREE( pPermX ); ABC_FREE( pPermY ); @@ -1783,7 +1786,7 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars ) { Emb_Man_t * p; - int clk, clkSetup; + int i, clk, clkSetup; // Gia_ManTestDistance( pGia ); // transform AIG into internal data-structure @@ -1843,6 +1846,17 @@ if ( pPars->fVerbose ) ABC_PRT( "Image dump", clock() - clk ); } + // transfer placement + if ( Gia_ManObjNum(pGia) == p->nObjs ) + { + // assuming normalized ordering of the AIG + pGia->pPlacement = ABC_CALLOC( Gia_Plc_t, p->nObjs ); + for ( i = 0; i < p->nObjs; i++ ) + { + pGia->pPlacement[i].xCoord = p->pPlacement[2*i+0]; + pGia->pPlacement[i].yCoord = p->pPlacement[2*i+1]; + } + } Emb_ManStop( p ); } diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index b87c77e5..79345fd0 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -226,6 +226,10 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) assert( Gia_ManEquivCheckLits( p, nLits ) ); if ( fVerbose ) { + printf( "Const0 = " ); + Gia_ManForEachConst( p, i ) + printf( "%d ", i ); + printf( "\n" ); Counter = 0; Gia_ManForEachClass( p, i ) Gia_ManEquivPrintOne( p, i, ++Counter ); @@ -275,15 +279,15 @@ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut ) { Gia_Obj_t * pRepr; - if ( ~pObj->Value ) - return; - assert( Gia_ObjIsAnd(pObj) ); if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) ) { Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut ); pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut ); Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll, fDualOut ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); @@ -303,18 +307,25 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose ) { Gia_Man_t * pNew; - Gia_Obj_t * pObj, * pRepr; + Gia_Obj_t * pObj; int i; + if ( !p->pReprs ) + { + printf( "Gia_ManEquivReduce(): Equivalence classes are not available.\n" ); + return NULL; + } if ( fDualOut && (Gia_ManPoNum(p) & 1) ) { printf( "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" ); return NULL; } +/* if ( !Gia_ManCheckTopoOrder( p ) ) { printf( "Gia_ManEquivReduce(): AIG is not in a correct topological order.\n" ); return NULL; } +*/ Gia_ManSetPhase( p ); if ( fDualOut ) Gia_ManEquivSetColors( p, fVerbose ); @@ -323,11 +334,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) - { pObj->Value = Gia_ManAppendCi(pNew); - if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) ) - pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); - } Gia_ManHashAlloc( pNew ); Gia_ManForEachCo( p, pObj, i ) Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut ); @@ -662,11 +669,13 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose ) printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" ); return NULL; } +/* if ( !Gia_ManCheckTopoOrder( p ) ) { printf( "Gia_ManSpecReduce(): AIG is not in a correct topological order.\n" ); return NULL; } +*/ vXorLits = Vec_IntAlloc( 1000 ); Gia_ManSetPhase( p ); Gia_ManFillValue( p ); @@ -786,11 +795,13 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames printf( "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" ); return NULL; } +/* if ( !Gia_ManCheckTopoOrder( p ) ) { printf( "Gia_ManSpecReduceInit(): AIG is not in a correct topological order.\n" ); return NULL; } +*/ assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 ); p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) ); vXorLits = Vec_IntAlloc( 1000 ); diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c index 8bc38ed9..a7cae8fe 100644 --- a/src/aig/gia/giaHash.c +++ b/src/aig/gia/giaHash.c @@ -86,7 +86,7 @@ static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1 ) void Gia_ManHashAlloc( Gia_Man_t * p ) { assert( p->pHTable == NULL ); - p->nHTable = Aig_PrimeCudd( p->nObjsAlloc / 3 ); + p->nHTable = Aig_PrimeCudd( p->nObjsAlloc ); p->pHTable = ABC_CALLOC( int, p->nHTable ); } @@ -174,6 +174,34 @@ void Gia_ManHashResize( Gia_Man_t * p ) ABC_FREE( pHTableOld ); } +/**Function******************************************************************** + + Synopsis [Profiles the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Gia_ManHashProfile( Gia_Man_t * p ) +{ + Gia_Obj_t * pEntry; + int i, Counter; + printf( "Table size = %d. Entries = %d.\n", p->nHTable, Gia_ManAndNum(p) ); + for ( i = 0; i < p->nHTable; i++ ) + { + Counter = 0; + for ( pEntry = (p->pHTable[i]? Gia_ManObj(p, Gia_Lit2Var(p->pHTable[i])) : NULL); + pEntry; + pEntry = (pEntry->Value? Gia_ManObj(p, Gia_Lit2Var(pEntry->Value)) : NULL) ) + Counter++; + if ( Counter ) + printf( "%d ", Counter ); + } + printf( "\n" ); +} /**Function************************************************************* diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 4439453d..dba90507 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -70,6 +70,8 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFree( p->vFlopClasses ); Vec_IntFree( p->vCis ); Vec_IntFree( p->vCos ); + ABC_FREE( p->pPlacement ); + ABC_FREE( p->pSwitching ); ABC_FREE( p->pCexComb ); ABC_FREE( p->pIso ); ABC_FREE( p->pMapping ); @@ -128,17 +130,48 @@ void Gia_ManPrintClasses( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_ManPrintStats( Gia_Man_t * p ) +void Gia_ManPrintPlacement( Gia_Man_t * p ) +{ + int i, nFixed = 0, nUndef = 0; + if ( p->pPlacement == NULL ) + return; + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + { + nFixed += p->pPlacement[i].fFixed; + nUndef += p->pPlacement[i].fUndef; + } + printf( "Placement: Objects = %8d. Fixed = %8d. Undef = %8d.\n", Gia_ManObjNum(p), nFixed, nUndef ); +} + +/**Function************************************************************* + + Synopsis [Prints stats for the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ) { if ( p->pName ) printf( "%8s : ", p->pName ); - printf( "i/o =%7d/%7d ", Gia_ManPiNum(p), Gia_ManPoNum(p) ); + printf( "i/o =%7d/%7d", Gia_ManPiNum(p), Gia_ManPoNum(p) ); if ( Gia_ManRegNum(p) ) - printf( "ff =%7d ", Gia_ManRegNum(p) ); - printf( "and =%8d ", Gia_ManAndNum(p) ); - printf( "lev =%5d ", Gia_ManLevelNum(p) ); - printf( "cut =%5d ", Gia_ManCrossCut(p) ); - printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) ); + printf( " ff =%7d", Gia_ManRegNum(p) ); + printf( " and =%8d", Gia_ManAndNum(p) ); + printf( " lev =%5d", Gia_ManLevelNum(p) ); + printf( " cut =%5d", Gia_ManCrossCut(p) ); + printf( " mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) ); + if ( fSwitch ) + { + if ( p->pSwitching ) + printf( " power =%7.2f", Gia_ManEvaluateSwitching(p) ); + else + printf( " power =%7.2f", Gia_ManComputeSwitching(p, 48, 16, 0) ); + } // printf( "obj =%5d ", Gia_ManObjNum(p) ); printf( "\n" ); @@ -147,6 +180,8 @@ void Gia_ManPrintStats( Gia_Man_t * p ) Gia_ManEquivPrintClasses( p, 0, 0.0 ); if ( p->pMapping ) Gia_ManPrintMappingStats( p ); + if ( p->pPlacement ) + Gia_ManPrintPlacement( p ); // print register classes // Gia_ManPrintClasses( p ); } diff --git a/src/aig/gia/giaPat.c b/src/aig/gia/giaPat.c new file mode 100644 index 00000000..7968932c --- /dev/null +++ b/src/aig/gia/giaPat.c @@ -0,0 +1,129 @@ +/**CFile**************************************************************** + + FileName [gia.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: gia.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); } + +//////////////////////////////////////////////////////////////////////// +/// 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; + 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 [Checks if the counter-examples asserts the output.] + + Description [Assumes that fMark0 and fMark1 are clean. Leaves them clean.] + + 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 ) +// Sat_ObjSetXValue( Gia_ManObj(p, Gia_Lit2Var(Entry)), Gia_LitIsCompl(Entry)? GIA_ZER : GIA_ONE ); + Sat_ObjSetXValue( Gia_ManCi(p, Gia_Lit2Var(Entry)), Gia_LitIsCompl(Entry)? 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" ); +// else +// printf( "Gia_SatVerifyPattern(): Verification succeeded.\n" ); +// assert( Value == GIA_ONE ); + // clean the nodes + Gia_ManForEachObjVec( vVisit, p, pObj, i ) + Sat_ObjSetXValue( pObj, 0 ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c index 71aefec3..713f224b 100644 --- a/src/aig/gia/giaSwitch.c +++ b/src/aig/gia/giaSwitch.c @@ -73,13 +73,13 @@ static inline unsigned * Gia_SwiDataCo( Gia_ManSwi_t * p, int i ) { return p->p void Gia_ManSetDefaultParamsSwi( Gia_ParSwi_t * p ) { memset( p, 0, sizeof(Gia_ParSwi_t) ); - p->nWords = 1; // the number of machine words of simulatation data + p->nWords = 10; // the number of machine words of simulatation data p->nIters = 48; // the number of all timeframes to simulate p->nPref = 16; // the number of first timeframes to skip when computing switching p->nRandPiFactor = 2; // primary input transition probability (-1=3/8; 0=1/2; 1=1/4; 2=1/8, etc) p->fProbOne = 0; // compute probability of signal being one (if 0, compute probability of switching) p->fProbTrans = 1; // compute signal transition probability (if 0, compute transition probability using probability of being one) - p->fVerbose = 1; // enables verbose output + p->fVerbose = 0; // enables verbose output } /**Function************************************************************* @@ -483,12 +483,14 @@ static inline void Gia_ManSwiSimulateRound( Gia_ManSwi_t * p, int fCount ) else if ( Gia_ObjIsCo(pObj) ) { assert( Gia_ObjValue(pObj) == GIA_NONE ); - Gia_ManSwiSimulateCo( p, iCos++, pObj ); +// Gia_ManSwiSimulateCo( p, iCos++, pObj ); + Gia_ManSwiSimulateCo( p, Gia_ObjCioId(pObj), pObj ); } else // if ( Gia_ObjIsCi(pObj) ) { assert( Gia_ObjValue(pObj) < p->pAig->nFront ); - Gia_ManSwiSimulateCi( p, pObj, iCis++ ); +// Gia_ManSwiSimulateCi( p, pObj, iCis++ ); + Gia_ManSwiSimulateCi( p, pObj, Gia_ObjCioId(pObj) ); } if ( fCount && !Gia_ObjIsCo(pObj) ) { @@ -498,8 +500,8 @@ static inline void Gia_ManSwiSimulateRound( Gia_ManSwi_t * p, int fCount ) p->pData1[i] += Gia_ManSwiSimInfoCountOnes( p, Gia_ObjValue(pObj) ); } } - assert( Gia_ManCiNum(p->pAig) == iCis ); - assert( Gia_ManCoNum(p->pAig) == iCos ); +// assert( Gia_ManCiNum(p->pAig) == iCis ); +// assert( Gia_ManCoNum(p->pAig) == iCos ); } /**Function************************************************************* @@ -633,12 +635,10 @@ Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * pAig, int nFrames, int nPref // set the default parameters Gia_ManSetDefaultParamsSwi( pPars ); // override some of the defaults - pPars->nWords = 10; // set number machine words to simulate pPars->nIters = nFrames; // set number of total timeframes if ( Abc_FrameReadFlag("seqsimframes") ) pPars->nIters = atoi( Abc_FrameReadFlag("seqsimframes") ); pPars->nPref = nPref; // set number of first timeframes to skip - pPars->fVerbose = 0; // disable verbose output // decide what should be computed if ( fProbOne ) { @@ -666,7 +666,94 @@ Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * pAig, int nFrames, int nPref return vResult; } - //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Computes probability of switching (or of being 1).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Gia_ManEvaluateSwitching( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + float SwitchTotal = 0.0; + int i; + assert( p->pSwitching ); + ABC_FREE( p->pRefs ); + Gia_ManCreateRefs( p ); + Gia_ManForEachObj( p, pObj, i ) + SwitchTotal += (float)Gia_ObjRefs(p, pObj) * p->pSwitching[i] / 255; + return SwitchTotal; +} + +/**Function************************************************************* + + Synopsis [Computes probability of switching (or of being 1).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne ) +{ + Gia_Man_t * pDfs; + Gia_Obj_t * pObj, * pObjDfs; + Vec_Int_t * vSwitching; + float * pSwitching, Switch, SwitchTotal = 0.0, SwitchTotal2 = 0.0; + int i; + Gia_ParSwi_t Pars, * pPars = &Pars; + ABC_FREE( p->pSwitching ); + // set the default parameters + Gia_ManSetDefaultParamsSwi( pPars ); + // override some of the defaults + pPars->nIters = nFrames; // set number of total timeframes + pPars->nPref = nPref; // set number of first timeframes to skip + // decide what should be computed + if ( fProbOne ) + { + // if the user asked to compute propability of 1, we do not need transition information + pPars->fProbOne = 1; // enable computing probabiblity of being one + pPars->fProbTrans = 0; // disable computing transition probability + } + else + { + // if the user asked for transition propabability, we do not need to compute probability of 1 + pPars->fProbOne = 0; // disable computing probabiblity of being one + pPars->fProbTrans = 1; // enable computing transition probability + } + // derives the DFS ordered AIG + Gia_ManCreateRefs( p ); +// pDfs = Gia_ManDupOrderDfs( p ); + pDfs = Gia_ManDup( p ); + assert( Gia_ManObjNum(pDfs) == Gia_ManObjNum(p) ); + // perform the computation of switching activity + vSwitching = Gia_ManSwiSimulate( pDfs, pPars ); + // transfer the computed result to the original AIG + p->pSwitching = ABC_CALLOC( unsigned char, Gia_ManObjNum(p) ); + pSwitching = (float *)vSwitching->pArray; + Gia_ManForEachObj( p, pObj, i ) + { + pObjDfs = Gia_ObjFromLit( pDfs, pObj->Value ); + Switch = pSwitching[ Gia_ObjId(pDfs, pObjDfs) ]; + p->pSwitching[i] = (char)((Switch >= 1.0) ? 255 : (int)((0.002 + Switch) * 255)); // 0.00196 = (1/255)/2 + SwitchTotal += (float)Gia_ObjRefs(p, pObj) * p->pSwitching[i] / 255; +// SwitchTotal2 += Gia_ObjRefs(p, pObj) * Switch; +// printf( "%d = %.2f\n", i, Gia_ObjRefs(p, pObj) * Switch ); + } +// printf( "\nSwitch float = %f. Switch char = %f.\n", SwitchTotal2, SwitchTotal ); + Vec_IntFree( vSwitching ); + Gia_ManStop( pDfs ); + return SwitchTotal; +} + +//////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index d5ff628a..055d7580 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -2,6 +2,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaAig.c \ src/aig/gia/giaAiger.c \ src/aig/gia/giaCof.c \ + src/aig/gia/giaCSat.c \ src/aig/gia/giaDfs.c \ src/aig/gia/giaDup.c \ src/aig/gia/giaEmbed.c \ @@ -15,6 +16,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaHash.c \ src/aig/gia/giaMan.c \ src/aig/gia/giaMap.c \ + src/aig/gia/giaPat.c \ src/aig/gia/giaRetime.c \ src/aig/gia/giaScl.c \ src/aig/gia/giaSim.c \ -- cgit v1.2.3