| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/ |
| H A D | giaPat.c | 93 void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit ) in Gia_SatVerifyPattern()
|
| H A D | giaGiarf.c | 676 int Gia_GiarfStorePattern( Vec_Ptr_t * vSimInfo, Vec_Ptr_t * vPres, Vec_Int_t * vCex ) in Gia_GiarfStorePattern()
696 void Gia_GiarfInsertPattern( Hcd_Man_t * p, Vec_Int_t * vCex, int k ) in Gia_GiarfInsertPattern()
763 Vec_Int_t * vCex; in Gia_ComputeEquivalencesLevel() local
|
| H A D | giaCSat.c | 238 static inline void Cbs_ManSaveModel( Cbs_Man_t * p, Vec_Int_t * vCex ) in Cbs_ManSaveModel()
249 static inline void Cbs_ManSaveModelAll( Cbs_Man_t * p, Vec_Int_t * vCex ) in Cbs_ManSaveModelAll()
1042 Vec_Int_t * vCex, * vVisit, * vCexStore; in Cbs_ManSolveMiterNc() local
|
| H A D | giaCSatOld.c | 208 static inline void Cbs0_ManSaveModel( Cbs0_Man_t * p, Vec_Int_t * vCex ) in Cbs0_ManSaveModel()
712 Vec_Int_t * vCex, * vVisit, * vCexStore; in Cbs_ManSolveMiter() local
|
| H A D | giaCTas.c | 285 static inline void Tas_ManSaveModel( Tas_Man_t * p, Vec_Int_t * vCex ) in Tas_ManSaveModel()
1522 Vec_Int_t * vCex, * vVisit, * vCexStore; in Tas_ManSolveMiterNc() local
1676 int Tas_StorePattern( Vec_Ptr_t * vSimInfo, Vec_Ptr_t * vPres, Vec_Int_t * vCex ) in Tas_StorePattern()
1704 Vec_Int_t * vCex, * vVisit, * vCexStore; in Tas_ManSolveMiterNc2() local
|
| H A D | giaCSat2.c | 317 static inline void Cbs2_ManSaveModel( Cbs2_Man_t * p, Vec_Int_t * vCex ) in Cbs2_ManSaveModel()
329 static inline void Cbs2_ManSaveModelAll( Cbs2_Man_t * p, Vec_Int_t * vCex ) in Cbs2_ManSaveModelAll()
1564 Vec_Int_t * vCex, * vVisit, * vCexStore; in Cbs2_ManSolveMiterNc() local
|
| H A D | giaSweeper.c | 753 …Int_t * Gia_ManGetCex( Gia_Man_t * pGia, Vec_Int_t * vId2Lit, sat_solver * pSat, Vec_Int_t * vCex ) in Gia_ManGetCex()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/cmd/ |
| H A D | cmdPlugin.c | 286 Vec_Int_t * Abc_ManExpandCex( Gia_Man_t * pGia, Vec_Int_t * vCex ) in Abc_ManExpandCex()
416 Vec_Int_t * vCex; in Cmd_CommandAbcPlugIn() local
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/fra/ |
| H A D | fraClau.c | 345 int Fra_ClauCheckProperty( Cla_Man_t * p, Vec_Int_t * vCex ) in Fra_ClauCheckProperty()
425 int Fra_ClauCheckClause( Cla_Man_t * p, Vec_Int_t * vClause, Vec_Int_t * vCex ) in Fra_ClauCheckClause()
598 void Fra_ClauPrintClause( Vec_Int_t * vSatCsVars, Vec_Int_t * vCex ) in Fra_ClauPrintClause()
|
| H A D | fraCore.c | 186 void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex ) in Fra_FraigVerifyCounterEx()
|
| H A D | fra.h | 206 Vec_Int_t * vCex; member
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/opt/mfs/ |
| H A D | mfsGia.c | 169 void Abc_NtkMfsResimulate( Gia_Man_t * p, Vec_Int_t * vCex ) in Abc_NtkMfsResimulate()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/cec/ |
| H A D | cecInt.h | 91 Vec_Int_t * vCex; // the latest counter-example member
|
| H A D | cecSolve.c | 993 void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out ) in Cec_ManSatAddToStore()
|