Searched refs:m_final_check_idx (Results 1 – 12 of 12) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | theory_array.h | 54 unsigned m_final_check_idx; variable
67 void init_search_eh() override { m_final_check_idx = 0; } in init_search_eh()
|
| H A D | theory_array.cpp | 32 m_final_check_idx(0) { in theory_array()
360 m_final_check_idx++; in final_check_eh()
367 if (m_final_check_idx % m_params.m_array_lazy_ieq_delay != 0) { in final_check_eh()
379 if (m_final_check_idx % 2 == 1) { in final_check_eh()
|
| H A D | theory_arith_core.h | 1428 m_final_check_idx = 0; in init_search_eh()
1436 unsigned old_idx = m_final_check_idx; in final_check_core()
1446 …TRACE("arith", tout << "m_final_check_idx: " << m_final_check_idx << ", result: " << result << "\n… in final_check_core()
1447 switch (m_final_check_idx) { in final_check_core()
1464 m_final_check_idx = (m_final_check_idx + 1) % 3; in final_check_core()
1478 while (m_final_check_idx != old_idx); in final_check_core()
1495 ctx.push_trail(value_trail<unsigned>(m_final_check_idx)); in final_check_eh()
1691 m_final_check_idx(0), in theory_arith()
|
| H A D | smt_context.cpp | 69 m_final_check_idx(0), in context()
3613 m_final_check_idx = 0; in init_search()
3921 unsigned old_idx = m_final_check_idx; in final_check()
3928 …TRACE("final_check_step", tout << "processing: " << m_final_check_idx << ", result: " << result <<… in final_check()
3930 if (m_final_check_idx < num_th) { in final_check()
3931 theory * th = m_theory_set[m_final_check_idx]; in final_check()
3945 m_final_check_idx = (m_final_check_idx + 1) % range; in final_check()
3959 while (m_final_check_idx != old_idx); in final_check()
|
| H A D | theory_arith.h | 485 unsigned m_final_check_idx; variable
|
| H A D | smt_context.h | 110 … unsigned m_final_check_idx; // circular counter used for implementing fairness variable
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | theory_array.h | 55 unsigned m_final_check_idx; variable
68 void init_search_eh() override { m_final_check_idx = 0; } in init_search_eh()
|
| H A D | theory_array.cpp | 32 m_final_check_idx(0) { in theory_array()
360 m_final_check_idx++; in final_check_eh()
367 if (m_final_check_idx % m_params.m_array_lazy_ieq_delay != 0) { in final_check_eh()
379 if (m_final_check_idx % 2 == 1) { in final_check_eh()
|
| H A D | theory_arith_core.h | 1428 m_final_check_idx = 0; in init_search_eh()
1436 unsigned old_idx = m_final_check_idx; in final_check_core()
1446 …TRACE("arith", tout << "m_final_check_idx: " << m_final_check_idx << ", result: " << result << "\n… in final_check_core()
1447 switch (m_final_check_idx) { in final_check_core()
1464 m_final_check_idx = (m_final_check_idx + 1) % 3; in final_check_core()
1478 while (m_final_check_idx != old_idx); in final_check_core()
1495 ctx.push_trail(value_trail<context, unsigned>(m_final_check_idx)); in final_check_eh()
1691 m_final_check_idx(0), in theory_arith()
|
| H A D | smt_context.cpp | 68 m_final_check_idx(0), in context()
3623 m_final_check_idx = 0; in init_search()
3931 unsigned old_idx = m_final_check_idx; in final_check()
3938 …TRACE("final_check_step", tout << "processing: " << m_final_check_idx << ", result: " << result <<… in final_check()
3940 if (m_final_check_idx < num_th) { in final_check()
3941 theory * th = m_theory_set[m_final_check_idx]; in final_check()
3955 m_final_check_idx = (m_final_check_idx + 1) % range; in final_check()
3969 while (m_final_check_idx != old_idx); in final_check()
|
| H A D | theory_arith.h | 485 unsigned m_final_check_idx; variable
|
| H A D | smt_context.h | 111 … unsigned m_final_check_idx; // circular counter used for implementing fairness variable
|