michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
1398 commits 3 branches 0 tags 28 MiB
Commit graph

142 commits

Author SHA1 Message Date
Leonardo de Moura
e7ae749221 feat(boost): implement multi-threading support using Boost 
To use Boost instead of the standard library, we must use the cmake option
    -D BOOST=ON

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 17:24:32 -08:00
Leonardo de Moura
8f2fe273ea refactor(*): isolate std::thread dependency 
This commit allows us to build Lean without the pthread dependency.
It is also useful if we want to implement multi-threading on top of Boost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 15:20:26 -08:00
Leonardo de Moura
e2999d3ff6 feat(*): add component name to check_stack and check_system 
I also reduced the stack size to 8 Mb in the tests at tests/lean and tests/lean/slow. The idea is to simulate stackoverflow conditions.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 15:11:55 -08:00
Leonardo de Moura
fa35fd6989 chore(*): make sure LEAN_THREAD_UNSAFE build flag is handled correctly 
When LEAN_THREAD_UNSAFE=ON, we:

- Do not run tests at tests/lua/threads
- Disable thread object at Lua API
- par tactical becomes an alias for interleave
- Disable some unit tests that use threads

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-04 10:27:22 -08:00
Soonho Kong
4de3b772fd feat(util/stackinfo): implement get_stack_size (Mac OSX version) 2013-12-01 22:24:12 -05:00
Leonardo de Moura
74dfdd02de feat(util): add primitives for checking the amount of available stack space 
Recursive functions that may go very deep should invoke the function check_stack. It throws an exception if the amount of stack space is limited.

The function check_system() is syntax sugar for
    check_interrupted();
    check_stack();

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 17:19:27 -08:00
Leonardo de Moura
737e634556 fix(util/list): bug in map template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 08:51:24 -08:00
Leonardo de Moura
7ff791eb9f feat(util/name_set): add mk_unique (with respect to a name_set) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 11:28:38 -08:00
Leonardo de Moura
6da13cc245 feat(util/list): map_append template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 11:28:38 -08:00
Leonardo de Moura
fe79bbf2b7 feat(util/list): filter template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-30 11:28:38 -08:00
Leonardo de Moura
8e87ef5da8 feat(util/lazy_list): add repeat and repeat_at_most templates for lazy_lists 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 11:16:37 -08:00
Leonardo de Moura
40a2f0a588 refactor(util/lazy_list): polish lazy_list API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 17:45:01 -08:00
Leonardo de Moura
bcd88cac08 style(util): missing includes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 17:05:46 -08:00
Leonardo de Moura
924187b055 feat(util/lazy_list): add par template for lazy lists) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 16:51:17 -08:00
Leonardo de Moura
157a2b36db feat(lazy_list): add timeout template for lazy_lists 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 16:27:36 -08:00
Leonardo de Moura
f19944cf09 refactor(util/lazy_list): 'lazier' lazy_lists 
In the new implementation, even the head of the lazy list is computed on demand.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 15:33:30 -08:00
Leonardo de Moura
9eb6da2a31 feat(util): add optional template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 13:27:22 -08:00
Leonardo de Moura
a776c8b158 feat(util/interrupt): add sleep_for, and simplify request_interrupt 
The Lean sleep_for checks the interrupt flag from time to time.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 11:32:12 -08:00
Leonardo de Moura
935349ec91 fix(tests/util/thread): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 10:23:20 -08:00
Leonardo de Moura
1f225d2752 feat(util/lazy_list): add useful lazy_list function templates 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 09:40:56 -08:00
Leonardo de Moura
8515821d56 feat(util/list): add map_filter template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
87eb254a1a fix(tests/util/thread): incorrect unit test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-20 11:28:19 -08:00
Leonardo de Moura
eba31a0516 test(util/interval): add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 19:07:09 -08:00
Leonardo de Moura
a98fdd9be6 refactor(shell): combine lean and leanlua executables in a single executable 
The main motivation is to allow users to configure/extend Lean using .lua files before loading the actual .lean files.
Example:
        ./lean extension1.lua extension2.lua file.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 16:48:21 -08:00
Leonardo de Moura
2265ef78c4 feat(util/list): add emplace_front 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 16:27:31 -08:00
Leonardo de Moura
e10d17a0f4 feat(util/sexpr): avoid recursion when destructing sexpr's 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 17:46:53 -08:00
Leonardo de Moura
76252816ac perf(util/list): avoid recursion in map and destructor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 16:47:52 -08:00
Leonardo de Moura
d67bf995ed feat(util/list): avoid recursion at for_each template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 15:52:31 -08:00
Leonardo de Moura
adf4856f88 feat(util/list): add map_reuse template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 15:32:02 -08:00
Leonardo de Moura
53dc8c8c57 test(util/shared_mutex): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 14:03:18 -08:00
Leonardo de Moura
1315378ebb test(*): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 09:13:34 -08:00
Leonardo de Moura
596e4aeb57 feat(util/shared_mutex): add shared_mutex object, this is a temporary replacement for std::shared_mutex that will be available in C++11 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 20:00:21 -08:00
Leonardo de Moura
5f11392fcc test(numerics/numeric_traits): add missing test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-28 07:50:33 -07:00
Leonardo de Moura
1d18f60dd5 fix(numerics): add missing numeric_traits<float>::zero() 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-28 07:47:23 -07:00
Leonardo de Moura
42edc4a72d test(set): add set of pointers test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
93d4466d06 refactor(interval): move interval unit tests to tests/util/interval 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-21 18:17:34 -07:00
Leonardo de Moura
e208309abd refactor(numerics): rename power operator to pow, the idea is to follow the C/C++ name convention for the power operator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-21 17:23:56 -07:00
Leonardo de Moura
1429cc9df2 feat(numerics): add finite field Z/pZ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-18 13:27:28 -07:00
Leonardo de Moura
bdade0e638 fix(numerics): problem with gcd tests on OSX 
Now, we only test gcd(a, b) for a != b && a != 0 && b != 0.
When one of these conditions do not hold, the result is implementation dependent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-17 10:38:02 -07:00
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
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
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