From 0870760eb5d8c160dd2423fed77a53635e04e3ae Mon Sep 17 00:00:00 2001 From: Nils Becker Date: Mon, 3 Dec 2018 22:39:29 +0100 Subject: [PATCH] logging meaning of theory specific constants --- src/ast/arith_decl_plugin.cpp | 27 ++++++++++++++++++++++-- src/ast/ast.cpp | 17 +++++++++++++++ src/ast/ast.h | 11 ++++++++++ src/ast/bv_decl_plugin.cpp | 39 ++++++++++++++++++++++++++++++++++- src/ast/bv_decl_plugin.h | 4 +++- src/ast/fpa_decl_plugin.cpp | 8 ++++++- src/smt/smt_quantifier.cpp | 2 +- 7 files changed, 102 insertions(+), 6 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index cdf18875c..926e515e2 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -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) { diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 067c4d127..178113ea7 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -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 sorts; diff --git a/src/ast/ast.h b/src/ast/ast.h index b81db5196..9c6c811b0 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -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: diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 6bbe3ce13..1ad25dc46 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -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(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; + } \ No newline at end of file diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 0d4d4d8be..3e087f63f 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -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); }; diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index c0caaa3ca..2baf4b158 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -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) { diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index f7af9bd51..4c855a71d 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -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 already_visited;