Home
last modified time | relevance | path

Searched refs:nLearntMax (Results 1 – 13 of 13) sorted by relevance

/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/
H A DsatSolver2.h118 int nLearntMax; // enables using reduce DB method member
241 static inline int sat_solver2_set_learntmax(sat_solver2* s, int nLearntMax) in sat_solver2_set_learntmax() argument
243 int temp = s->nLearntMax; in sat_solver2_set_learntmax()
244 s->nLearntMax = nLearntMax; in sat_solver2_set_learntmax()
H A DsatSolver2.c1138 s->nLearntMax = s->nLearntStart; in sat_solver2_new()
1419 assert( s->nLearntMax ); in sat_solver2_reducedb()
1439 s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces; in sat_solver2_reducedb()
1441 CounterStart = nLearnedOld - (s->nLearntMax / 20); in sat_solver2_reducedb()
1954 (double)s->nLearntMax, in sat_solver2_solve()
1964 if ( s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax && s->pPrf2 == NULL ) in sat_solver2_solve()
H A DsatSolver3.c1122 s->nLearntMax = s->nLearntStart; in sat_solver3_new()
1187 s->nLearntMax = s->nLearntStart; in zsat_solver3_new_seed()
1497 assert( s->nLearntMax > 0 ); in sat_solver3_reducedb()
1504 s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces; in sat_solver3_reducedb()
1521 CounterStart = nLearnedOld - (s->nLearntMax / 20); in sat_solver3_reducedb()
1859 if (s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax) in sat_solver3_search()
H A DsatSolver.c1148 s->nLearntMax = s->nLearntStart; in sat_solver_new()
1213 s->nLearntMax = s->nLearntStart; in zsat_solver_new_seed()
1532 assert( s->nLearntMax > 0 ); in sat_solver_reducedb()
1539 s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces; in sat_solver_reducedb()
1556 CounterStart = nLearnedOld - (s->nLearntMax / 20); in sat_solver_reducedb()
1903 if (s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax) in sat_solver_search()
H A DsatSolver3.h162 int nLearntMax; // max number of learned clauses member
H A DsatSolver.h164 int nLearntMax; // max number of learned clauses member
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/fra/
H A DfraCec.c197 pSat->nLearntStart = pSat->nLearntMax = nLearnedStart; in Fra_FraigSat()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/cnf/
H A DcnfUtil.c424 pSat->nLearntStart = pSat->nLearntMax = nLearnedStart; in Cnf_DataSolveFromFile()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bmc/
H A DbmcBmc2.c325 p->pSat->nLearntMax = p->pSat->nLearntStart; in Saig_BmcManStart()
H A DbmcBmc3.c1490 p->pSat->nLearntMax = p->pSat->nLearntStart; in Saig_ManBmcScalable()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/abs/
H A DabsVta.c1014 p->pSat->nLearntMax = p->pSat->nLearntStart; in Vga_ManStart()
H A DabsGla.c1124 p->pSat->nLearntMax = p->pSat->nLearntStart; in Ga2_ManRestart()
H A DabsGlaOld.c983 p->pSat->nLearntMax = p->pSat->nLearntStart; in Gla_ManStart()