| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bmc/ |
| H A D | bmcBCore.c | 57 Vec_Int_t * Bmc_ManBCoreCollectPivots( Gia_Man_t * p, char * pName, Vec_Int_t * vVarMap ) in Bmc_ManBCoreCollectPivots() argument
70 Vec_IntForEachEntryDouble( vVarMap, iVar, iFrame, i ) in Bmc_ManBCoreCollectPivots()
200 Vec_Int_t * vVarMap, * vCore; in Bmc_ManBCorePerform() local
210 vVarMap = Bmc_ManBCoreCollect( p, pPars->iFrame, pPars->iOutput, pSat ); in Bmc_ManBCorePerform()
215 Vec_Int_t * vPivots = Bmc_ManBCoreCollectPivots(p, pPars->pFilePivots, vVarMap); in Bmc_ManBCorePerform()
224 Vec_IntFree( vVarMap ); in Bmc_ManBCorePerform()
231 Vec_IntFree( vVarMap ); in Bmc_ManBCorePerform()
257 Intp_ManUnsatCorePrintForBmc( pFile, (Sto_Man_t *)pSatCnf, vCore, vVarMap ); in Bmc_ManBCorePerform()
262 Vec_IntFree( vVarMap ); in Bmc_ManBCorePerform()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/ |
| H A D | satProof.c | 653 Vec_Int_t * vVarMap;
657 vVarMap = Vec_IntStart( s->size );
664 pMask = Vec_IntEntryP(vVarMap, Entry);
670 Vec_IntForEachEntry( vVarMap, Entry, i )
673 Vec_IntFree( vVarMap );
725 vVarMap = Vec_IntStartFull( s->size );
727 Vec_IntWriteEntry( vVarMap, Entry, i );
752 Vec_IntFree( vVarMap );
828 vVarMap = Vec_IntStartFull( s->size );
830 Vec_IntWriteEntry( vVarMap, Entry, i );
[all …]
|
| H A D | satStore.h | 146 … Intp_ManUnsatCorePrintForBmc( FILE * pFile, Sto_Man_t * pCnf, void * vCore, void * vVarMap );
|
| H A D | satInterP.c | 1062 Vec_Int_t * vVarMap = (Vec_Int_t *)vVarMap0; in Intp_ManUnsatCorePrintForBmc() local
1079 iObj = Vec_IntEntry(vVarMap, 2*Abc_Lit2Var(pClause->pLits[v])); in Intp_ManUnsatCorePrintForBmc()
1080 iFrame = Vec_IntEntry(vVarMap, 2*Abc_Lit2Var(pClause->pLits[v])+1); in Intp_ManUnsatCorePrintForBmc()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/abci/ |
| H A D | abcQbf.c | 85 Vec_Int_t * vVarMap, * vForAlls, * vExists; in Abc_NtkQbf() local
90 vVarMap = Vec_IntStart( pCnf->nVars ); in Abc_NtkQbf()
93 Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Aig_ObjId(pObj)], 1 ); in Abc_NtkQbf()
97 Vec_IntForEachEntry( vVarMap, Entry, i ) in Abc_NtkQbf()
109 Vec_IntFree( vVarMap ); in Abc_NtkQbf()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
| H A D | AbcGlucose.cpp | 833 Vec_Int_t * vVarMap = Vec_IntStartFull( iFirstVar + nVars ); in bmcg_sat_solver_sop() local
837 Vec_IntWriteEntry( vVarMap, iFirstVar+i, i ); in bmcg_sat_solver_sop()
840 Vec_Str_t * vSop = Glucose_GenerateCubes( pSat, vVars, vVarMap, CubeLimit ); in bmcg_sat_solver_sop()
841 Vec_IntFree( vVarMap ); in bmcg_sat_solver_sop()
1085 Vec_Int_t * vVarMap = NULL; Vec_Str_t * vSop = NULL; in bmcg_sat_solver_quantify() local
1138 vVarMap = Vec_IntStartFull( Vec_IntSize(vObjsUsed) ); in bmcg_sat_solver_quantify()
1144 Vec_IntWriteEntry( vVarMap, iVar, i ), Count++; in bmcg_sat_solver_quantify()
1152 vSop = Glucose_GenerateCubes( pSats, vCiVars, vVarMap, 0 ); in bmcg_sat_solver_quantify()
1174 Vec_IntFreeP( &vVarMap ); in bmcg_sat_solver_quantify()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/ |
| H A D | giaQbf.c | 262 Vec_Int_t * vVarMap, * vForAlls, * vExists; in Gia_QbfDumpFile() local
267 vVarMap = Vec_IntStart( pCnf->nVars ); in Gia_QbfDumpFile()
270 Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Gia_ManCiIdToId(pGia, i)], 1 ); in Gia_QbfDumpFile()
274 Vec_IntForEachEntry( vVarMap, Entry, i ) in Gia_QbfDumpFile()
285 Vec_IntFree( vVarMap ); in Gia_QbfDumpFile()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/msat/ |
| H A D | msat.h | 98 extern void Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap );
|