| /**CFile**************************************************************** |
| |
| FileName [giaCSat2.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: giaCSat2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "gia.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| typedef struct Tas_Par_t_ Tas_Par_t; |
| struct Tas_Par_t_ |
| { |
| // conflict limits |
| int nBTLimit; // limit on the number of conflicts |
| // current parameters |
| int nBTThis; // number of conflicts |
| int nBTTotal; // total number of conflicts |
| // decision heuristics |
| int fUseHighest; // use node with the highest ID |
| // other parameters |
| int fVerbose; |
| }; |
| |
| typedef struct Tas_Sto_t_ Tas_Sto_t; |
| struct Tas_Sto_t_ |
| { |
| int iCur; // currently used |
| int nSize; // allocated size |
| char * pBuffer; // handles of objects stored in the queue |
| }; |
| |
| typedef struct Tas_Que_t_ Tas_Que_t; |
| struct Tas_Que_t_ |
| { |
| int iHead; // beginning of the queue |
| int iTail; // end of the queue |
| int nSize; // allocated size |
| int * pData; // handles of objects stored in the queue |
| }; |
| |
| typedef struct Tas_Var_t_ Tas_Var_t; |
| struct Tas_Var_t_ |
| { |
| unsigned fTerm : 1; // terminal node |
| unsigned fVal : 1; // current value |
| unsigned fValOld : 1; // previous value |
| unsigned fAssign : 1; // assigned status |
| unsigned fJQueue : 1; // part of J-frontier |
| unsigned fCompl0 : 1; // complemented attribute |
| unsigned fCompl1 : 1; // complemented attribute |
| unsigned fMark0 : 1; // multi-purpose mark |
| unsigned fMark1 : 1; // multi-purpose mark |
| unsigned fPhase : 1; // polarity |
| unsigned Level : 22; // decision level |
| int Id; // unique ID of this variable |
| int IdAig; // original ID of this variable |
| int Reason0; // reason of this variable |
| int Reason1; // reason of this variable |
| int Diff0; // difference for the first fanin |
| int Diff1; // difference for the second fanin |
| int Watch0; // handle of first watch |
| int Watch1; // handle of second watch |
| }; |
| |
| typedef struct Tas_Cls_t_ Tas_Cls_t; |
| struct Tas_Cls_t_ |
| { |
| int Watch0; // next clause to watch |
| int Watch1; // next clause to watch |
| int pVars[0]; // variable handles |
| }; |
| |
| typedef struct Tas_Man_t_ Tas_Man_t; |
| struct Tas_Man_t_ |
| { |
| // user data |
| Gia_Man_t * pAig; // AIG manager |
| Tas_Par_t Pars; // parameters |
| // solver data |
| Tas_Sto_t * pVars; // variables |
| Tas_Sto_t * pClauses; // clauses |
| // state representation |
| Tas_Que_t pProp; // propagation queue |
| Tas_Que_t pJust; // justification queue |
| Vec_Int_t * vModel; // satisfying assignment |
| Vec_Ptr_t * vTemp; // temporary storage |
| // 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 |
| int nConfTotal; // total conflicts |
| // runtime stats |
| clock_t timeSatUnsat; // unsat |
| clock_t timeSatSat; // sat |
| clock_t timeSatUndec; // undecided |
| clock_t timeTotal; // total runtime |
| }; |
| |
| static inline int Tas_VarIsAssigned( Tas_Var_t * pVar ) { return pVar->fAssign; } |
| static inline void Tas_VarAssign( Tas_Var_t * pVar ) { assert(!pVar->fAssign); pVar->fAssign = 1; } |
| static inline void Tas_VarUnassign( Tas_Var_t * pVar ) { assert(pVar->fAssign); pVar->fAssign = 0; pVar->fVal = 0; } |
| static inline int Tas_VarValue( Tas_Var_t * pVar ) { assert(pVar->fAssign); return pVar->fVal; } |
| static inline void Tas_VarSetValue( Tas_Var_t * pVar, int v ) { assert(pVar->fAssign); pVar->fVal = v; } |
| static inline int Tas_VarIsJust( Tas_Var_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)); } |
| static inline int Tas_VarFanin0Value( Tas_Var_t * pVar ) { return !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); } |
| static inline int Tas_VarFanin1Value( Tas_Var_t * pVar ) { return !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); } |
| |
| static inline int Tas_VarDecLevel( Tas_Man_t * p, Tas_Var_t * pVar ) { assert( pVar->Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*pVar->Value); } |
| static inline Tas_Var_t * Tas_VarReason0( Tas_Man_t * p, Tas_Var_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+1); } |
| static inline Tas_Var_t * Tas_VarReason1( Tas_Man_t * p, Tas_Var_t * pVar ) { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+2); } |
| static inline int Tas_ClauseDecLevel( Tas_Man_t * p, int hClause ) { return Tas_VarDecLevel( p, p->pClauses.pData[hClause] ); } |
| |
| static inline Tas_Var_t * Tas_ManVar( Tas_Man_t * p, int h ) { return (Tas_Var_t *)(p->pVars->pBuffer + h); } |
| static inline Tas_Cls_t * Tas_ManClause( Tas_Man_t * p, int h ) { return (Tas_Cls_t *)(p->pClauses->pBuffer + h); } |
| |
| #define Tas_ClaForEachVar( p, pClause, pVar, i ) \ |
| for ( pVar = Tas_ManVar(p, pClause->pVars[(i=0)]); pClause->pVars[i]; pVar = (Tas_Var_t *)(((char *)pVar + pClause->pVars[++i])) ) |
| |
| #define Tas_QueForEachVar( p, pQue, pVar, i ) \ |
| for ( pVar = Tas_ManVar(p, pQue->pVars[(i=pQue->iHead)]); i < pQue->iTail; pVar = Tas_ManVar(p, pQue->pVars[i++]) ) |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Tas_Var_t * Tas_ManCreateVar( Tas_Man_t * p ) |
| { |
| Tas_Var_t * pVar; |
| if ( p->pVars->iCur + sizeof(Tas_Var_t) > p->pVars->nSize ) |
| { |
| p->pVars->nSize *= 2; |
| p->pVars->pData = ABC_REALLOC( char, p->pVars->pData, p->pVars->nSize ); |
| } |
| pVar = p->pVars->pData + p->pVars->iCur; |
| p->pVars->iCur += sizeof(Tas_Var_t); |
| memset( pVar, 0, sizeof(Tas_Var_t) ); |
| pVar->Id = pVar - ((Tas_Var_t *)p->pVars->pData); |
| return pVar; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Tas_Var_t * Tas_ManObj2Var( Tas_Man_t * p, Gia_Obj_t * pObj ) |
| { |
| Tas_Var_t * pVar; |
| assert( !Gia_ObjIsComplement(pObj) ); |
| if ( pObj->Value == 0 ) |
| { |
| pVar = Tas_ManCreateVar( p ); |
| pVar-> |
| |
| } |
| return Tas_ManVar( p, pObj->Value ); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
