From a8586746bebe6bca001e208660d8ea908b4c15e3 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Sat, 23 Feb 2019 02:47:33 +0100 Subject: [PATCH] cleanup for pull request --- src/ast/bv_decl_plugin.cpp | 138 +++---------------------------- src/ast/bv_decl_plugin.h | 44 +++++++++- src/ast/datatype_decl_plugin.cpp | 82 +++++++++--------- src/ast/datatype_decl_plugin.h | 2 + src/util/mpz.cpp | 99 +++++++++++++++++++++- src/util/mpz.h | 13 ++- src/util/rational.h | 4 + 7 files changed, 212 insertions(+), 170 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index d95261402..29b3fd8a8 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -17,21 +17,12 @@ Revision History: --*/ #include -#include #include "ast/bv_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "util/warning.h" #include "ast/ast_pp.h" #include "ast/ast_smt2_pp.h" -#if defined(_MP_INTERNAL) -#include "util/mpn.h" -#elif defined(_MP_GMP) -#include -#else -#error No multi-precision library selected. -#endif - bv_decl_plugin::bv_decl_plugin(): m_bv_sym("bv"), m_concat_sym("concat"), @@ -875,14 +866,15 @@ app * bv_util::mk_numeral(rational const & val, sort* s) const { return mk_numeral(val, bv_size); } -void log_binary_data(std::ostream &out, unsigned val, unsigned numBits) { - SASSERT(numBits <= sizeof(unsigned)*8); - for (int shift = numBits-1; shift >= 0; --shift) { - if (val & (1 << shift)) { - out << "1"; - } else { - out << "0"; - } + void bv_util::log_mk_numeral(rational const & val, unsigned bv_size) const { + if (bv_size % 4 == 0) { + m_manager.trace_stream() << "#x"; + val.display_hex(m_manager.trace_stream(), bv_size); + m_manager.trace_stream() << "\n"; + } else { + m_manager.trace_stream() << "#b"; + val.display_bin(m_manager.trace_stream(), bv_size); + m_manager.trace_stream() << "\n"; } } @@ -891,73 +883,7 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { app * r = m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr); if (m_plugin->log_constant_meaning_prelude(r)) { - std::ios fmt(nullptr); - fmt.copyfmt(m_manager.trace_stream()); - SASSERT(val.is_int()); - if (val.is_small()) { - if (bv_size % 4 == 0) { - m_manager.trace_stream() << "#x" << std::hex << std::setw(bv_size/4) << std::setfill('0') << val << "\n"; - } else { - m_manager.trace_stream() << "#b"; - log_binary_data(m_manager.trace_stream(), val.get_unsigned(), bv_size); - m_manager.trace_stream() << "\n"; - } - return r; - } -#ifndef _MP_GMP - digit_t *digits = mpz_manager::digits(val.to_mpq().numerator()); - unsigned size = mpz_manager::size(val.to_mpq().numerator()); - if (bv_size % 4 == 0) { - m_manager.trace_stream() << "#x" << std::hex; - unsigned bitSize = size * sizeof(digit_t) * 8; - if (bv_size > bitSize) { - for (unsigned i = 0; i < (bv_size - bitSize)/4; ++i) { - m_manager.trace_stream() << 0; - } - } - m_manager.trace_stream() << digits[size-1] << std::setw(sizeof(digit_t)*2) << std::setfill('0'); - for (unsigned i = 1; i < size; ++i) { - m_manager.trace_stream() << digits[size-i-1]; - } - m_manager.trace_stream() << "\n"; - } else { - m_manager.trace_stream() << "#b"; - const unsigned digitBitSize = sizeof(digit_t) * 8; - unsigned bitSize = size * digitBitSize; - unsigned firstDigitLength; - if (bv_size > bitSize) { - firstDigitLength = 0; - for (unsigned i = 0; i < (bv_size - bitSize)/4; ++i) { - m_manager.trace_stream() << 0; - } - } else { - firstDigitLength = bv_size % digitBitSize; - } - for (unsigned i = 0; i < size; ++i) { - if (i == 0 && firstDigitLength != 0) { - log_binary_data(m_manager.trace_stream(), digits[size-1], firstDigitLength); - } else { - log_binary_data(m_manager.trace_stream(), digits[size-i-1], digitBitSize); - } - } - m_manager.trace_stream() << "\n"; - } -#else - // GMP version - const unsigned base = bv_size % 4 == 0 ? 16 : 2; - size_t sz = mpz_sizeinbase(*(val.to_mpq().numerator().m_ptr), base) + 2; - unsigned requiredLength = bv_size / (base == 16 ? 4 : 1); - unsigned padding = requiredLength > sz ? requiredLength - sz : 0; - sbuffer buffer(sz, 0); - mpz_get_str(buffer.c_ptr(), base, *(val.to_mpq().numerator().m_ptr)); - m_manager.trace_stream() << (base == 16 ? "#x" : "#b"); - for (unsigned i = 0; i < padding; ++i) { - m_manager.trace_stream() << 0; - } - m_manager.trace_stream() << buffer.c_ptr() << "\n"; -#endif - m_manager.trace_stream().copyfmt(fmt); - m_manager.trace_stream() << std::dec; + log_mk_numeral(val, bv_size); } return r; @@ -978,46 +904,4 @@ app * bv_util::mk_bv2int(expr* e) { sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT); 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_manager.has_trace_stream()) { - for (unsigned i = 0; i < n; ++i) { - if (!m_manager.is_true(es[i]) && !m_manager.is_true(es[i])) - return r; - } - - if (m_plugin->log_constant_meaning_prelude(r)) { - if (n % 4 == 0) { - m_manager.trace_stream() << " #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; - } else { - m_manager.trace_stream() << " #b"; - for (unsigned i = 0; i < n; ++i) { - m_manager.trace_stream() << (m_manager.is_true(es[i]) ? 1 : 0); - } - } - - m_manager.trace_stream() << ")\n"; - } - } - - return r; - } \ No newline at end of file +} \ No newline at end of file diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 3e087f63f..f69ce1c02 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -381,6 +381,8 @@ class bv_util : public bv_recognizers { ast_manager & m_manager; bv_decl_plugin * m_plugin; + void log_mk_numeral(rational const & val, unsigned bv_size) const; + public: bv_util(ast_manager & m); @@ -434,7 +436,47 @@ 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); + app * mk_bv(unsigned n, expr* const* es) { + app * r = m_manager.mk_app(get_fid(), OP_MKBV, n, es); + + if (m_manager.has_trace_stream()) { + for (unsigned i = 0; i < n; ++i) { + if (!m_manager.is_true(es[i]) && !m_manager.is_true(es[i])) + return r; + } + + if (m_plugin->log_constant_meaning_prelude(r)) { + if (n % 4 == 0) { + m_manager.trace_stream() << " #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; + } else { + m_manager.trace_stream() << " #b"; + for (unsigned i = 0; i < n; ++i) { + m_manager.trace_stream() << (m_manager.is_true(es[i]) ? 1 : 0); + } + } + + m_manager.trace_stream() << ")\n"; + } + } + + return r; + } }; diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 8b57a33ae..8bf0abbb3 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -453,6 +453,48 @@ namespace datatype { } } + void plugin::log_axiom_definitions(symbol const& s, sort * new_sort) { + symbol const& family_name = m_manager->get_family_name(get_family_id()); + for (constructor const* c : *m_defs[s]) { + func_decl_ref f = c->instantiate(new_sort); + const unsigned num_args = f->get_arity(); + if (num_args == 0) continue; + for (unsigned i = 0; i < num_args; ++i) { + m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n"; + ++m_id_counter; + } + const unsigned constructor_id = m_id_counter; + m_manager->trace_stream() << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name(); + for (unsigned i = 0; i < num_args; ++i) { + m_manager->trace_stream() << " " << family_name << "#" << constructor_id - num_args + i; + } + m_manager->trace_stream() << "\n"; + ++m_id_counter; + m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n"; + ++m_id_counter; + m_axiom_bases.insert(f->get_name(), constructor_id + 4); + std::ostringstream var_sorts; + for (accessor const* a : *c) { + var_sorts << " (;" << a->range()->get_name() << ")"; + } + std::string var_description = var_sorts.str(); + unsigned i = 0; + for (accessor const* a : *c) { + func_decl_ref acc = a->instantiate(new_sort); + m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n"; + ++m_id_counter; + m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i + << " " << family_name << "#" << m_id_counter - 1 << "\n"; + ++m_id_counter; + m_manager->trace_stream() << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1 + << " " << family_name << "#" << m_id_counter - 1 << "\n"; + m_manager->trace_stream() << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n"; + ++m_id_counter; + ++i; + } + } + } + bool plugin::mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts) { begin_def_block(); for (unsigned i = 0; i < num_datatypes; ++i) { @@ -471,45 +513,7 @@ namespace datatype { for (symbol const& s : m_def_block) { new_sorts.push_back(m_defs[s]->instantiate(ps)); if (m_manager->has_trace_stream()) { - symbol const& family_name = m_manager->get_family_name(get_family_id()); - for (constructor const* c : *m_defs[s]) { - func_decl_ref f = c->instantiate(new_sorts.back()); - const unsigned num_args = f->get_arity(); - if (num_args == 0) continue; - for (unsigned i = 0; i < num_args; ++i) { - m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n"; - ++m_id_counter; - } - const unsigned constructor_id = m_id_counter; - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name(); - for (unsigned i = 0; i < num_args; ++i) { - m_manager->trace_stream() << " " << family_name << "#" << constructor_id - num_args + i; - } - m_manager->trace_stream() << "\n"; - ++m_id_counter; - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n"; - ++m_id_counter; - m_axiom_bases.insert(f->get_name(), constructor_id + 4); - std::ostringstream var_sorts; - for (accessor const* a : *c) { - var_sorts << " (;" << a->range()->get_name() << ")"; - } - std::string var_description = var_sorts.str(); - unsigned i = 0; - for (accessor const* a : *c) { - func_decl_ref acc = a->instantiate(new_sorts.back()); - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n"; - ++m_id_counter; - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i - << " " << family_name << "#" << m_id_counter - 1 << "\n"; - ++m_id_counter; - m_manager->trace_stream() << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1 - << " " << family_name << "#" << m_id_counter - 1 << "\n"; - m_manager->trace_stream() << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n"; - ++m_id_counter; - ++i; - } - } + log_axiom_definitions(s, new_sorts.back()); } } return true; diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index cf0b47784..e9734ac0b 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -213,6 +213,8 @@ namespace datatype { void inherit(decl_plugin* other_p, ast_translation& tr) override; + void log_axiom_definitions(symbol const& s, sort * new_sort); + public: plugin(): m_id_counter(0), m_class_id(0) {} ~plugin() override; diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 0d3a6040d..27d3c882c 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -16,7 +16,8 @@ Author: Revision History: --*/ -#include +#include +#include #include "util/mpz.h" #include "util/buffer.h" #include "util/trace.h" @@ -1725,6 +1726,102 @@ void mpz_manager::display_smt2(std::ostream & out, mpz const & a, bool de } } +template +void mpz_manager::display_hex(std::ostream & out, mpz const & a, unsigned num_bits) const { + SASSERT(num_bits % 4 == 0); + std::ios fmt(nullptr); + fmt.copyfmt(out); + out << std::hex; + if (is_small(a)) { + out << std::setw(num_bits/4) << std::setfill('0') << get_uint64(a); + } else { +#ifndef _MP_GMP + digit_t *ds = digits(a); + unsigned sz = size(a); + unsigned bitSize = sz * sizeof(digit_t) * 8; + unsigned firstDigitSize; + if (num_bits >= bitSize) { + firstDigitSize = sizeof(digit_t) * 2; + + for (unsigned i = 0; i < (num_bits - bitSize)/4; ++i) { + out << "0"; + } + } else { + firstDigitSize = num_bits % (sizeof(digit_t) * 8) / 4; + } + + out << std::setfill('0') << std::setw(firstDigitSize) << ds[sz-1] << std::setw(sizeof(digit_t)*2); + for (unsigned i = 1; i < sz; ++i) { + out << ds[sz-i-1]; + } +#else + // GMP version + size_t sz = mpz_sizeinbase(*(a.m_ptr), 16); + unsigned requiredLength = num_bits / 4; + unsigned padding = requiredLength > sz ? requiredLength - sz : 0; + sbuffer buffer(sz, 0); + mpz_get_str(buffer.c_ptr(), 16, *(a.m_ptr)); + for (unsigned i = 0; i < padding; ++i) { + out << "0"; + } + out << buffer.c_ptr() + (sz > requiredLength ? sz - requiredLength : 0); +#endif + } + out.copyfmt(fmt); + out << std::dec; +} + +void display_binary_data(std::ostream &out, unsigned val, unsigned numBits) { + SASSERT(numBits <= sizeof(unsigned)*8); + for (int shift = numBits-1; shift >= 0; --shift) { + if (val & (1 << shift)) { + out << "1"; + } else { + out << "0"; + } + } + } + +template +void mpz_manager::display_bin(std::ostream & out, mpz const & a, unsigned num_bits) const { + if (is_small(a)) { + display_binary_data(out, get_uint64(a), num_bits); + } else { +#ifndef _MP_GMP + digit_t *ds = digits(a); + unsigned sz = size(a); + const unsigned digitBitSize = sizeof(digit_t) * 8; + unsigned bitSize = sz * digitBitSize; + unsigned firstDigitLength; + if (num_bits > bitSize) { + firstDigitLength = 0; + for (unsigned i = 0; i < (num_bits - bitSize); ++i) { + out << "0"; + } + } else { + firstDigitLength = num_bits % digitBitSize; + } + for (unsigned i = 0; i < sz; ++i) { + if (i == 0 && firstDigitLength != 0) { + display_binary_data(out, ds[sz-1], firstDigitLength); + } else { + display_binary_data(out, ds[sz-i-1], digitBitSize); + } + } +#else + // GMP version + size_t sz = mpz_sizeinbase(*(a.m_ptr), 2); + unsigned padding = num_bits > sz ? num_bits - sz : 0; + sbuffer buffer(sz, 0); + mpz_get_str(buffer.c_ptr(), 2, *(a.m_ptr)); + for (unsigned i = 0; i < padding; ++i) { + out << "0"; + } + out << buffer.c_ptr() + (sz > num_bits ? sz - num_bits : 0); +#endif + } +} + template std::string mpz_manager::to_string(mpz const & a) const { std::ostringstream buffer; diff --git a/src/util/mpz.h b/src/util/mpz.h index c258a1e62..0faf13d18 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -99,7 +99,6 @@ class mpz { friend class mpbq; friend class mpbq_manager; friend class mpz_stack; - friend class bv_util; mpz & operator=(mpz const & other) { UNREACHABLE(); return *this; } public: mpz(int v):m_val(v), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {} @@ -135,7 +134,6 @@ inline void swap(mpz & m1, mpz & m2) { m1.swap(m2); } template class mpz_manager { - friend class bv_util; mutable small_object_allocator m_allocator; mutable omp_nest_lock_t m_lock; #define MPZ_BEGIN_CRITICAL() if (SYNCH) omp_set_nest_lock(&m_lock); @@ -594,6 +592,17 @@ public: */ void display_smt2(std::ostream & out, mpz const & a, bool decimal) const; + /** + \brief Displays the num_bits least significant bits of a mpz number in hexadecimal format. + num_bits must be divisible by 4. + */ + void display_hex(std::ostream & out, mpz const & a, unsigned num_bits) const; + + /** + \brief Displays the num_bits least significant bits of a mpz number in binary format. + */ + void display_bin(std::ostream & out, mpz const & a, unsigned num_bits) const; + static unsigned hash(mpz const & a); static bool is_one(mpz const & a) { diff --git a/src/util/rational.h b/src/util/rational.h index dc805511f..bf68c0bf6 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -95,6 +95,10 @@ 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); } + bool is_uint64() const { return m().is_uint64(m_val); } bool is_int64() const { return m().is_int64(m_val); }