| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/rel/ |
| H A D | dl_mk_simple_joins.cpp | 262 pair_info * & ptr_inf = m_costs.insert_if_not_there(get_key(t1, t2), nullptr);
297 … ptr_vector<app> & rule_content = m_rules_content.insert_if_not_there(r, ptr_vector<app>());
|
| H A D | dl_sparse_table.cpp | 36 store_offset entry_ofs = m_data_indexer.insert_if_not_there(m_reserve); in insert_or_get_reserve_content()
45 store_offset entry_ofs = m_data_indexer.insert_if_not_there(m_reserve); in insert_reserve_content()
780 sp_table_vector * & vect = m_pool.insert_if_not_there(sig, nullptr); in recycle()
|
| H A D | dl_sparse_table.h | 299 return m_data_indexer.insert_if_not_there(ofs)==ofs; in insert_offset()
|
| H A D | dl_compiler.cpp | 40 auto& value = m_pred_regs.insert_if_not_there(pred, UINT_MAX); in ensure_predicate_loaded()
573 auto& value = var_indexes.insert_if_not_there(var_num, unsigned_vector()); in compile_rule_evaluation_run()
635 var_indexes.insert_if_not_there(v, unsigned_vector()).push_back(src_col); in compile_rule_evaluation_run()
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/rel/ |
| H A D | dl_mk_simple_joins.cpp | 262 pair_info * & ptr_inf = m_costs.insert_if_not_there(get_key(t1, t2), nullptr); in register_pair()
297 … ptr_vector<app> & rule_content = m_rules_content.insert_if_not_there(r, ptr_vector<app>()); in register_rule()
|
| H A D | dl_sparse_table.cpp | 36 store_offset entry_ofs = m_data_indexer.insert_if_not_there(m_reserve); in insert_or_get_reserve_content()
45 store_offset entry_ofs = m_data_indexer.insert_if_not_there(m_reserve); in insert_reserve_content()
780 sp_table_vector * & vect = m_pool.insert_if_not_there(sig, nullptr); in recycle()
|
| H A D | dl_sparse_table.h | 299 return m_data_indexer.insert_if_not_there(ofs)==ofs; in insert_offset()
|
| H A D | dl_compiler.cpp | 40 auto& value = m_pred_regs.insert_if_not_there(pred, UINT_MAX); in ensure_predicate_loaded()
573 auto& value = var_indexes.insert_if_not_there(var_num, unsigned_vector()); in compile_rule_evaluation_run()
635 var_indexes.insert_if_not_there(v, unsigned_vector()).push_back(src_col); in compile_rule_evaluation_run()
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/arith/ |
| H A D | recover_01_tactic.cpp | 128 auto& value = m_var2clauses.insert_if_not_there(x, ptr_vector<app>()); in save_clause()
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | smt_theory.h | 511 other = table.insert_if_not_there(v); in assume_eqs()
|
| H A D | smt_solver.cpp | 351 m_fds.insert_if_not_there(fd); in operator ()()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | smt_theory.h | 505 other = table.insert_if_not_there(v); in assume_eqs()
|
| H A D | smt_solver.cpp | 347 m_fds.insert_if_not_there(fd); in operator ()()
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/base/ |
| H A D | dl_context.cpp | 77 unsigned idx = m_el_numbers.insert_if_not_there(sym, newIdx); in get_number()
119 unsigned idx = m_el_numbers.insert_if_not_there(el, newIdx); in get_number()
1317 unsigned_vector& vars = var_idxs.insert_if_not_there(s, unsigned_vector()); in declare_vars()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/ |
| H A D | dl_context.cpp | 77 unsigned idx = m_el_numbers.insert_if_not_there(sym, newIdx); in get_number()
119 unsigned idx = m_el_numbers.insert_if_not_there(el, newIdx); in get_number()
1316 unsigned_vector& vars = var_idxs.insert_if_not_there(s, unsigned_vector()); in declare_vars()
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/spacer/ |
| H A D | spacer_pdr.cpp | 131 model_nodes& nodes = cache(n).insert_if_not_there(n.post(), ns); in add_leaf()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/ |
| H A D | recover_01_tactic.cpp | 104 auto& value = m_var2clauses.insert_if_not_there(x, ptr_vector<app>()); in save_clause()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/ |
| H A D | spacer_pdr.cpp | 131 model_nodes& nodes = cache(n).insert_if_not_there(n.post(), ns); in add_leaf()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/ |
| H A D | factor_rewriter.cpp | 345 m_powers.insert_if_not_there(f, 0)++; in collect_powers()
|
| H A D | bv_bounds.cpp | 526 auto& value = m_unsigned_lowers.insert_if_not_there(v, l); in bound_lo()
537 auto& value = m_unsigned_uppers.insert_if_not_there(v, u); in bound_up()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
| H A D | factor_rewriter.cpp | 345 m_powers.insert_if_not_there(f, 0)++; in collect_powers()
|
| H A D | bv_bounds.cpp | 526 auto& value = m_unsigned_lowers.insert_if_not_there(v, l); in bound_lo()
537 auto& value = m_unsigned_uppers.insert_if_not_there(v, u); in bound_up()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/macros/ |
| H A D | quasi_macros.cpp | 66 m_occurrences.insert_if_not_there(f, 0); in find_occurrences()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/macros/ |
| H A D | quasi_macros.cpp | 66 m_occurrences.insert_if_not_there(f, 0); in find_occurrences()
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/fp/ |
| H A D | datalog_parser.cpp | 1194 auto& value = m_sort_contents.insert_if_not_there(sort_name, nullptr); in ensure_sort_content()
1533 auto const & value = m_number_names.insert_if_not_there(num, el_name); in parse_map_file()
|