| /**CFile**************************************************************** | |
| FileName [cecSat.c] | |
| SystemName [ABC: Logic synthesis and verification system.] | |
| PackageName [Combinational equivalence checking.] | |
| Synopsis [Detection of structural isomorphism.] | |
| Author [Alan Mishchenko] | |
| Affiliation [UC Berkeley] | |
| Date [Ver. 1.0. Started - June 20, 2005.] | |
| Revision [$Id: cecSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] | |
| ***********************************************************************/ | |
| #include "aig/gia/gia.h" | |
| #include "misc/util/utilTruth.h" | |
| #include "sat/satoko/satoko.h" | |
| #include "cec.h" | |
| ABC_NAMESPACE_IMPL_START | |
| //////////////////////////////////////////////////////////////////////// | |
| /// DECLARATIONS /// | |
| //////////////////////////////////////////////////////////////////////// | |
| // sweeping manager | |
| typedef struct Cec2_Par_t_ Cec2_Par_t; | |
| struct Cec2_Par_t_ | |
| { | |
| int nSimWords; // simulation words | |
| int nSimRounds; // simulation rounds | |
| int nItersMax; // max number of iterations | |
| int nConfLimit; // SAT solver conflict limit | |
| int fIsMiter; // this is a miter | |
| int fUseCones; // use logic cones | |
| int fVeryVerbose; // verbose stats | |
| int fVerbose; // verbose stats | |
| }; | |
| // SAT solving manager | |
| typedef struct Cec2_Man_t_ Cec2_Man_t; | |
| struct Cec2_Man_t_ | |
| { | |
| Cec2_Par_t * pPars; // parameters | |
| Gia_Man_t * pAig; // user's AIG | |
| Gia_Man_t * pNew; // internal AIG | |
| // SAT solving | |
| satoko_t * pSat; // SAT solver | |
| Vec_Ptr_t * vFrontier; // CNF construction | |
| Vec_Ptr_t * vFanins; // CNF construction | |
| Vec_Wrd_t * vSims; // CI simulation info | |
| Vec_Int_t * vNodesNew; // nodes | |
| Vec_Int_t * vSatVars; // nodes | |
| Vec_Int_t * vObjSatPairs; // nodes | |
| Vec_Int_t * vCexTriples; // nodes | |
| // statistics | |
| int nPatterns; | |
| int nSatSat; | |
| int nSatUnsat; | |
| int nSatUndec; | |
| abctime timeSatSat; | |
| abctime timeSatUnsat; | |
| abctime timeSatUndec; | |
| abctime timeSim; | |
| abctime timeRefine; | |
| abctime timeExtra; | |
| abctime timeStart; | |
| }; | |
| static inline int Cec2_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjCopy2Array(p, Gia_ObjId(p, pObj)); } | |
| static inline int Cec2_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec2_ObjSatId(p, pObj) == -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), Num); return Num; } | |
| static inline void Cec2_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec2_ObjSatId(p, pObj) != -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), -1); } | |
| //////////////////////////////////////////////////////////////////////// | |
| /// FUNCTION DEFINITIONS /// | |
| //////////////////////////////////////////////////////////////////////// | |
| /**Function************************************************************* | |
| Synopsis [Sets parameter defaults.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec2_SetDefaultParams( Cec2_Par_t * p ) | |
| { | |
| memset( p, 0, sizeof(Cec2_Par_t) ); | |
| p->nSimWords = 12; // simulation words | |
| p->nSimRounds = 4; // simulation rounds | |
| p->nItersMax = 10; // max number of iterations | |
| p->nConfLimit = 1000; // conflict limit at a node | |
| p->fIsMiter = 0; // this is a miter | |
| p->fUseCones = 1; // use logic cones | |
| p->fVeryVerbose = 0; // verbose stats | |
| p->fVerbose = 0; // verbose stats | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Adds clauses to the solver.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec2_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, satoko_t * pSat ) | |
| { | |
| int fPolarFlip = 0; | |
| Gia_Obj_t * pNodeI, * pNodeT, * pNodeE; | |
| int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; | |
| assert( !Gia_IsComplement( pNode ) ); | |
| assert( pNode->fMark0 ); | |
| // get nodes (I = if, T = then, E = else) | |
| pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); | |
| // get the variable numbers | |
| VarF = Cec2_ObjSatId(p, pNode); | |
| VarI = Cec2_ObjSatId(p, pNodeI); | |
| VarT = Cec2_ObjSatId(p, Gia_Regular(pNodeT)); | |
| VarE = Cec2_ObjSatId(p, Gia_Regular(pNodeE)); | |
| // get the complementation flags | |
| fCompT = Gia_IsComplement(pNodeT); | |
| fCompE = Gia_IsComplement(pNodeE); | |
| // f = ITE(i, t, e) | |
| // i' + t' + f | |
| // i' + t + f' | |
| // i + e' + f | |
| // i + e + f' | |
| // create four clauses | |
| pLits[0] = Abc_Var2Lit(VarI, 1); | |
| pLits[1] = Abc_Var2Lit(VarT, 1^fCompT); | |
| pLits[2] = Abc_Var2Lit(VarF, 0); | |
| if ( fPolarFlip ) | |
| { | |
| if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); | |
| if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); | |
| if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); | |
| } | |
| RetValue = satoko_add_clause( pSat, pLits, 3 ); | |
| assert( RetValue ); | |
| pLits[0] = Abc_Var2Lit(VarI, 1); | |
| pLits[1] = Abc_Var2Lit(VarT, 0^fCompT); | |
| pLits[2] = Abc_Var2Lit(VarF, 1); | |
| if ( fPolarFlip ) | |
| { | |
| if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); | |
| if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); | |
| if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); | |
| } | |
| RetValue = satoko_add_clause( pSat, pLits, 3 ); | |
| assert( RetValue ); | |
| pLits[0] = Abc_Var2Lit(VarI, 0); | |
| pLits[1] = Abc_Var2Lit(VarE, 1^fCompE); | |
| pLits[2] = Abc_Var2Lit(VarF, 0); | |
| if ( fPolarFlip ) | |
| { | |
| if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); | |
| if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); | |
| if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); | |
| } | |
| RetValue = satoko_add_clause( pSat, pLits, 3 ); | |
| assert( RetValue ); | |
| pLits[0] = Abc_Var2Lit(VarI, 0); | |
| pLits[1] = Abc_Var2Lit(VarE, 0^fCompE); | |
| pLits[2] = Abc_Var2Lit(VarF, 1); | |
| if ( fPolarFlip ) | |
| { | |
| if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); | |
| if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); | |
| if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); | |
| } | |
| RetValue = satoko_add_clause( pSat, pLits, 3 ); | |
| assert( RetValue ); | |
| // two additional clauses | |
| // t' & e' -> f' | |
| // t & e -> f | |
| // t + e + f' | |
| // t' + e' + f | |
| if ( VarT == VarE ) | |
| { | |
| // assert( fCompT == !fCompE ); | |
| return; | |
| } | |
| pLits[0] = Abc_Var2Lit(VarT, 0^fCompT); | |
| pLits[1] = Abc_Var2Lit(VarE, 0^fCompE); | |
| pLits[2] = Abc_Var2Lit(VarF, 1); | |
| if ( fPolarFlip ) | |
| { | |
| if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); | |
| if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); | |
| if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); | |
| } | |
| RetValue = satoko_add_clause( pSat, pLits, 3 ); | |
| assert( RetValue ); | |
| pLits[0] = Abc_Var2Lit(VarT, 1^fCompT); | |
| pLits[1] = Abc_Var2Lit(VarE, 1^fCompE); | |
| pLits[2] = Abc_Var2Lit(VarF, 0); | |
| if ( fPolarFlip ) | |
| { | |
| if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); | |
| if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); | |
| if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); | |
| } | |
| RetValue = satoko_add_clause( pSat, pLits, 3 ); | |
| assert( RetValue ); | |
| } | |
| void Cec2_AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, satoko_t * pSat ) | |
| { | |
| int fPolarFlip = 0; | |
| Gia_Obj_t * pFanin; | |
| int * pLits, nLits, RetValue, i; | |
| assert( !Gia_IsComplement(pNode) ); | |
| assert( Gia_ObjIsAnd( pNode ) ); | |
| // create storage for literals | |
| nLits = Vec_PtrSize(vSuper) + 1; | |
| pLits = ABC_ALLOC( int, nLits ); | |
| // suppose AND-gate is A & B = C | |
| // add !A => !C or A + !C | |
| Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i ) | |
| { | |
| pLits[0] = Abc_Var2Lit(Cec2_ObjSatId(p, Gia_Regular(pFanin)), Gia_IsComplement(pFanin)); | |
| pLits[1] = Abc_Var2Lit(Cec2_ObjSatId(p, pNode), 1); | |
| if ( fPolarFlip ) | |
| { | |
| if ( Gia_Regular(pFanin)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); | |
| if ( pNode->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); | |
| } | |
| RetValue = satoko_add_clause( pSat, pLits, 2 ); | |
| assert( RetValue ); | |
| } | |
| // add A & B => C or !A + !B + C | |
| Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i ) | |
| { | |
| pLits[i] = Abc_Var2Lit(Cec2_ObjSatId(p, Gia_Regular(pFanin)), !Gia_IsComplement(pFanin)); | |
| if ( fPolarFlip ) | |
| { | |
| if ( Gia_Regular(pFanin)->fPhase ) pLits[i] = Abc_LitNot( pLits[i] ); | |
| } | |
| } | |
| pLits[nLits-1] = Abc_Var2Lit(Cec2_ObjSatId(p, pNode), 0); | |
| if ( fPolarFlip ) | |
| { | |
| if ( pNode->fPhase ) pLits[nLits-1] = Abc_LitNot( pLits[nLits-1] ); | |
| } | |
| RetValue = satoko_add_clause( pSat, pLits, nLits ); | |
| assert( RetValue ); | |
| ABC_FREE( pLits ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Adds clauses and returns CNF variable of the node.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec2_CollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) | |
| { | |
| //printf( "v%d ", Gia_ObjValue(pObj) ); | |
| // if the new node is complemented or a PI, another gate begins | |
| if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) || | |
| // (!fFirst && Gia_ObjValue(pObj) > 1) || | |
| (!fFirst && (p->pRefs ? Gia_ObjRefNum(p, pObj) : Gia_ObjValue(pObj)) > 1) || | |
| (fUseMuxes && pObj->fMark0) ) | |
| { | |
| Vec_PtrPushUnique( vSuper, pObj ); | |
| return; | |
| } | |
| // go through the branches | |
| Cec2_CollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes ); | |
| Cec2_CollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes ); | |
| } | |
| void Cec2_CollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) | |
| { | |
| assert( !Gia_IsComplement(pObj) ); | |
| assert( !Gia_ObjIsCi(pObj) ); | |
| Vec_PtrClear( vSuper ); | |
| Cec2_CollectSuper_rec( p, pObj, vSuper, 1, fUseMuxes ); | |
| } | |
| void Cec2_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * pSat ) | |
| { | |
| int iVar; | |
| assert( !Gia_IsComplement(pObj) ); | |
| assert( !Gia_ObjIsConst0(pObj) ); | |
| if ( Cec2_ObjSatId(p, pObj) >= 0 ) | |
| return; | |
| assert( Cec2_ObjSatId(p, pObj) == -1 ); | |
| iVar = satoko_add_variable(pSat, 0); | |
| if ( p->vVar2Obj ) | |
| { | |
| assert( Vec_IntSize(p->vVar2Obj) == iVar ); | |
| Vec_IntPush( p->vVar2Obj, Gia_ObjId(p, pObj) ); | |
| } | |
| Cec2_ObjSetSatId( p, pObj, iVar ); | |
| if ( Gia_ObjIsAnd(pObj) ) | |
| Vec_PtrPush( vFrontier, pObj ); | |
| } | |
| int Gia_ObjGetCnfVar( Gia_Man_t * pGia, int iObj, Vec_Ptr_t * vFrontier, Vec_Ptr_t * vFanins, satoko_t * pSat ) | |
| { | |
| Gia_Obj_t * pNode, * pFanin; | |
| Gia_Obj_t * pObj = Gia_ManObj(pGia, iObj); | |
| int i, k, fUseMuxes = 1; | |
| if ( Vec_IntSize(&pGia->vCopies2) < Gia_ManObjNum(pGia) ) | |
| Vec_IntFillExtra( &pGia->vCopies2, Gia_ManObjNum(pGia), -1 ); | |
| // quit if CNF is ready | |
| if ( Cec2_ObjSatId(pGia,pObj) >= 0 ) | |
| return Cec2_ObjSatId(pGia,pObj); | |
| assert( iObj > 0 ); | |
| if ( Gia_ObjIsCi(pObj) ) | |
| { | |
| int iVar = satoko_add_variable(pSat, 0); | |
| if ( pGia->vVar2Obj ) | |
| { | |
| assert( Vec_IntSize(pGia->vVar2Obj) == iVar ); | |
| Vec_IntPush( pGia->vVar2Obj, iObj ); | |
| } | |
| return Cec2_ObjSetSatId( pGia, pObj, iVar ); | |
| } | |
| assert( Gia_ObjIsAnd(pObj) ); | |
| // start the frontier | |
| Vec_PtrClear( vFrontier ); | |
| Cec2_ObjAddToFrontier( pGia, pObj, vFrontier, pSat ); | |
| // explore nodes in the frontier | |
| Vec_PtrForEachEntry( Gia_Obj_t *, vFrontier, pNode, i ) | |
| { | |
| // create the supergate | |
| assert( Cec2_ObjSatId(pGia,pNode) >= 0 ); | |
| if ( fUseMuxes && pNode->fMark0 ) | |
| { | |
| Vec_PtrClear( vFanins ); | |
| Vec_PtrPushUnique( vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) ); | |
| Vec_PtrPushUnique( vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) ); | |
| Vec_PtrPushUnique( vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) ); | |
| Vec_PtrPushUnique( vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) ); | |
| Vec_PtrForEachEntry( Gia_Obj_t *, vFanins, pFanin, k ) | |
| Cec2_ObjAddToFrontier( pGia, Gia_Regular(pFanin), vFrontier, pSat ); | |
| Cec2_AddClausesMux( pGia, pNode, pSat ); | |
| } | |
| else | |
| { | |
| Cec2_CollectSuper( pGia, pNode, fUseMuxes, vFanins ); | |
| Vec_PtrForEachEntry( Gia_Obj_t *, vFanins, pFanin, k ) | |
| Cec2_ObjAddToFrontier( pGia, Gia_Regular(pFanin), vFrontier, pSat ); | |
| Cec2_AddClausesSuper( pGia, pNode, vFanins, pSat ); | |
| //printf( "%d ", Vec_PtrSize(vFanins) ); | |
| } | |
| assert( Vec_PtrSize(vFanins) > 1 ); | |
| } | |
| return Cec2_ObjSatId(pGia,pObj); | |
| } | |
| int Cec2_ObjGetCnfVar( Cec2_Man_t * p, int iObj ) | |
| { | |
| return Gia_ObjGetCnfVar( p->pNew, iObj, p->vFrontier, p->vFanins, p->pSat ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Internal simulation APIs.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| static inline word * Cec2_ObjSim( Gia_Man_t * p, int iObj ) | |
| { | |
| return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj ); | |
| } | |
| static inline void Cec2_ObjSimSetInputBit( Gia_Man_t * p, int iObj, int Bit ) | |
| { | |
| word * pSim = Cec2_ObjSim( p, iObj ); | |
| if ( Abc_InfoHasBit( (unsigned*)pSim, p->iPatsPi ) != Bit ) | |
| Abc_InfoXorBit( (unsigned*)pSim, p->iPatsPi ); | |
| } | |
| static inline void Cec2_ObjSimRo( Gia_Man_t * p, int iObj ) | |
| { | |
| int w; | |
| word * pSimRo = Cec2_ObjSim( p, iObj ); | |
| word * pSimRi = Cec2_ObjSim( p, Gia_ObjRoToRiId(p, iObj) ); | |
| for ( w = 0; w < p->nSimWords; w++ ) | |
| pSimRo[w] = pSimRi[w]; | |
| } | |
| static inline void Cec2_ObjSimCo( Gia_Man_t * p, int iObj ) | |
| { | |
| int w; | |
| Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); | |
| word * pSimCo = Cec2_ObjSim( p, iObj ); | |
| word * pSimDri = Cec2_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) ); | |
| if ( Gia_ObjFaninC0(pObj) ) | |
| for ( w = 0; w < p->nSimWords; w++ ) | |
| pSimCo[w] = ~pSimDri[w]; | |
| else | |
| for ( w = 0; w < p->nSimWords; w++ ) | |
| pSimCo[w] = pSimDri[w]; | |
| } | |
| static inline void Cec2_ObjSimAnd( Gia_Man_t * p, int iObj ) | |
| { | |
| int w; | |
| Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); | |
| word * pSim = Cec2_ObjSim( p, iObj ); | |
| word * pSim0 = Cec2_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) ); | |
| word * pSim1 = Cec2_ObjSim( p, Gia_ObjFaninId1(pObj, iObj) ); | |
| if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) | |
| for ( w = 0; w < p->nSimWords; w++ ) | |
| pSim[w] = ~pSim0[w] & ~pSim1[w]; | |
| else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) ) | |
| for ( w = 0; w < p->nSimWords; w++ ) | |
| pSim[w] = ~pSim0[w] & pSim1[w]; | |
| else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) | |
| for ( w = 0; w < p->nSimWords; w++ ) | |
| pSim[w] = pSim0[w] & ~pSim1[w]; | |
| else | |
| for ( w = 0; w < p->nSimWords; w++ ) | |
| pSim[w] = pSim0[w] & pSim1[w]; | |
| } | |
| static inline int Cec2_ObjSimEqual( Gia_Man_t * p, int iObj0, int iObj1 ) | |
| { | |
| int w; | |
| word * pSim0 = Cec2_ObjSim( p, iObj0 ); | |
| word * pSim1 = Cec2_ObjSim( p, iObj1 ); | |
| if ( (pSim0[0] & 1) == (pSim1[0] & 1) ) | |
| { | |
| for ( w = 0; w < p->nSimWords; w++ ) | |
| if ( pSim0[w] != pSim1[w] ) | |
| return 0; | |
| return 1; | |
| } | |
| else | |
| { | |
| for ( w = 0; w < p->nSimWords; w++ ) | |
| if ( pSim0[w] != ~pSim1[w] ) | |
| return 0; | |
| return 1; | |
| } | |
| } | |
| static inline void Cec2_ObjSimCi( Gia_Man_t * p, int iObj ) | |
| { | |
| int w; | |
| word * pSim = Cec2_ObjSim( p, iObj ); | |
| for ( w = 0; w < p->nSimWords; w++ ) | |
| pSim[w] = Gia_ManRandomW( 0 ); | |
| pSim[0] <<= 1; | |
| } | |
| void Cec2_ManSimulateCis( Gia_Man_t * p ) | |
| { | |
| int i, Id; | |
| Gia_ManForEachCiId( p, Id, i ) | |
| Cec2_ObjSimCi( p, Id ); | |
| p->iPatsPi = 0; | |
| } | |
| Abc_Cex_t * Cec2_ManDeriveCex( Gia_Man_t * p, int iOut, int iPat ) | |
| { | |
| Abc_Cex_t * pCex; | |
| int i, Id; | |
| pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p), 1 ); | |
| pCex->iPo = iOut; | |
| if ( iPat == -1 ) | |
| return pCex; | |
| Gia_ManForEachCiId( p, Id, i ) | |
| if ( Abc_InfoHasBit((unsigned *)Cec2_ObjSim(p, Id), iPat) ) | |
| Abc_InfoSetBit( pCex->pData, i ); | |
| return pCex; | |
| } | |
| int Cec2_ManSimulateCos( Gia_Man_t * p ) | |
| { | |
| int i, Id; | |
| // check outputs and generate CEX if they fail | |
| Gia_ManForEachCoId( p, Id, i ) | |
| { | |
| Cec2_ObjSimCo( p, Id ); | |
| if ( Cec2_ObjSimEqual(p, Id, 0) ) | |
| continue; | |
| p->pCexSeq = Cec2_ManDeriveCex( p, i, Abc_TtFindFirstBit2(Cec2_ObjSim(p, Id), p->nSimWords) ); | |
| return 0; | |
| } | |
| return 1; | |
| } | |
| void Cec2_ManSaveCis( Gia_Man_t * p ) | |
| { | |
| int w, i, Id; | |
| assert( p->vSimsPi != NULL ); | |
| for ( w = 0; w < p->nSimWords; w++ ) | |
| Gia_ManForEachCiId( p, Id, i ) | |
| Vec_WrdPush( p->vSimsPi, Cec2_ObjSim(p, Id)[w] ); | |
| } | |
| int Cec2_ManSimulate( Gia_Man_t * p, Vec_Int_t * vTriples, Cec2_Man_t * pMan ) | |
| { | |
| extern void Cec2_ManSimClassRefineOne( Gia_Man_t * p, int iRepr ); | |
| abctime clk = Abc_Clock(); | |
| Gia_Obj_t * pObj; | |
| int i, iRepr, iObj, Entry, Count = 0; | |
| //Cec2_ManSaveCis( p ); | |
| Gia_ManForEachAnd( p, pObj, i ) | |
| Cec2_ObjSimAnd( p, i ); | |
| pMan->timeSim += Abc_Clock() - clk; | |
| if ( p->pReprs == NULL ) | |
| return 0; | |
| if ( vTriples ) | |
| { | |
| Vec_IntForEachEntryTriple( vTriples, iRepr, iObj, Entry, i ) | |
| { | |
| word * pSim0 = Cec2_ObjSim( p, iRepr ); | |
| word * pSim1 = Cec2_ObjSim( p, iObj ); | |
| int iPat = Abc_Lit2Var(Entry); | |
| int fPhase = Abc_LitIsCompl(Entry); | |
| if ( (fPhase ^ Abc_InfoHasBit((unsigned *)pSim0, iPat)) == Abc_InfoHasBit((unsigned *)pSim1, iPat) ) | |
| { | |
| //printf( "ERROR: Pattern %d did not disprove pair %d and %d.\n", iPat, iRepr, iObj ); | |
| Count++; | |
| } | |
| } | |
| } | |
| clk = Abc_Clock(); | |
| Gia_ManForEachClass0( p, i ) | |
| Cec2_ManSimClassRefineOne( p, i ); | |
| pMan->timeRefine += Abc_Clock() - clk; | |
| return Count; | |
| } | |
| void Cec2_ManSimAlloc( Gia_Man_t * p, int nWords ) | |
| { | |
| Vec_WrdFreeP( &p->vSims ); | |
| Vec_WrdFreeP( &p->vSimsPi ); | |
| p->vSims = Vec_WrdStart( Gia_ManObjNum(p) * nWords ); | |
| p->vSimsPi = Vec_WrdAlloc( Gia_ManCiNum(p) * nWords * 4 ); // storage for CI patterns | |
| p->nSimWords = nWords; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Computes hash key of the simulation info.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec2_ManSimHashKey( word * pSim, int nSims, int nTableSize ) | |
| { | |
| static int s_Primes[16] = { | |
| 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, | |
| 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 }; | |
| unsigned uHash = 0, * pSimU = (unsigned *)pSim; | |
| int i, nSimsU = 2 * nSims; | |
| if ( pSimU[0] & 1 ) | |
| for ( i = 0; i < nSimsU; i++ ) | |
| uHash ^= ~pSimU[i] * s_Primes[i & 0xf]; | |
| else | |
| for ( i = 0; i < nSimsU; i++ ) | |
| uHash ^= pSimU[i] * s_Primes[i & 0xf]; | |
| return (int)(uHash % nTableSize); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Creating initial equivalence classes.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec2_ManSimClassRefineOne( Gia_Man_t * p, int iRepr ) | |
| { | |
| int iObj, iPrev = iRepr, iPrev2, iRepr2; | |
| Gia_ClassForEachObj1( p, iRepr, iRepr2 ) | |
| if ( Cec2_ObjSimEqual(p, iRepr, iRepr2) ) | |
| iPrev = iRepr2; | |
| else | |
| break; | |
| if ( iRepr2 <= 0 ) // no refinement | |
| return; | |
| // relink remaining nodes of the class | |
| // nodes that are equal to iRepr, remain in the class of iRepr | |
| // nodes that are not equal to iRepr, move to the class of iRepr2 | |
| Gia_ObjSetRepr( p, iRepr2, GIA_VOID ); | |
| iPrev2 = iRepr2; | |
| for ( iObj = Gia_ObjNext(p, iRepr2); iObj > 0; iObj = Gia_ObjNext(p, iObj) ) | |
| { | |
| if ( Cec2_ObjSimEqual(p, iRepr, iObj) ) // remains with iRepr | |
| { | |
| Gia_ObjSetNext( p, iPrev, iObj ); | |
| iPrev = iObj; | |
| } | |
| else // moves to iRepr2 | |
| { | |
| Gia_ObjSetRepr( p, iObj, iRepr2 ); | |
| Gia_ObjSetNext( p, iPrev2, iObj ); | |
| iPrev2 = iObj; | |
| } | |
| } | |
| Gia_ObjSetNext( p, iPrev, -1 ); | |
| Gia_ObjSetNext( p, iPrev2, -1 ); | |
| } | |
| void Cec2_ManCreateClasses( Gia_Man_t * p, Cec2_Man_t * pMan ) | |
| { | |
| abctime clk; | |
| Gia_Obj_t * pObj; | |
| int nWords = p->nSimWords; | |
| int * pTable, nTableSize, i, Key; | |
| // allocate representation | |
| ABC_FREE( p->pReprs ); | |
| ABC_FREE( p->pNexts ); | |
| p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); | |
| p->pNexts = ABC_FALLOC( int, Gia_ManObjNum(p) ); | |
| // hash each node by its simulation info | |
| nTableSize = Abc_PrimeCudd( Gia_ManObjNum(p) ); | |
| pTable = ABC_FALLOC( int, nTableSize ); | |
| Gia_ManForEachObj( p, pObj, i ) | |
| { | |
| p->pReprs[i].iRepr = GIA_VOID; | |
| if ( Gia_ObjIsCo(pObj) ) | |
| continue; | |
| Key = Cec2_ManSimHashKey( Cec2_ObjSim(p, i), nWords, nTableSize ); | |
| assert( Key >= 0 && Key < nTableSize ); | |
| if ( pTable[Key] == -1 ) | |
| pTable[Key] = i; | |
| else | |
| Gia_ObjSetRepr( p, i, pTable[Key] ); | |
| } | |
| // create classes | |
| for ( i = Gia_ManObjNum(p) - 1; i >= 0; i-- ) | |
| { | |
| int iRepr = Gia_ObjRepr(p, i); | |
| if ( iRepr == GIA_VOID ) | |
| continue; | |
| Gia_ObjSetNext( p, i, Gia_ObjNext(p, iRepr) ); | |
| Gia_ObjSetNext( p, iRepr, i ); | |
| } | |
| ABC_FREE( pTable ); | |
| clk = Abc_Clock(); | |
| Gia_ManForEachClass0( p, i ) | |
| Cec2_ManSimClassRefineOne( p, i ); | |
| pMan->timeRefine += Abc_Clock() - clk; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars ) | |
| { | |
| Cec2_Man_t * p; | |
| Gia_Obj_t * pObj; int i; | |
| satoko_opts_t Pars; | |
| //assert( Gia_ManRegNum(pAig) == 0 ); | |
| p = ABC_CALLOC( Cec2_Man_t, 1 ); | |
| memset( p, 0, sizeof(Cec2_Man_t) ); | |
| p->timeStart = Abc_Clock(); | |
| p->pPars = pPars; | |
| p->pAig = pAig; | |
| // create new manager | |
| p->pNew = Gia_ManStart( Gia_ManObjNum(pAig) ); | |
| Gia_ManFillValue( pAig ); | |
| Gia_ManConst0(pAig)->Value = 0; | |
| Gia_ManForEachCi( pAig, pObj, i ) | |
| pObj->Value = Gia_ManAppendCi( p->pNew ); | |
| Gia_ManHashAlloc( p->pNew ); | |
| Vec_IntFill( &p->pNew->vCopies2, Gia_ManObjNum(p->pNew), -1 ); | |
| // SAT solving | |
| memset( &Pars, 0, sizeof(satoko_opts_t) ); | |
| p->pSat = satoko_create(); | |
| p->vFrontier = Vec_PtrAlloc( 1000 ); | |
| p->vFanins = Vec_PtrAlloc( 100 ); | |
| p->vNodesNew = Vec_IntAlloc( 100 ); | |
| p->vSatVars = Vec_IntAlloc( 100 ); | |
| p->vObjSatPairs = Vec_IntAlloc( 100 ); | |
| p->vCexTriples = Vec_IntAlloc( 100 ); | |
| Pars.conf_limit = pPars->nConfLimit; | |
| satoko_configure(p->pSat, &Pars); | |
| // remember pointer to the solver in the AIG manager | |
| pAig->pData = p->pSat; | |
| return p; | |
| } | |
| void Cec2_ManDestroy( Cec2_Man_t * p ) | |
| { | |
| if ( p->pPars->fVerbose ) | |
| { | |
| abctime timeTotal = Abc_Clock() - p->timeStart; | |
| abctime timeSat = p->timeSatSat + p->timeSatUnsat + p->timeSatUndec; | |
| abctime timeOther = timeTotal - timeSat - p->timeSim - p->timeRefine - p->timeExtra; | |
| // Abc_Print( 1, "%d\n", p->Num ); | |
| ABC_PRTP( "SAT solving", timeSat, timeTotal ); | |
| ABC_PRTP( " sat ", p->timeSatSat, timeTotal ); | |
| ABC_PRTP( " unsat ", p->timeSatUnsat, timeTotal ); | |
| ABC_PRTP( " fail ", p->timeSatUndec, timeTotal ); | |
| ABC_PRTP( "Simulation ", p->timeSim, timeTotal ); | |
| ABC_PRTP( "Refinement ", p->timeRefine, timeTotal ); | |
| ABC_PRTP( "Rollback ", p->timeExtra, timeTotal ); | |
| ABC_PRTP( "Other ", timeOther, timeTotal ); | |
| ABC_PRTP( "TOTAL ", timeTotal, timeTotal ); | |
| fflush( stdout ); | |
| } | |
| Vec_WrdFreeP( &p->pAig->vSims ); | |
| //Vec_WrdFreeP( &p->pAig->vSimsPi ); | |
| Gia_ManCleanMark01( p->pAig ); | |
| satoko_destroy( p->pSat ); | |
| Gia_ManStopP( &p->pNew ); | |
| Vec_PtrFreeP( &p->vFrontier ); | |
| Vec_PtrFreeP( &p->vFanins ); | |
| Vec_IntFreeP( &p->vNodesNew ); | |
| Vec_IntFreeP( &p->vSatVars ); | |
| Vec_IntFreeP( &p->vObjSatPairs ); | |
| Vec_IntFreeP( &p->vCexTriples ); | |
| ABC_FREE( p ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Verify counter-example.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec2_ManVerify_rec( Gia_Man_t * p, int iObj, satoko_t * pSat ) | |
| { | |
| int Value0, Value1; | |
| Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); | |
| if ( iObj == 0 ) return 0; | |
| if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) | |
| return pObj->fMark1; | |
| Gia_ObjSetTravIdCurrentId(p, iObj); | |
| if ( Gia_ObjIsCi(pObj) ) | |
| return pObj->fMark1 = satoko_var_polarity(pSat, Cec2_ObjSatId(p, pObj)) == SATOKO_LIT_TRUE; | |
| assert( Gia_ObjIsAnd(pObj) ); | |
| Value0 = Cec2_ManVerify_rec( p, Gia_ObjFaninId0(pObj, iObj), pSat ) ^ Gia_ObjFaninC0(pObj); | |
| Value1 = Cec2_ManVerify_rec( p, Gia_ObjFaninId1(pObj, iObj), pSat ) ^ Gia_ObjFaninC1(pObj); | |
| return pObj->fMark1 = Value0 & Value1; | |
| } | |
| void Cec2_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, satoko_t * pSat ) | |
| { | |
| // int val0 = satoko_var_polarity(pSat, Cec2_ObjSatId(p, Gia_ManObj(p, iObj0))) == SATOKO_LIT_TRUE; | |
| // int val1 = satoko_var_polarity(pSat, Cec2_ObjSatId(p, Gia_ManObj(p, iObj1))) == SATOKO_LIT_TRUE; | |
| int Value0, Value1; | |
| Gia_ManIncrementTravId( p ); | |
| Value0 = Cec2_ManVerify_rec( p, iObj0, pSat ); | |
| Value1 = Cec2_ManVerify_rec( p, iObj1, pSat ); | |
| if ( (Value0 ^ Value1) == fPhase ) | |
| printf( "CEX verification FAILED for obj %d and obj %d.\n", iObj0, iObj1 ); | |
| // else | |
| // printf( "CEX verification succeeded for obj %d and obj %d.\n", iObj0, iObj1 );; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Internal simulation APIs.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec2_ManCollect_rec( Cec2_Man_t * p, int iObj ) | |
| { | |
| Gia_Obj_t * pObj; | |
| if ( Gia_ObjIsTravIdCurrentId(p->pNew, iObj) ) | |
| return; | |
| Gia_ObjSetTravIdCurrentId(p->pNew, iObj); | |
| pObj = Gia_ManObj( p->pNew, iObj ); | |
| if ( Cec2_ObjSatId(p->pNew, pObj) >= 0 ) | |
| { | |
| Vec_IntPush( p->vNodesNew, iObj ); | |
| Vec_IntPush( p->vSatVars, Cec2_ObjSatId(p->pNew, pObj) ); | |
| } | |
| if ( !iObj ) | |
| return; | |
| if ( Gia_ObjIsAnd(pObj) ) | |
| { | |
| Cec2_ManCollect_rec( p, Gia_ObjFaninId0(pObj, iObj) ); | |
| Cec2_ManCollect_rec( p, Gia_ObjFaninId1(pObj, iObj) ); | |
| } | |
| else | |
| { | |
| assert( Cec2_ObjSatId(p->pNew, pObj) >= 0 ); | |
| Vec_IntPushTwo( p->vObjSatPairs, Gia_ManCiIdToId(p->pAig, Gia_ObjCioId(pObj)), Cec2_ObjSatId(p->pNew, pObj) ); // SAT var | |
| } | |
| } | |
| int Cec2_ManSolveTwo( Cec2_Man_t * p, int iObj0, int iObj1, int fPhase ) | |
| { | |
| Gia_Obj_t * pObj; | |
| int status, i, iVar0, iVar1; | |
| if (iObj1 < iObj0) | |
| iObj1 ^= iObj0, iObj0 ^= iObj1, iObj1 ^= iObj0; | |
| assert( iObj0 < iObj1 ); | |
| assert( p->pPars->fUseCones || satoko_varnum(p->pSat) == 0 ); | |
| if ( !iObj0 && Cec2_ObjSatId(p->pNew, Gia_ManConst0(p->pNew)) == -1 ) | |
| Cec2_ObjSetSatId( p->pNew, Gia_ManConst0(p->pNew), satoko_add_variable(p->pSat, 0) ); | |
| iVar0 = Cec2_ObjGetCnfVar( p, iObj0 ); | |
| iVar1 = Cec2_ObjGetCnfVar( p, iObj1 ); | |
| // collect inputs and internal nodes | |
| Vec_IntClear( p->vNodesNew ); | |
| Vec_IntClear( p->vSatVars ); | |
| Vec_IntClear( p->vObjSatPairs ); | |
| Gia_ManIncrementTravId( p->pNew ); | |
| Cec2_ManCollect_rec( p, iObj0 ); | |
| Cec2_ManCollect_rec( p, iObj1 ); | |
| //printf( "%d ", Vec_IntSize(p->vNodesNew) ); | |
| // solve direct | |
| if ( p->pPars->fUseCones ) satoko_mark_cone( p->pSat, Vec_IntArray(p->vSatVars), Vec_IntSize(p->vSatVars) ); | |
| satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, 1) ); | |
| satoko_assump_push( p->pSat, Abc_Var2Lit(iVar1, fPhase) ); | |
| status = satoko_solve( p->pSat ); | |
| satoko_assump_pop( p->pSat ); | |
| satoko_assump_pop( p->pSat ); | |
| if ( status == SATOKO_UNSAT && iObj0 > 0 ) | |
| { | |
| // solve reverse | |
| satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, 0) ); | |
| satoko_assump_push( p->pSat, Abc_Var2Lit(iVar1, !fPhase) ); | |
| status = satoko_solve( p->pSat ); | |
| satoko_assump_pop( p->pSat ); | |
| satoko_assump_pop( p->pSat ); | |
| } | |
| if ( p->pPars->fUseCones ) satoko_unmark_cone( p->pSat, Vec_IntArray(p->vSatVars), Vec_IntSize(p->vSatVars) ); | |
| //if ( status == SATOKO_SAT ) | |
| // Cec2_ManVerify( p->pNew, iObj0, iObj1, fPhase, p->pSat ); | |
| if ( p->pPars->fUseCones ) | |
| return status; | |
| Gia_ManForEachObjVec( p->vNodesNew, p->pNew, pObj, i ) | |
| Cec2_ObjCleanSatId( p->pNew, pObj ); | |
| return status; | |
| } | |
| int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj ) | |
| { | |
| abctime clk = Abc_Clock(); | |
| int i, IdAig, IdSat, status, RetValue = 1; | |
| Gia_Obj_t * pObj = Gia_ManObj( p->pAig, iObj ); | |
| Gia_Obj_t * pRepr = Gia_ObjReprObj( p->pAig, iObj ); | |
| int fCompl = Abc_LitIsCompl(pObj->Value) ^ Abc_LitIsCompl(pRepr->Value) ^ pObj->fPhase ^ pRepr->fPhase; | |
| status = Cec2_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl ); | |
| if ( status == SATOKO_SAT ) | |
| { | |
| p->nSatSat++; | |
| p->nPatterns++; | |
| p->pAig->iPatsPi = (p->pAig->iPatsPi == 64 * p->pAig->nSimWords - 1) ? 1 : p->pAig->iPatsPi + 1; | |
| assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords ); | |
| Vec_IntForEachEntryDouble( p->vObjSatPairs, IdAig, IdSat, i ) | |
| Cec2_ObjSimSetInputBit( p->pAig, IdAig, satoko_var_polarity(p->pSat, IdSat) == SATOKO_LIT_TRUE ); | |
| p->timeSatSat += Abc_Clock() - clk; | |
| RetValue = 0; | |
| } | |
| else if ( status == SATOKO_UNSAT ) | |
| { | |
| p->nSatUnsat++; | |
| pObj->Value = Abc_LitNotCond( pRepr->Value, fCompl ); | |
| Gia_ObjSetProved( p->pAig, iObj ); | |
| p->timeSatUnsat += Abc_Clock() - clk; | |
| RetValue = 1; | |
| } | |
| else | |
| { | |
| p->nSatUndec++; | |
| assert( status == SATOKO_UNDEC ); | |
| Gia_ObjSetFailed( p->pAig, iObj ); | |
| p->timeSatUndec += Abc_Clock() - clk; | |
| RetValue = 2; | |
| } | |
| if ( p->pPars->fUseCones ) | |
| return RetValue; | |
| clk = Abc_Clock(); | |
| satoko_rollback( p->pSat ); | |
| p->timeExtra += Abc_Clock() - clk; | |
| satoko_stats(p->pSat)->n_conflicts = 0; | |
| return RetValue; | |
| } | |
| void Cec2_ManPrintStats( Gia_Man_t * p, Cec2_Par_t * pPars, Cec2_Man_t * pMan ) | |
| { | |
| if ( !pPars->fVerbose ) | |
| return; | |
| printf( "S =%5d ", pMan ? pMan->nSatSat : 0 ); | |
| printf( "U =%5d ", pMan ? pMan->nSatUnsat : 0 ); | |
| printf( "F =%5d ", pMan ? pMan->nSatUndec : 0 ); | |
| Gia_ManEquivPrintClasses( p, pPars->fVeryVerbose, 0 ); | |
| } | |
| int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppNew ) | |
| { | |
| Cec2_Man_t * pMan = Cec2_ManCreate( p, pPars ); | |
| Gia_Obj_t * pObj, * pRepr, * pObjNew; | |
| int i, Iter, fDisproved = 1; | |
| // check if any output trivially fails under all-0 pattern | |
| Gia_ManRandomW( 1 ); | |
| Gia_ManSetPhase( p ); | |
| if ( pPars->fIsMiter ) | |
| { | |
| Gia_ManForEachCo( p, pObj, i ) | |
| if ( pObj->fPhase ) | |
| { | |
| p->pCexSeq = Cec2_ManDeriveCex( p, i, -1 ); | |
| goto finalize; | |
| } | |
| } | |
| // simulate one round and create classes | |
| Cec2_ManSimAlloc( p, pPars->nSimWords ); | |
| Cec2_ManSimulateCis( p ); | |
| Cec2_ManSimulate( p, NULL, pMan ); | |
| if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected | |
| goto finalize; | |
| Cec2_ManCreateClasses( p, pMan ); | |
| Cec2_ManPrintStats( p, pPars, pMan ); | |
| // perform additinal simulation | |
| for ( i = 0; i < pPars->nSimRounds; i++ ) | |
| { | |
| Cec2_ManSimulateCis( p ); | |
| Cec2_ManSimulate( p, NULL, pMan ); | |
| if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected | |
| goto finalize; | |
| Cec2_ManPrintStats( p, pPars, pMan ); | |
| } | |
| // perform sweeping | |
| //pMan = Cec2_ManCreate( p, pPars ); | |
| for ( Iter = 0; fDisproved && Iter < pPars->nItersMax; Iter++ ) | |
| { | |
| fDisproved = 0; | |
| pMan->nPatterns = 0; | |
| Cec2_ManSimulateCis( p ); | |
| Vec_IntClear( pMan->vCexTriples ); | |
| Gia_ManForEachAnd( p, pObj, i ) | |
| { | |
| if ( ~pObj->Value || Gia_ObjFailed(p, i) ) // skip swept nodes and failed nodes | |
| continue; | |
| if ( !~Gia_ObjFanin0(pObj)->Value || !~Gia_ObjFanin1(pObj)->Value ) // skip fanouts of non-swept nodes | |
| continue; | |
| assert( !Gia_ObjProved(p, i) && !Gia_ObjFailed(p, i) ); | |
| // duplicate the node | |
| pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); | |
| if ( Vec_IntSize(&pMan->pNew->vCopies2) == Abc_Lit2Var(pObj->Value) ) | |
| { | |
| pObjNew = Gia_ManObj( pMan->pNew, Abc_Lit2Var(pObj->Value) ); | |
| pObjNew->fMark0 = Gia_ObjIsMuxType( pObjNew ); | |
| Gia_ObjSetPhase( pMan->pNew, pObjNew ); | |
| Vec_IntPush( &pMan->pNew->vCopies2, -1 ); | |
| } | |
| assert( Vec_IntSize(&pMan->pNew->vCopies2) == Gia_ManObjNum(pMan->pNew) ); | |
| pRepr = Gia_ObjReprObj( p, i ); | |
| if ( pRepr == NULL || !~pRepr->Value ) | |
| continue; | |
| if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) ) | |
| { | |
| assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) ); | |
| Gia_ObjSetProved( p, i ); | |
| continue; | |
| } | |
| if ( Cec2_ManSweepNode(pMan, i) ) | |
| { | |
| if ( Gia_ObjProved(p, i) ) | |
| pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); | |
| continue; | |
| } | |
| pObj->Value = ~0; | |
| Vec_IntPushThree( pMan->vCexTriples, Gia_ObjId(p, pRepr), i, Abc_Var2Lit(p->iPatsPi, pObj->fPhase ^ pRepr->fPhase) ); | |
| fDisproved = 1; | |
| } | |
| if ( fDisproved ) | |
| { | |
| int Fails = Cec2_ManSimulate( p, pMan->vCexTriples, pMan ); | |
| if ( Fails && pPars->fVerbose ) | |
| printf( "Failed to resimulate %d times with pattern = %d (total = %d).\n", Fails, pMan->nPatterns, pPars->nSimWords * 64 ); | |
| if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected | |
| break; | |
| } | |
| Cec2_ManPrintStats( p, pPars, pMan ); | |
| } | |
| // finish the AIG, if it is not finished | |
| if ( ppNew ) | |
| { | |
| Gia_ManForEachAnd( p, pObj, i ) | |
| if ( !~pObj->Value ) | |
| pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); | |
| Gia_ManForEachCo( p, pObj, i ) | |
| pObj->Value = Gia_ManAppendCo( pMan->pNew, Gia_ObjFanin0Copy(pObj) ); | |
| *ppNew = Gia_ManCleanup( pMan->pNew ); | |
| (*ppNew)->pName = Abc_UtilStrsav( p->pName ); | |
| (*ppNew)->pSpec = Abc_UtilStrsav( p->pSpec ); | |
| } | |
| finalize: | |
| Cec2_ManDestroy( pMan ); | |
| //Gia_ManEquivPrintClasses( p, 1, 0 ); | |
| return p->pCexSeq ? 0 : 1; | |
| } | |
| Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars0 ) | |
| { | |
| Gia_Man_t * pNew = NULL; | |
| //abctime clk = Abc_Clock(); | |
| Cec2_Par_t Pars, * pPars = &Pars; | |
| Cec2_SetDefaultParams( pPars ); | |
| // set resource limits | |
| // pPars->nSimWords = pPars0->nWords; // simulation words | |
| // pPars->nSimRounds = pPars0->nRounds; // simulation rounds | |
| // pPars->nItersMax = pPars0->nItersMax; // max number of iterations | |
| pPars->nConfLimit = pPars0->nBTLimit; // conflict limit at a node | |
| pPars->fUseCones = pPars0->fUseCones; | |
| pPars->fVerbose = pPars0->fVerbose; | |
| // Gia_ManComputeGiaEquivs( p, 100000, 0 ); | |
| // Gia_ManEquivPrintClasses( p, 1, 0 ); | |
| Cec2_ManPerformSweeping( p, pPars, &pNew ); | |
| //Abc_PrintTime( 1, "SAT sweeping time", Abc_Clock() - clk ); | |
| return pNew; | |
| } | |
| //////////////////////////////////////////////////////////////////////// | |
| /// END OF FILE /// | |
| //////////////////////////////////////////////////////////////////////// | |
| ABC_NAMESPACE_IMPL_END | |