| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/fra/ |
| H A D | fraCec.c | 47 int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStar… in Fra_FraigSat()
320 int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ) in Fra_FraigCec()
451 int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, i… in Fra_FraigCecPartitioned()
513 int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmar… in Fra_FraigCecTop()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/int/ |
| H A D | intCtrex.c | 97 int nConfLimit = 1000000; in Inter_ManGetCounterExample() local
|
| H A D | intInt.h | 70 int nConfLimit; // the limit on the number of conflicts member
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/ssw/ |
| H A D | sswBmc.c | 126 int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame ) in Ssw_BmcDynamic()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/saig/ |
| H A D | saigTempor.c | 186 Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc… in Saig_ManTempor()
|
| H A D | saigRetMin.c | 52 int nConfLimit = 1000000; in Saig_ManRetimeInitState() local
99 int nConfLimit = 1000000; in Saig_ManRetimeUnsatCore() local
|
| H A D | saigGlaCba.c | 37 int nConfLimit; member
681 …n_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit… in Aig_Gla1ManPerform()
|
| H A D | saigRefSat.c | 504 int nConfLimit = 1000000; in Saig_RefManRunSat() local
708 int nConfLimit = 1000000; in Saig_RefManRefineWithSat() local
|
| H A D | saigGlaPba.c | 525 Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int T… in Aig_Gla2ManPerform()
|
| H A D | saigGlaPba2.c | 495 Vec_Int_t * Aig_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int T… in Aig_Gla3ManPerform()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bmc/ |
| H A D | bmcLoad.c | 163 int nConfLimit = 0; in Bmc_LoadTest() local
|
| H A D | bmcBmc.c | 207 int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, i… in Saig_ManBmcSimple()
|
| H A D | bmc.h | 93 int nConfLimit; // maximum number of conflicts at a node member
132 int nConfLimit; // maximum number of conflicts at a node member
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/abci/ |
| H A D | abcVerify.c | 56 void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit ) in Abc_NtkCecSat()
490 void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrame… in Abc_NtkSecSat()
|
| H A D | abcIvy.c | 392 Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ) in Abc_NtkIvySat()
459 Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTran… in Abc_NtkIvyFraig()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/abs/ |
| H A D | absOldSat.c | 504 int nConfLimit = 1000000; in Saig_RefManRunSat() local
708 int nConfLimit = 1000000; in Saig_RefManRefineWithSat() local
|
| H A D | abs.h | 52 int nConfLimit; // conflict limit member
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/pdr/ |
| H A D | pdrSat.c | 290 int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit,… in Pdr_ManCheckCube()
|
| H A D | pdr.h | 46 int nConfLimit; // limit on SAT solver conflicts member
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/ |
| H A D | satSolver3.c | 1996 void sat_solver3_set_resource_limits(sat_solver3* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit,… in sat_solver3_set_resource_limits()
2013 int sat_solver3_solve(sat_solver3* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nIn… in sat_solver3_solve()
2135 int sat_solver3_minimize_assumptions( sat_solver3* s, int * pLits, int nLits, int nConfLimit ) in sat_solver3_minimize_assumptions()
2194 int sat_solver3_minimize_assumptions2( sat_solver3* s, int * pLits, int nLits, int nConfLimit ) in sat_solver3_minimize_assumptions2()
|
| H A D | satSolver.c | 2049 void sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, A… in sat_solver_set_resource_limits()
2066 int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsL… in sat_solver_solve()
2207 int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit ) in sat_solver_minimize_assumptions()
2282 int sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit ) in sat_solver_minimize_assumptions2()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/cnf/ |
| H A D | cnfUtil.c | 402 int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, … in Cnf_DataSolveFromFile()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/ |
| H A D | giaQbf.c | 198 int Gia_ManSatEnum( Gia_Man_t * pGia, int nConfLimit, int nTimeOut, int fVerbose ) in Gia_ManSatEnum()
635 int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fG… in Gia_QbfSolve()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/msat/ |
| H A D | msatSolverSearch.c | 535 Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrack… in Msat_SolverSearch()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/fraig/ |
| H A D | fraig.h | 63 int nConfLimit; // the limit on the number of conflicts member
|