max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/smt2/elaborator): (/ <int> <int>) needs to coerce both arguments

Browse source
This commit is contained in:
Daniel Selsam 2016-07-25 10:22:02 -07:00 • committed by Leonardo de Moura
parent f336e817b3
commit 8b9f3f1e47
1 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/frontends/smt2/elaborator.cpp
View file

@ -44,13 +44,15 @@ struct arith_app_info {
name const & get_op_name() const { return m_op; }
bool has_int_inst_name() const { return !m_int_inst.is_anonymous(); }
name const & get_int_inst_name() const {
lean_assert(!m_int_inst.is_anonymous());
lean_assert(has_int_inst_name());
return m_int_inst;
}
bool has_real_inst_name() const { return !m_real_inst.is_anonymous(); }
name const & get_real_inst_name() const {
lean_assert(!m_real_inst.is_anonymous());
lean_assert(has_real_inst_name());
return m_real_inst;
}
@ -226,7 +228,8 @@ private:
}
}
// The arith-normalizer will push the coercions inside.
if (found_int && found_real) {
bool coerce_all_ints = is_constant(args[0]) && const_name(args[0]) == "/";
if (found_int && (found_real || coerce_all_ints)) {
for (unsigned i = 0; i < is_real.size(); ++i) {
if (is_int[i]) {
args[i+1] = mk_app(mk_constant(get_real_of_int_name()), args[i+1]);
@ -319,7 +322,7 @@ void initialize_elaborator() {
{"div", arith_app_info(get_div_name(), get_int_has_div_name(), name(), fun_attr::LEFT_ASSOC)},
// Real-specific
{"/", arith_app_info(get_div_name(), get_int_has_div_name(), get_real_has_div_name(), fun_attr::LEFT_ASSOC)},
{"/", arith_app_info(get_div_name(), name(), get_real_has_div_name(), fun_attr::LEFT_ASSOC)},
// Overloaded operators
{"+", arith_app_info(get_add_name(), get_int_has_add_name(), get_real_has_add_name(), fun_attr::LEFT_ASSOC)},