Searched refs:reduce_calls (Results 1 – 17 of 17) sorted by relevance
| /dports/math/yices/yices-2.6.2/src/solvers/cdcl/ |
| H A D | smt_core.h | 781 uint32_t reduce_calls; // number of calls to reduce_learned_clause_set member
1299 return s->stats.reduce_calls; in num_reduce_calls()
|
| H A D | sat_solver.h | 486 uint32_t reduce_calls; // number of calls to reduce_learned_clause_set member
|
| H A D | new_sat_solver2.h | 520 uint32_t reduce_calls; // number of calls to reduce_learned_clause_set member
|
| H A D | new_sat_solver.h | 578 uint32_t reduce_calls; // number of calls to reduce_learned_clause_set member
|
| H A D | sat_solver.c | 954 stat->reduce_calls = 0; in init_stats()
1638 solver->stats.reduce_calls ++; in reduce_learned_clause_set()
|
| H A D | smt_core.c | 1275 stat->reduce_calls = 0; in init_statistics()
4659 s->stats.reduce_calls ++; in reduce_clause_database()
5880 s->stats.reduce_calls = 0; in start_search()
|
| H A D | new_sat_solver2.c | 2406 stat->reduce_calls = 0; in init_stats()
4088 solver->stats.reduce_calls ++; in nsat_reduce_learned_clause_set()
9218 fprintf(f, "c reduce db : %"PRIu32"\n", stat->reduce_calls); in nsat_show_statistics()
|
| H A D | new_sat_solver.c | 2758 stat->reduce_calls = 0; in init_stats()
4455 solver->stats.reduce_calls ++; in nsat_reduce_learned_clause_set()
11271 fprintf(f, "c reduce db : %"PRIu32"\n", stat->reduce_calls); in nsat_show_statistics()
|
| /dports/math/yices/yices-2.6.2/src/context/ |
| H A D | context_statistics.c | 46 fprintf(f, " reduce db : %"PRIu32"\n", stat->reduce_calls); in show_stats()
|
| /dports/math/yices/yices-2.6.2/src/frontend/ |
| H A D | yices_sat.c | 438 fprintf(stderr, "reduce db : %"PRIu32"\n", stat->reduce_calls); in show_stats()
|
| H A D | yices_sat_new.c | 984 write_line_and_uint(2, "c reduce db : ", stat->reduce_calls); in show_stats()
|
| H A D | yices_smtcomp.c | 563 fprintf(stderr, " reduce db : %"PRIu32"\n", stat->reduce_calls); in show_stats()
|
| H A D | yices_smt.c | 1074 printf(" reduce db : %"PRIu32"\n", stat->reduce_calls); in show_stats()
|
| /dports/math/yices/yices-2.6.2/tests/unit/ |
| H A D | test_core3.c | 511 printf("reduce db : %"PRIu32"\n", stat->reduce_calls); in show_stats()
|
| H A D | test_core2.c | 505 printf("reduce db : %"PRIu32"\n", stat->reduce_calls); in show_stats()
|
| H A D | test_bit_solver.c.old | 278 printf("reduce db : %"PRIu32"\n", stat->reduce_calls);
|
| /dports/math/yices/yices-2.6.2/src/frontend/yices/ |
| H A D | yices_reval.c | 1894 printf(" reduce db : %"PRIu32"\n", stat->reduce_calls); in show_stats()
|