mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 12:28:44 +00:00
logging meaning of theory specific constants
This commit is contained in:
Nils Becker
nilsbecker
parent
988e8afc2e
commit
0870760eb5
|
|
@ -89,7 +89,14 @@ app * arith_decl_plugin::mk_numeral(algebraic_numbers::anum const & val, bool is
|
|||
parameter p(idx, true);
|
||||
SASSERT(p.is_external());
|
||||
func_decl * decl = m_manager->mk_const_decl(m_rootv_sym, m_real_decl, func_decl_info(m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM, 1, &p));
|
||||
return m_manager->mk_const(decl);
|
||||
app * r = m_manager->mk_const(decl);
|
||||
|
||||
if (log_constant_meaning_prelude(r)) {
|
||||
am().display_root(m_manager->trace_stream(), val);
|
||||
m_manager->trace_stream() << "\n";
|
||||
}
|
||||
|
||||
return r;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -415,7 +422,12 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
|
|||
r = m_manager->mk_const(m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, 2, p)));
|
||||
m_manager->inc_ref(r);
|
||||
m_small_ints.setx(u_val, r, 0);
|
||||
|
||||
if (log_constant_meaning_prelude(r)) {
|
||||
m_manager->trace_stream() << u_val << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
return r;
|
||||
}
|
||||
else {
|
||||
|
|
@ -425,6 +437,10 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
|
|||
r = m_manager->mk_const(m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, 2, p)));
|
||||
m_manager->inc_ref(r);
|
||||
m_small_reals.setx(u_val, r, 0);
|
||||
|
||||
if (log_constant_meaning_prelude(r)) {
|
||||
m_manager->trace_stream() << u_val << "\n";
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
|
@ -436,7 +452,14 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
|
|||
decl = m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, 2, p));
|
||||
else
|
||||
decl = m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, 2, p));
|
||||
return m_manager->mk_const(decl);
|
||||
app * r = m_manager->mk_const(decl);
|
||||
|
||||
if (log_constant_meaning_prelude(r)) {
|
||||
val.display(m_manager->trace_stream());
|
||||
m_manager->trace_stream() << "\n";
|
||||
}
|
||||
|
||||
return r;
|
||||
}
|
||||
|
||||
func_decl * arith_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity) {
|
||||
|
|
|
|||
|
|
@ -662,6 +662,23 @@ ast* ast_table::pop_erase() {
|
|||
//
|
||||
// -----------------------------------
|
||||
|
||||
/**
|
||||
\brief Checks wether a log is being generated and, if necessary, adds the beginning of an "[attach-meaning]" line
|
||||
to that log. The theory solver should add some description of the meaning of the term in terms of the theory's
|
||||
internal reasoning to the end of the line and insert a line break.
|
||||
|
||||
\param a the term that should be described.
|
||||
|
||||
\return true if a log is being generated, false otherwise.
|
||||
*/
|
||||
bool decl_plugin::log_constant_meaning_prelude(app * a) {
|
||||
if (m_manager->has_trace_stream()) {
|
||||
m_manager->trace_stream() << "[attach-meaning] #" << a->get_id() << " " << m_manager->get_family_name(m_family_id).str() << " ";
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
func_decl * decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned num_args, expr * const * args, sort * range) {
|
||||
ptr_buffer<sort> sorts;
|
||||
|
|
|
|||
|
|
@ -998,6 +998,17 @@ protected:
|
|||
|
||||
virtual void inherit(decl_plugin* other_p, ast_translation& ) { }
|
||||
|
||||
/**
|
||||
\brief Checks wether a log is being generated and, if necessary, adds the beginning of an "[attach-meaning]" line
|
||||
to that log. The theory solver should add some description of the meaning of the term in terms of the theory's
|
||||
internal reasoning to the end of the line and insert a line break.
|
||||
|
||||
\param a the term that should be described.
|
||||
|
||||
\return true if a log is being generated, false otherwise.
|
||||
*/
|
||||
bool log_constant_meaning_prelude(app * a);
|
||||
|
||||
friend class ast_manager;
|
||||
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -864,7 +864,15 @@ app * bv_util::mk_numeral(rational const & val, sort* s) const {
|
|||
|
||||
app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const {
|
||||
parameter p[2] = { parameter(val), parameter(static_cast<int>(bv_size)) };
|
||||
return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr);
|
||||
app * r = m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr);
|
||||
|
||||
if (m_plugin->log_constant_meaning_prelude(r)) {
|
||||
m_manager.trace_stream() << "(" << bv_size << " #d";
|
||||
val.display(m_manager.trace_stream());
|
||||
m_manager.trace_stream() << ")\n";
|
||||
}
|
||||
|
||||
return r;
|
||||
}
|
||||
|
||||
sort * bv_util::mk_sort(unsigned bv_size) {
|
||||
|
|
@ -883,3 +891,32 @@ app * bv_util::mk_bv2int(expr* e) {
|
|||
parameter p(s);
|
||||
return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e);
|
||||
}
|
||||
|
||||
|
||||
app * bv_util::mk_bv(unsigned n, expr* const* es) {
|
||||
app * r = m_manager.mk_app(get_fid(), OP_MKBV, n, es);
|
||||
|
||||
if (m_plugin->log_constant_meaning_prelude(r)) {
|
||||
m_manager.trace_stream() << "(" << n << " #x";
|
||||
|
||||
m_manager.trace_stream() << std::hex;
|
||||
uint8_t hexDigit = 0;
|
||||
unsigned curLength = (4 - n % 4) % 4;
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
hexDigit << 1;
|
||||
++curLength;
|
||||
if (m_manager.is_true(es[i])) {
|
||||
hexDigit |= 1;
|
||||
}
|
||||
if (curLength == 4) {
|
||||
m_manager.trace_stream() << hexDigit;
|
||||
hexDigit = 0;
|
||||
}
|
||||
}
|
||||
m_manager.trace_stream() << std::dec;
|
||||
|
||||
m_manager.trace_stream() << ")\n";
|
||||
}
|
||||
|
||||
return r;
|
||||
}
|
||||
|
|
@ -238,6 +238,8 @@ protected:
|
|||
func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity);
|
||||
|
||||
void get_offset_term(app * a, expr * & t, rational & offset) const;
|
||||
|
||||
friend class bv_util;
|
||||
public:
|
||||
bv_decl_plugin();
|
||||
|
||||
|
|
@ -432,7 +434,7 @@ public:
|
|||
app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); }
|
||||
app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); }
|
||||
|
||||
app * mk_bv(unsigned n, expr* const* es) { return m_manager.mk_app(get_fid(), OP_MKBV, n, es); }
|
||||
app * mk_bv(unsigned n, expr* const* es);
|
||||
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -92,7 +92,13 @@ func_decl * fpa_decl_plugin::mk_numeral_decl(mpf const & v) {
|
|||
}
|
||||
|
||||
app * fpa_decl_plugin::mk_numeral(mpf const & v) {
|
||||
return m_manager->mk_const(mk_numeral_decl(v));
|
||||
app * r = m_manager->mk_const(mk_numeral_decl(v));
|
||||
|
||||
if (log_constant_meaning_prelude(r)) {
|
||||
m_manager->trace_stream() << "(" << m_fm.to_string(v) << ")\n";
|
||||
}
|
||||
|
||||
return r;
|
||||
}
|
||||
|
||||
bool fpa_decl_plugin::is_numeral(expr * n, mpf & val) {
|
||||
|
|
|
|||
|
|
@ -210,7 +210,7 @@ namespace smt {
|
|||
get_stat(q)->update_max_generation(max_generation);
|
||||
fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def);
|
||||
if (f) {
|
||||
if (has_trace_stream()) {
|
||||
if (has_trace_stream() && pat != nullptr) {
|
||||
std::ostream & out = trace_stream();
|
||||
|
||||
obj_hashtable<enode> already_visited;
|
||||
|
|
|
|||
Loading…
Reference in a new issue