mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
insert fresh
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
fb124d6e93
commit
4b6a7371dd
|
@ -1794,7 +1794,8 @@ ast * ast_manager::register_node_core(ast * n) {
|
|||
CASSERT("nondet_bug", contains || slow_not_contains(n));
|
||||
#endif
|
||||
|
||||
ast * r = m_ast_table.insert_if_not_there(n);
|
||||
ast* r = m_ast_table.insert_if_not_there(n);
|
||||
|
||||
SASSERT(r->m_hash == h);
|
||||
if (r != n) {
|
||||
SASSERT(contains);
|
||||
|
|
|
@ -281,6 +281,28 @@ public:
|
|||
unsigned used_slots() const {
|
||||
return m_used_slots;
|
||||
}
|
||||
|
||||
void insert_fresh(T const& d) {
|
||||
if (!has_free_cells()) {
|
||||
expand_table();
|
||||
}
|
||||
unsigned mask = m_slots - 1;
|
||||
unsigned h = get_hash(d);
|
||||
unsigned idx = h & mask;
|
||||
cell * c = m_table + idx;
|
||||
cell * new_c = nullptr;
|
||||
m_size++;
|
||||
if (c->is_free()) {
|
||||
m_used_slots++;
|
||||
}
|
||||
else {
|
||||
new_c = get_free_cell();
|
||||
*new_c = *c;
|
||||
}
|
||||
c->m_next = new_c;
|
||||
c->m_data = d;
|
||||
CASSERT("chashtable_bug", check_invariant());
|
||||
}
|
||||
|
||||
void insert(T const & d) {
|
||||
if (!has_free_cells())
|
||||
|
|
Loading…
Reference in a new issue