mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

create as_bin as_hex wrappers for display

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-12 09:19:11 -08:00
parent 999e67df0d
commit 59b18d4a14
3 changed files with 33 additions and 9 deletions

2
src/api/api_numeral.cpp
View file

@ -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 {

8
src/ast/bv_decl_plugin.cpp
View file

@ -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";
}
}

32
src/util/rational.h
View file

@ -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); }