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

3691 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
ceb6537e3a Fix race condition when updating expression flags: max_shared and closed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
1398c927cd Fix compilation error with clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
4b61639f4d Use consistent naming for functional objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
4ae0c4c445 Remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
9b3c47a521 Refactor instantiate/abstract code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
c7b12a2815 Add abstract/instantiate for kernel expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
ed6d6483fe Rename abst_expr -> abst_body 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
9fd88e6e27 Add small demo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00
Leonardo de Moura
576726bf58 Use operator() for creating applications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:31 -07:00
Leonardo de Moura
54a02b4fc7 Simplify expr accessor names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:31 -07:00
Leonardo de Moura
2c3fc09e3c Add has_free_vars/closed function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:31 -07:00
Leonardo de Moura
17e69e32d7 Add expression offset pair 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:31 -07:00
Leonardo de Moura
6a2c9ef076 Rename/Reorg some kernel files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:31 -07:00
Leonardo de Moura
90f498994a Add some overloads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:31 -07:00
Soonho Kong
17834d531c Add update_doxygen.sh script and use it in .travis.yml 2013-07-24 06:33:01 -07:00
Soonho Kong
913b107449 Update .travis.yml to generate doxygen 2013-07-24 06:08:47 -07:00
Soonho Kong
fc27c4af89 Add Doxyfile (configuration file for Doxygen) 2013-07-24 08:22:12 -04:00
Soonho Kong
e5c39cad9c Add color code in format.cpp to test how it looks on terminal 2013-07-23 18:42:40 -07:00
Soonho Kong
ab81a57d86 Add test cases for format 2013-07-23 18:42:36 -07:00
Soonho Kong
03b1ce643e Restructure format, add group and flatten 2013-07-23 18:42:31 -07:00
Soonho Kong
71638a8ad4 Add pretty-print: format.cpp, format.h 2013-07-23 10:43:41 -07:00
Soonho Kong
03740ca77a Update .travis.yml to extend build matrix with/without tcmalloc 2013-07-23 10:43:41 -07:00
Soonho Kong
eb60e8054e Update the build image in README.md 2013-07-23 09:30:46 -07:00
Leonardo de Moura
f00d8c4683 Fix bug in max_sharing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-23 09:18:18 -07:00
Leonardo de Moura
dd74284fdc Cleanup eq_functor 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-23 09:12:15 -07:00
Leonardo de Moura
79d00f4d78 Rename max_sharing files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-23 09:01:54 -07:00
Leonardo de Moura
5aa25a635f Add max_shared flag to expr_cell. Improve app constructor. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-23 08:59:39 -07:00
Leonardo de Moura
2a9d0de57b Add max_shared: function for computing maximally shared expressions. 2013-07-22 19:31:27 -07:00
Leonardo de Moura
aed8a07c1b Add sexpr test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-22 19:02:11 -07:00
Leonardo de Moura
e6a694ebcc Add expr test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-22 17:58:35 -07:00
Leonardo de Moura
06320c8615 Replace expr == with recursive function. Add goodies for traversing expressions. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-22 16:40:17 -07:00
Leonardo de Moura
c4cd6c4f84 Add tests for kernel expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-22 13:04:27 -07:00
Leonardo de Moura
c32dfe22b6 Add expressions (dependent type theory) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-22 12:46:11 -07:00
Leonardo de Moura
a2e72dbd92 Rename get_kind() -> kind() 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-22 09:30:55 -07:00
Soonho Kong
34ebbb2727 Update README.md to include build-status image 2013-07-22 06:40:25 -07:00
Soonho Kong
bffe36a37f Add .travis.yml 2013-07-22 06:40:25 -07:00
Leonardo de Moura
03cc3739d4 Fix bugs in mpbq. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-21 20:12:04 -07:00
Leonardo de Moura
24cf1a7c3d Add cmp (total order) for sexpr 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-21 17:05:32 -07:00
Leonardo de Moura
f6e18045f3 Add eqp (pointer equality) tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-21 15:59:10 -07:00
Leonardo de Moura
9e966a0e57 Add total order for hierarchical names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-21 15:56:18 -07:00
Leonardo de Moura
ecb7316943 Fix bugs in hierarchical names module. Add unit tests. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-21 15:08:14 -07:00
Leonardo de Moura
ecc8e8f813 Improve consistency of unit tests names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-21 14:52:20 -07:00
Leonardo de Moura
8af56394cc Add foreach for S-expression lists 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-21 14:32:36 -07:00
Leonardo de Moura
b8315e5593 Fix ambiguous overloads. Improve == test for sexprs. Remove redundant code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-21 14:25:56 -07:00
Leonardo de Moura
80d8fdbf48 Fix tests exit code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-20 18:04:05 -07:00
Leonardo de Moura
403e6a141b Add useful goodies for S-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-20 18:01:10 -07:00
Leonardo de Moura
05991c827b Add S-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-20 17:22:13 -07:00
Leonardo de Moura
eda1a337de Add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-20 14:23:52 -07:00
Leonardo de Moura
f71fdea42e Add hash goodies, and name::hash() 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-20 14:23:34 -07:00
Leonardo de Moura
f7e59366ea Add neg, div, power to interval. Fix bug in -= operator at interval. Add some unit tests for interval class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-19 19:24:38 -07:00