mirror of
https://github.com/Z3Prover/z3
synced 2025-08-22 11:07:51 +00:00
0a93ff515d
* 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).
88 lines
3 KiB
C++
88 lines
3 KiB
C++
/*++
|
|
Copyright (c) 2012 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
fpa2bv_model_converter.h
|
|
|
|
Abstract:
|
|
|
|
Model conversion for fpa2bv_converter
|
|
|
|
Author:
|
|
|
|
Christoph (cwinter) 2012-02-09
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
#include "ast/ast_smt2_pp.h"
|
|
#include "ast/rewriter/fpa_rewriter.h"
|
|
#include "tactic/fpa/fpa2bv_model_converter.h"
|
|
|
|
void fpa2bv_model_converter::display(std::ostream & out) {
|
|
out << "(fpa2bv-model-converter";
|
|
m_bv2fp->display(out);
|
|
out << ")";
|
|
}
|
|
|
|
model_converter * fpa2bv_model_converter::translate(ast_translation & translator) {
|
|
fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to());
|
|
res->m_bv2fp = m_bv2fp->translate(translator);
|
|
return res;
|
|
}
|
|
|
|
void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
|
|
TRACE(fpa2bv_mc, tout << "BV Model: " << std::endl;
|
|
for (unsigned i = 0; i < mc->get_num_constants(); i++)
|
|
tout << mc->get_constant(i)->get_name() << " --> " <<
|
|
mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl;
|
|
for (unsigned i = 0; i < mc->get_num_functions(); i++) {
|
|
func_decl * f = mc->get_function(i);
|
|
tout << f->get_name() << "(...) := " << std::endl;
|
|
func_interp * fi = mc->get_func_interp(f);
|
|
for (unsigned j = 0; j < fi->num_entries(); j++) {
|
|
func_entry const * fe = fi->get_entry(j);
|
|
for (unsigned k = 0; k < f->get_arity(); k++)
|
|
tout << mk_ismt2_pp(fe->get_arg(k), m) << " ";
|
|
tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl;
|
|
}
|
|
tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
|
|
});
|
|
|
|
obj_hashtable<func_decl> seen;
|
|
m_bv2fp->convert_consts(mc, float_mdl, seen);
|
|
m_bv2fp->convert_rm_consts(mc, float_mdl, seen);
|
|
m_bv2fp->convert_min_max_specials(mc, float_mdl, seen);
|
|
m_bv2fp->convert_uf2bvuf(mc, float_mdl, seen);
|
|
|
|
// Keep all the non-float constants.
|
|
unsigned sz = mc->get_num_constants();
|
|
for (unsigned i = 0; i < sz; i++) {
|
|
func_decl * c = mc->get_constant(i);
|
|
if (!seen.contains(c))
|
|
float_mdl->register_decl(c, mc->get_const_interp(c));
|
|
}
|
|
|
|
// And keep everything else
|
|
sz = mc->get_num_functions();
|
|
for (unsigned i = 0; i < sz; i++) {
|
|
func_decl * f = mc->get_function(i);
|
|
if (!seen.contains(f)) {
|
|
TRACE(fpa2bv_mc, tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;);
|
|
func_interp * val = mc->get_func_interp(f)->copy();
|
|
float_mdl->register_decl(f, val);
|
|
}
|
|
}
|
|
|
|
sz = mc->get_num_uninterpreted_sorts();
|
|
for (unsigned i = 0; i < sz; i++) {
|
|
sort * s = mc->get_uninterpreted_sort(i);
|
|
ptr_vector<expr> u = mc->get_universe(s);
|
|
float_mdl->register_usort(s, u.size(), u.data());
|
|
}
|
|
}
|
|
|
|
model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv) {
|
|
return alloc(fpa2bv_model_converter, m, conv);
|
|
}
|