mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

fixed build errors and warnings

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-21 18:24:36 +00:00
parent 71042bbf6d
commit 95300e801d
5 changed files with 9 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -16,7 +16,8 @@ Author:
Notes:
--*/
#include<sstream>
#include<math.h>
#include"ast_smt2_pp.h"
#include"well_sorted.h"
#include"th_rewriter.h"
@ -688,8 +689,7 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
m_simp.mk_xor(x_is_pos, y_is_pos, sign_xor);
mk_ite(sign_xor, nzero, pzero, v6);
// else comes the actual multiplication.
unsigned ebits = m_util.get_ebits(f->get_range());
// else comes the actual multiplication.
unsigned sbits = m_util.get_sbits(f->get_range());
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
@ -2037,7 +2037,8 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
dbg_decouple("fpa2bv_to_float_res_exp", res_exp);
expr_ref rounded(m);
round(s, expr_ref (rm, m), res_sgn, res_sig, res_exp, rounded);
expr_ref rm_e(rm, m);
round(s, rm_e, res_sgn, res_sig, res_exp, rounded);
expr_ref is_neg(m), sig_inf(m);
m_simp.mk_eq(sgn, one1, is_neg);
@ -2098,7 +2099,6 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
mk_fp(sgn, e, s, result);
}
else {
mpf_manager & fm = fu().fm();
bv_util & bu = m_bv_util;
arith_util & au = m_arith_util;
@ -2333,7 +2333,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
expr_ref sig_rest(m);
sig_4 = m_bv_util.mk_extract(bv_sz - 1, bv_sz - sig_sz + 1, shifted_sig); // one short
sig_rest = m_bv_util.mk_extract(bv_sz - sig_sz, 0, shifted_sig);
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sig_rest);
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sig_rest.get());
sig_4 = m_bv_util.mk_concat(sig_4, sticky);
}
else {
@ -2496,7 +2496,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
// The exponent is at most bv_sz, i.e., we need ld(bv_sz)+1 ebits.
// exp < bv_sz (+sign bit which is [0])
unsigned exp_worst_case_sz = (unsigned)((log((double)bv_sz) / log((double)2)) + 1.0);
unsigned exp_worst_case_sz = (unsigned)((log((double)bv_sz) / log((double)2)) + 1.0);
if (exp_sz < exp_worst_case_sz) {
// exp_sz < exp_worst_case_sz and exp >= 0.
@ -2558,7 +2558,6 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
unsigned ebits = m_util.get_ebits(xs);
unsigned sbits = m_util.get_sbits(xs);
unsigned bv_sz = (unsigned)f->get_parameter(0).get_int();
unsigned rounding_sz = bv_sz + 3;
expr_ref bv0(m), bv1(m);
bv0 = m_bv_util.mk_numeral(0, 1);
@ -2575,7 +2574,6 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
expr_ref c1(m), v1(m);
c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
v1 = mk_to_ubv_unspecified(bv_sz);
dbg_decouple("fpa2bv_to_ubv_c1", c1);
// +-Zero -> 0
expr_ref c2(m), v2(m);
@ -2682,8 +2680,7 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
unsigned ebits = m_util.get_ebits(xs);
unsigned sbits = m_util.get_sbits(xs);
unsigned bv_sz = (unsigned)f->get_parameter(0).get_int();
unsigned rounding_sz = bv_sz + 3;
unsigned bv_sz = (unsigned)f->get_parameter(0).get_int();
expr_ref bv0(m), bv1(m), bv0_2(m), bv1_2(m), bv3_2(m);
bv0 = m_bv_util.mk_numeral(0, 1);

4
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -160,9 +160,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(f->get_num_parameters() == 2);
SASSERT(f->get_parameter(0).is_int());
SASSERT(f->get_parameter(1).is_int());
unsigned ebits = f->get_parameter(0).get_int();
unsigned sbits = f->get_parameter(1).get_int();
SASSERT(f->get_parameter(1).is_int());
return BR_FAILED;
}

4
src/ast/simplifier/fpa_simplifier_plugin.cpp
View file

@ -19,7 +19,6 @@ Author:
fpa_simplifier_plugin::fpa_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b) :
simplifier_plugin(symbol("fpa"), m),
m_util(m),
m_bsimp(b),
m_rw(m) {}
fpa_simplifier_plugin::~fpa_simplifier_plugin() {}
@ -28,9 +27,6 @@ bool fpa_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * cons
set_reduce_invoked();
SASSERT(f->get_family_id() == get_family_id());
/*switch (f->get_decl_kind()) {
case OP_FPA_FP: break;
}*/
return m_rw.mk_app_core(f, num_args, args, result) == BR_DONE;
}

1
src/ast/simplifier/fpa_simplifier_plugin.h
View file

@ -23,7 +23,6 @@ Author:
class fpa_simplifier_plugin : public simplifier_plugin {
fpa_util m_util;
basic_simplifier_plugin & m_bsimp;
fpa_rewriter m_rw;
public:

1
src/util/mpf.cpp
View file

@ -203,7 +203,6 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
m_mpq_manager.abs(x);
m_mpz_manager.set(o.significand, 0);
const mpz & p = m_powers2(sbits+3);
scoped_mpq v(m_mpq_manager);
m_mpq_manager.set(v, x);