Searched refs:clause_pool_add_problem_clause (Results 1 – 5 of 5) sorted by relevance
| /dports/math/yices/yices-2.6.2/src/solvers/cdcl/ |
| H A D | clause_pool.h | 150 extern cidx_t clause_pool_add_problem_clause(clause_pool_t *pool, uint32_t n, const literal_t *a);
|
| H A D | clause_pool.c | 274 cidx_t clause_pool_add_problem_clause(clause_pool_t *pool, uint32_t n, const literal_t *a) { in clause_pool_add_problem_clause() function
|
| H A D | new_sat_solver2.c | 878 static cidx_t clause_pool_add_problem_clause(clause_pool_t *pool, uint32_t n, const literal_t *a) { in clause_pool_add_problem_clause() function
3360 cidx = clause_pool_add_problem_clause(&solver->pool, n, lit); in add_large_clause()
6189 cidx = clause_pool_add_problem_clause(&solver->pool, n, (literal_t *) b->data); in pp_apply_subst_to_clause()
6984 cidx = clause_pool_add_problem_clause(&solver->pool, n, (literal_t *) b->data); in pp_add_resolvent()
|
| H A D | new_sat_solver.c | 907 static cidx_t clause_pool_add_problem_clause(clause_pool_t *pool, uint32_t n, const literal_t *a) { in clause_pool_add_problem_clause() function
3728 cidx = clause_pool_add_problem_clause(&solver->pool, n, lit); in add_large_clause()
7033 new_cidx = clause_pool_add_problem_clause(&solver->pool, n, (literal_t *) b->data); in pp_apply_subst_to_clause()
7866 cidx = clause_pool_add_problem_clause(&solver->pool, n, (literal_t *) b->data); in pp_add_resolvent()
|
| /dports/math/yices/yices-2.6.2/tests/unit/ |
| H A D | test_pool_alloc.c | 250 (void) clause_pool_add_problem_clause(&pool, j, clause); in build_instance()
|