diff options
Diffstat (limited to 'src/aig/gia/giaCSatB.c')
| -rw-r--r-- | src/aig/gia/giaCSatB.c | 490 |
1 files changed, 0 insertions, 490 deletions
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 /// -//////////////////////////////////////////////////////////////////////// - - |