mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-25 04:26:00 +00:00
Code Activity
z3/src/ast/ast_translation.cpp
LeeYoungJoon 0a93ff515d
Centralize and document TRACE tags using X-macros (#7657) 
* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros

* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md

* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled

* trace: improve trace tag handling system with hierarchical tagging

- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
  (class names and descriptions to be refined in a future update)

* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals

* trace : add cstring header

* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py

* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.

* trace : Add TODO comment for future implementation of tag_class activation

* trace : Disable code related to tag_class until implementation is ready (#7663).
2025-05-28 14:31:25 +01:00

372 lines
14 KiB
C++
Raw Blame History

/*++
Copyright (c) 2008 Microsoft Corporation
Module Name:
ast_translation.cpp
Abstract:
AST translation functions
Author:
Christoph Wintersteiger (t-cwinte) 2008-11-20
Revision History:
--*/
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/array_decl_plugin.h"
#include "ast/format.h"
#include "ast/ast_translation.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
ast_translation::~ast_translation() {
reset_cache();
}
void ast_translation::cleanup() {
reset_cache();
m_cache.finalize();
m_result_stack.finalize();
m_frame_stack.finalize();
m_extra_children_stack.finalize();
}
void ast_translation::reset_cache() {
for (auto & kv : m_cache) {
m_from_manager.dec_ref(kv.m_key);
m_to_manager.dec_ref(kv.m_value);
}
m_cache.reset();
}
void ast_translation::cache(ast * s, ast * t) {
SASSERT(!m_cache.contains(s));
if (s->get_ref_count() > 1) {
m_from_manager.inc_ref(s);
m_to_manager.inc_ref(t);
m_cache.insert(s, t);
++m_insert_count;
}
}
void ast_translation::collect_decl_extra_children(decl * d) {
unsigned num_params = d->get_num_parameters();
for (unsigned i = 0; i < num_params; i++) {
parameter const & p = d->get_parameter(i);
if (p.is_ast())
m_extra_children_stack.push_back(p.get_ast());
}
}
void ast_translation::push_frame(ast * n) {
// ensure poly roots are pushed first.
if (m_from_manager.has_type_vars() && n->get_kind() == AST_FUNC_DECL && to_func_decl(n)->is_polymorphic()) {
func_decl* g = m_from_manager.poly_root(to_func_decl(n));
if (n != g && m_cache.contains(g)) {
m_frame_stack.push_back(frame(n, 0, m_extra_children_stack.size(), m_result_stack.size()));
}
}
m_frame_stack.push_back(frame(n, 0, m_extra_children_stack.size(), m_result_stack.size()));
switch (n->get_kind()) {
case AST_SORT:
case AST_FUNC_DECL:
collect_decl_extra_children(to_decl(n));
break;
default:
break;
}
}
bool ast_translation::visit(ast * n) {
if (n->get_ref_count() > 1) {
ast * r;
if (m_cache.find(n, r)) {
m_result_stack.push_back(r);
++m_hit_count;
return true;
}
else {
++m_miss_count;
}
}
push_frame(n);
return false;
}
void ast_translation::copy_params(decl * d, unsigned rpos, buffer<parameter> & ps) {
unsigned num = d->get_num_parameters();
unsigned j = rpos;
for (unsigned i = 0; i < num; i++) {
parameter const & p = d->get_parameter(i);
if (p.is_ast()) {
ps.push_back(parameter(m_result_stack[j]));
j++;
}
else if (p.is_external()) {
SASSERT(d->get_family_id() != null_family_id);
decl_plugin & from_plugin = *(m_from_manager.get_plugin(d->get_family_id()));
decl_plugin & to_plugin = *(m_to_manager.get_plugin(d->get_family_id()));
ps.push_back(from_plugin.translate(p, to_plugin));
}
else {
ps.push_back(p);
}
}
}
void ast_translation::mk_sort(sort * s, frame & fr) {
sort_info * si = s->get_info();
sort * new_s;
if (si == nullptr) {
// TODO: investigate: this branch is probably unreachable.
// It became unreachable after we started using mk_uninterpreted_sort for creating uninterpreted sorts,
// and mk_uninterpreted_sort actually creates a user_sort.
new_s = m_to_manager.mk_uninterpreted_sort(s->get_name());
SASSERT(m_result_stack.size() == fr.m_rpos);
}
else {
buffer<parameter> ps;
copy_params(s, fr.m_rpos, ps);
new_s = m_to_manager.mk_sort(s->get_name(), sort_info(si->get_family_id(),
si->get_decl_kind(),
si->get_num_elements(),
si->get_num_parameters(),
ps.data(),
s->private_parameters()));
}
m_result_stack.shrink(fr.m_rpos);
m_result_stack.push_back(new_s);
m_extra_children_stack.shrink(fr.m_cpos);
cache(s, new_s);
m_frame_stack.pop_back();
}
void ast_translation::mk_func_decl(func_decl * f, frame & fr) {
func_decl_info * fi = f->get_info();
SASSERT(fr.m_cpos <= m_extra_children_stack.size());
unsigned num_extra = m_extra_children_stack.size() - fr.m_cpos;
sort ** new_domain = reinterpret_cast<sort**>(m_result_stack.data() + fr.m_rpos + num_extra);
sort * new_range = static_cast<sort*>(m_result_stack.back());
func_decl * new_f;
if (fi == nullptr) {
new_f = m_to_manager.mk_func_decl(f->get_name(),
f->get_arity(),
new_domain,
new_range);
}
else if (f->is_polymorphic() && m_from_manager.poly_root(f) != f) {
func_decl* fr = to_func_decl(m_cache[m_from_manager.poly_root(f)]);
new_f = m_to_manager.instantiate_polymorphic(fr, f->get_arity(), new_domain, new_range);
}
else {
buffer<parameter> ps;
copy_params(f, fr.m_rpos, ps);
func_decl_info new_fi(fi->get_family_id(),
fi->get_decl_kind(),
fi->get_num_parameters(),
ps.data());
new_fi.set_left_associative(fi->is_left_associative());
new_fi.set_right_associative(fi->is_right_associative());
new_fi.set_flat_associative(fi->is_flat_associative());
new_fi.set_commutative(fi->is_commutative());
new_fi.set_chainable(fi->is_chainable());
new_fi.set_pairwise(fi->is_pairwise());
new_fi.set_injective(fi->is_injective());
new_fi.set_skolem(fi->is_skolem());
new_fi.set_idempotent(fi->is_idempotent());
new_fi.set_lambda(fi->is_lambda());
new_f = m_to_manager.mk_func_decl(f->get_name(),
f->get_arity(),
new_domain,
new_range,
new_fi);
if (new_fi.is_lambda()) {
quantifier* q = from().is_lambda_def(f);
ast_translation tr(from(), to());
quantifier* new_q = tr(q);
to().add_lambda_def(new_f, new_q);
}
}
TRACE(ast_translation,
tout << f->get_name() << " "; if (fi) tout << *fi; tout << "\n";
tout << "---->\n";
tout << new_f->get_name() << " "; if (new_f->get_info()) tout << *(new_f->get_info()); tout << "\n";);
m_result_stack.shrink(fr.m_rpos);
m_result_stack.push_back(new_f);
m_extra_children_stack.shrink(fr.m_cpos);
cache(f, new_f);
m_frame_stack.pop_back();
}
ast * ast_translation::process(ast const * _n) {
if (!_n) return nullptr;
SASSERT(m_result_stack.empty());
SASSERT(m_frame_stack.empty());
SASSERT(m_extra_children_stack.empty());
++m_num_process;
if (m_num_process > (1 << 14)) {
reset_cache();
m_num_process = 0;
}
if (!visit(const_cast<ast*>(_n))) {
while (!m_frame_stack.empty()) {
loop:
++m_loop_count;
frame & fr = m_frame_stack.back();
ast * n = fr.m_n;
ast * r;
TRACE(ast_translation, tout << mk_ll_pp(n, m_from_manager, false) << "\n";);
if (fr.m_idx == 0 && n->get_ref_count() > 1) {
if (m_cache.find(n, r)) {
SASSERT(m_result_stack.size() == fr.m_rpos);
m_result_stack.push_back(r);
m_extra_children_stack.shrink(fr.m_cpos);
m_frame_stack.pop_back();
TRACE(ast_translation, tout << "hit\n";);
m_hit_count++;
continue;
}
else {
m_miss_count++;
}
}
switch (n->get_kind()) {
case AST_VAR: {
if (fr.m_idx == 0) {
fr.m_idx = 1;
if (!visit(to_var(n)->get_sort()))
goto loop;
}
sort * new_s = to_sort(m_result_stack.back());
var * new_var = m_to_manager.mk_var(to_var(n)->get_idx(), new_s);
m_result_stack.pop_back();
m_result_stack.push_back(new_var);
cache(n, new_var);
m_frame_stack.pop_back();
break;
}
case AST_APP: {
if (fr.m_idx == 0) {
fr.m_idx = 1;
if (!visit(to_app(n)->get_decl()))
goto loop;
}
unsigned num = to_app(n)->get_num_args();
while (fr.m_idx <= num) {
expr * arg = to_app(n)->get_arg(fr.m_idx - 1);
fr.m_idx++;
if (!visit(arg))
goto loop;
}
func_decl * new_f = to_func_decl(m_result_stack[fr.m_rpos]);
expr ** new_args = reinterpret_cast<expr **>(m_result_stack.data() + fr.m_rpos + 1);
expr * new_app = m_to_manager.mk_app(new_f, num, new_args);
m_result_stack.shrink(fr.m_rpos);
m_result_stack.push_back(new_app);
cache(n, new_app);
m_frame_stack.pop_back();
break;
}
case AST_QUANTIFIER: {
unsigned num_decls = to_quantifier(n)->get_num_decls();
unsigned num = num_decls + to_quantifier(n)->get_num_children();
while (fr.m_idx < num) {
ast * child;
if (fr.m_idx < num_decls)
child = to_quantifier(n)->get_decl_sort(fr.m_idx);
else
child = to_quantifier(n)->get_child(fr.m_idx - num_decls);
fr.m_idx++;
if (!visit(child))
goto loop;
}
symbol const * dnames = to_quantifier(n)->get_decl_names();
sort ** dsorts = reinterpret_cast<sort**>(m_result_stack.data() + fr.m_rpos);
expr * body = static_cast<expr*>(m_result_stack[fr.m_rpos + num_decls]);
unsigned num_pats = to_quantifier(n)->get_num_patterns();
expr ** pats = reinterpret_cast<expr**>(m_result_stack.data() + fr.m_rpos + num_decls + 1);
unsigned num_no_pats = to_quantifier(n)->get_num_no_patterns();
expr ** no_pats = pats + num_pats;
quantifier * new_q = m_to_manager.mk_quantifier(to_quantifier(n)->get_kind(),
num_decls,
dsorts,
dnames,
body,
to_quantifier(n)->get_weight(),
to_quantifier(n)->get_qid(),
to_quantifier(n)->get_skid(),
num_pats, pats,
num_no_pats, no_pats);
m_result_stack.shrink(fr.m_rpos);
m_result_stack.push_back(new_q);
cache(n, new_q);
m_frame_stack.pop_back();
break;
}
case AST_SORT: {
SASSERT(fr.m_cpos <= m_extra_children_stack.size());
unsigned num = m_extra_children_stack.size() - fr.m_cpos;
while (fr.m_idx < num) {
ast * c = m_extra_children_stack[fr.m_cpos + fr.m_idx];
fr.m_idx++;
if (!visit(c))
goto loop;
}
mk_sort(to_sort(n), fr);
break;
}
case AST_FUNC_DECL: {
SASSERT(fr.m_cpos <= m_extra_children_stack.size());
unsigned num_extra = m_extra_children_stack.size() - fr.m_cpos;
unsigned arity = to_func_decl(n)->get_arity();
unsigned num = num_extra + arity + 1;
while (fr.m_idx < num) {
ast * c;
if (fr.m_idx < num_extra)
c = m_extra_children_stack[fr.m_cpos + fr.m_idx];
else if (fr.m_idx < num_extra + arity)
c = to_func_decl(n)->get_domain(fr.m_idx - num_extra);
else
c = to_func_decl(n)->get_range();
fr.m_idx++;
if (!visit(c))
goto loop;
}
mk_func_decl(to_func_decl(n), fr);
break;
}
default:
UNREACHABLE();
break;
}
}
}
SASSERT(m_result_stack.size() == 1);
ast * r = m_result_stack.back();
m_result_stack.reset();
return r;
}
expr_dependency * expr_dependency_translation::operator()(expr_dependency * d) {
if (d == nullptr)
return d;
m_buffer.reset();
m_translation.from().linearize(d, m_buffer);
unsigned sz = m_buffer.size();
SASSERT(sz >= 1);
for (unsigned i = 0; i < sz; i++) {
m_buffer[i] = m_translation(m_buffer[i]);
}
return m_translation.to().mk_join(sz, m_buffer.data());
}
View git blame Copy permalink