mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

merging into unstable

Browse source
This commit is contained in:
Ken McMillan 2015-04-20 12:31:16 -07:00
commit 9bff93279f
3 changed files with 11 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/python/z3.py
View file

@ -8480,7 +8480,13 @@ def fpToReal(x):
return ArithRef(Z3_mk_fpa_to_real(x.ctx_ref(), x.ast), x.ctx) return ArithRef(Z3_mk_fpa_to_real(x.ctx_ref(), x.ast), x.ctx)
def fpToIEEEBV(x): def fpToIEEEBV(x):
"""Create a Z3 floating-point conversion expression, from floating-point expression to IEEE bit-vector. """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
The size of the resulting bit-vector is automatically determined.
Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
knows only one NaN and it will always produce the same bit-vector represenatation of
that NaN.
>>> x = FP('x', FPSort(8, 24)) >>> x = FP('x', FPSort(8, 24))
>>> y = fpToIEEEBV(x) >>> y = fpToIEEEBV(x)

3
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -902,6 +902,7 @@ template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_shl(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { void bit_blaster_tpl<Cfg>::mk_shl(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
numeral k; numeral k;
if (is_numeral(sz, b_bits, k)) { if (is_numeral(sz, b_bits, k)) {
if (k > numeral(sz)) k = numeral(sz);
unsigned n = static_cast<unsigned>(k.get_int64()); unsigned n = static_cast<unsigned>(k.get_int64());
if (n >= sz) n = sz; if (n >= sz) n = sz;
unsigned pos; unsigned pos;
@ -947,6 +948,7 @@ template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_lshr(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { void bit_blaster_tpl<Cfg>::mk_lshr(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
numeral k; numeral k;
if (is_numeral(sz, b_bits, k)) { if (is_numeral(sz, b_bits, k)) {
if (k > numeral(sz)) k = numeral(sz);
unsigned n = static_cast<unsigned>(k.get_int64()); unsigned n = static_cast<unsigned>(k.get_int64());
unsigned pos = 0; unsigned pos = 0;
for (unsigned i = n; i < sz; pos++, i++) for (unsigned i = n; i < sz; pos++, i++)
@ -989,6 +991,7 @@ template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_ashr(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { void bit_blaster_tpl<Cfg>::mk_ashr(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
numeral k; numeral k;
if (is_numeral(sz, b_bits, k)) { if (is_numeral(sz, b_bits, k)) {
if (k > numeral(sz)) k = numeral(sz);
unsigned n = static_cast<unsigned>(k.get_int64()); unsigned n = static_cast<unsigned>(k.get_int64());
unsigned pos = 0; unsigned pos = 0;
for (unsigned i = n; i < sz; pos++, i++) for (unsigned i = n; i < sz; pos++, i++)

2
src/tactic/arith/fix_dl_var_tactic.cpp
View file

@ -282,7 +282,7 @@ class fix_dl_var_tactic : public tactic {
expr_ref new_curr(m); expr_ref new_curr(m);
proof_ref new_pr(m); proof_ref new_pr(m);
unsigned size = g->size(); unsigned size = g->size();
for (unsigned idx = 0; idx < size; idx++) { for (unsigned idx = 0; !g->inconsistent() && idx < size; idx++) {
expr * curr = g->form(idx); expr * curr = g->form(idx);
m_rw(curr, new_curr, new_pr); m_rw(curr, new_curr, new_pr);
if (produce_proofs) { if (produce_proofs) {