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 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-09-17 01:39:44 +02:00
parent 8ff1e070be 65697eb277
commit da72911062
21 changed files with 507 additions and 660 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
.travis.yml
View file

@ -60,17 +60,15 @@ env:
- LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
# macOS (a.k.a OSX) support
# FIXME: macOS support is temporarily disabled due to @wintersteiger 's concerns.
# See https://github.com/Z3Prover/z3/pull/1207#issuecomment-322200998
# matrix:
# include:
# # For now just test a single configuration. macOS builds on TravisCI are
# # very slow so we should keep the number of configurations we test on this
# # OS to a minimum.
# - os: osx
# osx_image: xcode8.3
# # Note: Apple Clang does not support OpenMP
# env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0
matrix:
include:
# For now just test a single configuration. macOS builds on TravisCI are
# very slow so we should keep the number of configurations we test on this
# OS to a minimum.
- os: osx
osx_image: xcode8.3
# Note: Apple Clang does not support OpenMP
env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0
script:
# Use `travis_wait` when doing LTO builds because this configuration will
# have long link times during which it will not show any output which

67
src/ackermannization/ackr_model_converter.cpp
View file

@ -3,13 +3,13 @@ Copyright (c) 2015 Microsoft Corporation
Module Name:
ackr_model_converter.cpp
ackr_model_converter.cpp
Abstract:
Author:
Mikolas Janota
Mikolas Janota
Revision History:
--*/
@ -22,8 +22,8 @@ Revision History:
class ackr_model_converter : public model_converter {
public:
ackr_model_converter(ast_manager & m,
const ackr_info_ref& info,
model_ref& abstr_model)
const ackr_info_ref& info,
model_ref& abstr_model)
: m(m)
, info(info)
, abstr_model(abstr_model)
@ -31,7 +31,7 @@ public:
{ }
ackr_model_converter(ast_manager & m,
const ackr_info_ref& info)
const ackr_info_ref& info)
: m(m)
, info(info)
, fixed_model(false)
@ -51,8 +51,6 @@ public:
virtual void operator()(model_ref & md) { operator()(md, 0); }
//void display(std::ostream & out);
virtual model_converter * translate(ast_translation & translator) {
ackr_info_ref retv_info = info->translate(translator);
if (fixed_model) {
@ -63,42 +61,45 @@ public:
return alloc(ackr_model_converter, translator.to(), retv_info);
}
}
protected:
ast_manager& m;
ast_manager & m;
const ackr_info_ref info;
model_ref abstr_model;
bool fixed_model;
void convert(model * source, model * destination);
void add_entry(model_evaluator & evaluator,
app* term, expr* value,
obj_map<func_decl, func_interp*>& interpretations);
app* term, expr* value,
obj_map<func_decl, func_interp*>& interpretations);
void convert_constants(model * source, model * destination);
};
void ackr_model_converter::convert(model * source, model * destination) {
destination->copy_func_interps(*source);
destination->copy_usort_interps(*source);
convert_constants(source,destination);
convert_constants(source, destination);
}
void ackr_model_converter::convert_constants(model * source, model * destination) {
TRACE("ackr_model", tout << "converting constants\n";);
obj_map<func_decl, func_interp*> interpretations;
model_evaluator evaluator(*source);
evaluator.set_model_completion(true);
for (unsigned i = 0; i < source->get_num_constants(); i++) {
func_decl * const c = source->get_constant(i);
app * const term = info->find_term(c);
expr * value = source->get_const_interp(c);
if(!term) {
if (!term) {
destination->register_decl(c, value);
} else {
}
else {
add_entry(evaluator, term, value, interpretations);
}
}
obj_map<func_decl, func_interp*>::iterator e = interpretations.end();
for (obj_map<func_decl, func_interp*>::iterator i = interpretations.begin();
i!=e; ++i) {
i != e; ++i) {
func_decl* const fd = i->m_key;
func_interp* const fi = i->get_value();
fi->set_else(m.get_some_value(fd->get_range()));
@ -107,34 +108,40 @@ void ackr_model_converter::convert_constants(model * source, model * destination
}
void ackr_model_converter::add_entry(model_evaluator & evaluator,
app* term, expr* value,
obj_map<func_decl, func_interp*>& interpretations) {
app* term, expr* value,
obj_map<func_decl, func_interp*>& interpretations) {
TRACE("ackr_model", tout << "add_entry"
<< mk_ismt2_pp(term, m, 2)
<< "->"
<< mk_ismt2_pp(value, m, 2) << "\n";
<< mk_ismt2_pp(term, m, 2)
<< "->"
<< mk_ismt2_pp(value, m, 2) << "\n";
);
func_interp* fi = 0;
func_interp * fi = 0;
func_decl * const declaration = term->get_decl();
const unsigned sz = declaration->get_arity();
SASSERT(sz == term->get_num_args());
if (!interpretations.find(declaration, fi)) {
fi = alloc(func_interp,m,sz);
interpretations.insert(declaration, fi);
if (!interpretations.find(declaration, fi)) {
fi = alloc(func_interp, m, sz);
interpretations.insert(declaration, fi);
}
expr_ref_vector args(m);
for (unsigned gi = 0; gi < sz; ++gi) {
expr * const arg = term->get_arg(gi);
expr_ref aarg(m);
info->abstract(arg, aarg);
expr_ref arg_value(m);
evaluator(aarg,arg_value);
args.push_back(arg_value);
expr * const arg = term->get_arg(gi);
expr_ref aarg(m);
info->abstract(arg, aarg);
expr_ref arg_value(m);
evaluator(aarg, arg_value);
args.push_back(arg_value);
}
if (fi->get_entry(args.c_ptr()) == 0) {
TRACE("ackr_model",
tout << mk_ismt2_pp(declaration, m) << " args: " << std::endl;
for (unsigned i = 0; i < args.size(); i++)
tout << mk_ismt2_pp(args.get(i), m) << std::endl;
tout << " -> " << mk_ismt2_pp(value, m) << "\n"; );
fi->insert_new_entry(args.c_ptr(), value);
} else {
}
else {
TRACE("ackr_model", tout << "entry already present\n";);
}
}

8
src/ackermannization/ackr_model_converter.h
View file

@ -3,13 +3,13 @@ Copyright (c) 2015 Microsoft Corporation
Module Name:
ackr_model_converter.h
ackr_model_converter.h
Abstract:
Author:
Mikolas Janota
Mikolas Janota
Revision History:
--*/
@ -19,7 +19,7 @@ Revision History:
#include "tactic/model_converter.h"
#include "ackermannization/ackr_info.h"
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model);
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info);
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref & info, model_ref & abstr_model);
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref & info);
#endif /* LACKR_MODEL_CONVERTER_H_ */

16
src/api/api_ast.cpp
View file

@ -1204,16 +1204,12 @@ extern "C" {
case OP_FPA_TO_SBV: return Z3_OP_FPA_TO_SBV;
case OP_FPA_TO_REAL: return Z3_OP_FPA_TO_REAL;
case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV;
case OP_FPA_INTERNAL_MIN_I: return Z3_OP_FPA_MIN_I;
case OP_FPA_INTERNAL_MAX_I: return Z3_OP_FPA_MAX_I;
case OP_FPA_INTERNAL_BVWRAP: return Z3_OP_FPA_BVWRAP;
case OP_FPA_INTERNAL_BV2RM: return Z3_OP_FPA_BV2RM;
case OP_FPA_INTERNAL_MIN_UNSPECIFIED: return Z3_OP_FPA_MIN_UNSPECIFIED;
case OP_FPA_INTERNAL_MAX_UNSPECIFIED: return Z3_OP_FPA_MAX_UNSPECIFIED;
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: return Z3_OP_FPA_TO_UBV_UNSPECIFIED;
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return Z3_OP_FPA_TO_SBV_UNSPECIFIED;
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: return Z3_OP_FPA_TO_REAL_UNSPECIFIED;
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: return Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED;
case OP_FPA_MIN_I: return Z3_OP_FPA_MIN_I;
case OP_FPA_MAX_I: return Z3_OP_FPA_MAX_I;
case OP_FPA_BVWRAP: return Z3_OP_FPA_BVWRAP;
case OP_FPA_BV2RM: return Z3_OP_FPA_BV2RM;
case OP_FPA_MIN_UNSPECIFIED: return Z3_OP_FPA_MIN_UNSPECIFIED;
case OP_FPA_MAX_UNSPECIFIED: return Z3_OP_FPA_MAX_UNSPECIFIED;
return Z3_OP_UNINTERPRETED;
default:
return Z3_OP_INTERNAL;

16
src/api/z3_api.h
View file

@ -1005,18 +1005,6 @@ typedef enum
- Z3_OP_FPA_MAX_UNSPECIFIED: The same as Z3_OP_FPA_MAX, but the
arguments are expected to be zeroes with different signs.
- Z3_OP_FPA_TO_UBV_UNSPECIFIED: A term representing the unspecified
results of Z3_OP_FPA_TO_UBV.
- Z3_OP_FPA_TO_SBV_UNSPECIFIED: A term representing the unspecified
results of Z3_OP_FPA_TO_SBV.
- Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED: A term representing the unspecified
results of Z3_OP_FPA_TO_IEEE_BV.
- Z3_OP_FPA_TO_REAL_UNSPECIFIED: A term representing the unspecified
results of Z3_OP_FPA_TO_IEEE_BV.
- Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional
information is exposed. Tools may use the string representation of the
function declaration to obtain more information.
@ -1310,10 +1298,6 @@ typedef enum {
Z3_OP_FPA_BV2RM,
Z3_OP_FPA_MIN_UNSPECIFIED,
Z3_OP_FPA_MAX_UNSPECIFIED,
Z3_OP_FPA_TO_UBV_UNSPECIFIED,
Z3_OP_FPA_TO_SBV_UNSPECIFIED,
Z3_OP_FPA_TO_REAL_UNSPECIFIED,
Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED,
Z3_OP_INTERNAL,

81
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -120,9 +120,9 @@ expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr
res = m_fpa_util.mk_value(fp_val);
TRACE("bv2fpa", tout << "[" << mk_ismt2_pp(sgn, m) <<
" " << mk_ismt2_pp(exp, m) <<
" " << mk_ismt2_pp(sig, m) << "] == " <<
mk_ismt2_pp(res, m) << std::endl;);
" " << mk_ismt2_pp(exp, m) <<
" " << mk_ismt2_pp(sig, m) << "] == " <<
mk_ismt2_pp(res, m) << std::endl;);
m_fpa_util.fm().del(fp_val);
return res;
@ -263,7 +263,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
unsigned arity = bv_f->get_arity();
func_interp * bv_fi = mc->get_func_interp(bv_f);
if (bv_fi != 0) {
if (bv_fi) {
fpa_rewriter rw(m);
expr_ref ai(m);
result = alloc(func_interp, m, arity);
@ -285,15 +285,31 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
bv_fres = bv_fe->get_result();
ft_fres = rebuild_floats(mc, rng, to_app(bv_fres));
m_th_rw(ft_fres);
result->insert_new_entry(new_args.c_ptr(), ft_fres);
TRACE("bv2fpa",
for (unsigned i = 0; i < new_args.size(); i++)
tout << mk_ismt2_pp(bv_args[i], m) << " == " <<
mk_ismt2_pp(new_args[i], m) << std::endl;
tout << mk_ismt2_pp(bv_fres, m) << " == " << mk_ismt2_pp(ft_fres, m) << std::endl;);
func_entry * fe = result->get_entry(new_args.c_ptr());
if (fe == 0)
result->insert_new_entry(new_args.c_ptr(), ft_fres);
else {
// The BV model may have multiple equivalent entries using different
// representations of NaN. We can only keep one and we check that
// the results for all those entries are the same.
if (ft_fres != fe->get_result())
throw default_exception("BUG: UF function entries disagree with each other");
}
}
app_ref bv_els(m);
expr_ref ft_els(m);
bv_els = (app*)bv_fi->get_else();
ft_els = rebuild_floats(mc, rng, bv_els);
m_th_rw(ft_els);
result->set_else(ft_els);
if (bv_els != 0) {
ft_els = rebuild_floats(mc, rng, bv_els);
m_th_rw(ft_els);
result->set_else(ft_els);
}
}
return result;
@ -382,7 +398,7 @@ void bv2fpa_converter::convert_rm_consts(model_core * mc, model_core * target_mo
expr * bvval = to_app(val)->get_arg(0);
expr_ref fv(m);
fv = convert_bv2rm(mc, to_app(bvval));
TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;);
TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << std::endl;);
target_model->register_decl(var, fv);
seen.insert(to_app(bvval)->get_decl());
}
@ -447,14 +463,34 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
}
}
else {
func_interp * fmv = convert_func_interp(mc, f, it->m_value);
if (fmv) target_model->register_decl(f, fmv);
if (it->get_key().get_family_id() == m_fpa_util.get_fid()) {
// it->m_value contains the model for the unspecified cases of it->m_key.
func_interp * fmv = convert_func_interp(mc, f, it->m_value);
if (fmv) {
#if 0
// Upon request, add this 'recursive' definition?
unsigned n = fmv->get_arity();
expr_ref_vector args(m);
for (unsigned i = 0; i < n; i++)
args.push_back(m.mk_var(i, f->get_domain()[i]));
fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr()));
#else
fmv->set_else(0);
#endif
target_model->register_decl(f, fmv);
}
}
else {
func_interp * fmv = convert_func_interp(mc, f, it->m_value);
if (fmv) target_model->register_decl(f, fmv);
}
}
}
}
void bv2fpa_converter::display(std::ostream & out) {
out << "(fpa2bv-model-converter";
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++) {
@ -488,7 +524,6 @@ void bv2fpa_converter::display(std::ostream & out) {
out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " <<
mk_ismt2_pp(it->m_value.second, m, indent) << ")";
}
out << ")";
}
bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
@ -536,23 +571,3 @@ bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
return res;
}
void bv2fpa_converter::convert(model_core * mc, model_core * float_mdl) {
TRACE("bv2fpa", tout << "BV Model: " << std::endl;
for (unsigned i = 0; i < mc->get_num_constants(); i++)
tout << mc->get_constant(i)->get_name() << " --> " <<
mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl;
for (unsigned i = 0; i < mc->get_num_functions(); i++) {
func_decl * f = mc->get_function(i);
tout << f->get_name() << "(...) := " << std::endl;
func_interp * fi = mc->get_func_interp(f);
for (unsigned j = 0; j < fi->num_entries(); j++) {
func_entry const * fe = fi->get_entry(j);
for (unsigned k = 0; k < f->get_arity(); k++) {
tout << mk_ismt2_pp(fe->get_arg(k), m) << " ";
}
tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl;
}
tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
});
}

1
src/ast/fpa/bv2fpa_converter.h
View file

@ -50,7 +50,6 @@ public:
expr_ref convert_bv2rm(expr * eval_v);
expr_ref convert_bv2rm(model_core * mc, app * val);
void convert(model_core * mc, model_core * float_mdl);
void convert_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
void convert_rm_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
void convert_min_max_specials(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);

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

@ -1231,11 +1231,11 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
expr_ref c(m), v(m);
c = m.mk_and(both_are_zero, pn_or_np);
v = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, x, y);
v = m.mk_app(m_util.get_family_id(), OP_FPA_MIN_UNSPECIFIED, x, y);
// Note: This requires BR_REWRITE_FULL afterwards.
expr_ref min_i(m);
min_i = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MIN_I, x, y);
min_i = m.mk_app(m_util.get_family_id(), OP_FPA_MIN_I, x, y);
m_simp.mk_ite(c, v, min_i, result);
}
@ -1324,11 +1324,11 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
expr_ref c(m), v(m);
c = m.mk_and(both_are_zero, pn_or_np);
v = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, x, y);
v = m.mk_app(m_util.get_family_id(), OP_FPA_MAX_UNSPECIFIED, x, y);
// Note: This requires BR_REWRITE_FULL afterwards.
expr_ref max_i(m);
max_i = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MAX_I, x, y);
max_i = m.mk_app(m_util.get_family_id(), OP_FPA_MAX_I, x, y);
m_simp.mk_ite(c, v, max_i, result);
}
@ -2855,8 +2855,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;);
expr_ref unspec(m);
unspec = mk_to_real_unspecified(ebits, sbits);
mk_to_real_unspecified(f, num, args, unspec);
result = m.mk_ite(x_is_zero, zero, res);
result = m.mk_ite(x_is_inf, unspec, result);
result = m.mk_ite(x_is_nan, unspec, result);
@ -3158,14 +3157,11 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits),
m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
m_bv_util.mk_numeral(1, 1))));
else {
app_ref unspec(m);
unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits);
mk_to_ieee_bv_unspecified(unspec->get_decl(), 0, 0, nanv);
}
else
mk_to_ieee_bv_unspecified(f, num, args, nanv);
expr_ref sgn_e_s(m);
sgn_e_s = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
join_fp(x, sgn_e_s);
m_simp.mk_ite(x_is_nan, nanv, sgn_e_s, result);
TRACE("fpa2bv_to_ieee_bv", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
@ -3173,9 +3169,10 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
}
void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 0);
unsigned ebits = f->get_parameter(0).get_int();
unsigned sbits = f->get_parameter(1).get_int();
SASSERT(num == 1);
SASSERT(m_util.is_float(args[0]));
unsigned ebits = f->get_domain()[0]->get_parameter(0).get_int();
unsigned sbits = f->get_domain()[0]->get_parameter(1).get_int();
if (m_hi_fp_unspecified) {
result = m_bv_util.mk_concat(m_bv_util.mk_concat(
@ -3184,26 +3181,30 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
m_bv_util.mk_numeral(1, sbits-1));
}
else {
func_decl * fd;
if (m_uf2bvuf.find(f, fd))
result = m.mk_const(fd);
else {
fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
m_uf2bvuf.insert(f, fd);
expr * n = args[0];
expr_ref n_bv(m);
join_fp(n, n_bv);
func_decl * f_bv;
if (!m_uf2bvuf.find(f, f_bv)) {
sort * domain[2] = { m.get_sort(n_bv) };
f_bv = m.mk_fresh_func_decl(0, 1, domain, f->get_range());
m_uf2bvuf.insert(f, f_bv);
m.inc_ref(f);
m.inc_ref(fd);
result = m.mk_const(fd);
expr_ref exp_bv(m), exp_all_ones(m);
exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result);
exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_numeral(-1, ebits));
m_extra_assertions.push_back(exp_all_ones);
expr_ref sig_bv(m), sig_is_non_zero(m);
sig_bv = m_bv_util.mk_extract(sbits-2, 0, result);
sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1)));
m_extra_assertions.push_back(sig_is_non_zero);
m.inc_ref(f_bv);
}
result = m.mk_app(f_bv, n_bv);
expr_ref exp_bv(m), exp_all_ones(m);
exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result);
exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_numeral(-1, ebits));
m_extra_assertions.push_back(exp_all_ones);
expr_ref sig_bv(m), sig_is_non_zero(m);
sig_bv = m_bv_util.mk_extract(sbits-2, 0, result);
sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1)));
m_extra_assertions.push_back(sig_is_non_zero);
}
TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
@ -3238,18 +3239,16 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
mk_is_nzero(x, x_is_nzero);
// NaN, Inf, or negative (except -0) -> unspecified
expr_ref c1(m), v1(m);
if (!is_signed) {
expr_ref c1(m), v1(m), unspec_v(m);
if (!is_signed)
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(ebits, sbits, bv_sz);
}
else {
else
c1 = m.mk_or(x_is_nan, x_is_inf);
v1 = mk_to_sbv_unspecified(ebits, sbits, bv_sz);
}
mk_to_bv_unspecified(f, num, args, unspec_v);
v1 = unspec_v;
dbg_decouple("fpa2bv_to_bv_c1", c1);
// +-Zero -> 0
// +-0 -> 0
expr_ref c2(m), v2(m);
c2 = x_is_zero;
v2 = m_bv_util.mk_numeral(rational(0), bv_srt);
@ -3270,60 +3269,57 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
SASSERT(m_bv_util.get_bv_size(exp) == ebits);
SASSERT(m_bv_util.get_bv_size(lz) == ebits);
unsigned sig_sz = m_bv_util.get_bv_size(sig);
SASSERT(sig_sz == sbits);
unsigned sig_sz = sbits;
if (sig_sz < (bv_sz + 3))
sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, bv_sz - sig_sz + 3));
sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, bv_sz-sig_sz+3));
sig_sz = m_bv_util.get_bv_size(sig);
SASSERT(sig_sz >= (bv_sz + 3));
expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), bv0_e2(m), shift_abs(m), shift_le_0(m);
exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp),
m_bv_util.mk_zero_extend(2, lz));
e_m_lz_m_bv_sz = m_bv_util.mk_bv_sub(exp_m_lz,
m_bv_util.mk_numeral(bv_sz - 1, ebits + 2));
shift = m_bv_util.mk_bv_neg(e_m_lz_m_bv_sz);
bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2);
shift_le_0 = m_bv_util.mk_sle(shift, bv0_e2);
shift_abs = m.mk_ite(shift_le_0, e_m_lz_m_bv_sz, shift);
SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2);
SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2);
dbg_decouple("fpa2bv_to_bv_shift", shift);
dbg_decouple("fpa2bv_to_bv_shift_abs", shift_abs);
// x is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long
// [1][ ... sig ... ][r][g][ ... s ...]
// [ ... ubv ... ][r][g][ ... s ... ]
shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs);
SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz);
expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), is_neg_shift(m), big_sig(m);
exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp),
m_bv_util.mk_zero_extend(2, lz));
expr_ref c_in_limits(m);
if (!is_signed)
c_in_limits = m_bv_util.mk_sle(bv0_e2, shift);
else {
expr_ref one_sle_shift(m), one_eq_shift(m), p2(m), sig_is_p2(m), shift1_and_sig_p2(m);
one_sle_shift = m_bv_util.mk_sle(m_bv_util.mk_numeral(1, ebits + 2), shift);
one_eq_shift = m.mk_eq(m_bv_util.mk_numeral(0, ebits + 2), shift);
p2 = m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, sig_sz-1));
sig_is_p2 = m.mk_eq(sig, p2);
shift1_and_sig_p2 = m.mk_and(one_eq_shift, sig_is_p2);
c_in_limits = m.mk_or(one_sle_shift, shift1_and_sig_p2);
// big_sig is +- [... bv_sz+2 bits ...].[r][g][ ... sbits-1 ... ]
big_sig = m_bv_util.mk_zero_extend(bv_sz+2, sig);
unsigned big_sig_sz = sig_sz+bv_sz+2;
SASSERT(m_bv_util.get_bv_size(big_sig) == big_sig_sz);
is_neg_shift = m_bv_util.mk_sle(exp_m_lz, m_bv_util.mk_numeral(0, ebits+2));
shift = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_neg(exp_m_lz), exp_m_lz);
if (ebits+2 < big_sig_sz)
shift = m_bv_util.mk_zero_extend(big_sig_sz-ebits-2, shift);
else if (ebits+2 > big_sig_sz) {
expr_ref upper(m);
upper = m_bv_util.mk_extract(big_sig_sz, ebits+2, shift);
shift = m_bv_util.mk_extract(ebits+1, 0, shift);
shift = m.mk_ite(m.mk_eq(upper, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(upper))),
shift,
m_bv_util.mk_numeral(big_sig_sz-1, ebits+2));
}
dbg_decouple("fpa2bv_to_bv_in_limits", c_in_limits);
dbg_decouple("fpa2bv_to_bv_shift_uncapped", shift);
SASSERT(m_bv_util.get_bv_size(shift) == m_bv_util.get_bv_size(big_sig));
dbg_decouple("fpa2bv_to_bv_big_sig", big_sig);
expr_ref r_shifted_sig(m), l_shifted_sig(m);
r_shifted_sig = m_bv_util.mk_bv_lshr(sig, shift_abs);
l_shifted_sig = m_bv_util.mk_bv_shl(sig, m_bv_util.mk_bv_sub(
m_bv_util.mk_numeral(m_bv_util.get_bv_size(sig), m_bv_util.get_bv_size(sig)),
shift_abs));
dbg_decouple("fpa2bv_to_bv_r_shifted_sig", r_shifted_sig);
dbg_decouple("fpa2bv_to_bv_l_shifted_sig", l_shifted_sig);
expr_ref shift_limit(m);
shift_limit = m_bv_util.mk_numeral(bv_sz+2, m_bv_util.get_bv_size(shift));
shift = m.mk_ite(m_bv_util.mk_ule(shift, shift_limit), shift, shift_limit);
dbg_decouple("fpa2bv_to_bv_shift_limit", shift_limit);
dbg_decouple("fpa2bv_to_bv_is_neg_shift", is_neg_shift);
dbg_decouple("fpa2bv_to_bv_shift", shift);
expr_ref last(m), round(m), sticky(m);
last = m_bv_util.mk_extract(sig_sz - bv_sz - 0, sig_sz - bv_sz - 0, r_shifted_sig);
round = m_bv_util.mk_extract(sig_sz - bv_sz - 1, sig_sz - bv_sz - 1, r_shifted_sig);
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, l_shifted_sig.get());
expr_ref big_sig_shifted(m), int_part(m), last(m), round(m), stickies(m), sticky(m);
big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift),
m_bv_util.mk_bv_shl(big_sig, shift));
int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-(bv_sz+3), big_sig_shifted);
SASSERT(m_bv_util.get_bv_size(int_part) == bv_sz+3);
last = m_bv_util.mk_extract(big_sig_sz-(bv_sz+3), big_sig_sz-(bv_sz+3), big_sig_shifted);
round = m_bv_util.mk_extract(big_sig_sz-(bv_sz+4), big_sig_sz-(bv_sz+4), big_sig_shifted);
stickies = m_bv_util.mk_extract(big_sig_sz-(bv_sz+5), 0, big_sig_shifted);
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, stickies.get());
dbg_decouple("fpa2bv_to_bv_big_sig_shifted", big_sig_shifted);
dbg_decouple("fpa2bv_to_bv_int_part", int_part);
dbg_decouple("fpa2bv_to_bv_last", last);
dbg_decouple("fpa2bv_to_bv_round", round);
dbg_decouple("fpa2bv_to_bv_sticky", sticky);
@ -3333,33 +3329,31 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1);
dbg_decouple("fpa2bv_to_bv_rounding_decision", rounding_decision);
expr_ref unrounded_sig(m), pre_rounded(m), inc(m);
unrounded_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz, r_shifted_sig));
inc = m_bv_util.mk_zero_extend(1, m_bv_util.mk_zero_extend(bv_sz - 1, rounding_decision));
pre_rounded = m_bv_util.mk_bv_add(unrounded_sig, inc);
expr_ref inc(m), pre_rounded(m);
inc = m_bv_util.mk_zero_extend(bv_sz+2, rounding_decision);
pre_rounded = m_bv_util.mk_bv_add(int_part, inc);
dbg_decouple("fpa2bv_to_bv_inc", inc);
dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded);
expr_ref rnd_overflow(m), rnd(m), rnd_has_overflown(m);
rnd_overflow = m_bv_util.mk_extract(bv_sz, bv_sz, pre_rounded);
rnd = m_bv_util.mk_extract(bv_sz - 1, 0, pre_rounded);
rnd_has_overflown = m.mk_eq(rnd_overflow, bv1);
dbg_decouple("fpa2bv_to_bv_rnd_has_overflown", rnd_has_overflown);
if (is_signed) {
expr_ref sgn_eq_1(m), neg_rnd(m);
sgn_eq_1 = m.mk_eq(sgn, bv1);
neg_rnd = m_bv_util.mk_bv_neg(rnd);
m_simp.mk_ite(sgn_eq_1, neg_rnd, rnd, rnd);
expr_ref in_range(m);
if (!is_signed) {
expr_ref ul(m);
ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_numeral(-1, bv_sz));
in_range = m_bv_util.mk_ule(pre_rounded, ul);
}
else {
expr_ref ll(m), ul(m);
ll = m_bv_util.mk_sign_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1)));
ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_numeral(-1, bv_sz-1));
in_range = m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul));
}
dbg_decouple("fpa2bv_to_bv_in_range", in_range);
dbg_decouple("fpa2bv_to_bv_rnd", rnd);
expr_ref rounded(m);
rounded = m_bv_util.mk_extract(bv_sz-1, 0, pre_rounded);
dbg_decouple("fpa2bv_to_bv_rounded", rounded);
expr_ref unspec(m);
unspec = is_signed ? mk_to_sbv_unspecified(ebits, sbits, bv_sz) :
mk_to_ubv_unspecified(ebits, sbits, bv_sz);
result = m.mk_ite(rnd_has_overflown, unspec, rnd);
result = m.mk_ite(c_in_limits, result, unspec);
result = m.mk_ite(m.mk_not(in_range), unspec_v, rounded);
result = m.mk_ite(c2, v2, result);
result = m.mk_ite(c1, v1, result);
@ -3378,85 +3372,54 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
mk_to_bv(f, num, args, true, result);
}
void fpa2bv_converter::mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 0);
unsigned width = m_bv_util.get_bv_size(f->get_range());
void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
SASSERT(m_util.is_bv2rm(args[0]));
SASSERT(m_util.is_float(args[1]));
if (m_hi_fp_unspecified)
result = m_bv_util.mk_numeral(0, width);
result = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(f->get_range()));
else {
func_decl * fd;
if (!m_uf2bvuf.find(f, fd)) {
fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
m_uf2bvuf.insert(f, fd);
expr * rm_bv = to_app(args[0])->get_arg(0);
expr * n = args[1];
expr_ref n_bv(m);
join_fp(n, n_bv);
func_decl * f_bv;
if (!m_uf2bvuf.find(f, f_bv)) {
sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(n_bv) };
f_bv = m.mk_fresh_func_decl(0, 2, domain, f->get_range());
m_uf2bvuf.insert(f, f_bv);
m.inc_ref(f);
m.inc_ref(fd);
m.inc_ref(f_bv);
}
result = m.mk_const(fd);
result = m.mk_app(f_bv, rm_bv, n_bv);
}
TRACE("fpa2bv_to_ubv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
TRACE("fpa2bv_to_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
SASSERT(is_well_sorted(m, result));
}
expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
expr_ref res(m);
app_ref u(m);
u = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width);
mk_to_sbv_unspecified(u->get_decl(), 0, 0, res);
return res;
}
void fpa2bv_converter::mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 0);
unsigned width = m_bv_util.get_bv_size(f->get_range());
if (m_hi_fp_unspecified)
result = m_bv_util.mk_numeral(0, width);
else {
func_decl * fd;
if (!m_uf2bvuf.find(f, fd)) {
fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
m_uf2bvuf.insert(f, fd);
m.inc_ref(f);
m.inc_ref(fd);
}
result = m.mk_const(fd);
}
TRACE("fpa2bv_to_sbv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
SASSERT(is_well_sorted(m, result));
}
expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
expr_ref res(m);
app_ref u(m);
u = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);
mk_to_sbv_unspecified(u->get_decl(), 0, 0, res);
return res;
}
void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
if (m_hi_fp_unspecified)
result = m_arith_util.mk_numeral(rational(0), false);
else {
func_decl * fd;
if (!m_uf2bvuf.find(f, fd)) {
fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
m_uf2bvuf.insert(f, fd);
m.inc_ref(f);
m.inc_ref(fd);
}
result = m.mk_const(fd);
}
}
expr * n = args[0];
expr_ref n_bv(m);
join_fp(n, n_bv);
expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) {
expr_ref res(m);
app_ref u(m);
u = m_util.mk_internal_to_real_unspecified(ebits, sbits);
mk_to_real_unspecified(u->get_decl(), 0, 0, res);
return res;
func_decl * f_bv;
if (!m_uf2bvuf.find(f, f_bv)) {
sort * domain[2] = { m.get_sort(n_bv) };
f_bv = m.mk_fresh_func_decl(0, 1, domain, f->get_range());
m_uf2bvuf.insert(f, f_bv);
m.inc_ref(f);
m.inc_ref(f_bv);
}
result = m.mk_app(f_bv, n_bv);
}
}
void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@ -3467,6 +3430,7 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e
result = m_util.mk_fp(args[0], args[1], args[2]);
TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;);
}
void fpa2bv_converter::split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const {
SASSERT(m_util.is_fp(e));
SASSERT(to_app(e)->get_num_args() == 3);
@ -3485,6 +3449,14 @@ void fpa2bv_converter::split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_r
sig = e_sig;
}
void fpa2bv_converter::join_fp(expr * e, expr_ref & res) {
SASSERT(m_util.is_fp(e));
SASSERT(to_app(e)->get_num_args() == 3);
expr *sgn, *exp, *sig;
split_fp(e, sgn, exp, sig);
res = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, exp), sig);
}
void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp;
split_fp(e, sgn, exp, sig);
@ -4051,7 +4023,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
// put the sticky bit into the significand.
expr_ref ext_sticky(m);
ext_sticky = m_bv_util.mk_zero_extend(sbits+1, sticky);
expr * tmp[] = { sig, ext_sticky };
expr * tmp[2] = { sig, ext_sticky };
sig = m_bv_util.mk_bv_or(2, tmp);
SASSERT(is_well_sorted(m, sig));
SASSERT(m_bv_util.get_bv_size(sig) == sbits+2);

8
src/ast/fpa/fpa2bv_converter.h
View file

@ -76,6 +76,7 @@ public:
void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const;
void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const;
void join_fp(expr * e, expr_ref & res);
void mk_eq(expr * a, expr * b, expr_ref & result);
void mk_ite(expr * c, expr * t, expr * f, expr_ref & result);
@ -138,9 +139,8 @@ public:
void mk_to_fp_real_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
@ -226,10 +226,6 @@ private:
void mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & x, expr_ref & result);
void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result);
expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits);
};
#endif

16
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -143,24 +143,20 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL;
case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL;
case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_min_max_unspecified(f, args[0], args[1]); return BR_DONE;
case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE;
case OP_FPA_MIN_UNSPECIFIED:
case OP_FPA_MAX_UNSPECIFIED: result = m_conv.mk_min_max_unspecified(f, args[0], args[1]); return BR_DONE;
case OP_FPA_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE;
case OP_FPA_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_BV2RM:
case OP_FPA_BVWRAP:
case OP_FPA_BV2RM:
return BR_FAILED;
default:

121
src/ast/fpa_decl_plugin.cpp
View file

@ -361,10 +361,10 @@ func_decl * fpa_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_parameters
case OP_FPA_REM: name = "fp.rem"; break;
case OP_FPA_MIN: name = "fp.min"; break;
case OP_FPA_MAX: name = "fp.max"; break;
case OP_FPA_INTERNAL_MIN_I: name = "fp.min_i"; break;
case OP_FPA_INTERNAL_MAX_I: name = "fp.max_i"; break;
case OP_FPA_INTERNAL_MIN_UNSPECIFIED: name = "fp.min_unspecified"; break;
case OP_FPA_INTERNAL_MAX_UNSPECIFIED: name = "fp.max_unspecified"; break;
case OP_FPA_MIN_I: name = "fp.min_i"; break;
case OP_FPA_MAX_I: name = "fp.max_i"; break;
case OP_FPA_MIN_UNSPECIFIED: name = "fp.min_unspecified"; break;
case OP_FPA_MAX_UNSPECIFIED: name = "fp.max_unspecified"; break;
default:
UNREACHABLE();
break;
@ -676,10 +676,10 @@ func_decl * fpa_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters,
return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k));
}
func_decl * fpa_decl_plugin::mk_internal_bv2rm(decl_kind k, unsigned num_parameters, parameter const * parameters,
func_decl * fpa_decl_plugin::mk_bv2rm(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 1)
m_manager->raise_exception("invalid number of arguments to internal_rm");
m_manager->raise_exception("invalid number of arguments to bv2rm");
if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) || domain[0]->get_parameter(0).get_int() != 3)
m_manager->raise_exception("sort mismatch, expected argument of sort bitvector, size 3");
if (!is_rm_sort(range))
@ -690,7 +690,7 @@ func_decl * fpa_decl_plugin::mk_internal_bv2rm(decl_kind k, unsigned num_paramet
return m_manager->mk_func_decl(symbol("rm"), 1, &bv_srt, range, func_decl_info(m_family_id, k, num_parameters, parameters));
}
func_decl * fpa_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
func_decl * fpa_decl_plugin::mk_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 1)
m_manager->raise_exception("invalid number of arguments to bv_wrap");
@ -711,65 +711,6 @@ func_decl * fpa_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_param
}
}
func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified(
decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 0)
m_manager->raise_exception("invalid number of arguments to fp.to_ubv_unspecified");
if (num_parameters != 3)
m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 3");
if (!parameters[0].is_int() || !parameters[1].is_int() || !parameters[2].is_int())
m_manager->raise_exception("invalid parameters type provided to fp.to_ubv_unspecified; expecting 3 integers");
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, &parameters[2]);
return m_manager->mk_func_decl(symbol("fp.to_ubv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
}
func_decl * fpa_decl_plugin::mk_internal_to_sbv_unspecified(
decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 0)
m_manager->raise_exception("invalid number of arguments to fp.to_sbv_unspecified");
if (num_parameters != 3)
m_manager->raise_exception("invalid number of parameters to fp.to_sbv_unspecified; expecting 3");
if (!parameters[0].is_int() || !parameters[1].is_int() || !parameters[2].is_int())
m_manager->raise_exception("invalid parameters type provided to fp.to_sbv_unspecified; expecting 3 integers");
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, &parameters[2]);
return m_manager->mk_func_decl(symbol("fp.to_sbv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
}
func_decl * fpa_decl_plugin::mk_internal_to_real_unspecified(
decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 0)
m_manager->raise_exception("invalid number of arguments to fp.to_real_unspecified");
if (num_parameters != 2)
m_manager->raise_exception("invalid number of parameters to fp.to_real_unspecified; expecting 2");
if (!parameters[0].is_int() || !parameters[1].is_int())
m_manager->raise_exception("invalid parameters type provided to fp.to_real_unspecified; expecting 2 integers");
if (!is_sort_of(range, m_arith_fid, REAL_SORT))
m_manager->raise_exception("sort mismatch, expected range of Real sort");
return m_manager->mk_func_decl(symbol("fp.to_real_unspecified"), 0, domain, m_real_sort, func_decl_info(m_family_id, k, num_parameters, parameters));
}
func_decl * fpa_decl_plugin::mk_internal_to_ieee_bv_unspecified(
decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
if (arity != 0)
m_manager->raise_exception("invalid number of arguments to fp.to_ieee_bv_unspecified; expecting none");
if (num_parameters != 2)
m_manager->raise_exception("invalid number of parameters to fp.to_ieee_bv_unspecified; expecting 2");
if (!parameters[0].is_int() || !parameters[1].is_int())
m_manager->raise_exception("invalid parameters type provided to fp.to_ieee_bv_unspecified; expecting 2 integers");
parameter width_p[1] = { parameter(parameters[0].get_int() + parameters[1].get_int()) };
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, width_p);
return m_manager->mk_func_decl(symbol("fp.to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
}
func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
switch (k) {
@ -835,25 +776,17 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
case OP_FPA_TO_IEEE_BV:
return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_BVWRAP:
return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_BV2RM:
return mk_internal_bv2rm(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_BVWRAP:
return mk_bv_wrap(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_BV2RM:
return mk_bv2rm(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_MIN_I:
case OP_FPA_INTERNAL_MAX_I:
case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
case OP_FPA_MIN_I:
case OP_FPA_MAX_I:
case OP_FPA_MIN_UNSPECIFIED:
case OP_FPA_MAX_UNSPECIFIED:
return mk_binary_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
return mk_internal_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
return mk_internal_to_sbv_unspecified(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
return mk_internal_to_real_unspecified(k, num_parameters, parameters, arity, domain, range);
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
return mk_internal_to_ieee_bv_unspecified(k, num_parameters, parameters, arity, domain, range);
default:
m_manager->raise_exception("unsupported floating point operator");
return 0;
@ -1054,30 +987,6 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) {
return mk_value(v);
}
app * fpa_util::mk_internal_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) };
sort * range = m_bv_util.mk_sort(width);
return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, 3, ps, 0, 0, range);
}
app * fpa_util::mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) };
sort * range = m_bv_util.mk_sort(width);
return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, 3, ps, 0, 0, range);
}
app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) {
parameter ps[] = { parameter(ebits), parameter(sbits) };
sort * range = m_bv_util.mk_sort(ebits+sbits);
return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, 2, ps, 0, 0, range);
}
app * fpa_util::mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits) {
parameter ps[] = { parameter(ebits), parameter(sbits) };
sort * range = m_a_util.mk_real();
return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 2, ps, 0, 0, range);
}
bool fpa_util::contains_floats(ast * a) {
switch (a->get_kind()) {
case AST_APP: {

88
src/ast/fpa_decl_plugin.h
View file

@ -86,18 +86,13 @@ enum fpa_op_kind {
/* Extensions */
OP_FPA_TO_IEEE_BV,
/* Internal use only */
OP_FPA_INTERNAL_BVWRAP,
OP_FPA_INTERNAL_BV2RM,
OP_FPA_BVWRAP,
OP_FPA_BV2RM,
OP_FPA_INTERNAL_MIN_I,
OP_FPA_INTERNAL_MAX_I,
OP_FPA_INTERNAL_MIN_UNSPECIFIED,
OP_FPA_INTERNAL_MAX_UNSPECIFIED,
OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED,
OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED,
OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED,
OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED,
OP_FPA_MIN_I,
OP_FPA_MAX_I,
OP_FPA_MIN_UNSPECIFIED,
OP_FPA_MAX_UNSPECIFIED,
LAST_FLOAT_OP
};
@ -164,38 +159,16 @@ class fpa_decl_plugin : public decl_plugin {
func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_bv2rm(decl_kind k, unsigned num_parameters, parameter const * parameters,
func_decl * mk_bv2rm(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
func_decl * mk_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_to_ubv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_to_sbv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_to_real_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_to_ieee_bv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
virtual void set_manager(ast_manager * m, family_id id);
unsigned mk_id(mpf const & v);
void recycled_id(unsigned id);
virtual bool is_considered_uninterpreted(func_decl * f) {
if (f->get_family_id() != get_family_id())
return false;
switch (f->get_decl_kind())
{
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
return true;
default:
return false;
}
return false;
}
virtual bool is_considered_uninterpreted(func_decl * f) { return false; }
public:
fpa_decl_plugin();
@ -249,6 +222,7 @@ public:
family_id get_fid() const { return m_fid; }
family_id get_family_id() const { return m_fid; }
arith_util & au() { return m_a_util; }
bv_util & bu() { return m_bv_util; }
fpa_decl_plugin & plugin() { return *m_plugin; }
sort * mk_float_sort(unsigned ebits, unsigned sbits);
@ -373,35 +347,27 @@ public:
app * mk_bv2rm(expr * bv3) {
SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3);
return m().mk_app(m_fid, OP_FPA_INTERNAL_BV2RM, 0, 0, 1, &bv3, mk_rm_sort());
return m().mk_app(m_fid, OP_FPA_BV2RM, 0, 0, 1, &bv3, mk_rm_sort());
}
app * mk_internal_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
app * mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
app * mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits);
bool is_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); }
bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BVWRAP; }
bool is_bv2rm(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BV2RM); }
bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BV2RM; }
bool is_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_BVWRAP); }
bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BVWRAP; }
bool is_bv2rm(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_BV2RM); }
bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BV2RM; }
bool is_min_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_I); }
bool is_min_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED); }
bool is_max_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_I); }
bool is_max_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED); }
bool is_to_ubv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED); }
bool is_to_sbv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED); }
bool is_to_ieee_bv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED); }
bool is_to_real_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED); }
bool is_min_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MIN_I); }
bool is_min_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MIN_UNSPECIFIED); }
bool is_max_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MAX_I); }
bool is_max_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MAX_UNSPECIFIED); }
bool is_to_ubv(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_UBV); }
bool is_to_sbv(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_SBV); }
bool is_min_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_I; }
bool is_min_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_UNSPECIFIED; }
bool is_max_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_I; }
bool is_max_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_UNSPECIFIED; }
bool is_to_ubv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED; }
bool is_to_sbv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED; }
bool is_to_ieee_bv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED; }
bool is_to_real_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED; }
bool is_min_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MIN_I; }
bool is_min_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MIN_UNSPECIFIED; }
bool is_max_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MAX_I; }
bool is_max_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MAX_UNSPECIFIED; }
bool is_to_ubv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_UBV; }
bool is_to_sbv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_SBV; }
bool contains_floats(ast * a);
};

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

@ -94,21 +94,14 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break;
case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
case OP_FPA_INTERNAL_MIN_I:SASSERT(num_args == 2); st = mk_min_i(f, args[0], args[1], result); break;
case OP_FPA_INTERNAL_MAX_I: SASSERT(num_args == 2); st = mk_max_i(f, args[0], args[1], result); break;
case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
case OP_FPA_MIN_I:SASSERT(num_args == 2); st = mk_min_i(f, args[0], args[1], result); break;
case OP_FPA_MAX_I: SASSERT(num_args == 2); st = mk_max_i(f, args[0], args[1], result); break;
case OP_FPA_MIN_UNSPECIFIED:
case OP_FPA_MAX_UNSPECIFIED:
SASSERT(num_args == 2); st = BR_FAILED; break;
case OP_FPA_INTERNAL_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break;
case OP_FPA_INTERNAL_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break;
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
st = BR_FAILED;
break;
case OP_FPA_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break;
case OP_FPA_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break;
default:
NOT_IMPLEMENTED_YET();
@ -116,49 +109,10 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
return st;
}
br_status fpa_rewriter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) {
bv_util bu(m());
if (m_hi_fp_unspecified) {
// The "hardware interpretation" is 0.
result = bu.mk_numeral(0, width);
return BR_DONE;
}
else {
result = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width);
return BR_REWRITE1;
}
}
br_status fpa_rewriter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) {
bv_util bu(m());
if (m_hi_fp_unspecified) {
// The "hardware interpretation" is 0.
result = bu.mk_numeral(0, width);
return BR_DONE;
}
else {
result = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);
return BR_REWRITE1;
}
}
br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result) {
if (m_hi_fp_unspecified) {
// The "hardware interpretation" is 0.
result = m_util.au().mk_numeral(rational(0), false);
return BR_DONE;
}
else {
result = m_util.mk_internal_to_real_unspecified(ebits, sbits);
return BR_REWRITE1;
}
}
br_status fpa_rewriter::mk_to_fp(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());
bv_util bu(m());
scoped_mpf v(m_fm);
mpf_rounding_mode rmv;
rational r1, r2, r3;
@ -167,7 +121,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
unsigned sbits = f->get_parameter(1).get_int();
if (num_args == 1) {
if (bu.is_numeral(args[0], r1, bvs1)) {
if (m_util.bu().is_numeral(args[0], r1, bvs1)) {
// BV -> float
SASSERT(bvs1 == sbits + ebits);
unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
@ -226,10 +180,10 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
// TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
return BR_DONE;
}
else if (bu.is_numeral(args[1], r1, bvs1)) {
else if (m_util.bu().is_numeral(args[1], r1, bvs1)) {
// rm + signed bv -> float
TRACE("fp_rewriter", tout << "r1: " << r1 << std::endl;);
r1 = bu.norm(r1, bvs1, true);
r1 = m_util.bu().norm(r1, bvs1, true);
TRACE("fp_rewriter", tout << "r1 norm: " << r1 << std::endl;);
m_fm.set(v, ebits, sbits, rmv, r1.to_mpq());
result = m_util.mk_value(v);
@ -265,9 +219,9 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
result = m_util.mk_value(v);
return BR_DONE;
}
else if (bu.is_numeral(args[0], r1, bvs1) &&
bu.is_numeral(args[1], r2, bvs2) &&
bu.is_numeral(args[2], r3, bvs3)) {
else if (m_util.bu().is_numeral(args[0], r1, bvs1) &&
m_util.bu().is_numeral(args[1], r2, bvs2) &&
m_util.bu().is_numeral(args[2], r3, bvs3)) {
// 3 BV -> float
SASSERT(m_fm.mpz_manager().is_one(r2.to_mpq().denominator()));
SASSERT(m_fm.mpz_manager().is_one(r3.to_mpq().denominator()));
@ -290,7 +244,6 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg
SASSERT(f->get_num_parameters() == 2);
SASSERT(f->get_parameter(0).is_int());
SASSERT(f->get_parameter(1).is_int());
bv_util bu(m());
unsigned ebits = f->get_parameter(0).get_int();
unsigned sbits = f->get_parameter(1).get_int();
mpf_rounding_mode rmv;
@ -298,7 +251,7 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg
unsigned bvs;
if (m_util.is_rm_numeral(arg1, rmv) &&
bu.is_numeral(arg2, r, bvs)) {
m_util.bu().is_numeral(arg2, r, bvs)) {
scoped_mpf v(m_fm);
m_fm.set(v, ebits, sbits, rmv, r.to_mpq());
result = m_util.mk_value(v);
@ -331,6 +284,7 @@ br_status fpa_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref &
br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm_numeral(arg1, rm)) {
scoped_mpf v2(m_fm), v3(m_fm);
if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) {
@ -346,6 +300,7 @@ br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref &
br_status fpa_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm_numeral(arg1, rm)) {
scoped_mpf v2(m_fm), v3(m_fm);
if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) {
@ -355,7 +310,6 @@ br_status fpa_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref &
return BR_DONE;
}
}
return BR_FAILED;
}
@ -393,6 +347,7 @@ br_status fpa_rewriter::mk_neg(expr * arg1, expr_ref & result) {
br_status fpa_rewriter::mk_rem(expr * arg1, expr * arg2, expr_ref & result) {
scoped_mpf v1(m_fm), v2(m_fm);
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
scoped_mpf t(m_fm);
m_fm.rem(v1, v2, t);
@ -432,7 +387,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
scoped_mpf v1(m_fm), v2(m_fm);
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) {
result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2);
result = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2);
return BR_REWRITE1;
}
else {
@ -447,22 +402,24 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
c = m().mk_and(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
m().mk_or(m().mk_and(m_util.mk_is_positive(arg1), m_util.mk_is_negative(arg2)),
m().mk_and(m_util.mk_is_negative(arg1), m_util.mk_is_positive(arg2))));
v = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2);
v = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2);
result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_I, arg1, arg2));
result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_MIN_I, arg1, arg2));
return BR_REWRITE_FULL;
}
}
br_status fpa_rewriter::mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
scoped_mpf v1(m_fm), v2(m_fm);
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))
result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2);
result = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2);
else
result = m_util.mk_min(arg1, arg2);
return BR_DONE;
}
return BR_FAILED;
}
@ -479,7 +436,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
scoped_mpf v1(m_fm), v2(m_fm);
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) {
result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, arg1, arg2);
result = m().mk_app(get_fid(), OP_FPA_MAX_UNSPECIFIED, arg1, arg2);
return BR_REWRITE1;
}
else {
@ -494,27 +451,30 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
c = m().mk_and(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
m().mk_or(m().mk_and(m_util.mk_is_positive(arg1), m_util.mk_is_negative(arg2)),
m().mk_and(m_util.mk_is_negative(arg1), m_util.mk_is_positive(arg2))));
v = m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, arg1, arg2);
v = m().mk_app(get_fid(), OP_FPA_MAX_UNSPECIFIED, arg1, arg2);
result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_I, arg1, arg2));
result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_MAX_I, arg1, arg2));
return BR_REWRITE_FULL;
}
}
br_status fpa_rewriter::mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
scoped_mpf v1(m_fm), v2(m_fm);
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))
result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2);
result = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2);
else
result = m_util.mk_max(arg1, arg2);
return BR_DONE;
}
return BR_FAILED;
}
br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm_numeral(arg1, rm)) {
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)) {
@ -530,6 +490,7 @@ br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg
br_status fpa_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm_numeral(arg1, rm)) {
scoped_mpf v2(m_fm);
if (m_util.is_numeral(arg2, v2)) {
@ -545,6 +506,7 @@ br_status fpa_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
br_status fpa_rewriter::mk_round_to_integral(expr * arg1, expr * arg2, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm_numeral(arg1, rm)) {
scoped_mpf v2(m_fm);
if (m_util.is_numeral(arg2, v2)) {
@ -612,7 +574,6 @@ br_status fpa_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
return BR_DONE;
}
// TODO: more simplifications
return BR_FAILED;
}
@ -676,6 +637,7 @@ br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) {
br_status fpa_rewriter::mk_is_nan(expr * arg1, expr_ref & result) {
scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) {
result = (m_fm.is_nan(v)) ? m().mk_true() : m().mk_false();
return BR_DONE;
@ -686,6 +648,7 @@ br_status fpa_rewriter::mk_is_nan(expr * arg1, expr_ref & result) {
br_status fpa_rewriter::mk_is_inf(expr * arg1, expr_ref & result) {
scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) {
result = (m_fm.is_inf(v)) ? m().mk_true() : m().mk_false();
return BR_DONE;
@ -696,6 +659,7 @@ br_status fpa_rewriter::mk_is_inf(expr * arg1, expr_ref & result) {
br_status fpa_rewriter::mk_is_normal(expr * arg1, expr_ref & result) {
scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) {
result = (m_fm.is_normal(v)) ? m().mk_true() : m().mk_false();
return BR_DONE;
@ -706,6 +670,7 @@ br_status fpa_rewriter::mk_is_normal(expr * arg1, expr_ref & result) {
br_status fpa_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) {
scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) {
result = (m_fm.is_denormal(v)) ? m().mk_true() : m().mk_false();
return BR_DONE;
@ -716,6 +681,7 @@ br_status fpa_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) {
br_status fpa_rewriter::mk_is_negative(expr * arg1, expr_ref & result) {
scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) {
result = (m_fm.is_neg(v)) ? m().mk_true() : m().mk_false();
return BR_DONE;
@ -726,6 +692,7 @@ br_status fpa_rewriter::mk_is_negative(expr * arg1, expr_ref & result) {
br_status fpa_rewriter::mk_is_positive(expr * arg1, expr_ref & result) {
scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) {
result = (m_fm.is_neg(v) || m_fm.is_nan(v)) ? m().mk_false() : m().mk_true();
return BR_DONE;
@ -738,6 +705,7 @@ br_status fpa_rewriter::mk_is_positive(expr * arg1, expr_ref & result) {
// This the SMT =
br_status fpa_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
scoped_mpf v1(m_fm), v2(m_fm);
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
// Note: == is the floats-equality, here we need normal equality.
result = (m_fm.is_nan(v1) && m_fm.is_nan(v2)) ? m().mk_true() :
@ -751,10 +719,10 @@ br_status fpa_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result)
}
br_status fpa_rewriter::mk_bv2rm(expr * arg, expr_ref & result) {
bv_util bu(m());
rational bv_val;
unsigned sz = 0;
if (bu.is_numeral(arg, bv_val, sz)) {
if (m_util.bu().is_numeral(arg, bv_val, sz)) {
SASSERT(bv_val.is_uint64());
switch (bv_val.get_uint64()) {
case BV_RM_TIES_TO_AWAY: result = m_util.mk_round_nearest_ties_to_away(); break;
@ -773,13 +741,12 @@ br_status fpa_rewriter::mk_bv2rm(expr * arg, expr_ref & result) {
br_status fpa_rewriter::mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & result) {
unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
bv_util bu(m());
rational rsgn, rexp, rsig;
unsigned bvsz_sgn, bvsz_exp, bvsz_sig;
if (bu.is_numeral(sgn, rsgn, bvsz_sgn) &&
bu.is_numeral(sig, rsig, bvsz_sig) &&
bu.is_numeral(exp, rexp, bvsz_exp)) {
if (m_util.bu().is_numeral(sgn, rsgn, bvsz_sgn) &&
m_util.bu().is_numeral(sig, rsig, bvsz_sig) &&
m_util.bu().is_numeral(exp, rexp, bvsz_exp)) {
SASSERT(mpzm.is_one(rexp.to_mpq().denominator()));
SASSERT(mpzm.is_one(rsig.to_mpq().denominator()));
scoped_mpf v(m_fm);
@ -796,41 +763,7 @@ br_status fpa_rewriter::mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & res
return BR_FAILED;
}
br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_int());
int bv_sz = f->get_parameter(0).get_int();
mpf_rounding_mode rmv;
scoped_mpf v(m_fm);
if (m_util.is_rm_numeral(arg1, rmv) &&
m_util.is_numeral(arg2, v)) {
const mpf & x = v.get();
if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v))
return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
bv_util bu(m());
scoped_mpq q(m_fm.mpq_manager());
m_fm.to_sbv_mpq(rmv, v, q);
rational r(q);
rational ul, ll;
ul = m_fm.m_powers2.m1(bv_sz);
ll = rational(0);
if (r >= ll && r <= ul) {
result = bu.mk_numeral(r, bv_sz);
return BR_DONE;
}
else
return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
}
return BR_FAILED;
}
br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
br_status fpa_rewriter::mk_to_bv(func_decl * f, expr * arg1, expr * arg2, bool is_signed, expr_ref & result) {
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_int());
int bv_sz = f->get_parameter(0).get_int();
@ -842,7 +775,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
const mpf & x = v.get();
if (m_fm.is_nan(v) || m_fm.is_inf(v))
return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
return mk_to_bv_unspecified(f, result);
bv_util bu(m());
scoped_mpq q(m_fm.mpq_manager());
@ -850,19 +783,43 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
rational r(q);
rational ul, ll;
ul = m_fm.m_powers2.m1(bv_sz - 1);
ll = - m_fm.m_powers2(bv_sz - 1);
if (!is_signed) {
ul = m_fm.m_powers2.m1(bv_sz);
ll = rational(0);
}
else {
ul = m_fm.m_powers2.m1(bv_sz - 1);
ll = -m_fm.m_powers2(bv_sz - 1);
}
if (r >= ll && r <= ul) {
result = bu.mk_numeral(r, bv_sz);
return BR_DONE;
}
else
return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
return mk_to_bv_unspecified(f, result);
}
return BR_FAILED;
}
br_status fpa_rewriter::mk_to_bv_unspecified(func_decl * f, expr_ref & result) {
if (m_hi_fp_unspecified) {
unsigned bv_sz = m_util.bu().get_bv_size(f->get_range());
result = m_util.bu().mk_numeral(0, bv_sz);
return BR_DONE;
}
else
return BR_FAILED;
}
br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
return mk_to_bv(f, arg1, arg2, false, result);
}
br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
return mk_to_bv(f, arg1, arg2, true, result);
}
br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) {
TRACE("fp_rewriter", tout << "to_ieee_bv of " << mk_ismt2_pp(arg, m()) << std::endl;);
scoped_mpf v(m_fm);
@ -879,11 +836,8 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu
bu.mk_numeral(0, x.get_sbits() - 2),
bu.mk_numeral(1, 1) };
result = bu.mk_concat(4, args);
return BR_REWRITE1;
}
else
result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits());
return BR_REWRITE1;
}
else {
scoped_mpz rz(m_fm.mpq_manager());
@ -901,15 +855,17 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
if (m_util.is_numeral(arg, v)) {
if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
const mpf & x = v.get();
result = m_util.mk_internal_to_real_unspecified(x.get_ebits(), x.get_sbits());
if (m_hi_fp_unspecified) {
result = m_util.au().mk_numeral(rational(0), false);
return BR_DONE;
}
}
else {
scoped_mpq r(m_fm.mpq_manager());
m_fm.to_rational(v, r);
result = m_util.au().mk_numeral(r.get(), false);
return BR_DONE;
}
return BR_DONE;
}
return BR_FAILED;

13
src/ast/rewriter/fpa_rewriter.h
View file

@ -21,8 +21,9 @@ Notes:
#include "ast/ast.h"
#include "ast/rewriter/rewriter.h"
#include "util/params.h"
#include "ast/fpa_decl_plugin.h"
#include "ast/expr_map.h"
#include "util/params.h"
#include "util/mpf.h"
class fpa_rewriter {
@ -33,6 +34,9 @@ class fpa_rewriter {
app * mk_eq_nan(expr * arg);
app * mk_neq_nan(expr * arg);
br_status mk_to_bv(func_decl * f, expr * arg1, expr * arg2, bool is_signed, expr_ref & result);
br_status mk_to_bv_unspecified(func_decl * f, expr_ref & result);
public:
fpa_rewriter(ast_manager & m, params_ref const & p = params_ref());
~fpa_rewriter();
@ -73,14 +77,11 @@ public:
br_status mk_is_negative(expr * arg1, expr_ref & result);
br_status mk_is_positive(expr * arg1, expr_ref & result);
br_status mk_to_ieee_bv(expr * arg1, expr_ref & result);
br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
br_status mk_bv2rm(expr * arg, expr_ref & result);
br_status mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & result);
br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result);
@ -88,10 +89,6 @@ public:
br_status mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
br_status mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result);
br_status mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result);
br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result);
br_status mk_bvwrap(expr * arg, expr_ref & result);
};

14
src/cmd_context/cmd_context.cpp
View file

@ -1665,6 +1665,16 @@ void cmd_context::complete_model() {
}
}
for (unsigned i = 0; i < md->get_num_functions(); i++) {
func_decl * f = md->get_function(i);
func_interp * fi = md->get_func_interp(f);
IF_VERBOSE(12, verbose_stream() << "(model.completion " << f->get_name() << ")\n"; );
if (fi->is_partial()) {
sort * range = f->get_range();
fi->set_else(m().get_some_value(range));
}
}
for (auto kd : m_func_decls) {
symbol const & k = kd.m_key;
func_decls & v = kd.m_value;
@ -1948,13 +1958,13 @@ void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
TRACE("new_dt_eh", tout << "new datatype: "; m_owner.pm().display(tout, dt); tout << "\n";);
for (func_decl * c : *m_dt_util.get_datatype_constructors(dt)) {
TRACE("new_dt_eh", tout << "new constructor: " << c->get_name() << "\n";);
m_owner.insert(c);
m_owner.insert(c);
func_decl * r = m_dt_util.get_constructor_recognizer(c);
m_owner.insert(r);
TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";);
for (func_decl * a : *m_dt_util.get_constructor_accessors(c)) {
TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";);
m_owner.insert(a);
m_owner.insert(a);
}
}
if (m_owner.m_scopes.size() > 0) {

127
src/model/model_evaluator.cpp
View file

@ -33,9 +33,11 @@ Revision History:
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "model/model_smt2_pp.h"
#include "ast/rewriter/var_subst.h"
struct evaluator_cfg : public default_rewriter_cfg {
ast_manager & m;
model_core & m_model;
bool_rewriter m_b_rw;
arith_rewriter m_a_rw;
@ -53,6 +55,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
bool m_array_equalities;
evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p):
m(m),
m_model(md),
m_b_rw(m),
// We must allow customers to set parameters for arithmetic rewriter/evaluator.
@ -74,6 +77,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
m_ar_rw.set_expand_select_store(true);
m_ar_rw.set_expand_select_ite(true);
updt_params(p);
//add_unspecified_function_models(md);
}
void updt_params(params_ref const & _p) {
@ -85,10 +89,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
m_array_equalities = p.array_equalities();
}
ast_manager & m() const { return m_model.get_manager(); }
bool evaluate(func_decl* f, unsigned num, expr * const * args, expr_ref & result) {
func_interp* fi = m_model.get_func_interp(f);
bool evaluate(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
func_interp * fi = m_model.get_func_interp(f);
return (fi != 0) && eval_fi(fi, num, args, result);
}
@ -101,9 +103,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
bool actuals_are_values = true;
for (unsigned i = 0; actuals_are_values && i < num; i++) {
actuals_are_values = m().is_value(args[i]);
}
for (unsigned i = 0; actuals_are_values && i < num; i++)
actuals_are_values = m.is_value(args[i]);
if (!actuals_are_values)
return false; // let get_macro handle it
@ -120,7 +121,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
family_id fid = f->get_family_id();
bool is_uninterp = fid != null_family_id && m().get_plugin(fid)->is_considered_uninterpreted(f);
bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
if (num == 0 && (fid == null_family_id || is_uninterp)) {
expr * val = m_model.get_const_interp(f);
if (val != 0) {
@ -145,7 +146,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
if (k == OP_EQ) {
// theory dispatch for =
SASSERT(num == 2);
family_id s_fid = m().get_sort(args[0])->get_family_id();
family_id s_fid = m.get_sort(args[0])->get_family_id();
if (s_fid == m_a_rw.get_fid())
st = m_a_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_bv_rw.get_fid())
@ -178,16 +179,18 @@ struct evaluator_cfg : public default_rewriter_cfg {
st = m_f_rw.mk_app_core(f, num, args, result);
else if (fid == m_seq_rw.get_fid())
st = m_seq_rw.mk_app_core(f, num, args, result);
else if (fid == m().get_label_family_id() && num == 1) {
else if (fid == m.get_label_family_id() && num == 1) {
result = args[0];
st = BR_DONE;
}
else if (evaluate(f, num, args, result)) {
TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";);
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m) << "\n";
tout << "---->\n" << mk_ismt2_pp(result, m) << "\n";);
return BR_DONE;
}
if (st == BR_FAILED && !m.is_builtin_family_id(fid))
st = evaluate_partial_theory_func(f, num, args, result, result_pr);
if (st == BR_DONE && is_app(result)) {
app* a = to_app(result);
if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) {
@ -200,14 +203,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
void expand_value(expr_ref& val) {
vector<expr_ref_vector> stores;
expr_ref else_case(m());
expr_ref else_case(m);
bool _unused;
if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, _unused)) {
sort* srt = m().get_sort(val);
sort* srt = m.get_sort(val);
val = m_ar.mk_const_array(srt, else_case);
for (unsigned i = stores.size(); i > 0; ) {
--i;
expr_ref_vector args(m());
expr_ref_vector args(m);
args.push_back(val);
args.append(stores[i].size(), stores[i].c_ptr());
val = m_ar.mk_store(args.size(), args.c_ptr());
@ -220,6 +223,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
#define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
func_interp * fi = m_model.get_func_interp(f);
if (fi != 0) {
TRACE_MACRO;
if (fi->is_partial()) {
@ -228,31 +232,52 @@ struct evaluator_cfg : public default_rewriter_cfg {
expr * val = m_model.get_some_value(s);
fi->set_else(val);
}
else {
else
return false;
}
}
def = fi->get_interp();
def = fi->get_interp();
SASSERT(def != 0);
return true;
}
if (m_model_completion &&
(f->get_family_id() == null_family_id ||
m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f)))
m.get_plugin(f->get_family_id())->is_considered_uninterpreted(f)))
{
TRACE_MACRO;
sort * s = f->get_range();
expr * val = m_model.get_some_value(s);
func_interp * new_fi = alloc(func_interp, m(), f->get_arity());
func_interp * new_fi = alloc(func_interp, m, f->get_arity());
new_fi->set_else(val);
m_model.register_decl(f, new_fi);
def = val;
return true;
}
return false;
}
br_status evaluate_partial_theory_func(func_decl * f,
unsigned num, expr * const * args,
expr_ref & result, proof_ref & result_pr) {
SASSERT(f != 0);
SASSERT(!m.is_builtin_family_id(f->get_family_id()));
result = 0;
result_pr = 0;
func_interp * fi = m_model.get_func_interp(f);
if (fi) {
if (fi->is_partial())
fi->set_else(m.get_some_value(f->get_range()));
var_subst vs(m, false);
vs(fi->get_interp(), num, args, result);
return BR_REWRITE_FULL;
}
return BR_FAILED;
}
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("model evaluator");
@ -266,7 +291,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
if (a == b) {
result = m().mk_true();
result = m.mk_true();
return BR_DONE;
}
if (!m_array_equalities) {
@ -275,19 +300,19 @@ struct evaluator_cfg : public default_rewriter_cfg {
vector<expr_ref_vector> stores1, stores2;
bool args_are_unique1, args_are_unique2;
expr_ref else1(m()), else2(m());
expr_ref else1(m), else2(m);
if (extract_array_func_interp(a, stores1, else1, args_are_unique1) &&
extract_array_func_interp(b, stores2, else2, args_are_unique2)) {
expr_ref_vector conj(m()), args1(m()), args2(m());
if (m().are_equal(else1, else2)) {
expr_ref_vector conj(m), args1(m), args2(m);
if (m.are_equal(else1, else2)) {
// no op
}
else if (m().are_distinct(else1, else2) && !(m().get_sort(else1)->get_info()->get_num_elements().is_finite())) {
result = m().mk_false();
else if (m.are_distinct(else1, else2) && !(m.get_sort(else1)->get_info()->get_num_elements().is_finite())) {
result = m.mk_false();
return BR_DONE;
}
else {
conj.push_back(m().mk_eq(else1, else2));
conj.push_back(m.mk_eq(else1, else2));
}
if (args_are_unique1 && args_are_unique2 && !stores1.empty()) {
return mk_array_eq_core(stores1, else1, stores2, else2, conj, result);
@ -300,11 +325,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
for (unsigned i = 0; i < stores1.size(); ++i) {
args1.resize(1); args1.append(stores1[i].size() - 1, stores1[i].c_ptr());
args2.resize(1); args2.append(stores1[i].size() - 1, stores1[i].c_ptr());
expr_ref s1(m_ar.mk_select(args1.size(), args1.c_ptr()), m());
expr_ref s2(m_ar.mk_select(args2.size(), args2.c_ptr()), m());
conj.push_back(m().mk_eq(s1, s2));
expr_ref s1(m_ar.mk_select(args1.size(), args1.c_ptr()), m);
expr_ref s2(m_ar.mk_select(args2.size(), args2.c_ptr()), m);
conj.push_back(m.mk_eq(s1, s2));
}
result = m().mk_and(conj.size(), conj.c_ptr());
result = m.mk_and(conj.size(), conj.c_ptr());
return BR_REWRITE_FULL;
}
return BR_FAILED;
@ -362,15 +387,15 @@ struct evaluator_cfg : public default_rewriter_cfg {
if (table1.find(stores2[i].c_ptr(), args)) {
switch (compare(args[arity], val)) {
case l_true: table1.remove(args); break;
case l_false: result = m().mk_false(); return BR_DONE;
default: conj.push_back(m().mk_eq(val, args[arity])); break;
case l_false: result = m.mk_false(); return BR_DONE;
default: conj.push_back(m.mk_eq(val, args[arity])); break;
}
}
else {
switch (compare(else1, val)) {
case l_true: break;
case l_false: result = m().mk_false(); return BR_DONE;
default: conj.push_back(m().mk_eq(else1, val)); break;
case l_false: result = m.mk_false(); return BR_DONE;
default: conj.push_back(m.mk_eq(else1, val)); break;
}
}
}
@ -378,8 +403,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
for (; it != end; ++it) {
switch (compare((*it)[arity], else2)) {
case l_true: break;
case l_false: result = m().mk_false(); return BR_DONE;
default: conj.push_back(m().mk_eq((*it)[arity], else2)); break;
case l_false: result = m.mk_false(); return BR_DONE;
default: conj.push_back(m.mk_eq((*it)[arity], else2)); break;
}
}
result = mk_and(conj);
@ -387,8 +412,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
lbool compare(expr* a, expr* b) {
if (m().are_equal(a, b)) return l_true;
if (m().are_distinct(a, b)) return l_false;
if (m.are_equal(a, b)) return l_true;
if (m.are_distinct(a, b)) return l_false;
return l_undef;
}
@ -396,8 +421,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
bool args_are_values(expr_ref_vector const& store, bool& are_unique) {
bool are_values = true;
for (unsigned j = 0; are_values && j + 1 < store.size(); ++j) {
are_values = m().is_value(store[j]);
are_unique &= m().is_unique_value(store[j]);
are_values = m.is_value(store[j]);
are_unique &= m.is_unique_value(store[j]);
}
SASSERT(!are_unique || are_values);
return are_values;
@ -408,10 +433,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
SASSERT(m_ar.is_array(a));
bool are_values = true;
are_unique = true;
TRACE("model_evaluator", tout << mk_pp(a, m()) << "\n";);
TRACE("model_evaluator", tout << mk_pp(a, m) << "\n";);
while (m_ar.is_store(a)) {
expr_ref_vector store(m());
expr_ref_vector store(m);
store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
are_values &= args_are_values(store, are_unique);
stores.push_back(store);
@ -424,7 +449,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
if (!m_ar.is_as_array(a)) {
TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);
TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m) << "\n";);
return false;
}
@ -434,13 +459,13 @@ struct evaluator_cfg : public default_rewriter_cfg {
unsigned arity = f->get_arity();
unsigned base_sz = stores.size();
for (unsigned i = 0; i < sz; ++i) {
expr_ref_vector store(m());
expr_ref_vector store(m);
func_entry const* fe = g->get_entry(i);
store.append(arity, fe->get_args());
store.push_back(fe->get_result());
for (unsigned j = 0; j < store.size(); ++j) {
if (!is_ground(store[j].get())) {
TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m()) << "\n" << mk_pp(store[j].get(), m()) << "\n";);
TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";);
return false;
}
}
@ -448,18 +473,18 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
else_case = g->get_else();
if (!else_case) {
TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n";
/*model_smt2_pp(tout, m(), m_model, 0);*/
TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n";
/*model_smt2_pp(tout, m, m_model, 0);*/
);
return false;
}
if (!is_ground(else_case)) {
TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << else_case << "\n";);
TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m) << "\n" << else_case << "\n";);
return false;
}
for (unsigned i = stores.size(); are_values && i > base_sz; ) {
--i;
if (m().are_equal(else_case, stores[i].back())) {
if (m.are_equal(else_case, stores[i].back())) {
for (unsigned j = i + 1; j < stores.size(); ++j) {
stores[j-1].reset();
stores[j-1].append(stores[j]);
@ -469,7 +494,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
are_values &= args_are_values(stores[i], are_unique);
}
TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m()) << "\n";);
TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m) << "\n";);
return true;
}

15
src/smt/theory_fpa.cpp
View file

@ -119,6 +119,7 @@ namespace smt {
SASSERT(m_conversions.empty());
SASSERT(m_is_added_to_model.empty());
}
void theory_fpa::init(context * ctx) {
smt::theory::init(ctx);
m_is_initialized = true;
@ -237,7 +238,7 @@ namespace smt {
if (m_fpa_util.is_fp(e)) {
expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };
expr_ref tmp(m_bv_util.mk_concat(3, cargs), m);
expr_ref tmp(m_bv_util.mk_concat(3, cargs), m);
m_th_rw(tmp);
res = to_app(tmp);
}
@ -255,7 +256,7 @@ namespace smt {
}
func_decl_ref wrap_fd(m);
wrap_fd = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &es, bv_srt);
wrap_fd = m.mk_func_decl(get_family_id(), OP_FPA_BVWRAP, 0, 0, 1, &es, bv_srt);
res = m.mk_app(wrap_fd, e);
}
@ -890,14 +891,10 @@ namespace smt {
if (f->get_family_id() == get_family_id()) {
bool include =
m_fpa_util.is_min_unspecified(f) ||
m_fpa_util.is_max_unspecified(f) ||
m_fpa_util.is_to_ubv_unspecified(f) ||
m_fpa_util.is_to_sbv_unspecified(f) ||
m_fpa_util.is_to_ieee_bv_unspecified(f) ||
m_fpa_util.is_to_real_unspecified(f);
m_fpa_util.is_max_unspecified(f) ;
if (include && !m_is_added_to_model.contains(f)) {
m_is_added_to_model.insert(f);
get_manager().inc_ref(f);
//m_is_added_to_model.insert(f);
//get_manager().inc_ref(f);
return true;
}
return false;

5
src/smt/theory_fpa.h
View file

@ -82,7 +82,7 @@ namespace smt {
m_th(*th) {}
virtual ~fpa2bv_converter_wrapped() {}
virtual void mk_const(func_decl * f, expr_ref & result);
virtual void mk_rm_const(func_decl * f, expr_ref & result);
virtual void mk_rm_const(func_decl * f, expr_ref & result);
};
class fpa_value_proc : public model_value_proc {
@ -108,7 +108,7 @@ namespace smt {
result.append(m_deps);
}
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
};
class fpa_rm_value_proc : public model_value_proc {
@ -179,7 +179,6 @@ namespace smt {
expr_ref convert_atom(expr * e);
expr_ref convert_term(expr * e);
expr_ref convert_conversion_term(expr * e);
expr_ref convert_unwrap(expr * e);
void add_trail(ast * a);

23
src/tactic/fpa/fpa2bv_model_converter.cpp
View file

@ -33,12 +33,29 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator
}
void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl;
for (unsigned i = 0; i < mc->get_num_constants(); i++)
tout << mc->get_constant(i)->get_name() << " --> " <<
mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl;
for (unsigned i = 0; i < mc->get_num_functions(); i++) {
func_decl * f = mc->get_function(i);
tout << f->get_name() << "(...) := " << std::endl;
func_interp * fi = mc->get_func_interp(f);
for (unsigned j = 0; j < fi->num_entries(); j++) {
func_entry const * fe = fi->get_entry(j);
for (unsigned k = 0; k < f->get_arity(); k++)
tout << mk_ismt2_pp(fe->get_arg(k), m) << " ";
tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl;
}
tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
});
obj_hashtable<func_decl> seen;
m_bv2fp->convert_consts(mc, float_mdl, seen);
m_bv2fp->convert_rm_consts(mc, float_mdl, seen);
m_bv2fp->convert_min_max_specials(mc, float_mdl, seen);
m_bv2fp->convert_uf2bvuf(mc, float_mdl, seen);
// Keep all the non-float constants.
unsigned sz = mc->get_num_constants();
for (unsigned i = 0; i < sz; i++) {
@ -46,7 +63,7 @@ void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
if (!seen.contains(c))
float_mdl->register_decl(c, mc->get_const_interp(c));
}
// And keep everything else
sz = mc->get_num_functions();
for (unsigned i = 0; i < sz; i++) {
@ -57,7 +74,7 @@ void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
float_mdl->register_decl(f, val);
}
}
sz = mc->get_num_uninterpreted_sorts();
for (unsigned i = 0; i < sz; i++) {
sort * s = mc->get_uninterpreted_sort(i);

6
src/tactic/fpa/fpa2bv_model_converter.h
View file

@ -26,7 +26,7 @@ Notes:
class fpa2bv_model_converter : public model_converter {
ast_manager & m;
bv2fpa_converter * m_bv2fp;
public:
fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv):
m(m),
@ -53,10 +53,10 @@ public:
virtual model_converter * translate(ast_translation & translator);
protected:
fpa2bv_model_converter(ast_manager & m) :
fpa2bv_model_converter(ast_manager & m) :
m(m),
m_bv2fp(0) {}
void convert(model_core * mc, model * float_mdl);
};

8
src/util/mpf.cpp
View file

@ -1217,12 +1217,18 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
default: UNREACHABLE();
}
if (inc) m_mpz_manager.inc(z);
TRACE("mpf_dbg_sbv",
tout << "SBV: (" << to_string(x) << ") == " << m_mpq_manager.to_string(z) << std::endl;
tout << "sign=" << t.sign() << " last=" << last << " round=" << round <<
" sticky=" << sticky << " inc=" << inc << std::endl; );
}
else
m_mpz_manager.mul2k(z, (unsigned) e);
m_mpq_manager.set(o, z);
if (x.sign) m_mpq_manager.neg(o);
TRACE("mpf_dbg", tout << "SBV = " << m_mpq_manager.to_string(o) << std::endl;);
}
void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) {
@ -1248,6 +1254,8 @@ void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) {
m_mpz_manager.mul2k(o, sbits - 1);
m_mpz_manager.add(o, sig(x), o);
}
TRACE("mpf_dbg", tout << "IEEE_BV = " << m_mpz_manager.to_string(o) << std::endl;);
}
void mpf_manager::renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, mpz & sig) {