Commit graph

13 commits

Author SHA1 Message Date
Leonardo de Moura
5cfcb7e144 chore(kernel/for_each): use consistent naming convetions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-19 11:24:02 -08:00
Leonardo de Moura
7f088b7635 feat(kernel): add (optional) field m_type to expr_const, this field is useful for implementing the tactic framework
This field should not be visible in the external API.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-19 11:21:52 -08:00
Leonardo de Moura
2951c92ad1 feat(kernel/for_each): avoid recursion at for_each template
It saves a lot of stack space.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 18:08:31 -08:00
Leonardo de Moura
4bed9f85b0 feat(kernel/for_each): add option for disabling cache of atomic expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 15:25:17 -07:00
Leonardo de Moura
57d9d23bd4 feat(kernel/for_each): allow function F to interrupt for_each search
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 14:58:02 -07:00
Leonardo de Moura
2dd44bdf1a perf(kernel/for_each): delay initialization of visited set
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 14:52:08 -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
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
Soonho Kong
5c3866cd71 Use fullpath in #include directives, add missing STL headers 2013-09-13 03:35:29 -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
99219f998b Rename files sets.h and maps.h to expr_sets.h and expr_maps.h
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-15 19:02:28 -07:00
Soonho Kong
a1229692b0 Add static_asserts for higher-order functions in kernel/for_each.h and kernel/pp.cpp 2013-08-09 22:41:07 -07:00
Leonardo de Moura
2670e94398 Add pretty printer for Lean environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-07 19:10:12 -07:00