| /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
347 inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() ==… in nFreeVars()
351 if ( b && !decision[v]) dec_vars++; in setDecisionVar()
352 else if (!b && decision[v]) dec_vars--; in setDecisionVar()
378 uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; in solve()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/ |
| H A D | Solver.h | 139 uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; variable
329 inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() ==… in nFreeVars()
333 if ( b && !decision[v]) dec_vars++; in setDecisionVar()
334 else if (!b && decision[v]) dec_vars--; in setDecisionVar()
|
| H A D | Solver.cpp | 81 , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) in Solver()
654 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search()
|
| /dports/cad/yosys/yosys-yosys-0.12/libs/minisat/ |
| H A D | Solver.h | 152 …uint64_t dec_vars, num_clauses, num_learnts, clauses_literals, learnts_literals, max_literals, tot… variable
359 inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() ==… in nFreeVars()
363 if ( b && !decision[v]) dec_vars++; in setDecisionVar()
364 else if (!b && decision[v]) dec_vars--; in setDecisionVar()
|
| 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()
748 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search()
|
| /dports/math/minisat/minisat-2.2.1/minisat/core/ |
| H A D | Solver.h | 152 …uint64_t dec_vars, num_clauses, num_learnts, clauses_literals, learnts_literals, max_literals, tot… variable
359 inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() ==… in nFreeVars()
363 if ( b && !decision[v]) dec_vars++; in setDecisionVar()
364 else if (!b && decision[v]) dec_vars--; in setDecisionVar()
|
| 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()
742 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search()
|
| /dports/textproc/link-grammar/link-grammar-5.8.0/link-grammar/minisat/minisat/core/ |
| H A D | Solver.h | 152 …uint64_t dec_vars, num_clauses, num_learnts, clauses_literals, learnts_literals, max_literals, tot… variable
359 inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() ==… in nFreeVars()
363 if ( b && !decision[v]) dec_vars++; in setDecisionVar()
364 else if (!b && decision[v]) dec_vars--; in setDecisionVar()
|
| 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()
742 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search()
|
| /dports/math/vampire/vampire-4.5.1/Minisat/core/ |
| H A D | Solver.h | 158 …uint64_t dec_vars, num_clauses, num_learnts, clauses_literals, learnts_literals, max_literals, tot… variable
365 inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() ==… in nFreeVars()
370 if ( b && !decision[v]) dec_vars++; in setDecisionVar()
371 else if (!b && decision[v]) dec_vars--; in setDecisionVar()
|
| 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()
747 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
| H A D | Solver.h | 207 uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; variable
452 inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() ==… in nFreeVars()
456 if ( b && !decision[v]) dec_vars++; in setDecisionVar()
457 else if (!b && decision[v]) dec_vars--; in setDecisionVar()
|
| H A D | Solver.cc | 122 , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) in Solver()
1071 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
| H A D | Solver.h | 188 int64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; variable
420 inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() ==… in nFreeVars()
424 if ( b && !decision[v]) dec_vars++; in setDecisionVar()
425 else if (!b && decision[v]) dec_vars--; in setDecisionVar()
|
| H A D | Glucose.cpp | 129 , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) in Solver()
1058 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search()
|
| /dports/math/glucose/glucose-syrup-4.1/core/ |
| H A D | Solver.h | 85 dec_vars, enumerator
531 int a = stats[dec_vars]; in nFreeVars()
536 if ( b && !decision[v]) stats[dec_vars]++; in setDecisionVar()
537 else if (!b && decision[v]) stats[dec_vars]--; in setDecisionVar()
|
| H A D | Solver.cc | 1504 …(int) stats[dec_vars] - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int) s… in search()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/ |
| H A D | Solver.h | 277 uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; variable
535 inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() ==… in nFreeVars()
541 if ( b && !decision[v] ) dec_vars++; in setDecisionVar()
542 else if (!b && decision[v] ) dec_vars--; in setDecisionVar()
|
| H A D | Solver.cc | 134 , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) in Solver()
1321 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search()
|
| /dports/math/ogdf/OGDF/src/ogdf/external/ |
| H A D | Minisat.cpp | 149 Solver::dec_vars = 0; in reset()
|
| /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()
656 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search()
754 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search()
|