chore(kernel/inductive): cleanup code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(util/rb_tree): cleanup code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/constraint): remove choice constraints from the kernel, the kernel does not use them, we will implement them in elaborator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/trie): add value() method

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library): add token set

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/lua): add helper functions for checking expected number of arguments in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): improve argument validation in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/level): add workaround for clang++ bug: memory leak at thread_local

The fix has an advantage. There is only one copy of level Zero in the system even when multiple threads are used.
Moreover, it does no require any form of synchronization, and modules can be initialized in any order.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util): add lru cache

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/stackinfo): make sure check_stack can be invoked before 'main' (i.e., during initialization)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/lru_cache): typo

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/placeholder): use different names for different placeholders, it is bad design to assume that two structurally identical expressions are different when they are allocated twice (this design is not compatible with any form of hash-consing

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/aliases): it is bad design to instantiate parameter using the parameter name, the parameter names have no semantic value

Moreover, we could create type incorrect aliases by "accident".

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/expr): add optional expression caching (aka "partial" hash-consing)

We do not enforce full hash-consing because we would need to synchronize
the access to the hashtable/cache.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(kernel/expr_eq_fn): delay cache allocation

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(kernel/expr): cleanup

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(doc/lua): typo

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): expose replace_fn in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): expose instantiate_levels

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
doc(doc/lua): add universe polymorphism elimator example

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>