| /dports/textproc/link-grammar/link-grammar-5.8.0/link-grammar/minisat/minisat/core/ |
| H A D | Solver.cc | 163 if (value(ps[i]) == l_True || ps[i] == ~p) in addClause_()
224 if (value(c[i]) == l_True) in satisfied()
271 return mkLit(next, user_pol[next] == l_True); in pickBranchLit()
520 if (value(blocker) == l_True){ in propagate()
535 if (first != blocker && value(first) == l_True){ in propagate()
766 if (value(p) == l_True){ in search()
785 return l_True; in search()
875 if (status == l_True){ in solve_()
|
| /dports/math/vampire/vampire-4.5.1/Minisat/core/ |
| H A D | Solver.cc | 168 if (value(ps[i]) == l_True || ps[i] == ~p) in addClause_()
229 if (value(c[i]) == l_True) in satisfied()
276 return mkLit(next, user_pol[next] == l_True); in pickBranchLit()
525 if (value(blocker) == l_True){ in propagate()
540 if (first != blocker && value(first) == l_True){ in propagate()
773 if (value(p) == l_True){ in search()
792 return l_True; in search()
882 if (status == l_True){ in solve_()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/ |
| H A D | Solver.cpp | 141 if (value(ps[i]) == l_True || ps[i] == ~p) in addClause_()
200 if (value(c[i]) == l_True) in satisfied()
464 if (value(blocker) == l_True){ in propagate()
479 if (first != blocker && value(first) == l_True){ in propagate()
678 if (value(p) == l_True){ in search()
697 return l_True; in search()
784 if (status == l_True){ in solve_()
|
| H A D | SimpSolver.cpp | 96 lbool result = l_True; in solve_()
117 if (result == l_True) in solve_()
122 if (result == l_True) in solve_()
312 if (value(c[i]) == l_True){ in implied()
357 …assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated befo… in backwardSubsumptionCheck()
|
| /dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | completedetachreattacher.cpp | 114 if (solver->value(lit) == l_True) {
178 if (solver->value(*i) == l_True) {
|
| H A D | solver.cpp | 346 if (value(ps[i]) == l_True) { in sort_and_clean_clause()
1671 if (status == l_True) { in solve_with_assumptions()
1935 if (status == l_True) { in handle_found_solution()
2078 if (ret == l_True) { in execute_inprocess_strategy()
2222 assert(ret != l_True); in simplify_problem()
2996 if (value(lit) == l_True in check_implicit_propagated()
3008 if (val2 != l_True) { in check_implicit_propagated()
3014 assert(val2 == l_True); in check_implicit_propagated()
3557 status = l_True; in load_solution_from_file()
4149 if (value(inter) != l_True) { in check_assigns_for_assumptions()
[all …]
|
| H A D | propengine.cpp | 208 if (value(i->getBlockedLit()) == l_True) { in prop_long_cl_any_order()
331 if (likely(value(blocked) == l_True)) { in propagate_any_order_fast()
347 if (first != blocked && value(first) == l_True) { in propagate_any_order_fast()
599 if (val == l_True) { in propagate_long_clause_occur()
|
| H A D | propengine.h | 312 return ((value(bin.getLit1()) == l_True) in satisfied()
313 || (value(bin.getLit2()) == l_True)); in satisfied()
352 if (value(c[0]) == l_True) { in prop_normal_helper()
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | completedetachreattacher.cpp | 114 if (solver->value(lit) == l_True) { in attachClauses()
178 if (solver->value(*i) == l_True) { in clean_clause()
|
| H A D | solver.cpp | 346 if (value(ps[i]) == l_True) { in sort_and_clean_clause()
1671 if (status == l_True) { in solve_with_assumptions()
1935 if (status == l_True) { in handle_found_solution()
2078 if (ret == l_True) { in execute_inprocess_strategy()
2222 assert(ret != l_True); in simplify_problem()
2996 if (value(lit) == l_True in check_implicit_propagated()
3008 if (val2 != l_True) { in check_implicit_propagated()
3014 assert(val2 == l_True); in check_implicit_propagated()
3557 status = l_True; in load_solution_from_file()
4149 if (value(inter) != l_True) { in check_assigns_for_assumptions()
[all …]
|
| H A D | propengine.cpp | 208 if (value(i->getBlockedLit()) == l_True) { in prop_long_cl_any_order()
331 if (likely(value(blocked) == l_True)) { in propagate_any_order_fast()
347 if (first != blocked && value(first) == l_True) { in propagate_any_order_fast()
599 if (val == l_True) { in propagate_long_clause_occur()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bmc/ |
| H A D | bmcGen.c | 171 printf( "%c", status == l_True ? '+' : '-' ); in Gia_ManTestSatEnum()
172 if ( status == l_True ) in Gia_ManTestSatEnum()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/ |
| H A D | Solver.cc | 245 Lit l = mkLit(x, value(x) != l_True); in reason()
540 if (value(c[i]) == l_True) in satisfied()
671 Assert(dec_pol == l_True || dec_pol == l_False); in pickBranchLit()
672 return mkLit(next, (dec_pol == l_True) ); in pickBranchLit()
1085 if (value(blocker) == l_True){ in propagateBool()
1100 if (first != blocker && value(first) == l_True){ in propagateBool()
1346 return l_True; in search()
1378 if (value(p) == l_True) { in search()
1503 if (status == l_True){ in solve_()
1753 if (value(lemma[0]) != l_True || level(var(lemma[0])) > currentBacktrackLevel) { in updateLemmas()
[all …]
|
| /dports/math/glucose/glucose-syrup-4.1/parallel/ |
| H A D | ParallelSolver.cc | 439 lbool result = l_True; in solve_()
489 …cose! First thread to finish! (%s answer).\n", threadNumber(), status == l_True ? "SAT" : status =… in solve_()
493 if (firstToFinish && status == l_True) { in solve_()
|
| /dports/net-mgmt/icinga2/icinga2-2.13.2/lib/base/ |
| H A D | json.cpp | 49 const char l_True[] = "true"; variable
359 AppendChars((const char*)l_True, (const char*)l_True + 4); in Boolean()
|
| /dports/cad/yosys/yosys-yosys-0.12/libs/minisat/ |
| H A D | SimpSolver.cc | 115 lbool result = l_True; in solve_()
136 if (result == l_True) in solve_()
141 if (result == l_True && extend_model) in solve_()
332 if (value(c[i]) == l_True){ in implied()
377 …assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated befo… in backwardSubsumptionCheck()
|
| /dports/math/ogdf/OGDF/src/ogdf/lib/minisat/simp/ |
| H A D | SimpSolver.cpp | 94 lbool result = l_True; in solve_()
115 if (result == l_True) in solve_()
120 if (result == l_True) in solve_()
313 if (value(c[i]) == l_True){ in implied()
358 …assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated befo… in backwardSubsumptionCheck()
|
| /dports/math/minisat/minisat-2.2.1/minisat/simp/ |
| H A D | SimpSolver.cc | 109 lbool result = l_True; in solve_()
130 if (result == l_True) in solve_()
135 if (result == l_True && extend_model) in solve_()
326 if (value(c[i]) == l_True){ in implied()
371 …assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated befo… in backwardSubsumptionCheck()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
| H A D | AbcGlucose.cpp | 110 return (res == l_True ? 1 : res == l_False ? -1 : 0); in glucose_solver_solve()
121 return S->model[ivar] == l_True; in glucose_solver_read_cex_varvalue()
377 return (res == l_True ? 1 : res == l_False ? -1 : 0); in glucose_solver_solve()
388 return S->model[ivar] == l_True; in glucose_solver_read_cex_varvalue()
686 printf(ret == l_True ? "SATISFIABLE" : ret == l_False ? "UNSATISFIABLE" : "INDETERMINATE"); in Glucose_SolveCnf()
1346 printf(ret == l_True ? "SATISFIABLE" : ret == l_False ? "UNSATISFIABLE" : "INDETERMINATE"); in Glucose_SolveAig()
1350 if (ret == l_True) in Glucose_SolveAig()
1357 if (S.model[Vec_IntEntry(vCnfIds,Gia_ObjId(p, pObj))] == l_True) in Glucose_SolveAig()
1362 return (ret == l_True ? 10 : ret == l_False ? 20 : 0); in Glucose_SolveAig()
|
| H A D | SimpSolver.cpp | 99 lbool result = l_True; in solve_()
120 if (result == l_True) in solve_()
125 if (result == l_True) in solve_()
335 if (value(c[i]) == l_True){ in implied()
380 …assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated befo… in backwardSubsumptionCheck()
|
| /dports/math/chuffed/chuffed-e04bedd/chuffed/parallel/ |
| H A D | slave.cpp | 222 if (sat.value(x) != l_True || sat.level[var(x)] != 0) { in receiveLearnts()
299 if (value(c[0]) != l_True || level[var(c[0])] > hlevel) { in addLearnt()
306 …assert(value(c[0]) == l_True || (value(c[0]) != l_False && value(c[1]) != l_False) || enqueue_firs… in addLearnt()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/int2/ |
| H A D | int2Bmc.c | 113 …olve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ) == l_True ) in Int2_ManCheckInit()
335 if ( status == l_True ) in Int2_ManCheckBmc()
344 if ( status == l_True ) in Int2_ManCheckBmc()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/minisat/simp/ |
| H A D | SimpSolver.cc | 126 lbool result = l_True; in solve_()
147 if (result == l_True) in solve_()
152 if (result == l_True) in solve_()
356 if (value(c[i]) == l_True){ in implied()
401 …assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated befo… in backwardSubsumptionCheck()
|
| /dports/math/vampire/vampire-4.5.1/Minisat/simp/ |
| H A D | SimpSolver.cc | 126 lbool result = l_True; in solve_()
147 if (result == l_True) in solve_()
152 if (result == l_True && extend_model) in solve_()
405 if (value(c[i]) == l_True){ in implied()
454 …assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated befo… in backwardSubsumptionCheck()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
| H A D | Solver.cc | 215 if (value(ps[i]) == l_True || ps[i] == ~p) { in addClause_()
346 if (value(c[i]) == l_True) in satisfied()
773 return l_True; in assertAssumption()
811 if (value(blocker) == l_True){ in propagate()
826 if (first != blocker && value(first) == l_True){ in propagate()
1117 if (value(p) == l_True){ in search()
1139 return l_True; in search()
1149 return l_True; in search()
1242 if (status == l_True){ in solve_()
|