Fix bug in type checker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add more environment tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add more builtin constants

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Simplify how universe variable constraints are represented in the kernel. Allow universe variable to be created without an environment.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Fix test failure when using clang++ and release mode

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add basic definitions and axioms

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add subst proof rule. Define symm and trans using subst.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Require GMP version 5.0.5
Add a wrapper for MPFR
Add mpfp
add mpfp as friend class
add mpfp to cmakelists