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