Searched refs:pCnf2 (Results 1 – 4 of 4) sorted by relevance
75 assert( p->pCnf2->pObj2Count[Aig_ObjId(pObj)] >= 0 ); in Pdr_ObjSatVar2FindOrAdd()115 iClaBeg = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)]; in Pdr_ObjSatVar2()116 iClaEnd = iClaBeg + p->pCnf2->pObj2Count[Aig_ObjId(pObj)]; in Pdr_ObjSatVar2()140 for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ ) in Pdr_ObjSatVar2()158 for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ ) in Pdr_ObjSatVar2()176 assert( p->pCnf2->pObj2Count[Aig_ObjId(pObj)] >= 0 ); in Pdr_ObjSatVar2FindOrAdd()208 iClaBeg = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)]; in Pdr_ObjSatVar2()209 iClaEnd = iClaBeg + p->pCnf2->pObj2Count[Aig_ObjId(pObj)]; in Pdr_ObjSatVar2()217 for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ ) in Pdr_ObjSatVar2()394 if ( p->pCnf2 == NULL ) in Pdr_ManNewSolver2()[all …]
107 Cnf_Dat_t * pCnf2; // CNF for this AIG member
355 Cnf_DataFree( p->pCnf2 ); in Pdr_ManStop()
1068 Cnf_Dat_t * pCnf2; in Gia_ManFaultAddOne() local1074 pCnf2 = Cnf_DeriveGiaRemapped( pC ); in Gia_ManFaultAddOne()1075 Cnf_DataLiftGia( pCnf2, pC, sat_solver_nvars(pSat) ); in Gia_ManFaultAddOne()1077 for ( i = 0; i < pCnf2->nClauses; i++ ) in Gia_ManFaultAddOne()1078 if ( !sat_solver_addclause( pSat, pCnf2->pClauses[i], pCnf2->pClauses[i+1] ) ) in Gia_ManFaultAddOne()1080 Cnf_DataFree( pCnf2 ); in Gia_ManFaultAddOne()1106 Cnf_DataFree( pCnf2 ); in Gia_ManFaultAddOne()1119 Cnf_DataFree( pCnf2 ); in Gia_ManFaultAddOne()1310 Cnf_Dat_t * pCnf2; in Gia_ManFaultDumpNewFaults() local1318 pCnf2 = Cnf_DeriveGiaRemapped( pC ); in Gia_ManFaultDumpNewFaults()[all …]