mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 17:32:45 +00:00
Code Activity

Improve generation accounting (#10008)

Browse source 
Details in original PR: https://github.com/Z3Prover/z3/pull/10007

---------

Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
This commit is contained in:
Can Cebeci 2026-06-30 16:17:02 -07:00 • committed by GitHub
parent d666ef1ddf
commit 03572a61f8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
14 changed files with 365 additions and 147 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/smt/mam.cpp
View file

@ -215,7 +215,6 @@ namespace {
unsigned short m_num_args;
unsigned m_ireg;
unsigned m_oreg;
unsigned m_curr_max_generation = 0;
};
struct get_cgr : public instruction {
@ -1881,47 +1880,33 @@ namespace {
m_pool.recycle(v);
}
void update_max_generation(enode * n, enode * prev, enode * min_gen_match=nullptr) {
unsigned new_gen = min_gen_match ? min_gen_match->get_generation() : n->get_generation();
m_max_generation = std::max(m_max_generation, new_gen);
void update_max_generation(enode * n, enode * prev) {
m_max_generation = std::max(m_max_generation, m_context.get_generation(n));
if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality))
m_used_enodes.push_back(std::make_tuple(prev, n));
}
void get_f_app(func_decl* lbl, unsigned num_expected_args, enode* curr, enode*& matching_cgr, enode*& min_gen_match) {
if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args) {
if (curr->is_cgr() && !matching_cgr)
matching_cgr = curr;
if (!min_gen_match || min_gen_match->get_generation() > curr->get_generation()) {
min_gen_match = curr;
}
}
}
// We have to provide the number of expected arguments because we have flat-assoc applications such as +.
// Flat-assoc applications may have arbitrary number of arguments.
enode * get_first_f_app(func_decl * lbl, unsigned num_expected_args, enode * curr) {
enode * first = curr;
enode *matching_cgr = nullptr, *min_gen_match = nullptr;
do {
get_f_app(lbl, num_expected_args, curr, matching_cgr, min_gen_match);
if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
update_max_generation(curr, first);
return curr;
}
curr = curr->get_next();
}
while (curr != first);
if (matching_cgr)
update_max_generation(matching_cgr, first, min_gen_match);
return matching_cgr;
return nullptr;
}
enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) {
curr = curr->get_next();
while (curr != first) {
if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args && curr->is_cgr()) {
if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality))
m_used_enodes.push_back(std::make_tuple(first, curr));
if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
update_max_generation(curr, first);
return curr;
}
curr = curr->get_next();
@ -2065,7 +2050,7 @@ namespace {
void get_min_max_top_generation(unsigned& min, unsigned& max) {
SASSERT(!m_pattern_instances.empty());
if (m_min_top_generation.empty()) {
min = max = m_pattern_instances[0]->get_generation();
min = max = m_context.get_generation(m_pattern_instances[0]);
m_min_top_generation.push_back(min);
m_max_top_generation.push_back(max);
}
@ -2074,7 +2059,7 @@ namespace {
max = m_max_top_generation.back();
}
for (unsigned i = m_min_top_generation.size(); i < m_pattern_instances.size(); ++i) {
unsigned curr = m_pattern_instances[i]->get_generation();
unsigned curr = m_context.get_generation(m_pattern_instances[i]);
min = std::min(min, curr);
m_min_top_generation.push_back(min);
max = std::max(max, curr);
@ -2315,7 +2300,8 @@ namespace {
m_min_top_generation.reset();
m_max_top_generation.reset();
m_pattern_instances.push_back(n);
m_max_generation = n->get_generation();
m_max_generation = m_context.get_generation(n);
if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality)) {
m_used_enodes.reset();
@ -2492,7 +2478,6 @@ namespace {
m_backtrack_stack[m_top].m_old_max_generation = m_curr_max_generation; \
m_backtrack_stack[m_top].m_old_used_enodes_size = m_curr_used_enodes_size; \
m_backtrack_stack[m_top].m_curr = m_app; \
const_cast<bind*>(static_cast<const bind*>(m_pc))->m_curr_max_generation = m_max_generation; \
m_top++;
BIND_COMMON();
@ -2556,7 +2541,7 @@ namespace {
case YIELD1:
m_bindings[0] = m_registers[static_cast<const yield *>(m_pc)->m_bindings[0]];
#define ON_MATCH(NUM) \
m_max_generation = std::max(m_max_generation, get_max_generation(NUM, m_bindings.begin())); \
m_max_generation = std::max(m_max_generation, get_max_generation(m_context, NUM, m_bindings.begin())); \
if (m_context.get_cancel_flag()) { \
return false; \
} \
@ -2760,7 +2745,6 @@ namespace {
#define BBIND_COMMON() m_b = static_cast<const bind*>(bp.m_instr); \
m_n1 = m_registers[m_b->m_ireg]; \
m_app = get_next_f_app(m_b->m_label, m_b->m_num_args, m_n1, bp.m_curr); \
m_max_generation = m_b->m_curr_max_generation; \
if (!m_app) { \
m_top--; \
goto backtrack; \
@ -3972,10 +3956,6 @@ namespace {
}
return;
}
DEBUG_CODE(
for (unsigned i = 0; i < num_bindings; ++i) {
SASSERT(bindings[i]->get_generation() <= max_generation);
});
#endif
unsigned min_gen = 0, max_gen = 0;

7
src/smt/smt_case_split_queue.cpp
View file

@ -1012,7 +1012,7 @@ namespace {
stack.pop_back();
if (m_context.e_internalized(curr)) {
gen = m_context.get_enode(curr)->get_generation();
gen = m_context.get_generation(m_context.get_enode(curr));
if (gen > maxgen)
maxgen = gen;
if (gen < mingen)
@ -1046,7 +1046,7 @@ namespace {
void operator()(expr * e) {
if (m_context.e_internalized(e)) {
enode * n = m_context.get_enode(e);
n->set_generation(&m_context, m_generation);
m_context.set_generation(n, m_generation);
}
}
};
@ -1069,7 +1069,8 @@ namespace {
stack.pop_back();
if (m_context.e_internalized(curr)) {
unsigned curr_gen = m_context.get_enode(curr)->get_generation();
enode * n = m_context.get_enode(curr);
unsigned curr_gen = m_context.get_generation(n);
if (curr_gen > gen) {
// Lower it.
set_generation_rec(e, gen);

63
src/smt/smt_cg_table.cpp
View file

@ -170,7 +170,7 @@ namespace smt {
void cg_table::display_binary(std::ostream& out, void* t) const {
binary_table* tb = UNTAG(binary_table*, t);
out << "b ";
for (enode* n : *tb) {
for (auto const& [n, v] : *tb) {
out << n->get_owner_id() << " " << cg_binary_hash()(n) << " ";
}
out << "\n";
@ -179,7 +179,7 @@ namespace smt {
void cg_table::display_binary_comm(std::ostream& out, void* t) const {
comm_table* tb = UNTAG(comm_table*, t);
out << "bc ";
for (enode* n : *tb) {
for (auto const& [n, v] : *tb) {
out << n->get_owner_id() << " ";
}
out << "\n";
@ -188,7 +188,7 @@ namespace smt {
void cg_table::display_unary(std::ostream& out, void* t) const {
unary_table* tb = UNTAG(unary_table*, t);
out << "un ";
for (enode* n : *tb) {
for (auto const& [n, v] : *tb) {
out << n->get_owner_id() << " ";
}
out << "\n";
@ -197,36 +197,73 @@ namespace smt {
void cg_table::display_nary(std::ostream& out, void* t) const {
table* tb = UNTAG(table*, t);
out << "nary ";
for (enode* n : *tb) {
for (auto const& [n, v] : *tb) {
out << n->get_owner_id() << " ";
}
out << "\n";
}
enode_bool_pair cg_table::insert(enode * n) {
enode_bool_gen_ptr cg_table::insert(enode * n, unsigned generation) {
// it doesn't make sense to insert a constant.
SASSERT(n->get_num_args() > 0);
SASSERT(!m_manager.is_and(n->get_expr()));
SASSERT(!m_manager.is_or(n->get_expr()));
enode * n_prime;
unsigned* payload = nullptr;
void * t = get_table(n);
switch (static_cast<table_kind>(GET_TAG(t))) {
case UNARY:
n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n);
return enode_bool_pair(n_prime, false);
if (auto* e = UNTAG(unary_table*, t)->find_core(n)) {
n_prime = e->get_data().m_key;
payload = &e->get_data().m_value;
}
else {
e = UNTAG(unary_table*, t)->insert_if_not_there3(n, generation);
n_prime = e->get_data().m_key;
payload = &e->get_data().m_value;
(*payload) = generation;
}
return enode_bool_gen_ptr(n_prime, false, payload);
case BINARY:
n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n);
if (auto* e = UNTAG(binary_table*, t)->find_core(n)) {
n_prime = e->get_data().m_key;
payload = &e->get_data().m_value;
}
else {
e = UNTAG(binary_table*, t)->insert_if_not_there3(n, generation);
n_prime = e->get_data().m_key;
payload = &e->get_data().m_value;
(*payload) = generation;
}
TRACE(cg_table, tout << "insert: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " inserted: " << (n == n_prime) << " " << n_prime->get_owner_id() << "\n";
display_binary(tout, t); tout << "contains_ptr: " << contains_ptr(n) << "\n";);
return enode_bool_pair(n_prime, false);
return enode_bool_gen_ptr(n_prime, false, payload);
case BINARY_COMM:
m_commutativity = false;
n_prime = UNTAG(comm_table*, t)->insert_if_not_there(n);
return enode_bool_pair(n_prime, m_commutativity);
if (auto* e = UNTAG(comm_table*, t)->find_core(n)) {
n_prime = e->get_data().m_key;
payload = &e->get_data().m_value;
}
else {
e = UNTAG(comm_table*, t)->insert_if_not_there3(n, generation);
n_prime = e->get_data().m_key;
payload = &e->get_data().m_value;
(*payload) = generation;
}
return enode_bool_gen_ptr(n_prime, m_commutativity, payload);
default:
n_prime = UNTAG(table*, t)->insert_if_not_there(n);
return enode_bool_pair(n_prime, false);
if (auto* e = UNTAG(table*, t)->find_core(n)) {
n_prime = e->get_data().m_key;
payload = &e->get_data().m_value;
}
else {
e = UNTAG(table*, t)->insert_if_not_there3(n, generation);
n_prime = e->get_data().m_key;
payload = &e->get_data().m_value;
(*payload) = generation;
}
return enode_bool_gen_ptr(n_prime, false, payload);
}
}

48
src/smt/smt_cg_table.h
View file

@ -21,10 +21,14 @@ Revision History:
#include "smt/smt_enode.h"
#include "util/hashtable.h"
#include "util/chashtable.h"
#include "util/map.h"
namespace smt {
typedef std::pair<enode *, bool> enode_bool_pair;
typedef std::tuple<enode*, bool, unsigned*> enode_bool_gen_ptr;
typedef std::pair<enode*, unsigned*> enode_gen_ptr;
typedef std::pair<enode *, enode *> enode_pair;
// one table per function symbol
@ -48,7 +52,7 @@ namespace smt {
}
};
typedef chashtable<enode *, cg_unary_hash, cg_unary_eq> unary_table;
typedef map<enode*, unsigned, cg_unary_hash, cg_unary_eq> unary_table;
struct cg_binary_hash {
unsigned operator()(enode * n) const {
@ -68,7 +72,7 @@ namespace smt {
}
};
typedef chashtable<enode*, cg_binary_hash, cg_binary_eq> binary_table;
typedef map<enode*, unsigned, cg_binary_hash, cg_binary_eq> binary_table;
struct cg_comm_hash {
unsigned operator()(enode * n) const {
@ -103,7 +107,7 @@ namespace smt {
}
};
typedef chashtable<enode*, cg_comm_hash, cg_comm_eq> comm_table;
typedef map<enode*, unsigned, cg_comm_hash, cg_comm_eq> comm_table;
struct cg_hash {
unsigned operator()(enode * n) const;
@ -113,7 +117,7 @@ namespace smt {
bool operator()(enode * n1, enode * n2) const;
};
typedef chashtable<enode*, cg_hash, cg_eq> table;
typedef map<enode*, unsigned, cg_hash, cg_eq> table;
ast_manager & m_manager;
bool m_commutativity; //!< true if the last found congruence used commutativity
@ -148,7 +152,7 @@ namespace smt {
return n' and a boolean indicating whether n and n' are congruence
modulo commutativity, otherwise insert n and return (n,false).
*/
enode_bool_pair insert(enode * n);
enode_bool_gen_ptr insert(enode * n, unsigned generation);
void erase(enode * n);
@ -167,35 +171,47 @@ namespace smt {
}
}
enode * find(enode * n) const {
enode_gen_ptr find_gen(enode * n) const {
SASSERT(n->get_num_args() > 0);
enode * r = nullptr;
void * t = const_cast<cg_table*>(this)->get_table(n);
unary_table::entry* e = nullptr;
switch (static_cast<table_kind>(GET_TAG(t))) {
case UNARY:
return UNTAG(unary_table*, t)->find(n, r) ? r : nullptr;
e = UNTAG(unary_table*, t)->find_core(n);
return e ? enode_gen_ptr(e->get_data().m_key, &e->get_data().m_value) : enode_gen_ptr(nullptr, nullptr);
case BINARY:
return UNTAG(binary_table*, t)->find(n, r) ? r : nullptr;
e = UNTAG(binary_table*, t)->find_core(n);
return e ? enode_gen_ptr(e->get_data().m_key, &e->get_data().m_value) : enode_gen_ptr(nullptr, nullptr);
case BINARY_COMM:
return UNTAG(comm_table*, t)->find(n, r) ? r : nullptr;
e = UNTAG(comm_table*, t)->find_core(n);
return e ? enode_gen_ptr(e->get_data().m_key, &e->get_data().m_value) : enode_gen_ptr(nullptr, nullptr);
default:
return UNTAG(table*, t)->find(n, r) ? r : nullptr;
e = UNTAG(table*, t)->find_core(n);
return e ? enode_gen_ptr(e->get_data().m_key, &e->get_data().m_value) : enode_gen_ptr(nullptr, nullptr);
}
}
enode * find(enode * n) const {
return find_gen(n).first;
}
bool contains_ptr(enode * n) const {
enode * r;
SASSERT(n->get_num_args() > 0);
void * t = const_cast<cg_table*>(this)->get_table(n);
unary_table::entry* e = nullptr;
switch (static_cast<table_kind>(GET_TAG(t))) {
case UNARY:
return UNTAG(unary_table*, t)->find(n, r) && n == r;
e = UNTAG(unary_table*, t)->find_core(n);
return e && n == e->get_data().m_key;
case BINARY:
return UNTAG(binary_table*, t)->find(n, r) && n == r;
e = UNTAG(binary_table*, t)->find_core(n);
return e && n == e->get_data().m_key;
case BINARY_COMM:
return UNTAG(comm_table*, t)->find(n, r) && n == r;
e = UNTAG(comm_table*, t)->find_core(n);
return e && n == e->get_data().m_key;
default:
return UNTAG(table*, t)->find(n, r) && n == r;
e = UNTAG(table*, t)->find_core(n);
return e && n == e->get_data().m_key;
}
}

121
src/smt/smt_context.cpp
View file

@ -537,7 +537,8 @@ namespace smt {
mark_as_relevant(r1);
}
push_trail(add_eq_trail(*this, r1, n1, r2->get_num_parents()));
unsigned r2_num_parents = r2->get_num_parents();
m_qmanager->add_eq_eh(r1, r2);
@ -568,6 +569,8 @@ namespace smt {
SASSERT(r1->get_root() == r2);
reinsert_parents_into_cg_table(r1, r2, n1, n2, js);
push_trail(add_eq_trail(*this, r1, n1, r2_num_parents));
if (n2->is_bool())
propagate_bool_enode_assignment(r1, r2, n1, n2);
@ -594,6 +597,8 @@ namespace smt {
must be removed from the congruence table since their hash code will change.
*/
void context::remove_parents_from_cg_table(enode * r1) {
SASSERT(m_r1_parent_generations.empty());
// Remove parents from the congruence table
for (enode * parent : enode::parents(r1)) {
CTRACE(add_eq, !parent->is_marked() && parent->is_cgc_enabled() && parent->is_true_eq() && m_cg_table.contains_ptr(parent), tout << parent->get_owner_id() << "\n";);
@ -603,7 +608,8 @@ namespace smt {
tout << "\n";
tout << "contains: " << m_cg_table.contains(parent) << "\n";
if (m_cg_table.contains(parent)) {
tout << "owner: " << m_cg_table.find(parent)->get_owner_id() << "\n";
enode* owner = m_cg_table.find(parent);
tout << "owner: " << owner->get_owner_id() << "\n";
}
m_cg_table.display(tout);
);
@ -614,6 +620,7 @@ namespace smt {
SASSERT(!parent->is_cgc_enabled() || m_cg_table.contains_ptr(parent));
parent->set_mark();
if (parent->is_cgc_enabled()) {
m_r1_parent_generations.push_back(std::make_pair(parent, get_generation(parent)));
m_cg_table.erase(parent);
SASSERT(!m_cg_table.contains_ptr(parent));
}
@ -621,6 +628,21 @@ namespace smt {
}
}
// Sticky update to the generation number of the congruence class
// Goes out of scope when n is garbage collected.
void context::set_generation_sticky(enode * n, unsigned generation) {
SASSERT(n->uses_cg_table());
auto [cgr, cgc_gen] = m_cg_table.find_gen(n);
SASSERT(cgr);
SASSERT(cgc_gen);
// Callers are responsible for this. Sticky updates are too expensive to accommodate no-ops.
SASSERT(generation < *cgc_gen);
*cgc_gen = generation;
m_sticky_generation_updates.insert(n, generation);
}
/**
\brief Reinsert the parents of r1 that were removed from the
cg_table at remove_parents_from_cg_table. Some of these parents will
@ -638,6 +660,7 @@ namespace smt {
enode_vector & r2_parents = r2->m_parents;
enode_vector & r1_parents = r1->m_parents;
unsigned num_r1_parents = r1_parents.size();
unsigned cgc_enabled_idx = 0;
for (unsigned i = 0; i < num_r1_parents; ++i) {
enode* parent = r1_parents[i];
if (!parent->is_marked())
@ -658,26 +681,40 @@ namespace smt {
m_dyn_ack_manager.cg_conflict_eh(n1->get_app(), n2->get_app());
assign(literal(v), mk_justification(eq_propagation_justification(lhs, rhs)));
}
if (parent->is_cgc_enabled()) {
auto [p, parent_generation] = m_r1_parent_generations[cgc_enabled_idx++];
SASSERT(p == parent);
m_constant_generations.insert(parent, parent_generation);
}
// It is not necessary to reinsert the equality to the congruence table
// (because the only congruence propagations that could lead to are already handled by the assign() here).
continue;
}
}
if (parent->is_cgc_enabled()) {
auto [parent_prime, used_commutativity] = m_cg_table.insert(parent);
auto [p, parent_generation] = m_r1_parent_generations[cgc_enabled_idx++];
SASSERT(p == parent);
auto [parent_prime, used_commutativity, gen_ptr] = m_cg_table.insert(parent, parent_generation);
if (parent_prime == parent) {
SASSERT(parent);
SASSERT(parent->is_cgr());
SASSERT(parent->is_cgr());
SASSERT(m_cg_table.contains_ptr(parent));
SASSERT(*gen_ptr == parent_generation);
r2_parents.push_back(parent);
continue;
}
parent->m_cg = parent_prime;
SASSERT(!m_cg_table.contains_ptr(parent));
merge_cgc_generations(parent, parent_generation, parent_prime, gen_ptr);
if (parent_prime->m_root != parent->m_root) {
TRACE(cg, tout << "found new congruence: #" << parent->get_owner_id() << " = #" << parent_prime->get_owner_id()
<< " used_commutativity: " << used_commutativity << "\n";);
push_new_congruence(parent, parent_prime, used_commutativity);
}
}
else {
// If congruence closure is not enabled for parent, then I just copy it
@ -685,6 +722,7 @@ namespace smt {
r2_parents.push_back(parent);
}
}
m_r1_parent_generations.reset();
}
/**
@ -940,6 +978,8 @@ namespace smt {
// unmerge "equivalence" classes
std::swap(r1->m_next, r2->m_next);
SASSERT(m_r1_parent_generations.empty());
// remove the parents of r1 that remained as congruence roots
enode_vector::iterator it = r2->begin_parents();
enode_vector::iterator end = r2->end_parents();
@ -956,6 +996,8 @@ namespace smt {
display(tout << "\n"););
SASSERT(parent->is_cgr());
SASSERT(m_cg_table.contains_ptr(parent));
if (!parent->is_eq())
m_r1_parent_generations.push_back(std::make_pair(parent, get_generation(parent)));
m_cg_table.erase(parent);
}
}
@ -970,22 +1012,50 @@ namespace smt {
// restore parents of r2
r2->m_parents.shrink(r2_num_parents);
unsigned cgr_parent_idx = 0;
// try to reinsert parents of r1 that are not cgr
for (enode * parent : enode::parents(r1)) {
TRACE(add_eq_parents, tout << "visiting: #" << parent->get_owner_id() << "\n";);
if (parent->is_cgc_enabled()) {
enode * cg = parent->m_cg;
if (!parent->is_true_eq() &&
(parent == cg || // parent was root of the congruence class before and after the merge
!congruent(parent, cg) // parent was root of the congruence class before but not after the merge
)) {
auto [parent_cg, used_commutativity] = m_cg_table.insert(parent);
(parent == cg || // parent was root of the congruence class before and after the merge
!congruent(parent, cg)) // parent was root of the congruence class before but not after the merge
) {
unsigned gen;
if (parent->is_eq()) {
gen = 0;
} else if (parent == cg) {
enode *p = nullptr;
unsigned parent_generation;
if (cgr_parent_idx < m_r1_parent_generations.size()) {
std::tie(p, parent_generation) = m_r1_parent_generations[cgr_parent_idx];
}
if (p == parent) {
cgr_parent_idx++;
gen = parent_generation;
} else {
SASSERT(m_cg_table.contains_ptr(parent));
continue;
}
} else {
// Insert at some dummy generation here. An undo_merge_cgr will immediately follow to set the generation.
unsigned dummy_generation = 100000; // NOT UINT_MAX. In case this goes badly overflows would be hell to debug.
gen = dummy_generation;
}
auto [parent_cg, used_commutativity, gen_ptr] = m_cg_table.insert(parent, gen);
(void)used_commutativity;
(void)gen_ptr;
parent->m_cg = parent_cg;
}
}
}
m_r1_parent_generations.reset();
// restore theory vars
if (r2->m_th_var_list.get_next() == nullptr) {
// common case: r2 has at most one variable
@ -1020,6 +1090,30 @@ namespace smt {
CASSERT("add_eq", check_invariant());
}
void context::undo_merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation) {
// TODO: optimization: don't bother unrolling e1 if e1 is an enode about to be garbage collected.
set_generation(e1, e1_generation);
set_generation(e2, e2_generation);
apply_sticky_updates(e1, e1_generation, e2, e2_generation);
}
void context::apply_sticky_updates(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation) {
SASSERT(e1->uses_cg_table());
SASSERT(e2->uses_cg_table());
// optimization opportunity: we actually just need to look at updates above the current decision level.
// Then we wouldn't have to check for minimum either.
for (auto const& [t, generation] : m_sticky_generation_updates) {
// SASSERT(t->uses_cg_table()); // may not hold if t is an equality that became true at some point after the generation update.
if (generation < e1_generation && congruent(t, e1)) {
set_generation(e1, generation);
} else if (generation < e2_generation && congruent(t, e2)) {
set_generation(e2, generation);
}
}
}
/**
\brief Auxiliary method for undo_add_eq.
It restores the theory variables of a given root enode.
@ -1283,7 +1377,7 @@ namespace smt {
*/
enode * context::get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args) {
enode * tmp = m_tmp_enode.set(f, num_args, args);
enode * r = m_cg_table.find(tmp);
enode * r = m_cg_table.find(tmp);
#ifdef Z3DEBUG
if (r != nullptr) {
SASSERT(r->get_decl() == f);
@ -2246,8 +2340,9 @@ namespace smt {
unsigned ilvl = e->get_iscope_lvl();
if (ilvl <= new_scope_lvl)
continue; // node and its children will not be recreated during backtracking
TRACE(cached_generation, tout << "caching: #" << n->get_id() << " " << e->get_generation() << "\n";);
m_cached_generation.insert(n, e->get_generation());
unsigned generation = get_generation(e);
TRACE(cached_generation, tout << "caching: #" << n->get_id() << " " << generation << "\n";);
m_cached_generation.insert(n, generation);
}
for (expr * arg : *to_app(n)) {
if (is_app(arg) || is_quantifier(arg))

41
src/smt/smt_context.h
View file

@ -46,6 +46,7 @@ Revision History:
#include "util/ref.h"
#include "util/timer.h"
#include "util/statistics.h"
#include "util/map.h"
#include "smt/fingerprints.h"
#include "smt/proto_model/proto_model.h"
#include "smt/theory_user_propagator.h"
@ -66,6 +67,9 @@ namespace smt {
class context;
class kernel;
// Hash table for storing enode -> generation mappings
typedef ptr_addr_map<enode, unsigned> enode_generation_table;
struct oom_exception : public z3_error {
oom_exception() : z3_error(ERR_MEMOUT) {}
};
@ -156,6 +160,9 @@ namespace smt {
vector<enode_vector> m_decl2enodes; // decl -> enode (for decls with arity > 0)
enode_vector m_empty_vector;
cg_table m_cg_table;
enode_generation_table m_sticky_generation_updates;
enode_generation_table m_constant_generations; // generations for enodes with !e->uses_cg_table()
vector<std::pair<enode*, unsigned>> m_r1_parent_generations; // generations of parents removed from m_cg_table while merging r1
struct new_eq {
enode * m_lhs;
@ -615,6 +622,21 @@ namespace smt {
return m_qmanager->get_generation(q);
}
unsigned get_generation(enode * e) const {
// We don't support patterns with equality so there is no need to track generations for them.
if (e->is_eq())
return 0;
if (!e->uses_cg_table())
return m_constant_generations.find(e);
auto [cgr, generation] = m_cg_table.find_gen(e);
SASSERT(cgr);
return *generation;
}
void set_generation(enode * e, unsigned generation);
/**
\brief Return true if the logical context internalized universal quantifiers.
*/
@ -1131,12 +1153,16 @@ namespace smt {
void push_new_th_diseq(theory_id th, theory_var lhs, theory_var rhs);
friend class add_eq_trail;
friend class merge_cgc_generations_trail;
void remove_parents_from_cg_table(enode * r1);
void reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js);
void merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned *e2_generation_ptr);
void set_generation_sticky(enode * e, unsigned generation);
void invert_trans(enode * n);
theory_var get_closest_var(enode * n, theory_id th_id);
@ -1147,6 +1173,10 @@ namespace smt {
void propagate_bool_enode_assignment_core(enode * source, enode * target);
void undo_merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation);
void apply_sticky_updates(enode * e1, unsigned e1_generation, enode * e2, unsigned e2_generation);
void undo_add_eq(enode * r1, enode * n1, unsigned r2_num_parents);
void restore_theory_vars(enode * r2, enode * r1);
@ -1193,6 +1223,15 @@ namespace smt {
static bool is_eq(enode const * n1, enode const * n2) { return n1->get_root() == n2->get_root(); }
enode * get_cg_root(enode * n) const {
SASSERT(n->get_num_args() > 0);
if (!n->uses_cg_table())
return n->get_cg();
auto r = m_cg_table.find(n);
SASSERT(r != nullptr);
return r;
}
bool is_diseq(enode * n1, enode * n2) const;
bool is_diseq_slow(enode * n1, enode * n2) const;

46
src/smt/smt_enode.cpp
View file

@ -21,12 +21,12 @@ Revision History:
#include "smt/smt_enode.h"
namespace smt {
/**
\brief Initialize an enode in the given memory position.
*/
enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner,
bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent) {
SASSERT(m.is_bool(owner) || !merge_tf);
enode * n = new (mem) enode();
@ -35,7 +35,6 @@ namespace smt {
n->m_next = n;
n->m_cg = nullptr;
n->m_class_size = 1;
n->m_generation = generation;
n->m_func_decl_id = UINT_MAX;
n->m_mark = false;
n->m_mark2 = false;
@ -64,19 +63,19 @@ namespace smt {
return n;
}
enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner,
bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent) {
SASSERT(m.is_bool(owner) || !merge_tf);
unsigned sz = get_enode_size(suppress_args || !::is_app(owner) ? 0 : to_app(owner)->get_num_args());
void * mem = r.allocate(sz);
return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent);
return init(m, mem, app2enode, owner, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent);
}
enode * enode::mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner) {
unsigned sz = get_enode_size(owner->get_num_args());
void * mem = alloc_svect(char, sz);
return init(m, mem, app2enode, owner, 0, false, false, 0, true, false);
return init(m, mem, app2enode, owner, false, false, 0, true, false);
}
void enode::del_eh(ast_manager & m, bool update_children_parent) {
@ -131,20 +130,6 @@ namespace smt {
m_th_var_list.del_var(id);
}
/**
\brief Push old value of generation on the context trail stack
and update the generation.
*/
void enode::set_generation(context * ctx, unsigned generation) {
if (m_generation == generation)
return;
if (ctx)
ctx->push_trail(value_trail<unsigned>(m_generation));
m_generation = generation;
}
void enode::set_lbl_hash(context & ctx) {
SASSERT(m_lbl_hash == -1);
// m_lbl_hash should be different from -1, if and only if,
@ -161,16 +146,17 @@ namespace smt {
}
}
enode * enode::get_eq_enode_with_min_gen() {
if (m_generation == 0)
return this;
enode * enode::get_eq_enode_with_min_gen(context * ctx) {
enode * r = this;
enode * curr = this;
unsigned r_gen = ctx->get_generation(r);
do {
if (curr->m_generation < r->m_generation) {
unsigned curr_gen = ctx->get_generation(curr);
if (curr_gen == 0)
return curr;
if (curr_gen < r_gen) {
r = curr;
if (r->m_generation == 0)
return r;
r_gen = curr_gen;
}
curr = curr->m_next;
}
@ -307,10 +293,10 @@ namespace smt {
}
}
unsigned get_max_generation(unsigned num_enodes, enode * const * enodes) {
unsigned get_max_generation(context & ctx, unsigned num_enodes, enode * const * enodes) {
unsigned max = 0;
for (unsigned i = 0; i < num_enodes; ++i) {
unsigned curr = enodes[i]->get_generation();
unsigned curr = ctx.get_generation(enodes[i]);
if (curr > max)
max = curr;
}

27
src/smt/smt_enode.h
View file

@ -64,7 +64,6 @@ namespace smt {
enode * m_next; //!< Next element in the equivalence class.
enode * m_cg;
unsigned m_class_size; //!< Size of the equivalence class if the enode is the root.
unsigned m_generation; //!< Tracks how many quantifier instantiation rounds were needed to generate this enode.
unsigned m_func_decl_id; //!< Id generated by the congruence table for fast indexing.
@ -102,7 +101,7 @@ namespace smt {
approx_set m_lbls;
approx_set m_plbls;
enode * m_args[0]; //!< Cached args
friend class context;
friend class conflict_resolution;
friend class quantifier_manager;
@ -132,8 +131,8 @@ namespace smt {
friend class tmp_enode;
static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner,
bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent);
public:
@ -141,9 +140,9 @@ namespace smt {
return sizeof(enode) + num_args * sizeof(enode*);
}
static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent);
static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner,
bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent);
static enode * mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner);
@ -314,6 +313,10 @@ namespace smt {
return m_cg;
}
bool uses_cg_table() const {
return get_num_args() > 0 && is_cgc_enabled() && !is_true_eq();
}
bool is_cgc_enabled() const {
return m_cgc_enabled;
}
@ -393,18 +396,12 @@ namespace smt {
trans_justification get_trans_justification() {
return m_trans;
}
unsigned get_generation() const {
return m_generation;
}
void set_generation(context * ctx, unsigned generation);
/**
\brief Return the enode n that is in the eqc of *this, and has the minimal generation.
That is, there is no other enode with smaller generation.
*/
enode * get_eq_enode_with_min_gen();
enode * get_eq_enode_with_min_gen(context * ctx);
unsigned get_iscope_lvl() const {
return m_iscope_lvl;
@ -460,7 +457,7 @@ namespace smt {
return congruent(n1, n2, aux);
}
unsigned get_max_generation(unsigned num_enodes, enode * const * enodes);
unsigned get_max_generation(context & ctx, unsigned num_enodes, enode * const * enodes);
void unmark_enodes(unsigned num_enodes, enode * const * enodes);

80
src/smt/smt_internalizer.cpp
View file

@ -102,8 +102,66 @@ namespace smt {
}
void context::update_generation(enode * e) {
if (0 < m_generation && m_generation < e->get_generation())
e->set_generation(nullptr, m_generation);
// We don't support patterns with equality so there is no need to track generations for them.
if (e->is_eq())
return;
enode *cgr = e->get_num_args() == 0 ? e : get_cg_root(e);
if (0 < m_generation && m_generation < get_generation(cgr)) {
if (e->uses_cg_table())
set_generation_sticky(e, m_generation);
else
m_constant_generations[e] = m_generation; // Sticky by default. Won't unmerge
}
}
void context::set_generation(enode * e, unsigned generation) {
// We don't support patterns with equality so there is no need to track generations for them.
if (e->is_eq())
return;
if (e->uses_cg_table()) {
auto [cgr, cgc_gen] = m_cg_table.find_gen(e);
SASSERT(cgc_gen);
*cgc_gen = generation;
} else {
m_constant_generations[e] = generation;
}
}
class merge_cgc_generations_trail : public trail {
context& ctx;
enode* m_e1;
unsigned m_e1_generation;
enode* m_e2;
unsigned m_e2_generation;
public:
merge_cgc_generations_trail(context& ctx, enode* e1, unsigned e1_generation, enode* e2, unsigned e2_generation):
ctx(ctx),
m_e1(e1),
m_e1_generation(e1_generation),
m_e2(e2),
m_e2_generation(e2_generation) {
}
void undo() override {
ctx.undo_merge_cgc_generations(m_e1, m_e1_generation, m_e2, m_e2_generation);
}
};
void context::merge_cgc_generations(enode * e1, unsigned e1_generation, enode * e2, unsigned *e2_generation_ptr) {
// We assume the congruence has already been updated. We might want to move that here, too.
SASSERT(e2->is_cgr());
SASSERT(!m_cg_table.contains_ptr(e1));
SASSERT(m_cg_table.contains_ptr(e2));
// Push trail even if we have a no-op. Otherwise we can't restore e1's generation after unmerging.
push_trail(merge_cgc_generations_trail(*this, e1, e1_generation, e2, *e2_generation_ptr));
if (e1_generation >= *e2_generation_ptr)
return; // no-op
*e2_generation_ptr = e1_generation;
}
void context::ts_visit_child(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo, bool & visited) {
@ -1002,7 +1060,7 @@ namespace smt {
CTRACE(cached_generation, generation != m_generation,
tout << "cached_generation: #" << n->get_id() << " " << generation << " " << m_generation << "\n";);
}
enode *e = enode::mk(m, get_region(), m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl,
enode *e = enode::mk(m, get_region(), m_app2enode, to_app(n), suppress_args, merge_tf, m_scope_lvl,
cgc_enabled, true);
TRACE(mk_enode_detail, tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
if (m.is_unique_value(n))
@ -1022,8 +1080,11 @@ namespace smt {
}
else {
if (cgc_enabled) {
auto [e_prime, used_commutativity] = m_cg_table.insert(e);
auto [e_prime, used_commutativity, sibling_gen_ptr] = m_cg_table.insert(e, generation);
if (e != e_prime) {
// We don't support patterns with equality so there is no need to track generations for them.
if (!e->is_eq())
merge_cgc_generations(e, generation, e_prime, sibling_gen_ptr);
e->m_cg = e_prime;
push_new_congruence(e, e_prime, used_commutativity);
}
@ -1032,6 +1093,8 @@ namespace smt {
}
}
else {
SASSERT(!e->uses_cg_table());
m_constant_generations.insert(e, generation);
e->m_cg = e;
}
}
@ -1041,7 +1104,10 @@ namespace smt {
m_decl2enodes.resize(decl_id+1);
m_decl2enodes[decl_id].push_back(e);
}
} else {
m_constant_generations.insert(e, generation);
}
SASSERT(e_internalized(n));
m_stats.m_num_mk_enode++;
TRACE(mk_enode, tout << "created enode: #" << e->get_owner_id() << " for:\n" << mk_pp(n, m) << "\n";
@ -1066,10 +1132,11 @@ namespace smt {
unsigned n_id = n->get_id();
enode * e = m_app2enode[n_id];
m_app2enode[n_id] = nullptr;
if (e->is_cgr() && !e->is_true_eq() && e->is_cgc_enabled()) {
if (e->is_cgr() && e->uses_cg_table()) {
SASSERT(m_cg_table.contains_ptr(e));
m_cg_table.erase(e);
}
SASSERT(!(e->get_num_args() > 0 && m_cg_table.contains_ptr(e)));
if (e->get_num_args() > 0 && !e->is_eq()) {
unsigned decl_id = e->get_decl_id();
SASSERT(decl_id < m_decl2enodes.size());
@ -1080,6 +1147,9 @@ namespace smt {
SASSERT(m_e_internalized_stack.size() == m_enodes.size());
m_enodes.pop_back();
m_e_internalized_stack.pop_back();
m_sticky_generation_updates.erase(e);
if (!e->uses_cg_table())
m_constant_generations.erase(e);
}
/**

2
src/smt/smt_model_checker.cpp
View file

@ -109,7 +109,7 @@ namespace smt {
for (auto const& kv : *m_root2value) {
enode * n = kv.m_key;
expr * val = kv.m_value;
n = n->get_eq_enode_with_min_gen();
n = n->get_eq_enode_with_min_gen(m_context);
expr* e = n->get_expr();
if (!m.is_value(e))
m_value2expr.insert(val, e);

12
src/smt/smt_model_finder.cpp
View file

@ -1235,7 +1235,7 @@ namespace smt {
// a necessary instantiation.
enode* e_arg = n->get_arg(m_arg_i);
expr* arg = e_arg->get_expr();
A_f_i->insert(arg, e_arg->get_generation());
A_f_i->insert(arg, ctx->get_generation(e_arg));
}
}
}
@ -1253,7 +1253,7 @@ namespace smt {
if (ctx->is_relevant(n)) {
enode* e_arg = n->get_arg(m_arg_i);
expr* arg = e_arg->get_expr();
s->insert(arg, e_arg->get_generation());
s->insert(arg, ctx->get_generation(e_arg));
}
}
}
@ -1309,7 +1309,7 @@ namespace smt {
bv_rw.mk_sub(arg, m_offset, arg_minus_k);
else
arith_rw.mk_sub(arg, m_offset, arg_minus_k);
S_j->insert(arg_minus_k, e_arg->get_generation());
S_j->insert(arg_minus_k, ctx->get_generation(e_arg));
}
}
}
@ -1421,7 +1421,7 @@ namespace smt {
auto e = n->get_expr();
if (srt == n->get_sort()) {
TRACE(model_finder, tout << "inserting " << mk_pp(e, m) << " into inst set\n");
S->insert(e, n->get_generation());
S->insert(e, ctx->get_generation(n));
}
else if (is_app(e) && to_app(e)->get_decl()->is_skolem())
;
@ -1557,7 +1557,7 @@ namespace smt {
if (ctx->is_relevant(p) && p->get_decl() == m_select->get_decl()) {
SASSERT(m_arg_i < p->get_num_args());
enode* e_arg = p->get_arg(m_arg_i);
A_f_i->insert(e_arg->get_expr(), e_arg->get_generation());
A_f_i->insert(e_arg->get_expr(), ctx->get_generation(e_arg));
}
}
}
@ -1686,7 +1686,7 @@ namespace smt {
node* S_q_i = slv.get_uvar(q, m_var_i);
for (enode* n : ctx->enodes()) {
if (ctx->is_relevant(n) && n->get_expr()->get_sort() == s) {
S_q_i->insert(n->get_expr(), n->get_generation());
S_q_i->insert(n->get_expr(), ctx->get_generation(n));
}
}
}

11
src/smt/smt_quantifier.cpp
View file

@ -250,15 +250,12 @@ namespace smt {
trace_stream() << "\n";
} else {
std::ostream & out = trace_stream();
obj_hashtable<enode> already_visited;
// In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables
// is used. We need to make sure that all of these equalities appear in the log.
for (unsigned i = 0; i < num_bindings; ++i) {
log_justification_to_root(out, bindings[i], already_visited, m_context, m());
}
for (auto n : used_enodes) {
enode *orig = std::get<0>(n);
enode *substituted = std::get<1>(n);
@ -267,7 +264,6 @@ namespace smt {
log_justification_to_root(out, substituted, already_visited, m_context, m());
}
}
// At this point all relevant equalities for the match are logged.
out << "[new-match] " << f->get_data_hash() << " #" << q->get_id() << " #" << pat->get_id();
for (unsigned i = 0; i < num_bindings; ++i) {
@ -288,7 +284,7 @@ namespace smt {
out << "\n";
}
}
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
@ -709,8 +705,9 @@ namespace smt {
}
enode* n = m_context->get_enode(e);
new_bindings.push_back(n);
if (n->get_generation() > max_gen)
max_gen = n->get_generation();
unsigned gen = m_context->get_generation(n);
if (gen > max_gen)
max_gen = gen;
}
TRACE(ho_matching,

4
src/smt/smt_quick_checker.cpp
View file

@ -235,8 +235,8 @@ namespace smt {
TRACE(quick_checker, tout << "found new candidate\n";);
TRACE(quick_checker_sizes, tout << "found new candidate\n";
for (unsigned i = 0; i < m_num_bindings; ++i) tout << "#" << m_bindings[i]->get_owner_id() << " "; tout << "\n";);
unsigned max_generation = get_max_generation(m_num_bindings, m_bindings.data());
if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(),
unsigned max_generation = get_max_generation(m_context, m_num_bindings, m_bindings.data());
if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(),
max_generation,
0, // min_top_generation is only available for instances created by the MAM
0, // max_top_generation is only available for instances created by the MAM

2
src/util/chashtable.h
View file

@ -484,7 +484,7 @@ public:
unsigned idx = h & mask;
cell * c = m_table + idx;
if (c->is_free())
return;
return;
cell * prev = nullptr;
do {
if (equals(c->m_data, d)) {