/dports/math/glucose/glucose-syrup-4.1/parallel/ |
H A D | ParallelSolver.cc | 159 sort(learnts, reduceDBAct_lt(ca)); in reduceDB() 161 sort(learnts, reduceDB_lt(ca)); in reduceDB() 165 …if (ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd() <= 3) nbclausesbeforereduce += specialI… in reduceDB() 173 limit = learnts.size() / 2; in reduceDB() 182 Clause& c = ca[learnts[i]]; in reduceDB() 183 if (i == learnts.size() / 2) in reduceDB() 187 removeClause(learnts[i]); in reduceDB() 193 learnts[j++] = learnts[i]; in reduceDB() 196 learnts.shrink(i - j); in reduceDB() 198 if (learnts.size() > 0) in reduceDB() [all …]
|
/dports/math/chuffed/chuffed-e04bedd/chuffed/core/ |
H A D | sat.cpp | 104 for (int i = 0; i < learnts.size(); i++) free(learnts[i]); in ~SAT() 236 learnts.push(&c); in addClause() 310 if (simplify(*learnts[i])) removeClause(*learnts[i]); in simplifyDB() 311 else learnts[j++] = learnts[i]; in simplifyDB() 313 learnts.resize(j); in simplifyDB() 523 std::sort((Clause**) learnts, (Clause**) learnts + learnts.size(), activity_lt()); in reduceDB() 526 if (!locked(*learnts[i])) removeClause(*learnts[i]); in reduceDB() 527 else learnts[j++] = learnts[i]; in reduceDB() 530 learnts[j++] = learnts[i]; in reduceDB() 532 learnts.resize(j); in reduceDB() [all …]
|
/dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/ |
H A D | Solver.C | 66 for (int i = 0; i < learnts.size(); i++) free(learnts[i]); in ~Solver() 497 sort(learnts, reduceDB_lt()); in reduceDB() 499 if (learnts[i]->size() > 2 && !locked(*learnts[i])) in reduceDB() 500 removeClause(*learnts[i]); in reduceDB() 502 learnts[j++] = learnts[i]; in reduceDB() 504 for (; i < learnts.size(); i++){ in reduceDB() 505 if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() < extra_lim) in reduceDB() 508 learnts[j++] = learnts[i]; in reduceDB() 510 learnts.shrink(i - j); in reduceDB() 546 removeSatisfied(learnts); in simplify() [all …]
|
H A D | Solver.h | 127 vec<Clause*> learnts; // List of learnt clauses. variable 239 for (int i = 0; i < learnts.size(); i++) in claBumpActivity() 240 learnts[i]->activity() *= 1e-20; in claBumpActivity() 254 inline int Solver::nLearnts () const { return learnts.size(); } in nLearnts()
|
/dports/math/igraph/igraph-0.9.5/vendor/glpk/minisat/ |
H A D | minisat.c | 396 s->stats.learnts--; in clause_remove() 556 s->stats.learnts++; in solver_record() 863 clause** learnts = (clause**)vecp_begin(&s->learnts); in solver_reducedb() local 866 sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), clause_cmp); in solver_reducedb() 871 != learnts[i]) in solver_reducedb() 874 learnts[j++] = learnts[i]; in solver_reducedb() 879 != learnts[i] in solver_reducedb() 883 learnts[j++] = learnts[i]; in solver_reducedb() 888 vecp_resize(&s->learnts,j); in solver_reducedb() 1001 vecp_new(&s->learnts); in solver_new() [all …]
|
H A D | minisat.h | 138 double clauses, clauses_literals, learnts, learnts_literals, member 152 vecp learnts; /* List of learnt clauses. member
|
/dports/math/glpk/glpk-5.0/src/minisat/ |
H A D | minisat.c | 396 s->stats.learnts--; in clause_remove() 556 s->stats.learnts++; in solver_record() 863 clause** learnts = (clause**)vecp_begin(&s->learnts); in solver_reducedb() local 866 sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), clause_cmp); in solver_reducedb() 871 != learnts[i]) in solver_reducedb() 874 learnts[j++] = learnts[i]; in solver_reducedb() 879 != learnts[i] in solver_reducedb() 883 learnts[j++] = learnts[i]; in solver_reducedb() 888 vecp_resize(&s->learnts,j); in solver_reducedb() 1001 vecp_new(&s->learnts); in solver_new() [all …]
|
H A D | minisat.h | 138 double clauses, clauses_literals, learnts, learnts_literals, member 152 vecp learnts; /* List of learnt clauses. member
|
/dports/cad/yosys/yosys-yosys-0.12/libs/minisat/ |
H A D | Solver.cc | 592 sort(learnts, reduceDB_lt(ca)); in reduceDB() 596 Clause& c = ca[learnts[i]]; in reduceDB() 598 removeClause(learnts[i]); in reduceDB() 600 learnts[j++] = learnts[i]; in reduceDB() 602 learnts.shrink(i - j); in reduceDB() 658 removeSatisfied(learnts); in simplify() 731 learnts.push(cr); in search() 1044 if (!isRemoved(learnts[i])){ in relocAll() 1045 ca.reloc(learnts[i], to); in relocAll() 1046 learnts[j++] = learnts[i]; in relocAll() [all …]
|
/dports/math/minisat/minisat-2.2.1/minisat/core/ |
H A D | Solver.cc | 586 sort(learnts, reduceDB_lt(ca)); in reduceDB() 590 Clause& c = ca[learnts[i]]; in reduceDB() 592 removeClause(learnts[i]); in reduceDB() 594 learnts[j++] = learnts[i]; in reduceDB() 596 learnts.shrink(i - j); in reduceDB() 652 removeSatisfied(learnts); in simplify() 725 learnts.push(cr); in search() 1038 if (!isRemoved(learnts[i])){ in relocAll() 1039 ca.reloc(learnts[i], to); in relocAll() 1040 learnts[j++] = learnts[i]; in relocAll() [all …]
|
/dports/textproc/link-grammar/link-grammar-5.8.0/link-grammar/minisat/minisat/core/ |
H A D | Solver.cc | 586 sort(learnts, reduceDB_lt(ca)); in reduceDB() 590 Clause& c = ca[learnts[i]]; in reduceDB() 592 removeClause(learnts[i]); in reduceDB() 594 learnts[j++] = learnts[i]; in reduceDB() 596 learnts.shrink(i - j); in reduceDB() 652 removeSatisfied(learnts); in simplify() 725 learnts.push(cr); in search() 1038 if (!isRemoved(learnts[i])){ in relocAll() 1039 ca.reloc(learnts[i], to); in relocAll() 1040 learnts[j++] = learnts[i]; in relocAll() [all …]
|
/dports/math/vampire/vampire-4.5.1/Minisat/core/ |
H A D | Solver.cc | 591 sort(learnts, reduceDB_lt(ca)); in reduceDB() 595 Clause& c = ca[learnts[i]]; in reduceDB() 597 removeClause(learnts[i]); in reduceDB() 599 learnts[j++] = learnts[i]; in reduceDB() 601 learnts.shrink(i - j); in reduceDB() 657 removeSatisfied(learnts); in simplify() 730 learnts.push(cr); in search() 1045 if (!isRemoved(learnts[i])){ in relocAll() 1046 ca.reloc(learnts[i], to); in relocAll() 1047 learnts[j++] = learnts[i]; in relocAll() [all …]
|
/dports/math/glucose/glucose-syrup-4.1/core/ |
H A D | Solver.cc | 306 s.learnts.memCopyTo(learnts); in Solver() 1268 int limit = learnts.size() / 2; in reduceDB() 1271 Clause &c = ca[learnts[i]]; in reduceDB() 1273 removeClause(learnts[i]); in reduceDB() 1279 learnts[j++] = learnts[i]; in reduceDB() 1282 learnts.shrink(i - j); in reduceDB() 1339 removeSatisfied(learnts); in simplify() 1421 learnts[j++] = learnts[i]; in adaptSolver() 1424 learnts.shrink(i - j); in adaptSolver() 1433 learnts.shrink(learnts.size()); in adaptSolver() [all …]
|
/dports/math/ogdf/OGDF/src/ogdf/lib/minisat/core/ |
H A D | Solver.cpp | 532 sort(learnts, reduceDB_lt(ca)); in reduceDB() 535 for (i = j = 0; i < learnts.size(); i++){ in reduceDB() 536 Clause& c = ca[learnts[i]]; in reduceDB() 538 removeClause(learnts[i]); in reduceDB() 540 learnts[j++] = learnts[i]; in reduceDB() 542 learnts.shrink(i - j); in reduceDB() 590 removeSatisfied(learnts); in simplify() 639 learnts.push(cr); in search() 737 learnts.push(cr); in search() 1077 for (int i = 0; i < learnts.size(); i++) in relocAll() [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/ |
H A D | Solver.cpp | 530 sort(learnts, reduceDB_lt(ca)); in reduceDB() 533 for (i = j = 0; i < learnts.size(); i++){ in reduceDB() 534 Clause& c = ca[learnts[i]]; in reduceDB() 536 removeClause(learnts[i]); in reduceDB() 538 learnts[j++] = learnts[i]; in reduceDB() 540 learnts.shrink(i - j); in reduceDB() 588 removeSatisfied(learnts); in simplify() 637 learnts.push(cr); in search() 670 if (learnts.size()-nAssigns() >= max_learnts) in search() 903 for (i = 0; i < learnts.size(); i++) in relocAll() [all …]
|
H A D | Solver.h | 173 vec<CRef> learnts; // List of learnt clauses. variable 300 for (int i = 0; i < learnts.size(); i++) in claBumpActivity() 301 ca[learnts[i]].activity() *= (float)1e-20; in claBumpActivity() 327 inline int Solver::nLearnts () const { return learnts.size(); } in nLearnts()
|
/dports/math/clasp/clasp-3.3.5/clasp/ |
H A D | solver_types.h | 67 uint32 learnts; //!< Limit on number of learnt lemmas. member 244 …STAT(Array learnts; DOXY(lemmas of each learnt type) , "lemmas" , MEM_FUN(lemma… 254 STAT(NO_ARG , "lemmas_conflict", VALUE(learnts[0]) , LHS.learnts[0] += RHS.learnts[0]) \ 255 STAT(NO_ARG , "lemmas_loop" , VALUE(learnts[1]) , LHS.learnts[1] += RHS.learnts[1]) \ 256 STAT(NO_ARG , "lemmas_other" , VALUE(learnts[2]) , LHS.learnts[2] += RHS.learnts[2]) \ 266 learnts[t-1]+= 1; in addLearnt() 272 …uint64 lemmas() const { return std::accumulate(learnts, learnts+Constraint_t::Type__max, ui… in lemmas() 276 uint64 lemmas(type_t t)const { return learnts[t-1]; } in lemmas() 282 double distRatio() const { return ratio(distributed, learnts[0] + learnts[1]); } in distRatio()
|
/dports/math/clingo/clingo-5.5.1/clasp/clasp/ |
H A D | solver_types.h | 67 uint32 learnts; //!< Limit on number of learnt lemmas. member 244 …STAT(Array learnts; DOXY(lemmas of each learnt type) , "lemmas" , MEM_FUN(lemma… 254 STAT(NO_ARG , "lemmas_conflict", VALUE(learnts[0]) , LHS.learnts[0] += RHS.learnts[0]) \ 255 STAT(NO_ARG , "lemmas_loop" , VALUE(learnts[1]) , LHS.learnts[1] += RHS.learnts[1]) \ 256 STAT(NO_ARG , "lemmas_other" , VALUE(learnts[2]) , LHS.learnts[2] += RHS.learnts[2]) \ 266 learnts[t-1]+= 1; in addLearnt() 272 …uint64 lemmas() const { return std::accumulate(learnts, learnts+Constraint_t::Type__max, ui… in lemmas() 276 uint64 lemmas(type_t t)const { return learnts[t-1]; } in lemmas() 282 double distRatio() const { return ratio(distributed, learnts[0] + learnts[1]); } in distRatio()
|
/dports/math/clingo/clingo-5.5.1/clasp/clasp-da10954/clasp/ |
H A D | solver_types.h | 67 uint32 learnts; //!< Limit on number of learnt lemmas. member 244 …STAT(Array learnts; DOXY(lemmas of each learnt type) , "lemmas" , MEM_FUN(lemma… 254 STAT(NO_ARG , "lemmas_conflict", VALUE(learnts[0]) , LHS.learnts[0] += RHS.learnts[0]) \ 255 STAT(NO_ARG , "lemmas_loop" , VALUE(learnts[1]) , LHS.learnts[1] += RHS.learnts[1]) \ 256 STAT(NO_ARG , "lemmas_other" , VALUE(learnts[2]) , LHS.learnts[2] += RHS.learnts[2]) \ 266 learnts[t-1]+= 1; in addLearnt() 272 …uint64 lemmas() const { return std::accumulate(learnts, learnts+Constraint_t::Type__max, ui… in lemmas() 276 uint64 lemmas(type_t t)const { return learnts[t-1]; } in lemmas() 282 double distRatio() const { return ratio(distributed, learnts[0] + learnts[1]); } in distRatio()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
H A D | Glucose.cpp | 939 sort(learnts, reduceDB_lt(ca)); in reduceDB() 942 …if(ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd()<=3) nbclausesbeforereduce +=specialIncRe… in reduceDB() 949 int limit = learnts.size() / 2; in reduceDB() 951 Clause& c = ca[learnts[i]]; in reduceDB() 953 removeClause(learnts[i]); in reduceDB() 959 learnts[j++] = learnts[i]; in reduceDB() 962 learnts.shrink(i - j); in reduceDB() 1010 removeSatisfied(learnts); in simplify() 1098 learnts.push(cr); in search() 1418 ca.reloc(learnts[i], to); in relocAll() [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/satoko/ |
H A D | solver_api.c | 100 s->learnts = vec_uint_alloc(0); in satoko_create() 138 vec_uint_free(s->learnts); in satoko_destroy() 449 s->book_cl_lrnt = vec_uint_size(s->learnts); in satoko_bookmark() 476 vec_uint_clear(s->learnts); in satoko_reset() 512 unsigned n_learnts = vec_uint_size(s->learnts) - s->book_cl_lrnt; in satoko_rollback() 526 vec_uint_foreach_start(s->learnts, cref, i, s->book_cl_lrnt) in satoko_rollback() 534 vec_uint_shrink(s->learnts, s->book_cl_lrnt); in satoko_rollback() 589 unsigned n_lrnts = vec_uint_size(s->learnts); in satoko_write_dimacs() 617 array = vec_uint_data(s->learnts); in satoko_write_dimacs() 637 return vec_uint_size(s->learnts); in satoko_learntnum()
|
H A D | solver.c | 417 array = vec_uint_data(s->learnts); in solver_garbage_collect() 418 for (i = 0; i < vec_uint_size(s->learnts); i++) in solver_garbage_collect() 432 unsigned n_learnts = vec_uint_size(s->learnts); in solver_reduce_cdb() 438 vec_uint_foreach_start(s->learnts, cref, i, s->book_cl_lrnt) in solver_reduce_cdb() 451 vec_uint_clear(s->learnts); in solver_reduce_cdb() 465 vec_uint_push_back(s->learnts, cref); in solver_reduce_cdb() 472 vec_uint_size(s->learnts), n_learnts, in solver_reduce_cdb() 473 100.0 * vec_uint_size(s->learnts) / n_learnts); in solver_reduce_cdb() 503 vec_uint_push_back(s->learnts, cref); in solver_clause_create() 657 if (s->opts.learnt_ratio && vec_uint_size(s->learnts) > 100 && in solver_search()
|
/dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
H A D | Solver.cc | 877 sort(learnts, reduceDB_lt(ca)); in reduceDB() 880 for (i = j = 0; i < learnts.size(); i++){ in reduceDB() 881 Clause& c = ca[learnts[i]]; in reduceDB() 883 removeClause(learnts[i]); in reduceDB() 885 learnts[j++] = learnts[i]; in reduceDB() 887 learnts.shrink(i - j); in reduceDB() 940 removeSatisfied(learnts); in simplify() 995 learnts.push(cr); in search() 1206 Debug("bvminisat") <<"BVMinisat::Solving learned clauses " << learnts.size() <<"\n"; in solve_() 1436 for (int i = 0; i < learnts.size(); i++) in relocAll() [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/ |
H A D | satSolver3.c | 552 s->stats.learnts++; in sat_solver3_clause_new() 1168 s->stats.learnts = 0; in sat_solver3_new() 1233 s->stats.learnts = 0; in zsat_solver3_new_seed() 1393 s->stats.learnts = 0; in sat_solver3_restart() 1436 s->stats.learnts = 0; in zsat_solver3_restart_seed() 1544 s->stats.learnts--; in sat_solver3_reducedb() 1547 assert( s->stats.learnts == (unsigned)j ); in sat_solver3_reducedb() 1599 s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld ); in sat_solver3_reducedb() 1656 s->stats.learnts = pMem->BookMarkE[1]; in sat_solver3_rollback() 1686 s->stats.learnts = 0; in sat_solver3_rollback() [all …]
|
H A D | satSolver.c | 569 s->stats.learnts++; in sat_solver_clause_new() 1194 s->stats.learnts = 0; in sat_solver_new() 1259 s->stats.learnts = 0; in zsat_solver_new_seed() 1428 s->stats.learnts = 0; in sat_solver_restart() 1471 s->stats.learnts = 0; in zsat_solver_restart_seed() 1579 s->stats.learnts--; in sat_solver_reducedb() 1582 assert( s->stats.learnts == (unsigned)j ); in sat_solver_reducedb() 1634 s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld ); in sat_solver_reducedb() 1691 s->stats.learnts = pMem->BookMarkE[1]; in sat_solver_rollback() 1721 s->stats.learnts = 0; in sat_solver_rollback() [all …]
|