mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fixing rewrite logging (https://bitbucket.org/viperproject/axiom-profiler/issues/13/version-486-of-z3-not-compatible-with)

Browse source
This commit is contained in:
Nils Becker 2019-07-10 16:17:30 +02:00
parent 88aa689a70
commit 23d01f5974
1 changed files with 33 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/ast/rewriter/th_rewriter.cpp
View file

@ -34,6 +34,8 @@ Notes:
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "ast/well_sorted.h"
#include "ast/ast.h"
#include <map>
namespace {
struct th_rewriter_cfg : public default_rewriter_cfg {
@ -557,6 +559,28 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
return BR_DONE;
}
void count_subterm_references(expr * e, map<expr *, unsigned, ptr_hash<expr>, ptr_eq<expr>> & reference_map) {
if (is_app(e)) {
app * a = to_app(e);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
expr * child = a->get_arg(i);
reference_map.insert(child, reference_map.get(child, 0) + 1);
}
}
}
void log_enodes_for_new_terms(expr *term) {
map<expr *, unsigned, ptr_hash<expr>, ptr_eq<expr>> reference_map;
count_subterm_references(term, reference_map);
// Any term that was newly introduced by the rewrite step is only referenced within the result term.
for (auto kv : reference_map) {
if (kv.m_key->get_ref_count() == kv.m_value) {
m().trace_stream() << "[attach-enode] #" << kv.m_key->get_id() << " 0\n";
}
}
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = nullptr;
br_status st = reduce_app_core(f, num, args, result);
@ -581,8 +605,15 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
result_pr = m().mk_rewrite(tmp, result);
tmp = m().mk_eq(tmp, result);
m().trace_stream() << "[instance] " << static_cast<void *>(nullptr) << " #" << tmp->get_id() << "\n";
m().trace_stream() << "[attach-enode] #" << result->get_id() << " 0\n";
m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n";
// Make sure that both the result term and equality were newly introduced.
if (tmp->get_ref_count() == 1) {
if (result->get_ref_count() == 1) {
log_enodes_for_new_terms(result);
m().trace_stream() << "[attach-enode] #" << result->get_id() << " 0\n";
}
m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n";
}
m().trace_stream() << "[end-of-instance]\n";
m().trace_stream().flush();
}