Searched refs:vId2Lit (Results 1 – 4 of 4) sorted by relevance
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/ |
| H A D | giaSweeper.c | 67 Vec_Int_t * vId2Lit; // mapping of Obj IDs into SAT literal member
89 … { assert( Vec_IntEntry(p->vId2Lit, Abc_Lit2Var(Lit)) ); return Abc_Lit2LitL( Vec_IntA… in Swp_ManLit2Lit()
118 p->vId2Lit = Vec_IntAlloc( 10000 ); in Swp_ManStart()
137 Vec_IntFree( p->vId2Lit ); in Swp_ManStop()
175 nMem += Vec_IntCap(p->vId2Lit); in Gia_SweeperMemUsage()
516 Vec_IntClear( pSwp->vId2Lit ); in Gia_SweeperCleanup()
760 if ( Gia_ObjId(pGia, pObj) >= Vec_IntSize(vId2Lit) ) in Gia_ManGetCex()
765 LitSat = Vec_IntEntry( vId2Lit, Gia_ObjId(pGia, pObj) ); in Gia_ManGetCex()
857 p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp ); in Gia_SweeperCheckEquiv()
897 p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp ); in Gia_SweeperCheckEquiv()
[all …]
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/abci/ |
| H A D | abcDress2.c | 148 Vec_Int_t * vId2Lit; in Abc_NtkDressMapClasses() local
152 vId2Lit = Vec_IntAlloc( 0 ); in Abc_NtkDressMapClasses()
153 Vec_IntFill( vId2Lit, Abc_NtkObjNumMax(pNtk), -1 ); in Abc_NtkDressMapClasses()
165 Vec_IntWriteEntry( vId2Lit, i, Aig_ObjId(pObjRepr) ); in Abc_NtkDressMapClasses()
168 return vId2Lit; in Abc_NtkDressMapClasses()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/abs/ |
| H A D | absGla.c | 59 Vec_Ptr_t * vId2Lit; // mapping, for each timeframe, of object ID into SAT literal member
95 …Man_t * p, int f ) { return (Vec_Int_t *)Vec_PtrEntry( p->vId2Lit, f ); … in Ga2_MapFrameMap()
399 p->vId2Lit = Vec_PtrAlloc( 1000 ); in Ga2_ManStart()
438 double memMap = Vec_VecMemoryInt( (Vec_Vec_t *)p->vId2Lit ); in Ga2_ManReportMemory()
475 Vec_VecFree( (Vec_Vec_t *)p->vId2Lit ); in Ga2_ManStop()
1045 Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i ) in Ga2_ManShrinkAbs()
1596 if ( f == Vec_PtrSize(p->vId2Lit) ) in Gia_ManPerformGla()
1597 Vec_PtrPush( p->vId2Lit, Vec_IntAlloc(0) ); in Gia_ManPerformGla()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bmc/ |
| H A D | bmcBmc3.c | 55 Vec_Int_t * vId2Lit; // mapping cuts into literals member
777 p->vId2Lit = Vec_IntAlloc( 10000 ); in Saig_Bmc3ManStart()
836 Vec_IntFree( p->vId2Lit ); in Saig_Bmc3ManStop()
1112 assert( iEntry == Vec_IntSize(p->vId2Lit) ); in Saig_ManBmcCreateCnf_rec()
1113 Vec_IntPush( p->vId2Lit, iLit ); in Saig_ManBmcCreateCnf_rec()
1118 iLit = Vec_IntEntry( p->vId2Lit, iRes ); in Saig_ManBmcCreateCnf_rec()
|