| /dports/math/boolector/boolector-3.2.2/src/ |
| H A D | btormc.h | 89 BoolectorNodePtrStack init_assumptions; member
|
| H A D | btormc.c | 243 BTOR_INIT_STACK (mm, res->init_assumptions); in btor_mc_new()
337 while (mc->forward && !BTOR_EMPTY_STACK (mc->init_assumptions)) in btor_mc_delete()
338 boolector_release (mc->forward, BTOR_POP_STACK (mc->init_assumptions)); in btor_mc_delete()
339 BTOR_RELEASE_STACK (mc->init_assumptions); in btor_mc_delete()
867 BTOR_PUSH_STACK (mc->init_assumptions, in initialize_states_of_frame()
1378 for (j = 0; j < BTOR_COUNT_STACK (mc->init_assumptions); j++) in check_last_forward_frame()
1381 boolector_assume (mc->forward, BTOR_PEEK_STACK (mc->init_assumptions, j)); in check_last_forward_frame()
|
| /dports/math/z3/z3-z3-4.8.13/src/qe/ |
| H A D | nlqsat.cpp | 268 init_assumptions(); in check_sat()
288 void init_assumptions() { in init_assumptions() function in qe::nlqsat
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/qe/ |
| H A D | nlqsat.cpp | 268 init_assumptions(); in check_sat()
288 void init_assumptions() { in init_assumptions() function in qe::nlqsat
|
| /dports/math/z3/z3-z3-4.8.13/src/sat/ |
| H A D | sat_solver.cpp | 1317 init_assumptions(num_lits, lits); in check()
1787 void solver::init_assumptions(unsigned num_lits, literal const* lits) { in init_assumptions() function in sat::solver
4387 init_assumptions(1, &lit); in get_bounded_consequences()
4390 init_assumptions(asms.size(), asms.data()); in get_bounded_consequences()
4446 init_assumptions(1, &lit); in get_consequences()
4449 init_assumptions(asms.size(), asms.data()); in get_consequences()
|
| H A D | sat_solver.h | 549 void init_assumptions(unsigned num_lits, literal const* lits);
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/ |
| H A D | sat_solver.cpp | 1310 init_assumptions(num_lits, lits);
1762 void solver::init_assumptions(unsigned num_lits, literal const* lits) {
4335 init_assumptions(1, &lit);
4338 init_assumptions(asms.size(), asms.c_ptr());
4394 init_assumptions(1, &lit);
4397 init_assumptions(asms.size(), asms.c_ptr());
|
| H A D | sat_solver.h | 507 void init_assumptions(unsigned num_lits, literal const* lits);
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | smt_consequences.cpp | 374 init_assumptions(assumptions); in get_consequences()
|
| H A D | smt_context.cpp | 3264 void context::init_assumptions(expr_ref_vector const& asms) { in init_assumptions() function in smt::context
3562 init_assumptions(asms); in check()
3584 init_assumptions(asms); in check()
|
| H A D | smt_context.h | 1200 void init_assumptions(expr_ref_vector const& asms);
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | smt_consequences.cpp | 374 init_assumptions(assumptions); in get_consequences()
|
| H A D | smt_context.cpp | 3274 void context::init_assumptions(expr_ref_vector const& asms) { in init_assumptions() function in smt::context
3572 init_assumptions(asms); in check()
3594 init_assumptions(asms); in check()
|
| H A D | smt_context.h | 1194 void init_assumptions(expr_ref_vector const& asms);
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/fd_solver/ |
| H A D | smtfd_solver.cpp | 1666 init_assumptions(num_assumptions, assumptions, asms); in check_abs()
1789 void init_assumptions(unsigned sz, expr* const* user_asms, expr_ref_vector& asms) { in init_assumptions() function in smtfd::solver
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/fd_solver/ |
| H A D | smtfd_solver.cpp | 1664 init_assumptions(num_assumptions, assumptions, asms);
1787 void init_assumptions(unsigned sz, expr* const* user_asms, expr_ref_vector& asms) {
|