mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-20 15:40:37 +00:00
Code Activity

add init-table for common sub-expressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-19 10:07:46 -07:00
parent f885fe953f
commit 9e505edb66
2 changed files with 12 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/model/func_interp.cpp
View file

@ -231,10 +231,8 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) {
m_args_are_values = false;
m_entries.push_back(new_entry);
if (!m_entry_table && m_entries.size() > 500) {
m_entry_table = alloc(entry_table, 1024,
func_entry_hash(m_arity), func_entry_eq(m_arity));
for (func_entry* curr : m_entries)
m_entry_table->insert(curr);
init_table();
ptr_vector<expr> null_args;
null_args.resize(m_arity, nullptr);
m_key = func_entry::mk(m(), m_arity, null_args.data(), nullptr);
@ -243,6 +241,12 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) {
m_entry_table->insert(new_entry);
}
void func_interp::init_table() {
m_entry_table = alloc(entry_table, 1024, func_entry_hash(m_arity), func_entry_eq(m_arity));
for (func_entry *curr : m_entries)
m_entry_table->insert(curr);
}
void func_interp::del_entry(unsigned idx) {
auto* e = m_entries[idx];
if (m_entry_table)
@ -310,12 +314,8 @@ void func_interp::compress() {
if (m_entry_table) {
dealloc(m_entry_table);
m_entry_table = nullptr;
if (m_entries.size() > 500) {
m_entry_table = alloc(entry_table, 1024,
func_entry_hash(m_arity), func_entry_eq(m_arity));
for (func_entry* curr : m_entries)
m_entry_table->insert(curr);
}
if (m_entries.size() > 500)
init_table();
}
}
// other compression, if else is a default branch.

2
src/model/func_interp.h
View file

@ -104,6 +104,8 @@ class func_interp {
void reset_interp_cache();
void init_table();
expr * get_interp_core() const;
expr_ref get_array_interp_core(func_decl * f) const;