feat(kernel): add weight to kernel definitions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(conversion): add more conversion tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
add(numerics): add prime number generator/iterator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(numerics): add test to make sure that zeros of different precision mpfp numbers are the equal.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(numerics): add zero() method to all numeric_traits

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(style): fix warnings produced by cpplint.py, disable sizeof(type) warning

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(numerics): add is_prime function

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(numerics): add gcd and extended gcd templates (for primitive types)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(numerics): problem with gcd tests on OSX

Now, we only test gcd(a, b) for a != b && a != 0 && b != 0.
When one of these conditions do not hold, the result is implementation dependent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(numerics): add finite field Z/pZ

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(numerics/zpz): add numeric_traits for zpz numerals

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(numerics): rename power operator to pow, the idea is to follow the C/C++ name convention for the power operator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(interval): organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(interval): move interval unit tests to tests/util/interval

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(polynomial): add multivariate polynomials

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(metavar): reorganize and simplify metavariables

- Use hierarchical names instead of unsigned integers to identify metavariables.
- Associate type with metavariable.
- Replace metavar_env with substitution.
- Rename meta_ctx --> local_ctx
- Rename meta_entry --> local_entry
- Disable old elaborator
- Rename unification_problems to unification_constraints
- Add metavar_generator
- Fix metavar unit tests
- Modify type checker to use metavar_generator
- Fix placeholder module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(metavar): encode two of the bad examples as unit tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel): add unification_constraint and trace objects to the kernel

Trace objects will be used to justify steps performed by engines such as the elaborator. We use them to implement non-chronological backtracking in the elaborator. They are also use to justify to the user why something did not work.

The unification constraints are in the kernel because the type checker may create them when type checking a term containing metavariables.

Remark: a minimalistic kernel does not need to include metavariables, unification constraints, nor trace objects. We include these objects in our kernel to minimize code duplication.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel): move printer and formatter objects to the kernel

The printer and formatter objects are not trusted code.
We moved them to the kernel to be able to provide them as an argument to the trace objects.
Another motivation is to eliminate the kernel_exception_formatter hack.
With the formatter in the kernel, we can implement the pretty printer for kernel exceptions as a virtual method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel_exception): delete kernel_exception_formatter, and implement kernel_exception pretty printer as a virtual method

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