/dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/ |
H A D | Solver.C | 45 , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) in Solver() 150 if (c.learnt()) learnts_literals += c.size(); in attachClause() 160 if (c.learnt()) learnts_literals -= c.size(); in detachClause() 554 …simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but … in simplify() 726 …ses(), (int)clauses_literals, (int)nof_learnts, nLearnts(), (double)learnts_literals/nLearnts(), p… in solve()
|
H A D | Solver.h | 96 uint64_t clauses_literals, learnts_literals, max_literals, tot_literals; variable
|
/dports/math/chuffed/chuffed-e04bedd/chuffed/core/ |
H A D | sat.cpp | 82 , learnts_literals(0) in SAT() 233 if (c.learnt) learnts_literals += c.size(); in addClause() 264 if (c.learnt) learnts_literals -= c.size(); in removeClause() 314 next_simp_db = propagations + clauses_literals + learnts_literals; in simplifyDB() 567 …printf("%%%%%%mzn-stat: avgLearntClauseLen=%.2f\n", learnts.size() ? (double) learnts_literals / l… in printStats()
|
H A D | sat.h | 114 long long int clauses_literals, learnts_literals, max_literals, tot_literals; variable
|
/dports/math/ogdf/OGDF/src/ogdf/lib/minisat/core/ |
H A D | Solver.cpp | 81 , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) in Solver() 167 if (c.learnt()) learnts_literals += c.size(); in attachClause() 184 if (c.learnt()) learnts_literals -= c.size(); in detachClause() 597 …simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but … in simplify() 657 (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); in search() 755 … (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); in search()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/ |
H A D | Solver.cpp | 81 , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) in Solver() 167 if (c.learnt()) learnts_literals += c.size(); in attachClause() 184 if (c.learnt()) learnts_literals -= c.size(); in detachClause() 595 …simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but … in simplify() 655 …(int)max_learnts, nLearnts(), ((double)((int64_t)learnts_literals))/nLearnts(), progressEstimate()… in search()
|
/dports/cad/yosys/yosys-yosys-0.12/libs/minisat/ |
H A D | Solver.cc | 91 …, dec_vars(0), num_clauses(0), num_learnts(0), clauses_literals(0), learnts_literals(0), max_liter… in Solver() 195 if (c.learnt()) num_learnts++, learnts_literals += c.size(); in attachClause() 213 if (c.learnt()) num_learnts--, learnts_literals -= c.size(); in detachClause() 689 …simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but … in simplify() 749 … (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); in search()
|
/dports/math/minisat/minisat-2.2.1/minisat/core/ |
H A D | Solver.cc | 85 …, dec_vars(0), num_clauses(0), num_learnts(0), clauses_literals(0), learnts_literals(0), max_liter… in Solver() 189 if (c.learnt()) num_learnts++, learnts_literals += c.size(); in attachClause() 207 if (c.learnt()) num_learnts--, learnts_literals -= c.size(); in detachClause() 683 …simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but … in simplify() 743 … (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); in search()
|
/dports/textproc/link-grammar/link-grammar-5.8.0/link-grammar/minisat/minisat/core/ |
H A D | Solver.cc | 85 …, dec_vars(0), num_clauses(0), num_learnts(0), clauses_literals(0), learnts_literals(0), max_liter… in Solver() 189 if (c.learnt()) num_learnts++, learnts_literals += c.size(); in attachClause() 207 if (c.learnt()) num_learnts--, learnts_literals -= c.size(); in detachClause() 683 …simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but … in simplify() 743 … (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); in search()
|
/dports/math/vampire/vampire-4.5.1/Minisat/core/ |
H A D | Solver.cc | 90 …, dec_vars(0), num_clauses(0), num_learnts(0), clauses_literals(0), learnts_literals(0), max_liter… in Solver() 194 if (c.learnt()) num_learnts++, learnts_literals += c.size(); in attachClause() 212 if (c.learnt()) num_learnts--, learnts_literals -= c.size(); in detachClause() 688 …simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but … in simplify() 748 … (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); in search()
|
/dports/math/cvc3/cvc3-2.4.1/src/sat/ |
H A D | minisat_solver.h | 164 int64_t clauses_literals, learnts_literals, max_literals, member 168 clauses_literals(0), learnts_literals(0), max_literals(0), in SolverStats()
|
H A D | minisat_solver.cpp | 232 d_stats.learnts_literals += newLemma->size(); in insertLemma() 860 d_stats.learnts_literals += c->size(); in insertClause() 876 if (c->learnt()) d_stats.learnts_literals -= c->size(); in remove() 1933 d_simpDB_props = d_stats.clauses_literals + d_stats.learnts_literals; in simplifyDB() 2527 d_stats.learnts_literals -= lemma->size(); in push() 2731 d_stats.learnts_literals -= lemma->size(); in pop()
|
H A D | dpllt_minisat.cpp | 99 << (solver->getStats().clauses_literals + solver->getStats().learnts_literals) << endl; in search()
|
/dports/math/igraph/igraph-0.9.5/vendor/glpk/minisat/ |
H A D | minisat.c | 397 s->stats.learnts_literals -= clause_size(c); in clause_remove() 557 s->stats.learnts_literals += veci_size(cls); in solver_record() 1045 s->stats.learnts_literals = 0; in solver_new() 1175 + s->stats.learnts_literals); in solver_simplify() 1220 s->stats.learnts_literals / (double)s->stats.learnts; in solver_solve() 1230 (double)s->stats.learnts_literals, in solver_solve()
|
H A D | minisat.h | 138 double clauses, clauses_literals, learnts, learnts_literals, member
|
/dports/math/glpk/glpk-5.0/src/minisat/ |
H A D | minisat.c | 397 s->stats.learnts_literals -= clause_size(c); in clause_remove() 557 s->stats.learnts_literals += veci_size(cls); in solver_record() 1045 s->stats.learnts_literals = 0; in solver_new() 1175 + s->stats.learnts_literals); in solver_simplify() 1220 s->stats.learnts_literals / (double)s->stats.learnts; in solver_solve() 1230 (double)s->stats.learnts_literals, in solver_solve()
|
H A D | minisat.h | 138 double clauses, clauses_literals, learnts, learnts_literals, member
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/ |
H A D | satSolver3.c | 553 s->stats.learnts_literals += size; in sat_solver3_clause_new() 1169 s->stats.learnts_literals = 0; in sat_solver3_new() 1234 s->stats.learnts_literals = 0; in zsat_solver3_new_seed() 1394 s->stats.learnts_literals = 0; in sat_solver3_restart() 1437 s->stats.learnts_literals = 0; in zsat_solver3_restart_seed() 1543 s->stats.learnts_literals -= clause_size(c); in sat_solver3_reducedb() 1687 s->stats.learnts_literals = 0; in sat_solver3_rollback() 1913 s->stats.learnts_literals / (double)s->stats.learnts; in sat_solver3_solve_internal() 1924 (double)s->stats.learnts_literals, in sat_solver3_solve_internal()
|
H A D | satVec.h | 155 ABC_INT64_T clauses_literals, learnts_literals, tot_literals; member
|
H A D | satSolver.c | 570 s->stats.learnts_literals += size; in sat_solver_clause_new() 1195 s->stats.learnts_literals = 0; in sat_solver_new() 1260 s->stats.learnts_literals = 0; in zsat_solver_new_seed() 1429 s->stats.learnts_literals = 0; in sat_solver_restart() 1472 s->stats.learnts_literals = 0; in zsat_solver_restart_seed() 1578 s->stats.learnts_literals -= clause_size(c); in sat_solver_reducedb() 1722 s->stats.learnts_literals = 0; in sat_solver_rollback() 1957 s->stats.learnts_literals / (double)s->stats.learnts; in sat_solver_solve_internal() 1968 (double)s->stats.learnts_literals, in sat_solver_solve_internal()
|
/dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
H A D | Solver.cc | 122 , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) in Solver() 311 if (c.learnt()) learnts_literals += c.size(); in attachClause() 330 if (c.learnt()) learnts_literals -= c.size(); in detachClause() 947 …simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but … in simplify() 1072 … (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); in search()
|
/dports/math/ogdf/OGDF/include/ogdf/lib/minisat/core/ |
H A D | Solver.h | 155 uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; variable 378 uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; in solve()
|
/dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/ |
H A D | Solver.cc | 134 , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) in Solver() 503 if (c.removable()) learnts_literals += c.size(); in attachClause() 523 if (c.removable()) learnts_literals -= c.size(); in detachClause() 1236 …simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but … in simplify() 1322 … (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); in search()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
H A D | Glucose.cpp | 129 , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) in Solver() 300 if (c.learnt()) learnts_literals += c.size(); in attachClause() 329 if (c.learnt()) learnts_literals -= c.size(); in detachClause() 1019 …simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but … in simplify()
|
/dports/math/cvc4/CVC4-1.7/src/prop/minisat/ |
H A D | minisat.cpp | 276 d_statLearntsLiterals.setData(d_minisat->learnts_literals); in init()
|