Home
last modified time | relevance | path

Searched refs:learnts (Results 1 – 25 of 62) sorted by relevance

123

/dports/math/glucose/glucose-syrup-4.1/parallel/
H A DParallelSolver.cc159 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 Dsat.cpp104 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 DSolver.C66 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 DSolver.h127 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 Dminisat.c396 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 Dminisat.h138 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 Dminisat.c396 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 Dminisat.h138 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 DSolver.cc592 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 DSolver.cc586 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 DSolver.cc586 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 DSolver.cc591 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 DSolver.cc306 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 DSolver.cpp532 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 DSolver.cpp530 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 DSolver.h173 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 Dsolver_types.h67 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 Dsolver_types.h67 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 Dsolver_types.h67 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 DGlucose.cpp939 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 Dsolver_api.c100 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 Dsolver.c417 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 DSolver.cc877 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 DsatSolver3.c552 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 DsatSolver.c569 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 …]

123