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

574 commits

Author SHA1 Message Date
Leonardo de Moura
2800292947 Add timestamp to metavar_env 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 19:50:48 -07:00
Leonardo de Moura
5a4bc331d2 Make unification_problems a virtual class. Associate a 'standard' context with each metavariable in metavar_env 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 19:38:36 -07:00
Leonardo de Moura
63e102055e Move metavariables to the kernel. This is the first step for implementing the new elaborator. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 12:09:01 -07:00
Soonho Kong
e4b327bbaa Use C++11's <random> in pdeque/pvector tests (cygwin doesn't support rand_r) 2013-09-15 01:38:57 -07:00
Soonho Kong
dcc917a6b4 Use "sprintf" instead of "snprintf" because cygwin doesn't support "snprintf" 2013-09-15 01:38:21 -07:00
Soonho Kong
b553521578 Attempt to suppress valgrind warnings on Travis 
- don't understand why cmake on travis doesn't pick up the memcheck.supp
file. It works on my local machine.
 2013-09-15 01:17:05 -07:00
Soonho Kong
30f4b2de5f Update memcheck.supp 
[skip ci]
 2013-09-14 19:33:47 -07:00
Soonho Kong
ce05345129 Update CTestConfig.cmake to fix memcheck.supp 2013-09-14 20:22:05 -04:00
Soonho Kong
60903d3cea Fix cygwin build which was failed due to snprintf 2013-09-14 17:11:37 -07:00
Soonho Kong
c96a6982a0 Add <ctime> header for time() in pdeque/pvector tests 2013-09-13 20:42:49 -07:00
Soonho Kong
5266e22f05 Remove debug code from cpplint.py 2013-09-13 20:37:31 -07:00
Soonho Kong
eda25e77a4 Use time(0) as an initial seed for rand_r() in pvector/pdeque tests 2013-09-13 20:28:15 -07:00
Soonho Kong
f8c0c02cb0 Exclude 'style_check' from MemCheck list 2013-09-13 20:27:35 -07:00
Soonho Kong
0905529720 Add "style_check" test 2013-09-13 20:00:55 -07:00
Soonho Kong
0c450b5c23 Add StyleCheck.cmake 2013-09-13 19:21:02 -07:00
Soonho Kong
f620f54b32 Add target "style" to run cpplint.py 
- try "ninja style"
 2013-09-13 19:15:38 -07:00
Soonho Kong
bc60b47295 Apply coding style 2013-09-13 18:48:09 -07:00
Leonardo de Moura
99eaff0b4f Extract private and static, and add treeview to documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 17:55:37 -07:00
Leonardo de Moura
bcc3827a99 Modify Doxygen file to extract all elements even the undocumented ones. Disable warnings for undocumented entities. Add extra comments. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 13:46:22 -07:00
Leonardo de Moura
d54834279e Use consistent coding style for if-then-else 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 12:57:40 -07:00
Leonardo de Moura
8c735f1daa Use consistent coding style for spaces after ',' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 12:49:03 -07:00
Leonardo de Moura
2c68117adf Tag TODOs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 12:25:21 -07:00
Leonardo de Moura
18f9378f97 Rename numtype.h to num_type.h 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 09:07:44 -07:00
Leonardo de Moura
573ec5ccc2 Rename import_all. The idea is to use consistent name for library files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 09:06:46 -07:00
Leonardo de Moura
0c09e4524a Use consistent names for import functions, and library files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 08:58:34 -07:00
Leonardo de Moura
070c87bef0 Rename arith library files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 08:55:09 -07:00
Soonho Kong
5c3866cd71 Use fullpath in #include directives, add missing STL headers 2013-09-13 03:35:29 -07:00
Leonardo de Moura
4c19cc6957 Rename lean frontend files. The prefix lean_ is not necessary anymore. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 20:09:35 -07:00
Leonardo de Moura
26097475fd Use fullpath in #include directives. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 20:04:10 -07:00
Leonardo de Moura
c655e9fe7b Move sexpr_funcs to sexpr_fn. Using consistent file name conventions. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 18:27:46 -07:00
Leonardo de Moura
2e990ef7d3 Fix warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 14:02:40 -07:00
Leonardo de Moura
bc69e7803f Add support for writing a[i] = v instead of a.set(i, v) in the pdeque class. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 11:18:26 -07:00
Leonardo de Moura
74b8a4f0ac Add support for writing a[i] = v instead of a.set(i, v) in the pvector class. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 11:12:02 -07:00
Leonardo de Moura
f972cc9aae Fix bugs in pvector. Improve test driver 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 11:01:40 -07:00
Leonardo de Moura
55ff49d2d5 Replace queue.h with pdeque.h 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 10:09:54 -07:00
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