mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-30 13:19:04 +00:00
Code Activity

fix #7861

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-11 10:19:16 -07:00
parent 7566cc744d
commit 9196a3c369
2 changed files with 45 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/model/func_interp.cpp
View file

@ -86,6 +86,7 @@ func_interp::~func_interp() {
m().dec_ref(m_else); m().dec_ref(m_else);
m().dec_ref(m_interp); m().dec_ref(m_interp);
m().dec_ref(m_array_interp); m().dec_ref(m_array_interp);
dealloc(m_entry_table);
} }
func_interp * func_interp::copy() const { func_interp * func_interp::copy() const {
@ -177,6 +178,13 @@ bool func_interp::is_constant() const {
args_are_values to true if for all entries e e.args_are_values() is true. args_are_values to true if for all entries e e.args_are_values() is true.
*/ */
func_entry * func_interp::get_entry(expr * const * args) const { func_entry * func_interp::get_entry(expr * const * args) const {
if (m_entry_table) {
func_entry key(m(), m_arity, args, m().mk_true()), * entry = nullptr;
if (m_entry_table->find(&key, entry))
return entry;
else
return nullptr;
}
for (func_entry* curr : m_entries) { for (func_entry* curr : m_entries) {
if (curr->eq_args(m(), m_arity, args)) if (curr->eq_args(m(), m_arity, args))
return curr; return curr;
@ -214,10 +222,20 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) {
if (!new_entry->args_are_values()) if (!new_entry->args_are_values())
m_args_are_values = false; m_args_are_values = false;
m_entries.push_back(new_entry); m_entries.push_back(new_entry);
if (!m_entry_table && m_entries.size() > 500) {
m_entry_table = alloc(entry_table, 1000,
func_entry_hash(m_arity), func_entry_eq(m_arity));
for (func_entry* curr : m_entries)
m_entry_table->insert(curr);
}
else if (m_entry_table)
m_entry_table->insert(new_entry);
} }
void func_interp::del_entry(unsigned idx) { void func_interp::del_entry(unsigned idx) {
auto* e = m_entries[idx]; auto* e = m_entries[idx];
if (m_entry_table)
m_entry_table->remove(e);
m_entries[idx] = m_entries.back(); m_entries[idx] = m_entries.back();
m_entries.pop_back(); m_entries.pop_back();
e->deallocate(m(), m_arity); e->deallocate(m(), m_arity);

27
src/model/func_interp.h
View file

@ -63,6 +63,30 @@ public:
bool eq_args(ast_manager & m, unsigned arity, expr * const * args) const; bool eq_args(ast_manager & m, unsigned arity, expr * const * args) const;
}; };
struct func_entry_eq {
unsigned m_arity;
func_entry_eq(unsigned arity) : m_arity(arity) {}
bool operator()(func_entry* a, func_entry* b) const {
for (unsigned i = 0; i < m_arity; ++i)
if (a->get_arg(i) != b->get_arg(i))
return false;
return true;
}
};
struct func_entry_hash {
unsigned m_arity;
struct chasher {
unsigned operator()(func_entry* e, unsigned idx) const {
return e->get_arg(idx)->get_id();
}
};
func_entry_hash(unsigned arity) : m_arity(arity) {}
unsigned operator()(func_entry* e) const {
return get_composite_hash(e, m_arity, default_kind_hash_proc<func_entry*>(), chasher());
}
};
class func_interp { class func_interp {
ast_manager & m_manager; ast_manager & m_manager;
unsigned m_arity; unsigned m_arity;
@ -74,6 +98,9 @@ class func_interp {
expr * m_array_interp; // <! interp with lambda abstraction expr * m_array_interp; // <! interp with lambda abstraction
using entry_table = ptr_hashtable<func_entry, func_entry_hash, func_entry_eq>;
entry_table* m_entry_table = nullptr;
void reset_interp_cache(); void reset_interp_cache();
expr * get_interp_core() const; expr * get_interp_core() const;