/dports/math/z3/z3-z3-4.8.13/src/muz/dataflow/ |
H A D | dataflow.h | 67 auto& value = m_body2rules.insert_if_not_there(d, nullptr); in init_bottom_up() 75 … bool new_info = m_facts.insert_if_not_there(sym, Fact()).init_up(m_context, cur); in init_bottom_up() 88 m_facts.insert_if_not_there(sym, Fact()).init_down(m_context, r); in init_top_down() 102 …bool new_info = m_facts.insert_if_not_there(head_sym, Fact()).propagate_up(m_context, r, tail_fact… in step_bottom_up() 240 return m_facts.insert_if_not_there(sym, Fact()); in get()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/dataflow/ |
H A D | dataflow.h | 67 auto& value = m_body2rules.insert_if_not_there(d, nullptr); 75 … bool new_info = m_facts.insert_if_not_there(sym, Fact()).init_up(m_context, cur); 88 m_facts.insert_if_not_there(sym, Fact()).init_down(m_context, r); in mk_index_sort() 102 …bool new_info = m_facts.insert_if_not_there(head_sym, Fact()).propagate_up(m_context, r, tail_fact… 240 return m_facts.insert_if_not_there(sym, Fact()); in eval_q()
|
/dports/math/z3/z3-z3-4.8.13/src/smt/ |
H A D | smt_cg_table.cpp | 216 n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n); in insert() 219 n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n); in insert() 225 n_prime = UNTAG(comm_table*, t)->insert_if_not_there(n); in insert() 228 n_prime = UNTAG(table*, t)->insert_if_not_there(n); in insert()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
H A D | smt_cg_table.cpp | 216 n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n); in insert() 219 n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n); in insert() 225 n_prime = UNTAG(comm_table*, t)->insert_if_not_there(n); in insert() 228 n_prime = UNTAG(table*, t)->insert_if_not_there(n); in insert()
|
/dports/math/z3/z3-z3-4.8.13/src/util/ |
H A D | obj_pair_set.h | 39 …bool insert_if_not_there(T1 * t1, T2 * t2) { return m_set.insert_if_not_there2(obj_pair(t1, t2)); } in insert_if_not_there() function 40 bool insert_if_not_there(obj_pair const & p) { return m_set.insert_if_not_there2(p); } in insert_if_not_there() function
|
H A D | obj_ref_hashtable.h | 70 key_data const & insert_if_not_there(Key * k, Value const & v) { in insert_if_not_there() function 72 return m_table.insert_if_not_there(k, v); in insert_if_not_there()
|
H A D | obj_triple_hashtable.h | 155 key_data const & insert_if_not_there(Key1 * k1, Key2 * k2, Key3 * k3, Value const & v) { in insert_if_not_there() function 156 return m_table.insert_if_not_there(key_data(k1, k2, k3, v)); in insert_if_not_there()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/util/ |
H A D | obj_pair_set.h | 40 …bool insert_if_not_there(T1 * t1, T2 * t2) { return m_set.insert_if_not_there2(obj_pair(t1, t2)); } in insert_if_not_there() function 41 bool insert_if_not_there(obj_pair const & p) { return m_set.insert_if_not_there2(p); } in insert_if_not_there() function
|
H A D | obj_ref_hashtable.h | 70 key_data const & insert_if_not_there(Key * k, Value const & v) { in insert_if_not_there() function 72 return m_table.insert_if_not_there(k, v); in insert_if_not_there()
|
H A D | obj_triple_hashtable.h | 157 key_data const & insert_if_not_there(Key1 * k1, Key2 * k2, Key3 * k3, Value const & v) { in insert_if_not_there() function 158 return m_table.insert_if_not_there(key_data(k1, k2, k3, v)); in insert_if_not_there()
|
/dports/math/z3/z3-z3-4.8.13/src/ast/euf/ |
H A D | euf_etable.cpp | 210 n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n); in insert() 213 n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n); in insert() 217 n_prime = UNTAG(comm_table*, t)->insert_if_not_there(n); in insert() 220 n_prime = UNTAG(table*, t)->insert_if_not_there(n); in insert()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/euf/ |
H A D | euf_etable.cpp | 210 n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n); in insert() 213 n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n); in insert() 217 n_prime = UNTAG(comm_table*, t)->insert_if_not_there(n); in insert() 220 n_prime = UNTAG(table*, t)->insert_if_not_there(n); in insert()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/model/ |
H A D | model_core.cpp | 60 auto& value = m_interp.insert_if_not_there(d, v0); in register_decl() 88 auto& value = m_finterp.insert_if_not_there(d, nullptr); in update_func_interp()
|
/dports/math/z3/z3-z3-4.8.13/src/math/polynomial/ |
H A D | polynomial_cache.cpp | 143 polynomial * p_prime = m_poly_table.insert_if_not_there(p); in mk_unique() 156 psc_chain_entry * old_entry = m_psc_chain_cache.insert_if_not_there(entry); in psc_chain() 183 factor_entry * old_entry = m_factor_cache.insert_if_not_there(entry); in factor()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/polynomial/ |
H A D | polynomial_cache.cpp | 143 polynomial * p_prime = m_poly_table.insert_if_not_there(p); in mk_unique() 156 psc_chain_entry * old_entry = m_psc_chain_cache.insert_if_not_there(entry); in psc_chain() 183 factor_entry * old_entry = m_factor_cache.insert_if_not_there(entry); in factor()
|
/dports/math/z3/z3-z3-4.8.13/src/model/ |
H A D | model_core.cpp | 60 auto& value = m_interp.insert_if_not_there(d, v0); in register_decl() 89 auto& value = m_finterp.insert_if_not_there(d, nullptr); in update_func_interp()
|
/dports/math/z3/z3-z3-4.8.13/src/tactic/bv/ |
H A D | bv_size_reduction_tactic.cpp | 71 auto& value = m_signed_lowers.insert_if_not_there(v, k); in update_signed_lower() 80 auto& value = m_signed_uppers.insert_if_not_there(v, k); in update_signed_upper() 90 auto& value = m_unsigned_lowers.insert_if_not_there(v, k); in update_unsigned_lower() 100 auto& value = m_unsigned_uppers.insert_if_not_there(v, k); in update_unsigned_upper()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/bv/ |
H A D | bv_size_reduction_tactic.cpp | 71 auto& value = m_signed_lowers.insert_if_not_there(v, k); in update_signed_lower() 80 auto& value = m_signed_uppers.insert_if_not_there(v, k); in update_signed_upper() 90 auto& value = m_unsigned_lowers.insert_if_not_there(v, k); in update_unsigned_lower() 100 auto& value = m_unsigned_uppers.insert_if_not_there(v, k); in update_unsigned_upper()
|
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/ |
H A D | bv_ackerman.cpp | 47 vv* other = m_table.insert_if_not_there(n); in used_eq_eh() 71 vv* other = m_table.insert_if_not_there(n); in used_diseq_eh()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/ |
H A D | bv_ackerman.cpp | 45 vv* other = m_table.insert_if_not_there(n); in used_eq_eh() 69 vv* other = m_table.insert_if_not_there(n); in used_diseq_eh()
|
/dports/math/z3/z3-z3-4.8.13/src/muz/transforms/ |
H A D | dl_mk_array_instantiation.cpp | 117 selects.insert_if_not_there(arg, ptr_vector<expr>()); in create_head() 144 selects.insert_if_not_there(f->get_arg(0), ptr_vector<expr>()); in retrieve_selects() 224 selects.insert_if_not_there(*it, ptr_vector<expr>()); in retrieve_all_selects()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/transforms/ |
H A D | dl_mk_array_instantiation.cpp | 117 selects.insert_if_not_there(arg, ptr_vector<expr>()); in create_head() 144 selects.insert_if_not_there(f->get_arg(0), ptr_vector<expr>()); in retrieve_selects() 224 selects.insert_if_not_there(*it, ptr_vector<expr>()); in retrieve_all_selects()
|
/dports/math/z3/z3-z3-4.8.13/src/tactic/core/ |
H A D | symmetry_reduce_tactic.cpp | 283 inv_map.insert_if_not_there(n, ptr_vector<app>()).push_back(t); in compute_inv_app() 344 auto& value = m_use_funs.insert_if_not_there(to_app(e), 0); in operator ()() 371 auto& value = m_sibs.insert_if_not_there(to_app(e), 0); in operator ()() 514 m_occs.insert_if_not_there(n, 0); in operator ()() 519 m_occs.insert_if_not_there(to_app(arg), 0)++; in operator ()()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/core/ |
H A D | symmetry_reduce_tactic.cpp | 285 inv_map.insert_if_not_there(n, ptr_vector<app>()).push_back(t); in compute_inv_app() 348 auto& value = m_use_funs.insert_if_not_there(to_app(e), 0); in operator ()() 375 auto& value = m_sibs.insert_if_not_there(to_app(e), 0); in operator ()() 518 m_occs.insert_if_not_there(n, 0); in operator ()() 523 m_occs.insert_if_not_there(to_app(arg), 0)++; in operator ()()
|
/dports/math/z3/z3-z3-4.8.13/src/ast/ |
H A D | num_occurs.cpp | 27 m_num_occurs.insert_if_not_there(ARG, 0)++; \ in process()
|