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.
This commit is contained in:
Leonardo de Moura
parent
74f10fdf5c
commit
4b6583ae9f
28 changed files with 19 additions and 401 deletions
|
|
@ -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} $<TARGET_OBJECTS:util>)
|
||||
add_subdirectory(util/numerics)
|
||||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:numerics>)
|
||||
add_subdirectory(util/sexpr)
|
||||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:sexpr>)
|
||||
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)
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
add_executable(leanchecker checker.cpp text_import.cpp simple_pp.cpp
|
||||
$<TARGET_OBJECTS:util> $<TARGET_OBJECTS:sexpr>
|
||||
$<TARGET_OBJECTS:kernel> $<TARGET_OBJECTS:inductive> $<TARGET_OBJECTS:quotient>)
|
||||
target_link_libraries(leanchecker ${EXTRA_UTIL_LIBS})
|
||||
target_link_libraries(leanchecker ${EXTRA_LIBS})
|
||||
install(TARGETS leanchecker DESTINATION bin)
|
||||
|
|
|
|||
|
|
@ -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 {
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#include <string>
|
||||
#include "library/kernel_serializer.h"
|
||||
#include "util/numerics/mpz.h"
|
||||
#include "util/mpz.h"
|
||||
|
||||
namespace lean {
|
||||
static name * g_prenum_name = nullptr;
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <string>
|
||||
#include "util/numerics/mpz.h"
|
||||
#include "util/mpz.h"
|
||||
#include "kernel/expr.h"
|
||||
#include "library/constants.h"
|
||||
#include "library/num.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.
|
||||
|
|
|
|||
|
|
@ -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 {
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
||||
|
|
|
|||
|
|
@ -1,10 +1,10 @@
|
|||
add_executable(name name.cpp $<TARGET_OBJECTS:util>)
|
||||
target_link_libraries(name ${EXTRA_LIBS})
|
||||
add_exec_test(name "name")
|
||||
add_executable(sexpr_tst sexpr.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
|
||||
add_executable(sexpr_tst sexpr.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:sexpr>)
|
||||
target_link_libraries(sexpr_tst ${EXTRA_LIBS})
|
||||
add_exec_test(sexpr "sexpr_tst")
|
||||
add_executable(format format.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
|
||||
add_executable(format format.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:sexpr>)
|
||||
target_link_libraries(format ${EXTRA_LIBS})
|
||||
add_exec_test(format "format")
|
||||
add_executable(buffer buffer.cpp $<TARGET_OBJECTS:util>)
|
||||
|
|
@ -13,7 +13,7 @@ add_exec_test(buffer "buffer")
|
|||
add_executable(list list.cpp $<TARGET_OBJECTS:util>)
|
||||
target_link_libraries(list ${EXTRA_LIBS})
|
||||
add_exec_test(list "list")
|
||||
add_executable(options options.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
|
||||
add_executable(options options.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:sexpr>)
|
||||
target_link_libraries(options ${EXTRA_LIBS})
|
||||
add_exec_test(options "options")
|
||||
add_executable(rb_tree rb_tree.cpp $<TARGET_OBJECTS:util>)
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ Author: Soonho Kong
|
|||
#include <string>
|
||||
#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"
|
||||
|
|
|
|||
|
|
@ -1,6 +0,0 @@
|
|||
add_executable(mpq mpq.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
|
||||
target_link_libraries(mpq ${EXTRA_LIBS})
|
||||
add_exec_test(mpq "mpq")
|
||||
add_executable(mpz mpz.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
|
||||
target_link_libraries(mpz ${EXTRA_LIBS})
|
||||
add_exec_test(mpz "mpz")
|
||||
|
|
@ -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 <iostream>
|
||||
#include <sstream>
|
||||
#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;
|
||||
}
|
||||
|
|
@ -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 <iostream>
|
||||
#include <sstream>
|
||||
#include <string>
|
||||
#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;
|
||||
}
|
||||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
@ -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 {
|
||||
/**
|
||||
|
|
@ -7,7 +7,7 @@ Author: Leonardo de Moura
|
|||
#include <memory>
|
||||
#include "util/sstream.h"
|
||||
#include "util/thread.h"
|
||||
#include "util/numerics/mpz.h"
|
||||
#include "util/mpz.h"
|
||||
#include <string>
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -1 +0,0 @@
|
|||
add_library(numerics OBJECT init_module.cpp mpz.cpp mpq.cpp)
|
||||
|
|
@ -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 <cstddef>
|
||||
#include <gmp.h>
|
||||
#include "util/memory.h"
|
||||
|
||||
namespace lean {
|
||||
void initialize_numerics_module() {
|
||||
}
|
||||
|
||||
void finalize_numerics_module() {
|
||||
}
|
||||
}
|
||||
|
|
@ -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();
|
||||
}
|
||||
|
|
@ -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 <tt>a^k</tt>.
|
||||
*/
|
||||
template<typename T>
|
||||
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;
|
||||
}
|
||||
}
|
||||
|
|
@ -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<class T>
|
||||
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;
|
||||
}
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue