mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 09:05:31 +00:00
cleanup for pull request
This commit is contained in:
nilsbecker
parent
6e508d4221
commit
a8586746be
7 changed files with 212 additions and 170 deletions
|
|
@ -17,21 +17,12 @@ Revision History:
|
|||
|
||||
--*/
|
||||
#include<sstream>
|
||||
#include<iomanip>
|
||||
#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<gmp.h>
|
||||
#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<true>::digits(val.to_mpq().numerator());
|
||||
unsigned size = mpz_manager<true>::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<char, 1024> 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;
|
||||
}
|
||||
}
|
||||
|
|
@ -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;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue