Home
last modified time | relevance | path

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 Dclause_pool.c124 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 Dclause_pool.h99 uint32_t num_prob_literals; // sum of the length of these clauses member
H A Dnew_sat_solver2.h242 uint32_t num_prob_literals; // sum of the length of these clauses member
H A Dnew_sat_solver.h242 uint32_t num_prob_literals; // sum of the length of these clauses member
H A Dnew_sat_solver2.c762 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 Dnew_sat_solver.c791 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 Dsmt_core.h1350 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 Dtest_pool_alloc.c271 fprintf(f, " prob literals : %"PRIu32"\n", pool.num_prob_literals); in print_statistics()
H A Dtest_core3.c216 num_prob_clauses(core), num_prob_literals(core), in show_progress()
H A Dtest_core2.c201 num_prob_clauses(core), num_prob_literals(core), in show_progress()
/dports/math/yices/yices-2.6.2/src/context/
H A Dcontext_solver.c56 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 Dyices_sat_new.c998 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 Dnew_bvsolver.c1802 printf("num. clause literals: %"PRIu64"\n\n", num_prob_literals(solver->core)); in bv_solver_bitblast()
H A Dbvsolver.c1895 printf("num. clause literals: %"PRIu64"\n\n", num_prob_literals(solver->core)); in bv_solver_bitblast()