From 4b6583ae9f6e15f47fb324d7ceffd6fc9ef80e87 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Apr 2018 11:30:04 -0700 Subject: [PATCH] refactor(util): move mpz/mpq to util The new lean_obj objects will be defined at util. Reason: we will define `name`, `options`, `format`, ... on top of lean_obj. lean_obj depends on mpz. Remark: lean_obj will replace vm_obj. --- src/CMakeLists.txt | 3 - src/checker/CMakeLists.txt | 2 +- src/frontends/lean/parser_config.h | 2 +- src/frontends/lean/pp.h | 2 +- src/frontends/lean/prenum.cpp | 2 +- src/frontends/lean/prenum.h | 2 +- src/frontends/lean/scanner.h | 2 +- src/init/init.cpp | 3 - src/library/compiler/nat_value.cpp | 2 +- src/library/compiler/nat_value.h | 2 +- src/library/num.h | 2 +- src/library/vm/vm.h | 2 +- src/tests/util/CMakeLists.txt | 6 +- src/tests/util/format.cpp | 2 +- src/tests/util/numerics/CMakeLists.txt | 6 - src/tests/util/numerics/mpq.cpp | 211 ------------------------- src/tests/util/numerics/mpz.cpp | 84 ---------- src/tests/util/sexpr.cpp | 2 +- src/util/CMakeLists.txt | 2 +- src/util/{numerics => }/mpq.cpp | 2 +- src/util/{numerics => }/mpq.h | 2 +- src/util/{numerics => }/mpz.cpp | 2 +- src/util/{numerics => }/mpz.h | 0 src/util/numerics/CMakeLists.txt | 1 - src/util/numerics/init_module.cpp | 17 -- src/util/numerics/init_module.h | 11 -- src/util/numerics/power.h | 26 --- src/util/numerics/remainder.h | 20 --- 28 files changed, 19 insertions(+), 401 deletions(-) delete mode 100644 src/tests/util/numerics/CMakeLists.txt delete mode 100644 src/tests/util/numerics/mpq.cpp delete mode 100644 src/tests/util/numerics/mpz.cpp rename src/util/{numerics => }/mpq.cpp (98%) rename src/util/{numerics => }/mpq.h (99%) rename src/util/{numerics => }/mpz.cpp (98%) rename src/util/{numerics => }/mpz.h (100%) delete mode 100644 src/util/numerics/CMakeLists.txt delete mode 100644 src/util/numerics/init_module.cpp delete mode 100644 src/util/numerics/init_module.h delete mode 100644 src/util/numerics/power.h delete mode 100644 src/util/numerics/remainder.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1279eff477..c9ace0de9d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -391,8 +391,6 @@ configure_file("${LEAN_SOURCE_DIR}/../library/init/version.lean.in" "${LEAN_SOUR include_directories("${LEAN_BINARY_DIR}") add_subdirectory(util) set(LEAN_OBJS ${LEAN_OBJS} $) -add_subdirectory(util/numerics) -set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(util/sexpr) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(kernel) @@ -451,7 +449,6 @@ function(add_exec_test name tgt) endfunction() add_subdirectory(tests/util) -add_subdirectory(tests/util/numerics) add_subdirectory(tests/kernel) add_subdirectory(tests/library) add_subdirectory(tests/frontends/lean) diff --git a/src/checker/CMakeLists.txt b/src/checker/CMakeLists.txt index 07eabbe296..4d7388fe6c 100644 --- a/src/checker/CMakeLists.txt +++ b/src/checker/CMakeLists.txt @@ -1,5 +1,5 @@ add_executable(leanchecker checker.cpp text_import.cpp simple_pp.cpp $ $ $ $ $) -target_link_libraries(leanchecker ${EXTRA_UTIL_LIBS}) +target_link_libraries(leanchecker ${EXTRA_LIBS}) install(TARGETS leanchecker DESTINATION bin) diff --git a/src/frontends/lean/parser_config.h b/src/frontends/lean/parser_config.h index 44136b0c1a..f7b9b25a4a 100644 --- a/src/frontends/lean/parser_config.h +++ b/src/frontends/lean/parser_config.h @@ -12,7 +12,7 @@ Author: Leonardo de Moura #include "frontends/lean/token_table.h" #include "frontends/lean/parse_table.h" #include "frontends/lean/cmd_table.h" -#include "util/numerics/mpz.h" +#include "util/mpz.h" namespace lean { struct token_entry { diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index cbc24fc279..26f3ee84b4 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -11,12 +11,12 @@ Author: Leonardo de Moura #include "util/pair.h" #include "util/name_map.h" #include "util/name_set.h" +#include "util/mpz.h" #include "util/sexpr/options.h" #include "util/sexpr/format.h" #include "kernel/environment.h" #include "kernel/abstract_type_context.h" #include "frontends/lean/token_table.h" -#include "util/numerics/mpz.h" namespace lean { class notation_entry; diff --git a/src/frontends/lean/prenum.cpp b/src/frontends/lean/prenum.cpp index f062acaace..49fcc36239 100644 --- a/src/frontends/lean/prenum.cpp +++ b/src/frontends/lean/prenum.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include #include "library/kernel_serializer.h" -#include "util/numerics/mpz.h" +#include "util/mpz.h" namespace lean { static name * g_prenum_name = nullptr; diff --git a/src/frontends/lean/prenum.h b/src/frontends/lean/prenum.h index 47c2474247..5bc0737692 100644 --- a/src/frontends/lean/prenum.h +++ b/src/frontends/lean/prenum.h @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include "kernel/expr.h" -#include "util/numerics/mpz.h" +#include "util/mpz.h" namespace lean { /** \brief Create a pre-numeral. We create pre-numerals at parsing time. The elaborator is responsible for diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h index ad2041bc98..1c03023cfd 100644 --- a/src/frontends/lean/scanner.h +++ b/src/frontends/lean/scanner.h @@ -11,7 +11,7 @@ Author: Leonardo de Moura #include "util/name.h" #include "util/flet.h" #include "util/utf8.h" -#include "util/numerics/mpq.h" +#include "util/mpq.h" #include "kernel/environment.h" #include "library/io_state.h" #include "frontends/lean/token_table.h" diff --git a/src/init/init.cpp b/src/init/init.cpp index 7343be7091..e32456daaf 100644 --- a/src/init/init.cpp +++ b/src/init/init.cpp @@ -7,7 +7,6 @@ Author: Leonardo de Moura #include "util/stackinfo.h" #include "util/thread.h" #include "util/init_module.h" -#include "util/numerics/init_module.h" #include "util/sexpr/init_module.h" #include "kernel/init_module.h" #include "kernel/inductive/inductive.h" @@ -27,7 +26,6 @@ namespace lean { void initialize() { save_stack_info(); initialize_util_module(); - initialize_numerics_module(); initialize_sexpr_module(); initialize_kernel_module(); initialize_inductive_module(); @@ -67,7 +65,6 @@ void finalize() { finalize_inductive_module(); finalize_kernel_module(); finalize_sexpr_module(); - finalize_numerics_module(); finalize_util_module(); run_post_thread_finalizers(); #ifdef LEAN_TRACK_CUSTOM_ALLOCATORS diff --git a/src/library/compiler/nat_value.cpp b/src/library/compiler/nat_value.cpp index 17d3e7cb2f..3a675e65fb 100644 --- a/src/library/compiler/nat_value.cpp +++ b/src/library/compiler/nat_value.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "util/numerics/mpz.h" +#include "util/mpz.h" #include "kernel/expr.h" #include "library/constants.h" #include "library/num.h" diff --git a/src/library/compiler/nat_value.h b/src/library/compiler/nat_value.h index 1f7df82613..1cd642abbd 100644 --- a/src/library/compiler/nat_value.h +++ b/src/library/compiler/nat_value.h @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include "library/type_context.h" -#include "util/numerics/mpz.h" +#include "util/mpz.h" namespace lean { /** \brief Replace nat numerals encoded using bit0, bit1, one with an auxiliary nat_value macro. diff --git a/src/library/num.h b/src/library/num.h index a61ab63186..58521526b0 100644 --- a/src/library/num.h +++ b/src/library/num.h @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "util/numerics/mpz.h" +#include "util/mpz.h" #include "kernel/environment.h" namespace lean { diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 50f6e7b78c..a708d5744f 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -15,7 +15,7 @@ Author: Leonardo de Moura #include "util/rc.h" #include "util/interrupt.h" #include "util/serializer.h" -#include "util/numerics/mpz.h" +#include "util/mpz.h" #include "kernel/environment.h" #include "kernel/pos_info_provider.h" diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index 299706af77..bbd22e20ef 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -1,10 +1,10 @@ add_executable(name name.cpp $) target_link_libraries(name ${EXTRA_LIBS}) add_exec_test(name "name") -add_executable(sexpr_tst sexpr.cpp $ $ $) +add_executable(sexpr_tst sexpr.cpp $ $) target_link_libraries(sexpr_tst ${EXTRA_LIBS}) add_exec_test(sexpr "sexpr_tst") -add_executable(format format.cpp $ $ $) +add_executable(format format.cpp $ $) target_link_libraries(format ${EXTRA_LIBS}) add_exec_test(format "format") add_executable(buffer buffer.cpp $) @@ -13,7 +13,7 @@ add_exec_test(buffer "buffer") add_executable(list list.cpp $) target_link_libraries(list ${EXTRA_LIBS}) add_exec_test(list "list") -add_executable(options options.cpp $ $ $) +add_executable(options options.cpp $ $) target_link_libraries(options ${EXTRA_LIBS}) add_exec_test(options "options") add_executable(rb_tree rb_tree.cpp $) diff --git a/src/tests/util/format.cpp b/src/tests/util/format.cpp index 1ec64f1b0d..7ee15f2e1c 100644 --- a/src/tests/util/format.cpp +++ b/src/tests/util/format.cpp @@ -11,7 +11,7 @@ Author: Soonho Kong #include #include "util/test.h" #include "util/init_module.h" -#include "util/numerics/mpq.h" +#include "util/mpq.h" #include "util/sexpr/format.h" #include "util/sexpr/sexpr_fn.h" #include "util/sexpr/options.h" diff --git a/src/tests/util/numerics/CMakeLists.txt b/src/tests/util/numerics/CMakeLists.txt deleted file mode 100644 index 710c918e1d..0000000000 --- a/src/tests/util/numerics/CMakeLists.txt +++ /dev/null @@ -1,6 +0,0 @@ -add_executable(mpq mpq.cpp $ $ $) -target_link_libraries(mpq ${EXTRA_LIBS}) -add_exec_test(mpq "mpq") -add_executable(mpz mpz.cpp $ $ $) -target_link_libraries(mpz ${EXTRA_LIBS}) -add_exec_test(mpz "mpz") diff --git a/src/tests/util/numerics/mpq.cpp b/src/tests/util/numerics/mpq.cpp deleted file mode 100644 index df2ac0b78d..0000000000 --- a/src/tests/util/numerics/mpq.cpp +++ /dev/null @@ -1,211 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/test.h" -#include "util/serializer.h" -#include "util/numerics/mpq.h" -#include "util/init_module.h" -using namespace lean; - -static void tst0() { - lean::mpq n1("10000000000000000000000000000000000000000"); - lean::mpq n2(317, 511); - std::cout << n1*n2 << "\n"; -} - -static void tst1() { - mpq a(2, 3), b(4, 3); - b = a / b; - lean_assert(b == mpq(1, 2)); - a = mpq(2); - a.inv(); - lean_assert(a == b); - a = -2; - b = mpq(-1, 2); - a.inv(); - lean_assert(a == b); -} - -static void tst2() { - mpq a(2, 3); - lean_assert(floor(a) == 0); - lean_assert(ceil(a) == 1); - mpq b(-2, 3); - lean_assert(floor(b) == -1); - lean_assert(ceil(b) == 0); - mpq c; - lean_assert(floor(c) == 0); - lean_assert(ceil(c) == 0); - mpq d(3); - lean_assert(d > 0); - lean_assert(d.is_pos()); - lean_assert(floor(d) == d); - lean_assert(ceil(d) == d); - mpq e(-3); - lean_assert(e < 0); - lean_assert(e.is_neg()); - lean_assert(floor(e) == e); - lean_assert(ceil(e) == e); -} - -static void tst3() { - mpq a("1"); - mpq b(1); - lean_assert(a == b); -} - -static void tst4() { - mpq a(8, 6); - lean_assert(a == mpq(4, 3)); - lean_assert(mpq(1, 2)+mpq(1, 2) == mpq(1)); - lean_assert(mpq("1/2") < mpq("2/3")); - lean_assert(mpq(-1, 2).is_neg()); - lean_assert(mpq(-1, 2).is_nonpos()); - lean_assert(!mpq(-1, 2).is_zero()); - lean_assert(mpq(1, 2) > mpq()); - lean_assert(mpq().is_zero()); - lean_assert(mpq(2, 3) + mpq(4, 3) == mpq(2)); - lean_assert(mpq(1, 2) >= mpq(1, 3)); - lean_assert(mpq(3, 4).get_denominator() == 4); - lean_assert(mpq(3, 4).get_numerator() == 3); - lean_assert(mpq(1, 2) / mpq(5, 4) == mpq(2, 5)); - lean_assert(mpq(1, 2) - mpq(2, 3) == mpq(-1, 6)); - lean_assert(mpq(3, 4) * mpq(2, 3) == mpq(1, 2)); - a *= 3; - lean_assert(a == 4); - a /= 2; - lean_assert(a == 2); - lean_assert(a.is_integer()); - a /= 5; - lean_assert(a == mpq(2, 5)); - lean_assert(!a.is_integer()); - mpq b(3, 7); - a *= b; - lean_assert(a == mpq(6, 35)); - a /= b; - lean_assert(a == mpq(2, 5)); - mpz c(5); - a *= c; - lean_assert(a == 2); - a += c; - lean_assert(a == 7); - a -= c; - lean_assert(a == 2); - a /= c; - lean_assert(a == mpq(2, 5)); -} - -static void tst5() { - mpq a; - a = 1; - lean_assert(a == mpq(1)); - lean_assert(a <= 1); - lean_assert(a < 2); - lean_assert(a > 0); - lean_assert(a >= 0); - lean_assert(a >= 1); - lean_assert(!(a >= 2)); - lean_assert(a == 1); - lean_assert(1 == a); - lean_assert(a != 2); - lean_assert(!(a == 3)); - lean_assert(a < mpz(2)); - lean_assert(a <= mpz(1)); - lean_assert(a > 0); - lean_assert(a <= 1u); - lean_assert(a < 2u); - lean_assert(a > 0u); - lean_assert(a >= 1u); - lean_assert(a == 1u); - lean_assert(1u >= a); - lean_assert(2u > a); - a = "1/3"; - lean_assert(a == mpq(1, 3)); - a = 2.0; - lean_assert(a == mpq(2)); - a = mpz(10); - lean_assert(a == mpq(10)); - lean_assert(a >= mpz(10)); - lean_assert(mpz(10) <= a); - lean_assert(mpz(10) >= a); - lean_assert(mpz(10) == a); -} - -static void check_dec(mpq const & q, char const * expected, unsigned prec = 10) { - std::ostringstream s; - display_decimal(s, q, prec); - std::cout << s.str() << "\n"; - lean_assert(s.str() == expected); -} - -static void tst6() { - mpq v1(1); - v1.floor(); - lean_assert(v1 == 1); - v1.ceil(); - lean_assert(v1 == 1); - v1 = mpq(1, 2); - v1.floor(); - lean_assert(v1 == 0); - v1 = mpq(1, 2); - v1.ceil(); - lean_assert(v1 == 1); - v1 -= 2u; - lean_assert(v1 == -1); - v1 = mpq(-1, 2); - v1.floor(); - lean_assert(v1 == -1); - v1 = mpq(-1, 2); - v1.ceil(); - lean_assert(v1 == 0); - check_dec(mpq(-1, 2), "-0.5"); - check_dec(mpq(1, 3), "0.33333?", 5); - check_dec(mpq(3), "3"); - check_dec(mpq(-2, 1), "-2"); - check_dec(mpq(-1, 3), "-0.33333?", 5); - check_dec(mpq(-1, 7), "-0.14285?", 5); - - lean_assert(cmp(mpq(1, 2), mpz(1)) < 0); - lean_assert(cmp(mpq(3, 2), mpz(1)) > 0); - lean_assert(cmp(mpq(-3, 2), mpz(-1)) < 0); -} - -static void tst7() { - std::ostringstream out; - serializer s(out); - mpq n1("-100000000000000000000000000000000000/3"); - lean_assert(n1.is_neg()); - mpq n2("-3/4"); - mpq n3("1200/2131"); - mpq n4("321/345"); - mpq n5(1, 3); - s << n1 << n2 << n3 << n4 << n5; - std::istringstream in(out.str()); - deserializer d(in); - mpq m1, m2, m3, m4, m5; - d >> m1 >> m2 >> m3 >> m4 >> m5; - lean_assert(n1 == m1); - lean_assert(n2 == m2); - lean_assert(n3 == m3); - lean_assert(n4 == m4); - lean_assert(n5 == m5); -} - -int main() { - initialize_util_module(); - tst0(); - tst1(); - tst2(); - tst3(); - tst4(); - tst5(); - tst6(); - tst7(); - finalize_util_module(); - return has_violations() ? 1 : 0; -} diff --git a/src/tests/util/numerics/mpz.cpp b/src/tests/util/numerics/mpz.cpp deleted file mode 100644 index 12e46413e8..0000000000 --- a/src/tests/util/numerics/mpz.cpp +++ /dev/null @@ -1,84 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include "util/test.h" -#include "util/serializer.h" -#include "util/numerics/mpz.h" -using namespace lean; - -static void tst1() { - mpz a(-10); - lean_assert_eq(a.log2(), 0); - lean_assert_eq(a.mlog2(), 3); - lean_assert_eq(a.is_power_of_two(), false); - unsigned shift = 0; - lean_assert_eq(a.is_power_of_two(shift), false); - lean_assert_eq(mpz(10).mlog2(), 0); - mpz r; - mpz b(30); - b-=10u; - lean_assert_eq(b, mpz(20)); - lean_assert(root(r, mpz(4), 2)); - lean_assert_eq(r, 2); - lean_assert(!root(r, mpz(10), 2)); - lean_assert_eq(r, 3); - lean_assert_eq(mpz(10) % mpz(3), mpz(1)); - lean_assert_eq(mpz(10) % mpz(-3), 1); - lean_assert_eq(mpz(-10) % mpz(-3), 2); - lean_assert_eq(mpz(-10) % mpz(3), 2); - mpz big; - big = pow(mpz(10), 10000); - std::ostringstream out; - out << big; - std::string s = out.str(); - lean_assert_eq(s.size(), 10001); - lean_assert_eq(s[0], '1'); - for (unsigned i = 1; i < 10001; i++) { - lean_assert_eq(s[i], '0'); - } -} - -static void tst2() { - std::ostringstream out; - serializer s(out); - mpz n1("-100000000000000000000000000000000000"); - lean_assert(n1.is_neg()); - mpz n2("0"); - mpz n3("1200"); - mpz n4("321"); - s << n1 << n2 << n3 << n4; - std::istringstream in(out.str()); - deserializer d(in); - mpz m1, m2, m3, m4; - d >> m1 >> m2 >> m3 >> m4; - lean_assert(n1 == m1); - lean_assert(n2 == m2); - lean_assert(n3 == m3); - lean_assert(n4 == m4); -} - -static void tst3() { - mpz n1(1099511627776ull); - mpz n2("1099511627776"); - lean_assert(n1 == n2); -} - -static void tst4() { - mpz n1(1152921504609785454ull); - mpz n2("1152921504609785454"); - lean_assert(n1 == n2); -} - -int main() { - tst1(); - tst2(); - tst3(); - tst4(); - return has_violations() ? 1 : 0; -} diff --git a/src/tests/util/sexpr.cpp b/src/tests/util/sexpr.cpp index 76cbb737f2..505927aac7 100644 --- a/src/tests/util/sexpr.cpp +++ b/src/tests/util/sexpr.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include "util/test.h" #include "util/name.h" #include "util/init_module.h" -#include "util/numerics/mpq.h" +#include "util/mpq.h" #include "util/sexpr/sexpr.h" #include "util/sexpr/sexpr_fn.h" #include "util/sexpr/format.h" diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index a773d07c35..e29d70a171 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(util OBJECT debug.cpp name.cpp name_set.cpp fresh_name.cpp +add_library(util OBJECT debug.cpp mpz.cpp mpq.cpp name.cpp name_set.cpp fresh_name.cpp exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp path.cpp stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp diff --git a/src/util/numerics/mpq.cpp b/src/util/mpq.cpp similarity index 98% rename from src/util/numerics/mpq.cpp rename to src/util/mpq.cpp index aa046a294d..88448cfa63 100644 --- a/src/util/numerics/mpq.cpp +++ b/src/util/mpq.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include "util/sstream.h" #include "util/thread.h" -#include "util/numerics/mpq.h" +#include "util/mpq.h" namespace lean { MK_THREAD_LOCAL_GET_DEF(mpz, get_tlocal1); diff --git a/src/util/numerics/mpq.h b/src/util/mpq.h similarity index 99% rename from src/util/numerics/mpq.h rename to src/util/mpq.h index 57f334d63e..bc8cfbc229 100644 --- a/src/util/numerics/mpq.h +++ b/src/util/mpq.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "util/numerics/mpz.h" +#include "util/mpz.h" namespace lean { /** diff --git a/src/util/numerics/mpz.cpp b/src/util/mpz.cpp similarity index 98% rename from src/util/numerics/mpz.cpp rename to src/util/mpz.cpp index ac25db66be..ada14373ee 100644 --- a/src/util/numerics/mpz.cpp +++ b/src/util/mpz.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include #include "util/sstream.h" #include "util/thread.h" -#include "util/numerics/mpz.h" +#include "util/mpz.h" #include namespace lean { diff --git a/src/util/numerics/mpz.h b/src/util/mpz.h similarity index 100% rename from src/util/numerics/mpz.h rename to src/util/mpz.h diff --git a/src/util/numerics/CMakeLists.txt b/src/util/numerics/CMakeLists.txt deleted file mode 100644 index da09d8bd4d..0000000000 --- a/src/util/numerics/CMakeLists.txt +++ /dev/null @@ -1 +0,0 @@ -add_library(numerics OBJECT init_module.cpp mpz.cpp mpq.cpp) diff --git a/src/util/numerics/init_module.cpp b/src/util/numerics/init_module.cpp deleted file mode 100644 index dd796f885b..0000000000 --- a/src/util/numerics/init_module.cpp +++ /dev/null @@ -1,17 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/memory.h" - -namespace lean { -void initialize_numerics_module() { -} - -void finalize_numerics_module() { -} -} diff --git a/src/util/numerics/init_module.h b/src/util/numerics/init_module.h deleted file mode 100644 index 76524a6a07..0000000000 --- a/src/util/numerics/init_module.h +++ /dev/null @@ -1,11 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -namespace lean { -void initialize_numerics_module(); -void finalize_numerics_module(); -} diff --git a/src/util/numerics/power.h b/src/util/numerics/power.h deleted file mode 100644 index fbc28dab87..0000000000 --- a/src/util/numerics/power.h +++ /dev/null @@ -1,26 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ - -namespace lean { -/** - \brief Template for computing a^k. -*/ -template -T power(T const & a, unsigned k) { - unsigned mask = 1; - T power(a); - T b(a); - b = 1; - while (mask <= k) { - if (mask & k) - b *= power; - power *= power; - mask = mask << 1; - } - return b; -} -} diff --git a/src/util/numerics/remainder.h b/src/util/numerics/remainder.h deleted file mode 100644 index 1ebde52653..0000000000 --- a/src/util/numerics/remainder.h +++ /dev/null @@ -1,20 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/debug.h" - -namespace lean { -template -T remainder(T a, T b) { - lean_assert(b != 0); - if (a > 0) - return a % b; - else if (b > 0) - return a % b + b; - else - return a % b - b; -} -}