Home
last modified time | relevance | path

Searched refs:learnts_literals (Results 1 – 25 of 38) sorted by relevance

12

/dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/
H A DSolver.C45 , 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 DSolver.h96 uint64_t clauses_literals, learnts_literals, max_literals, tot_literals; variable
/dports/math/chuffed/chuffed-e04bedd/chuffed/core/
H A Dsat.cpp82 , 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 Dsat.h114 long long int clauses_literals, learnts_literals, max_literals, tot_literals; variable
/dports/math/ogdf/OGDF/src/ogdf/lib/minisat/core/
H A DSolver.cpp81 , 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 DSolver.cpp81 , 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 DSolver.cc91 …, 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 DSolver.cc85 …, 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 DSolver.cc85 …, 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 DSolver.cc90 …, 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 Dminisat_solver.h164 int64_t clauses_literals, learnts_literals, max_literals, member
168 clauses_literals(0), learnts_literals(0), max_literals(0), in SolverStats()
H A Dminisat_solver.cpp232 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 Ddpllt_minisat.cpp99 << (solver->getStats().clauses_literals + solver->getStats().learnts_literals) << endl; in search()
/dports/math/igraph/igraph-0.9.5/vendor/glpk/minisat/
H A Dminisat.c397 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 Dminisat.h138 double clauses, clauses_literals, learnts, learnts_literals, member
/dports/math/glpk/glpk-5.0/src/minisat/
H A Dminisat.c397 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 Dminisat.h138 double clauses, clauses_literals, learnts, learnts_literals, member
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/
H A DsatSolver3.c553 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 DsatVec.h155 ABC_INT64_T clauses_literals, learnts_literals, tot_literals; member
H A DsatSolver.c570 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 DSolver.cc122 , 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 DSolver.h155 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 DSolver.cc134 , 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 DGlucose.cpp129 , 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 Dminisat.cpp276 d_statLearntsLiterals.setData(d_minisat->learnts_literals); in init()

12