From 59b18d4a14eeec6bd887b8135e34677f373e9f02 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jan 2024 09:19:11 -0800 Subject: [PATCH] create as_bin as_hex wrappers for display Signed-off-by: Nikolaj Bjorner --- src/api/api_numeral.cpp | 2 +- src/ast/bv_decl_plugin.cpp | 8 ++------ src/util/rational.h | 32 ++++++++++++++++++++++++++++++-- 3 files changed, 33 insertions(+), 9 deletions(-) diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 98dceffb7..b90a84bb7 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -188,7 +188,7 @@ extern "C" { bool ok = Z3_get_numeral_rational(c, a, r); if (ok && r.is_int() && !r.is_neg()) { std::stringstream strm; - r.display_bin(strm, r.get_num_bits()); + strm << r.as_bin(r.get_num_bits()); return mk_c(c)->mk_external_string(std::move(strm).str()); } else { diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 6b2106f3f..327e280cf 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -912,13 +912,9 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { if (m_plugin->log_constant_meaning_prelude(r)) { if (bv_size % 4 == 0) { - m_manager.trace_stream() << "#x"; - val.display_hex(m_manager.trace_stream(), bv_size); - m_manager.trace_stream() << "\n"; + m_manager.trace_stream() << "#x" << val.as_hex(bv_size) << "\n"; } else { - m_manager.trace_stream() << "#b"; - val.display_bin(m_manager.trace_stream(), bv_size); - m_manager.trace_stream() << "\n"; + m_manager.trace_stream() << "#b" << val.as_bin(bv_size) << "\n"; } } diff --git a/src/util/rational.h b/src/util/rational.h index db60077ac..e9924bca7 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -30,6 +30,10 @@ class rational { static synch_mpq_manager & m() { return *g_mpq_manager; } + void display_hex(std::ostream & out, unsigned num_bits) const { SASSERT(is_int()); m().display_hex(out, m_val.numerator(), num_bits); } + + void display_bin(std::ostream& out, unsigned num_bits) const { SASSERT(is_int()); m().display_bin(out, m_val.numerator(), num_bits); } + public: static void initialize(); static void finalize(); @@ -96,9 +100,33 @@ public: void display_smt2(std::ostream & out) const { return m().display_smt2(out, m_val, false); } - void display_hex(std::ostream & out, unsigned num_bits) const { SASSERT(is_int()); return m().display_hex(out, m_val.numerator(), num_bits); } - void display_bin(std::ostream & out, unsigned num_bits) const { SASSERT(is_int()); return m().display_bin(out, m_val.numerator(), num_bits); } + struct as_hex_wrapper { + rational const& r; + unsigned bw; + }; + + as_hex_wrapper as_hex(unsigned bw) const { return as_hex_wrapper{*this, bw}; } + + friend inline std::ostream& operator<<(std::ostream& out, as_hex_wrapper const& ab) { + ab.r.display_hex(out, ab.bw); + return out; + } + + + + struct as_bin_wrapper { + rational const& r; + unsigned bw; + }; + + as_bin_wrapper as_bin(unsigned bw) const { return as_bin_wrapper{*this, bw}; } + + friend inline std::ostream& operator<<(std::ostream& out, as_bin_wrapper const& ab) { + ab.r.display_bin(out, ab.bw); + return out; + } + bool is_uint64() const { return m().is_uint64(m_val); }