Searched refs:clause_is_locked (Results 1 – 4 of 4) sorted by relevance
| /dports/math/yices/yices-2.6.2/src/solvers/cdcl/ |
| H A D | smt_core.c | 4579 static bool clause_is_locked(smt_core_t *s, clause_t *cl) { in clause_is_locked() function
4648 if (get_activity(v[i]) <= act_threshold && ! clause_is_locked(s, v[i])) { in reduce_clause_database()
4653 if (! clause_is_locked(s, v[i])) { in reduce_clause_database()
4711 if (! clause_is_locked(s, cl)) { in remove_irrelevant_learned_clauses()
4842 ! clause_is_locked(s, v[i])) { in simplify_clause_set()
4856 if (! clause_is_locked(s, v[i])) { in simplify_clause_set()
4873 ! clause_is_locked(s, v[i])) { in simplify_clause_set()
4886 if (! clause_is_locked(s, v[i])) { in simplify_clause_set()
5621 assert(! clause_is_locked(s, cl)); in mark_clause_to_remove()
|
| H A D | sat_solver.c | 1550 static bool clause_is_locked(sat_solver_t *solver, clause_t *cl) { in clause_is_locked() function
1624 if (! clause_is_locked(solver, v[i])) { in reduce_learned_clause_set()
1632 if (get_activity(v[i]) <= act_threshold && ! clause_is_locked(solver, v[i])) { in reduce_learned_clause_set()
|
| H A D | new_sat_solver2.c | 3981 static bool clause_is_locked(const sat_solver_t *solver, cidx_t cidx) { in clause_is_locked() function
4022 if (! clause_is_locked(solver, cidx) && in collect_learned_clauses()
9650 if (clause_is_locked(solver, c1)) { in check_candidate_clauses_to_delete()
|
| H A D | new_sat_solver.c | 4348 static bool clause_is_locked(const sat_solver_t *solver, cidx_t cidx) { in clause_is_locked() function
4389 if (! clause_is_locked(solver, cidx) && in collect_learned_clauses()
11940 if (clause_is_locked(solver, c1)) { in check_candidate_clauses_to_delete()
|