diff options
Diffstat (limited to 'src/aig/gia/giaCSat1.c')
| -rw-r--r-- | src/aig/gia/giaCSat1.c | 602 |
1 files changed, 602 insertions, 0 deletions
diff --git a/src/aig/gia/giaCSat1.c b/src/aig/gia/giaCSat1.c new file mode 100644 index 00000000..12b7071f --- /dev/null +++ b/src/aig/gia/giaCSat1.c @@ -0,0 +1,602 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + + |