Support hash consing

Hash consing refers to algorithms that guarantee perfect
sharing of syntactically equal expressions. Most symbolic
execution tools that implement hash consing seem to make
strong assumptions about the distribution of hash values.
This implementation assumes very little and it specifically
designed to handle hash collision. This is important to
ensure correct verification results.

Furthermore, unlike other symbolic execution tools, native
symbolic execution can use templates to statically allocate
a hash table for each expression type T, ExprStore<T>.
The benefits of this are at least threefold:

1) It is more likely to find a good hash function for each
   individual expression type T than having to design one
   that works equally well for all expression types.
2) It is possible to efficiently design expressions such
   that they are are evicted from the hash table as soon
   as their destructor is called.
3) make_shared_expr<T> and ExprStore<T> can directly call
   member functions of Expr subclasses without polymorphism.

Point (1) may lead to future performance improvements.

Point (2) helps us to maintain a low memory footprint;
however, it requires a careful design of ExprStore<T>
whose destructor is written in such a way that its hash
table can have static storage duration despite the fact
that expressions maintain a pointer to it. To see the
challenges of this, recall the undefined behaviour of
C++ concerning statically allocated memory across
different translation units.

The last point (3), in turn, is important to handle things
like hash collision where we need to check the equality of
symbolic expressions instead of merely their hash values.