Searched refs:nb_clauses (Results 1 – 8 of 8) sorted by relevance
/dports/math/yices/yices-2.6.2/src/solvers/cdcl/ |
H A D | sat_solver.c | 987 solver->nb_clauses = 0; in init_sat_solver() 1322 solver->nb_clauses ++; in add_clause_core() 1488 solver->nb_clauses ++; in add_learned_clause() 1595 solver->nb_clauses -= (n - j); in delete_learned_clauses() 1724 solver->nb_clauses -= n - j; in simplify_clause_set() 1740 solver->nb_clauses -= n - j; in simplify_clause_set() 3020 sol->reduce_threshold = sol->nb_clauses/4; in solve()
|
H A D | sat_solver.h | 540 uint32_t nb_clauses; // Number of clauses with at least 3 literals member
|
H A D | smt_core.c | 1496 s->nb_clauses = 0; in init_smt_core() 1724 s->nb_clauses = 0; in reset_smt_core() 2976 s->nb_clauses ++; in add_learned_clause() 3069 s->nb_clauses ++; in try_cache_theory_clause() 3932 s->nb_clauses ++; in new_problem_clause() 4619 s->nb_clauses -= (n - j); in delete_learned_clauses() 4917 s->nb_clauses -= n - j; in simplify_clause_set() 4937 s->nb_clauses -= n - j; in simplify_clause_set() 5227 s->nb_clauses = n; in restore_clauses() 5676 s->nb_clauses -= n - j; in remove_garbage_clauses() [all …]
|
H A D | smt_core.h | 961 …uint32_t nb_clauses; // Number of clauses with at least 3 literals (problem + learned claus… member
|
/dports/math/yices/yices-2.6.2/src/frontend/ |
H A D | yices_sat.c | 494 fprintf(f, "nb. of big clauses : %"PRIu32"\n", sol->nb_clauses); in print_solver_size()
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/python/src/ |
H A D | pycryptosat.cpp.in | 655 static PyObject* nb_clauses(Solver *self) 1037 …//{"nb_clauses", (PyCFunction) nb_clauses, METH_VARARGS | METH_KEYWORDS, "returns number of clause…
|
/dports/math/cryptominisat/cryptominisat-5.8.0/python/src/ |
H A D | pycryptosat.cpp.in | 655 static PyObject* nb_clauses(Solver *self) 1037 …//{"nb_clauses", (PyCFunction) nb_clauses, METH_VARARGS | METH_KEYWORDS, "returns number of clause…
|
/dports/math/yices/yices-2.6.2/tests/unit/ |
H A D | test_bit_solver.c.old | 346 fprintf(f, "nb. of big clauses : %"PRIu32"\n", sol->nb_clauses);
|