mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
Ken McMillan
commit
a318b0f104
|
|
@ -319,8 +319,8 @@ static void get_file_params(const char *filename, hash_map<std::string,std::stri
|
|||
tokenize(first_line.substr(2,first_line.size()-2),tokens);
|
||||
for(unsigned i = 0; i < tokens.size(); i++){
|
||||
std::string &tok = tokens[i];
|
||||
int eqpos = tok.find('=');
|
||||
if(eqpos >= 0 && eqpos < (int)tok.size()){
|
||||
size_t eqpos = tok.find('=');
|
||||
if(eqpos >= 0 && eqpos < tok.size()){
|
||||
std::string left = tok.substr(0,eqpos);
|
||||
std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1);
|
||||
params[left] = right;
|
||||
|
|
@ -377,8 +377,8 @@ extern "C" {
|
|||
#else
|
||||
|
||||
|
||||
static Z3_ast and_vec(Z3_context ctx,std::vector<Z3_ast> &c){
|
||||
return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0];
|
||||
static Z3_ast and_vec(Z3_context ctx,svector<Z3_ast> &c){
|
||||
return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0];
|
||||
}
|
||||
|
||||
static Z3_ast parents_vector_to_tree(Z3_context ctx, int num, Z3_ast *cnsts, int *parents){
|
||||
|
|
@ -395,15 +395,15 @@ extern "C" {
|
|||
}
|
||||
}
|
||||
else {
|
||||
std::vector<std::vector<Z3_ast> > chs(num);
|
||||
std::vector<svector<Z3_ast> > chs(num);
|
||||
for(int i = 0; i < num-1; i++){
|
||||
std::vector<Z3_ast> &c = chs[i];
|
||||
svector<Z3_ast> &c = chs[i];
|
||||
c.push_back(cnsts[i]);
|
||||
Z3_ast foo = Z3_mk_interp(ctx,and_vec(ctx,c));
|
||||
chs[parents[i]].push_back(foo);
|
||||
}
|
||||
{
|
||||
std::vector<Z3_ast> &c = chs[num-1];
|
||||
svector<Z3_ast> &c = chs[num-1];
|
||||
c.push_back(cnsts[num-1]);
|
||||
res = and_vec(ctx,c);
|
||||
}
|
||||
|
|
@ -468,7 +468,7 @@ extern "C" {
|
|||
static std::string read_msg;
|
||||
static std::vector<Z3_ast> read_theory;
|
||||
|
||||
static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, std::vector<Z3_ast> &assertions){
|
||||
static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, svector<Z3_ast> &assertions){
|
||||
read_error.clear();
|
||||
try {
|
||||
std::string foo(filename);
|
||||
|
|
@ -510,26 +510,26 @@ extern "C" {
|
|||
|
||||
hash_map<std::string,std::string> file_params;
|
||||
get_file_params(filename,file_params);
|
||||
|
||||
int num_theory = 0;
|
||||
|
||||
unsigned num_theory = 0;
|
||||
if(file_params.find("THEORY") != file_params.end())
|
||||
num_theory = atoi(file_params["THEORY"].c_str());
|
||||
|
||||
std::vector<Z3_ast> assertions;
|
||||
svector<Z3_ast> assertions;
|
||||
if(!iZ3_parse(ctx,filename,error,assertions))
|
||||
return false;
|
||||
|
||||
if(num_theory > (int)assertions.size())
|
||||
num_theory = assertions.size();
|
||||
int num = assertions.size() - num_theory;
|
||||
if(num_theory > assertions.size())
|
||||
num_theory = assertions.size();
|
||||
unsigned num = assertions.size() - num_theory;
|
||||
|
||||
read_cnsts.resize(num);
|
||||
read_parents.resize(num);
|
||||
read_theory.resize(num_theory);
|
||||
|
||||
for(int j = 0; j < num_theory; j++)
|
||||
for(unsigned j = 0; j < num_theory; j++)
|
||||
read_theory[j] = assertions[j];
|
||||
for(int j = 0; j < num; j++)
|
||||
for(unsigned j = 0; j < num; j++)
|
||||
read_cnsts[j] = assertions[j+num_theory];
|
||||
|
||||
if(ret_num_theory)
|
||||
|
|
@ -543,12 +543,12 @@ extern "C" {
|
|||
return true;
|
||||
}
|
||||
|
||||
for(int j = 0; j < num; j++)
|
||||
for(unsigned j = 0; j < num; j++)
|
||||
read_parents[j] = SHRT_MAX;
|
||||
|
||||
hash_map<Z3_ast,int> pred_map;
|
||||
|
||||
for(int j = 0; j < num; j++){
|
||||
for(unsigned j = 0; j < num; j++){
|
||||
Z3_ast lhs = 0, rhs = read_cnsts[j];
|
||||
|
||||
if(Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx,Z3_to_app(ctx,rhs))) == Z3_OP_IMPLIES){
|
||||
|
|
@ -602,7 +602,7 @@ extern "C" {
|
|||
}
|
||||
}
|
||||
|
||||
for(int j = 0; j < num-1; j++)
|
||||
for(unsigned j = 0; j < num-1; j++)
|
||||
if(read_parents[j] == SHRT_MIN){
|
||||
read_error << "formula " << j+1 << ": unreferenced";
|
||||
goto fail;
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ public class BitVecNum extends BitVecExpr
|
|||
{
|
||||
Native.LongPtr res = new Native.LongPtr();
|
||||
if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
|
||||
throw new Z3Exception("Numeral is not an int64");
|
||||
throw new Z3Exception("Numeral is not a long");
|
||||
return res.value;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -6424,7 +6424,7 @@ class Tactic:
|
|||
_z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expressions expected")
|
||||
goal = _to_goal(goal)
|
||||
if len(arguments) > 0 or len(keywords) > 0:
|
||||
p = args2params(arguments, keywords, a.ctx)
|
||||
p = args2params(arguments, keywords, self.ctx)
|
||||
return ApplyResult(Z3_tactic_apply_ex(self.ctx.ref(), self.tactic, goal.goal, p.params), self.ctx)
|
||||
else:
|
||||
return ApplyResult(Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx)
|
||||
|
|
|
|||
|
|
@ -479,7 +479,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
// otherwise t2 is also a quantifier.
|
||||
return true;
|
||||
}
|
||||
UNREACHABLE();
|
||||
IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
case PR_DER: {
|
||||
|
|
@ -488,13 +488,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
match_fact(p, fact) &&
|
||||
match_iff(fact.get(), t1, t2) &&
|
||||
match_quantifier(t1, is_forall, decls1, body1) &&
|
||||
is_forall &&
|
||||
match_or(body1.get(), terms1)) {
|
||||
is_forall) {
|
||||
// TBD: check that terms are set of equalities.
|
||||
// t2 is an instance of a predicate in terms1
|
||||
return true;
|
||||
}
|
||||
UNREACHABLE();
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
case PR_HYPOTHESIS: {
|
||||
|
|
@ -832,7 +831,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
}
|
||||
else {
|
||||
IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" <<
|
||||
mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n";);
|
||||
mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n" << mk_pp(p, m) << "\n";);
|
||||
}
|
||||
fmls[i] = premise1;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -19,6 +19,7 @@ Revision History:
|
|||
|
||||
--*/
|
||||
|
||||
|
||||
#include "iz3translate.h"
|
||||
#include "iz3proof.h"
|
||||
#include "iz3profiling.h"
|
||||
|
|
|
|||
|
|
@ -475,10 +475,11 @@ namespace smt {
|
|||
bool theory_arith<Ext>::all_coeff_int(row const & r) const {
|
||||
typename vector<row_entry>::const_iterator it = r.begin_entries();
|
||||
typename vector<row_entry>::const_iterator end = r.end_entries();
|
||||
for (; it != end; ++it) {
|
||||
if (!it->is_dead() && !it->m_coeff.is_int())
|
||||
for (; it != end; ++it) {
|
||||
if (!it->is_dead() && !it->m_coeff.is_int()) {
|
||||
TRACE("gomory_cut", display_row(tout, r, true););
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1588,8 +1588,7 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
|
|||
v2 = x;
|
||||
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
SASSERT(ebits < sbits);
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
|
||||
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
|
||||
unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
|
||||
|
|
@ -1619,9 +1618,22 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
|
|||
expr_ref shift(m), r_shifted(m), l_shifted(m);
|
||||
shift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits-1, ebits+1),
|
||||
m_bv_util.mk_sign_extend(1, a_exp));
|
||||
r_shifted = m_bv_util.mk_bv_lshr(a_sig, m_bv_util.mk_zero_extend(sbits-ebits-1, shift));
|
||||
if (sbits > (ebits+1))
|
||||
r_shifted = m_bv_util.mk_bv_lshr(a_sig, m_bv_util.mk_zero_extend(sbits-(ebits+1), shift));
|
||||
else if (sbits < (ebits+1))
|
||||
r_shifted = m_bv_util.mk_extract(ebits, ebits-sbits+1, m_bv_util.mk_bv_lshr(m_bv_util.mk_zero_extend(ebits+1-sbits, a_sig), shift));
|
||||
else // sbits == ebits+1
|
||||
r_shifted = m_bv_util.mk_bv_lshr(a_sig, shift);
|
||||
SASSERT(is_well_sorted(m, r_shifted));
|
||||
SASSERT(m_bv_util.get_bv_size(r_shifted) == sbits);
|
||||
l_shifted = m_bv_util.mk_bv_shl(r_shifted, m_bv_util.mk_zero_extend(sbits-ebits-1, shift));
|
||||
|
||||
if (sbits > (ebits+1))
|
||||
l_shifted = m_bv_util.mk_bv_shl(r_shifted, m_bv_util.mk_zero_extend(sbits-(ebits+1), shift));
|
||||
else if (sbits < (ebits+1))
|
||||
l_shifted = m_bv_util.mk_extract(ebits, ebits-sbits+1, m_bv_util.mk_bv_shl(m_bv_util.mk_zero_extend(ebits+1-sbits, r_shifted), shift));
|
||||
else // sbits == ebits+1
|
||||
l_shifted = m_bv_util.mk_bv_shl(r_shifted, shift);
|
||||
SASSERT(is_well_sorted(m, l_shifted));
|
||||
SASSERT(m_bv_util.get_bv_size(l_shifted) == sbits);
|
||||
|
||||
res_sig = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1),
|
||||
|
|
@ -1825,146 +1837,158 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
|
|||
mk_triple(args[0], args[1], args[2], result);
|
||||
}
|
||||
else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) {
|
||||
// We also support float to float conversion
|
||||
// We also support float to float conversion
|
||||
sort * s = f->get_range();
|
||||
expr_ref rm(m), x(m);
|
||||
rm = args[0];
|
||||
x = args[1];
|
||||
|
||||
expr_ref c1(m), c2(m), c3(m), c4(m), c5(m);
|
||||
expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m);
|
||||
expr_ref one1(m);
|
||||
|
||||
one1 = m_bv_util.mk_numeral(1, 1);
|
||||
expr_ref ninf(m), pinf(m);
|
||||
mk_plus_inf(f, pinf);
|
||||
mk_minus_inf(f, ninf);
|
||||
|
||||
// NaN -> NaN
|
||||
mk_is_nan(x, c1);
|
||||
mk_nan(f, v1);
|
||||
|
||||
// +0 -> +0
|
||||
mk_is_pzero(x, c2);
|
||||
mk_pzero(f, v2);
|
||||
|
||||
// -0 -> -0
|
||||
mk_is_nzero(x, c3);
|
||||
mk_nzero(f, v3);
|
||||
|
||||
// +oo -> +oo
|
||||
mk_is_pinf(x, c4);
|
||||
v4 = pinf;
|
||||
|
||||
// -oo -> -oo
|
||||
mk_is_ninf(x, c5);
|
||||
v5 = ninf;
|
||||
|
||||
// otherwise: the actual conversion with rounding.
|
||||
sort * s = f->get_range();
|
||||
expr_ref sgn(m), sig(m), exp(m), lz(m);
|
||||
unpack(x, sgn, sig, exp, lz, true);
|
||||
|
||||
dbg_decouple("fpa2bv_to_float_x_sig", sig);
|
||||
dbg_decouple("fpa2bv_to_float_x_exp", exp);
|
||||
dbg_decouple("fpa2bv_to_float_lz", lz);
|
||||
|
||||
expr_ref res_sgn(m), res_sig(m), res_exp(m);
|
||||
|
||||
res_sgn = sgn;
|
||||
|
||||
unsigned from_sbits = m_util.get_sbits(m.get_sort(args[1]));
|
||||
unsigned from_ebits = m_util.get_ebits(m.get_sort(args[1]));
|
||||
unsigned from_sbits = m_util.get_sbits(m.get_sort(x));
|
||||
unsigned from_ebits = m_util.get_ebits(m.get_sort(x));
|
||||
unsigned to_sbits = m_util.get_sbits(s);
|
||||
unsigned to_ebits = m_util.get_ebits(s);
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(sgn) == 1);
|
||||
SASSERT(m_bv_util.get_bv_size(sig) == from_sbits);
|
||||
SASSERT(m_bv_util.get_bv_size(exp) == from_ebits);
|
||||
SASSERT(m_bv_util.get_bv_size(lz) == from_ebits);
|
||||
if (from_sbits == to_sbits && from_ebits == to_ebits)
|
||||
result = x;
|
||||
else {
|
||||
expr_ref c1(m), c2(m), c3(m), c4(m), c5(m);
|
||||
expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m);
|
||||
expr_ref one1(m);
|
||||
|
||||
if (from_sbits < (to_sbits + 3))
|
||||
{
|
||||
// make sure that sig has at least to_sbits + 3
|
||||
res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits+3-from_sbits));
|
||||
}
|
||||
else if (from_sbits > (to_sbits + 3))
|
||||
{
|
||||
// collapse the extra bits into a sticky bit.
|
||||
expr_ref sticky(m), low(m), high(m);
|
||||
low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig);
|
||||
high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig);
|
||||
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get());
|
||||
res_sig = m_bv_util.mk_concat(high, sticky);
|
||||
}
|
||||
else
|
||||
res_sig = sig;
|
||||
one1 = m_bv_util.mk_numeral(1, 1);
|
||||
expr_ref ninf(m), pinf(m);
|
||||
mk_plus_inf(f, pinf);
|
||||
mk_minus_inf(f, ninf);
|
||||
|
||||
res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder.
|
||||
unsigned sig_sz = m_bv_util.get_bv_size(res_sig);
|
||||
SASSERT(sig_sz == to_sbits+4);
|
||||
// NaN -> NaN
|
||||
mk_is_nan(x, c1);
|
||||
mk_nan(f, v1);
|
||||
|
||||
expr_ref exponent_overflow(m);
|
||||
exponent_overflow = m.mk_false();
|
||||
// +0 -> +0
|
||||
mk_is_pzero(x, c2);
|
||||
mk_pzero(f, v2);
|
||||
|
||||
if (from_ebits < (to_ebits + 2))
|
||||
{
|
||||
res_exp = m_bv_util.mk_sign_extend(to_ebits-from_ebits+2, exp);
|
||||
}
|
||||
else if (from_ebits > (to_ebits + 2))
|
||||
{
|
||||
expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m);
|
||||
expr_ref no_ovf(m), zero1(m), s_is_one(m), s_is_zero(m);
|
||||
high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp);
|
||||
low = m_bv_util.mk_extract(to_ebits+1, 0, exp);
|
||||
lows = m_bv_util.mk_extract(to_ebits+1, to_ebits+1, low);
|
||||
// -0 -> -0
|
||||
mk_is_nzero(x, c3);
|
||||
mk_nzero(f, v3);
|
||||
|
||||
// +oo -> +oo
|
||||
mk_is_pinf(x, c4);
|
||||
v4 = pinf;
|
||||
|
||||
// -oo -> -oo
|
||||
mk_is_ninf(x, c5);
|
||||
v5 = ninf;
|
||||
|
||||
high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get());
|
||||
high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get());
|
||||
// otherwise: the actual conversion with rounding.
|
||||
expr_ref sgn(m), sig(m), exp(m), lz(m);
|
||||
unpack(x, sgn, sig, exp, lz, true);
|
||||
|
||||
zero1 = m_bv_util.mk_numeral(0, 1);
|
||||
m_simp.mk_eq(high_red_and, one1, h_and_eq);
|
||||
m_simp.mk_eq(high_red_or, zero1, h_or_eq);
|
||||
m_simp.mk_eq(lows, zero1, s_is_zero);
|
||||
m_simp.mk_eq(lows, one1, s_is_one);
|
||||
dbg_decouple("fpa2bv_to_float_x_sig", sig);
|
||||
dbg_decouple("fpa2bv_to_float_x_exp", exp);
|
||||
dbg_decouple("fpa2bv_to_float_lz", lz);
|
||||
|
||||
expr_ref res_sgn(m), res_sig(m), res_exp(m);
|
||||
|
||||
res_sgn = sgn;
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(sgn) == 1);
|
||||
SASSERT(m_bv_util.get_bv_size(sig) == from_sbits);
|
||||
SASSERT(m_bv_util.get_bv_size(exp) == from_ebits);
|
||||
SASSERT(m_bv_util.get_bv_size(lz) == from_ebits);
|
||||
|
||||
if (from_sbits < (to_sbits + 3))
|
||||
{
|
||||
// make sure that sig has at least to_sbits + 3
|
||||
res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits+3-from_sbits));
|
||||
}
|
||||
else if (from_sbits > (to_sbits + 3))
|
||||
{
|
||||
// collapse the extra bits into a sticky bit.
|
||||
expr_ref sticky(m), low(m), high(m);
|
||||
low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig);
|
||||
high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig);
|
||||
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get());
|
||||
res_sig = m_bv_util.mk_concat(high, sticky);
|
||||
}
|
||||
else
|
||||
res_sig = sig;
|
||||
|
||||
res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder.
|
||||
unsigned sig_sz = m_bv_util.get_bv_size(res_sig);
|
||||
SASSERT(sig_sz == to_sbits+4);
|
||||
|
||||
expr_ref exponent_overflow(m);
|
||||
exponent_overflow = m.mk_false();
|
||||
|
||||
if (from_ebits < (to_ebits + 2))
|
||||
{
|
||||
res_exp = m_bv_util.mk_sign_extend(to_ebits-from_ebits+2, exp);
|
||||
|
||||
// subtract lz for subnormal numbers.
|
||||
expr_ref lz_ext(m);
|
||||
lz_ext = m_bv_util.mk_zero_extend(to_ebits-from_ebits+2, lz);
|
||||
res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext);
|
||||
}
|
||||
else if (from_ebits > (to_ebits + 2))
|
||||
{
|
||||
expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m);
|
||||
expr_ref no_ovf(m), zero1(m), s_is_one(m), s_is_zero(m);
|
||||
high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp);
|
||||
low = m_bv_util.mk_extract(to_ebits+1, 0, exp);
|
||||
lows = m_bv_util.mk_extract(to_ebits+1, to_ebits+1, low);
|
||||
|
||||
expr_ref c2(m);
|
||||
m_simp.mk_ite(h_or_eq, s_is_one, m.mk_false(), c2);
|
||||
m_simp.mk_ite(h_and_eq, s_is_zero, c2, exponent_overflow);
|
||||
high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get());
|
||||
high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get());
|
||||
|
||||
zero1 = m_bv_util.mk_numeral(0, 1);
|
||||
m_simp.mk_eq(high_red_and, one1, h_and_eq);
|
||||
m_simp.mk_eq(high_red_or, zero1, h_or_eq);
|
||||
m_simp.mk_eq(lows, zero1, s_is_zero);
|
||||
m_simp.mk_eq(lows, one1, s_is_one);
|
||||
|
||||
// Note: Upon overflow, we _could_ try to shift the significand around...
|
||||
expr_ref c2(m);
|
||||
m_simp.mk_ite(h_or_eq, s_is_one, m.mk_false(), c2);
|
||||
m_simp.mk_ite(h_and_eq, s_is_zero, c2, exponent_overflow);
|
||||
|
||||
// Note: Upon overflow, we _could_ try to shift the significand around...
|
||||
|
||||
res_exp = low;
|
||||
}
|
||||
else
|
||||
res_exp = exp;
|
||||
// subtract lz for subnormal numbers.
|
||||
expr_ref lz_ext(m), lz_rest(m), lz_redor(m), lz_redor_bool(m);
|
||||
lz_ext = m_bv_util.mk_extract(to_ebits+1, 0, lz);
|
||||
lz_rest = m_bv_util.mk_extract(from_ebits-1, to_ebits+2, lz);
|
||||
lz_redor = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lz_rest.get());
|
||||
m_simp.mk_eq(lz_redor, one1, lz_redor_bool);
|
||||
m_simp.mk_or(exponent_overflow, lz_redor_bool, exponent_overflow);
|
||||
|
||||
// subtract lz for subnormal numbers.
|
||||
expr_ref lz_ext(m);
|
||||
lz_ext = m_bv_util.mk_zero_extend(to_ebits-from_ebits+2, lz);
|
||||
res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext);
|
||||
SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits+2);
|
||||
res_exp = m_bv_util.mk_bv_sub(low, lz_ext);
|
||||
}
|
||||
else // from_ebits == (to_ebits + 2)
|
||||
res_exp = m_bv_util.mk_bv_sub(exp, lz);
|
||||
|
||||
dbg_decouple("fpa2bv_to_float_res_sig", res_sig);
|
||||
dbg_decouple("fpa2bv_to_float_res_exp", res_exp);
|
||||
SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits+2);
|
||||
SASSERT(is_well_sorted(m, res_exp));
|
||||
|
||||
expr_ref rounded(m);
|
||||
round(s, rm, res_sgn, res_sig, res_exp, rounded);
|
||||
|
||||
dbg_decouple("fpa2bv_to_float_res_sig", res_sig);
|
||||
dbg_decouple("fpa2bv_to_float_res_exp", res_exp);
|
||||
|
||||
expr_ref is_neg(m), sig_inf(m);
|
||||
m_simp.mk_eq(sgn, one1, is_neg);
|
||||
mk_ite(is_neg, ninf, pinf, sig_inf);
|
||||
expr_ref rounded(m);
|
||||
round(s, rm, res_sgn, res_sig, res_exp, rounded);
|
||||
|
||||
expr_ref is_neg(m), sig_inf(m);
|
||||
m_simp.mk_eq(sgn, one1, is_neg);
|
||||
mk_ite(is_neg, ninf, pinf, sig_inf);
|
||||
|
||||
dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow);
|
||||
dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow);
|
||||
mk_ite(exponent_overflow, sig_inf, rounded, v6);
|
||||
|
||||
mk_ite(exponent_overflow, sig_inf, rounded, v6);
|
||||
|
||||
// And finally, we tie them together.
|
||||
mk_ite(c5, v5, v6, result);
|
||||
mk_ite(c4, v4, result, result);
|
||||
mk_ite(c3, v3, result, result);
|
||||
mk_ite(c2, v2, result, result);
|
||||
mk_ite(c1, v1, result, result);
|
||||
// And finally, we tie them together.
|
||||
mk_ite(c5, v5, v6, result);
|
||||
mk_ite(c4, v4, result, result);
|
||||
mk_ite(c3, v3, result, result);
|
||||
mk_ite(c2, v2, result, result);
|
||||
mk_ite(c1, v1, result, result);
|
||||
}
|
||||
}
|
||||
else {
|
||||
// .. other than that, we only support rationals for asFloat
|
||||
|
|
@ -2167,14 +2191,14 @@ void fpa2bv_converter::mk_bot_exp(unsigned sz, expr_ref & result) {
|
|||
}
|
||||
|
||||
void fpa2bv_converter::mk_min_exp(unsigned ebits, expr_ref & result) {
|
||||
SASSERT(ebits > 0);
|
||||
SASSERT(ebits >= 2);
|
||||
const mpz & z = m_mpf_manager.m_powers2.m1(ebits-1, true);
|
||||
result = m_bv_util.mk_numeral(z + mpz(1), ebits);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_max_exp(unsigned ebits, expr_ref & result) {
|
||||
SASSERT(ebits > 0);
|
||||
result = m_bv_util.mk_numeral(m_mpf_manager.m_powers2.m1(ebits-1, false), ebits);
|
||||
SASSERT(ebits >= 2);
|
||||
result = m_bv_util.mk_numeral(m_mpf_manager.m_powers2.m1(ebits-1, false), ebits);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref & result) {
|
||||
|
|
@ -2220,14 +2244,14 @@ void fpa2bv_converter::mk_bias(expr * e, expr_ref & result) {
|
|||
unsigned ebits = m_bv_util.get_bv_size(e);
|
||||
SASSERT(ebits >= 2);
|
||||
|
||||
expr_ref mask(m);
|
||||
mask = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits);
|
||||
result = m_bv_util.mk_bv_add(e, mask);
|
||||
expr_ref bias(m);
|
||||
bias = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits);
|
||||
result = m_bv_util.mk_bv_add(e, bias);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) {
|
||||
unsigned ebits = m_bv_util.get_bv_size(e);
|
||||
SASSERT(ebits >= 2);
|
||||
SASSERT(ebits >= 3);
|
||||
|
||||
expr_ref e_plus_one(m);
|
||||
e_plus_one = m_bv_util.mk_bv_add(e, m_bv_util.mk_numeral(1, ebits));
|
||||
|
|
@ -2263,6 +2287,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
|
|||
|
||||
expr_ref denormal_sig(m), denormal_exp(m);
|
||||
denormal_sig = m_bv_util.mk_zero_extend(1, sig);
|
||||
SASSERT(ebits >= 3); // Note: when ebits=2 there is no 1-exponent, so mk_unbias will produce a 0.
|
||||
denormal_exp = m_bv_util.mk_numeral(1, ebits);
|
||||
mk_unbias(denormal_exp, denormal_exp);
|
||||
dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp);
|
||||
|
|
@ -2436,13 +2461,12 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
|
|||
t = m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2));
|
||||
t = m_bv_util.mk_bv_sub(t, lz);
|
||||
t = m_bv_util.mk_bv_sub(t, m_bv_util.mk_sign_extend(2, e_min));
|
||||
expr_ref TINY(m);
|
||||
dbg_decouple("fpa2bv_rnd_t", t);
|
||||
expr_ref TINY(m);
|
||||
TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral((unsigned)-1, ebits+2));
|
||||
|
||||
TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;);
|
||||
SASSERT(is_well_sorted(m, TINY));
|
||||
|
||||
dbg_decouple("fpa2bv_rnd_TINY", TINY);
|
||||
TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;);
|
||||
SASSERT(is_well_sorted(m, TINY));
|
||||
|
||||
expr_ref beta(m);
|
||||
beta = m_bv_util.mk_bv_add(m_bv_util.mk_bv_sub(exp, lz), m_bv_util.mk_numeral(1, ebits+2));
|
||||
|
|
@ -2455,7 +2479,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
|
|||
dbg_decouple("fpa2bv_rnd_e_min", e_min);
|
||||
dbg_decouple("fpa2bv_rnd_e_max", e_max);
|
||||
|
||||
expr_ref sigma(m), sigma_add(m), e_min_p2(m);
|
||||
expr_ref sigma(m), sigma_add(m);
|
||||
sigma_add = m_bv_util.mk_bv_sub(exp, m_bv_util.mk_sign_extend(2, e_min));
|
||||
sigma_add = m_bv_util.mk_bv_add(sigma_add, m_bv_util.mk_numeral(1, ebits+2));
|
||||
m_simp.mk_ite(TINY, sigma_add, lz, sigma);
|
||||
|
|
@ -2477,9 +2501,10 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
|
|||
rs_sig(m), ls_sig(m), big_sh_sig(m), sigma_le_cap(m);
|
||||
sigma_neg = m_bv_util.mk_bv_neg(sigma);
|
||||
sigma_cap = m_bv_util.mk_numeral(sbits+2, sigma_size);
|
||||
sigma_le_cap = m_bv_util.mk_sle(sigma_neg, sigma_cap);
|
||||
sigma_le_cap = m_bv_util.mk_ule(sigma_neg, sigma_cap);
|
||||
m_simp.mk_ite(sigma_le_cap, sigma_neg, sigma_cap, sigma_neg_capped);
|
||||
dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg);
|
||||
dbg_decouple("fpa2bv_rnd_sigma_cap", sigma_cap);
|
||||
dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped);
|
||||
sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral((unsigned)-1, sigma_size));
|
||||
dbg_decouple("fpa2bv_rnd_sigma_lt_zero", sigma_lt_zero);
|
||||
|
|
|
|||
|
|
@ -360,6 +360,8 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
|
|||
mk_inf(ebits, sbits, x.sign, o);
|
||||
else if (is_zero(x))
|
||||
mk_zero(ebits, sbits, x.sign, o);
|
||||
else if (x.ebits == ebits && x.sbits == sbits)
|
||||
set(o, x);
|
||||
else {
|
||||
set(o, x);
|
||||
unpack(o, true);
|
||||
|
|
@ -1378,12 +1380,12 @@ bool mpf_manager::has_top_exp(mpf const & x) {
|
|||
}
|
||||
|
||||
mpf_exp_t mpf_manager::mk_bot_exp(unsigned ebits) {
|
||||
SASSERT(ebits > 0);
|
||||
SASSERT(ebits >= 2);
|
||||
return m_mpz_manager.get_int64(m_powers2.m1(ebits-1, true));
|
||||
}
|
||||
|
||||
mpf_exp_t mpf_manager::mk_top_exp(unsigned ebits) {
|
||||
SASSERT(ebits > 0);
|
||||
SASSERT(ebits >= 2);
|
||||
return m_mpz_manager.get_int64(m_powers2(ebits-1));
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue