Searched refs:num_prob_literals (Results 1 – 14 of 14) sorted by relevance
/dports/math/yices/yices-2.6.2/src/solvers/cdcl/ |
H A D | clause_pool.c | 124 prob_lits == pool->num_prob_literals && in good_statistics() 150 pool->num_prob_literals = 0; in init_clause_pool() 184 pool->num_prob_literals = 0; in reset_clause_pool() 283 pool->num_prob_literals += n; in clause_pool_add_problem_clause() 386 assert(pool->num_prob_literals >= n); in clause_pool_delete_clause() 388 pool->num_prob_literals -= n; in clause_pool_delete_clause() 422 assert(pool->num_prob_literals >= old_n); in clause_pool_shrink_clause() 423 pool->num_prob_literals -= (old_n - n); in clause_pool_shrink_clause()
|
H A D | clause_pool.h | 99 uint32_t num_prob_literals; // sum of the length of these clauses member
|
H A D | new_sat_solver2.h | 242 uint32_t num_prob_literals; // sum of the length of these clauses member
|
H A D | new_sat_solver.h | 242 uint32_t num_prob_literals; // sum of the length of these clauses member
|
H A D | new_sat_solver2.c | 762 pool->num_prob_literals = 0; in init_clause_pool() 790 pool->num_prob_literals = 0; in reset_clause_pool() 887 pool->num_prob_literals += n; in clause_pool_add_problem_clause() 1174 assert(pool->num_prob_literals >= n); in clause_pool_delete_clause() 1176 pool->num_prob_literals -= n; in clause_pool_delete_clause() 1207 assert(pool->num_prob_literals >= old_n); in clause_pool_shrink_clause() 1208 pool->num_prob_literals -= (old_n - n); in clause_pool_shrink_clause() 4307 solver->pool.num_prob_clauses, solver->pool.num_prob_literals, in simplify_clause_database() 7238 pool->num_prob_literals = 0; in pp_rebuild_watch_vectors() 7262 pool->num_prob_literals += n; in pp_rebuild_watch_vectors() [all …]
|
H A D | new_sat_solver.c | 791 pool->num_prob_literals = 0; in init_clause_pool() 819 pool->num_prob_literals = 0; in reset_clause_pool() 916 pool->num_prob_literals += n; in clause_pool_add_problem_clause() 1203 assert(pool->num_prob_literals >= n); in clause_pool_delete_clause() 1205 pool->num_prob_literals -= n; in clause_pool_delete_clause() 1236 assert(pool->num_prob_literals >= old_n); in clause_pool_shrink_clause() 1237 pool->num_prob_literals -= (old_n - n); in clause_pool_shrink_clause() 4674 solver->pool.num_prob_clauses, solver->pool.num_prob_literals, in simplify_clause_database() 8208 pool->num_prob_literals = 0; in pp_rebuild_watch_vectors() 8232 pool->num_prob_literals += n; in pp_rebuild_watch_vectors() [all …]
|
H A D | smt_core.h | 1350 static inline uint64_t num_prob_literals(smt_core_t *s) { in num_prob_literals() function
|
/dports/math/yices/yices-2.6.2/tests/unit/ |
H A D | test_pool_alloc.c | 271 fprintf(f, " prob literals : %"PRIu32"\n", pool.num_prob_literals); in print_statistics()
|
H A D | test_core3.c | 216 num_prob_clauses(core), num_prob_literals(core), in show_progress()
|
H A D | test_core2.c | 201 num_prob_clauses(core), num_prob_literals(core), in show_progress()
|
/dports/math/yices/yices-2.6.2/src/context/ |
H A D | context_solver.c | 56 num_binary_clauses(core), num_prob_clauses(core), num_prob_literals(core), in trace_stats() 62 num_binary_clauses(core), num_prob_clauses(core), num_prob_literals(core), in trace_stats()
|
/dports/math/yices/yices-2.6.2/src/frontend/ |
H A D | yices_sat_new.c | 998 write_line_and_uint(2, "c lits in pb. clauses : ", solver->pool.num_prob_literals); in show_stats()
|
/dports/math/yices/yices-2.6.2/src/solvers/bv/ |
H A D | new_bvsolver.c | 1802 printf("num. clause literals: %"PRIu64"\n\n", num_prob_literals(solver->core)); in bv_solver_bitblast()
|
H A D | bvsolver.c | 1895 printf("num. clause literals: %"PRIu64"\n\n", num_prob_literals(solver->core)); in bv_solver_bitblast()
|