michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/num): bug in to_pos_num, missing test

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-26 08:18:07 -07:00
parent 99438f0ee0
commit 02b7f980b0
1 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/num.cpp
View file

@ -54,12 +54,14 @@ expr from_num(mpz const & n) {
optional<mpz> to_pos_num(expr const & e) {
if (e == g_one) {
return some(mpz(1));
} else if (app_fn(e) == g_bit0) {
if (auto r = to_pos_num(app_arg(e)))
return some(2*(*r));
} else if (app_fn(e) == g_bit1) {
if (auto r = to_pos_num(app_arg(e)))
return some(2*(*r) + 1);
} else if (is_app(e)) {
if (app_fn(e) == g_bit0) {
if (auto r = to_pos_num(app_arg(e)))
return some(2*(*r));
} else if (app_fn(e) == g_bit1) {
if (auto r = to_pos_num(app_arg(e)))
return some(2*(*r) + 1);
}
}
return optional<mpz>();
}