mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-01 21:49:29 +00:00
Code Activity

#7861

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-11 15:05:11 -07:00
parent 8440623f6d
commit 3a409e0673
2 changed files with 17 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/model/func_interp.cpp
View file

@ -31,7 +31,7 @@ func_entry::func_entry(ast_manager & m, unsigned arity, expr * const * args, exp
for (unsigned i = 0; i < arity; i++) { for (unsigned i = 0; i < arity; i++) {
expr * arg = args[i]; expr * arg = args[i];
//SASSERT(is_ground(arg)); //SASSERT(is_ground(arg));
if (!m.is_value(arg)) if (arg && !m.is_value(arg))
m_args_are_values = false; m_args_are_values = false;
m.inc_ref(arg); m.inc_ref(arg);
m_args[i] = arg; m_args[i] = arg;
@ -80,13 +80,16 @@ func_interp::func_interp(ast_manager & m, unsigned arity):
} }
func_interp::~func_interp() { func_interp::~func_interp() {
dealloc(m_entry_table);
for (func_entry* curr : m_entries) { for (func_entry* curr : m_entries) {
curr->deallocate(m(), m_arity); curr->deallocate(m(), m_arity);
} }
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);
if (m_key)
m_key->deallocate(m(), m_arity);
} }
func_interp * func_interp::copy() const { func_interp * func_interp::copy() const {
@ -179,8 +182,13 @@ bool func_interp::is_constant() const {
*/ */
func_entry * func_interp::get_entry(expr * const * args) const { func_entry * func_interp::get_entry(expr * const * args) const {
if (m_entry_table) { if (m_entry_table) {
func_entry key(m(), m_arity, args, m().mk_true()), * entry = nullptr; for (unsigned i = 0; i < m_arity; ++i)
if (m_entry_table->find(&key, entry)) m_key->m_args[i] = args[i];
func_entry * entry = nullptr;
bool found = m_entry_table->find(m_key, entry);
for (unsigned i = 0; i < m_arity; ++i)
m_key->m_args[i] = nullptr;
if (found)
return entry; return entry;
else else
return nullptr; return nullptr;
@ -227,6 +235,9 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) {
func_entry_hash(m_arity), func_entry_eq(m_arity)); func_entry_hash(m_arity), func_entry_eq(m_arity));
for (func_entry* curr : m_entries) for (func_entry* curr : m_entries)
m_entry_table->insert(curr); m_entry_table->insert(curr);
ptr_vector<expr> null_args;
null_args.resize(m_arity, nullptr);
m_key = func_entry::mk(m(), m_arity, null_args.data(), nullptr);
} }
else if (m_entry_table) else if (m_entry_table)
m_entry_table->insert(new_entry); m_entry_table->insert(new_entry);

1
src/model/func_interp.h
View file

@ -100,6 +100,7 @@ class func_interp {
using entry_table = ptr_hashtable<func_entry, func_entry_hash, func_entry_eq>; using entry_table = ptr_hashtable<func_entry, func_entry_hash, func_entry_eq>;
entry_table* m_entry_table = nullptr; entry_table* m_entry_table = nullptr;
func_entry* m_key = nullptr;
void reset_interp_cache(); void reset_interp_cache();