diff options
Diffstat (limited to 'src/aig/gia/giaCTas2.c')
-rw-r--r-- | src/aig/gia/giaCTas2.c | 208 |
1 files changed, 208 insertions, 0 deletions
diff --git a/src/aig/gia/giaCTas2.c b/src/aig/gia/giaCTas2.c new file mode 100644 index 00000000..855dcdd3 --- /dev/null +++ b/src/aig/gia/giaCTas2.c @@ -0,0 +1,208 @@ +/**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 + int timeSatUnsat; // unsat + int timeSatSat; // sat + int timeSatUndec; // undecided + int 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 + |