Add SMT expression smart pointer

This is a smart pointer to share SMT expressions. This also gives
us flexibility to change the implementation of how this sharing is
achieved and what functions can be called. For example, expressions
can only be directly encoded through the UnsafeExprPtr class. This
marks the feature as unsafe and requires an explicit cast from the
type-safe ExprPtr<T> class.