Home
last modified time | relevance | path

Searched refs:nb_clauses (Results 1 – 8 of 8) sorted by relevance

/dports/math/yices/yices-2.6.2/src/solvers/cdcl/
H A Dsat_solver.c987 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 Dsat_solver.h540 uint32_t nb_clauses; // Number of clauses with at least 3 literals member
H A Dsmt_core.c1496 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 Dsmt_core.h961 …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 Dyices_sat.c494 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 Dpycryptosat.cpp.in655 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 Dpycryptosat.cpp.in655 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 Dtest_bit_solver.c.old346 fprintf(f, "nb. of big clauses : %"PRIu32"\n", sol->nb_clauses);