| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/abs/ |
| H A D | absOldCex.c | 276 Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons ); in Saig_ManCbaFindReason_rec()
290 int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ); in Saig_ManCbaFindReason_rec()
291 int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) ); in Saig_ManCbaFindReason_rec()
314 Vec_Int_t * vPrios, * vReasons; in Saig_ManCbaFindReason() local
318 vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) ); in Saig_ManCbaFindReason()
325 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i ); in Saig_ManCbaFindReason()
333 int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ); in Saig_ManCbaFindReason()
334 int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) ); in Saig_ManCbaFindReason()
339 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 ); in Saig_ManCbaFindReason()
341 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 ); in Saig_ManCbaFindReason()
[all …]
|
| H A D | absOldSat.c | 133 Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons ); in Saig_RefManFindReason_rec()
147 int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ); in Saig_RefManFindReason_rec()
148 int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) ); in Saig_RefManFindReason_rec()
171 Vec_Int_t * vPrios, * vPi2Prio, * vReasons; in Saig_RefManFindReason() local
175 vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) ); in Saig_RefManFindReason()
189 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i ); in Saig_RefManFindReason()
199 int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ); in Saig_RefManFindReason()
200 int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) ); in Saig_RefManFindReason()
205 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 ); in Saig_RefManFindReason()
207 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 ); in Saig_RefManFindReason()
[all …]
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/saig/ |
| H A D | saigRefSat.c | 133 Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons ); in Saig_RefManFindReason_rec()
147 int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ); in Saig_RefManFindReason_rec()
148 int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) ); in Saig_RefManFindReason_rec()
171 Vec_Int_t * vPrios, * vPi2Prio, * vReasons; in Saig_RefManFindReason() local
175 vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) ); in Saig_RefManFindReason()
189 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i ); in Saig_RefManFindReason()
199 int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ); in Saig_RefManFindReason()
200 int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) ); in Saig_RefManFindReason()
205 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 ); in Saig_RefManFindReason()
207 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 ); in Saig_RefManFindReason()
[all …]
|
| /dports/math/stp/stp-2.3.3/lib/extlib-abc/aig/dar/ |
| H A D | darLib.c | 277 void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios ) in Dar_LibSetup() argument
367 p->pPrios[i][k] = Vec_IntEntry(vPrios, Counter++); in Dar_LibSetup()
371 assert( Counter == Vec_IntSize(vPrios) ); in Dar_LibSetup()
554 Vec_Int_t * vObjs, * vOuts, * vPrios; in Dar_LibRead() local
560 vPrios = Dar_LibReadPrios(); in Dar_LibRead()
568 Dar_LibSetup( p, vOuts, vPrios ); in Dar_LibRead()
571 Vec_IntFree( vPrios ); in Dar_LibRead()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/opt/dar/ |
| H A D | darLib.c | 284 void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios ) in Dar_LibSetup() argument
374 p->pPrios[i][k] = Vec_IntEntry(vPrios, Counter++); in Dar_LibSetup()
378 assert( Counter == Vec_IntSize(vPrios) ); in Dar_LibSetup()
561 Vec_Int_t * vObjs, * vOuts, * vPrios; in Dar_LibRead() local
567 vPrios = Dar_LibReadPrios(); in Dar_LibRead()
575 Dar_LibSetup( p, vOuts, vPrios ); in Dar_LibRead()
578 Vec_IntFree( vPrios ); in Dar_LibRead()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/pdr/ |
| H A D | pdrCore.c | 501 static inline int Vec_IntSelectSortPrioReverseLit( int * pArray, int nSize, Vec_Int_t * vPrios ) in Vec_IntSelectSortPrioReverseLit() argument
508 …if ( Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[best_i… in Vec_IntSelectSortPrioReverseLit()
|