Searched refs:m_consts (Results 1 – 14 of 14) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/math/lp/ |
| H A D | int_gcd_test.cpp | 118 m_consts = 0; in gcd_test_for_row()
129 m_consts += aux * lra.column_lower_bound(j).x; in gcd_test_for_row()
158 << " least_coeff: " << m_least_coeff << " consts: " << m_consts << "\n";); in gcd_test_for_row()
169 if (!(m_consts / gcds).is_int()) { in gcd_test_for_row()
190 mpq l(m_consts); in ext_gcd_test()
191 mpq u(m_consts); in ext_gcd_test()
284 mpq offset = m_consts / m_least_coeff; in accumulate_parity()
290 …TRACE("gcd_test", tout << least_idx << " modulus: " << modulus << " consts: " << m_consts << " sig… in accumulate_parity()
|
| H A D | int_gcd_test.h | 50 mpq m_consts; variable
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/transforms/ |
| H A D | dl_mk_elim_term_ite.cpp | 32 app_ref_vector& m_consts; member
34 …uninterp_const_collector(app_ref_vector &v, expr_ref_vector const& g) : m_consts(v), m_ground(g) {} in uninterp_const_collector()
40 m_consts.push_back(a); in operator ()()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/transforms/ |
| H A D | dl_mk_elim_term_ite.cpp | 32 app_ref_vector& m_consts; member
34 …uninterp_const_collector(app_ref_vector &v, expr_ref_vector const& g) : m_consts(v), m_ground(g) {} in uninterp_const_collector()
40 m_consts.push_back(a); in operator ()()
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | theory_array_full.cpp | 127 for (enode * n : d2->m_consts) { in set_prop_upward()
164 return d->m_stores.size() + 2*d2->m_consts.size() + 2*d2->m_maps.size(); in get_lambda_equiv_size()
173 ptr_vector<enode> & consts = m_var_data_full[v]->m_consts; in add_const()
217 display_ids(out, d->m_consts.size(), d->m_consts.data()); in display_var()
232 d->m_consts.push_back(n); in mk_var()
340 for (enode * n : d2->m_consts) { in merge_eh()
378 for (enode * n : d_full->m_consts) { in add_parent_select()
|
| H A D | theory_array_full.h | 29 ptr_vector<enode> m_consts; member
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | theory_array_full.cpp | 127 for (enode * n : d2->m_consts) { in set_prop_upward()
164 return d->m_stores.size() + 2*d2->m_consts.size() + 2*d2->m_maps.size(); in get_lambda_equiv_size()
173 ptr_vector<enode> & consts = m_var_data_full[v]->m_consts; in add_const()
217 display_ids(out, d->m_consts.size(), d->m_consts.c_ptr()); in display_var()
232 d->m_consts.push_back(n); in mk_var()
340 for (enode * n : d2->m_consts) { in merge_eh()
378 for (enode * n : d_full->m_consts) { in add_parent_select()
|
| H A D | theory_array_full.h | 29 ptr_vector<enode> m_consts; member
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/ |
| H A D | dl_util.h | 146 app_ref_vector m_consts; variable
155 variable_intersection(ast_manager & m) : m_consts(m) {} in variable_intersection()
182 m_consts.reset(); in reset()
|
| H A D | dl_util.cpp | 220 if(!values_match(f->get_arg(f_index), m_consts[i].get())) { in args_self_match()
255 m_consts.push_back(c1); in populate_self()
257 SASSERT(m_const_indexes.size()==m_consts.size()); in populate_self()
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/base/ |
| H A D | dl_util.h | 146 app_ref_vector m_consts; variable
155 variable_intersection(ast_manager & m) : m_consts(m) {} in variable_intersection()
182 m_consts.reset(); in reset()
|
| H A D | dl_util.cpp | 220 if(!values_match(f->get_arg(f_index), m_consts[i].get())) { in args_self_match()
255 m_consts.push_back(c1); in populate_self()
257 SASSERT(m_const_indexes.size()==m_consts.size()); in populate_self()
|
| /dports/cad/verilator/verilator-4.216/src/ |
| H A D | V3AstNodes.cpp | 1081 const auto& er = m_consts.equal_range(hash.value()); in findConst()
1096 m_consts.emplace(hash.value(), varScopep); in findConst()
|
| H A D | V3AstNodes.h | 9163 std::unordered_multimap<uint32_t, AstVarScope*> m_consts; // Constant tables (scalars) variable
|