mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-09-12 14:47:49 +02:00
parent a8b47b4fb2 646dcfb6e6
commit e3840a7fc6
6 changed files with 20 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -6495,7 +6495,7 @@ class Optimize(Z3PPObject):
return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))
def reason_unknown(self):
"""Return a string that describes why the last `check()` returned `unknown`."""
"""Return a string that describes why the last `check()` returned `unknown`."""
return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
def model(self):

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

@ -468,7 +468,7 @@ br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg
scoped_mpf v2(m_fm), v3(m_fm), v4(m_fm);
if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3) && m_util.is_numeral(arg4, v4)) {
scoped_mpf t(m_fm);
m_fm.fused_mul_add(rm, v2, v3, v4, t);
m_fm.fma(rm, v2, v3, v4, t);
result = m_util.mk_value(t);
return BR_DONE;
}

4
src/muz/rel/check_relation.cpp
View file

@ -430,12 +430,12 @@ namespace datalog {
IF_VERBOSE(3, verbose_stream() << objective << " verified\n";);
}
else if (res == l_true) {
IF_VERBOSE(3, verbose_stream() << "NOT verified " << res << "\n";
IF_VERBOSE(0, verbose_stream() << "NOT verified " << res << "\n";
verbose_stream() << mk_pp(fml1, m) << "\n";
verbose_stream() << mk_pp(fml2, m) << "\n";
verbose_stream().flush();
);
throw 0;
throw default_exception("operation was not verified");
}
}

2
src/smt/smt_context.h
View file

@ -157,7 +157,7 @@ namespace smt {
u_map<bool_var> m_expr2bool_var;
#endif
ptr_vector<expr> m_bool_var2expr; // bool_var -> expr
char_vector m_assignment; //!< mapping literal id -> assignment lbool
signed_char_vector m_assignment; //!< mapping literal id -> assignment lbool
vector<watch_list> m_watches; //!< per literal
vector<clause_set> m_lit_occs; //!< index for backward subsumption
svector<bool_var_data> m_bdata; //!< mapping bool_var -> data

19
src/util/mpf.cpp
View file

@ -638,7 +638,11 @@ void mpf_manager::mul(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf &
// Remove the extra bits, keeping a sticky bit.
scoped_mpz sticky_rem(m_mpz_manager);
m_mpz_manager.machine_div_rem(o.significand, m_powers2(x.sbits-4), o.significand, sticky_rem);
if (o.sbits >= 4)
m_mpz_manager.machine_div_rem(o.significand, m_powers2(o.sbits - 4), o.significand, sticky_rem);
else
m_mpz_manager.mul2k(o.significand, 4-o.sbits, o.significand);
if (!m_mpz_manager.is_zero(sticky_rem) && m_mpz_manager.is_even(o.significand))
m_mpz_manager.inc(o.significand);
@ -728,7 +732,7 @@ void mpf_manager::div(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf &
}
}
void mpf_manager::fused_mul_add(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf const &z, mpf & o) {
void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf const &z, mpf & o) {
SASSERT(x.sbits == y.sbits && x.ebits == y.ebits &&
x.sbits == y.sbits && z.ebits == z.ebits);
@ -861,7 +865,7 @@ void mpf_manager::fused_mul_add(mpf_rounding_mode rm, mpf const & x, mpf const &
o.exponent = mul_res.exponent();
unsigned extra = x.sbits-4;
unsigned extra = 0;
// Result could overflow into 4.xxx ...
SASSERT(m_mpz_manager.lt(o.significand, m_powers2(2 * x.sbits + 2)));
if(m_mpz_manager.ge(o.significand, m_powers2(2 * x.sbits + 1)))
@ -871,8 +875,13 @@ void mpf_manager::fused_mul_add(mpf_rounding_mode rm, mpf const & x, mpf const &
TRACE("mpf_dbg", tout << "Addition overflew!" << std::endl;);
}
// Get rid of the extra bits.
m_mpz_manager.machine_div_rem(o.significand, m_powers2(extra), o.significand, sticky_rem);
// Remove the extra bits, keeping a sticky bit.
m_mpz_manager.set(sticky_rem, 0);
if (o.sbits >= (4+extra))
m_mpz_manager.machine_div_rem(o.significand, m_powers2(4+extra), o.significand, sticky_rem);
else
m_mpz_manager.mul2k(o.significand, (4+extra) - o.sbits, o.significand);
if (!m_mpz_manager.is_zero(sticky_rem) && m_mpz_manager.is_even(o.significand))
m_mpz_manager.inc(o.significand);

2
src/util/mpf.h
View file

@ -121,7 +121,7 @@ public:
void mul(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o);
void div(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o);
void fused_mul_add(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf const &z, mpf & o);
void fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf const &z, mpf & o);
void sqrt(mpf_rounding_mode rm, mpf const & x, mpf & o);