Leonardo de Moura
|
cd5e45bae2
|
Reduce pvector delta_cell quota on reads. Add example that demonstrates why this is needed.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-12 08:28:24 -07:00 |
|
Soonho Kong
|
5858c9d5e0
|
Update tests/util/list.cpp to suppress a g++ warning
|
2013-09-12 01:39:04 -07:00 |
|
Leonardo de Moura
|
f7196e05ff
|
Add 'persistent' vectors. We should use the same approach for queues.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-11 19:48:55 -07:00 |
|
Leonardo de Moura
|
ef0e0ad382
|
Add (optional) performance tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-11 19:48:55 -07:00 |
|
Leonardo de Moura
|
572c7ced2a
|
Add #include<atomic> to expr.h. We need it when #define LEAN_THREAD_UNSAFE_REF_COUNT is used
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-11 19:48:55 -07:00 |
|
Leonardo de Moura
|
ed15a2df9b
|
Use split_reverse_second instead of split and then reverse in queue
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-11 19:48:55 -07:00 |
|
Leonardo de Moura
|
37498f9fb8
|
Add persistent queues
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-11 19:48:54 -07:00 |
|
Leonardo de Moura
|
3657320edb
|
Add basic list functions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-11 19:48:54 -07:00 |
|
Soonho Kong
|
7a6032dd86
|
Update memcheck.supp to ignore bash memroy leak on Fedora19
|
2013-09-10 22:44:24 -04:00 |
|
Soonho Kong
|
9e3583a04a
|
Update memcheck.supp to match the thread bug patterns we get by using clang++-3.3
|
2013-09-10 17:37:22 -07:00 |
|
Soonho Kong
|
a993424165
|
Use "--gen-suppressions=all" in valgrind
|
2013-09-10 17:09:39 -07:00 |
|
Soonho Kong
|
6569406fb9
|
Update memcheck.supp
add reference for the suppression stuff
[skip ci]
|
2013-09-10 15:47:47 -07:00 |
|
Soonho Kong
|
3505ed8adb
|
Use suppressions file to ignore certain valgrind warnings
|
2013-09-10 15:37:09 -07:00 |
|
Soonho Kong
|
9113f824bd
|
Use '--track-origins=yes' option in valgrind
|
2013-09-10 14:31:30 -07:00 |
|
Leonardo de Moura
|
6fe86ffefd
|
Fix initialized memory error reported by Valgrind. Disable 2 tests that produce memory leaks due to a bug in g++.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-10 13:51:02 -07:00 |
|
Soonho Kong
|
fae6c29237
|
Fix memory leaks in mpfp.h
|
2013-09-10 13:26:14 -07:00 |
|
Soonho Kong
|
8ce18a1508
|
Use "--leak-check=full" option in valgrind
|
2013-09-10 13:12:22 -07:00 |
|
Soonho Kong
|
f4edbba325
|
Turn off '--show-reachable=yes' valgrind option
|
2013-09-10 12:34:33 -07:00 |
|
Soonho Kong
|
b04bdae763
|
Use "--trace-children=yes" option for MemCheck(valgrind) to handle
leantests shell script
|
2013-09-10 10:47:04 -07:00 |
|
Leonardo de Moura
|
4c67721d32
|
Fix test error on Cygwin
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-09 18:35:11 -07:00 |
|
Leonardo de Moura
|
adfbba6447
|
Fix problem reported by Soonho
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-08 23:10:33 -07:00 |
|
Leonardo de Moura
|
2ca30571b4
|
Display the input term in the output of the Check command. It is useful to see the fully elaborated term.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-08 22:55:21 -07:00 |
|
Leonardo de Moura
|
a8ba50531b
|
Fix typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-08 20:38:11 -07:00 |
|
Leonardo de Moura
|
59a589037e
|
Keep expanded form when pretty printings variable declarations with implicit marks (i.e., curly braces)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-08 11:23:46 -07:00 |
|
Leonardo de Moura
|
df116f88e0
|
Improve pretty printer for Pi's
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-08 11:04:07 -07:00 |
|
Leonardo de Moura
|
1cee392483
|
Add light_checker: module for extracting the type of (fully elaborated) expressions. It is much faster than type_checker, which infers the type but also check whether the input is type correct or not.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-07 22:33:18 -07:00 |
|
Leonardo de Moura
|
33c4b44b2b
|
Encapsulate context implementation. The current implementantion based on lists may be a performance problem in the future, and we should be able to change it without affecting the whole code base.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-07 11:15:11 -07:00 |
|
Leonardo de Moura
|
bab11b57ad
|
Move Symm and Trans back to basic_thms.cpp
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 23:49:35 -07:00 |
|
Leonardo de Moura
|
c674bb3790
|
Add castlib as an independent library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 23:40:47 -07:00 |
|
Leonardo de Moura
|
7a9d53d0d7
|
Refactor arith libraries
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 23:19:47 -07:00 |
|
Leonardo de Moura
|
b92bbeb83b
|
Add casting propagation and normalization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 20:45:26 -07:00 |
|
Leonardo de Moura
|
7eab229114
|
Improve check_pi in lean elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 18:58:33 -07:00 |
|
Leonardo de Moura
|
c0c2f52087
|
Add Cast, DomInj and RanInj. Improve operator << for lean_frontend objects.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 18:32:15 -07:00 |
|
Leonardo de Moura
|
b62816cc25
|
Fix problem with pretty printer. Add another test for elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 18:01:11 -07:00 |
|
Leonardo de Moura
|
edafd519e1
|
Add missing case to elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 17:43:08 -07:00 |
|
Leonardo de Moura
|
26bf7bcaac
|
Fix bug in the elaborator. Move character ' to class A
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 17:12:35 -07:00 |
|
Leonardo de Moura
|
8840b37258
|
Fix type checker and elaborator for let expressions. Fix get_coercions (we need to pass the context). Fix pretty printer for def_type_mismatch_exception.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 11:02:00 -07:00 |
|
Leonardo de Moura
|
2459c4ae7c
|
Add (optional) type to let declarations
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 10:06:26 -07:00 |
|
Leonardo de Moura
|
6da194334e
|
Move 'slow' test files to different subdir. Modify CTestCustom.cmake.in to run leantests.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 08:48:12 -07:00 |
|
Leonardo de Moura
|
6f3b0c30fb
|
Add 'Variables' command.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 08:48:12 -07:00 |
|
Leonardo de Moura
|
3dc55c452c
|
Parse decimal values
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 08:48:12 -07:00 |
|
Leonardo de Moura
|
b3a095b068
|
Fix pretty printer for evaluator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-05 18:57:29 -07:00 |
|
Leonardo de Moura
|
c22bd8b6ed
|
Clean elaborator_exception pretty printing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-05 10:15:52 -07:00 |
|
Leonardo de Moura
|
eb96e6441f
|
Moved kernel exception formatting to kernel_exception_formatter.cpp.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-05 10:15:43 -07:00 |
|
Soonho Kong
|
974b99b424
|
Update CTestCustom.cmake.in
Exclude "threads" test from valgrind targets
[skip ci]
|
2013-09-04 16:41:04 -07:00 |
|
Leonardo de Moura
|
87d3961158
|
Improve elaborator error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-04 16:36:58 -07:00 |
|
Leonardo de Moura
|
613d83cdf4
|
Improve application type mismatch errors. We also show the implicit arguments (not just their types)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-04 16:36:58 -07:00 |
|
Leonardo de Moura
|
408005b730
|
Fix typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-04 16:36:57 -07:00 |
|
Soonho Kong
|
30e5ac7004
|
Fix OSX linker warning issue
|
2013-09-04 15:35:07 -07:00 |
|
Leonardo de Moura
|
be7fa0932a
|
Add unicode name for the types: Nat, Int and Real
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-04 09:03:41 -07:00 |
|