Leonardo de Moura
cf2c0f8ebb
feat(numerics): add gcd and extended gcd templates (for primitive types)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-16 18:18:20 -07:00
Leonardo de Moura
39f68ed0d6
feat(numerics): add is_prime function
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-16 17:25:08 -07:00
Leonardo de Moura
1097bbfb22
fix(style): fix warnings produced by cpplint.py, disable sizeof(type) warning
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-16 17:04:39 -07:00
Leonardo de Moura
105f55c68b
feat(numerics): add zero() method to all numeric_traits
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-16 16:55:17 -07:00
Leonardo de Moura
ff04c5a2e2
test(numerics): add test to make sure that zeros of different precision mpfp numbers are the equal.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-16 16:54:43 -07:00
Leonardo de Moura
467eff4662
add(numerics): add prime number generator/iterator
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-16 16:05:45 -07:00
Leonardo de Moura
29ad71f9fc
test(conversion): add more conversion tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-15 15:35:08 -07:00
Leonardo de Moura
0783805671
feat(kernel): add weight to kernel definitions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-15 14:50:08 -07:00
Leonardo de Moura
e01da4d4e5
doc(todo): update todo.md
2013-10-02 09:56:45 -07:00
Leonardo de Moura
5bd6ba37d0
fix(light_checker): fix inconsistent cache bug in light_checker, add tests that expose the problem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-01 19:25:58 -07:00
Leonardo de Moura
aa5be3262f
fix(type_checker): fix inconsistent cache bug in type_checker, add tests that expose the problem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-01 19:23:55 -07:00
Leonardo de Moura
2089d12bd0
fix(replace_using_ctx): fix inconsistent cache bug in replace_using_ctx, and add tests that expose the problem
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-01 18:52:18 -07:00
Soonho Kong
760f2e15ce
feat(library/replace_using_ctx): add static_assert
2013-10-01 16:47:49 -07:00
Soonho Kong
e3b762e909
feat(kernel): add static_assert to expr,expr_eq,replace
2013-10-01 16:47:36 -07:00
Soonho Kong
b823c7d779
feat(util): add static_assert to {scoped,splay}_{map,set}
2013-10-01 16:47:28 -07:00
Soonho Kong
a726f5fbb7
feat(util/list): add static_asserts for map/for_each/compare
2013-10-01 09:05:53 -07:00
Soonho Kong
3381df0150
fix(util/list_fn): rename iter to for_each
2013-10-01 09:03:07 -07:00
Soonho Kong
c50bc13be0
test(library/rewriter): add more tests
2013-10-01 00:30:38 -07:00
Soonho Kong
7c0b56ad0d
feat(library/rewriter): implement repeat/app/lambda/pi/try rewriter
...
- refactor to use rewriter_cell
- implement display and operator<< for debugging
2013-10-01 00:30:31 -07:00
Soonho Kong
e6c76fbe76
refactor(library/rewriter/fo_match): add more lean_trace for debugging
2013-10-01 00:20:12 -07:00
Soonho Kong
a832173f5f
feat(kernel/expr): add expr::operator() which takes 8 args
2013-10-01 00:19:30 -07:00
Soonho Kong
1a3ea26032
feat(util/list_fn): add iter function
2013-10-01 00:18:55 -07:00
Leonardo de Moura
15979ab991
fix(lean): fix warnings produced by cppcheck
...
Fix (relevant) warnings produced by http://cppcheck.sourceforge.net .
Most warnings produced were incorrect. The tool does not seem to support some of the C++11 new features.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-30 21:38:55 -07:00
Leonardo de Moura
30089aa4f8
test(type_checker): add example showing how to use the kernel exception formatter
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-30 16:39:29 -07:00
Soonho Kong
2619c30fe9
fix(script/demangle_cpptype): process line-by-line, instead of waiting for EOF
2013-09-29 18:36:01 -07:00
Soonho Kong
54f4c4d9bc
test(library/rewriter/fo_match): clean up enable_trace
2013-09-29 18:36:01 -07:00
Leonardo de Moura
8d3ae665e7
fix(splay_map): fix typo
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-29 17:30:08 -07:00
Leonardo de Moura
21f9699661
test(splay_tree): add missing test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-29 17:28:10 -07:00
Leonardo de Moura
790c2a72d5
test(safe_arith): add unit tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-29 17:20:32 -07:00
Leonardo de Moura
1179b6b52b
test(hash): add missing tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-29 17:20:32 -07:00
Leonardo de Moura
57b6148bbb
test(buffer): add missing tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-29 17:20:32 -07:00
Soonho Kong
a46b313c1c
chore(travis): use demangle_cpptype.py to print out test/valgrind output
...
[skip ci]
2013-09-29 16:30:02 -07:00
Soonho Kong
c364110415
chore(scrips): add demangle_cpptype.py
2013-09-29 15:57:25 -07:00
Leonardo de Moura
02f621aa45
test(lazy_list): add more tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-29 14:38:35 -07:00
Soonho Kong
80c282d0a3
chore(travis): do not use c++filt on Linux builds
...
There is a bug in c++filt on Linux. For instance,
c++filt -t 355687428096000
causes a segmentation fault.
2013-09-29 13:27:32 -07:00
Leonardo de Moura
3c8dff9085
feat(lazy_list): implement ML-like lazy lists
...
We will use lazy lists to represent the set of solutions produced by the elaborator. The elaborator plugins will also use lazy lists.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-29 12:35:26 -07:00
Soonho Kong
58e2ec331c
chore(travis): use c++filt to handle demangled c++ names
2013-09-28 23:38:22 -07:00
Soonho Kong
841a1fb20c
fix(debug): print type in lean_assert, print bool correctly
...
- use typeinfo to print out a type of value when an assertion fails.
need to use "c++filt --types" to demangle names for non-basic types.
- use std::boolalpha and std::noboolalpha to control the printed values
for "true" and "false"
2013-09-28 23:38:21 -07:00
Soonho Kong
4602dfd209
test(util/numerics): more tests to improve coverage
2013-09-28 23:38:17 -07:00
Soonho Kong
d3c2d2da5f
doc(automatic_builds): add how to prevent a build on Travis-ci
...
[skip ci]
2013-09-28 13:40:41 -07:00
Soonho Kong
d48ec2ddfa
chore(travis): fix git-commit-msg extraction
...
[skip-ci]
2013-09-28 13:33:13 -07:00
Soonho Kong
fb3635a9ef
test(util/numerics/mpbp): add more tests for improving coverage
2013-09-28 01:01:52 -07:00
Soonho Kong
6519d4bb0f
chore(memcheck.supp): generalize TCmalloc_Bug2 pattern
...
to suppress a warning from MSR 32bit build
[skip-ci]
2013-09-27 19:16:02 -07:00
Soonho Kong
db6e0ce319
chore(travis): set stack size as unlimited before run valgrind
2013-09-27 19:05:23 -07:00
Soonho Kong
f1407d501a
chore(travis): fix testcov problem
2013-09-27 17:56:33 -07:00
Soonho Kong
0ce089b942
chore(travis): push all linux builds to cdash
2013-09-27 17:56:33 -07:00
Soonho Kong
3527babfee
chore(travis): use consistent build name
...
- have build name is in the form of
"<BRANCH>_<CXX_COMPILER>_<BUILD_TYPE>(_TC)?"
to have consistency over time.
- have "Generator" field in cdash XMLs which is in the form of
"<GIT_COMMIT>###<GIT_SUBJECT>"
it will be displayed as a small mouseover-text.
2013-09-27 12:22:44 -07:00
Soonho Kong
0065d69e0a
chore(build): put --coverage CXX_FLAGS for TESTCOV build
2013-09-27 10:24:31 -07:00
Leonardo de Moura
d2667d56c0
test(lean/parser): add more tests for improving coverage
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-27 09:59:50 -07:00
Leonardo de Moura
0ff69d28f3
test(lean/scanner): add more tests for improving coverage
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-27 09:59:50 -07:00