mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-12 18:36:44 +01:00
parent d8ea3023fc
commit bc257211d6
6 changed files with 37 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -165,7 +165,6 @@ void fpa2bv_converter::mk_numeral(sort * s, mpf const & v, expr_ref & result) {
result = m_util.mk_fp(bv_sgn, biased_exp, bv_sig);
TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is "
<< mk_ismt2_pp(result, m) << std::endl;);
}
}

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

@ -71,9 +71,9 @@ public:
bool is_rm(expr * e) { return is_app(e) && m_util.is_rm(e); }
bool is_rm(sort * s) { return m_util.is_rm(s); }
bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); }
void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
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;

10
src/ast/fpa_decl_plugin.h
View file

@ -259,7 +259,7 @@ public:
bool is_rm(sort * s) const { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }
bool is_float(expr * e) const { return is_float(m_manager.get_sort(e)); }
bool is_rm(expr * e) const { return is_rm(m_manager.get_sort(e)); }
bool is_fp(expr * e) const { return is_app_of(e, m_fid, OP_FPA_FP); }
bool is_fp(expr * e) const { return is_app_of(e, m_fid, OP_FPA_FP); }
unsigned get_ebits(sort * s) const;
unsigned get_sbits(sort * s) const;
@ -294,13 +294,13 @@ public:
bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); }
bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); }
app * mk_fp(expr * sgn, expr * exp, expr * sig) {
app * mk_fp(expr * sgn, expr * exp, expr * sig) {
SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);
SASSERT(m_bv_util.is_bv(exp));
SASSERT(m_bv_util.is_bv(sig));
return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig);
SASSERT(m_bv_util.is_bv(sig));
return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig);
}
app * mk_to_fp(sort * s, expr * bv_t) {
SASSERT(is_float(s) && s->get_num_parameters() == 2);
return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 1, &bv_t);

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

@ -98,7 +98,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
case OP_FPA_INTERNAL_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;

40
src/smt/theory_fpa.cpp
View file

@ -116,15 +116,15 @@ namespace smt {
SASSERT(m_trail_stack.get_num_scopes() == 0);
SASSERT(m_conversions.empty());
SASSERT(m_is_added_to_model.empty());
}
SASSERT(m_is_added_to_model.empty());
}
void theory_fpa::init(context * ctx) {
smt::theory::init(ctx);
m_is_initialized = true;
}
app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
TRACE("t_fpa_detail",
TRACE("t_fpa_detail",
ast_manager & m = m_th.get_manager();
for (unsigned i = 0; i < values.size(); i++)
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
@ -201,7 +201,7 @@ namespace smt {
app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
SASSERT(values.size() == 1);
TRACE("t_fpa_detail",
TRACE("t_fpa_detail",
ast_manager & m = m_th.get_manager();
for (unsigned i = 0; i < values.size(); i++)
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
@ -235,12 +235,12 @@ namespace smt {
app_ref res(m);
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 * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };
res = m_bv_util.mk_concat(3, cargs);
m_th_rw((expr_ref&)res);
}
else {
sort * es = m.get_sort(e);
sort * es = m.get_sort(e);
sort_ref bv_srt(m);
if (m_converter.is_rm(es))
@ -264,7 +264,7 @@ namespace smt {
SASSERT(!m_fpa_util.is_fp(e));
SASSERT(m_bv_util.is_bv(e));
SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s));
ast_manager & m = get_manager();
ast_manager & m = get_manager();
app_ref res(m);
unsigned bv_sz = m_bv_util.get_bv_size(e);
@ -285,7 +285,7 @@ namespace smt {
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, e),
m_bv_util.mk_extract(sbits - 2, 0, e));
}
return res;
}
@ -312,7 +312,7 @@ namespace smt {
TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << std::endl;
tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << std::endl;);
if (m_fpa_util.is_rm(e)) {
if (m_fpa_util.is_rm(e)) {
SASSERT(m_fpa_util.is_bv2rm(e_conv));
expr_ref bv_rm(m);
m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
@ -329,7 +329,7 @@ namespace smt {
}
else
UNREACHABLE();
return res;
}
@ -362,7 +362,7 @@ namespace smt {
res = convert_atom(e);
else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e))
res = convert_term(e);
else
else
res = convert_conversion_term(e);
TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl;
@ -448,7 +448,7 @@ namespace smt {
TRACE("t_fpa_internalize", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
SASSERT(term->get_family_id() == get_family_id());
SASSERT(!get_context().e_internalized(term));
ast_manager & m = get_manager();
context & ctx = get_context();
@ -494,7 +494,7 @@ namespace smt {
SASSERT(n->get_owner()->get_decl()->get_range() == s);
ast_manager & m = get_manager();
context & ctx = get_context();
context & ctx = get_context();
app_ref owner(n->get_owner(), m);
if (!is_attached_to_var(n)) {
@ -510,7 +510,7 @@ namespace smt {
assert_cnstr(valid);
}
}
if (!ctx.relevancy())
relevant_eh(owner);
}
@ -600,7 +600,7 @@ namespace smt {
xe_eq_ye = m.mk_eq(xe, ye);
not_xe_eq_ye = m.mk_not(xe_eq_ye);
c_eq_iff = m.mk_iff(not_xe_eq_ye, c);
assert_cnstr(c_eq_iff);
assert_cnstr(c_eq_iff);
assert_cnstr(mk_side_conditions());
return;
@ -689,10 +689,10 @@ namespace smt {
pop_scope_eh(m_trail_stack.get_num_scopes());
m_converter.reset();
m_rw.reset();
m_th_rw.reset();
m_trail_stack.pop_scope(m_trail_stack.get_num_scopes());
m_th_rw.reset();
m_trail_stack.pop_scope(m_trail_stack.get_num_scopes());
if (m_factory) {
dealloc(m_factory);
dealloc(m_factory);
m_factory = 0;
}
ast_manager & m = get_manager();
@ -862,8 +862,8 @@ namespace smt {
}
bool theory_fpa::include_func_interp(func_decl * f) {
TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);
TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);
if (f->get_family_id() == get_family_id()) {
bool include =
m_fpa_util.is_min_unspecified(f) ||

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

@ -234,7 +234,7 @@ fpa2bv_model_converter::array_model fpa2bv_model_converter::convert_array_func_i
array_util arr_util(m);
array_model am(m);
sort_ref_vector array_domain(m);
sort_ref_vector array_domain(m);
unsigned arity = f->get_range()->get_num_parameters()-1;
expr_ref as_arr_mdl(m);
@ -245,21 +245,21 @@ fpa2bv_model_converter::array_model fpa2bv_model_converter::convert_array_func_i
for (unsigned i = 0; i < arity; i++)
array_domain.push_back(to_sort(f->get_range()->get_parameter(i).get_ast()));
sort * rng = to_sort(f->get_range()->get_parameter(arity).get_ast());
bv_f = arr_util.get_as_array_func_decl(to_app(as_arr_mdl));
am.new_float_fd = m.mk_fresh_func_decl(arity, array_domain.c_ptr(), rng);
am.new_float_fi = convert_func_interp(am.new_float_fd, bv_f, bv_mdl);
am.new_float_fi = convert_func_interp(am.new_float_fd, bv_f, bv_mdl);
am.bv_fd = bv_f;
am.result = arr_util.mk_as_array(f->get_range(), am.new_float_fd);
return am;
}
func_interp * fpa2bv_model_converter::convert_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl) {
func_interp * fpa2bv_model_converter::convert_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl) {
SASSERT(f->get_arity() > 0);
func_interp * result = 0;
sort * rng = f->get_range();
sort * const * dmn = f->get_domain();
sort * const * dmn = f->get_domain();
unsigned arity = bv_f->get_arity();
func_interp * bv_fi = bv_mdl->get_func_interp(bv_f);
@ -276,7 +276,7 @@ func_interp * fpa2bv_model_converter::convert_func_interp(func_decl * f, func_de
for (unsigned j = 0; j < arity; j++) {
sort * ft_dj = dmn[j];
expr * bv_aj = bv_args[j];
expr * bv_aj = bv_args[j];
ai = rebuild_floats(bv_mdl, ft_dj, bv_aj);
m_th_rw(ai);
new_args.push_back(ai);
@ -293,7 +293,7 @@ func_interp * fpa2bv_model_converter::convert_func_interp(func_decl * f, func_de
bv_els = bv_fi->get_else();
ft_els = rebuild_floats(bv_mdl, rng, bv_els);
m_th_rw(ft_els);
result->set_else(ft_els);
result->set_else(ft_els);
}
return result;
@ -409,7 +409,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
it++) {
seen.insert(it->m_value);
func_decl * f = it->m_key;
func_decl * f = it->m_key;
if (f->get_arity() == 0)
{
array_util au(m);
@ -426,7 +426,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
bv_mdl->eval(it->m_value, val);
if (val) float_mdl->register_decl(f, val);
}
}
}
else {
func_interp * fmv = convert_func_interp(f, it->m_value, bv_mdl);
if (fmv) float_mdl->register_decl(f, fmv);