Commit graph

2 commits

Author SHA1 Message Date
Leonardo de Moura
660b9299ad refactor(kernel): (de)serialization procedures don't need to be in the kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 17:23:36 -07:00
Leonardo de Moura
1be758e4ef feat(library/resolve_macro.cpp): add macro to encode propositional resolution proofs compactly
This is also a test for the macro_definition infrastructure that we have in the kernel.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:11 -07:00