From 6d2cf4f464d5fec4dbae1afe907c9d077664ee81 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Mon, 10 Dec 2018 22:49:08 +0100 Subject: [PATCH] smt-like logging of theory specific meaning of constants --- src/ast/arith_decl_plugin.cpp | 5 +- src/ast/bv_decl_plugin.cpp | 129 ++++++++++++++++++++++++++++------ src/ast/fpa_decl_plugin.cpp | 3 +- src/util/mpz.h | 2 + src/util/rational.h | 2 + 5 files changed, 115 insertions(+), 26 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 926e515e2..883e004a7 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -92,7 +92,7 @@ app * arith_decl_plugin::mk_numeral(algebraic_numbers::anum const & val, bool is app * r = m_manager->mk_const(decl); if (log_constant_meaning_prelude(r)) { - am().display_root(m_manager->trace_stream(), val); + am().display_root_smt2(m_manager->trace_stream(), val); m_manager->trace_stream() << "\n"; } @@ -427,7 +427,6 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { m_manager->trace_stream() << u_val << "\n"; } } - return r; } else { @@ -455,7 +454,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { app * r = m_manager->mk_const(decl); if (log_constant_meaning_prelude(r)) { - val.display(m_manager->trace_stream()); + val.display_smt2(m_manager->trace_stream()); m_manager->trace_stream() << "\n"; } diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 1ad25dc46..ce75cd90e 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -17,12 +17,22 @@ Revision History: --*/ #include +#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"), @@ -867,9 +877,71 @@ 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)) { - m_manager.trace_stream() << "(" << bv_size << " #d"; - val.display(m_manager.trace_stream()); - m_manager.trace_stream() << ")\n"; + 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" << std::bitset(val.get_unsigned()).to_string().substr(sizeof(unsigned)*8 - bv_size) << "\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) { + m_manager.trace_stream() << std::bitset(digits[size-1]).to_string().substr(digitBitSize - firstDigitLength); + } else { + m_manager.trace_stream() << std::bitset(digits[size-i-1]); + } + } + 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; } return r; @@ -892,30 +964,43 @@ app * bv_util::mk_bv2int(expr* e) { 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; + if (m_manager.has_trace_stream()) { 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; + if (!m_manager.is_true(es[i]) && !m_manager.is_true(es[i])) + return r; + } - m_manager.trace_stream() << ")\n"; + 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/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 2baf4b158..1e693b29a 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -95,7 +95,8 @@ app * fpa_decl_plugin::mk_numeral(mpf const & 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"; + m_fm.display_smt2(m_manager->trace_stream(), v, false); + m_manager->trace_stream() << "\n"; } return r; diff --git a/src/util/mpz.h b/src/util/mpz.h index 2df03666f..c258a1e62 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -99,6 +99,7 @@ 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) {} @@ -134,6 +135,7 @@ 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); diff --git a/src/util/rational.h b/src/util/rational.h index 3403848c4..dc805511f 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -93,6 +93,8 @@ public: void display_decimal(std::ostream & out, unsigned prec, bool truncate = false) const { return m().display_decimal(out, m_val, prec, truncate); } + void display_smt2(std::ostream & out) const { return m().display_smt2(out, m_val, false); } + bool is_uint64() const { return m().is_uint64(m_val); } bool is_int64() const { return m().is_int64(m_val); }