mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-09 23:42:21 +00:00
Code Activity

Make axiom profiler logs reflect binding rewrites to eclass root (#10446)

Browse source 
Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
This commit is contained in:
Can Cebeci 2026-08-07 13:53:43 -07:00 • committed by GitHub
parent b9b1249d14
commit a88e7e3e3e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 20 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/smt/smt_quantifier.cpp
View file

@ -246,7 +246,7 @@ namespace smt {
if (pat == nullptr) {
trace_stream() << "[inst-discovered] MBQI " << f->get_data_hash() << " #" << q->get_id();
for (unsigned i = 0; i < num_bindings; ++i) {
trace_stream() << " #" << bindings[num_bindings - i - 1]->get_owner_id();
trace_stream() << " #" << f->get_arg(num_bindings - i - 1)->get_owner_id();
}
trace_stream() << "\n";
} else {
@ -269,7 +269,7 @@ namespace smt {
for (unsigned i = 0; i < num_bindings; ++i) {
// I don't want to use mk_pp because it creates expressions for pretty printing.
// This nasty side-effect may change the behavior of Z3.
out << " #" << bindings[num_bindings - i - 1]->get_owner_id();
out << " #" << f->get_arg(num_bindings - i - 1)->get_owner_id();
}
out << " ;";
for (auto n : used_enodes) {
@ -307,11 +307,27 @@ namespace smt {
get_stat(q)->update_max_generation(max_generation);
fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings);
if (f) {
vector<std::tuple<enode *, enode *>> trace_used_enodes(used_enodes);
for (unsigned i = 0; i < num_bindings; ++i) {
enode * orig = bindings[i];
enode * root = f->get_arg(i);
if (orig == root)
continue;
bool found = false;
for (auto [used_orig, used_substituted] : trace_used_enodes) {
if (used_orig == orig && used_substituted == root) {
found = true;
break;
}
}
if (!found)
trace_used_enodes.push_back(std::make_tuple(orig, root));
}
if (is_trace_enabled(TraceTag::causality)) {
log_causality(f,pat,used_enodes);
log_causality(f, pat, trace_used_enodes);
}
if (has_trace_stream()) {
log_add_instance(f, q, pat, num_bindings, bindings, used_enodes);
log_add_instance(f, q, pat, num_bindings, bindings, trace_used_enodes);
}
m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
m_num_instances++;